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 75 f95a405c3180
parent 74 dfa9dbb8f8e6
child 76 39cef7b9212a 
--- a/thys/Re1.thy	Fri Mar 13 21:27:03 2015 +0000
+++ b/thys/Re1.thy	Fri Apr 10 22:38:36 2015 +0100
@@ -31,6 +31,11 @@
 | SEQ rexp rexp
 | ALT rexp rexp
 
+fun SEQS :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp"
+where
+  "SEQS r [] = r"
+| "SEQS r (r'#rs) = SEQ r (SEQS r' rs)"
+
 section {* Semantics of Regular Expressions *}
  
 fun
@@ -51,6 +56,22 @@
 | "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))"
 
@@ -69,6 +90,12 @@
 | 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 *}
 
 fun flat :: "val \<Rightarrow> string"
@@ -79,6 +106,22 @@
 | "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) = []"
@@ -107,6 +150,11 @@
 | "\<turnstile> Void : EMPTY"
 | "\<turnstile> Char c : CHAR c"
 
+inductive Prfs :: "val list \<Rightarrow> rexp list \<Rightarrow> bool"  ("\<Turnstile> _ : _" [100, 100] 100)
+where
+  "\<Turnstile> [] : []"
+| "\<lbrakk>\<turnstile>v : r; \<Turnstile> vs : rs\<rbrakk> \<Longrightarrow> \<Turnstile> (v#vs) : (r#rs)"
+
 fun mkeps :: "rexp \<Rightarrow> val"
 where
   "mkeps(EMPTY) = Void"
@@ -130,6 +178,15 @@
 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.
@@ -142,7 +199,7 @@
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
-apply(induct)
+apply(induct v r rule: Prf.induct)
 apply(auto simp add: Sequ_def)
 done
 
@@ -176,6 +233,33 @@
 | "Void \<succ>EMPTY Void"
 | "(Char c) \<succ>(CHAR c) (Char c)"
 
+inductive ValOrd2 :: "val \<Rightarrow> rexp \<Rightarrow> nat \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsupset>_,_ _" [100, 100, 100, 100] 100)
+where
+  "v2 \<sqsupset>r2,n v2' \<Longrightarrow> (Seq v1 v2) \<sqsupset>(SEQ r1 r2),(length (flat v1) + n) (Seq v1 v2')" 
+| "\<lbrakk>v1 \<sqsupset>r1,n v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<sqsupset>(SEQ r1 r2),(n + length (flat v2)) (Seq v1' v2')" 
+| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<sqsupset>(ALT r1 r2),(length (flat v1)) (Right v2)"
+| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<sqsupset>(ALT r1 r2),(length (flat v2)) (Left v1)"
+| "v2 \<sqsupset>r2,n v2' \<Longrightarrow> (Right v2) \<sqsupset>(ALT r1 r2),n (Right v2')"
+| "v1 \<sqsupset>r1,n v1' \<Longrightarrow> (Left v1) \<sqsupset>(ALT r1 r2),n (Left v1')"
+| "Void \<sqsupset>EMPTY,0 Void"
+| "(Char c) \<sqsupset>(CHAR c),1 (Char c)"
+
+lemma 
+  assumes "v1 \<sqsupset>r,n v2"
+  shows "length(flat v1) = n"
+using assms
+apply(induct)
+apply(auto)
+done
+
+lemma 
+  assumes "v1 \<sqsupset>r,n v2"
+  shows "length(flat v2) <= n"
+using assms
+apply(induct)
+apply(auto)
+oops
+
 
 section {* The ordering is reflexive *}
 
@@ -541,10 +625,12 @@
 apply(case_tac "nullable r1")
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all (no_asm_use))[5]
 apply(auto)[1]
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(clarify)
+apply(simp only: injval.simps flat.simps)
 apply(auto)[1]
 apply (metis mkeps_flat)
 apply(simp)
@@ -552,6 +638,41 @@
 apply(simp_all)[5]
 done
 
+lemma v4_flat_left:
+  assumes "\<turnstile> v : der c r" "\<not>(nullable_left r)" shows "flat_left (injval r c v) = c # (flat_left v)"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all (no_asm_use))[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp only: injval.simps)
+apply (metis nullable_left)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+done
+
+
 lemma v4_proj:
   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
   shows "c # flat (projval r c v) = flat v"
@@ -682,61 +803,6 @@
 apply(simp add: v4)
 done
 
-(*
-lemma 
- assumes "\<turnstile> v : der c r" "flat v \<noteq> []"
- shows "injval r c v \<succ>r mkeps r"
-using assms
-apply(induct c r arbitrary: v rule: der.induct)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(case_tac "c = c'")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis ValOrd.intros(6))
-apply(clarify)
-apply (metis ValOrd.intros(4) drop_0 drop_all le_add2 list.distinct(1) list.size(3) mkeps_flat monoid_add_class.add.right_neutral nat_less_le v4)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(simp)
-defer
-apply(rule ValOrd.intros)
-apply metis
-apply(case_tac "nullable r1")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-defer
-apply(clarify)
-apply(rule ValOrd.intros)
-apply metis
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-defer
-apply(subst mkeps_flat)
-oops
-*)
-
-
 lemma LeftRight:
   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
   and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 
