Pumping.thy

theory Pumping
  imports Main
begin

datatype 't regexp =
  EmptySet
  | EmptyStr
  | Char 't
  | App "'t regexp" "'t regexp"
  | Union "'t regexp" "'t regexp"
  | Star "'t regexp"

inductive match_regexp 
  :: "'t list \<Rightarrow> 't regexp \<Rightarrow> bool"
  (infix "=~" 60)
  where
    MEmpty: "[] =~ EmptyStr" |
    MChar: "[x] =~ Char x" |
    MApp: "\<lbrakk>x1 =~ e1; x2 =~ e2\<rbrakk> \<Longrightarrow> x1 @ x2 =~ App e1 e2" |
    MUnionL: "x =~ e1 \<Longrightarrow> x =~ Union e1 e2" |
    MUnionR: "x =~ e2 \<Longrightarrow> x =~ Union e1 e2" |
    MStar0: "[] =~ Star e" |
    MStarApp: "\<lbrakk>x1 =~ e; x2 =~ Star e\<rbrakk> \<Longrightarrow> x1 @ x2 =~ Star e"

inductive_cases matchE: "s =~ e"
inductive_simps matchS: "s =~ e"

fun pumping_constant :: "'t regexp \<Rightarrow> nat" where
  "pumping_constant EmptySet = 0" |
  "pumping_constant EmptyStr = 1" |
  "pumping_constant (Char _) = 2" |
  "pumping_constant (App e1 e2) = pumping_constant e1 + pumping_constant e2" |
  "pumping_constant (Union e1 e2) = pumping_constant e1 + pumping_constant e2" |
  "pumping_constant (Star _) = 1"

fun napp :: "nat \<Rightarrow> 't list \<Rightarrow> 't list" where
  "napp n s = concat (replicate n s)"

lemma napp_star: "s =~ e \<Longrightarrow> napp n s =~ Star e"
proof (induction n)
  case 0
  then show ?case by (simp add: MStar0) 
next
  case (Suc n)
  then show ?case by (simp add: MStarApp)
qed

lemma pumping:
  "\<lbrakk>s =~ re; pumping_constant re \<le> length s\<rbrakk> \<Longrightarrow>
    \<exists>s1 s2 s3. s = s1 @ s2 @ s3 \<and> s2 \<noteq> [] \<and> (\<forall>m. s1 @ napp m s2 @ s3 =~ re)"
proof (induction rule: match_regexp.induct)
  case MEmpty
  then show ?case by simp
next
  case (MChar x)
  then show ?case by simp
next
  case (MApp x1 e1 x2 e2)
  moreover show ?case
  proof (rule disjE)
    show "pumping_constant e1 \<le> length x1 \<or> pumping_constant e2 \<le> length x2"
      using calculation(5) by auto
  next
    assume "pumping_constant e1 \<le> length x1"
    then obtain s1 s2 s3 where
      pump: "x1 = s1 @ s2 @ s3 \<and> s2 \<noteq> [] \<and> (\<forall>m. s1 @ napp m s2 @ s3 =~ e1)"
      using calculation(3) by auto
    
    have p1: "x1 @ x2 = s1 @ s2 @ (s3 @ x2)" using pump by auto
    have p2: "s2 \<noteq> []" using pump by auto
    have p3: "\<forall>m. s1 @ napp m s2 @ (s3 @ x2) =~ App e1 e2"
      using MApp(2) match_regexp.MApp pump by fastforce

    show ?thesis using p1 p2 p3 by blast
  next
    assume "pumping_constant e2 \<le> length x2"
    then obtain s1 s2 s3 where
      pump: "x2 = s1 @ s2 @ s3 \<and> s2 \<noteq> [] \<and> (\<forall>m. s1 @ napp m s2 @ s3 =~ e2)"
      using calculation(4) by auto
    
    have p1: "x1 @ x2 = (x1 @ s1) @ s2 @ s3" using pump by auto
    have p2: "s2 \<noteq> []" using pump by auto
    have p3: "\<forall>m. (x1 @ s1) @ napp m s2 @ s3 =~ App e1 e2"
      using calculation(1) match_regexp.MApp pump by fastforce

    show ?thesis using p1 p2 p3 by blast
  qed
next
  case (MUnionL x e1 e2)
  moreover have "pumping_constant e1 \<le> length x"
    using calculation(3) by auto
  then obtain s1 s2 s3 where
    pump: "x = s1 @ s2 @ s3 \<and> s2 \<noteq> [] \<and> (\<forall>m. s1 @ napp m s2 @ s3 =~ e1)"
    using calculation by auto
  show ?case using match_regexp.MUnionL pump by blast
next
  case (MUnionR x e2 e1)
  moreover have "pumping_constant e2 \<le> length x"
    using calculation(3) by auto
  then obtain s1 s2 s3 where
    pump: "x = s1 @ s2 @ s3 \<and> s2 \<noteq> [] \<and> (\<forall>m. s1 @ napp m s2 @ s3 =~ e2)"
    using calculation by auto
  show ?case using match_regexp.MUnionR pump by blast
next
  case (MStar0 e)
  then show ?case by simp
next
  case (MStarApp x1 e x2)
  then show ?case
  proof (cases x2)
    case Nil
    moreover have "x1 \<noteq> []" using calculation(1) MStarApp.prems by auto
    moreover have "x1 @ x2 = [] @ x1 @ []" using calculation(1) by auto
    moreover have "\<forall>m. [] @ napp m x1 @ [] =~ Star e" using MStarApp(1) napp_star by auto
    ultimately show ?thesis by blast
  next
    case (Cons a xs)
    then have "pumping_constant (Star e) \<le> length x2" by simp
    then obtain s1 s2 s3 where
      pump: "x2 = s1 @ s2 @ s3 \<and> s2 \<noteq> [] \<and> (\<forall>m. s1 @ napp m s2 @ s3 =~ Star e)"
      using MStarApp(4) by auto

    have p1: "x1 @ x2 = (x1 @ s1) @ s2 @ s3" using pump by auto
    have p2: "s2 \<noteq> []" using pump by auto
    have p3: "\<forall>m. (x1 @ s1) @ napp m s2 @ s3 =~ Star e"
      using MStarApp(1) pump match_regexp.MStarApp by auto
    
    show ?thesis using p1 p2 p3 by blast
  qed
qed

end