lexing: comparison thys/Positions.thy

equal deleted inserted replaced

-:8927b737936f
+:925232418a15
 | "Pos (Char c) = {[]}"
 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}"
 | "Pos (Stars []) = {[]}"
-| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {(Suc n)#ps | n ps. n#ps \<in> Pos (Stars vs)}"
+| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
 lemma Pos_empty:
 shows "[] \<in> Pos v"
-apply(induct v rule: Pos.induct)
+by (induct v rule: Pos.induct)(auto)
-apply(auto)
-done
 fun intlen :: "'a list \<Rightarrow> int"
 where
 "intlen [] = 0"
 | "intlen (x#xs) = 1 + intlen xs"
 lemma inlen_bigger:
 shows "0 \<le> intlen xs"
-apply(induct xs)
+by (induct xs)(auto)
-apply(auto)
-done
 lemma intlen_append:
 shows "intlen (xs @ ys) = intlen xs + intlen ys"
-apply(induct xs arbitrary: ys)
+by (induct xs arbitrary: ys) (auto)
-apply(auto)
-done
 lemma intlen_length:
 assumes "length xs < length ys"
 shows "intlen xs < intlen ys"
 using assms
 and   "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"
 and   "pflat_len (Left v) (0#p) = pflat_len v p"
 and   "pflat_len (Left v) (Suc 0#p) = -1"
 and   "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
 and   "pflat_len (Right v) (0#p) = -1"
+and   "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)"
+and   "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p"
 and   "pflat_len v [] = intlen (flat v)"
-apply(auto simp add: pflat_len_def Pos_empty)
+by (auto simp add: pflat_len_def Pos_empty)
-done
 lemma pflat_len_Stars_simps:
 assumes "n < length vs"
 shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
 using assms
 apply(induct vs arbitrary: n p)
-apply(simp)
+apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
-apply(simp)
-apply(simp add: pflat_len_def)
-apply(auto)[1]
-apply (metis at.simps(6))
-apply (metis Suc_less_eq Suc_pred)
-by (metis diff_Suc_1 less_Suc_eq_0_disj nth_Cons')
-lemma pflat_len_Stars_simps2:
-shows "pflat_len (Stars (v#vs)) (Suc n # p) = pflat_len (Stars vs) (n#p)"
-and   "pflat_len (Stars (v#vs)) (0 # p) = pflat_len v p"
-using assms
-apply(simp_all add: pflat_len_def)
 done
 lemma Two_to_Three_aux:
 assumes "p \<in> Pos v1 \<union> Pos v2" "pflat_len v1 p = pflat_len v2 p"
 shows "p \<in> Pos v1 \<inter> Pos v2"
 using assms
 apply(simp add: pflat_len_def)
 apply(auto split: if_splits)
 apply (smt inlen_bigger)+
 done
 lemma Two_to_Three_orig:
 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p"
 shows "Pos v1 = Pos v2"
 using assms
 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _")
 where
 "ps1 \<sqsubset>spre ps2 \<equiv> (ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2)"
-inductive lex_lists :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
+inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
 where
 "[] \<sqsubset>lex p#ps"
 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"
 lemma lex_irrfl:
 fixes ps1 ps2 :: "nat list"
 assumes "ps1 \<sqsubset>lex ps2"
 shows "ps1 \<noteq> ps2"
 using assms
-apply(induct rule: lex_lists.induct)
+apply(induct rule: lex_list.induct)
 apply(auto)
 done
-lemma lex_append:
+lemma lex_simps [simp]:
-assumes "ps2 \<noteq> []"
-shows "ps \<sqsubset>lex ps @ ps2"
-using assms
-apply(induct ps)
-apply(auto intro: lex_lists.intros)
-apply(case_tac ps2)
-apply(simp)
-apply(simp)
-apply(auto intro: lex_lists.intros)
-done
-lemma lexordp_simps [simp]:
 fixes xs ys :: "nat list"
-shows "[] \<sqsubset>lex ys = (ys \<noteq> [])"
+shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
-and   "xs \<sqsubset>lex [] = False"
+and   "xs \<sqsubset>lex [] \<longleftrightarrow> False"
 and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))"
 apply -
