Derivative.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 ⇒ 't regexp ⇒ bool"
  (infix "=~" 60)
  where
    MEmpty: "[] =~ EmptyStr" |
    MChar: "[x] =~ Char x" |
    MApp: "⟦x1 =~ e1; x2 =~ e2⟧ ⟹ x1 @ x2 =~ App e1 e2" |
    MUnionL: "x =~ e1 ⟹ x =~ Union e1 e2" |
    MUnionR: "x =~ e2 ⟹ x =~ Union e1 e2" |
    MStar0: "[] =~ Star e" |
    MStarApp: "⟦x1 =~ e; x2 =~ Star e⟧ ⟹ x1 @ x2 =~ Star e"

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

fun match_empty :: "'t regexp ⇒ bool" where
  "match_empty EmptySet = False" |
  "match_empty EmptyStr = True" |
  "match_empty (Char _) = False" |
  "match_empty (App e1 e2) ⟷ match_empty e1 ∧ match_empty e2" |
  "match_empty (Union e1 e2) ⟷ match_empty e1 ∨ match_empty e2" |
  "match_empty (Star e) = True"

lemma empty_lemma: "match_empty e ⟷ [] =~ e"
proof (induction e)
  case EmptySet
  then show ?case using matchE by auto
next
  case EmptyStr
  then show ?case using MEmpty by auto
next
  case (Char x)
  then show ?case using matchE by auto
next
  case (App e1 e2)
  show ?case
  proof
    show "match_empty (App e1 e2) ⟹ [] =~ App e1 e2"
      using App.IH MApp by fastforce
  next
    show "[] =~ App e1 e2 ⟹ match_empty (App e1 e2)"
      using App.IH matchE by auto
  qed
next
  case (Union e1 e2)
  show ?case
  proof
    show "match_empty (Union e1 e2) ⟹ [] =~ Union e1 e2"
      using Union.IH MUnionL MUnionR by fastforce
  next
    show "[] =~ Union e1 e2 ⟹ match_empty (Union e1 e2)"
      using Union.IH matchE by auto
  qed
next
  case (Star e)
  then show ?case using MStar0 by auto
qed

fun derivative :: "'t ⇒ 't regexp ⇒ 't regexp" where
  "derivative _ EmptySet = EmptySet" |
  "derivative _ EmptyStr = EmptySet" |
  "derivative a (Char b) = (if a = b then EmptyStr else EmptySet)" |
  "derivative a (App e1 e2) =
    (if match_empty e1 then
      Union (App (derivative a e1) e2) (derivative a e2)
    else
      App (derivative a e1) e2)" |
  "derivative a (Union e1 e2) = Union (derivative a e1) (derivative a e2)" |
  "derivative a (Star e) = App (derivative a e) (Star e)"

lemma [intro]: "s =~ derivative a e ⟹ a # s =~ e"
proof (induction e arbitrary: s)
  case EmptySet
  then show ?case using matchE by auto
next
  case EmptyStr
  then show ?case using matchE by auto
next
  case (Char x)
  then show ?case
    apply (case_tac "a = x")
    using MChar matchE apply force
    using matchE by auto
next
  case (App e1 e2)
  have lem: "s =~ App (derivative a e1) e2 ⟹ a # s =~ App e1 e2"
  proof -
    assume "s =~ App (derivative a e1) e2"
    then obtain s1 s2 where
      "s = s1 @ s2"
      "s1 =~ derivative a e1"
      "s2 =~ e2"
      by (rule matchE, auto)
    then show ?thesis using App.IH(1) MApp by fastforce
  qed
  
  show "s =~ derivative a (App e1 e2) ⟹ ?case"
    apply (case_tac "match_empty e1")
     apply (simp_all)
  proof (rule matchE, auto)
    assume "s =~ App (derivative a e1) e2"
    then show ?thesis using lem by auto
  next
    assume "s =~ derivative a e2"
    then have "a # s =~ e2" using App.IH(2) by simp
    then show "⟦match_empty e1; s =~ derivative a e2⟧ ⟹ a # s =~ App e1 e2"
      using MApp empty_lemma by fastforce
  next
    assume "s =~ App (derivative a e1) e2"
    then show ?thesis using lem by auto
  qed
