theory Matcher2
  imports "Main" 
begin

lemma Suc_Union:
  "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))"
by (metis UN_insert atMost_Suc)

lemma Suc_reduce_Union:
  "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)


section \<open>Regular Expressions\<close>

datatype rexp =
  NULL
| EMPTY
| CH char
| SEQ rexp rexp
| ALT rexp rexp
| STAR rexp
| NOT rexp
| PLUS rexp
| OPT rexp
| NTIMES rexp nat
| NMTIMES rexp nat nat
| UPNTIMES rexp nat


section \<open>Sequential Composition of Sets\<close>

definition
  Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
where 
  "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"

text \<open>Two Simple Properties about Sequential Composition\<close>

lemma seq_empty [simp]:
  shows "A ;; {[]} = A"
  and   "{[]} ;; A = A"
by (simp_all add: Seq_def)

lemma seq_null [simp]:
  shows "A ;; {} = {}"
  and   "{} ;; A = {}"
by (simp_all add: Seq_def)

lemma seq_union:
  shows "A ;; (B \<union> C) = A ;; B \<union> A ;; C"
  and   "(B \<union> C) ;; A = B ;; A \<union> C ;; A"
by (auto simp add: Seq_def)

lemma seq_Union:
  shows "A ;; (\<Union>x\<in>B. C x) = (\<Union>x\<in>B. A ;; C x)"
by (auto simp add: Seq_def)

lemma seq_empty_in [simp]:
  "[] \<in> A ;; B \<longleftrightarrow> ([] \<in> A \<and> [] \<in> B)"
by (simp add: Seq_def)

lemma seq_assoc: 
  shows "A ;; (B ;; C) = (A ;; B) ;; C" 
apply(auto simp add: Seq_def)
apply(metis append_assoc)
apply(metis)
done


section \<open>Power for Sets\<close>

fun 
  pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101)
where
   "A \<up> 0 = {[]}"
|  "A \<up> (Suc n) = A ;; (A \<up> n)"

lemma pow_empty [simp]:
  shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
by (induct n) (auto)

lemma pow_plus:
  "A \<up> (n + m) = A \<up> n ;; A \<up> m"
by (induct n) (simp_all add: seq_assoc)

section \<open>Kleene Star for Sets\<close>

inductive_set
  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
  for A :: "string set"
where
  start[intro]: "[] \<in> A\<star>"
| step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"

text \<open>A Standard Property of Star\<close>

lemma star_decomp: 
  assumes a: "c # x \<in> A\<star>" 
  shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
using a 
using a
by (induct x\<equiv>"c # x" rule: Star.induct) 
   (auto simp add: append_eq_Cons_conv)

lemma star_cases:
  shows "A\<star> = {[]} \<union> A ;; A\<star>"
unfolding Seq_def 
by (auto) (metis Star.simps)

lemma Star_in_Pow:
  assumes a: "s \<in> A\<star>"
  shows "\<exists>n. s \<in> A \<up> n"
using a
apply(induct)
apply(auto)
apply(rule_tac x="Suc n" in exI)
apply(auto simp add: Seq_def)
done

lemma Pow_in_Star:
  assumes a: "s \<in> A \<up> n"
  shows "s \<in> A\<star>"
using a
by (induct n arbitrary: s) (auto simp add: Seq_def)


lemma Star_def2: 
  shows "A\<star> = (\<Union>n. A \<up> n)"
using Star_in_Pow Pow_in_Star
by (auto)


section \<open>Semantics of Regular Expressions\<close>
 
fun
  L :: "rexp \<Rightarrow> string set"
where
  "L (NULL) = {}"
| "L (EMPTY) = {[]}"
| "L (CH c) = {[c]}"
| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
| "L (STAR r) = (L r)\<star>"
| "L (NOT r) = UNIV - (L r)"
| "L (PLUS r) = (L r) ;; ((L r)\<star>)"
| "L (OPT r) = (L r) \<union> {[]}"
| "L (NTIMES r n) = (L r) \<up> n"
| "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
| "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"

lemma "L (NOT NULL) = UNIV"
apply(simp)
done

section \<open>The Matcher\<close>

fun
 nullable :: "rexp \<Rightarrow> bool"
where
  "nullable (NULL) = False"
