diff -r 279d0bc48308 -r ca8f9645db69 thys/Re1.thy
--- a/thys/Re1.thy	Mon Jun 08 14:37:19 2015 +0100
+++ b/thys/Re1.thy	Wed Jun 10 14:51:35 2015 +0100
@@ -47,6 +47,17 @@
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
+fun zeroable 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)"
+
+lemma L_ALT_cases:
+  "L (ALT r1 r2) \<noteq> {} \<Longrightarrow> (L r1 \<noteq> {}) \<or> (L r1 = {} \<and> L r2 \<noteq> {})"
+by(auto)
+
 fun
  nullable :: "rexp \<Rightarrow> bool"
 where
@@ -56,25 +67,6 @@
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
-fun
- nullable_left :: "rexp \<Rightarrow> bool"
-where
-  "nullable_left (NULL) = False"
-| "nullable_left (EMPTY) = True"
-| "nullable_left (CHAR c) = False"
-| "nullable_left (ALT r1 r2) = (nullable_left r1 \<or> nullable_left r2)"
-| "nullable_left (SEQ r1 r2) = nullable_left r1"
-
-lemma nullable_left:
-  "nullable r \<Longrightarrow> nullable_left r"
-apply(induct r)
-apply(auto)
-done
-
-
-value "L(CHAR c)"
-value "L(SEQ(CHAR c)(CHAR b))"
-
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 apply (induct r) 
@@ -90,11 +82,6 @@
 | Right val
 | Left val
 
-fun Seqs :: "val \<Rightarrow> val list \<Rightarrow> val"
-where
-  "Seqs v [] = v"
-| "Seqs v (v'#vs) = Seq v (Seqs v' vs)"
-
 
 section {* The string behind a value *}
 
@@ -106,30 +93,6 @@
 | "flat(Right v) = flat(v)"
 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
-fun flat_left :: "val \<Rightarrow> string"
-where
-  "flat_left(Void) = []"
-| "flat_left(Char c) = [c]"
-| "flat_left(Left v) = flat_left(v)"
-| "flat_left(Right v) = flat_left(v)"
-| "flat_left(Seq v1 v2) = flat_left(v1)"
-
-fun flat_right :: "val \<Rightarrow> string"
-where
-  "flat_right(Void) = []"
-| "flat_right(Char c) = [c]"
-| "flat_right(Left v) = flat(v)"
-| "flat_right(Right v) = flat(v)"
-| "flat_right(Seq v1 v2) = flat(v2)"
-
-fun head :: "val \<Rightarrow> string"
-where
-  "head(Void) = []"
-| "head(Char c) = [c]"
-| "head(Left v) = head(v)"
-| "head(Right v) = head(v)"
-| "head(Seq v1 v2) = head v1"
-
 fun flats :: "val \<Rightarrow> string list"
 where
   "flats(Void) = [[]]"
@@ -142,6 +105,7 @@
 
 section {* Relation between values and regular expressions *}
 
+
 inductive Prfs :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile>_ _ : _" [100, 100, 100] 100)
 where
  "\<lbrakk>\<Turnstile>s1 v1 : r1; \<Turnstile>s2 v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>(s1 @ s2) (Seq v1 v2) : SEQ r1 r2"
@@ -156,7 +120,6 @@
 apply(auto)
 done
 
-
 inductive Prfn :: "nat \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<TTurnstile>_ _ : _" [100, 100, 100] 100)
 where
  "\<lbrakk>\<TTurnstile>n1 v1 : r1; \<TTurnstile>n2 v2 : r2\<rbrakk> \<Longrightarrow> \<TTurnstile>(n1 + n2) (Seq v1 v2) : SEQ r1 r2"
@@ -166,7 +129,7 @@
 | "\<TTurnstile>1 (Char c) : CHAR c"
 
 lemma Prfn_flat:
-  "\<TTurnstile>n v : r \<Longrightarrow> length(flat v) = n"
+  "\<TTurnstile>n v : r \<Longrightarrow> length (flat v) = n"
 apply(induct rule: Prfn.induct)
 apply(auto)
 done
@@ -243,13 +206,6 @@
 apply(auto)
 done
 
-lemma mkeps_flat_left:
-  assumes "nullable(r)" shows "flat_left (mkeps r) = []"
-using assms
-apply(induct rule: nullable.induct)
-apply(auto)
-done
-
 text {*
   The value mkeps returns is always the correct POSIX
   value.
@@ -275,9 +231,7 @@
 apply(auto)
 done
 
-definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
-where
-  "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
+
 
 section {* Ordering of values *}
 
@@ -434,6 +388,99 @@
 apply(simp_all)[8]
 done
 
+definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
+where
+  "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
+
+
+lemma
+  "L r \<noteq> {} \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> flat vmax}. vmax 2\<succ> v)"
+apply(induct r)
+apply(simp)
+apply(rule impI)
+apply(simp)
+apply(rule_tac x="Void" in exI)
+apply(simp)
+apply(rule conjI)
+apply (metis Prf.intros(4))
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(7))
+apply(simp)
+apply(rule_tac x="Char char" in exI)
+apply(simp)
+apply(rule conjI)
+apply (metis Prf.intros)
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(8))
+apply(simp)
+apply(rule impI)
+apply(simp add: Sequ_def)[1]
+apply(erule exE)+
+apply(erule conjE)+
+apply(clarify)
+defer
+apply(rule impI)
+apply(drule L_ALT_cases)
+apply(erule disjE)
+apply(simp)
+apply(erule exE)
+apply(clarify)
+apply(rule_tac x="Left vmax" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(2))
+apply(simp)
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(6))
+apply(clarify)
+apply (metis ValOrd2.intros(3) length_append ordered_cancel_comm_monoid_diff_class.le_iff_add prefix_def)
+apply(simp)
+apply(clarify)
+apply(rule_tac x="Right vmax" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(3))
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)+
+apply(simp)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf_flat_L empty_iff)
+apply (metis ValOrd2.intros(5))
+apply(drule mp)
+apply (metis empty_iff)
+apply(drule mp)
+apply (metis empty_iff)
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac x="Seq vmax vmaxa" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(1))
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)+
+apply(simp)
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(case_tac "vmax = v1")
+apply(simp)
+apply (simp add: ValOrd2.intros(1) prefix_def)
+
 lemma
   "s \<in> L r \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r \<and> flat v = s}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v = s}. vmax 2\<succ> v)"
 apply(induct s arbitrary: r rule: length_induct)
@@ -1630,12 +1677,7 @@
 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
 by (metis)
 
-fun zeroable 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)"
+
 
 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 by (metis Prf_flat_L nullable_correctness)