-apply (metis lex_append lex_lists.simps list.simps(3))
+apply (metis lex_irrfl lex_list.intros(1) list.exhaust)
-using lex_lists.cases apply blast
+using lex_list.cases apply blast
-using lex_lists.cases lex_lists.intros(2) lex_lists.intros(3) not_less_iff_gr_or_eq by fastforce
+using lex_list.cases lex_list.intros(2) lex_list.intros(3) not_less_iff_gr_or_eq by fastforce
-lemma lex_append_cancel [simp]:
-fixes ps ps1 ps2 :: "nat list"
-shows "ps @ ps1 \<sqsubset>lex ps @ ps2 \<longleftrightarrow> ps1 \<sqsubset>lex ps2"
-apply(induct ps)
-apply(auto)
-done
 lemma lex_trans:
 fixes ps1 ps2 ps3 :: "nat list"
 assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
 shows "ps1 \<sqsubset>lex ps3"
 using assms
-apply(induct arbitrary: ps3 rule: lex_lists.induct)
+apply(induct arbitrary: ps3 rule: lex_list.induct)
-apply(erule lex_lists.cases)
+apply(erule lex_list.cases)
 apply(simp_all)
 apply(rotate_tac 2)
-apply(erule lex_lists.cases)
+apply(erule lex_list.cases)
 apply(simp_all)
-apply(erule lex_lists.cases)
+apply(erule lex_list.cases)
 apply(simp_all)
 done
-lemma trichotomous_aux:
-fixes p q :: "nat list"
-assumes "p \<sqsubset>lex q" "p \<noteq> q"
-shows "\<not>(q \<sqsubset>lex p)"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(auto)
-done
-lemma trichotomous_aux2:
-fixes p q :: "nat list"
-assumes "p \<sqsubset>lex q" "q \<sqsubset>lex p"
-shows "False"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(auto)
-done
 lemma trichotomous:
 fixes p q :: "nat list"
 shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
 apply(induct p arbitrary: q)
 apply(auto)
 apply(case_tac q)
 apply(auto)
 done
-(*
-definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool"
-where
-"dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)"
-*)
 lemma outside_lemma:
 assumes "p \<notin> Pos v1 \<union> Pos v2"
 shows "pflat_len v1 p = pflat_len v2 p"
 using assms
 apply(auto simp add: pflat_len_def)
 done
-(*
-lemma dpos_lemma_aux:
-assumes "p \<in> Pos v1 \<union> Pos v2"
-and "pflat_len v1 p = pflat_len v2 p"
-shows "p \<in> Pos v1 \<inter> Pos v2"
-using assms
-apply(auto simp add: pflat_len_def)
-apply (smt inlen_bigger)
-apply (smt inlen_bigger)
-done
-lemma dpos_lemma:
-assumes "p \<in> Pos v1 \<union> Pos v2"
-and "pflat_len v1 p = pflat_len v2 p"
-shows "\<not>dpos v1 v2 p"
-using assms
-apply(auto simp add: dpos_def dpos_lemma_aux)
-using dpos_lemma_aux apply auto[1]
-using dpos_lemma_aux apply auto[1]
-done
-lemma dpos_lemma2:
-assumes "p \<in> Pos v1 \<union> Pos v2"
-and "dpos v1 v2 p"
-shows "pflat_len v1 p \<noteq> pflat_len v2 p"
-using assms
-using dpos_lemma by blast
-*)
 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")
 where
 "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> pflat_len v1 p > pflat_len v2 p \<and>
 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))"
 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
 lemma val_ord_shorterI:
 assumes "length (flat v') < length (flat v)"
 shows "v :\<sqsubset>val v'"