next
  case (Union e1 e2)
  assume "s =~ derivative a (Union e1 e2)"
  then have "s =~ derivative a e1 ∨ s =~ derivative a e2" using matchE by auto
  then show ?case using MUnionL MUnionR Union.IH(1) Union.IH(2) by blast
next
  case (Star e)
  assume "s =~ derivative a (Star e)"
  then obtain s1 s2 where
    "s = s1 @ s2"
    "s1 =~ derivative a e"
    "s2 =~ Star e"
    by (rule matchE, auto)
  then show ?case using Star.IH MStarApp by force
qed

fun kleene :: "nat ⇒ 't regexp ⇒ 't list set" where
  "kleene 0 _ = {[]}" |
  "kleene (Suc n) e = { u @ v | u v. u =~ e ∧ v ∈ kleene n e }"

lemma kleene_star[intro]: "s ∈ kleene n e ⟹ s =~ Star e"
proof (induction n arbitrary: s)
  case 0
  then have "s = []" by auto
  then show ?case using MStar0 by auto
next
  case (Suc n)
  then obtain u v where
    "s = u @ v"
    "u =~ e"
    "v ∈ kleene n e"
    by auto
  then have "v =~ Star e" using Suc.IH by auto
  then show ?case using ‹s = u @ v› ‹u =~ e› MStarApp by auto
qed

lemma kleene_star_iff: "s =~ Star e ⟷ (∃n. s ∈ kleene n e)"
proof
  show "s =~ Star e ⟹ ∃n. s ∈ kleene n e"
  proof (induction "s" "Star e" rule: match_regexp.induct)
    have "[] ∈ kleene 0 e" by auto
    then show "∃n. [] ∈ kleene n e" by blast
  next
    fix x1 x2
    assume "∃n. x2 ∈ kleene n e"
    then obtain n where "x2 ∈ kleene n e" by auto
    moreover assume "x1 =~ e"
    then have "x1 @ x2 ∈ kleene (Suc n) e" using calculation by auto
    ultimately show "∃n. x1 @ x2 ∈ kleene n e" by blast
  qed
next
  assume "∃n. s ∈ kleene n e"
  then obtain n where "s ∈ kleene n e" by auto
  then show "s =~ Star e" by auto
qed

lemma split_kleene[intro]: "⟦s ∈ kleene n e; s ≠ []⟧ ⟹ ∃s1 s2. s = s1 @ s2 ∧ s1 =~ e ∧ s2 =~ Star e ∧ s1 ≠ []"
proof (induction n arbitrary: s)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then obtain u v where
    "s = u @ v"
    "u =~ e"
    "v ∈ kleene n e"
    by auto
  then show ?case
  proof (cases "u = []")
    case True
    moreover have "v ≠ []" using Suc.prems(2) ‹s = u @ v› calculation by blast
    moreover obtain s1 s2 where
      "v = s1 @ s2"
      "s1 =~ e"
      "s2 =~ Star e"
      "s1 ≠ []"
      using Suc.IH calculation ‹v ∈ kleene n e› by blast
    ultimately show ?thesis using ‹s = u @ v› by auto
  next
    case False
    moreover have "v =~ Star e" using ‹v ∈ kleene n e› by blast
    ultimately show ?thesis using ‹s = u @ v› ‹u =~ e› by blast
  qed
qed

lemma productive: "a # s =~ Star e ⟹ ∃s1 s2. s = s1 @ s2 ∧ a # s1 =~ e ∧ s2 =~ Star e"
proof -
  assume "a # s =~ Star e"
  then obtain s1 s2 where
    "a # s = s1 @ s2"
    "s1 =~ e"
    "s2 =~ Star e"
    "s1 ≠ []"
    by (metis kleene_star_iff list.distinct(1) split_kleene)
  moreover obtain s1' where
    "a # s1' = s1"
    by (meson Cons_eq_append_conv calculation)
  ultimately have "s = s1' @ s2 ∧ a # s1' =~ e ∧ s2 =~ Star e" by auto
  then show ?thesis by auto
