# HG changeset patch
# User urbanc
# Date 1287489065 0
# Node ID 074d9a4b2bc9466f775eb36f438ed9c8f8dbf420
# Parent  f20f391b21faa6677c3d6bbf4a49e8a6fb62e6a4
added a file about the easy closure properties of regular sets (the difficult parts, like complement, are missing)

diff -r f20f391b21fa -r 074d9a4b2bc9 Closure.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Closure.thy	Tue Oct 19 11:51:05 2010 +0000
@@ -0,0 +1,223 @@
+theory "RegSet"
+  imports "Main" 
+begin
+
+
+text {* Sequential composition of sets *}
+
+definition
+  lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
+where 
+  "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+
+
+section {* Kleene star for sets *}
+
+inductive_set
+  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
+  for L :: "string set"
+where
+  start[intro]: "[] \<in> L\<star>"
+| step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"
+
+
+text {* A standard property of star *}
+
+lemma lang_star_cases:
+  shows "L\<star> =  {[]} \<union> L ; L\<star>"
+proof
+  { fix x
+    have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>"
+      unfolding lang_seq_def
+    by (induct rule: Star.induct) (auto)
+  }
+  then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto
+next
+  show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>" 
+    unfolding lang_seq_def by auto
+qed
+
+
+lemma lang_star_cases2:
+  shows "[] \<notin> L \<Longrightarrow> L\<star> - {[]} =  L ; L\<star>"
+by (subst lang_star_cases)
+   (simp add: lang_seq_def)
+
+
+section {* Regular Expressions *}
+
+datatype rexp =
+  NULL
+| EMPTY
+| CHAR char
+| SEQ rexp rexp
+| ALT rexp rexp
+| STAR rexp
+
+
+section {* Semantics of Regular Expressions *}
+
+fun
+  L :: "rexp \<Rightarrow> string set"
+where
+  "L (NULL) = {}"
+| "L (EMPTY) = {[]}"
+| "L (CHAR 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>"
+
+abbreviation
+  CUNIV :: "string set"
+where
+  "CUNIV \<equiv> (\<lambda>x. [x]) ` (UNIV::char set)"
+
+lemma CUNIV_star_minus:
+  "(CUNIV\<star> - {[c]}) = {[]} \<union> (CUNIV - {[c]}; (CUNIV\<star>))"
+apply(subst lang_star_cases)
+apply(simp add: lang_seq_def)
+oops
+
+
+lemma string_in_CUNIV:
+  shows "s \<in> CUNIV\<star>"
+proof (induct s)
+  case Nil
+  show "[] \<in> CUNIV\<star>" by (rule start)
+next
+  case (Cons c s)
+  have "[c] \<in> CUNIV" by simp
+  moreover
+  have "s \<in> CUNIV\<star>" by fact
+  ultimately have "[c] @ s \<in> CUNIV\<star>" by (rule step)
+  then show "c # s \<in> CUNIV\<star>" by simp
+qed
+
+lemma UNIV_CUNIV_star: 
+  shows "UNIV = CUNIV\<star>"
+using string_in_CUNIV
+by (auto)
+
+abbreviation 
+  reg :: "string set => bool"
+where
+  "reg L1 \<equiv> (\<exists>r. L r = L1)"
+
+lemma reg_null [intro]:
+  shows "reg {}"
+by (metis L.simps(1))
+
+lemma reg_empty [intro]:
+  shows "reg {[]}"
+by (metis L.simps(2))
+
+lemma reg_star [intro]:
+  shows "reg L1 \<Longrightarrow> reg (L1\<star>)"
+by (metis L.simps(6))
+
+lemma reg_seq [intro]:
+  assumes a: "reg L1" "reg L2"
+  shows "reg (L1 ; L2)"
+using a
+by (metis L.simps(4)) 
+
+lemma reg_union [intro]:
+  assumes a: "reg L1" "reg L2"
+  shows "reg (L1 \<union> L2)"
+using a
+by (metis L.simps(5)) 
+
+lemma reg_string [intro]:
+  fixes s::string
+  shows "reg {s}"
+proof (induct s)
+  case Nil
+  show "reg {[]}" by (rule reg_empty)
+next
+  case (Cons c s)
+  have "reg {s}" by fact
+  then obtain r where "L r = {s}" by auto
+  then have "L (SEQ (CHAR c) r) = {[c]} ; {s}" by simp
+  also have "\<dots> = {c # s}" by (simp add: lang_seq_def)
+  finally show "reg {c # s}" by blast 
+qed
+
+lemma reg_finite [intro]:
+  assumes a: "finite L1"
+  shows "reg L1"
+using a
+proof(induct)
+  case empty
+  show "reg {}" by (rule reg_null)
+next
+  case (insert s S)
+  have "reg {s}" by (rule reg_string)
+  moreover 
+  have "reg S" by fact
+  ultimately have "reg ({s} \<union> S)" by (rule reg_union)
+  then show "reg (insert s S)" by simp
+qed
+  
+lemma reg_cuniv [intro]:
+  shows "reg (CUNIV)"
+by (rule reg_finite) (auto)
+
+lemma reg_univ:
+  shows "reg (UNIV::string set)"
+proof -
+  have "reg CUNIV" by (rule reg_cuniv)
+  then have "reg (CUNIV\<star>)" by (rule reg_star)
+  then show "reg UNIV" by (simp add: UNIV_CUNIV_star)
+qed
+
+lemma reg_finite_subset:
+  assumes a: "finite L1"
+  and     b: "reg L1" "L2 \<subseteq> L1"
+  shows "reg L2"
+using a b
+apply(induct arbitrary: L2)
+apply(simp add: reg_empty)
+oops
+
+
+lemma reg_not:
+  shows "reg (UNIV - L r)"
+proof (induct r)
+  case NULL
+  have "reg UNIV" by (rule reg_univ)
+  then show "reg (UNIV - L NULL)" by simp
+next
+  case EMPTY
+  have "[] \<notin> CUNIV" by auto
+  moreover
+  have "reg (CUNIV; CUNIV\<star>)" by auto
+  ultimately have "reg (CUNIV\<star> - {[]})" 
+    using lang_star_cases2 by simp
+  then show "reg (UNIV - L EMPTY)" by (simp add: UNIV_CUNIV_star)
+next
+  case (CHAR c)
+  then show "?case"
+    apply(simp)
+   
+using reg_UNIV
+apply(simp)
+apply(simp add: char_star2[symmetric])
+apply(rule reg_seq)
+apply(rule reg_cuniv)
+apply(rule reg_star)
+apply(rule reg_cuniv)
+oops
+
+
+
+end    
+   
+
+
+
+  
+
+  
+  
+
+
diff -r f20f391b21fa -r 074d9a4b2bc9 Matcher.thy
--- 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