9 

     9 fun 

    10 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ >_ _" [100, 100, 100] 100)

    10   size :: "val \<Rightarrow> nat"

    11 where

    11 where

    12   C2: "v1 >r1 v1' \<Longrightarrow> (Seq v1 v2) >(SEQ r1 r2) (Seq v1' v2')" 

    12   "size (Void) = 0"

    13 | C1: "v2 >r2 v2' \<Longrightarrow> (Seq v1 v2) >(SEQ r1 r2) (Seq v1 v2')" 

    13 | "size (Char c) = 0"

    14 | A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) >(ALT r1 r2) (Left v1)"

    14 | "size (Left v) = 1 + size v"

    15 | A2: "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) >(ALT r1 r2) (Right v2)"

    15 | "size (Right v) = 1 + size v"

    16 | A3: "v2 >r2 v2' \<Longrightarrow> (Right v2) >(ALT r1 r2) (Right v2')"

    16 | "size (Seq v1 v2) = 1 + (size v1) + (size v2)"

    17 | A4: "v1 >r1 v1' \<Longrightarrow> (Left v1) >(ALT r1 r2) (Left v1')"

    17 | "size (Stars []) = 0"

    18 | K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) >(STAR r) (Stars (v # vs))"

    18 | "size (Stars (v#vs)) = 1 + (size v) + (size (Stars vs))" 

    19 | K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) >(STAR r) (Stars [])"

    19 

    20 | K3: "v1 >r v2 \<Longrightarrow> (Stars (v1 # vs1)) >(STAR r) (Stars (v2 # vs2))"

    20 lemma Star_size [simp]:

    21 | K4: "(Stars vs1) >(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) >(STAR r) (Stars (v # vs2))"

    21   "\<lbrakk>n < length vs; 0 < length vs\<rbrakk> \<Longrightarrow> size (nth vs n) < size (Stars vs)"

    22 apply(induct vs arbitrary: n)

    23 apply(simp)

    24 apply(auto)

    25 by (metis One_nat_def Suc_pred less_Suc0 less_Suc_eq list.size(3) not_add_less1 not_less_eq nth_Cons' trans_less_add2)

    26 

    27 lemma Star_size0 [simp]:

    28   "0 < length vs \<Longrightarrow> 0 < size (Stars vs)"

    29 apply(induct vs)

    30 apply(auto)

    31 done

    32 

    33 

    34 fun 

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

    36 where

    37   "at v [] = v"

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

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

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

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

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

    43 

    44 fun 

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

    46 where

    47   "ato v [] = Some v"

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

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

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

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

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

    53 | "ato v p = None"

    54 

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

    56 where

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

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

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

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

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

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

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

    64 

    65 lemma Pos_empty:

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

    67 apply(induct v rule: Pos.induct)

    68 apply(auto)

    69 done

    70 

    71 lemma Pos_finite_aux:

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

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

    74 using assms

    75 apply(induct vs)

    76 apply(simp)

    77 apply(simp)

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

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

    80 apply(assumption)

    81 back

    82 apply(auto simp add: image_def)

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

    84 apply(simp)

    85 apply(simp)

    86 done

    87 

    88 lemma Pos_finite:

    89   shows "finite (Pos v)"

    90 apply(induct v rule: val.induct)

    91 apply(auto)

    92 apply(simp add: Pos_finite_aux)

    93 done

    94 

    95 

    96 lemma ato_test:

    97   assumes "p \<in> Pos v"

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

    99 using assms

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

   101 apply(auto)

   102 apply force

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

   104 

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

   106 where

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

   108 

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

   110 where

   111   "intlen [] = 0"

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

   113 

   114 lemma inlen_bigger:

   115   shows "0 \<le> intlen xs"

   116 apply(induct xs)

   117 apply(auto)

   118 done 

   119 

   120 lemma intlen_append:

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

   122 apply(induct xs arbitrary: ys)

   123 apply(auto)

   124 done 

   125 

   126 lemma intlen_length:

   127   assumes "length xs < length ys"

   128   shows "intlen xs < intlen ys"

   129 using assms

   130 apply(induct xs arbitrary: ys)

   131 apply(auto)

   132 apply(case_tac ys)

   133 apply(simp_all)

   134 apply (smt inlen_bigger)

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

   136 

   137 

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

   139 where

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

   141 

   142 lemma pflat_len_simps:

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

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

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

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

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

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

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

   150 apply(auto simp add: pflat_len_def Pos_empty)

   151 done

   152 

   153 lemma pflat_len_Stars_simps:

   154   assumes "n < length vs"

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

   156 using assms 

   157 apply(induct vs arbitrary: n p)

   158 apply(simp)

   159 apply(simp)

   160 apply(simp add: pflat_len_def)

   161 apply(auto)[1]

   162 apply (metis at.simps(6))

   163 apply (metis Suc_less_eq Suc_pred)

   164 by (metis diff_Suc_1 less_Suc_eq_0_disj nth_Cons')

   165 

   166 

   167 lemma Two_to_Three_aux:

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

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

   170 using assms

   171 apply(simp add: pflat_len_def)

   172 apply(auto split: if_splits)

   173 apply (smt inlen_bigger)+

   174 done

   175 

   176 lemma Two_to_Three:

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

   178   shows "Pos v1 = Pos v2"

   179 using assms

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

   181 

   182 lemma Two_to_Three_orig:

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

   184   shows "Pos v1 = Pos v2"

   185 using assms

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

   187 

   188 lemma set_eq1:

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

   190   shows "A = B"

   191 using assms

   192 by (simp add: insert_ident)

   193 

   194 lemma set_eq2:

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

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

   197   shows "B = C"

   198 using assms

   199 using Un_Int_distrib sup_bot.left_neutral sup_commute by blast

   200 

   201 

   202 

   203 lemma Three_to_One:

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

   205   and "Pos v1 = Pos v2" 

   206   shows "v1 = v2"

   207 using assms

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

   209 apply(erule Prf.cases)

   210 apply(simp_all)

   211 apply(erule Prf.cases)

   212 apply(simp_all)

   213 apply(erule Prf.cases)

   214 apply(simp_all)

   215 apply(erule Prf.cases)

   216 apply(simp_all)

   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 apply(drule_tac x="r1a" in meta_spec)

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

   225 apply(simp)

   226 apply(drule_tac meta_mp)

   227 thm subset_antisym

   228 apply(rule subset_antisym)

   229 apply(auto)[3]

   230 apply(clarify)

   231 apply(simp add: insert_ident)

   232 using Pos_empty apply blast

   233 apply(erule Prf.cases)

   234 apply(simp_all)

   235 apply(erule Prf.cases)

   236 apply(simp_all)

   237 apply(clarify)

   238 apply(simp add: insert_ident)

   239 using Pos_empty apply blast

   240 apply(simp add: insert_ident)

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

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

   243 apply(simp)

   244 apply(drule_tac meta_mp)

   245 apply(rule subset_antisym)

   246 apply(auto)[3]

   247 apply(erule Prf.cases)

   248 apply(simp_all)

   249 apply(erule Prf.cases)

   250 apply(simp_all)

   251 apply(simp add: insert_ident)

   252 apply(clarify)

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

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

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

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

   257 apply(simp)

   258 apply(drule_tac meta_mp)

   259 apply(rule subset_antisym)

   260 apply(rule subsetI)

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

   262 prefer 2

   263 apply(auto)[1]

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

   265 prefer 2

   266 apply (metis (no_types, lifting) Un_iff)

   267 apply(simp)

   268 apply(rule subsetI)

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

   270 prefer 2

   271 apply(auto)[1]

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

   273 prefer 2

   274 apply (metis (no_types, lifting) Un_iff)

   275 apply(simp (no_asm_use))

   276 apply(simp)

   277 apply(drule_tac meta_mp)

   278 apply(rule subset_antisym)

   279 apply(rule subsetI)

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

   281 prefer 2

   282 apply(auto)[1]

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

   284 prefer 2

   285 apply (metis (no_types, lifting) Un_iff)

   286 apply(simp)

   287 apply(rule subsetI)

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

   289 prefer 2

   290 apply(auto)[1]

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

   292 prefer 2

   293 apply (metis (no_types, lifting) Un_iff)

   294 apply(simp (no_asm_use))

   295 apply(simp)

   296 apply(erule Prf.cases)

   297 apply(simp_all)

   298 apply(erule Prf.cases)

   299 apply(simp_all)

   300 apply(auto)[1]

   301 using Pos_empty apply fastforce

   302 apply(erule Prf.cases)

   303 apply(simp_all)

   304 apply(erule Prf.cases)

   305 apply(simp_all)

   306 apply(auto)[1]

   307 using Pos_empty apply fastforce

   308 apply(clarify)

   309 apply(simp add: insert_ident)

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

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

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

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

   314 apply(simp)

   315 apply(drule_tac meta_mp)

   316 apply(rule subset_antisym)

   317 apply(rule subsetI)

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

   319 prefer 2

   320 apply(auto)[1]

   321 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)}")

   322 prefer 2

   323 apply (metis (no_types, lifting) Un_iff)

   324 apply(simp)

   325 apply(rule subsetI)

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

   327 prefer 2

   328 apply(auto)[1]

   329 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)}")

   330 prefer 2

   331 apply (metis (no_types, lifting) Un_iff)

   332 apply(simp (no_asm_use))

   333 apply(simp)

   334 apply(drule_tac meta_mp)

   335 apply(rule subset_antisym)

   336 apply(rule subsetI)

   337 apply(case_tac vsa)

   338 apply(simp)

   339 apply (simp add: Pos_empty)

   340 apply(simp)

   341 apply(clarify)

   342 apply(erule disjE)

   343 apply (simp add: Pos_empty)

   344 apply(erule disjE)

   345 apply(clarify)

   346 apply(subgoal_tac 

   347   "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))}")

   348 prefer 2

   349 apply blast

   350 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)}")

   351 prefer 2

   352 apply (metis (no_types, lifting) Un_iff)

   353 apply(simp)

   354 apply(clarify)

   355 apply(subgoal_tac 

   356   "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))}")

   357 prefer 2

   358 apply blast

   359 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)}")

   360 prefer 2

   361 apply (metis (no_types, lifting) Un_iff)

   362 apply(simp)

   363 apply(rule subsetI)

   364 apply(case_tac vsb)

   365 apply(simp)

   366 apply (simp add: Pos_empty)

   367 apply(simp)

   368 apply(clarify)

   369 apply(erule disjE)

   370 apply (simp add: Pos_empty)

   371 apply(erule disjE)

   372 apply(clarify)

   373 apply(subgoal_tac 

   374   "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))}")

   375 prefer 2

   376 apply(simp)

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

   378 apply blast

   379 using list.inject apply blast

   380 apply(clarify)

   381 apply(subgoal_tac 

   382   "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))}")

   383 prefer 2

   384 apply(simp)

   385 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)}")

   386 prefer 2

   387 apply (metis (no_types, lifting) Un_iff)

   388 apply(simp (no_asm_use))

   389 apply(simp)

   390 done

   391 

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

   393 where

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

   395 

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

   397 where

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

   399 

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

   401 where

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

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

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

   405 

   406 lemma lex_irrfl:

   407   fixes ps1 ps2 :: "nat list"

   408   assumes "ps1 \<sqsubset>lex ps2"

   409   shows "ps1 \<noteq> ps2"

   410 using assms

   411 apply(induct rule: lex_lists.induct)

   412 apply(auto)

   413 done

   414 

   415 lemma lex_append:

   416   assumes "ps2 \<noteq> []"  

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

   418 using assms

   419 apply(induct ps)

   420 apply(auto intro: lex_lists.intros)

   421 apply(case_tac ps2)

   422 apply(simp)

   423 apply(simp)

   424 apply(auto intro: lex_lists.intros)

   425 done

   426 

   427 lemma lexordp_simps [simp]:

   428   fixes xs ys :: "nat list"

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

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

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

   432 apply -

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

   434 using lex_lists.cases apply blast

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

   436 

   437 lemma lex_append_cancel [simp]:

   438   fixes ps ps1 ps2 :: "nat list"

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

   440 apply(induct ps)

   441 apply(auto)

   442 done

   443 

   444 lemma lex_trans:

   445   fixes ps1 ps2 ps3 :: "nat list"

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

   447   shows "ps1 \<sqsubset>lex ps3"

   448 using assms

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

   450 apply(erule lex_lists.cases)

   451 apply(simp_all)

   452 apply(rotate_tac 2)

   453 apply(erule lex_lists.cases)

   454 apply(simp_all)

   455 apply(erule lex_lists.cases)

   456 apply(simp_all)

   457 done

   458 

   459 lemma trichotomous_aux:

   460   fixes p q :: "nat list"

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

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

   463 using assms

   464 apply(induct rule: lex_lists.induct)

   465 apply(auto)

   466 done

   467 

   468 lemma trichotomous_aux2:

   469   fixes p q :: "nat list"

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

   471   shows "False"

   472 using assms

   473 apply(induct rule: lex_lists.induct)

   474 apply(auto)

   475 done

   476 

   477 lemma trichotomous:

   478   fixes p q :: "nat list"

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

   480 apply(induct p arbitrary: q)

   481 apply(auto)

   482 apply(case_tac q)

   483 apply(auto)

   484 done

   485 

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

   487   where

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

   489 

   490 definition

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

   492 

   493 lemma outside_lemma:

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

   495   shows "pflat_len v1 p = pflat_len v2 p"

   496 using assms

   497 apply(auto simp add: pflat_len_def)

   498 done

   499 

   500 lemma dpos_lemma_aux:

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

   502   and "pflat_len v1 p = pflat_len v2 p"

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

   504 using assms

   505 apply(auto simp add: pflat_len_def)

   506 apply (smt inlen_bigger)

   507 apply (smt inlen_bigger)

   508 done

   509 

   510 lemma dpos_lemma:

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

   512   and "pflat_len v1 p = pflat_len v2 p"

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

   514 using assms

   515 apply(auto simp add: dpos_def dpos_lemma_aux)

   516 using dpos_lemma_aux apply auto[1]

   517 using dpos_lemma_aux apply auto[1]

   518 done

   519 

   520 lemma dpos_lemma2:

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

   522   and "dpos v1 v2 p"

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

   524 using assms

   525 using dpos_lemma by blast

   526 

   527 lemma DPos_lemma:

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

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

   530 using assms

   531 unfolding DPos_def 

   532 apply(auto simp add: pflat_len_def dpos_def)

   533 apply (smt inlen_bigger)

   534 by (smt inlen_bigger)

   535 

   536 

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

   538 where

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

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

   541 

   542 

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

   544 where

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

   546 

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

   548 where

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

   550 

   551 lemma val_ord_shorterI:

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

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

   554 using assms(1)

   555 apply(subst val_ord_ex_def)

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

   557 apply(subst val_ord_def)

   558 apply(rule conjI)

   559 apply (simp add: Pos_empty)

   560 apply(rule conjI)

   561 apply(simp add: pflat_len_simps)

   562 apply (simp add: intlen_length)

   563 apply(simp)

   564 done

   565 

   566 

   567 

   568 lemma val_ord_ALTI:

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

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

   571 using assms(1)

   572 apply(subst (asm) val_ord_def)

   573 apply(erule conjE)

   574 apply(subst val_ord_def)

   575 apply(rule conjI)

   576 apply(simp)

   577 apply(rule conjI)

   578 apply(simp add: pflat_len_simps)

   579 apply(rule ballI)

   580 apply(rule impI)

   581 apply(simp only: Pos.simps)

   582 apply(auto)[1]

   583 using assms(2)

   584 apply(simp add: pflat_len_simps)

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

   586 done

   587 

   588 lemma val_ord_ALTI2:

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

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

   591 using assms(1)

   592 apply(subst (asm) val_ord_def)

   593 apply(erule conjE)

   594 apply(subst val_ord_def)

   595 apply(rule conjI)

   596 apply(simp)

   597 apply(rule conjI)

   598 apply(simp add: pflat_len_simps)

   599 apply(rule ballI)

   600 apply(rule impI)

   601 apply(simp only: Pos.simps)

   602 apply(auto)[1]

   603 using assms(2)

   604 apply(simp add: pflat_len_simps)

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

   606 done

   607 

   608 lemma val_ord_STARI:

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

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

   611 using assms(1)

   612 apply(subst (asm) val_ord_def)

   613 apply(erule conjE)

   614 apply(subst val_ord_def)

   615 apply(rule conjI)

   616 apply(simp)

   617 apply(rule conjI)

   618 apply(subst pflat_len_Stars_simps)

   619 apply(simp)

   620 apply(subst pflat_len_Stars_simps)

   621 apply(simp)

   622 apply(simp)

   623 apply(rule ballI)

   624 apply(rule impI)

   625 apply(simp)

   626 apply(auto)

   627 using assms(2)

   628 apply(simp add: pflat_len_simps)

   629 apply(auto simp add: pflat_len_Stars_simps)

   630 done

   631 

   632 lemma val_ord_STARI2:

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

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

   635 using assms(1)

   636 apply(subst (asm) val_ord_def)

   637 apply(erule conjE)+

   638 apply(subst val_ord_def)

   639 apply(rule conjI)

   640 apply(simp)

   641 apply(rule conjI)

   642 apply(case_tac vs1)

   643 apply(simp)

   644 apply(simp)

   645 apply(auto)[1]

   646 apply(case_tac vs2)

   647 apply(simp)

   648 apply (simp add: pflat_len_def)

   649 apply(simp)

   650 apply(auto)[1]

   651 apply (simp add: pflat_len_Stars_simps)

   652 using pflat_len_def apply auto[1]

   653 apply(rule ballI)

   654 apply(rule impI)

   655 apply(simp)

   656 using assms(2)

   657 apply(auto)

   658 apply (simp add: pflat_len_simps(7))

   659 apply (simp add: pflat_len_Stars_simps)

   660 using assms(2)

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

   662 apply force

   663 apply force

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

   665 apply force

   666 apply force

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

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

   669 apply force

   670 apply force

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

   672 apply force

   673 apply force

   674 done

   675 

   676 

   677 lemma val_ord_SEQI:

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

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

   680 using assms(1)

   681 apply(subst (asm) val_ord_def)

   682 apply(erule conjE)

   683 apply(subst val_ord_def)

   684 apply(rule conjI)

   685 apply(simp)

   686 apply(rule conjI)

   687 apply(simp add: pflat_len_simps)

   688 apply(rule ballI)

   689 apply(rule impI)

   690 apply(simp only: Pos.simps)

   691 apply(auto)[1]

   692 apply(simp add: pflat_len_simps)

   693 using assms(2)

   694 apply(simp)

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

   696 done

   697 

   698 

   699 lemma val_ord_SEQI2:

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

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

   702 using assms(1)

   703 apply(subst (asm) val_ord_def)

   704 apply(erule conjE)+

   705 apply(subst val_ord_def)

   706 apply(rule conjI)

   707 apply(simp)

   708 apply(rule conjI)

   709 apply(simp add: pflat_len_simps)

   710 apply(rule ballI)

   711 apply(rule impI)

   712 apply(simp only: Pos.simps)

   713 apply(auto)

   714 apply(auto simp add: pflat_len_def intlen_append)

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

   716 done

   717 

   718 lemma val_ord_SEQE_0:

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

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

   721 using assms(1)

   722 apply(simp add: val_ord_def val_ord_ex_def)

   723 apply(auto)[1]

   724 apply(simp add: pflat_len_simps)

   725 apply(simp add: val_ord_def pflat_len_def)

   726 apply(auto)[1]

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

   728 apply(simp)

   729 apply(simp)

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

   731 apply(simp)

   732 apply(simp)

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

   734 apply(simp)

   735 apply(simp)

   736 apply(simp add: val_ord_def pflat_len_def)

   737 apply(auto)[1]

   738 done

   739 

   740 lemma val_ord_SEQE_1:

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

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

   743 using assms(1)

   744 apply(simp add: val_ord_def pflat_len_def)

   745 apply(auto)[1]

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

   747 apply(simp)

   748 apply(simp)

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

   750 apply(simp)

   751 apply(simp)

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

   753 apply(simp)

   754 apply(auto)[1]

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

   756 apply(simp)

   757 apply(auto)

   758 apply(simp add: intlen_append)

   759 apply force

   760 apply(simp add: intlen_append)

   761 apply force

   762 apply(simp add: intlen_append)

   763 apply force

   764 apply(simp add: intlen_append)

   765 apply force

   766 done

   767 

   768 lemma val_ord_SEQE_2:

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

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

   771   shows "v1 = v1'"

   772 proof -

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

   774   using assms(1) 

   775   apply(simp add: val_ord_def)

   776   apply(rule ballI)

   777   apply(clarify)

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

   779   apply(auto)[1]

   780   apply(simp add: pflat_len_simps)

   781   done

   782   then have "Pos v1 = Pos v1'"

   783   apply(rule_tac Two_to_Three_orig)

   784   apply(rule ballI)

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

   786   apply(simp)

   787   apply(simp)

   788   done

   789   then show "v1 = v1'" 

   790   apply(rule_tac Three_to_One)

   791   apply(rule assms)

   792   apply(rule assms)

   793   apply(simp)

   794   done

   795 qed

   796 

   797 lemma val_ord_SEQ:

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

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

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

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

   802 using assms(1)

   803 apply(subst (asm) val_ord_ex_def)

   804 apply(erule exE)

   805 apply(simp only: val_ord_def)

   806 apply(simp)

   807 apply(erule conjE)+

   808 apply(erule disjE)

   809 prefer 2

   810 apply(erule disjE)

   811 apply(erule exE)

   812 apply(rule disjI1)

   813 apply(simp)

   814 apply(subst val_ord_ex_def)

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

   816 apply(rule val_ord_SEQE_0)

   817 apply(simp add: val_ord_def)

   818 apply(erule exE)

   819 apply(rule disjI2)

   820 apply(rule conjI)

   821 thm val_ord_SEQE_1

   822 apply(rule_tac val_ord_SEQE_2)

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

   824 apply(rule assms(3))

   825 apply(rule assms(4))

   826 apply(subst val_ord_ex_def)

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

   828 apply(rule_tac val_ord_SEQE_1)

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

   830 apply(simp)

   831 using assms(2)

   832 apply(simp add: pflat_len_simps)

   833 done

   834 

   835 lemma val_ord_ex_trans:

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

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

   838 using assms

   839 unfolding val_ord_ex_def

   840 apply(clarify)

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

   842 prefer 2

   843 apply(rule trichotomous)

   844 apply(erule disjE)

   845 apply(simp)

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

   847 apply(subst val_ord_def)

   848 apply(rule conjI)

   849 apply(simp add: val_ord_def)

   850 apply(auto)[1]

   851 apply(simp add: val_ord_def)

   852 apply(simp add: val_ord_def)

   853 apply(auto)[1]

   854 using outside_lemma apply blast

   855 apply(simp add: val_ord_def)

   856 apply(auto)[1]

   857 using outside_lemma apply force

   858 apply auto[1]

   859 apply(simp add: val_ord_def)

   860 apply(auto)[1]

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

   862 apply(simp add: val_ord_def)

   863 apply(auto)[1]

   864 by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)

   865 

   866 

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

   868 where

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

   870 

   871 

   872 lemma pos_append:

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

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

   875 using assms

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

   877 apply(simp_all)

   878 apply(auto)[1]

   879 apply(simp add: append_eq_Cons_conv)

   880 apply(auto)[1]

   881 apply(auto)[1]

   882 apply(simp add: append_eq_Cons_conv)

   883 apply(auto)[1]

   884 apply(auto)[1]

   885 apply(simp add: append_eq_Cons_conv)

   886 apply(auto)[1]

   887 apply(simp add: append_eq_Cons_conv)

   888 apply(auto)[1]

   889 apply(auto)[1]

   890 apply(simp add: append_eq_Cons_conv)

   891 apply(auto)[1]

   892 apply(simp add: append_eq_Cons_conv)

   893 apply(auto)[1]

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

   895 

   896 

   897 lemma Pos_pre:

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

   899   shows "q \<in> Pos v"

   900 using assms

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

   902 apply(simp_all add: prefix_list_def)

   903 apply (meson append_eq_Cons_conv append_is_Nil_conv)

   904 apply (meson append_eq_Cons_conv append_is_Nil_conv)

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

   906 apply(auto)

   907 apply (meson append_eq_Cons_conv)

   908 apply(simp add: append_eq_Cons_conv)

   909 apply(auto)

   910 done

   911 

   912 lemma lex_lists_order:

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

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

   915 using assms

   916 apply(induct rule: lex_lists.induct)

   917 apply(simp add: prefix_list_def)

   918 apply(auto)

   919 using trichotomous_aux2 by auto

   920 

   921 lemma lex_appendL:

   922   assumes "q \<sqsubset>lex p" 

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

   924 using assms

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

   926 apply(auto)

   927 done

   928 

   929 

   930 inductive 

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

   932 where

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

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

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

   936 | "\<Turnstile> Void : ONE"

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

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

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

   940 

   941 lemma Prf_CPrf:

   942   assumes "\<Turnstile> v : r"

   943   shows "\<turnstile> v : r"

   944 using assms

   945 apply(induct)

   946 apply(auto intro: Prf.intros)

   947 done

   948 

   949 definition

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

   951 

   952 definition

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

   954 

   955 lemma CPT_CPTpre_subset:

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

   957 apply(auto simp add: CPT_def CPTpre_def)

   958 done

   959 

   960 

   961 lemma CPTpre_subsets:

   962   "CPTpre ZERO s = {}"

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

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

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

   966   "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)}"

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

   968     {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)}"

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

   970 apply(auto simp add: CPTpre_def)

   971 apply(erule CPrf.cases)

   972 apply(simp_all)

   973 apply(erule CPrf.cases)

   974 apply(simp_all)

   975 apply(erule CPrf.cases)

   976 apply(simp_all)

   977 apply(erule CPrf.cases)

   978 apply(simp_all)

   979 apply(erule CPrf.cases)

   980 apply(simp_all)

   981 apply(erule CPrf.cases)

   982 apply(simp_all)

   983 apply(erule CPrf.cases)

   984 apply(simp_all)

   985 apply(rule CPrf.intros)

   986 done

   987 

   988 

   989 lemma CPTpre_simps:

   990   shows "CPTpre ONE s = {Void}"

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

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

   993   and   "CPTpre (SEQ r1 r2) s = 

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

   995 apply -

   996 apply(rule subset_antisym)

   997 apply(rule CPTpre_subsets)

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

   999 apply(case_tac "c = d")

  1000 apply(simp)

  1001 apply(rule subset_antisym)

  1002 apply(rule CPTpre_subsets)

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

  1004 apply(simp)

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

  1006 apply(erule CPrf.cases)

  1007 apply(simp_all)

  1008 apply(rule subset_antisym)

  1009 apply(rule CPTpre_subsets)

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

  1011 apply(rule subset_antisym)

  1012 apply(rule CPTpre_subsets)

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

  1014 done

  1015 

  1016 lemma CPT_simps:

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

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

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

  1020   and   "CPT (SEQ r1 r2) s = 

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

  1022 apply -

  1023 apply(rule subset_antisym)

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

  1025 apply(erule CPrf.cases)

  1026 apply(simp_all)[7]

  1027 apply(erule CPrf.cases)

  1028 apply(simp_all)[7]

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

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

  1031 apply(erule CPrf.cases)

  1032 apply(simp_all)[7]

  1033 apply(erule CPrf.cases)

  1034 apply(simp_all)[7]

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

  1036 apply(erule CPrf.cases)

  1037 apply(simp_all)[7]

  1038 apply(clarify)

  1039 apply blast

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

  1041 apply(erule CPrf.cases)

  1042 apply(simp_all)[7]

  1043 done

  1044 

  1045 lemma CPTpre_SEQ:

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

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

  1048 using assms

  1049 apply(simp add: CPTpre_simps)

  1050 apply(auto simp add: CPTpre_def)

  1051 apply (simp add: prefix_list_def)

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

  1053 

  1054 lemma Cond_prefix:

  1055   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)"

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

  1057   shows "t1 \<sqsubseteq>pre s1"

  1058 using assms

  1059 apply(auto simp add: Sequ_def prefix_list_def append_eq_append_conv2)

  1060 done

  1061 

  1062 

  1063 

  1064 lemma CPTpre_test:

  1065   assumes "s \<in> r \<rightarrow> v"

  1066   shows "\<not>(\<exists>v' \<in> CPT r s. v :\<sqsubset>val v')"

  1067 using assms

  1068 apply(induct r arbitrary: s v rule: rexp.induct)

  1069 apply(erule Posix.cases)

  1070 apply(simp_all)

  1071 apply(erule Posix.cases)

  1072 apply(simp_all)

  1073 apply(simp add: CPT_simps)

  1074 apply(simp add: val_ord_def val_ord_ex_def)

  1075 apply(erule Posix.cases)

  1076 apply(simp_all)

  1077 apply(simp add: CPT_simps)

  1078 apply (simp add: val_ord_def val_ord_ex_def)

  1079 (* SEQ *)

  1080 apply(rule ballI)

  1081 apply(erule Posix.cases)

  1082 apply(simp_all)

  1083 apply(clarify)

  1084 apply(subst (asm) CPT_simps)

  1085 apply(simp)

  1086 apply(clarify)

  1087 thm val_ord_SEQ

  1088 apply(drule_tac ?r="r1" in val_ord_SEQ)

  1089 apply(simp)

  1090 apply (simp add: CPT_def Posix1(2))

  1091 apply (simp add: Posix1a)

  1092 apply (simp add: CPT_def Posix1a)

  1093 using Prf_CPrf apply auto[1]

  1094 apply(erule disjE)

  1095 apply(drule_tac x="s1" in meta_spec)

  1096 apply(drule_tac x="v1" in meta_spec)

  1097 apply(simp)

  1098 apply(drule_tac x="v1a" in bspec)

  1099 apply(subgoal_tac "s1 = s1a")

  1100 apply(simp)

  1101 apply(auto simp add: append_eq_append_conv2)[1]

  1102 apply (metis (mono_tags, lifting) CPT_def L_flat_Prf1 Prf_CPrf append_Nil append_Nil2 mem_Collect_eq)

  1103 apply(simp add: CPT_def)

  1104 apply(auto)[1]

  1105 oops

  1106 

  1107 

  1108 lemma test: 

  1109   assumes "finite A"

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

  1111 using assms

  1112 apply(induct A)

  1113 apply(simp)

  1114 apply(auto)

  1115 apply(case_tac x)

  1116 apply(simp_all)

  1117 done

  1118 

  1119 lemma CPTpre_STAR_finite:

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

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

  1122 apply(induct s rule: length_induct)

  1123 apply(case_tac xs)

  1124 apply(simp)

  1125 apply(simp add: CPTpre_subsets)

  1126 apply(rule finite_subset)

  1127 apply(rule CPTpre_subsets)

  1128 apply(simp)

  1129 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)

  1130 apply(auto)[1]

  1131 apply(rule finite_imageI)

  1132 apply(simp add: Collect_case_prod_Sigma)

  1133 apply(rule finite_SigmaI)

  1134 apply(rule assms)

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

  1136 apply(simp)

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