@@ -820,15 +886,92 @@
 by (metis h)
 
 lemma Prf_inj_test:
-  assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2"
-  shows "(injval r c v1) \<succ>r (injval r c v2)"
-sorry
+  assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"  "\<Turnstile> vs : rs" "flat v1 = flat v2"
+  shows "Seqs (injval r c v1) vs \<succ>(SEQS r rs) Seqs (injval r c v2) vs"
+using assms
+apply(induct arbitrary: v1 v2 vs rs rule: der.induct)
+(* NULL case *)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* EMPTY case *)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* CHAR case *)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* ALT case *)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis ValOrd.intros(6))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis LeftRight ValOrd.intros(3) der.simps(4) injval.simps(2) injval.simps(3))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis RightLeft ValOrd.intros(4) der.simps(4) injval.simps(2) injval.simps(3))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis ValOrd.intros(5))
+(* SEQ case *)
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+defer
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+apply(clarify)
+apply(rule ValOrd.intros(2))
+apply(rotate_tac 2)
+apply(drule_tac x="v1c" in meta_spec)
+apply(rotate_tac 10)
+apply(drule_tac x="v1'" in meta_spec)
+apply(drule_tac meta_mp)
+apply(assumption)
+apply(drule_tac meta_mp)
+apply(assumption)
+apply(drule_tac meta_mp)
+apply(assumption)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(subst v4)
+apply(simp)
+apply(subst (asm) v4)
+apply(simp)
+apply(simp)
+apply(simp add: prefix_def)
+oops
 
 lemma Prf_inj:
   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)
   shows "(injval r c v1) \<succ>r (injval r c v2)"
 using assms
-apply(induct arbitrary: v1 v2 rule: der.induct)
+apply(induct c r arbitrary: v1 v2 rule: der.induct)
 (* NULL case *)
 apply(simp)
 apply(erule ValOrd.cases)
@@ -970,6 +1113,7 @@
 apply (metis list.distinct(1) mkeps_flat v4)
 oops
 
+
 lemma POSIX_der:
   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
   shows "POSIX (injval r c v) r"
@@ -977,7 +1121,7 @@
 unfolding POSIX_def
 apply(auto)
 thm v3
-apply (metis v3)
+apply (erule v3)
 thm v4
 apply(subst (asm) v4)
 apply(assumption)
@@ -998,10 +1142,123 @@
 apply(rule_tac x="flat v" in exI)
 apply(simp)
 apply(simp)
-thm Prf_inj_test
-apply(drule Prf_inj_test)
+oops
+
+lemma POSIX_der:
+  assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
+  shows "POSIX (injval r c v) r"
+using assms
+apply(induct c r arbitrary: v rule: der.induct)
+(* null case*)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* empty case *)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* char case *)
+apply(simp add: POSIX_def)
+apply(case_tac "c = c'")
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf.intros(5))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* alt case *)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp (no_asm) add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(2) v3)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis POSIX_ALT2 POSIX_def ValOrd.intros(6))
+apply (metis ValOrd.intros(3) order_refl)
+apply(simp (no_asm) add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(3) v3)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+defer
+apply (metis POSIX_ALT1a POSIX_def ValOrd.intros(5))
+prefer 2
+apply(subst (asm) (5) POSIX_def)
+apply(auto)[1]
+apply(rotate_tac 5)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(subst (asm) v4)
 apply(simp)
-apply (metis v3_proj)
+apply(drule_tac x="Left (projval r1a c v1)" in spec)
+apply(clarify)
+apply(drule mp)
+apply(rule conjI)
+apply (metis Prf.intros(2) v3_proj)
+apply(simp)
+apply (metis v4_proj2)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis less_not_refl v4_proj2)
+(* seq case *)
+apply(case_tac "nullable r1")
+defer
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf.intros(1) v3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(subst (asm) (3) v4)
+apply(simp)
+apply(simp)
+apply(subgoal_tac "flat v1a \<noteq> []")
+prefer 2
+apply (metis Prf_flat_L nullable_correctness)
+apply(subgoal_tac "\<exists>s. flat v1a = c # s")
+prefer 2
+apply (metis append_eq_Cons_conv)
+apply(auto)[1]
+ 
+
+apply(auto)
+thm v3
+apply (erule v3)
+thm v4
+apply(subst (asm) v4)
+apply(assumption)
+apply(drule_tac x="projval r c v'" in spec)
+apply(drule mp)
+apply(rule conjI)
+thm v3_proj
+apply(rule v3_proj)
+apply(simp)
+apply(rule_tac x="flat v" in exI)
+apply(simp)
+thm t
 apply(rule_tac c="c" in  t)
 apply(simp)
 thm v4_proj
@@ -1010,10 +1267,7 @@
 apply(rule_tac x="flat v" in exI)
 apply(simp)
 apply(simp)
-
-apply(simp add: Cons_eq_append_conv)
-apply(auto)[1]
-
+oops
 
 
 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
lexing