Mercurial Mercurial > hg > lexing / comparison
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/SpecExt.thy
changeset 397 e1b74d618f1b
parent 359 fedc16924b76
equal deleted inserted replaced
396:cc8e231529fb 397:e1b74d618f1b 
     1    
     1    
     2 theory SpecExt
 
     2 theory SpecExt
 
     3   imports Main (*"~~/src/HOL/Library/Sublist"*)
 
     3   imports Main "HOL-Library.Sublist" (*"~~/src/HOL/Library/Sublist"*)
 
     4 begin
 
     4 begin
 
     5 
     5 
     6 section {* Sequential Composition of Languages *}
 
     6 section {* Sequential Composition of Languages *}
 
     7 
     7 
     8 definition
 
     8 definition
 
   163 using assms
 
   163 using assms
 
   164 apply(induct n arbitrary: s)
 
   164 apply(induct n arbitrary: s)
 
   165 apply(auto simp add: Sequ_def)
 
   165 apply(auto simp add: Sequ_def)
 
   166   done
 
   166   done
 
   167 
   167 
   168 lemma
 
       
   169   assumes "[] \<in> A" "n \<noteq> 0" "A \<noteq> {}"
 
       
   170   shows "A \<up> (Suc n) = A \<up> n"
 
       
   171 
       
   172 lemma Der_Pow_0:
 
   168 lemma Der_Pow_0:
 
   173   shows "Der c (A \<up> 0) = {}"
 
   169   shows "Der c (A \<up> 0) = {}"
 
   174 by(simp add: Der_def)
 
   170 by(simp add: Der_def)
 
   175 
   171 
   176 lemma Der_Pow_Suc:
 
   172 lemma Der_Pow_Suc:
 
   219 section {* Regular Expressions *}
 
   215 section {* Regular Expressions *}
 
   220 
   216 
   221 datatype rexp =
 
   217 datatype rexp =
 
   222   ZERO
 
   218   ZERO
 
   223 | ONE
 
   219 | ONE
 
   224 | CHAR char
 
   220 | CH char
 
   225 | SEQ rexp rexp
 
   221 | SEQ rexp rexp
 
   226 | ALT rexp rexp
 
   222 | ALT rexp rexp
 
   227 | STAR rexp
 
   223 | STAR rexp
 
   228 | UPNTIMES rexp nat
 
   224 | UPNTIMES rexp nat
 
   229 | NTIMES rexp nat
 
   225 | NTIMES rexp nat
 
   236 fun
 
   232 fun
 
   237   L :: "rexp \<Rightarrow> string set"
 
   233   L :: "rexp \<Rightarrow> string set"
 
   238 where
 
   234 where
 
   239   "L (ZERO) = {}"
 
   235   "L (ZERO) = {}"
 
   240 | "L (ONE) = {[]}"
 
   236 | "L (ONE) = {[]}"
 
   241 | "L (CHAR c) = {[c]}"
 
   237 | "L (CH c) = {[c]}"
 
   242 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
   238 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
   243 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
   239 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
   244 | "L (STAR r) = (L r)\<star>"
 
   240 | "L (STAR r) = (L r)\<star>"
 
   245 | "L (UPNTIMES r n) = (\<Union>i\<in>{..n} . (L r) \<up> i)"
 
   241 | "L (UPNTIMES r n) = (\<Union>i\<in>{..n} . (L r) \<up> i)"
 
   246 | "L (NTIMES r n) = (L r) \<up> n"
 
   242 | "L (NTIMES r n) = (L r) \<up> n"
 
   253 fun
 
   249 fun
 
   254  nullable :: "rexp \<Rightarrow> bool"
 
   250  nullable :: "rexp \<Rightarrow> bool"
 
   255 where
 
   251 where
 
   256   "nullable (ZERO) = False"
 
   252   "nullable (ZERO) = False"
 
   257 | "nullable (ONE) = True"
 
   253 | "nullable (ONE) = True"
 
   258 | "nullable (CHAR c) = False"
 
   254 | "nullable (CH c) = False"
 
   259 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
   255 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
   260 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
   256 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
   261 | "nullable (STAR r) = True"
 
   257 | "nullable (STAR r) = True"
 
   262 | "nullable (UPNTIMES r n) = True"
 
   258 | "nullable (UPNTIMES r n) = True"
 
   263 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 
   259 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 
   268 fun
 
   264 fun
 
   269  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   265  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   270 where
 
   266 where
 
   271   "der c (ZERO) = ZERO"
 
   267   "der c (ZERO) = ZERO"
 
   272 | "der c (ONE) = ZERO"
 
   268 | "der c (ONE) = ZERO"
 
   273 | "der c (CHAR d) = (if c = d then ONE else ZERO)"
 
   269 | "der c (CH d) = (if c = d then ONE else ZERO)"
 
   274 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 
   270 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 
   275 | "der c (SEQ r1 r2) = 
   271 | "der c (SEQ r1 r2) = 
   276      (if nullable r1
 
   272      (if nullable r1
 
   277       then ALT (SEQ (der c r1) r2) (der c r2)
 
   273       then ALT (SEQ (der c r1) r2) (der c r2)
 
   278       else SEQ (der c r1) r2)"
 
   274       else SEQ (der c r1) r2)"
 
   338   apply(induct m arbitrary: n x)
 
   334   apply(induct m arbitrary: n x)
 
   339   apply(auto simp add: Sequ_def)
 
   335   apply(auto simp add: Sequ_def)
 
   340   by (metis append.assoc)
 
   336   by (metis append.assoc)
 
   341   
   337   
   342 
   338 
   343 
       
   344 lemma
 
       
   345  "L(FROMNTIMES r n) = L(SEQ (NTIMES r n) (STAR r))"
 
       
   346   apply(auto simp add: Sequ_def)
 
       
   347   defer
 
       
   348    apply(subgoal_tac "\<exists>m. s2 \<in> (L r) \<up> m")
 
       
   349   prefer 2
 
       
   350     apply (simp add: Star_Pow)
 
       
   351   apply(auto)
 
       
   352   apply(rule_tac x="n + m" in bexI)
 
       
   353     apply (simp add: pow_add)
 
       
   354    apply simp
 
       
   355   apply(subgoal_tac "\<exists>m. m + n = xa")
 
       
   356    apply(auto)
 
       
   357    prefer 2
 
       
   358   using le_add_diff_inverse2 apply auto[1]
 
       
   359   by (smt Pow_Star Sequ_def add.commute mem_Collect_eq pow_add2)
 
       
   360   
       
   361 lemma
 
       
   362    "L (der c (FROMNTIMES r n)) = 
       
   363      L (SEQ (der c r) (FROMNTIMES r (n - 1)))"
 
       
   364   apply(auto simp add: Sequ_def)
 
       
   365   using Star_Pow apply blast
 
       
   366   using Pow_Star by blast
 
       
   367   
       
   368 lemma
 
       
   369  "L (der c (UPNTIMES r n)) = 
       
   370     L(if n = 0 then ZERO  else 
       
   371       ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))"
 
       
   372   apply(auto simp add: Sequ_def)
 
       
   373   using SpecExt.Pow_empty by blast 
       
   374 
       
   375 abbreviation "FROM \<equiv> FROMNTIMES"
 
       
   376 
       
   377 lemma
 
       
   378   shows "L (der c (FROM r n)) = 
       
   379          L (if n <= 0 then SEQ (der c r) (ALT ONE (FROM r 0))
 
       
   380                       else SEQ (der c r) (ALT ZERO (FROM r (n -1))))"
 
       
   381   apply(auto simp add: Sequ_def)
 
       
   382   oops
 
       
   383 
       
   384 
       
   385 fun 
   339 fun 
   386  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   340  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   387 where
 
   341 where
 
   388   "ders [] r = r"
 
   342   "ders [] r = r"
 
   389 | "ders (c # s) r = ders s (der c r)"
 
   343 | "ders (c # s) r = ders s (der c r)"
 
   452 apply(simp)
 
   406 apply(simp)
 
   453 apply(clarify)
 
   407 apply(clarify)
 
   454 apply(auto simp add: Sequ_def Der_def Cons_eq_append_conv)[1]
 
   408 apply(auto simp add: Sequ_def Der_def Cons_eq_append_conv)[1]
 
   455 apply(rule_tac x="Suc xa" in bexI)
 
   409 apply(rule_tac x="Suc xa" in bexI)
 
   456 apply(auto simp add: Sequ_def)[2]
 
   410 apply(auto simp add: Sequ_def)[2]
 
   457 apply (metis append_Cons)
 
   411      apply (metis append_Cons)
 
   458 apply (metis (no_types, hide_lams) Pow_decomp atMost_iff diff_Suc_eq_diff_pred diff_is_0_eq)
 
   412  apply(rule_tac x="xa - 1" in bexI)
 
       
   413      apply(auto simp add: Sequ_def)[2]
 
       
   414   apply (metis One_nat_def Pow_decomp)
 
   459 apply(rule impI)+
 
   415 apply(rule impI)+
 
   460 apply(subst Sequ_Union_in)
 
   416 apply(subst Sequ_Union_in)
 
   461 apply(subst Der_Pow_Sequ[symmetric])
 
   417 apply(subst Der_Pow_Sequ[symmetric])
 
   462 apply(subst Pow.simps[symmetric])
 
   418 apply(subst Pow.simps[symmetric])
 
   463 apply(subst Der_UNION[symmetric])
 
   419 apply(subst Der_UNION[symmetric])
 
   483 | Char char
 
   439 | Char char
 
   484 | Seq val val
 
   440 | Seq val val
 
   485 | Right val
 
   441 | Right val
 
   486 | Left val
 
   442 | Left val
 
   487 | Stars "val list"
 
   443 | Stars "val list"
 
   488 
   444 | Nt val
 
   489 
   445 
   490 section {* The string behind a value *}
 
   446 section {* The string behind a value *}
 
   491 
   447 
   492 fun 
   448 fun 
   493   flat :: "val \<Rightarrow> string"
 
   449   flat :: "val \<Rightarrow> string"
 
   497 | "flat (Left v) = flat v"
 
   453 | "flat (Left v) = flat v"
 
   498 | "flat (Right v) = flat v"
 
   454 | "flat (Right v) = flat v"
 
   499 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
 
   455 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
 
   500 | "flat (Stars []) = []"
 
   456 | "flat (Stars []) = []"
 
   501 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
   457 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
       
   458 | "flat (Nt v) = flat v"
 
   502 
   459 
   503 abbreviation
 
   460 abbreviation
 
   504   "flats vs \<equiv> concat (map flat vs)"
 
   461   "flats vs \<equiv> concat (map flat vs)"
 
   505 
   462 
   506 lemma flat_Stars [simp]:
 
   463 lemma flat_Stars [simp]:
 
   595 where
 
   552 where
 
   596  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
 
   553  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
 
   597 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
   554 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
   598 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
   555 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
   599 | "\<Turnstile> Void : ONE"
 
   556 | "\<Turnstile> Void : ONE"
 
   600 | "\<Turnstile> Char c : CHAR c"
 
   557 | "\<Turnstile> Char c : CH c"
 
   601 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 
   558 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 
   602 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : UPNTIMES r n"
 
   559 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : UPNTIMES r n"
 
   603 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; 
   560 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; 
   604     \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; 
   561     \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; 
   605     length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n"
 
   562     length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n"
 
   620 inductive_cases Prf_elims:
 
   577 inductive_cases Prf_elims:
 
   621   "\<Turnstile> v : ZERO"
 
   578   "\<Turnstile> v : ZERO"
 
   622   "\<Turnstile> v : SEQ r1 r2"
 
   579   "\<Turnstile> v : SEQ r1 r2"
 
   623   "\<Turnstile> v : ALT r1 r2"
 
   580   "\<Turnstile> v : ALT r1 r2"
 
   624   "\<Turnstile> v : ONE"
 
   581   "\<Turnstile> v : ONE"
 
   625   "\<Turnstile> v : CHAR c"
 
   582   "\<Turnstile> v : CH c"
 
   626   "\<Turnstile> vs : STAR r"
 
   583   "\<Turnstile> vs : STAR r"
 
   627   "\<Turnstile> vs : UPNTIMES r n"
 
   584   "\<Turnstile> vs : UPNTIMES r n"
 
   628   "\<Turnstile> vs : NTIMES r n"
 
   585   "\<Turnstile> vs : NTIMES r n"
 
   629   "\<Turnstile> vs : FROMNTIMES r n"
 
   586   "\<Turnstile> vs : FROMNTIMES r n"
 
   630   "\<Turnstile> vs : NMTIMES r n m"
 
   587   "\<Turnstile> vs : NMTIMES r n m"
 
   865   then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" "length ss \<le> n"
 
   822   then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" "length ss \<le> n"
 
   866   using Pow_cstring_nonempty by force
 
   823   using Pow_cstring_nonempty by force
 
   867   then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n"
 
   824   then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n"
 
   868   using IH flats_cval_nonempty by (smt order.trans) 
   825   using IH flats_cval_nonempty by (smt order.trans) 
   869   then show "\<exists>v. \<Turnstile> v : UPNTIMES r n \<and> flat v = s"
 
   826   then show "\<exists>v. \<Turnstile> v : UPNTIMES r n \<and> flat v = s"
 
   870   using Prf.intros(7) flat_Stars by blast
 
   827     using Prf.intros(7) flat_Stars by blast
 
       
   828 next 
       
   829   case (NOT r)
 
       
   830   then show ?case sorry
 
   871 qed (auto intro: Prf.intros)
 
   831 qed (auto intro: Prf.intros)
 
   872 
   832 
   873 
   833 
   874 lemma L_flat_Prf:
 
   834 lemma L_flat_Prf:
 
   875   shows "L(r) = {flat v | v. \<Turnstile> v : r}"
 
   835   shows "L(r) = {flat v | v. \<Turnstile> v : r}"
 
   915 where  "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
 
   875 where  "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
 
   916 
   876 
   917 lemma LV_simps:
 
   877 lemma LV_simps:
 
   918   shows "LV ZERO s = {}"
 
   878   shows "LV ZERO s = {}"
 
   919   and   "LV ONE s = (if s = [] then {Void} else {})"
 
   879   and   "LV ONE s = (if s = [] then {Void} else {})"
 
   920   and   "LV (CHAR c) s = (if s = [c] then {Char c} else {})"
 
   880   and   "LV (CH c) s = (if s = [c] then {Char c} else {})"
 
   921   and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
 
   881   and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
 
   922 unfolding LV_def
 
   882 unfolding LV_def
 
   923 apply(auto intro: Prf.intros elim: Prf.cases)
 
   883 apply(auto intro: Prf.intros elim: Prf.cases)
 
   924 done
 
   884 done
 
   925 
   885 
  1224   show "finite (LV ZERO s)" by (simp add: LV_simps)
 
  1184   show "finite (LV ZERO s)" by (simp add: LV_simps)
 
  1225 next
 
  1185 next
 
  1226   case (ONE s)
 
  1186   case (ONE s)
 
  1227   show "finite (LV ONE s)" by (simp add: LV_simps)
 
  1187   show "finite (LV ONE s)" by (simp add: LV_simps)
 
  1228 next
 
  1188 next
 
  1229   case (CHAR c s)
 
  1189   case (CH c s)
 
  1230   show "finite (LV (CHAR c) s)" by (simp add: LV_simps)
 
  1190   show "finite (LV (CH c) s)" by (simp add: LV_simps)
 
  1231 next 
  1191 next 
  1232   case (ALT r1 r2 s)
 
  1192   case (ALT r1 r2 s)
 
  1233   then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
 
  1193   then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
 
  1234 next 
  1194 next 
  1235   case (SEQ r1 r2 s)
 
  1195   case (SEQ r1 r2 s)
 
  1268     by (metis (no_types, lifting) LV_NTIMES_4 LV_NTIMES_5 LV_STAR_finite finite_Stars_Append finite_Stars_Pow finite_UN_I finite_atMost finite_subset)
 
  1228     by (metis (no_types, lifting) LV_NTIMES_4 LV_NTIMES_5 LV_STAR_finite finite_Stars_Append finite_Stars_Pow finite_UN_I finite_atMost finite_subset)
 
  1269 next
 
  1229 next
 
  1270   case (NMTIMES r n m s)
 
  1230   case (NMTIMES r n m s)
 
  1271   have "\<And>s. finite (LV r s)" by fact
 
  1231   have "\<And>s. finite (LV r s)" by fact
 
  1272   then show "finite (LV (NMTIMES r n m) s)"
 
  1232   then show "finite (LV (NMTIMES r n m) s)"
 
  1273     by (simp add: LV_NMTIMES_6)         
  1233     by (simp add: LV_NMTIMES_6)    
       
  1234 next 
       
  1235   case (NOT r s)
 
       
  1236   then show ?case sorry
 
  1274 qed
 
  1237 qed
 
  1275 
  1238 
  1276 
  1239 
  1277 
  1240 
  1278 section {* Our POSIX Definition *}
 
  1241 section {* Our POSIX Definition *}
 
  1279 
  1242 
  1280 inductive 
  1243 inductive 
  1281   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
  1244   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 
  1282 where
 
  1245 where
 
  1283   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
 
  1246   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
 
  1284 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
 
  1247 | Posix_CHAR: "[c] \<in> (CH c) \<rightarrow> (Char c)"
 
  1285 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
  1248 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 
  1286 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
  1249 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 
  1287 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
 
  1250 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
 
  1288     \<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 r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
  1251     \<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 r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
  1289     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
 
  1252     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
 
  1318     \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (v # vs)"    
  1281     \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (v # vs)"    
  1319   
  1282   
  1320 inductive_cases Posix_elims:
 
  1283 inductive_cases Posix_elims:
 
  1321   "s \<in> ZERO \<rightarrow> v"
 
  1284   "s \<in> ZERO \<rightarrow> v"
 
  1322   "s \<in> ONE \<rightarrow> v"
 
  1285   "s \<in> ONE \<rightarrow> v"
 
  1323   "s \<in> CHAR c \<rightarrow> v"
 
  1286   "s \<in> CH c \<rightarrow> v"
 
  1324   "s \<in> ALT r1 r2 \<rightarrow> v"
 
  1287   "s \<in> ALT r1 r2 \<rightarrow> v"
 
  1325   "s \<in> SEQ r1 r2 \<rightarrow> v"
 
  1288   "s \<in> SEQ r1 r2 \<rightarrow> v"
 
  1326   "s \<in> STAR r \<rightarrow> v"
 
  1289   "s \<in> STAR r \<rightarrow> v"
 
  1327   "s \<in> NTIMES r n \<rightarrow> v"
 
  1290   "s \<in> NTIMES r n \<rightarrow> v"
 
  1328   "s \<in> UPNTIMES r n \<rightarrow> v"
 
  1291   "s \<in> UPNTIMES r n \<rightarrow> v"
 
  1394   case (Posix_ONE v2)
 
  1357   case (Posix_ONE v2)
 
  1395   have "[] \<in> ONE \<rightarrow> v2" by fact
 
  1358   have "[] \<in> ONE \<rightarrow> v2" by fact
 
  1396   then show "Void = v2" by cases auto
 
  1359   then show "Void = v2" by cases auto
 
  1397 next 
  1360 next 
  1398   case (Posix_CHAR c v2)
 
  1361   case (Posix_CHAR c v2)
 
  1399   have "[c] \<in> CHAR c \<rightarrow> v2" by fact
 
  1362   have "[c] \<in> CH c \<rightarrow> v2" by fact
 
  1400   then show "Char c = v2" by cases auto
 
  1363   then show "Char c = v2" by cases auto
 
  1401 next 
  1364 next 
  1402   case (Posix_ALT1 s r1 v r2 v2)
 
  1365   case (Posix_ALT1 s r1 v r2 v2)
 
  1403   have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
 
  1366   have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
 
  1404   moreover
 
  1367   moreover
 
  1501   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs')"
 
  1464   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs')"
 
  1502   apply(cases) apply (auto simp add: append_eq_append_conv2)
 
  1465   apply(cases) apply (auto simp add: append_eq_append_conv2)
 
  1503     using Posix1(1) Posix1(2) apply blast 
  1466     using Posix1(1) Posix1(2) apply blast 
  1504      apply(case_tac n)
 
  1467      apply(case_tac n)
 
  1505       apply(simp)
 
  1468       apply(simp)
 
  1506       apply(simp)
 
  1469      apply(simp)
 
  1507     apply(drule_tac x="va" in meta_spec)
 
  1470     apply (smt (verit, ccfv_threshold) L.simps(9) Posix1(1) UN_E append_eq_append_conv2)
 
  1508     apply(drule_tac x="vs" in meta_spec)
 
  1471     by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) append_Nil2 append_self_conv2)
 
  1509     apply(simp)
 
       
  1510      apply(drule meta_mp)
 
       
  1511     apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil diff_Suc_1 local.Posix_FROMNTIMES1(4) val.inject(5))
 
       
  1512     apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil)
 
       
  1513     by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) self_append_conv self_append_conv2)
 
       
  1514   moreover
 
  1472   moreover
 
  1515   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
 
  1473   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
 
  1516             "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
 
  1474             "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
 
  1517   ultimately show "Stars (v # vs) = v2" by auto    
  1475   ultimately show "Stars (v # vs) = v2" by auto    
  1518 next
 
  1476 next
 
  1553       apply(simp)
 
  1511       apply(simp)
 
  1554      apply(simp)
 
  1512      apply(simp)
 
  1555        apply(case_tac m)
 
  1513        apply(case_tac m)
 
  1556       apply(simp)
 
  1514       apply(simp)
 
  1557      apply(simp)
 
  1515      apply(simp)
 
  1558     apply(drule_tac x="va" in meta_spec)
 
  1516     apply (metis L.simps(10) Posix1(1) UN_E append.right_neutral append_Nil)
 
  1559     apply(drule_tac x="vs" in meta_spec)
 
  1517     by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append_Nil self_append_conv)
 
  1560     apply(simp)
 
       
  1561      apply(drule meta_mp)
 
       
  1562       apply(drule Posix1(1))
 
       
  1563       apply(drule Posix1(1))
 
       
  1564       apply(drule Posix1(1))
 
       
  1565       apply(frule Posix1(1))
 
       
  1566       apply(simp)
 
       
  1567     using Posix_NMTIMES1.hyps(4) apply force
 
       
  1568      apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2)
 
       
  1569     by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil)      
       
  1570   moreover
 
  1518   moreover
 
  1571   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
 
  1519   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
 
  1572             "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
 
  1520             "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
 
  1573   ultimately show "Stars (v # vs) = v2" by auto     
  1521   ultimately show "Stars (v # vs) = v2" by auto     
  1574 next
 
  1522 next
 
  1614      defer
 
  1562      defer
 
  1615   defer
 
  1563   defer
 
  1616      apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2]
 
  1564      apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2]
 
  1617   apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq)
 
  1565   apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq)
 
  1618      apply(simp)
 
  1566      apply(simp)
 
  1619      apply(clarify)
 
       
  1620      apply(case_tac n)
 
  1567      apply(case_tac n)
 
  1621       apply(simp)
 
  1568       apply(simp)
 
  1622      apply(simp)
 
  1569      apply(simp)
 
  1623      apply(erule Prf_elims)
 
  1570      apply(erule Prf_elims)
 
  1624       apply(simp)
 
  1571       apply(simp)
 
  1630      apply(simp)
 
  1577      apply(simp)
 
  1631      apply(rule Prf.intros)  
  1578      apply(rule Prf.intros)  
  1632       apply(simp)
 
  1579       apply(simp)
 
  1633      apply(simp)
 
  1580      apply(simp)
 
  1634     apply(simp)
 
  1581     apply(simp)
 
  1635    apply(clarify)
 
       
  1636    apply(erule Prf_elims)
 
  1582    apply(erule Prf_elims)
 
  1637       apply(simp)
 
  1583       apply(simp)
 
  1638   apply(rule Prf.intros)  
  1584   apply(rule Prf.intros)  
  1639        apply(simp)
 
  1585        apply(simp)
 
  1640      apply(simp)
 
  1586      apply(simp)
 
  1658   apply (metis Prf.intros(8) length_removeAll_less less_irrefl_nat removeAll.simps(1) self_append_conv2)
 
  1604   apply (metis Prf.intros(8) length_removeAll_less less_irrefl_nat removeAll.simps(1) self_append_conv2)
 
  1659   (* NMTIMES *)
 
  1605   (* NMTIMES *)
 
  1660   apply(simp)
 
  1606   apply(simp)
 
  1661   apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
 
  1607   apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
 
  1662   apply(simp)
 
  1608   apply(simp)
 
  1663   apply(clarify)
 
       
  1664   apply(rotate_tac 6)
 
  1609   apply(rotate_tac 6)
 
  1665   apply(erule Prf_elims)
 
  1610   apply(erule Prf_elims)
 
  1666    apply(simp)
 
  1611    apply(simp)
 
  1667   apply(subst append.simps(2)[symmetric])
 
  1612   apply(subst append.simps(2)[symmetric])
 
  1668       apply(rule Prf.intros) 
  1613       apply(rule Prf.intros) 
  1673   apply(rule Prf.intros) 
  1618   apply(rule Prf.intros) 
  1674         apply(simp)
 
  1619         apply(simp)
 
  1675   apply(simp)
 
  1620   apply(simp)
 
  1676   apply(simp)
 
  1621   apply(simp)
 
  1677   apply(simp)
 
  1622   apply(simp)
 
  1678   apply(clarify)
 
       
  1679   apply(rotate_tac 6)
 
  1623   apply(rotate_tac 6)
 
  1680   apply(erule Prf_elims)
 
  1624   apply(erule Prf_elims)
 
  1681    apply(simp)
 
  1625    apply(simp)
 
  1682       apply(rule Prf.intros) 
  1626       apply(rule Prf.intros) 
  1683         apply(simp)
 
  1627         apply(simp)
lexing