--- 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)