-using assms(1)
+using assms
-apply(subst val_ord_ex_def)
+unfolding val_ord_ex_def
-apply(rule_tac x="[]" in exI)
+by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) val_ord_def)
-apply(subst val_ord_def)
-apply(rule conjI)
+lemma val_ord_spreI:
-apply (simp add: Pos_empty)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply (simp add: intlen_length)
-apply(simp)
-done
-lemma val_ord_spre:
 assumes "(flat v') \<sqsubset>spre (flat v)"
 shows "v :\<sqsubset>val v'"
+using assms
+apply(rule_tac val_ord_shorterI)
+by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
+lemma val_ord_LeftI:
+assumes "v :\<sqsubset>val v'" "flat v = flat v'"
+shows "(Left v) :\<sqsubset>val (Left v')"
 using assms(1)
-apply(rule_tac val_ord_shorterI)
+unfolding val_ord_ex_def
-apply(simp add: sprefix_list_def prefix_list_def)
 apply(auto)
-apply(case_tac ps')
+apply(rule_tac x="0#p" in exI)
+using assms(2)
+apply(auto simp add: val_ord_def pflat_len_simps)
+done
+lemma val_ord_RightI:
+assumes "v :\<sqsubset>val v'" "flat v = flat v'"
+shows "(Right v) :\<sqsubset>val (Right v')"
+using assms(1)
+unfolding val_ord_ex_def
 apply(auto)
-by (metis append_eq_conv_conj drop_all le_less_linear neq_Nil_conv)
+apply(rule_tac x="Suc 0#p" in exI)
-lemma val_ord_ALTI:
-assumes "v \<sqsubset>val p v'" "flat v = flat v'"
-shows "(Left v) \<sqsubset>val (0#p) (Left v')"
-using assms(1)
-apply(subst (asm) val_ord_def)
-apply(erule conjE)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply(rule ballI)
-apply(rule impI)
-apply(simp only: Pos.simps)
-apply(auto)[1]
 using assms(2)
-apply(simp add: pflat_len_simps)
+apply(auto simp add: val_ord_def pflat_len_simps)
-apply(auto simp add: pflat_len_simps)[2]
+done
-done
-lemma val_ord_ALTI2:
-assumes "v \<sqsubset>val p v'" "flat v = flat v'"
-shows "(Right v) \<sqsubset>val (1#p) (Right v')"
-using assms(1)
-apply(subst (asm) val_ord_def)
-apply(erule conjE)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply(rule ballI)
-apply(rule impI)
-apply(simp only: Pos.simps)
-apply(auto)[1]
-using assms(2)
-apply(simp add: pflat_len_simps)
-apply(auto simp add: pflat_len_simps)[2]
-done
 lemma val_ord_ALTE:
 assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)"
 shows "p = 0 \<and> v1 \<sqsubset>val ps v2"
 using assms(1)
 apply(simp add: val_ord_def)
 apply(auto simp add: pflat_len_simps)
-apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
-by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
 lemma val_ord_ALTE2:
 assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)"
 shows "p = 1 \<and> v1 \<sqsubset>val ps v2"
 using assms(1)
 apply(simp add: val_ord_def)
 apply(auto simp add: pflat_len_simps)
-apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
-by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
 lemma val_ord_STARI:
 assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
 shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))"
 using assms(1)
 apply(rule ballI)
 apply(rule impI)
 apply(simp)
 using assms(2)
 apply(auto)
-apply (simp add: pflat_len_simps(7))
+apply (simp add: pflat_len_simps(9))
 apply (simp add: pflat_len_Stars_simps)
 using assms(2)
 apply(auto simp add: pflat_len_def)[1]
 apply force
 apply force
 apply(simp add: val_ord_def)
 apply(auto)[1]
 by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)
