theory Matcher2 imports "Main" beginlemma 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 natsection \<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)donesection \<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 aby (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 aapply(induct)apply(auto)apply(rule_tac x="Suc n" in exI)apply(auto simp add: Seq_def)donelemma Pow_in_Star: assumes a: "s \<in> A \<up> n" shows "s \<in> A\<star>"using aby (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_Starby (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)donesection \<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 autolemma 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)deferdeferdeferapply(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 2apply(auto)[1]apply(subgoal_tac "Suc n < Suc m")prefer 2apply(auto)[1]apply(subgoal_tac "Suc (M r) * 2 * Suc n < Suc (Suc (M r)) * 2 * Suc m")prefer 2apply(subgoal_tac "Suc (M r) * 2 < Suc (Suc (M r)) * 2")prefer 2apply(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 4apply(simp)apply(simp)apply (metis zero_less_one)apply(simp)done*)sorryfun 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) donesection \<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_defby autolemma Der_empty [simp]: shows "Der c {[]} = {}"unfolding Der_defby autolemma Der_char [simp]: shows "Der c {[d]} = (if c = d then {[]} else {})"unfolding Der_defby autolemma Der_union [simp]: shows "Der c (A \<union> B) = Der c A \<union> Der c B"unfolding Der_defby autolemma 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_defby (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>" .qedlemma 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 forcelemma 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)" .qedlemma Der_UNIV [simp]: "Der c (UNIV - A) = UNIV - Der c A"unfolding Der_defby (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 simplemma der_correctness: shows "L (der c r) = Der c (L r)"proof(induct r) case NULL then show ?case by simpnext case EMPTY then show ?case by simpnext case (CH x) then show ?case by simpnext case (SEQ r1 r2) then show ?case by (simp add: nullable_correctness) next case (ALT r1 r2) then show ?case by simpnext case (STAR r) then show ?case by simp next case (NOT r) then show ?case by simpnext case (PLUS r) then show ?case by simpnext case (OPT r) then show ?case by simpnext 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 simpnext case (NMTIMES r n m) then show ?case apply(case_tac n) sorrynext case (UPNTIMES r x2) then show ?case sorryqedlemma 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)donelemma 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 simplemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"proof(induct n) case 0 show ?case by simpnext 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 blastqedlemma 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