--- a/progs/Matcher.thy	Sun May 21 07:35:35 2017 +0100
+++ b/progs/Matcher.thy	Wed May 31 09:14:39 2017 +0100
@@ -6,8 +6,8 @@
 section {* Regular Expressions *}
 
 datatype rexp =
-  NULL
-| EMPTY
+  ZERO
+| ONE
 | CHAR char
 | SEQ rexp rexp
 | ALT rexp rexp
@@ -63,8 +63,8 @@
 fun
   L :: "rexp \<Rightarrow> string set"
 where
-  "L (NULL) = {}"
-| "L (EMPTY) = {[]}"
+  "L (ZERO) = {}"
+| "L (ONE) = {[]}"
 | "L (CHAR c) = {[c]}"
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
@@ -75,180 +75,61 @@
 fun
  nullable :: "rexp \<Rightarrow> bool"
 where
-  "nullable (NULL) = False"
-| "nullable (EMPTY) = True"
+  "nullable (ZERO) = False"
+| "nullable (ONE) = True"
 | "nullable (CHAR c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (STAR r) = True"
 
-fun
- noccurs :: "rexp \<Rightarrow> bool"
-where
-  "noccurs (NULL) = True"
-| "noccurs (EMPTY) = False"
-| "noccurs (CHAR c) = False"
-| "noccurs (ALT r1 r2) = (noccurs r1 \<or> noccurs r2)"
-| "noccurs (SEQ r1 r2) = (noccurs r1 \<or> noccurs r2)"
-| "noccurs (STAR r) = (noccurs r)"
 
-lemma
-  "\<not> noccurs r \<Longrightarrow> L r \<noteq> {}"
-apply(induct r)
-apply(auto simp add: Seq_def)
-done
-
-lemma
-  "L r = {} \<Longrightarrow> noccurs r"
-apply(induct r)
-apply(auto simp add: Seq_def)
-done
-
-lemma does_not_hold:
-  "noccurs r \<Longrightarrow> L r = {}"
-apply(induct r)
-apply(auto simp add: Seq_def)
-oops
-
-fun
- der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
-where
-  "der c (NULL) = NULL"
-| "der c (EMPTY) = NULL"
-| "der c (CHAR c') = (if c = c' 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)"
-
-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 {* Correctness Proof of the Matcher *}
+section {* Correctness Proof for Nullable *}
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-by (induct r) (auto simp add: Seq_def) 
-section {* Left-Quotient of a Set *}
-
-fun
- zeroable :: "rexp \<Rightarrow> bool"
-where
-  "zeroable (NULL) = True"
-| "zeroable (EMPTY) = False"
-| "zeroable (CHAR c) = False"
-| "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
-| "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
-| "zeroable (STAR r) = False"
-
-
-lemma zeroable_correctness:
-  shows "zeroable r  \<longleftrightarrow>  (L r = {})"
 apply(induct r)
-apply(auto simp add: Seq_def)[6]
-done
-
-section {* Left-Quotient of a Set *}
-
-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_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)
+(* ZERO case *)
+apply(simp only: nullable.simps)
+apply(simp only: L.simps)
+apply(simp)
+(* ONE case *)
+apply(simp only: nullable.simps)
+apply(simp only: L.simps)
+apply(simp)
+(* CHAR case *)
+apply(simp only: nullable.simps)
+apply(simp only: L.simps)
+apply(simp)
+prefer 2
+(* ALT case *)
+apply(simp (no_asm) only: nullable.simps)
+apply(simp only:)
+apply(simp only: L.simps)
+apply(simp)
+(* SEQ case *)
+oops
 
-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 der_correctness:
-  shows "L (der c r) = Der c (L r)"
-by (induct r) 
-   (simp_all add: nullable_correctness)
-
-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)
-
-section {* Examples *}
-
-definition 
-  "CHRA \<equiv> CHAR (CHR ''a'')"
+lemma nullable_correctness:
+  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
+apply(induct r)
+apply(simp_all)
+(* all easy subgoals are proved except the last 2 *)
+(* where the definition of Seq needs to be unfolded. *)
+oops
 
-definition 
-  "ALT1 \<equiv> ALT CHRA EMPTY"
-
-definition 
-  "SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1"
-
-value "matcher SEQ3 ''aaa''"
+lemma nullable_correctness:
+  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
+apply(induct r)
+apply(simp_all add: Seq_def)
+(* except the star case every thing is proved *)
+(* we need to use the rule for Star.start *)
+oops
 
-value "matcher NULL []"
-value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"
-value "matcher (CHAR a) [a,a]"
-value "matcher (STAR (CHAR a)) []"
-value "matcher (STAR (CHAR a))  [a,a]"
-value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"
-value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"
-
-section {* Incorrect Matcher - fun-definition rejected *}
-
-fun
-  match :: "rexp list \<Rightarrow> string \<Rightarrow> bool"
-where
-  "match [] [] = True"
-| "match [] (c # s) = False"
-| "match (NULL # rs) s = False"  
-| "match (EMPTY # rs) s = match rs s"
-| "match (CHAR c # rs) [] = False"
-| "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)"         
-| "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)" 
-| "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s"
-| "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)"
+lemma nullable_correctness:
+  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
+apply(induct r)
+apply(simp_all add: Seq_def Star.start)
+done
 
 
 end    
\ No newline at end of file