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/LexerExt.thy
changeset 239 e59cec211f4f
parent 238 2dc1647eab9e
child 243 09ab631ce7fa 
--- a/thys/LexerExt.thy	Fri Mar 17 19:47:42 2017 +0000
+++ b/thys/LexerExt.thy	Mon Mar 20 15:13:17 2017 +0000
@@ -223,6 +223,9 @@
 | NMTIMES rexp nat nat
 | PLUS rexp
 | AND rexp rexp
+| NOT rexp
+| ALLL
+| ALLBUT
 
 section {* Semantics of Regular Expressions *}
  
@@ -241,6 +244,9 @@
 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" 
 | "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)"
 | "L (AND r1 r2) = (L r1) \<inter> (L r2)"
+| "L (NOT r) = UNIV - (L r)"
+| "L (ALLL) = UNIV"
+| "L (ALLBUT) = UNIV - {[]}"
 
 section {* Nullable, Derivatives *}
 
@@ -259,6 +265,10 @@
 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 | "nullable (PLUS r) = (nullable r)"
 | "nullable (AND r1 r2) = (nullable r1 \<and> nullable r2)"
+| "nullable (NOT r) = (\<not>nullable r)"
+| "nullable (ALLL) = True"
+| "nullable (ALLBUT) = False"
+
 
 fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -285,6 +295,10 @@
                            SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 | "der c (AND r1 r2) = AND (der c r1) (der c r2)"
+| "der c (NOT r) = NOT (der c r)"
+| "der c (ALLL) = ALLL"
+| "der c (ALLBUT) = ALLL"
+
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -339,7 +353,7 @@
 apply(simp only: der.simps if_True)
 apply(simp only: L.simps)
 apply(simp)
-apply(auto)
+apply(auto)[3]
 apply(subst (asm) Sequ_UNION[symmetric])
 apply(subst (asm) test[symmetric])
 apply(auto simp add: Der_UNION)[1]
@@ -364,12 +378,20 @@
 apply(case_tac xa)
 apply(simp)
 apply(simp)
-apply(auto)
+apply(auto)[1]
 apply(auto simp add: Sequ_def Der_def)[1]
 using Star_def apply auto[1]
 apply(case_tac "[] \<in> L r")
-apply(auto)
-using Der_UNION Der_star Star_def by fastforce
+apply(auto)[1]
+using Der_UNION Der_star Star_def apply fastforce
+apply(simp)
+apply(simp)
+apply(simp add: Der_def)
+apply(blast)
+(* ALLL*)
+apply(simp add: Der_def)
+apply(simp add: Der_def)
+done
 
 lemma ders_correctness:
   shows "L (ders s r) = Ders s (L r)"
@@ -412,6 +434,9 @@
 | Left val
 | Stars "val list"
 | And val val
+| Not val
+| Alll
+| Allbut
 
 section {* The string behind a value *}
 
@@ -426,78 +451,14 @@
 | "flat (Stars []) = []"
 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
 | "flat (And v1 v2) = flat v1"
+| "flat (Not v) = flat v"
+| "flat Allbut = []"
+
 
 lemma flat_Stars [simp]:
  "flat (Stars vs) = concat (map flat vs)"
 by (induct vs) (auto)
 
-
-section {* Relation between values and regular expressions *}
-
-inductive 
-  Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
-where
- "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
-| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
-| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
-| "\<turnstile> Void : ONE"
-| "\<turnstile> Char c : CHAR c"
-| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r"
-| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n"
-| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n"
-| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n"
-| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m"
-| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r"
-| "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2; flat v1 = flat v2\<rbrakk> \<Longrightarrow> \<turnstile> And v1 v2: AND r1 r2"
-
-
-inductive_cases Prf_elims:
-  "\<turnstile> v : ZERO"
-  "\<turnstile> v : SEQ r1 r2"
-  "\<turnstile> v : ALT r1 r2"
-  "\<turnstile> v : ONE"
-  "\<turnstile> v : CHAR c"
-(*  "\<turnstile> vs : STAR r"*)
-
-lemma Prf_STAR:
-   assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r"  
-   shows "concat (map flat vs) \<in> L r\<star>"
-using assms 
-apply(induct vs)
-apply(auto)
-done
-
-lemma Prf_Pow:
-  assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r" 
-  shows "concat (map flat vs) \<in> L r \<up> length vs"
-using assms
-apply(induct vs)
-apply(auto simp add: Sequ_def)
-done
-
-lemma Prf_flat_L:
-  assumes "\<turnstile> v : r" shows "flat v \<in> L r"
-using assms
-apply(induct v r rule: Prf.induct)
-apply(auto simp add: Sequ_def)
-apply(rule Prf_STAR)
-apply(simp)
-apply(rule_tac x="length vs" in bexI)
-apply(rule Prf_Pow)
-apply(simp)
-apply(simp)
-apply(rule Prf_Pow)
-apply(simp)
-apply(rule_tac x="length vs" in bexI)
-apply(rule Prf_Pow)
-apply(simp)
-apply(simp)
-apply(rule_tac x="length vs" in bexI)
-apply(rule Prf_Pow)
-apply(simp)
-apply(simp)
-using Prf_Pow by blast
-
 lemma Star_Pow:
   assumes "s \<in> A \<up> n"
   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)"
