Mercurial Mercurial > hg > lexing / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Re1.thy
changeset 48 652861c9473f
parent 20 c11651bbebf5
child 49 c616ec6b1e3c 
--- a/thys/Re1.thy	Fri Dec 26 21:17:55 2014 +0000
+++ b/thys/Re1.thy	Mon Jan 19 09:55:58 2015 +0000
@@ -72,6 +72,13 @@
 | "flat(Right v) = flat(v)"
 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
+fun flats :: "val \<Rightarrow> string list"
+where
+  "flats(Void) = [[]]"
+| "flats(Char c) = [[c]]"
+| "flats(Left v) = flats(v)"
+| "flats(Right v) = flats(v)"
+| "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
 
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
@@ -93,6 +100,10 @@
 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 *}
 
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
@@ -106,19 +117,24 @@
 | "Void \<succ>EMPTY Void"
 | "(Char c) \<succ>(CHAR c) (Char c)"
 
-(*
-lemma
-  assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
-  shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))"
+section {* The ordering is reflexive *}
+
+lemma ValOrd_refl:
+  assumes "\<turnstile> v : r"
+  shows "v \<succ>r v"
 using assms
-apply(simp)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(simp)
+apply(induct)
+apply(auto intro: ValOrd.intros)
 done
-*)
+
+lemma ValOrd_flats:
+  assumes "v1 \<succ>r v2"
+  shows "hd (flats v2) = hd (flats v1)"
+using assms
+apply(induct)
+apply(auto)
+done
+
 
 section {* Posix definition *}
 
@@ -140,7 +156,6 @@
   "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')"
 
 
-(*
 lemma POSIX_SEQ:
   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
   shows "POSIX v1 r1 \<and> POSIX v2 r2"
@@ -149,13 +164,25 @@
 apply(auto)
 apply(drule_tac x="Seq v' v2" in spec)
 apply(simp)
-apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
+apply(erule impE)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(clarify)
+defer
 apply(drule_tac x="Seq v1 v'" in spec)
 apply(simp)
-by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
-*)
+apply(erule impE)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)
+apply(clarify)
+oops (*not true*)
 
-(*
 lemma POSIX_SEQ_I:
   assumes "POSIX v1 r1" "POSIX v2 r2" 
   shows "POSIX (Seq v1 v2) (SEQ r1 r2)" 
@@ -167,13 +194,23 @@
 apply(simp_all)[5]
 apply(auto)[1]
 apply(rule ValOrd.intros)
+oops (* maybe also not true *)
 
+lemma POSIX3_SEQ_I:
+  assumes "POSIX3 v1 r1" "POSIX3 v2 r2" 
+  shows "POSIX3 (Seq v1 v2) (SEQ r1 r2)" 
+using assms
+unfolding POSIX3_def
 apply(auto)
-done
-*)
-
-
-
+apply (metis Prf.intros(1))
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(case_tac "v1 = v1a")
+apply(auto)
+apply (metis ValOrd.intros(1))
+apply (rule ValOrd.intros(2))
 
 lemma POSIX_ALT2:
   assumes "POSIX (Left v1) (ALT r1 r2)"
@@ -318,15 +355,7 @@
 done
 
 
-section {* The ordering is reflexive *}
 
-lemma ValOrd_refl:
-  assumes "\<turnstile> v : r"
-  shows "v \<succ>r v"
-using assms
-apply(induct)
-apply(auto intro: ValOrd.intros)
-done
 
 
 section {* The Matcher *}
@@ -380,6 +409,55 @@
 apply(simp add: POSIX2_def)
 oops
 
