diff -r dcfc9b23b263 -r 09ab631ce7fa thys/LexerExt.thy
--- a/thys/LexerExt.thy	Sun Apr 02 02:14:01 2017 +0800
+++ b/thys/LexerExt.thy	Wed May 17 09:38:58 2017 +0100
@@ -67,11 +67,6 @@
 unfolding Der_def Sequ_def
 by (auto simp add: Cons_eq_append_conv)
 
-lemma Der_inter [simp]:
-  shows "Der c (A \<inter> B) = Der c A \<inter> Der c B"
-unfolding Der_def
-by auto
-
 lemma Der_union [simp]:
   shows "Der c (A \<union> B) = Der c A \<union> Der c B"
 unfolding Der_def
@@ -222,10 +217,6 @@
 | FROMNTIMES rexp nat
 | NMTIMES rexp nat nat
 | PLUS rexp
-| AND rexp rexp
-| NOT rexp
-| ALLL
-| ALLBUT
 
 section {* Semantics of Regular Expressions *}
  
@@ -243,10 +234,6 @@
 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)"
 | "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 *}
 
@@ -264,11 +251,6 @@
 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)"
 | "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"
@@ -294,11 +276,6 @@
                            SEQ (der c r) (UPNTIMES r (m - 1))) else 
                            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"
@@ -353,7 +330,7 @@
 apply(simp only: der.simps if_True)
 apply(simp only: L.simps)
 apply(simp)
-apply(auto)[3]
+apply(auto)
 apply(subst (asm) Sequ_UNION[symmetric])
 apply(subst (asm) test[symmetric])
 apply(auto simp add: Der_UNION)[1]
@@ -378,20 +355,12 @@
 apply(case_tac xa)
 apply(simp)
 apply(simp)
-apply(auto)[1]
+apply(auto)
 apply(auto simp add: Sequ_def Der_def)[1]
 using Star_def apply auto[1]
 apply(case_tac "[] \<in> L r")
-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
+apply(auto)
+using Der_UNION Der_star Star_def by fastforce
 
 lemma ders_correctness:
   shows "L (ders s r) = Ders s (L r)"
@@ -433,10 +402,7 @@
 | Right val
 | Left val
 | Stars "val list"
-| And val val
-| Not val
-| Alll
-| Allbut
+
 
 section {* The string behind a value *}
 
@@ -450,15 +416,77 @@
 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
 | "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"
+
+
+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)"
@@ -479,6 +507,90 @@
 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
+done
+
+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 
@@ -493,9 +605,6 @@
 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
 | "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"
@@ -512,61 +621,25 @@
 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
 | "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_nullable:
+  assumes "nullable(r)" 
+  shows "\<turnstile> mkeps r : r"
+using assms
+apply(induct r rule: mkeps.induct) 
+apply(auto intro: Prf.intros)
+by (metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl)
+
 lemma mkeps_flat:
   assumes "nullable(r)" 
   shows "flat (mkeps r) = []"
 using assms
-apply (induct r) 
-apply(auto)[15]
-apply(case_tac "x3a < x2")
-apply(auto)[2]
-done
+apply (induct rule: nullable.induct) 
+apply(auto)
+by meson
 
-lemma Prf_injval_flat:
-  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)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 3)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 4)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-done
 
 lemma Prf_injval:
   assumes "\<turnstile> v : der c r" 
@@ -647,18 +720,41 @@
 apply(simp_all)
 apply(auto)
 using Prf.intros apply auto[1]
-(* AND *)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto)
-apply(rule Prf.intros)
-apply(simp)
-apply(simp)
-apply(simp add: Prf_injval_flat)
 done
 
 
-
+lemma Prf_injval_flat:
+  assumes "\<turnstile> v : der c r" 
+  shows "flat (injval r c v) = c # (flat v)"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(auto elim!: Prf_elims split: if_splits)
+apply(metis mkeps_flat)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+done
 
 
 section {* Our Alternative Posix definition *}
@@ -696,7 +792,6 @@
 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = [];
     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)"
-| Posix_AND: "\<lbrakk>s \<in> r1 \<rightarrow> v1; s \<in> r2 \<rightarrow> v2\<rbrakk> \<Longrightarrow> s \<in> (AND r1 r2) \<rightarrow> (And v1 v2)"
 
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
@@ -831,9 +926,7 @@
 apply(simp_all)
 apply(rule Prf.intros)
 apply(auto)
-apply(rule Prf.intros)
-apply(auto)
-by (simp add: Posix1(2))
+done
 
 
 lemma  Posix_NTIMES_mkeps:
@@ -1088,17 +1181,6 @@
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
-next 
-  case (Posix_AND s r1 v1 r2 v2 v')
-  have "s \<in> AND r1 r2 \<rightarrow> v'" 
-       "s \<in> r1 \<rightarrow> v1" "s \<in> r2 \<rightarrow> v2" by fact+
-  then obtain v1' v2' where "v' = And v1' v2'" "s \<in> r1 \<rightarrow> v1'" "s \<in> r2 \<rightarrow> v2'"
-  apply(cases) apply (auto simp add: append_eq_append_conv2)
-  done
-  moreover
-  have IHs: "\<And>v1'. s \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'"
-            "\<And>v2'. s \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+
-  ultimately show "And v1 v2 = v'" by simp
 qed
 
 lemma NTIMES_Stars:
@@ -1523,17 +1605,6 @@
   apply(simp)
   apply(simp)
   done  
-next
-  case (AND r1 r2)
-  then show ?case
-  apply -
-  apply(erule Posix.cases)
-  apply(simp_all)
-  apply(auto)
-  apply(rule Posix.intros)
-  apply(simp)
-  apply(simp)
-  done
 qed