| "nullable (EMPTY) = True"
| "nullable (CH c) = False"
| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
| "nullable (STAR r) = True"
| "nullable (NOT r) = (\<not>(nullable r))"
| "nullable (PLUS r) = (nullable r)"
| "nullable (OPT r) = True"
| "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
| "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
| "nullable (UPNTIMES r n) = True"

fun M :: "rexp \<Rightarrow> nat"
where
  "M (NULL) = 0"
| "M (EMPTY) = 0"
| "M (CH char) = 0"
| "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
| "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
| "M (STAR r) = Suc (M r)"
| "M (NOT r) = Suc (M r)"
| "M (PLUS r) = Suc (M r)"
| "M (OPT r) = Suc (M r)"
| "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
| "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
| "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"

function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
where
  "der c (NULL) = NULL"
| "der c (EMPTY) = NULL"
| "der c (CH d) = (if c = d then EMPTY else NULL)"
| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
| "der c (STAR r) = SEQ (der c r) (STAR r)"
| "der c (NOT r) = NOT(der c r)"
| "der c (PLUS r) = SEQ (der c r) (STAR r)"
| "der c (OPT r) = der c r"
| "der c (NTIMES r 0) = NULL"
| "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
| "der c (NMTIMES r n m) = 
        (if m < n then NULL else 
        (if n = m then der c (NTIMES r n) else
                       ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
| "der c (UPNTIMES r 0) = NULL"
| "der c (UPNTIMES r (Suc n)) = der c (ALT (NTIMES r (Suc n)) (UPNTIMES r n))"
by pat_completeness auto

lemma bigger1:
  "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b"
by (metis le0 mult_strict_mono')

termination der 
apply(relation "measure (\<lambda>(c, r). M r)") 
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(simp_all del: M.simps)
apply(simp_all only: M.simps)
defer
defer
defer
apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
prefer 2
     apply(auto)[1]

(*
apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
prefer 2
apply(auto)[1]
apply(subgoal_tac "Suc n < Suc m")
prefer 2
apply(auto)[1]
apply(subgoal_tac "Suc (M r) * 2 * Suc n < Suc (Suc (M r)) * 2 * Suc m")
prefer 2
apply(subgoal_tac "Suc (M r) * 2 < Suc (Suc (M r)) * 2")
prefer 2
apply(auto)[1]
apply(rule bigger1)
apply(assumption)
apply(simp)
apply (metis zero_less_Suc)
apply (metis mult_is_0 neq0_conv old.nat.distinct(2))
apply(rotate_tac 4)
apply(drule_tac a="1" and b="(Suc (Suc m) - Suc n)" in bigger1)
prefer 4
apply(simp)
apply(simp)
apply (metis zero_less_one)
apply(simp)
done
*)
sorry

fun 
 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
where
  "ders [] r = r"
| "ders (c # s) r = ders s (der c r)"

fun
  matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool"
where
  "matcher r s = nullable (ders s r)"


section \<open>Correctness Proof of the Matcher\<close>

lemma nullable_correctness:
  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
apply(induct r) 
apply(auto simp add: Seq_def) 
done

section \<open>Left-Quotient of a Set\<close>

definition
  Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
where
  "Der c A \<equiv> {s. [c] @ s \<in> A}"

lemma Der_null [simp]:
  shows "Der c {} = {}"
unfolding Der_def
by auto

lemma Der_empty [simp]:
  shows "Der c {[]} = {}"
unfolding Der_def
by auto

lemma Der_char [simp]:
  shows "Der c {[d]} = (if c = d then {[]} else {})"
unfolding Der_def
by auto

lemma Der_union [simp]:
  shows "Der c (A \<union> B) = Der c A \<union> Der c B"
unfolding Der_def
by auto

lemma Der_insert_nil [simp]:
  shows "Der c (insert [] A) = Der c A"
unfolding Der_def 
by auto 

lemma Der_seq [simp]:
  shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
unfolding Der_def Seq_def
by (auto simp add: Cons_eq_append_conv)

lemma Der_star [simp]:
  shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
proof -    
  have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
    by (simp only: star_cases[symmetric])
  also have "... = Der c (A ;; A\<star>)"
    by (simp only: Der_union Der_empty) (simp)
  also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
    by simp
  also have "... =  (Der c A) ;; A\<star>"
    unfolding Seq_def Der_def
    by (auto dest: star_decomp)
  finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
qed

lemma test:
  assumes "[] \<in> A"
  shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)"
  using assms
  apply(induct n)
   apply(simp)
  apply(simp)
  apply(auto simp add: Der_def Seq_def)
  apply blast
  by force

lemma Der_ntimes [simp]:
  shows "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
proof -    
  have "Der c (A  \<up> (Suc n)) = Der c (A ;; A \<up> n)"
    by(simp)
  also have "... = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
    by simp
  also have "... =  (Der c A) ;; (A \<up> n)"
    using test by force
  finally show "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" .
qed



lemma Der_UNIV [simp]:
  "Der c (UNIV - A) = UNIV - Der c A"
unfolding Der_def
by (auto)

lemma Der_pow [simp]:
  shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
unfolding Der_def 
by(auto simp add: Cons_eq_append_conv Seq_def)

lemma Der_UNION [simp]: 
  shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
  by (auto simp add: Der_def)

lemma if_f:
  shows "f(if B then C else D) = (if B then f(C) else f(D))"
  by simp


lemma der_correctness:
  shows "L (der c r) = Der c (L r)"
proof(induct r)
  case NULL
  then show ?case by simp
next
  case EMPTY
  then show ?case by simp
next
  case (CH x)
  then show ?case by simp
next
  case (SEQ r1 r2)
  then show ?case
    by (simp add: nullable_correctness) 
next
  case (ALT r1 r2)
  then show ?case by simp
next
  case (STAR r)
  then show ?case
    by simp 
next
  case (NOT r)
  then show ?case by simp
next
  case (PLUS r)
  then show ?case by simp
next
  case (OPT r)
  then show ?case by simp
next
  case (NTIMES r n)
  then show ?case
    apply(induct n)
     apply(simp)
    apply(simp only: L.simps)
    apply(simp only: Der_pow)
    apply(simp only: der.simps L.simps)
    apply(simp only: nullable_correctness)
    apply(simp only: if_f)
    by simp
next
  case (NMTIMES r n m)
  then show ?case 
    apply(case_tac n)
    sorry
next
  case (UPNTIMES r x2)
  then show ?case sorry
qed




lemma der_correctness:
  shows "L (der c r) = Der c (L r)"
apply(induct rule: der.induct) 
apply(simp_all add: nullable_correctness 
    Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
apply(rule impI)+
apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
apply(auto simp add: Seq_def)
done

lemma L_der_NTIMES:
  shows "L(der c (NTIMES r n)) = L (if n = 0 then NULL else if nullable r then 
         SEQ (der c r) (UPNTIMES r (n - 1)) else SEQ (der c r) (NTIMES r (n - 1)))"
apply(induct n)
apply(simp)
apply(simp)
apply(auto)
apply(auto simp add: Seq_def)
apply(rule_tac x="s1" in exI)
apply(simp)
apply(rule_tac x="xa" in bexI)
apply(simp)
apply(simp)
apply(rule_tac x="s1" in exI)
apply(simp)
by (metis Suc_pred atMost_iff le_Suc_eq)

lemma "L(der c (UPNTIMES r 0)) = {}"
by simp

lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
proof(induct n)
  case 0 show ?case by simp
next
  case (Suc n)
  have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
  { assume a: "nullable r"
    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
    by (simp only: der_correctness)
    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
    by(simp only: L.simps Suc_Union)
    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
    by (simp only: der_correctness)
    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
    by(auto simp add: Seq_def)
    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
    using IH by simp
    also have "... = L (SEQ (der c r) (UPNTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
    using a unfolding L_der_NTIMES by simp
    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
    by (auto, metis Suc_Union Un_iff seq_Union)
    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
    } 
  moreover
  { assume a: "\<not>nullable r"
    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
    by (simp only: der_correctness)
    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
    by(simp only: L.simps Suc_Union)
    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
    by (simp only: der_correctness)
    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
    by(auto simp add: Seq_def)
    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
    using IH by simp
    also have "... = L (SEQ (der c r) (NTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
    using a unfolding L_der_NTIMES by simp
    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
    by (simp add: Suc_Union seq_union(1))
    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
  }
  ultimately  
  show "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))"
  by blast
qed

lemma matcher_correctness:
  shows "matcher r s \<longleftrightarrow> s \<in> L r"
by (induct s arbitrary: r)
   (simp_all add: nullable_correctness der_correctness Der_def)

end