-lemma Pos_pre:
-assumes "p \<in> Pos v" "q \<sqsubseteq>pre p"
-shows "q \<in> Pos v"
-using assms
-apply(induct v arbitrary: p q rule: Pos.induct)
-apply(simp_all add: prefix_list_def)
-apply (meson append_eq_Cons_conv append_is_Nil_conv)
-apply (meson append_eq_Cons_conv append_is_Nil_conv)
-apply (metis (no_types, lifting) Cons_eq_append_conv append_is_Nil_conv)
-apply(auto)
-apply (meson append_eq_Cons_conv)
-apply(simp add: append_eq_Cons_conv)
-apply(auto)
-done
-lemma lex_lists_order:
-assumes "q' \<sqsubset>lex q" "\<not>(q' \<sqsubseteq>pre q)"
-shows "\<not>(q \<sqsubset>lex q')"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(simp add: prefix_list_def)
-apply(auto)
-using trichotomous_aux2 by auto
-lemma lex_appendL:
-assumes "q \<sqsubset>lex p"
-shows "q \<sqsubset>lex p @ q'"
-using assms
-apply(induct arbitrary: q' rule: lex_lists.induct)
-apply(auto)
-done
 inductive
 CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 where
 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
 apply(erule CPrf.cases)
 apply(simp_all)[7]
 done
-lemma CPTpre_SEQ:
-assumes "v \<in> CPTpre (SEQ r1 r2) s"
-shows "\<exists>s'. flat v = s' \<and> (s' \<sqsubseteq>pre s) \<and> s' \<in> L (SEQ r1 r2)"
-using assms
-apply(simp add: CPTpre_simps)
-apply(auto simp add: CPTpre_def)
-apply (simp add: prefix_list_def)
-by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5))
-term "{vs. Stars vs \<in> A}"
 lemma test:
 assumes "finite A"
 shows "finite {vs. Stars vs \<in> A}"
 using assms
 apply(induct A)
 apply(erule disjE)
 apply(subst (asm) val_ord_ex_def)
 apply(erule exE)
 apply(subst val_ord_ex1_def)
 apply(rule disjI1)
+apply(rule val_ord_LeftI)
 apply(subst val_ord_ex_def)
-apply(rule_tac x="0#p" in exI)
+apply(auto)[1]
-apply(rule val_ord_ALTI)
-apply(simp)
 using Posix1(2) apply blast
 using val_ord_ex1_def apply blast
 apply(subst val_ord_ex1_def)
 apply(rule disjI1)
 apply (simp add: Posix1(2) val_ord_shorterI)
 apply(drule_tac x="v2a" in meta_spec)
 apply(drule meta_mp)
 apply(auto simp add: CPTpre_def)[1]
 apply(subst (asm) val_ord_ex1_def)
 apply(erule disjE)
-apply(subst (asm) val_ord_ex_def)
-apply(erule exE)
 apply(subst val_ord_ex1_def)
 apply(rule disjI1)
-apply(subst val_ord_ex_def)
+apply(rule val_ord_RightI)
-apply(rule_tac x="1#p" in exI)
-apply(rule val_ord_ALTI2)
 apply(simp)
 using Posix1(2) apply blast
 apply (simp add: val_ord_ex1_def)
 apply(subst val_ord_ex1_def)
 apply(rule disjI1)
 apply (subst val_ord_ex1_def)
 apply(rule disjI1)
 apply (subst val_ord_ex_def)
 apply(case_tac p)
 apply(simp)
-apply (metis Posix1(2) flat_Stars not_less_iff_gr_or_eq pflat_len_simps(7) same_append_eq val_ord_def)
+apply (metis Posix1(2) append_eq_conv_conj flat_Stars not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_def)
 using Posix1(2) val_ord_STARI2 apply fastforce
 apply(simp add: val_ord_ex1_def)
 apply (subst (asm) val_ord_ex_def)
 apply(erule exE)
 apply (subst val_ord_ex1_def)
 apply(simp(no_asm)  add: val_ord_def)
 apply(rule conjI)
 apply(simp add: val_ord_def)
 apply(rule conjI)
 apply(simp add: val_ord_def)
