--- a/progs/Matcher2.thy	Fri Nov 15 10:29:04 2013 +0000
+++ b/progs/Matcher2.thy	Sun Nov 17 18:16:20 2013 +0000
@@ -52,6 +52,7 @@
 
 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:
@@ -62,6 +63,30 @@
   "[] \<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 {* Power for Sets *}
+
+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 {* Kleene Star for Sets *}
 
 inductive_set
@@ -71,33 +96,43 @@
   start[intro]: "[] \<in> A\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
 
-
 text {* A Standard Property of Star *}
 
-lemma star_cases:
-  shows "A\<star> = {[]} \<union> A ;; A\<star>"
-unfolding Seq_def
-by (auto) (metis Star.simps)
-
 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)
 
-section {* Power for Sets *}
+lemma star_cases:
+  shows "A\<star> = {[]} \<union> A ;; A\<star>"
+unfolding Seq_def 
+by (auto) (metis Star.simps)
 
-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 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 pow_empty [simp]:
-  shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
-by (induct n) (auto)
+lemma Star_def2: 
+  shows "A\<star> = (\<Union>n. A \<up> n)"
+using Star_in_Pow Pow_in_Star
+by (auto)
+
 
 
 section {* Semantics of Regular Expressions *}
@@ -265,4 +300,39 @@
    (simp_all add: nullable_correctness der_correctness Der_def)
 
 
+
+
+lemma bb: "A \<up> n ;; A\<star> \<subseteq> A\<star>"
+apply(induct n)
+apply(simp)
+apply(simp)
+apply(subst aa[symmetric])
+apply(subst Seq_def)
+apply(auto)
+done
+
+lemma cc: "(\<Union>i\<in>{..n}. A \<up> i) ;; A\<star> \<subseteq> A\<star>"
+apply(induct n)
+apply(simp)
+apply(simp add: Suc_Union del: pow.simps)
+apply(simp only: seq_union)
+apply(rule Un_least)
+defer
+apply(simp)
+apply(rule bb)
+done
+
+lemma "A\<star> ;; A\<star> = A\<star>"
+apply(simp add: Seq_def)
+apply(rule subset_antisym)
+defer
+apply(auto)[1]
+apply(auto simp add: Star_def2)
+
+apply(subst (asm) Star_def2)
+apply(subst (asm) Star_def2)
+apply(auto)
+
+
+
 end    
\ No newline at end of file