thys/Positions.thy
changeset 268 6746f5e1f1f8
parent 267 32b222d77fa0
child 269 12772d537b71
equal deleted inserted replaced
267:32b222d77fa0 268:6746f5e1f1f8
     1    
     1    
     2 theory Positions
     2 theory Positions
     3   imports "Spec" 
     3   imports "Spec" "Lexer" 
     4 begin
     4 begin
     5 
     5 
     6 section {* Positions in Values *}
     6 section {* Positions in Values *}
     7 
     7 
     8 fun 
     8 fun 
    36 
    36 
    37 lemma Pos_empty:
    37 lemma Pos_empty:
    38   shows "[] \<in> Pos v"
    38   shows "[] \<in> Pos v"
    39 by (induct v rule: Pos.induct)(auto)
    39 by (induct v rule: Pos.induct)(auto)
    40 
    40 
    41 fun intlen :: "'a list \<Rightarrow> int"
    41 abbreviation
    42 where
    42   "intlen vs \<equiv> int (length vs)"
    43   "intlen [] = 0"
    43 
    44 | "intlen (x # xs) = 1 + intlen xs"
       
    45 
       
    46 lemma intlen_int:
       
    47   shows "intlen xs = int (length xs)"
       
    48 by (induct xs)(simp_all)
       
    49 
       
    50 lemma intlen_bigger:
       
    51   shows "0 \<le> intlen xs"
       
    52 by (induct xs)(auto)
       
    53 
       
    54 lemma intlen_append:
       
    55   shows "intlen (xs @ ys) = intlen xs + intlen ys"
       
    56 by (simp add: intlen_int)
       
    57 
       
    58 lemma intlen_length:
       
    59   shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
       
    60 by (simp add: intlen_int)
       
    61 
       
    62 lemma intlen_length_eq:
       
    63   shows "intlen xs = intlen ys \<longleftrightarrow> length xs = length ys"
       
    64 by (simp add: intlen_int)
       
    65 
    44 
    66 definition pflat_len :: "val \<Rightarrow> nat list => int"
    45 definition pflat_len :: "val \<Rightarrow> nat list => int"
    67 where
    46 where
    68   "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
    47   "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
    69 
    48 
   163 definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
   142 definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
   164 where
   143 where
   165   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
   144   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
   166 
   145 
   167 
   146 
       
   147 lemma PosOrd_trans:
       
   148   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
       
   149   shows "v1 :\<sqsubset>val v3"
       
   150 proof -
       
   151   from assms obtain p p'
       
   152     where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
       
   153   then have pos: "p \<in> Pos v1" "p' \<in> Pos v2" unfolding PosOrd_def pflat_len_def
       
   154     by (smt not_int_zless_negative)+
       
   155   have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
       
   156     by (rule lex_trichotomous)
       
   157   moreover
       
   158     { assume "p = p'"
       
   159       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
       
   160       by (smt Un_iff)
       
   161       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
       
   162     }   
       
   163   moreover
       
   164     { assume "p \<sqsubset>lex p'"
       
   165       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
       
   166       by (smt Un_iff lex_trans)
       
   167       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
       
   168     }
       
   169   moreover
       
   170     { assume "p' \<sqsubset>lex p"
       
   171       with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
       
   172       by (smt Un_iff lex_trans pflat_len_def)
       
   173       then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
       
   174     }
       
   175   ultimately show "v1 :\<sqsubset>val v3" by blast
       
   176 qed
       
   177 
       
   178 lemma PosOrd_irrefl:
       
   179   assumes "v :\<sqsubset>val v"
       
   180   shows "False"
       
   181 using assms unfolding PosOrd_ex_def PosOrd_def
       
   182 by auto
       
   183 
       
   184 lemma PosOrd_assym:
       
   185   assumes "v1 :\<sqsubset>val v2" 
       
   186   shows "\<not>(v2 :\<sqsubset>val v1)"
       
   187 using assms
       
   188 using PosOrd_irrefl PosOrd_trans by blast 
       
   189 
       
   190 text {*
       
   191   :\<sqsubseteq>val and :\<sqsubset>val are partial orders.
       
   192 *}
       
   193 
       
   194 lemma PosOrd_ordering:
       
   195   shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
       
   196 unfolding ordering_def PosOrd_ex_eq_def
       
   197 apply(auto)
       
   198 using PosOrd_irrefl apply blast
       
   199 using PosOrd_assym apply blast
       
   200 using PosOrd_trans by blast
       
   201 
       
   202 lemma PosOrd_order:
       
   203   shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"
       
   204 using PosOrd_ordering
       
   205 apply(simp add: class.order_def class.preorder_def class.order_axioms_def)
       
   206 unfolding ordering_def
       
   207 by blast
       
   208 
       
   209 
       
   210 lemma PosOrd_ex_eq2:
       
   211   shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)"
       
   212 using PosOrd_ordering 
       
   213 unfolding ordering_def
       
   214 by auto
       
   215 
       
   216 lemma PosOrdeq_trans:
       
   217   assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3"
       
   218   shows "v1 :\<sqsubseteq>val v3"
       
   219 using assms PosOrd_ordering 
       
   220 unfolding ordering_def
       
   221 by blast
       
   222 
       
   223 lemma PosOrdeq_antisym:
       
   224   assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1"
       
   225   shows "v1 = v2"
       
   226 using assms PosOrd_ordering 
       
   227 unfolding ordering_def
       
   228 by blast
       
   229 
       
   230 lemma PosOrdeq_refl:
       
   231   shows "v :\<sqsubseteq>val v" 
       
   232 unfolding PosOrd_ex_eq_def
       
   233 by auto
       
   234 
       
   235 
       
   236 
       
   237 
   168 lemma PosOrd_shorterE:
   238 lemma PosOrd_shorterE:
   169   assumes "v1 :\<sqsubset>val v2" 
   239   assumes "v1 :\<sqsubset>val v2" 
   170   shows "length (flat v2) \<le> length (flat v1)"
   240   shows "length (flat v2) \<le> length (flat v1)"
   171 using assms unfolding PosOrd_ex_def PosOrd_def
   241 using assms unfolding PosOrd_ex_def PosOrd_def
   172 apply(auto simp add: pflat_len_def intlen_int split: if_splits)
   242 apply(auto simp add: pflat_len_def split: if_splits)
   173 apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le)
   243 apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le)
   174 by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear)
   244 by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear)
   175 
   245 
   176 lemma PosOrd_shorterI:
   246 lemma PosOrd_shorterI:
   177   assumes "length (flat v2) < length (flat v1)"
   247   assumes "length (flat v2) < length (flat v1)"
   178   shows "v1 :\<sqsubset>val v2" 
   248   shows "v1 :\<sqsubset>val v2"
   179 using assms
   249 unfolding PosOrd_ex_def PosOrd_def pflat_len_def 
   180 unfolding PosOrd_ex_def
   250 using assms Pos_empty by force
   181 by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
       
   182 
   251 
   183 lemma PosOrd_spreI:
   252 lemma PosOrd_spreI:
   184   assumes "flat v' \<sqsubset>spre flat v"
   253   assumes "flat v' \<sqsubset>spre flat v"
   185   shows "v :\<sqsubset>val v'" 
   254   shows "v :\<sqsubset>val v'" 
   186 using assms
   255 using assms
   187 apply(rule_tac PosOrd_shorterI)
   256 apply(rule_tac PosOrd_shorterI)
   188 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
   257 unfolding prefix_list_def sprefix_list_def
       
   258 by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear)
   189 
   259 
   190 
   260 
   191 lemma PosOrd_Left_Right:
   261 lemma PosOrd_Left_Right:
   192   assumes "flat v1 = flat v2"
   262   assumes "flat v1 = flat v2"
   193   shows "Left v1 :\<sqsubset>val Right v2" 
   263   shows "Left v1 :\<sqsubset>val Right v2" 
   194 unfolding PosOrd_ex_def
   264 unfolding PosOrd_ex_def
   195 apply(rule_tac x="[0]" in exI)
   265 apply(rule_tac x="[0]" in exI)
   196 using assms 
   266 using assms 
   197 apply(auto simp add: PosOrd_def pflat_len_simps intlen_int)
   267 apply(auto simp add: PosOrd_def pflat_len_simps)
   198 done
   268 done
   199 
   269 
   200 lemma PosOrd_Left_eq:
   270 lemma PosOrd_Left_eq:
   201   assumes "flat v = flat v'"
   271   assumes "flat v = flat v'"
   202   shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" 
   272   shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" 
   217 done
   287 done
   218 
   288 
   219 
   289 
   220 lemma PosOrd_RightI:
   290 lemma PosOrd_RightI:
   221   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
   291   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
   222   shows "(Right v) :\<sqsubset>val (Right v')" 
   292   shows "Right v :\<sqsubset>val Right v'" 
   223 using assms(1)
   293 using assms(1)
   224 unfolding PosOrd_ex_def
   294 unfolding PosOrd_ex_def
   225 apply(auto)
   295 apply(auto)
   226 apply(rule_tac x="Suc 0#p" in exI)
   296 apply(rule_tac x="Suc 0#p" in exI)
   227 using assms(2)
   297 using assms(2)
   228 apply(auto simp add: PosOrd_def pflat_len_simps)
   298 apply(auto simp add: PosOrd_def pflat_len_simps)
   229 done
   299 done
   230 
   300 
   231 lemma PosOrd_RightE:
   301 lemma PosOrd_RightE:
   232   assumes "(Right v1) :\<sqsubset>val (Right v2)"
   302   assumes "Right v1 :\<sqsubset>val Right v2"
   233   shows "v1 :\<sqsubset>val v2"
   303   shows "v1 :\<sqsubset>val v2"
   234 using assms
   304 using assms
   235 apply(simp add: PosOrd_ex_def)
   305 apply(simp add: PosOrd_ex_def)
   236 apply(erule exE)
   306 apply(erule exE)
   237 apply(case_tac p)
   307 apply(case_tac p)
   256 done
   326 done
   257 
   327 
   258 
   328 
   259 lemma PosOrd_SeqI1:
   329 lemma PosOrd_SeqI1:
   260   assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
   330   assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
   261   shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
   331   shows "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" 
   262 using assms(1)
   332 using assms(1)
   263 apply(subst (asm) PosOrd_ex_def)
   333 apply(subst (asm) PosOrd_ex_def)
   264 apply(subst (asm) PosOrd_def)
   334 apply(subst (asm) PosOrd_def)
   265 apply(clarify)
   335 apply(clarify)
   266 apply(subst PosOrd_ex_def)
   336 apply(subst PosOrd_ex_def)
   273 apply(simp only: Pos.simps)
   343 apply(simp only: Pos.simps)
   274 apply(auto)[1]
   344 apply(auto)[1]
   275 apply(simp add: pflat_len_simps)
   345 apply(simp add: pflat_len_simps)
   276 using assms(2)
   346 using assms(2)
   277 apply(simp)
   347 apply(simp)
   278 apply(auto simp add: pflat_len_simps)[2]
   348 apply(auto simp add: pflat_len_simps)
   279 done
   349 by (metis length_append of_nat_add)
   280 
   350 
   281 lemma PosOrd_SeqI2:
   351 lemma PosOrd_SeqI2:
   282   assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
   352   assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
   283   shows "(Seq v v2) :\<sqsubset>val (Seq v v2')" 
   353   shows "Seq v v2 :\<sqsubset>val Seq v v2'" 
   284 using assms(1)
   354 using assms(1)
   285 apply(subst (asm) PosOrd_ex_def)
   355 apply(subst (asm) PosOrd_ex_def)
   286 apply(subst (asm) PosOrd_def)
   356 apply(subst (asm) PosOrd_def)
   287 apply(clarify)
   357 apply(clarify)
   288 apply(subst PosOrd_ex_def)
   358 apply(subst PosOrd_ex_def)
   299 apply(simp)
   369 apply(simp)
   300 apply(auto simp add: pflat_len_simps)
   370 apply(auto simp add: pflat_len_simps)
   301 done
   371 done
   302 
   372 
   303 lemma PosOrd_SeqE:
   373 lemma PosOrd_SeqE:
   304   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
   374   assumes "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" 
   305   shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'"
   375   shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'"
   306 using assms
   376 using assms
   307 apply(simp add: PosOrd_ex_def)
   377 apply(simp add: PosOrd_ex_def)
   308 apply(erule exE)
   378 apply(erule exE)
   309 apply(case_tac p)
   379 apply(case_tac p)
   310 apply(simp add: PosOrd_def)
   380 apply(simp add: PosOrd_def)
   311 apply(auto simp add: pflat_len_simps intlen_append)[1]
   381 apply(auto simp add: pflat_len_simps)[1]
   312 apply(rule_tac x="[]" in exI)
   382 apply(rule_tac x="[]" in exI)
   313 apply(drule_tac x="[]" in spec)
   383 apply(drule_tac x="[]" in spec)
   314 apply(simp add: Pos_empty pflat_len_simps)
   384 apply(simp add: Pos_empty pflat_len_simps)
   315 apply(case_tac a)
   385 apply(case_tac a)
   316 apply(rule disjI1)
   386 apply(rule disjI1)
   317 apply(simp add: PosOrd_def)
   387 apply(simp add: PosOrd_def)
   318 apply(auto simp add: pflat_len_simps intlen_append)[1]
   388 apply(auto simp add: pflat_len_simps)[1]
   319 apply(rule_tac x="list" in exI)
   389 apply(rule_tac x="list" in exI)
   320 apply(simp)
   390 apply(simp)
   321 apply(rule ballI)
   391 apply(rule ballI)
   322 apply(rule impI)
   392 apply(rule impI)
   323 apply(drule_tac x="0#q" in bspec)
   393 apply(drule_tac x="0#q" in bspec)
   324 apply(simp)
   394 apply(simp)
   325 apply(simp add: pflat_len_simps)
   395 apply(simp add: pflat_len_simps)
   326 apply(case_tac nat)
   396 apply(case_tac nat)
   327 apply(rule disjI2)
   397 apply(rule disjI2)
   328 apply(simp add: PosOrd_def)
   398 apply(simp add: PosOrd_def)
   329 apply(auto simp add: pflat_len_simps intlen_append)
   399 apply(auto simp add: pflat_len_simps)
   330 apply(rule_tac x="list" in exI)
   400 apply(rule_tac x="list" in exI)
   331 apply(simp add: Pos_empty)
   401 apply(simp add: Pos_empty)
   332 apply(rule ballI)
   402 apply(rule ballI)
   333 apply(rule impI)
   403 apply(rule impI)
   334 apply(auto)[1]
   404 apply(auto)[1]
   340 apply(simp add: pflat_len_simps)
   410 apply(simp add: pflat_len_simps)
   341 apply(simp add: PosOrd_def pflat_len_def)
   411 apply(simp add: PosOrd_def pflat_len_def)
   342 done
   412 done
   343 
   413 
   344 lemma PosOrd_StarsI:
   414 lemma PosOrd_StarsI:
   345   assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
   415   assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)"
   346   shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" 
   416   shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" 
   347 using assms(1)
   417 using assms(1)
   348 apply(subst (asm) PosOrd_ex_def)
   418 apply(subst (asm) PosOrd_ex_def)
   349 apply(subst (asm) PosOrd_def)
   419 apply(subst (asm) PosOrd_def)
   350 apply(clarify)
   420 apply(clarify)
   351 apply(subst PosOrd_ex_def)
   421 apply(subst PosOrd_ex_def)
   352 apply(subst PosOrd_def)
   422 apply(subst PosOrd_def)
   353 apply(rule_tac x="0#p" in exI)
   423 apply(rule_tac x="0#p" in exI)
   354 apply(simp add: pflat_len_Stars_simps pflat_len_simps)
   424 apply(simp add: pflat_len_Stars_simps pflat_len_simps)
   355 using assms(2)
   425 using assms(2)
   356 apply(simp add: pflat_len_simps intlen_append)
   426 apply(simp add: pflat_len_simps)
   357 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
   427 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
   358 done
   428 by (metis length_append of_nat_add)
   359 
   429 
   360 lemma PosOrd_StarsI2:
   430 lemma PosOrd_StarsI2:
   361   assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"
   431   assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flats vs1 = flats vs2"
   362   shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))" 
   432   shows "Stars (v#vs1) :\<sqsubset>val Stars (v#vs2)" 
   363 using assms(1)
   433 using assms(1)
   364 apply(subst (asm) PosOrd_ex_def)
   434 apply(subst (asm) PosOrd_ex_def)
   365 apply(subst (asm) PosOrd_def)
   435 apply(subst (asm) PosOrd_def)
   366 apply(clarify)
   436 apply(clarify)
   367 apply(subst PosOrd_ex_def)
   437 apply(subst PosOrd_ex_def)
   368 apply(subst PosOrd_def)
   438 apply(subst PosOrd_def)
   369 apply(case_tac p)
   439 apply(case_tac p)
   370 apply(simp add: pflat_len_simps)
   440 apply(simp add: pflat_len_simps)
   371 apply(rule_tac x="[]" in exI)
       
   372 apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append)
       
   373 apply(rule_tac x="Suc a#list" in exI)
   441 apply(rule_tac x="Suc a#list" in exI)
   374 apply(simp add: pflat_len_Stars_simps pflat_len_simps)
   442 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2))
   375 using assms(2)
       
   376 apply(simp add: pflat_len_simps intlen_append)
       
   377 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
       
   378 done
   443 done
   379 
   444 
   380 lemma PosOrd_Stars_appendI:
   445 lemma PosOrd_Stars_appendI:
   381   assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
   446   assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
   382   shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
   447   shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
   392 using assms
   457 using assms
   393 apply(subst (asm) PosOrd_ex_def)
   458 apply(subst (asm) PosOrd_ex_def)
   394 apply(erule exE)
   459 apply(erule exE)
   395 apply(case_tac p)
   460 apply(case_tac p)
   396 apply(simp)
   461 apply(simp)
   397 apply(simp add: PosOrd_def pflat_len_simps intlen_append)
   462 apply(simp add: PosOrd_def pflat_len_simps)
   398 apply(subst PosOrd_ex_def)
   463 apply(subst PosOrd_ex_def)
   399 apply(rule_tac x="[]" in exI)
   464 apply(rule_tac x="[]" in exI)
   400 apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
   465 apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
   401 apply(simp)
   466 apply(simp)
   402 apply(case_tac a)
   467 apply(case_tac a)
   403 apply(clarify)
   468 apply(clarify)
   404 apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
   469 apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
   405 apply(clarify)
   470 apply(clarify)
   406 apply(simp add: PosOrd_ex_def)
   471 apply(simp add: PosOrd_ex_def)
   407 apply(rule_tac x="nat#list" in exI)
   472 apply(rule_tac x="nat#list" in exI)
   408 apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
   473 apply(auto simp add: PosOrd_def pflat_len_simps)[1]
   409 apply(case_tac q)
   474 apply(case_tac q)
   410 apply(simp add: PosOrd_def pflat_len_simps intlen_append)
   475 apply(simp add: PosOrd_def pflat_len_simps)
   411 apply(clarify)
   476 apply(clarify)
   412 apply(drule_tac x="Suc a # lista" in bspec)
   477 apply(drule_tac x="Suc a # lista" in bspec)
   413 apply(simp)
   478 apply(simp)
   414 apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
   479 apply(auto simp add: PosOrd_def pflat_len_simps)[1]
   415 apply(case_tac q)
   480 apply(case_tac q)
   416 apply(simp add: PosOrd_def pflat_len_simps intlen_append)
   481 apply(simp add: PosOrd_def pflat_len_simps)
   417 apply(clarify)
   482 apply(clarify)
   418 apply(drule_tac x="Suc a # lista" in bspec)
   483 apply(drule_tac x="Suc a # lista" in bspec)
   419 apply(simp)
   484 apply(simp)
   420 apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
   485 apply(auto simp add: PosOrd_def pflat_len_simps)[1]
   421 done
   486 done
   422 
   487 
   423 lemma PosOrd_Stars_appendE:
   488 lemma PosOrd_Stars_appendE:
   424   assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
   489   assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
   425   shows "Stars vs1 :\<sqsubset>val Stars vs2"
   490   shows "Stars vs1 :\<sqsubset>val Stars vs2"
   436 apply(rule_tac iffI)
   501 apply(rule_tac iffI)
   437 apply(erule PosOrd_Stars_appendE)
   502 apply(erule PosOrd_Stars_appendE)
   438 apply(rule PosOrd_Stars_appendI)
   503 apply(rule PosOrd_Stars_appendI)
   439 apply(auto)
   504 apply(auto)
   440 done
   505 done
   441 
       
   442 lemma PosOrd_trans:
       
   443   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
       
   444   shows "v1 :\<sqsubset>val v3"
       
   445 proof -
       
   446   from assms obtain p p'
       
   447     where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
       
   448   have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
       
   449     by (rule lex_trichotomous)
       
   450   moreover
       
   451     { assume "p = p'"
       
   452       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
       
   453       by fastforce
       
   454       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
       
   455     }   
       
   456   moreover
       
   457     { assume "p \<sqsubset>lex p'"
       
   458       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
       
   459       by (smt Un_iff lex_trans)
       
   460       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
       
   461     }
       
   462   moreover
       
   463     { assume "p' \<sqsubset>lex p"
       
   464       with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
       
   465       by (smt Un_iff intlen_bigger lex_trans pflat_len_def)
       
   466       then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
       
   467     }
       
   468   ultimately show "v1 :\<sqsubset>val v3" by blast
       
   469 qed
       
   470 
       
   471 
       
   472 lemma PosOrd_irrefl:
       
   473   assumes "v :\<sqsubset>val v"
       
   474   shows "False"
       
   475 using assms unfolding PosOrd_ex_def PosOrd_def
       
   476 by auto
       
   477 
   506 
   478 lemma PosOrd_almost_trichotomous:
   507 lemma PosOrd_almost_trichotomous:
   479   shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
   508   shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
   480 apply(auto simp add: PosOrd_ex_def)
   509 apply(auto simp add: PosOrd_ex_def)
   481 apply(auto simp add: PosOrd_def)
   510 apply(auto simp add: PosOrd_def)
   483 apply(auto simp add: Pos_empty pflat_len_simps)
   512 apply(auto simp add: Pos_empty pflat_len_simps)
   484 apply(drule_tac x="[]" in spec)
   513 apply(drule_tac x="[]" in spec)
   485 apply(auto simp add: Pos_empty pflat_len_simps)
   514 apply(auto simp add: Pos_empty pflat_len_simps)
   486 done
   515 done
   487 
   516 
   488 lemma WW1:
       
   489   assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1"
       
   490   shows "False"
       
   491 using assms
       
   492 apply(auto simp add: PosOrd_ex_def PosOrd_def)
       
   493 using assms PosOrd_irrefl PosOrd_trans by blast
       
   494 
   517 
   495 lemma PosOrd_SeqE2:
   518 lemma PosOrd_SeqE2:
   496   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
   519   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
   497   shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')"
   520   shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')"
   498 using assms 
   521 using assms 
   510 apply(auto simp add: PosOrd_def pflat_len_simps)
   533 apply(auto simp add: PosOrd_def pflat_len_simps)
   511 apply(case_tac p)
   534 apply(case_tac p)
   512 apply(auto simp add: PosOrd_def pflat_len_simps)
   535 apply(auto simp add: PosOrd_def pflat_len_simps)
   513 apply(case_tac a)
   536 apply(case_tac a)
   514 apply(auto simp add: PosOrd_def pflat_len_simps)
   537 apply(auto simp add: PosOrd_def pflat_len_simps)
   515 apply (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
   538 apply (metis PosOrd_SeqI1 PosOrd_def PosOrd_ex_def PosOrd_shorterI PosOrd_assym assms less_linear)
   516 by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
   539 by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def PosOrd_assym assms of_nat_eq_iff)
   517 
   540 
   518 lemma PosOrd_SeqE4:
   541 lemma PosOrd_SeqE4:
   519   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
   542   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
   520   shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')"
   543   shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')"
   521 using assms 
   544 using assms 
   529 prefer 2
   552 prefer 2
   530 apply(simp)
   553 apply(simp)
   531 apply(auto)
   554 apply(auto)
   532 apply(case_tac "length (flat v1') < length (flat v1)")
   555 apply(case_tac "length (flat v1') < length (flat v1)")
   533 using PosOrd_shorterI apply blast
   556 using PosOrd_shorterI apply blast
   534 by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2))
   557 by (metis PosOrd_SeqI1 PosOrd_shorterI PosOrd_assym antisym_conv3 append_eq_append_conv assms(2))
   535 
   558 
   536 
   559 
   537 
   560 
   538 section {* The Posix Value is smaller than any other Value *}
   561 section {* The Posix Value is smaller than any other Value *}
   539 
   562 
   540 
   563 
   541 lemma Posix_PosOrd:
   564 lemma Posix_PosOrd:
   542   assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CV r s" 
   565   assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s" 
   543   shows "v1 :\<sqsubseteq>val v2"
   566   shows "v1 :\<sqsubseteq>val v2"
   544 using assms
   567 using assms
   545 proof (induct arbitrary: v2 rule: Posix.induct)
   568 proof (induct arbitrary: v2 rule: Posix.induct)
   546   case (Posix_ONE v)
   569   case (Posix_ONE v)
   547   have "v \<in> CV ONE []" by fact
   570   have "v \<in> LV ONE []" by fact
   548   then have "v = Void"
   571   then have "v = Void"
   549     by (simp add: CV_simps)
   572     by (simp add: LV_simps)
   550   then show "Void :\<sqsubseteq>val v"
   573   then show "Void :\<sqsubseteq>val v"
   551     by (simp add: PosOrd_ex_eq_def)
   574     by (simp add: PosOrd_ex_eq_def)
   552 next
   575 next
   553   case (Posix_CHAR c v)
   576   case (Posix_CHAR c v)
   554   have "v \<in> CV (CHAR c) [c]" by fact
   577   have "v \<in> LV (CHAR c) [c]" by fact
   555   then have "v = Char c"
   578   then have "v = Char c"
   556     by (simp add: CV_simps)
   579     by (simp add: LV_simps)
   557   then show "Char c :\<sqsubseteq>val v"
   580   then show "Char c :\<sqsubseteq>val v"
   558     by (simp add: PosOrd_ex_eq_def)
   581     by (simp add: PosOrd_ex_eq_def)
   559 next
   582 next
   560   case (Posix_ALT1 s r1 v r2 v2)
   583   case (Posix_ALT1 s r1 v r2 v2)
   561   have as1: "s \<in> r1 \<rightarrow> v" by fact
   584   have as1: "s \<in> r1 \<rightarrow> v" by fact
   562   have IH: "\<And>v2. v2 \<in> CV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
   585   have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
   563   have "v2 \<in> CV (ALT r1 r2) s" by fact
   586   have "v2 \<in> LV (ALT r1 r2) s" by fact
   564   then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
   587   then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
   565     by(auto simp add: CV_def prefix_list_def)
   588     by(auto simp add: LV_def prefix_list_def)
   566   then consider
   589   then consider
   567     (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
   590     (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
   568   | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
   591   | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
   569   by (auto elim: CPrf.cases)
   592   by (auto elim: Prf.cases)
   570   then show "Left v :\<sqsubseteq>val v2"
   593   then show "Left v :\<sqsubseteq>val v2"
   571   proof(cases)
   594   proof(cases)
   572      case (Left v3)
   595      case (Left v3)
   573      have "v3 \<in> CV r1 s" using Left(2,3) 
   596      have "v3 \<in> LV r1 s" using Left(2,3) 
   574        by (auto simp add: CV_def prefix_list_def)
   597        by (auto simp add: LV_def prefix_list_def)
   575      with IH have "v :\<sqsubseteq>val v3" by simp
   598      with IH have "v :\<sqsubseteq>val v3" by simp
   576      moreover
   599      moreover
   577      have "flat v3 = flat v" using as1 Left(3)
   600      have "flat v3 = flat v" using as1 Left(3)
   578        by (simp add: Posix1(2)) 
   601        by (simp add: Posix1(2)) 
   579      ultimately have "Left v :\<sqsubseteq>val Left v3"
   602      ultimately have "Left v :\<sqsubseteq>val Left v3"
   581      then show "Left v :\<sqsubseteq>val v2" unfolding Left .
   604      then show "Left v :\<sqsubseteq>val v2" unfolding Left .
   582   next
   605   next
   583      case (Right v3)
   606      case (Right v3)
   584      have "flat v3 = flat v" using as1 Right(3)
   607      have "flat v3 = flat v" using as1 Right(3)
   585        by (simp add: Posix1(2)) 
   608        by (simp add: Posix1(2)) 
   586      then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 
   609      then have "Left v :\<sqsubseteq>val Right v3" 
   587        by (auto simp add: PosOrd_ex_eq_def PosOrd_Left_Right)
   610        unfolding PosOrd_ex_eq_def
       
   611        by (simp add: PosOrd_Left_Right)
   588      then show "Left v :\<sqsubseteq>val v2" unfolding Right .
   612      then show "Left v :\<sqsubseteq>val v2" unfolding Right .
   589   qed
   613   qed
   590 next
   614 next
   591   case (Posix_ALT2 s r2 v r1 v2)
   615   case (Posix_ALT2 s r2 v r1 v2)
   592   have as1: "s \<in> r2 \<rightarrow> v" by fact
   616   have as1: "s \<in> r2 \<rightarrow> v" by fact
   593   have as2: "s \<notin> L r1" by fact
   617   have as2: "s \<notin> L r1" by fact
   594   have IH: "\<And>v2. v2 \<in> CV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
   618   have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
   595   have "v2 \<in> CV (ALT r1 r2) s" by fact
   619   have "v2 \<in> LV (ALT r1 r2) s" by fact
   596   then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
   620   then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
   597     by(auto simp add: CV_def prefix_list_def)
   621     by(auto simp add: LV_def prefix_list_def)
   598   then consider
   622   then consider
   599     (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
   623     (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
   600   | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
   624   | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
   601   by (auto elim: CPrf.cases)
   625   by (auto elim: Prf.cases)
   602   then show "Right v :\<sqsubseteq>val v2"
   626   then show "Right v :\<sqsubseteq>val v2"
   603   proof (cases)
   627   proof (cases)
   604     case (Right v3)
   628     case (Right v3)
   605      have "v3 \<in> CV r2 s" using Right(2,3) 
   629      have "v3 \<in> LV r2 s" using Right(2,3) 
   606        by (auto simp add: CV_def prefix_list_def)
   630        by (auto simp add: LV_def prefix_list_def)
   607      with IH have "v :\<sqsubseteq>val v3" by simp
   631      with IH have "v :\<sqsubseteq>val v3" by simp
   608      moreover
   632      moreover
   609      have "flat v3 = flat v" using as1 Right(3)
   633      have "flat v3 = flat v" using as1 Right(3)
   610        by (simp add: Posix1(2)) 
   634        by (simp add: Posix1(2)) 
   611      ultimately have "Right v :\<sqsubseteq>val Right v3" 
   635      ultimately have "Right v :\<sqsubseteq>val Right v3" 
   612         by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
   636         by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
   613      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
   637      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
   614   next
   638   next
   615      case (Left v3)
   639      case (Left v3)
   616      have "v3 \<in> CV r1 s" using Left(2,3) as2  
   640      have "v3 \<in> LV r1 s" using Left(2,3) as2  
   617        by (auto simp add: CV_def prefix_list_def)
   641        by (auto simp add: LV_def prefix_list_def)
   618      then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
   642      then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
   619        by (simp add: Posix1(2) CV_def) 
   643        by (simp add: Posix1(2) LV_def) 
   620      then have "False" using as1 as2 Left
   644      then have "False" using as1 as2 Left
   621        by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf)
   645        by (auto simp add: Posix1(2) L_flat_Prf1)
   622      then show "Right v :\<sqsubseteq>val v2" by simp
   646      then show "Right v :\<sqsubseteq>val v2" by simp
   623   qed
   647   qed
   624 next 
   648 next 
   625   case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
   649   case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
   626   have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
   650   have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
   627   then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
   651   then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
   628   have IH1: "\<And>v3. v3 \<in> CV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
   652   have IH1: "\<And>v3. v3 \<in> LV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
   629   have IH2: "\<And>v3. v3 \<in> CV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
   653   have IH2: "\<And>v3. v3 \<in> LV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
   630   have cond: "\<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)" by fact
   654   have cond: "\<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)" by fact
   631   have "v3 \<in> CV (SEQ r1 r2) (s1 @ s2)" by fact
   655   have "v3 \<in> LV (SEQ r1 r2) (s1 @ s2)" by fact
   632   then obtain v3a v3b where eqs:
   656   then obtain v3a v3b where eqs:
   633     "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
   657     "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
   634     "flat v3a @ flat v3b = s1 @ s2" 
   658     "flat v3a @ flat v3b = s1 @ s2" 
   635     by (force simp add: prefix_list_def CV_def elim: CPrf.cases)
   659     by (force simp add: prefix_list_def LV_def elim: Prf.cases)
   636   with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
   660   with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
   637     by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv)
   661     by (smt L_flat_Prf1 append_eq_append_conv2 append_self_conv)
   638   then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
   662   then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
   639     by (simp add: sprefix_list_def append_eq_conv_conj)
   663     by (simp add: sprefix_list_def append_eq_conv_conj)
   640   then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" 
   664   then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" 
   641     using PosOrd_spreI as1(1) eqs by blast
   665     using PosOrd_spreI as1(1) eqs by blast
   642   then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CV r1 s1 \<and> v3b \<in> CV r2 s2)" using eqs(2,3)
   666   then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3)
   643     by (auto simp add: CV_def)
   667     by (auto simp add: LV_def)
   644   then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
   668   then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
   645   then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
   669   then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
   646     unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
   670     unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
   647   then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
   671   then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
   648 next 
   672 next 
   649   case (Posix_STAR1 s1 r v s2 vs v3) 
   673   case (Posix_STAR1 s1 r v s2 vs v3) 
   650   have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
   674   have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
   651   then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
   675   then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
   652   have IH1: "\<And>v3. v3 \<in> CV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
   676   have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
   653   have IH2: "\<And>v3. v3 \<in> CV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
   677   have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
   654   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
   678   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
   655   have cond2: "flat v \<noteq> []" by fact
   679   have cond2: "flat v \<noteq> []" by fact
   656   have "v3 \<in> CV (STAR r) (s1 @ s2)" by fact
   680   have "v3 \<in> LV (STAR r) (s1 @ s2)" by fact
   657   then consider 
   681   then consider 
   658     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
   682     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
   659     "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
   683     "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
   660     "flat (Stars (v3a # vs3)) = s1 @ s2"
   684     "flat (Stars (v3a # vs3)) = s1 @ s2"
   661   | (Empty) "v3 = Stars []"
   685   | (Empty) "v3 = Stars []"
   662   unfolding CV_def
   686   unfolding LV_def  
   663   apply(auto)
   687   apply(auto)
   664   apply(erule CPrf.cases)
   688   apply(erule Prf.cases)
   665   apply(simp_all)
   689   apply(simp_all)
   666   apply(auto)[1]
   690   apply(auto)[1]
   667   apply(case_tac vs)
   691   apply(case_tac vs)
   668   apply(auto)
   692   apply(auto)
   669   using CPrf.intros(6) by blast
   693   using Prf.intros(6) by blast
   670   then show "Stars (v # vs) :\<sqsubseteq>val v3" (* HERE *)
   694   then show "Stars (v # vs) :\<sqsubseteq>val v3" 
   671     proof (cases)
   695     proof (cases)
   672       case (NonEmpty v3a vs3)
   696       case (NonEmpty v3a vs3)
   673       have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
   697       have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
   674       with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
   698       with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
   675         unfolding prefix_list_def
   699         unfolding prefix_list_def
   676         by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) 
   700         by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) 
   677       then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
   701       then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
   678         by (simp add: sprefix_list_def append_eq_conv_conj)
   702         by (simp add: sprefix_list_def append_eq_conv_conj)
   679       then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
   703       then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
   680         using PosOrd_spreI as1(1) NonEmpty(4) by blast
   704         using PosOrd_spreI as1(1) NonEmpty(4) by blast
   681       then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CV r s1 \<and> Stars vs3 \<in> CV (STAR r) s2)" 
   705       then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" 
   682         using NonEmpty(2,3) by (auto simp add: CV_def)
   706         using NonEmpty(2,3) by (auto simp add: LV_def)
   683       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
   707       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
   684       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
   708       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
   685          unfolding PosOrd_ex_eq_def by auto     
   709          unfolding PosOrd_ex_eq_def by auto     
   686       then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
   710       then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
   687         unfolding  PosOrd_ex_eq_def
   711         unfolding  PosOrd_ex_eq_def
   688         by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) val.inject(5))
   712         using PosOrd_StarsI PosOrd_StarsI2 by auto 
   689       then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
   713       then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
   690     next 
   714     next 
   691       case Empty
   715       case Empty
   692       have "v3 = Stars []" by fact
   716       have "v3 = Stars []" by fact
   693       then show "Stars (v # vs) :\<sqsubseteq>val v3"
   717       then show "Stars (v # vs) :\<sqsubseteq>val v3"
   694       unfolding PosOrd_ex_eq_def using cond2
   718       unfolding PosOrd_ex_eq_def using cond2
   695       by (simp add: PosOrd_shorterI)
   719       by (simp add: PosOrd_shorterI)
   696     qed      
   720     qed      
   697 next 
   721 next 
   698   case (Posix_STAR2 r v2)
   722   case (Posix_STAR2 r v2)
   699   have "v2 \<in> CV (STAR r) []" by fact
   723   have "v2 \<in> LV (STAR r) []" by fact
   700   then have "v2 = Stars []" 
   724   then have "v2 = Stars []" 
   701     unfolding CV_def by (auto elim: CPrf.cases) 
   725     unfolding LV_def by (auto elim: Prf.cases) 
   702   then show "Stars [] :\<sqsubseteq>val v2"
   726   then show "Stars [] :\<sqsubseteq>val v2"
   703   by (simp add: PosOrd_ex_eq_def)
   727   by (simp add: PosOrd_ex_eq_def)
   704 qed
   728 qed
   705 
   729 
   706 
   730 
   707 lemma Posix_PosOrd_reverse:
   731 lemma Posix_PosOrd_reverse:
   708   assumes "s \<in> r \<rightarrow> v1" 
   732   assumes "s \<in> r \<rightarrow> v1" 
   709   shows "\<not>(\<exists>v2 \<in> CV r s. v2 :\<sqsubset>val v1)"
   733   shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)"
   710 using assms
   734 using assms
   711 by (metis Posix_PosOrd less_irrefl PosOrd_def 
   735 by (metis Posix_PosOrd less_irrefl PosOrd_def 
   712     PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
   736     PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
   713 
   737 
   714 
   738 
   727   have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; 
   751   have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; 
   728              \<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
   752              \<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
   729              \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
   753              \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
   730   have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
   754   have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
   731   have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
   755   have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
   732   have "flat v \<in> r \<rightarrow> v" using as2 by simp
   756   have "flat v \<in> r \<rightarrow> v" "flat v \<noteq> []" using as2 by auto
   733   moreover
   757   moreover
   734   have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
   758   have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
   735     proof (rule IH)
   759     proof (rule IH)
   736       show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
   760       show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
   737     next 
   761     next 
   740         apply(subst (asm) (2) LV_def)
   764         apply(subst (asm) (2) LV_def)
   741         apply(auto)
   765         apply(auto)
   742         apply(erule Prf.cases)
   766         apply(erule Prf.cases)
   743         apply(simp_all)
   767         apply(simp_all)
   744         apply(drule_tac x="Stars (v # vs)" in bspec)
   768         apply(drule_tac x="Stars (v # vs)" in bspec)
   745         apply(simp add: LV_def CV_def)
   769         apply(simp add: LV_def)
   746         using Posix_Prf Prf.intros(6) calculation
   770         using Posix_LV Prf.intros(6) calculation
   747         apply(rule_tac Prf.intros)
   771         apply(rule_tac Prf.intros)
   748         apply(simp add:)
   772         apply(simp add:)
       
   773         prefer 2
   749         apply (simp add: PosOrd_StarsI2)
   774         apply (simp add: PosOrd_StarsI2)
       
   775         apply(drule Posix_LV) 
       
   776         apply(simp add: LV_def)
   750         done
   777         done
   751     qed
   778     qed
   752   moreover
   779   moreover
   753   have "flat v \<noteq> []" using as2 by simp
   780   have "flat v \<noteq> []" using as2 by simp
   754   moreover
   781   moreover
   776 
   803 
   777 
   804 
   778 
   805 
   779 section {* The Smallest Value is indeed the Posix Value *}
   806 section {* The Smallest Value is indeed the Posix Value *}
   780 
   807 
   781 text {*
       
   782   The next lemma seems to require LV instead of CV in the Star-case.
       
   783 *}
       
   784 
       
   785 lemma PosOrd_Posix:
   808 lemma PosOrd_Posix:
   786   assumes "v1 \<in> CV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
   809   assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
   787   shows "s \<in> r \<rightarrow> v1" 
   810   shows "s \<in> r \<rightarrow> v1" 
   788 using assms
   811 using assms
   789 proof(induct r arbitrary: s v1)
   812 proof(induct r arbitrary: s v1)
   790   case (ZERO s v1)
   813   case (ZERO s v1)
   791   have "v1 \<in> CV ZERO s" by fact
   814   have "v1 \<in> LV ZERO s" by fact
   792   then show "s \<in> ZERO \<rightarrow> v1" unfolding CV_def
   815   then show "s \<in> ZERO \<rightarrow> v1" unfolding LV_def
   793     by (auto elim: CPrf.cases)
   816     by (auto elim: Prf.cases)
   794 next 
   817 next 
   795   case (ONE s v1)
   818   case (ONE s v1)
   796   have "v1 \<in> CV ONE s" by fact
   819   have "v1 \<in> LV ONE s" by fact
   797   then show "s \<in> ONE \<rightarrow> v1" unfolding CV_def
   820   then show "s \<in> ONE \<rightarrow> v1" unfolding LV_def
   798     by(auto elim!: CPrf.cases intro: Posix.intros)
   821     by(auto elim!: Prf.cases intro: Posix.intros)
   799 next 
   822 next 
   800   case (CHAR c s v1)
   823   case (CHAR c s v1)
   801   have "v1 \<in> CV (CHAR c) s" by fact
   824   have "v1 \<in> LV (CHAR c) s" by fact
   802   then show "s \<in> CHAR c \<rightarrow> v1" unfolding CV_def
   825   then show "s \<in> CHAR c \<rightarrow> v1" unfolding LV_def
   803     by (auto elim!: CPrf.cases intro: Posix.intros)
   826     by (auto elim!: Prf.cases intro: Posix.intros)
   804 next
   827 next
   805   case (ALT r1 r2 s v1)
   828   case (ALT r1 r2 s v1)
   806   have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
   829   have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
   807   have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
   830   have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
   808   have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
   831   have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
   809   have as2: "v1 \<in> CV (ALT r1 r2) s" by fact
   832   have as2: "v1 \<in> LV (ALT r1 r2) s" by fact
   810   then consider 
   833   then consider 
   811      (Left) v1' where
   834      (Left) v1' where
   812         "v1 = Left v1'" "s = flat v1'"
   835         "v1 = Left v1'" "s = flat v1'"
   813         "v1' \<in> CV r1 s"
   836         "v1' \<in> LV r1 s"
   814   |  (Right) v1' where
   837   |  (Right) v1' where
   815         "v1 = Right v1'" "s = flat v1'"
   838         "v1 = Right v1'" "s = flat v1'"
   816         "v1' \<in> CV r2 s"
   839         "v1' \<in> LV r2 s"
   817   unfolding CV_def by (auto elim: CPrf.cases)
   840   unfolding LV_def by (auto elim: Prf.cases)
   818   then show "s \<in> ALT r1 r2 \<rightarrow> v1"
   841   then show "s \<in> ALT r1 r2 \<rightarrow> v1"
   819    proof (cases)
   842    proof (cases)
   820      case (Left v1')
   843      case (Left v1')
   821      have "v1' \<in> CV r1 s" using as2
   844      have "v1' \<in> LV r1 s" using as2
   822        unfolding CV_def Left by (auto elim: CPrf.cases)
   845        unfolding LV_def Left by (auto elim: Prf.cases)
   823      moreover
   846      moreover
   824      have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
   847      have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
   825        unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force  
   848        unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force  
   826      ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
   849      ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
   827      then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
   850      then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
   828      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
   851      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
   829    next
   852    next
   830      case (Right v1')
   853      case (Right v1')
   831      have "v1' \<in> CV r2 s" using as2
   854      have "v1' \<in> LV r2 s" using as2
   832        unfolding CV_def Right by (auto elim: CPrf.cases)
   855        unfolding LV_def Right by (auto elim: Prf.cases)
   833      moreover
   856      moreover
   834      have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
   857      have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
   835        unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force   
   858        unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force   
   836      ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
   859      ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
   837      moreover 
   860      moreover 
   839          then obtain v' where "v' \<in>  LV r1 s"
   862          then obtain v' where "v' \<in>  LV r1 s"
   840             unfolding LV_def using L_flat_Prf2 by blast
   863             unfolding LV_def using L_flat_Prf2 by blast
   841          then have "Left v' \<in>  LV (ALT r1 r2) s" 
   864          then have "Left v' \<in>  LV (ALT r1 r2) s" 
   842             unfolding LV_def by (auto intro: Prf.intros)
   865             unfolding LV_def by (auto intro: Prf.intros)
   843          with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" 
   866          with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" 
   844             unfolding LV_def Right by (auto)
   867             unfolding LV_def Right 
       
   868             by (auto)
   845          then have False using PosOrd_Left_Right Right by blast  
   869          then have False using PosOrd_Left_Right Right by blast  
   846        }
   870        }
   847      then have "s \<notin> L r1" by rule 
   871      then have "s \<notin> L r1" by rule 
   848      ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros)
   872      ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros)
   849      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp
   873      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp
   850   qed
   874   qed
   851 next 
   875 next 
   852   case (SEQ r1 r2 s v1)
   876   case (SEQ r1 r2 s v1)
   853   have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
   877   have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
   854   have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
   878   have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
   855   have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
   879   have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
   856   have as2: "v1 \<in> CV (SEQ r1 r2) s" by fact
   880   have as2: "v1 \<in> LV (SEQ r1 r2) s" by fact
   857   then obtain 
   881   then obtain 
   858     v1a v1b where eqs:
   882     v1a v1b where eqs:
   859         "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
   883         "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
   860         "v1a \<in> CV r1 (flat v1a)" "v1b \<in> CV r2 (flat v1b)" 
   884         "v1a \<in> LV r1 (flat v1a)" "v1b \<in> LV r2 (flat v1b)" 
   861   unfolding CV_def by(auto elim: CPrf.cases)
   885   unfolding LV_def by(auto elim: Prf.cases)
   862   have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
   886   have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
   863     proof
   887     proof
   864       fix v2
   888       fix v2
   865       assume "v2 \<in> LV r1 (flat v1a)"
   889       assume "v2 \<in> LV r1 (flat v1a)"
   866       with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s"
   890       with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s"
   867          by (simp add: CV_def LV_def Prf.intros(1) Prf_CPrf)
   891          by (simp add: LV_def Prf.intros(1))
   868       with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" 
   892       with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" 
   869          using eqs by (simp add: LV_def) 
   893          using eqs by (simp add: LV_def) 
   870       then show "\<not> v2 :\<sqsubset>val v1a"
   894       then show "\<not> v2 :\<sqsubset>val v1a"
   871          using PosOrd_SeqI1 by blast
   895          using PosOrd_SeqI1 by blast
   872     qed     
   896     qed     
   875   have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
   899   have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
   876     proof 
   900     proof 
   877       fix v2
   901       fix v2
   878       assume "v2 \<in> LV r2 (flat v1b)"
   902       assume "v2 \<in> LV r2 (flat v1b)"
   879       with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s"
   903       with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s"
   880          by (simp add: CV_def LV_def Prf.intros Prf_CPrf)
   904          by (simp add: LV_def Prf.intros)
   881       with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" 
   905       with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" 
   882          using eqs by (simp add: LV_def) 
   906          using eqs by (simp add: LV_def) 
   883       then show "\<not> v2 :\<sqsubset>val v1b"
   907       then show "\<not> v2 :\<sqsubset>val v1b"
   884          using PosOrd_SeqI2 by auto
   908          using PosOrd_SeqI2 by auto
   885     qed     
   909     qed     
   887   moreover
   911   moreover
   888   have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" 
   912   have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" 
   889   proof
   913   proof
   890      assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2"
   914      assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2"
   891      then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast
   915      then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast
   892      then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<turnstile> vA : r1" "flat vB = s4" "\<turnstile> vB : r2"
   916      then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<Turnstile> vA : r1" "flat vB = s4" "\<Turnstile> vB : r2"
   893         using L_flat_Prf2 by blast
   917         using L_flat_Prf2 by blast
   894      then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1
   918      then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1
   895        by (auto simp add: LV_def intro: Prf.intros)
   919        by (auto simp add: LV_def intro!: Prf.intros)
   896      with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto
   920      with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto
   897      then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto 
   921      then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto 
   898      then show "False"
   922      then show "False"
   899        using PosOrd_shorterI by blast  
   923        using PosOrd_shorterI by blast  
   900   qed
   924   qed
   901   ultimately
   925   ultimately
   902   show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs
   926   show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs
   903     by (rule Posix.intros)
   927     by (rule Posix.intros)
   904 next
   928 next
   905    case (STAR r s v1)
   929    case (STAR r s v1)
   906    have IH: "\<And>s v1. \<lbrakk>v1 \<in> CV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
   930    have IH: "\<And>s v1. \<lbrakk>v1 \<in> LV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
   907    have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
   931    have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
   908    have as2: "v1 \<in> CV (STAR r) s" by fact
   932    have as2: "v1 \<in> LV (STAR r) s" by fact
   909    then obtain 
   933    then obtain 
   910     vs where eqs:
   934     vs where eqs:
   911         "v1 = Stars vs" "s = flat (Stars vs)"
   935         "v1 = Stars vs" "s = flat (Stars vs)"
   912         "\<forall>v \<in> set vs. v \<in> CV r (flat v)"
   936         "\<forall>v \<in> set vs. v \<in> LV r (flat v)"
   913         unfolding CV_def by (auto elim: CPrf.cases)
   937         unfolding LV_def by (auto elim: Prf.cases)
   914    have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" 
   938    have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" 
   915      proof 
   939      proof 
   916         fix v
   940         fix v
   917         assume a: "v \<in> set vs"
   941         assume a: "v \<in> set vs"
   918         then obtain pre post where e: "vs = pre @ [v] @ post"
   942         then obtain pre post where e: "vs = pre @ [v] @ post"
   924              fix v2
   948              fix v2
   925              assume w: "v2 :\<sqsubset>val v"
   949              assume w: "v2 :\<sqsubset>val v"
   926              assume "v2 \<in> LV r (flat v)"
   950              assume "v2 \<in> LV r (flat v)"
   927              then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" 
   951              then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" 
   928                  using as2 unfolding e eqs
   952                  using as2 unfolding e eqs
   929                  apply(auto simp add: CV_def LV_def intro!: Prf.intros)[1]
   953                  apply(auto simp add: LV_def intro!: Prf.intros elim: Prf_elims dest: Prf_Stars_appendE)
   930                  using CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros apply blast
   954                  apply(auto dest!: Prf_Stars_appendE elim: Prf.cases)
   931                  by (metis CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros(2) val.inject(5))
   955                  done
   932              then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
   956              then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
   933                 using q by simp     
   957                 using q by simp     
   934              with w show "False"
   958              with w show "False"
   935                 using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
   959                 using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
   936                 PosOrd_StarsI PosOrd_Stars_appendI by auto
   960                 PosOrd_StarsI PosOrd_Stars_appendI by auto
   937           qed     
   961           qed     
   938         with IH
   962         with IH
   939         show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs CV_def
   963         show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs LV_def
   940         by (auto elim: CPrf.cases)
   964         by (auto elim: Prf.cases)
   941      qed
   965      qed
   942    moreover
   966    moreover
   943    have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
   967    have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
   944      proof 
   968      proof 
   945        assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
   969        assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
   946        then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
   970        then obtain vs2 where "\<Turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
   947                              "Stars vs2 :\<sqsubset>val Stars vs" 
   971                              "Stars vs2 :\<sqsubset>val Stars vs" 
   948          unfolding LV_def
   972          unfolding LV_def by (force elim: Prf_elims intro: Prf.intros)
   949          apply(auto)
       
   950          apply(erule Prf.cases)
       
   951          apply(auto intro: Prf.intros)
       
   952          done
       
   953        then show "False" using as1 unfolding eqs
   973        then show "False" using as1 unfolding eqs
   954          apply -
   974          by (auto simp add: LV_def)
   955          apply(drule_tac x="Stars vs2" in bspec)
       
   956          apply(auto simp add: LV_def)
       
   957          done
       
   958      qed
   975      qed
   959    ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
   976    ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
   960      thm PosOrd_Posix_Stars
   977      thm PosOrd_Posix_Stars
   961      by (rule PosOrd_Posix_Stars)
   978      by (rule PosOrd_Posix_Stars)
   962    then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
   979    then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
   963 qed
   980 qed
   964 
   981 
       
   982 lemma Least_existence:
       
   983   assumes "LV r s \<noteq> {}"
       
   984   shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
       
   985 proof -
       
   986   from assms
       
   987   obtain vposix where "s \<in> r \<rightarrow> vposix"
       
   988   unfolding LV_def 
       
   989   using L_flat_Prf1 lexer_correct_Some by blast
       
   990   then have "\<forall>v \<in> LV r s. vposix :\<sqsubseteq>val v"
       
   991     by (simp add: Posix_PosOrd)
       
   992   then show "\<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
       
   993     using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast
       
   994 qed 
       
   995 
       
   996 lemma Least_existence1:
       
   997   assumes "LV r s \<noteq> {}"
       
   998   shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v"
       
   999 using Least_existence[OF assms] assms
       
  1000 apply -
       
  1001 apply(erule bexE)
       
  1002 apply(rule_tac a="vmin" in ex1I)
       
  1003 apply(auto)[1]
       
  1004 apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2))
       
  1005 apply(auto)[1]
       
  1006 apply(simp add: PosOrdeq_antisym)
       
  1007 done
       
  1008 
       
  1009 lemma
       
  1010   shows "partial_order_on UNIV {(v1, v2). v1 :\<sqsubseteq>val v2}"
       
  1011 apply(simp add: partial_order_on_def)
       
  1012 apply(simp add: preorder_on_def refl_on_def)
       
  1013 apply(simp add: PosOrdeq_refl)
       
  1014 apply(auto)
       
  1015 apply(rule transI)
       
  1016 apply(auto intro: PosOrdeq_trans)[1]
       
  1017 apply(rule antisymI)
       
  1018 apply(simp add: PosOrdeq_antisym)
       
  1019 done
       
  1020 
       
  1021 lemma
       
  1022  "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}"
       
  1023 apply(rule finite_acyclic_wf)
       
  1024 prefer 2
       
  1025 apply(simp add: acyclic_def)
       
  1026 apply(induct_tac rule: trancl.induct)
       
  1027 apply(auto)[1]
       
  1028 oops
       
  1029 
       
  1030 
   965 unused_thms
  1031 unused_thms
   966 
  1032 
   967 end
  1033 end