--- a/Matcher.thy	Thu Oct 07 05:30:21 2010 +0000
+++ b/Matcher.thy	Tue Oct 19 11:51:05 2010 +0000
@@ -68,7 +68,7 @@
 where
   "der c (NULL) = NULL"
 | "der c (EMPTY) = NULL"
-| "der c (CHAR c') = (if c=c' then EMPTY else 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)"
@@ -77,7 +77,7 @@
  derivative :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "derivative [] r = r"
-| "derivative (c#s) r = derivative s (der c r)"
+| "derivative (c # s) r = derivative s (der c r)"
 
 fun
   matches :: "rexp \<Rightarrow> string \<Rightarrow> bool"
@@ -92,29 +92,29 @@
 by (induct r) (auto) 
 
 lemma der_correctness:
-  shows "s \<in> L (der c r) \<longleftrightarrow> c#s \<in> L r"
+  shows "s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r"
 proof (induct r arbitrary: s)
   case (SEQ r1 r2 s)
-  have ih1: "\<And>s. s \<in> L (der c r1) \<longleftrightarrow> c#s \<in> L r1" by fact
-  have ih2: "\<And>s. s \<in> L (der c r2) \<longleftrightarrow> c#s \<in> L r2" by fact
-  show "s \<in> L (der c (SEQ r1 r2)) \<longleftrightarrow> c#s \<in> L (SEQ r1 r2)" 
+  have ih1: "\<And>s. s \<in> L (der c r1) \<longleftrightarrow> c # s \<in> L r1" by fact
+  have ih2: "\<And>s. s \<in> L (der c r2) \<longleftrightarrow> c # s \<in> L r2" by fact
+  show "s \<in> L (der c (SEQ r1 r2)) \<longleftrightarrow> c # s \<in> L (SEQ r1 r2)" 
     using ih1 ih2 by (auto simp add: nullable_correctness Cons_eq_append_conv)
 next
   case (STAR r s)
-  have ih: "\<And>s. s \<in> L (der c r) \<longleftrightarrow> c#s \<in> L r" by fact
-  show "s \<in> L (der c (STAR r)) \<longleftrightarrow> c#s \<in> L (STAR r)"
+  have ih: "\<And>s. s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r" by fact
+  show "s \<in> L (der c (STAR r)) \<longleftrightarrow> c # s \<in> L (STAR r)"
   proof
     assume "s \<in> L (der c (STAR r))"
     then have "s \<in> L (der c r) ; L r\<star>" by simp
-    then have "c#s \<in> L r ; (L r)\<star>" 
+    then have "c # s \<in> L r ; (L r)\<star>" 
       by (auto simp add: ih Cons_eq_append_conv)
-    then have "c#s \<in> (L r)\<star>" using lang_star_cases by auto
-    then show "c#s \<in> L (STAR r)" by simp
+    then have "c # s \<in> (L r)\<star>" using lang_star_cases by auto
+    then show "c # s \<in> L (STAR r)" by simp
   next
-    assume "c#s \<in> L (STAR r)"
-    then have "c#s \<in> (L r)\<star>" by simp
+    assume "c # s \<in> L (STAR r)"
+    then have "c # s \<in> (L r)\<star>" by simp
     then have "s \<in> L (der c r); (L r)\<star>"
-      by (induct x\<equiv>"c#s" rule: Star.induct)
+      by (induct x\<equiv>"c # s" rule: Star.induct)
          (auto simp add: ih append_eq_Cons_conv)
     then show "s \<in> L (der c (STAR r))" by simp  
   qed
@@ -141,14 +141,14 @@
   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)"
+| "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)"
 apply(pat_completeness)
 apply(auto)
 done