+lemma mkeps_POSIX3:
+  assumes "nullable r"
+  shows "POSIX3 (mkeps r) r"
+using assms
+apply(induct r)
+apply(auto)[1]
+apply(simp add: POSIX3_def)
+apply(auto)[1]
+apply (metis Prf.intros(4))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros)
+apply(simp add: POSIX3_def)
+apply(auto)[1]
+apply(simp add: POSIX3_def)
+apply(auto)[1]
+apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(2) add_leE gen_length_code(1) gen_length_def mkeps_flat)
+apply(auto)
+apply(simp add: POSIX3_def)
+apply(auto)
+apply (metis Prf.intros(2))
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(6))
+apply(auto)[1]
+apply (metis ValOrd.intros(3))
+apply(simp add: POSIX3_def)
+apply(auto)
+apply (metis Prf.intros(2))
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(6))
+apply (metis ValOrd.intros(3))
+apply(simp add: POSIX3_def)
+apply(auto)
+apply (metis Prf.intros(3))
+apply(rotate_tac 5)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf_flat_L drop_0 drop_all list.size(3) mkeps_flat nullable_correctness)
+by (metis ValOrd.intros(5))
+
+
 lemma mkeps_POSIX:
   assumes "nullable r"
   shows "POSIX (mkeps r) r"
@@ -635,6 +713,45 @@
 apply(simp add: v4)
 done
 
+lemma "L r \<noteq> {} \<Longrightarrow> \<exists>v. POSIX3 v r"
+apply(induct r)
+apply(simp)
+apply(simp add: POSIX3_def)
+apply(rule_tac x="Void" in exI)
+apply(auto)[1]
+apply (metis Prf.intros(4))
+apply (metis POSIX3_def flat.simps(1) mkeps.simps(1) mkeps_POSIX3 nullable.simps(2) order_refl)
+apply(simp add: POSIX3_def)
+apply(rule_tac x="Char char" in exI)
+apply(auto)[1]
+apply (metis Prf.intros(5))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply(simp add: Sequ_def)
+apply(auto)[1]
+apply(drule meta_mp)
+apply(auto)[2]
+apply(drule meta_mp)
+apply(auto)[2]
+apply(rule_tac x="Seq v va" in exI)
+apply(simp (no_asm) add: POSIX3_def)
+apply(auto)[1]
+apply (metis POSIX3_def Prf.intros(1))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(case_tac "v  \<succ>r1a v1")
+apply(rule ValOrd.intros(2))
+apply(simp)
+apply(case_tac "v = v1")
+apply(rule ValOrd.intros(1))
+apply(simp)
+apply(simp)
+apply (metis ValOrd_refl)
+apply(simp add: POSIX3_def)
+
+
 lemma "\<exists>v. POSIX v r"
 apply(induct r)
 apply(rule exI)
@@ -684,26 +801,7 @@
 apply(rule ValOrd.intros)
 apply(case_tac "\<exists>r1a r1b. r1 = ALT r1a r1b")
 apply(auto)
-apply(rule_tac x = "Seq () va" in exI )
-apply(simp (no_asm) add: POSIX_def)
-apply(auto)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto)[1]
-apply(rule ValOrd.intros(2))
-apply(rule ValOrd.intros)
-
-apply(case_tac "v \<succ>r1a v1")
-apply (metis ValOrd.intros(2))
-apply(simp add: POSIX_def)
-apply(case_tac "flat v = flat v1")
-apply(auto)[1]
-apply(simp only: append_eq_append_conv2)
-apply(auto)
-thm append_eq_append_conv2
+oops (* not sure if this can be proved by induction *)
 
 text {* 
 
@@ -742,12 +840,29 @@
 prefer 2
 apply(auto simp add: POSIX_def)[1]
 apply (metis POSIX_ALT1a POSIX_def flat.simps(4))
+apply(frule POSIX_ALT1a)
+apply(drule POSIX_ALT1b)
+apply(rule POSIX_ALT_I2)
 apply(rotate_tac 1)
 apply(drule_tac x="v2" in meta_spec)
 apply(simp)
 apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)")
 prefer 2
 apply (metis Prf.intros(3) v3)
+
+apply auto[1]
+apply(subst v4)
+apply(auto)[2]
+apply(subst (asm) (4) POSIX_def)
+apply(subst (asm) v4)
+apply(drule_tac x="v2" in meta_spec)
+apply(simp)
+
+apply(auto)[2]
+
+thm POSIX_ALT_I2
+apply(rule POSIX_ALT_I2)
+
 apply(rule ccontr)
 apply(auto simp add: POSIX_def)[1]
lexing