@@ -518,91 +479,6 @@
 using Star_Pow by blast
 
 
-lemma Star_val:
-  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
-  shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
-using assms
-apply(induct ss)
-apply(auto)
-apply (metis empty_iff list.set(1))
-by (metis concat.simps(2) list.simps(9) set_ConsD)
-
-lemma Star_val_length:
-  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
-  shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r) \<and> (length vs) = (length ss)"
-using assms
-apply(induct ss)
-apply(auto)
-by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD)
-
-
-
-
-
-lemma L_flat_Prf2:
-  assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
-using assms
-apply(induct r arbitrary: s)
-apply(auto simp add: Sequ_def intro: Prf.intros)
-using Prf.intros(1) flat.simps(5) apply blast
-using Prf.intros(2) flat.simps(3) apply blast
-using Prf.intros(3) flat.simps(4) apply blast
-apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
-apply(auto)[1]
-apply(rule_tac x="Stars vs" in exI)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-using Star_string Star_val apply force
-apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")
-apply(auto)[1]
-apply(rule_tac x="Stars vs" in exI)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-apply(simp)
-using Star_Pow Star_val_length apply blast
-apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x2)")
-apply(auto)[1]
-apply(rule_tac x="Stars vs" in exI)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-apply(simp)
-using Star_Pow Star_val_length apply blast
-apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")
-apply(auto)[1]
-apply(rule_tac x="Stars vs" in exI)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-apply(simp)
-using Star_Pow Star_val_length apply blast
-apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")
-apply(auto)[1]
-apply(rule_tac x="Stars vs" in exI)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-apply(simp)
-apply(simp)
-using Star_Pow Star_val_length apply blast
-apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)")
-apply(auto)[1]
-apply(rule_tac x="Stars vs" in exI)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-apply(simp)
-using Star_Pow Star_val_length apply blast
-(* AND *)
-using Prf.intros(12) by fastforce
-
-lemma L_flat_Prf:
-  "L(r) = {flat v | v. \<turnstile> v : r}"
-using Prf_flat_L L_flat_Prf2 by blast
-
-
 section {* Sulzmann and Lu functions *}
 
 fun 
@@ -618,6 +494,8 @@
 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"
 | "mkeps(PLUS r) = Stars ([mkeps r])"
 | "mkeps(AND r1 r2) = And (mkeps r1) (mkeps r2)"
+| "mkeps(NOT r) = Not (Allbut)"
+| "mkeps(ALLL) = Void"
 
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -636,32 +514,29 @@
 | "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 | "injval (AND r1 r2) c (And v1 v2) = And (injval r1 c v1) (injval r2 c v2)"
 
+
 section {* Mkeps, injval *}
 
 lemma mkeps_flat:
   assumes "nullable(r)" 
   shows "flat (mkeps r) = []"
 using assms
-apply (induct rule: nullable.induct) 
-apply(auto)
-by meson
-
-lemma mkeps_nullable:
-  assumes "nullable(r)" 
-  shows "\<turnstile> mkeps r : r"
-using assms
-apply(induct r rule: mkeps.induct) 
-apply(auto intro: Prf.intros)
-apply(metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl)
-apply(rule Prf.intros)
-apply(simp_all add: mkeps_flat)
+apply (induct r) 
+apply(auto)[15]
+apply(case_tac "x3a < x2")
+apply(auto)[2]
 done
 
 lemma Prf_injval_flat:
-  assumes "\<turnstile> v : der c r" 
+  assumes "flat v \<in> L (der c r)" 
   shows "flat (injval r c v) = c # (flat v)"
 using assms
 apply(induct arbitrary: v rule: der.induct)
+apply(simp_all)
+apply(case_tac "c = d")
+prefer 2
+apply(simp)
+apply(simp)
 apply(auto elim!: Prf_elims split: if_splits)
 apply(metis mkeps_flat)
 apply(rotate_tac 2)
lexing