qed

lemma [intro]: "a # s =~ e ⟹ s =~ derivative a e"
proof (induction e arbitrary: s)
  case EmptySet
  then show ?case using matchE by auto
next
  case EmptyStr
  then show ?case using matchE by auto
next
  case (Char x)
  then have "a = x" and "s = []" using matchE by auto
  then show ?case by (simp add: MEmpty)
next
  case (App e1 e2)
  show "a # s =~ App e1 e2 ⟹ ?case"
  proof (erule matchE, auto)
      fix x1 x2
      assume "a # s = x1 @ x2"
             "x1 =~ e1"
             "x2 =~ e2"
    then show "s =~ Union (App (derivative a e1) e2) (derivative a e2)"
    proof (cases "x1 = []")
      case True
      then show ?thesis by (simp add: App.IH(2) MUnionR ‹a # s = x1 @ x2› ‹x2 =~ e2›)
    next
      case False
      then show ?thesis
        by (metis App.IH(1) MApp MUnionL ‹a # s = x1 @ x2› 
            ‹x1 =~ e1› ‹x2 =~ e2› append_eq_Cons_conv)
    qed
  next
    fix x1 x2
    assume "a # s = x1 @ x2"
           "x1 =~ e1"
           "x2 =~ e2"
           "¬match_empty e1"
    moreover have "x1 ≠ []" using empty_lemma calculation by auto
    ultimately show "s =~ App (derivative a e1) e2"
      by (metis App.IH(1) MApp append_eq_Cons_conv) 
  qed
next
  case (Union e1 e2)
  show "a # s =~ Union e1 e2 ⟹ ?case"
  proof (erule matchE, auto)
    assume "a # s =~ e1"
    then have "s =~ derivative a e1" using Union.IH by auto
    then show "s =~ Union (derivative a e1) (derivative a e2)" using MUnionL by auto
  next
    assume "a # s =~ e2"
    then have "s =~ derivative a e2" using Union.IH by auto
    then show "s =~ Union (derivative a e1) (derivative a e2)" using MUnionR by auto 
  qed
next
  case (Star e)
  assume "a # s =~ Star e"
  then have "∃s1 s2. a # s1 =~ e ∧ s2 =~ Star e ∧ s = s1 @ s2" using productive by fastforce
  then obtain s1 s2 where
    "a # s1 =~ e"
    "s2 =~ Star e"
    "s = s1 @ s2"
    by auto
  moreover have "s1 =~ derivative a e" using Star.IH calculation by auto
  moreover have "a # s1 @ s2 =~ Star e" using Star.prems calculation by auto
  ultimately show "a # s =~ Star e ⟹ s =~ derivative a (Star e)"
    by (simp add: MApp)
qed

fun match_deriv :: "'t list ⇒ 't regexp ⇒ bool" where
  "match_deriv [] e ⟷ match_empty e" |
  "match_deriv (a # s) e ⟷ match_deriv s (derivative a e)"

lemma "match_deriv s e ⟷ s =~ e"
proof
  show "match_deriv s e ⟹ s =~ e"
  proof (induction s arbitrary: e)
    case Nil
    then show ?case using empty_lemma by auto
  next
    case (Cons a s)
    have "match_deriv s (derivative a e)" using Cons.prems by simp
    then have "s =~ derivative a e" using Cons.IH by auto
    then show ?case by auto
  qed
next
  show "s =~ e ⟹ match_deriv s e"
  proof (induction s arbitrary: e)
    case Nil
    then show ?case using empty_lemma by auto
  next
    case (Cons a s)
    assume "a # s =~ e"
    then have "s =~ derivative a e" by auto
    then have "match_deriv s (derivative a e)" using Cons.IH by auto
    then show ?case by simp
  qed
qed

end