-apply(auto simp add: pflat_len_simps pflat_len_Stars_simps2)[1]
+apply(auto simp add: pflat_len_simps)[1]
 apply(rule ballI)
 apply(rule impI)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 apply(clarify)
 apply(case_tac q)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 apply(clarify)
 apply(erule disjE)
 prefer 2
 apply(drule_tac x="Suc a # list" in bspec)
 apply(simp)
 apply(drule mp)
 apply(simp)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 apply(drule_tac x="Suc a # list" in bspec)
 apply(simp)
 apply(drule mp)
 apply(simp)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
 done
 lemma Posix_val_ord_reverse:
 assumes "s \<in> r \<rightarrow> v1"
 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)"
 using assms
 by (metis Posix_val_ord_stronger less_irrefl val_ord_def
 val_ord_ex1_def val_ord_ex_def val_ord_ex_trans)
-thm Posix.intros(6)
-inductive Prop :: "rexp \<Rightarrow> val list \<Rightarrow> bool"
-where
-"Prop r []"
-| "\<lbrakk>Prop r vs;
-\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = concat (map flat vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
-\<Longrightarrow> Prop r (v # vs)"
 lemma STAR_val_ord_ex:
 assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
 shows "Stars vs1 :\<sqsubset>val Stars vs2"
 using assms
 apply(simp)
 apply(case_tac a)
 apply(clarify)
 prefer 2
 using STAR_val_ord val_ord_ex_def apply blast
-apply(auto simp add: pflat_len_Stars_simps2 val_ord_def pflat_len_def)[1]
+apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1]
 done
 lemma STAR_val_ord_exI:
 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
 apply(erule STAR_val_ord_ex_append)
 apply(rule STAR_val_ord_exI)
 apply(auto)
 done
-lemma Posix_STARI:
-assumes "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> (flat v) \<in> r \<rightarrow> v" "Prop r vs"
-shows "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
-using assms
-apply(induct vs arbitrary: r)
-apply(simp)
-apply(rule Posix.intros)
-apply(simp)
-apply(rule Posix.intros)
-apply(simp)
-apply(auto)[1]
-apply(erule Prop.cases)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(erule Prop.cases)
-apply(simp)
-apply(auto)[1]
-done
 lemma CPrf_stars:
 assumes "\<Turnstile> Stars vs : STAR r"
 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
 using assms
 apply(simp)
 apply(drule mp)
 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
 apply(subst (asm) (2) val_ord_ex_def)
 apply(simp)
-apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def)
 apply(auto simp add: CPT_def PT_def)[1]
 using CPrf_stars apply auto[1]
 apply(auto)[1]
 apply(auto simp add: CPT_def PT_def)[1]
 apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r")
 apply(drule mp)
 apply (simp add: Posix1a Prf.intros(7))
 apply(simp)
 apply(subst (asm) (2) val_ord_ex_def)
 apply(simp)
-apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def)
 proof -
 fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list"
 assume a1: "s\<^sub>3 \<noteq> []"
 assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)"
 assume a3: "flat vA = flat a @ s\<^sub>3"
 apply(drule_tac x="Left v2" in spec)
 apply(simp)
 apply(drule mp)
 apply(rule Prf.intros)
 apply(simp)
-apply (meson val_ord_ALTI val_ord_ex_def)
+apply (meson val_ord_LeftI)
 apply(assumption)
 (* ALT Right *)
 apply(auto simp add: CPT_def)[1]
 apply(rule Posix.intros)
 apply(rotate_tac 1)
 apply(drule_tac x="Right v2a" in spec)
 apply(simp)
 apply(drule mp)
 apply(rule Prf.intros)
 apply(simp)
-apply(subst (asm) (2) val_ord_ex_def)
+apply(drule val_ord_RightI)
-apply(erule exE)
-apply(drule val_ord_ALTI2)
 apply(assumption)
 apply(auto simp add: val_ord_ex_def)[1]
 apply(assumption)
 apply(auto)[1]
 apply(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a")

changeset 251	925232418a15
parent 250	8927b737936f
child 252	022b80503766