1    

     2 theory Positions

     3   imports "Lexer" 

     4 begin

     5 

     6 fun 

     7   at :: "val \<Rightarrow> nat list \<Rightarrow> val"

     8 where

     9   "at v [] = v"

    10 | "at (Left v) (0#ps)= at v ps"

    11 | "at (Right v) (Suc 0#ps)= at v ps"

    12 | "at (Seq v1 v2) (0#ps)= at v1 ps"

    13 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"

    14 | "at (Stars vs) (n#ps)= at (nth vs n) ps"

    15 

    16 (*

    17 fun 

    18   ato :: "val \<Rightarrow> nat list \<Rightarrow> val option"

    19 where

    20   "ato v [] = Some v"

    21 | "ato (Left v) (0#ps)= ato v ps"

    22 | "ato (Right v) (Suc 0#ps)= ato v ps"

    23 | "ato (Seq v1 v2) (0#ps)= ato v1 ps"

    24 | "ato (Seq v1 v2) (Suc 0#ps)= ato v2 ps"

    25 | "ato (Stars vs) (n#ps)= (if (n < length vs) then ato (nth vs n) ps else None)"

    26 | "ato v p = None"

    27 *)

    28 

    29 

    30 fun Pos :: "val \<Rightarrow> (nat list) set"

    31 where

    32   "Pos (Void) = {[]}"

    33 | "Pos (Char c) = {[]}"

    34 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"

    35 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"

    36 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" 

    37 | "Pos (Stars []) = {[]}"

    38 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {(Suc n)#ps | n ps. n#ps \<in> Pos (Stars vs)}"

    39 

    40 lemma Pos_empty:

    41   shows "[] \<in> Pos v"

    42 apply(induct v rule: Pos.induct)

    43 apply(auto)

    44 done

    45 

    46 lemma Pos_finite_aux:

    47   assumes "\<forall>v \<in> set vs. finite (Pos v)"

    48   shows "finite (Pos (Stars vs))"

    49 using assms

    50 apply(induct vs)

    51 apply(simp)

    52 apply(simp)

    53 apply(subgoal_tac "finite (Pos (Stars vs) - {[]})")

    54 apply(rule_tac f="\<lambda>l. Suc (hd l) # tl l" in finite_surj)

    55 apply(assumption)

    56 back

    57 apply(auto simp add: image_def)

    58 apply(rule_tac x="n#ps" in bexI)

    59 apply(simp)

    60 apply(simp)

    61 done

    62 

    63 lemma Pos_finite:

    64   shows "finite (Pos v)"

    65 apply(induct v rule: val.induct)

    66 apply(auto)

    67 apply(simp add: Pos_finite_aux)

    68 done

    69 

    70 (*

    71 lemma ato_test:

    72   assumes "p \<in> Pos v"

    73   shows "\<exists>v'. ato v p = Some v'"

    74 using assms

    75 apply(induct v arbitrary: p rule: Pos.induct)

    76 apply(auto)

    77 apply force

    78 by (metis ato.simps(6) option.distinct(1))

    79 *)

    80 

    81 

    82 definition pflat :: "val \<Rightarrow> nat list => string option"

    83 where

    84   "pflat v p \<equiv> (if p \<in> Pos v then Some (flat (at v p)) else None)"

    85 

    86 fun intlen :: "'a list \<Rightarrow> int"

    87 where

    88   "intlen [] = 0"

    89 | "intlen (x#xs) = 1 + intlen xs"

    90 

    91 lemma inlen_bigger:

    92   shows "0 \<le> intlen xs"

    93 apply(induct xs)

    94 apply(auto)

    95 done 

    96 

    97 lemma intlen_append:

    98   shows "intlen (xs @ ys) = intlen xs + intlen ys"

    99 apply(induct xs arbitrary: ys)

   100 apply(auto)

   101 done 

   102 

   103 lemma intlen_length:

   104   assumes "length xs < length ys"

   105   shows "intlen xs < intlen ys"

   106 using assms

   107 apply(induct xs arbitrary: ys)

   108 apply(auto)

   109 apply(case_tac ys)

   110 apply(simp_all)

   111 apply (smt inlen_bigger)

   112 by (smt Suc_lessE intlen.simps(2) length_Suc_conv)

   113 

   114 

   115 definition pflat_len :: "val \<Rightarrow> nat list => int"

   116 where

   117   "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"

   118 

   119 lemma pflat_len_simps:

   120   shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"

   121   and   "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"

   122   and   "pflat_len (Left v) (0#p) = pflat_len v p"

   123   and   "pflat_len (Left v) (Suc 0#p) = -1"

   124   and   "pflat_len (Right v) (Suc 0#p) = pflat_len v p"

   125   and   "pflat_len (Right v) (0#p) = -1"

   126   and   "pflat_len v [] = intlen (flat v)"

   127 apply(auto simp add: pflat_len_def Pos_empty)

   128 done

   129 

   130 lemma pflat_len_Stars_simps:

   131   assumes "n < length vs"

   132   shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"

   133 using assms 

   134 apply(induct vs arbitrary: n p)

   135 apply(simp)

   136 apply(simp)

   137 apply(simp add: pflat_len_def)

   138 apply(auto)[1]

   139 apply (metis at.simps(6))

   140 apply (metis Suc_less_eq Suc_pred)

   141 by (metis diff_Suc_1 less_Suc_eq_0_disj nth_Cons')

   142 

   143 

   144 lemma pflat_len_Stars_simps2:

   145   shows "pflat_len (Stars (v#vs)) (Suc n # p) = pflat_len (Stars vs) (n#p)"

   146   and   "pflat_len (Stars (v#vs)) (0 # p) = pflat_len v p"

   147 using assms 

   148 apply(simp_all add: pflat_len_def)

   149 done

   150 

   151 lemma Two_to_Three_aux:

   152   assumes "p \<in> Pos v1 \<union> Pos v2" "pflat_len v1 p = pflat_len v2 p"

   153   shows "p \<in> Pos v1 \<inter> Pos v2"

   154 using assms

   155 apply(simp add: pflat_len_def)

   156 apply(auto split: if_splits)

   157 apply (smt inlen_bigger)+

   158 done

   159 

   160 lemma Two_to_Three:

   161   assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat v1 p = pflat v2 p"

   162   shows "Pos v1 = Pos v2"

   163 using assms

   164 by (metis Un_iff option.distinct(1) pflat_def subsetI subset_antisym)

   165 

   166 lemma Two_to_Three_orig:

   167   assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p"

   168   shows "Pos v1 = Pos v2"

   169 using assms

   170 by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym)

   171 

   172 lemma set_eq1:

   173   assumes "insert [] A = insert [] B" "[] \<notin> A"  "[] \<notin> B"

   174   shows "A = B"

   175 using assms

   176 by (simp add: insert_ident)

   177 

   178 lemma set_eq2:

   179   assumes "A \<union> B = A \<union> C"

   180   and "A \<inter> B = {}" "A \<inter> C = {}"  

   181   shows "B = C"

   182 using assms

   183 using Un_Int_distrib sup_bot.left_neutral sup_commute by blast

   184 

   185 

   186 

   187 lemma Three_to_One:

   188   assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" 

   189   and "Pos v1 = Pos v2" 

   190   shows "v1 = v2"

   191 using assms

   192 apply(induct v1 arbitrary: r v2 rule: Pos.induct)

   193 apply(erule Prf.cases)

   194 apply(simp_all)

   195 apply(erule Prf.cases)

   196 apply(simp_all)

   197 apply(erule Prf.cases)

   198 apply(simp_all)

   199 apply(erule Prf.cases)

   200 apply(simp_all)

   201 apply(erule Prf.cases)

   202 apply(simp_all)

   203 apply(erule Prf.cases)

   204 apply(simp_all)

   205 apply(clarify)

   206 apply(simp add: insert_ident)

   207 apply(drule_tac x="r1a" in meta_spec)

   208 apply(drule_tac x="v1a" in meta_spec)

   209 apply(simp)

   210 apply(drule_tac meta_mp)

   211 thm subset_antisym

   212 apply(rule subset_antisym)

   213 apply(auto)[3]

   214 apply(clarify)

   215 apply(simp add: insert_ident)

   216 using Pos_empty apply blast

   217 apply(erule Prf.cases)

   218 apply(simp_all)

   219 apply(erule Prf.cases)

   220 apply(simp_all)

   221 apply(clarify)

   222 apply(simp add: insert_ident)

   223 using Pos_empty apply blast

   224 apply(simp add: insert_ident)

   225 apply(drule_tac x="r2a" in meta_spec)

   226 apply(drule_tac x="v2b" in meta_spec)

   227 apply(simp)

   228 apply(drule_tac meta_mp)

   229 apply(rule subset_antisym)

   230 apply(auto)[3]

   231 apply(erule Prf.cases)

   232 apply(simp_all)

   233 apply(erule Prf.cases)

   234 apply(simp_all)

   235 apply(simp add: insert_ident)

   236 apply(clarify)

   237 apply(drule_tac x="r1a" in meta_spec)

   238 apply(drule_tac x="r2a" in meta_spec)

   239 apply(drule_tac x="v1b" in meta_spec)

   240 apply(drule_tac x="v2c" in meta_spec)

   241 apply(simp)

   242 apply(drule_tac meta_mp)

   243 apply(rule subset_antisym)

   244 apply(rule subsetI)

   245 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}")

   246 prefer 2

   247 apply(auto)[1]

   248 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}")

   249 prefer 2

   250 apply (metis (no_types, lifting) Un_iff)

   251 apply(simp)

   252 apply(rule subsetI)

   253 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}")

   254 prefer 2

   255 apply(auto)[1]

   256 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}")

   257 prefer 2

   258 apply (metis (no_types, lifting) Un_iff)

   259 apply(simp (no_asm_use))

   260 apply(simp)

   261 apply(drule_tac meta_mp)

   262 apply(rule subset_antisym)

   263 apply(rule subsetI)

   264 apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2b}")

   265 prefer 2

   266 apply(auto)[1]

   267 apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}")

   268 prefer 2

   269 apply (metis (no_types, lifting) Un_iff)

   270 apply(simp)

   271 apply(rule subsetI)

   272 apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2c}")

   273 prefer 2

   274 apply(auto)[1]

   275 apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}  \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}")

   276 prefer 2

   277 apply (metis (no_types, lifting) Un_iff)

   278 apply(simp (no_asm_use))

   279 apply(simp)

   280 apply(erule Prf.cases)

   281 apply(simp_all)

   282 apply(erule Prf.cases)

   283 apply(simp_all)

   284 apply(auto)[1]

   285 using Pos_empty apply fastforce

   286 apply(erule Prf.cases)

   287 apply(simp_all)

   288 apply(erule Prf.cases)

   289 apply(simp_all)

   290 apply(auto)[1]

   291 using Pos_empty apply fastforce

   292 apply(clarify)

   293 apply(simp add: insert_ident)

   294 apply(drule_tac x="rb" in meta_spec)

   295 apply(drule_tac x="STAR rb" in meta_spec)

   296 apply(drule_tac x="vb" in meta_spec)

   297 apply(drule_tac x="Stars vsb" in meta_spec)

   298 apply(simp)

   299 apply(drule_tac meta_mp)

   300 apply(rule subset_antisym)

   301 apply(rule subsetI)

   302 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va}")

   303 prefer 2

   304 apply(auto)[1]

   305 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")

   306 prefer 2

   307 apply (metis (no_types, lifting) Un_iff)

   308 apply(simp)

   309 apply(rule subsetI)

   310 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb}")

   311 prefer 2

   312 apply(auto)[1]

   313 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")

   314 prefer 2

   315 apply (metis (no_types, lifting) Un_iff)

   316 apply(simp (no_asm_use))

   317 apply(simp)

   318 apply(drule_tac meta_mp)

   319 apply(rule subset_antisym)

   320 apply(rule subsetI)

   321 apply(case_tac vsa)

   322 apply(simp)

   323 apply (simp add: Pos_empty)

   324 apply(simp)

   325 apply(clarify)

   326 apply(erule disjE)

   327 apply (simp add: Pos_empty)

   328 apply(erule disjE)

   329 apply(clarify)

   330 apply(subgoal_tac 

   331   "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")

   332 prefer 2

   333 apply blast

   334 apply(subgoal_tac "Suc 0 # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union>  {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")

   335 prefer 2

   336 apply (metis (no_types, lifting) Un_iff)

   337 apply(simp)

   338 apply(clarify)

   339 apply(subgoal_tac 

   340   "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")

   341 prefer 2

   342 apply blast

   343 apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")

   344 prefer 2

   345 apply (metis (no_types, lifting) Un_iff)

   346 apply(simp)

   347 apply(rule subsetI)

   348 apply(case_tac vsb)

   349 apply(simp)

   350 apply (simp add: Pos_empty)

   351 apply(simp)

   352 apply(clarify)

   353 apply(erule disjE)

   354 apply (simp add: Pos_empty)

   355 apply(erule disjE)

   356 apply(clarify)

   357 apply(subgoal_tac 

   358   "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")

   359 prefer 2

   360 apply(simp)

   361 apply(subgoal_tac "Suc 0 # ps \<in> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")

   362 apply blast

   363 using list.inject apply blast

   364 apply(clarify)

   365 apply(subgoal_tac 

   366   "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")

   367 prefer 2

   368 apply(simp)

   369 apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")

   370 prefer 2

   371 apply (metis (no_types, lifting) Un_iff)

   372 apply(simp (no_asm_use))

   373 apply(simp)

   374 done

   375 

   376 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _")

   377 where

   378   "ps1 \<sqsubseteq>pre ps2 \<equiv> (\<exists>ps'. ps1 @ps' = ps2)"

   379 

   380 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _")

   381 where

   382   "ps1 \<sqsubset>spre ps2 \<equiv> (ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2)"

   383 

   384 inductive lex_lists :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")

   385 where

   386   "[] \<sqsubset>lex p#ps"

   387 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"

   388 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"

   389 

   390 lemma lex_irrfl:

   391   fixes ps1 ps2 :: "nat list"

   392   assumes "ps1 \<sqsubset>lex ps2"

   393   shows "ps1 \<noteq> ps2"

   394 using assms

   395 apply(induct rule: lex_lists.induct)

   396 apply(auto)

   397 done

   398 

   399 lemma lex_append:

   400   assumes "ps2 \<noteq> []"  

   401   shows "ps \<sqsubset>lex ps @ ps2"

   402 using assms

   403 apply(induct ps)

   404 apply(auto intro: lex_lists.intros)

   405 apply(case_tac ps2)

   406 apply(simp)

   407 apply(simp)

   408 apply(auto intro: lex_lists.intros)

   409 done

   410 

   411 lemma lexordp_simps [simp]:

   412   fixes xs ys :: "nat list"

   413   shows "[] \<sqsubset>lex ys = (ys \<noteq> [])"

   414   and   "xs \<sqsubset>lex [] = False"

   415   and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))"

   416 apply -

   417 apply (metis lex_append lex_lists.simps list.simps(3))

   418 using lex_lists.cases apply blast

   419 using lex_lists.cases lex_lists.intros(2) lex_lists.intros(3) not_less_iff_gr_or_eq by fastforce

   420 

   421 lemma lex_append_cancel [simp]:

   422   fixes ps ps1 ps2 :: "nat list"

   423   shows "ps @ ps1 \<sqsubset>lex ps @ ps2 \<longleftrightarrow> ps1 \<sqsubset>lex ps2"

   424 apply(induct ps)

   425 apply(auto)

   426 done

   427 

   428 lemma lex_trans:

   429   fixes ps1 ps2 ps3 :: "nat list"

   430   assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"

   431   shows "ps1 \<sqsubset>lex ps3"

   432 using assms

   433 apply(induct arbitrary: ps3 rule: lex_lists.induct)

   434 apply(erule lex_lists.cases)

   435 apply(simp_all)

   436 apply(rotate_tac 2)

   437 apply(erule lex_lists.cases)

   438 apply(simp_all)

   439 apply(erule lex_lists.cases)

   440 apply(simp_all)

   441 done

   442 

   443 lemma trichotomous_aux:

   444   fixes p q :: "nat list"

   445   assumes "p \<sqsubset>lex q" "p \<noteq> q"

   446   shows "\<not>(q \<sqsubset>lex p)"

   447 using assms

   448 apply(induct rule: lex_lists.induct)

   449 apply(auto)

   450 done

   451 

   452 lemma trichotomous_aux2:

   453   fixes p q :: "nat list"

   454   assumes "p \<sqsubset>lex q" "q \<sqsubset>lex p"

   455   shows "False"

   456 using assms

   457 apply(induct rule: lex_lists.induct)

   458 apply(auto)

   459 done

   460 

   461 lemma trichotomous:

   462   fixes p q :: "nat list"

   463   shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"

   464 apply(induct p arbitrary: q)

   465 apply(auto)

   466 apply(case_tac q)

   467 apply(auto)

   468 done

   469 

   470 definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" 

   471   where

   472   "dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)"

   473 

   474 definition

   475   "DPos v1 v2 \<equiv> {p. dpos v1 v2 p}"

   476 

   477 lemma outside_lemma:

   478   assumes "p \<notin> Pos v1 \<union> Pos v2"

   479   shows "pflat_len v1 p = pflat_len v2 p"

   480 using assms

   481 apply(auto simp add: pflat_len_def)

   482 done

   483 

   484 lemma dpos_lemma_aux:

   485   assumes "p \<in> Pos v1 \<union> Pos v2"

   486   and "pflat_len v1 p = pflat_len v2 p"

   487   shows "p \<in> Pos v1 \<inter> Pos v2"

   488 using assms

   489 apply(auto simp add: pflat_len_def)

   490 apply (smt inlen_bigger)

   491 apply (smt inlen_bigger)

   492 done

   493 

   494 lemma dpos_lemma:

   495   assumes "p \<in> Pos v1 \<union> Pos v2"

   496   and "pflat_len v1 p = pflat_len v2 p"

   497   shows "\<not>dpos v1 v2 p"

   498 using assms

   499 apply(auto simp add: dpos_def dpos_lemma_aux)

   500 using dpos_lemma_aux apply auto[1]

   501 using dpos_lemma_aux apply auto[1]

   502 done

   503 

   504 lemma dpos_lemma2:

   505   assumes "p \<in> Pos v1 \<union> Pos v2"

   506   and "dpos v1 v2 p"

   507   shows "pflat_len v1 p \<noteq> pflat_len v2 p"

   508 using assms

   509 using dpos_lemma by blast

   510 

   511 lemma DPos_lemma:

   512   assumes "p \<in> DPos v1 v2"

   513   shows "pflat_len v1 p \<noteq> pflat_len v2 p"

   514 using assms

   515 unfolding DPos_def 

   516 apply(auto simp add: pflat_len_def dpos_def)

   517 apply (smt inlen_bigger)

   518 by (smt inlen_bigger)

   519 

   520 

   521 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")

   522 where

   523   "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> pflat_len v1 p > pflat_len v2 p \<and>

   524                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))"

   525 

   526 

   527 definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _")

   528 where

   529   "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"

   530 

   531 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _")

   532 where

   533   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"

   534 

   535 lemma val_ord_shorterI:

   536   assumes "length (flat v') < length (flat v)"

   537   shows "v :\<sqsubset>val v'" 

   538 using assms(1)

   539 apply(subst val_ord_ex_def)

   540 apply(rule_tac x="[]" in exI)

   541 apply(subst val_ord_def)

   542 apply(rule conjI)

   543 apply (simp add: Pos_empty)

   544 apply(rule conjI)

   545 apply(simp add: pflat_len_simps)

   546 apply (simp add: intlen_length)

   547 apply(simp)

   548 done

   549 

   550 lemma val_ord_spre:

   551   assumes "(flat v') \<sqsubset>spre (flat v)"

   552   shows "v :\<sqsubset>val v'" 

   553 using assms(1)

   554 apply(rule_tac val_ord_shorterI)

   555 apply(simp add: sprefix_list_def prefix_list_def)

   556 apply(auto)

   557 apply(case_tac ps')

   558 apply(auto)

   559 by (metis append_eq_conv_conj drop_all le_less_linear neq_Nil_conv)

   560 

   561 

   562 lemma val_ord_ALTI:

   563   assumes "v \<sqsubset>val p v'" "flat v = flat v'"

   564   shows "(Left v) \<sqsubset>val (0#p) (Left v')" 

   565 using assms(1)

   566 apply(subst (asm) val_ord_def)

   567 apply(erule conjE)

   568 apply(subst val_ord_def)

   569 apply(rule conjI)

   570 apply(simp)

   571 apply(rule conjI)

   572 apply(simp add: pflat_len_simps)

   573 apply(rule ballI)

   574 apply(rule impI)

   575 apply(simp only: Pos.simps)

   576 apply(auto)[1]

   577 using assms(2)

   578 apply(simp add: pflat_len_simps)

   579 apply(auto simp add: pflat_len_simps)[2]

   580 done

   581 

   582 lemma val_ord_ALTI2:

   583   assumes "v \<sqsubset>val p v'" "flat v = flat v'"

   584   shows "(Right v) \<sqsubset>val (1#p) (Right v')" 

   585 using assms(1)

   586 apply(subst (asm) val_ord_def)

   587 apply(erule conjE)

   588 apply(subst val_ord_def)

   589 apply(rule conjI)

   590 apply(simp)

   591 apply(rule conjI)

   592 apply(simp add: pflat_len_simps)

   593 apply(rule ballI)

   594 apply(rule impI)

   595 apply(simp only: Pos.simps)

   596 apply(auto)[1]

   597 using assms(2)

   598 apply(simp add: pflat_len_simps)

   599 apply(auto simp add: pflat_len_simps)[2]

   600 done

   601 

   602 lemma val_ord_ALTE:

   603   assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)"

   604   shows "p = 0 \<and> v1 \<sqsubset>val ps v2"

   605 using assms(1)

   606 apply(simp add: val_ord_def)

   607 apply(auto simp add: pflat_len_simps)

   608 apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)

   609 by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)

   610 

   611 lemma val_ord_ALTE2:

   612   assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)"

   613   shows "p = 1 \<and> v1 \<sqsubset>val ps v2"

   614 using assms(1)

   615 apply(simp add: val_ord_def)

   616 apply(auto simp add: pflat_len_simps)

   617 apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)

   618 by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)

   619 

   620 lemma val_ord_STARI:

   621   assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"

   622   shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))" 

   623 using assms(1)

   624 apply(subst (asm) val_ord_def)

   625 apply(erule conjE)

   626 apply(subst val_ord_def)

   627 apply(rule conjI)

   628 apply(simp)

   629 apply(rule conjI)

   630 apply(subst pflat_len_Stars_simps)

   631 apply(simp)

   632 apply(subst pflat_len_Stars_simps)

   633 apply(simp)

   634 apply(simp)

   635 apply(rule ballI)

   636 apply(rule impI)

   637 apply(simp)

   638 apply(auto)

   639 using assms(2)

   640 apply(simp add: pflat_len_simps)

   641 apply(auto simp add: pflat_len_Stars_simps)

   642 done

   643 

   644 lemma val_ord_STARI2:

   645   assumes "(Stars vs1) \<sqsubset>val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"

   646   shows "(Stars (v#vs1)) \<sqsubset>val (Suc n#p) (Stars (v#vs2))" 

   647 using assms(1)

   648 apply(subst (asm) val_ord_def)

   649 apply(erule conjE)+

   650 apply(subst val_ord_def)

   651 apply(rule conjI)

   652 apply(simp)

   653 apply(rule conjI)

   654 apply(case_tac vs1)

   655 apply(simp)

   656 apply(simp)

   657 apply(auto)[1]

   658 apply(case_tac vs2)

   659 apply(simp)

   660 apply (simp add: pflat_len_def)

   661 apply(simp)

   662 apply(auto)[1]

   663 apply (simp add: pflat_len_Stars_simps)

   664 using pflat_len_def apply auto[1]

   665 apply(rule ballI)

   666 apply(rule impI)

   667 apply(simp)

   668 using assms(2)

   669 apply(auto)

   670 apply (simp add: pflat_len_simps(7))

   671 apply (simp add: pflat_len_Stars_simps)

   672 using assms(2)

   673 apply(auto simp add: pflat_len_def)[1]

   674 apply force

   675 apply force

   676 apply(auto simp add: pflat_len_def)[1]

   677 apply force

   678 apply force

   679 apply(auto simp add: pflat_len_def)[1]

   680 apply(auto simp add: pflat_len_def)[1]

   681 apply force

   682 apply force

   683 apply(auto simp add: pflat_len_def)[1]

   684 apply force

   685 apply force

   686 done

   687 

   688 

   689 lemma val_ord_SEQI:

   690   assumes "v1 \<sqsubset>val p v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"

   691   shows "(Seq v1 v2) \<sqsubset>val (0#p) (Seq v1' v2')" 

   692 using assms(1)

   693 apply(subst (asm) val_ord_def)

   694 apply(erule conjE)

   695 apply(subst val_ord_def)

   696 apply(rule conjI)

   697 apply(simp)

   698 apply(rule conjI)

   699 apply(simp add: pflat_len_simps)

   700 apply(rule ballI)

   701 apply(rule impI)

   702 apply(simp only: Pos.simps)

   703 apply(auto)[1]

   704 apply(simp add: pflat_len_simps)

   705 using assms(2)

   706 apply(simp)

   707 apply(auto simp add: pflat_len_simps)[2]

   708 done

   709 

   710 

   711 lemma val_ord_SEQI2:

   712   assumes "v2 \<sqsubset>val p v2'" "flat v2 = flat v2'"

   713   shows "(Seq v v2) \<sqsubset>val (1#p) (Seq v v2')" 

   714 using assms(1)

   715 apply(subst (asm) val_ord_def)

   716 apply(erule conjE)+

   717 apply(subst val_ord_def)

   718 apply(rule conjI)

   719 apply(simp)

   720 apply(rule conjI)

   721 apply(simp add: pflat_len_simps)

   722 apply(rule ballI)

   723 apply(rule impI)

   724 apply(simp only: Pos.simps)

   725 apply(auto)

   726 apply(auto simp add: pflat_len_def intlen_append)

   727 apply(auto simp add: assms(2))

   728 done

   729 

   730 lemma val_ord_SEQE_0:

   731   assumes "(Seq v1 v2) \<sqsubset>val 0#p (Seq v1' v2')" 

   732   shows "v1 \<sqsubset>val p v1'"

   733 using assms(1)

   734 apply(simp add: val_ord_def val_ord_ex_def)

   735 apply(auto)[1]

   736 apply(simp add: pflat_len_simps)

   737 apply(simp add: val_ord_def pflat_len_def)

   738 apply(auto)[1]

   739 apply(drule_tac x="0#q" in bspec)

   740 apply(simp)

   741 apply(simp)

   742 apply(drule_tac x="0#q" in bspec)

   743 apply(simp)

   744 apply(simp)

   745 apply(drule_tac x="0#q" in bspec)

   746 apply(simp)

   747 apply(simp)

   748 apply(simp add: val_ord_def pflat_len_def)

   749 apply(auto)[1]

   750 done

   751 

   752 lemma val_ord_SEQE_1:

   753   assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" 

   754   shows "v2 \<sqsubset>val p v2'"

   755 using assms(1)

   756 apply(simp add: val_ord_def pflat_len_def)

   757 apply(auto)[1]

   758 apply(drule_tac x="1#q" in bspec)

   759 apply(simp)

   760 apply(simp)

   761 apply(drule_tac x="1#q" in bspec)

   762 apply(simp)

   763 apply(simp)

   764 apply(drule_tac x="1#q" in bspec)

   765 apply(simp)

   766 apply(auto)[1]

   767 apply(drule_tac x="1#q" in bspec)

   768 apply(simp)

   769 apply(auto)

   770 apply(simp add: intlen_append)

   771 apply force

   772 apply(simp add: intlen_append)

   773 apply force

   774 apply(simp add: intlen_append)

   775 apply force

   776 apply(simp add: intlen_append)

   777 apply force

   778 done

   779 

   780 lemma val_ord_SEQE_2:

   781   assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" 

   782   and "\<turnstile> v1 : r" "\<turnstile> v1' : r" 

   783   shows "v1 = v1'"

   784 proof -

   785   have "\<forall>q \<in> Pos v1 \<union> Pos v1'. 0 # q \<sqsubset>lex 1#p \<longrightarrow> pflat_len v1 q = pflat_len v1' q"

   786   using assms(1) 

   787   apply(simp add: val_ord_def)

   788   apply(rule ballI)

   789   apply(clarify)

   790   apply(drule_tac x="0#q" in bspec)

   791   apply(auto)[1]

   792   apply(simp add: pflat_len_simps)

   793   done

   794   then have "Pos v1 = Pos v1'"

   795   apply(rule_tac Two_to_Three_orig)

   796   apply(rule ballI)

   797   apply(drule_tac x="pa" in bspec)

   798   apply(simp)

   799   apply(simp)

   800   done

   801   then show "v1 = v1'" 

   802   apply(rule_tac Three_to_One)

   803   apply(rule assms)

   804   apply(rule assms)

   805   apply(simp)

   806   done

   807 qed

   808 

   809 lemma val_ord_SEQ:

   810   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 

   811   and "flat (Seq v1 v2) = flat (Seq v1' v2')"

   812   and "\<turnstile> v1 : r" "\<turnstile> v1' : r" 

   813   shows "(v1 :\<sqsubset>val v1') \<or> (v1 = v1' \<and> (v2 :\<sqsubset>val v2'))"

   814 using assms(1)

   815 apply(subst (asm) val_ord_ex_def)

   816 apply(erule exE)

   817 apply(simp only: val_ord_def)

   818 apply(simp)

   819 apply(erule conjE)+

   820 apply(erule disjE)

   821 prefer 2

   822 apply(erule disjE)

   823 apply(erule exE)

   824 apply(rule disjI1)

   825 apply(simp)

   826 apply(subst val_ord_ex_def)

   827 apply(rule_tac x="ps" in exI)

   828 apply(rule val_ord_SEQE_0)

   829 apply(simp add: val_ord_def)

   830 apply(erule exE)

   831 apply(rule disjI2)

   832 apply(rule conjI)

   833 thm val_ord_SEQE_1

   834 apply(rule_tac val_ord_SEQE_2)

   835 apply(auto simp add: val_ord_def)[3]

   836 apply(rule assms(3))

   837 apply(rule assms(4))

   838 apply(subst val_ord_ex_def)

   839 apply(rule_tac x="ps" in exI)

   840 apply(rule_tac val_ord_SEQE_1)

   841 apply(auto simp add: val_ord_def)[1]

   842 apply(simp)

   843 using assms(2)

   844 apply(simp add: pflat_len_simps)

   845 done

   846 

   847 

   848 lemma val_ord_ex_trans:

   849   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"

   850   shows "v1 :\<sqsubset>val v3"

   851 using assms

   852 unfolding val_ord_ex_def

   853 apply(clarify)

   854 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p")

   855 prefer 2

   856 apply(rule trichotomous)

   857 apply(erule disjE)

   858 apply(simp)

   859 apply(rule_tac x="pa" in exI)

   860 apply(subst val_ord_def)

   861 apply(rule conjI)

   862 apply(simp add: val_ord_def)

   863 apply(auto)[1]

   864 apply(simp add: val_ord_def)

   865 apply(simp add: val_ord_def)

   866 apply(auto)[1]

   867 using outside_lemma apply blast

   868 apply(simp add: val_ord_def)

   869 apply(auto)[1]

   870 using outside_lemma apply force

   871 apply auto[1]

   872 apply(simp add: val_ord_def)

   873 apply(auto)[1]

   874 apply (metis (no_types, hide_lams) lex_trans outside_lemma)

   875 apply(simp add: val_ord_def)

   876 apply(auto)[1]

   877 by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)

   878 

   879 

   880 definition fdpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" 

   881 where

   882   "fdpos v1 v2 p \<equiv>  ({q. q \<sqsubset>lex p} \<inter> DPos v1 v2 = {})"

   883 

   884 

   885 lemma pos_append:

   886   assumes "p @ q \<in> Pos v"

   887   shows "q \<in> Pos (at v p)"

   888 using assms

   889 apply(induct arbitrary: p q rule: Pos.induct) 

   890 apply(simp_all)

   891 apply(auto)[1]

   892 apply(simp add: append_eq_Cons_conv)

   893 apply(auto)[1]

   894 apply(auto)[1]

   895 apply(simp add: append_eq_Cons_conv)

   896 apply(auto)[1]

   897 apply(auto)[1]

   898 apply(simp add: append_eq_Cons_conv)

   899 apply(auto)[1]

   900 apply(simp add: append_eq_Cons_conv)

   901 apply(auto)[1]

   902 apply(auto)[1]

   903 apply(simp add: append_eq_Cons_conv)

   904 apply(auto)[1]

   905 apply(simp add: append_eq_Cons_conv)

   906 apply(auto)[1]

   907 by (metis append_Cons at.simps(6))

   908 

   909 

   910 lemma Pos_pre:

   911   assumes "p \<in> Pos v" "q \<sqsubseteq>pre p"

   912   shows "q \<in> Pos v"

   913 using assms

   914 apply(induct v arbitrary: p q rule: Pos.induct)

   915 apply(simp_all add: prefix_list_def)

   916 apply (meson append_eq_Cons_conv append_is_Nil_conv)

   917 apply (meson append_eq_Cons_conv append_is_Nil_conv)

   918 apply (metis (no_types, lifting) Cons_eq_append_conv append_is_Nil_conv)

   919 apply(auto)

   920 apply (meson append_eq_Cons_conv)

   921 apply(simp add: append_eq_Cons_conv)

   922 apply(auto)

   923 done

   924 

   925 lemma lex_lists_order:

   926   assumes "q' \<sqsubset>lex q" "\<not>(q' \<sqsubseteq>pre q)"

   927   shows "\<not>(q \<sqsubset>lex q')"

   928 using assms

   929 apply(induct rule: lex_lists.induct)

   930 apply(simp add: prefix_list_def)

   931 apply(auto)

   932 using trichotomous_aux2 by auto

   933 

   934 lemma lex_appendL:

   935   assumes "q \<sqsubset>lex p" 

   936   shows "q \<sqsubset>lex p @ q'"

   937 using assms

   938 apply(induct arbitrary: q' rule: lex_lists.induct)

   939 apply(auto)

   940 done

   941 

   942 

   943 inductive 

   944   CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)

   945 where

   946  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"

   947 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"

   948 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"

   949 | "\<Turnstile> Void : ONE"

   950 | "\<Turnstile> Char c : CHAR c"

   951 | "\<Turnstile> Stars [] : STAR r"

   952 | "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"

   953 

   954 lemma Prf_CPrf:

   955   assumes "\<Turnstile> v : r"

   956   shows "\<turnstile> v : r"

   957 using assms

   958 apply(induct)

   959 apply(auto intro: Prf.intros)

   960 done

   961 

   962 definition

   963   "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"

   964 

   965 definition

   966   "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"

   967 

   968 lemma CPT_CPTpre_subset:

   969   shows "CPT r s \<subseteq> CPTpre r s"

   970 apply(auto simp add: CPT_def CPTpre_def)

   971 done

   972 

   973 

   974 lemma CPTpre_subsets:

   975   "CPTpre ZERO s = {}"

   976   "CPTpre ONE s \<subseteq> {Void}"

   977   "CPTpre (CHAR c) s \<subseteq> {Char c}"

   978   "CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"

   979   "CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"

   980   "CPTpre (STAR r) s \<subseteq> {Stars []} \<union>

   981     {Stars (v#vs) | v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}"

   982   "CPTpre (STAR r) [] = {Stars []}"

   983 apply(auto simp add: CPTpre_def)

   984 apply(erule CPrf.cases)

   985 apply(simp_all)

   986 apply(erule CPrf.cases)

   987 apply(simp_all)

   988 apply(erule CPrf.cases)

   989 apply(simp_all)

   990 apply(erule CPrf.cases)

   991 apply(simp_all)

   992 apply(erule CPrf.cases)

   993 apply(simp_all)

   994 apply(erule CPrf.cases)

   995 apply(simp_all)

   996 apply(erule CPrf.cases)

   997 apply(simp_all)

   998 apply(rule CPrf.intros)

   999 done

  1000 

  1001 

  1002 lemma CPTpre_simps:

  1003   shows "CPTpre ONE s = {Void}"

  1004   and   "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})"

  1005   and   "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"

  1006   and   "CPTpre (SEQ r1 r2) s = 

  1007           {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"

  1008 apply -

  1009 apply(rule subset_antisym)

  1010 apply(rule CPTpre_subsets)

  1011 apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1]

  1012 apply(case_tac "c = d")

  1013 apply(simp)

  1014 apply(rule subset_antisym)

  1015 apply(rule CPTpre_subsets)

  1016 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]

  1017 apply(simp)

  1018 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]

  1019 apply(erule CPrf.cases)

  1020 apply(simp_all)

  1021 apply(rule subset_antisym)

  1022 apply(rule CPTpre_subsets)

  1023 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]

  1024 apply(rule subset_antisym)

  1025 apply(rule CPTpre_subsets)

  1026 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]

  1027 done

  1028 

  1029 lemma CPT_simps:

  1030   shows "CPT ONE s = (if s = [] then {Void} else {})"

  1031   and   "CPT (CHAR c) [d] = (if c = d then {Char c} else {})"

  1032   and   "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"

  1033   and   "CPT (SEQ r1 r2) s = 

  1034           {Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}"

  1035 apply -

  1036 apply(rule subset_antisym)

  1037 apply(auto simp add: CPT_def)[1]

  1038 apply(erule CPrf.cases)

  1039 apply(simp_all)[7]

  1040 apply(erule CPrf.cases)

  1041 apply(simp_all)[7]

  1042 apply(auto simp add: CPT_def intro: CPrf.intros)[1]

  1043 apply(auto simp add: CPT_def intro: CPrf.intros)[1]

  1044 apply(erule CPrf.cases)

  1045 apply(simp_all)[7]

  1046 apply(erule CPrf.cases)

  1047 apply(simp_all)[7]

  1048 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]

  1049 apply(erule CPrf.cases)

  1050 apply(simp_all)[7]

  1051 apply(clarify)

  1052 apply blast

  1053 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]

  1054 apply(erule CPrf.cases)

  1055 apply(simp_all)[7]

  1056 done

  1057 

  1058 lemma CPTpre_SEQ:

  1059   assumes "v \<in> CPTpre (SEQ r1 r2) s"

  1060   shows "\<exists>s'. flat v = s' \<and> (s' \<sqsubseteq>pre s) \<and> s' \<in> L (SEQ r1 r2)"

  1061 using assms

  1062 apply(simp add: CPTpre_simps)

  1063 apply(auto simp add: CPTpre_def)

  1064 apply (simp add: prefix_list_def)

  1065 by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5))

  1066 

  1067 lemma Cond_prefix:

  1068   assumes "\<forall>s\<^sub>3. s1 @ s\<^sub>3 \<in> L r1 \<longrightarrow> s\<^sub>3 = [] \<or> (\<forall>s\<^sub>4. s1 @ s\<^sub>3 @ s\<^sub>4 \<sqsubseteq>pre s1 @ s2 \<longrightarrow> s\<^sub>4 \<notin> L r2)"

  1069   and "t1 \<in> L r1" "t2 \<in> L r2" "t1 @ t2 \<sqsubseteq>pre s1 @ s2"

  1070   shows "t1 \<sqsubseteq>pre s1"

  1071 using assms

  1072 apply(auto simp add: Sequ_def prefix_list_def append_eq_append_conv2)

  1073 done

  1074 

  1075 

  1076 

  1077 lemma test: 

  1078   assumes "finite A"

  1079   shows "finite {vs. Stars vs \<in> A}"

  1080 using assms

  1081 apply(induct A)

  1082 apply(simp)

  1083 apply(auto)

  1084 apply(case_tac x)

  1085 apply(simp_all)

  1086 done

  1087 

  1088 lemma CPTpre_STAR_finite:

  1089   assumes "\<And>s. finite (CPTpre r s)"

  1090   shows "finite (CPTpre (STAR r) s)"

  1091 apply(induct s rule: length_induct)

  1092 apply(case_tac xs)

  1093 apply(simp)

  1094 apply(simp add: CPTpre_subsets)

  1095 apply(rule finite_subset)

  1096 apply(rule CPTpre_subsets)

  1097 apply(simp)

  1098 apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)

  1099 apply(auto)[1]

  1100 apply(rule finite_imageI)

  1101 apply(simp add: Collect_case_prod_Sigma)

  1102 apply(rule finite_SigmaI)

  1103 apply(rule assms)

  1104 apply(case_tac "flat v = []")

  1105 apply(simp)

  1106 apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)

  1107 apply(simp)

  1108 apply(auto)[1]

  1109 apply(rule test)

  1110 apply(simp)

  1111 done

  1112 

  1113 lemma CPTpre_finite:

  1114   shows "finite (CPTpre r s)"

  1115 apply(induct r arbitrary: s)

  1116 apply(simp add: CPTpre_subsets)

  1117 apply(rule finite_subset)

  1118 apply(rule CPTpre_subsets)

  1119 apply(simp)

  1120 apply(rule finite_subset)

  1121 apply(rule CPTpre_subsets)

  1122 apply(simp)

  1123 apply(rule finite_subset)

  1124 apply(rule CPTpre_subsets)

  1125 thm finite_subset

  1126 apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2).  v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset)

  1127 apply(auto)[1]

  1128 apply(rule finite_imageI)

  1129 apply(simp add: Collect_case_prod_Sigma)

  1130 apply(rule finite_subset)

  1131 apply(rule CPTpre_subsets)

  1132 apply(simp)

  1133 by (simp add: CPTpre_STAR_finite)

  1134 

  1135