lexing: comparison thys/Positions.thy

equal deleted inserted replaced

-:fff2e1b40dfc
+:32b222d77fa0
 lemma Pos_stars:
 "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
 apply(induct vs)
-apply(simp)
+apply(auto simp add: insert_ident less_Suc_eq_0_disj)
-apply(simp add: insert_ident)
+done
-apply(rule subset_antisym)
-using less_Suc_eq_0_disj by auto
 lemma Pos_empty:
 shows "[] \<in> Pos v"
 by (induct v rule: Pos.induct)(auto)
 fun intlen :: "'a list \<Rightarrow> int"
 where
 "intlen [] = 0"
 | "intlen (x # xs) = 1 + intlen xs"
+lemma intlen_int:
+shows "intlen xs = int (length xs)"
+by (induct xs)(simp_all)
 lemma intlen_bigger:
 shows "0 \<le> intlen xs"
 by (induct xs)(auto)
 lemma intlen_append:
 shows "intlen (xs @ ys) = intlen xs + intlen ys"
-by (induct xs arbitrary: ys) (auto)
+by (simp add: intlen_int)
 lemma intlen_length:
 shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
-apply(induct xs arbitrary: ys)
+by (simp add: intlen_int)
-apply (auto simp add: intlen_bigger not_less)
-apply (metis intlen.elims intlen_bigger le_imp_0_less)
-apply (smt Suc_lessI intlen.simps(2) length_Suc_conv nat_neq_iff)
-by (smt Suc_lessE intlen.simps(2) length_Suc_conv)
 lemma intlen_length_eq:
 shows "intlen xs = intlen ys \<longleftrightarrow> length xs = length ys"
-apply(induct xs arbitrary: ys)
+by (simp add: intlen_int)
-apply (auto simp add: intlen_bigger not_less)
-apply(case_tac ys)
-apply(simp_all)
-apply (smt intlen_bigger)
-apply (smt intlen.elims intlen_bigger length_Suc_conv)
-by (metis intlen.simps(2) length_Suc_conv)
 definition pflat_len :: "val \<Rightarrow> nat list => int"
 where
 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
 by (auto simp add: pflat_len_def Pos_empty)
 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(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
 done
 lemma pflat_len_outside:
 assumes "p \<notin> Pos v1"
 shows "pflat_len v1 p = -1 "
-using assms by (auto simp add: pflat_len_def)
+using assms by (simp add: pflat_len_def)
 section {* Orderings *}
 lemma PosOrd_shorterE:
 assumes "v1 :\<sqsubset>val v2"
 shows "length (flat v2) \<le> length (flat v1)"
-using assms
+using assms unfolding PosOrd_ex_def PosOrd_def
-apply(auto simp add: pflat_len_simps PosOrd_ex_def PosOrd_def)
+apply(auto simp add: pflat_len_def intlen_int split: if_splits)
-apply(case_tac p)
+apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le)
-apply(simp add: pflat_len_simps intlen_length)
+by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear)
-apply(simp)
-apply(drule_tac x="[]" in bspec)
-apply(simp add: Pos_empty)
-apply(simp add: pflat_len_simps le_less intlen_length_eq)
-done
 lemma PosOrd_shorterI:
 assumes "length (flat v2) < length (flat v1)"
 shows "v1 :\<sqsubset>val v2"
 using assms
 assumes "flat v1 = flat v2"
 shows "Left v1 :\<sqsubset>val Right v2"
 unfolding PosOrd_ex_def
 apply(rule_tac x="[0]" in exI)
 using assms
-apply(auto simp add: PosOrd_def pflat_len_simps)
+apply(auto simp add: PosOrd_def pflat_len_simps intlen_int)
-apply(smt intlen_bigger)
 done
 lemma PosOrd_Left_eq:
 assumes "flat v = flat v'"
 shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'"
 apply(case_tac "length (flat v1') < length (flat v1)")
 using PosOrd_shorterI apply blast
 by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2))
 section {* The Posix Value is smaller than any other Value *}
 lemma Posix_PosOrd:
-assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s"
+assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CV r s"
 shows "v1 :\<sqsubseteq>val v2"
 using assms
 proof (induct arbitrary: v2 rule: Posix.induct)
 case (Posix_ONE v)
-have "v \<in> CPT ONE []" by fact
+have "v \<in> CV ONE []" by fact
 then have "v = Void"
-by (simp add: CPT_simps)
+by (simp add: CV_simps)
 then show "Void :\<sqsubseteq>val v"
 by (simp add: PosOrd_ex_eq_def)
 next
 case (Posix_CHAR c v)
-have "v \<in> CPT (CHAR c) [c]" by fact
+have "v \<in> CV (CHAR c) [c]" by fact
 then have "v = Char c"
-by (simp add: CPT_simps)
+by (simp add: CV_simps)
 then show "Char c :\<sqsubseteq>val v"
 by (simp add: PosOrd_ex_eq_def)
 next
 case (Posix_ALT1 s r1 v r2 v2)
 have as1: "s \<in> r1 \<rightarrow> v" by fact
-have IH: "\<And>v2. v2 \<in> CPT r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+have IH: "\<And>v2. v2 \<in> CV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
-have "v2 \<in> CPT (ALT r1 r2) s" by fact
+have "v2 \<in> CV (ALT r1 r2) s" by fact
 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
-by(auto simp add: CPT_def prefix_list_def)
+by(auto simp add: CV_def prefix_list_def)
 then consider
 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s"
 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
 by (auto elim: CPrf.cases)
 then show "Left v :\<sqsubseteq>val v2"
 proof(cases)
 case (Left v3)
-have "v3 \<in> CPT r1 s" using Left(2,3)
+have "v3 \<in> CV r1 s" using Left(2,3)
-by (auto simp add: CPT_def prefix_list_def)
+by (auto simp add: CV_def prefix_list_def)
 with IH have "v :\<sqsubseteq>val v3" by simp
 moreover
 have "flat v3 = flat v" using as1 Left(3)
 by (simp add: Posix1(2))
 ultimately have "Left v :\<sqsubseteq>val Left v3"
 qed
 next
 case (Posix_ALT2 s r2 v r1 v2)
 have as1: "s \<in> r2 \<rightarrow> v" by fact
 have as2: "s \<notin> L r1" by fact
-have IH: "\<And>v2. v2 \<in> CPT r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+have IH: "\<And>v2. v2 \<in> CV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
-have "v2 \<in> CPT (ALT r1 r2) s" by fact
+have "v2 \<in> CV (ALT r1 r2) s" by fact
 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
-by(auto simp add: CPT_def prefix_list_def)
+by(auto simp add: CV_def prefix_list_def)
 then consider
 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s"
 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
 by (auto elim: CPrf.cases)
 then show "Right v :\<sqsubseteq>val v2"
 proof (cases)
 case (Right v3)
-have "v3 \<in> CPT r2 s" using Right(2,3)
+have "v3 \<in> CV r2 s" using Right(2,3)
-by (auto simp add: CPT_def prefix_list_def)
+by (auto simp add: CV_def prefix_list_def)
 with IH have "v :\<sqsubseteq>val v3" by simp
 moreover
 have "flat v3 = flat v" using as1 Right(3)
 by (simp add: Posix1(2))
 ultimately have "Right v :\<sqsubseteq>val Right v3"
 by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
 then show "Right v :\<sqsubseteq>val v2" unfolding Right .
 next
 case (Left v3)
-have "v3 \<in> CPT r1 s" using Left(2,3) as2
+have "v3 \<in> CV r1 s" using Left(2,3) as2
-by (auto simp add: CPT_def prefix_list_def)
+by (auto simp add: CV_def prefix_list_def)
 then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
-by (simp add: Posix1(2) CPT_def)
+by (simp add: Posix1(2) CV_def)
 then have "False" using as1 as2 Left
 by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf)
 then show "Right v :\<sqsubseteq>val v2" by simp
 qed
 next
 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
 have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
 then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
-have IH1: "\<And>v3. v3 \<in> CPT r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
+have IH1: "\<And>v3. v3 \<in> CV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
-have IH2: "\<And>v3. v3 \<in> CPT r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
+have IH2: "\<And>v3. v3 \<in> CV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
 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
-have "v3 \<in> CPT (SEQ r1 r2) (s1 @ s2)" by fact
+have "v3 \<in> CV (SEQ r1 r2) (s1 @ s2)" by fact
 then obtain v3a v3b where eqs:
 "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
 "flat v3a @ flat v3b = s1 @ s2"
-by (force simp add: prefix_list_def CPT_def elim: CPrf.cases)
+by (force simp add: prefix_list_def CV_def elim: CPrf.cases)
 with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
 by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv)
 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
 by (simp add: sprefix_list_def append_eq_conv_conj)
 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)"
 using PosOrd_spreI as1(1) eqs by blast
-then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPT r1 s1 \<and> v3b \<in> CPT r2 s2)" using eqs(2,3)
+then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CV r1 s1 \<and> v3b \<in> CV r2 s2)" using eqs(2,3)
-by (auto simp add: CPT_def)
+by (auto simp add: CV_def)
 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast
 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
 unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2)
 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
 next
 case (Posix_STAR1 s1 r v s2 vs v3)
 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
-have IH1: "\<And>v3. v3 \<in> CPT r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+have IH1: "\<And>v3. v3 \<in> CV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
-have IH2: "\<And>v3. v3 \<in> CPT (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+have IH2: "\<And>v3. v3 \<in> CV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
 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
 have cond2: "flat v \<noteq> []" by fact
-have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact
+have "v3 \<in> CV (STAR r) (s1 @ s2)" by fact
 then consider
 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
 "flat (Stars (v3a # vs3)) = s1 @ s2"
 | (Empty) "v3 = Stars []"
-unfolding CPT_def
+unfolding CV_def
 apply(auto)
 apply(erule CPrf.cases)
 apply(simp_all)
 apply(auto)[1]
 apply(case_tac vs)
 by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7))
 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
 by (simp add: sprefix_list_def append_eq_conv_conj)
 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)"
 using PosOrd_spreI as1(1) NonEmpty(4) by blast
-then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPT r s1 \<and> Stars vs3 \<in> CPT (STAR r) s2)"
+then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CV r s1 \<and> Stars vs3 \<in> CV (STAR r) s2)"
-using NonEmpty(2,3) by (auto simp add: CPT_def)
+using NonEmpty(2,3) by (auto simp add: CV_def)
 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)"
 unfolding PosOrd_ex_eq_def by auto
 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
 unfolding  PosOrd_ex_eq_def
 unfolding PosOrd_ex_eq_def using cond2
 by (simp add: PosOrd_shorterI)
 qed
 next
 case (Posix_STAR2 r v2)
-have "v2 \<in> CPT (STAR r) []" by fact
+have "v2 \<in> CV (STAR r) []" by fact
 then have "v2 = Stars []"
-unfolding CPT_def by (auto elim: CPrf.cases)
+unfolding CV_def by (auto elim: CPrf.cases)
 then show "Stars [] :\<sqsubseteq>val v2"
 by (simp add: PosOrd_ex_eq_def)
 qed
-lemma Posix_PosOrd_stronger:
-assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s"
-shows "v1 :\<sqsubseteq>val v2"
-proof -
-from assms(2) have "v2 \<in> CPT r s \<or> flat v2 \<sqsubset>spre s"
-unfolding CPTpre_def CPT_def sprefix_list_def prefix_list_def by auto
-moreover
-{ assume "v2 \<in> CPT r s"
-with assms(1)
-have "v1 :\<sqsubseteq>val v2" by (rule Posix_PosOrd)
-}
-moreover
-{ assume "flat v2 \<sqsubset>spre s"
-then have "flat v2 \<sqsubset>spre flat v1" using assms(1)
-using Posix1(2) by blast
-then have "v1 :\<sqsubseteq>val v2"
-by (simp add: PosOrd_ex_eq_def PosOrd_spreI)
-}
-ultimately show "v1 :\<sqsubseteq>val v2" by blast
-qed
 lemma Posix_PosOrd_reverse:
 assumes "s \<in> r \<rightarrow> v1"
-shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)"
+shows "\<not>(\<exists>v2 \<in> CV r s. v2 :\<sqsubset>val v1)"
 using assms
-by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def
+by (metis Posix_PosOrd less_irrefl PosOrd_def
 PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
-lemma test2:
-assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
-shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))"
-using assms
-apply(induct vs)
-apply(auto simp add: CPT_def)
-apply(rule CPrf.intros)
-apply(simp)
-apply(rule CPrf.intros)
-apply(simp_all)
-by (metis (no_types, lifting) CPT_def Posix_CPT mem_Collect_eq)
 lemma PosOrd_Posix_Stars:
 assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
-and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
+and "\<not>(\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
 shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs"
 using assms
 proof(induct vs)
 case Nil
 show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []"
 by(simp add: Posix.intros)
 next
 case (Cons v vs)
 have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> [];
-\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
+\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
 \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
 have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
-have as3: "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
+have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
 have "flat v \<in> r \<rightarrow> v" using as2 by simp
 moreover
 have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
 proof (rule IH)
 show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
 next
-show "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
+show "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
 apply(auto)
-apply(subst (asm) (2) PT_def)
+apply(subst (asm) (2) LV_def)
 apply(auto)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(drule_tac x="Stars (v # vs)" in bspec)
-apply(simp add: PT_def CPT_def)
+apply(simp add: LV_def CV_def)
 using Posix_Prf Prf.intros(6) calculation
 apply(rule_tac Prf.intros)
 apply(simp add:)
 apply (simp add: PosOrd_StarsI2)
 done
 apply(rotate_tac 5)
 apply(erule Prf.cases)
 apply(simp_all)
 apply(clarify)
 apply(drule_tac x="Stars (va#vs)" in bspec)
-apply(auto simp add: PT_def)[1]
+apply(auto simp add: LV_def)[1]
 apply(rule Prf.intros)
 apply(simp)
 by (simp add: PosOrd_StarsI PosOrd_shorterI)
 ultimately show "flat (Stars (v # vs)) \<in> STAR r \<rightarrow> Stars (v # vs)"
 by (simp add: Posix.intros)
 section {* The Smallest Value is indeed the Posix Value *}
 text {*
-The next lemma seems to require PT instead of CPT in the Star-case.
+The next lemma seems to require LV instead of CV in the Star-case.
 *}
 lemma PosOrd_Posix:
-assumes "v1 \<in> CPT r s" "\<forall>v\<^sub>2 \<in> PT r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
+assumes "v1 \<in> CV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
 shows "s \<in> r \<rightarrow> v1"
 using assms
 proof(induct r arbitrary: s v1)
 case (ZERO s v1)
-have "v1 \<in> CPT ZERO s" by fact
+have "v1 \<in> CV ZERO s" by fact
-then show "s \<in> ZERO \<rightarrow> v1" unfolding CPT_def
+then show "s \<in> ZERO \<rightarrow> v1" unfolding CV_def
 by (auto elim: CPrf.cases)
 next
 case (ONE s v1)
-have "v1 \<in> CPT ONE s" by fact
+have "v1 \<in> CV ONE s" by fact
-then show "s \<in> ONE \<rightarrow> v1" unfolding CPT_def
+then show "s \<in> ONE \<rightarrow> v1" unfolding CV_def
 by(auto elim!: CPrf.cases intro: Posix.intros)
 next
 case (CHAR c s v1)
-have "v1 \<in> CPT (CHAR c) s" by fact
+have "v1 \<in> CV (CHAR c) s" by fact
-then show "s \<in> CHAR c \<rightarrow> v1" unfolding CPT_def
+then show "s \<in> CHAR c \<rightarrow> v1" unfolding CV_def
 by (auto elim!: CPrf.cases intro: Posix.intros)
 next
 case (ALT r1 r2 s v1)
-have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CPT r1 s; \<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
+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
-have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CPT r2 s; \<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
+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
-have as1: "\<forall>v2\<in>PT (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
+have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
-have as2: "v1 \<in> CPT (ALT r1 r2) s" by fact
+have as2: "v1 \<in> CV (ALT r1 r2) s" by fact
 then consider
 (Left) v1' where
 "v1 = Left v1'" "s = flat v1'"
-"v1' \<in> CPT r1 s"
+"v1' \<in> CV r1 s"
 |  (Right) v1' where
 "v1 = Right v1'" "s = flat v1'"
-"v1' \<in> CPT r2 s"
+"v1' \<in> CV r2 s"
-unfolding CPT_def by (auto elim: CPrf.cases)
+unfolding CV_def by (auto elim: CPrf.cases)
 then show "s \<in> ALT r1 r2 \<rightarrow> v1"
 proof (cases)
 case (Left v1')
-have "v1' \<in> CPT r1 s" using as2
+have "v1' \<in> CV r1 s" using as2
-unfolding CPT_def Left by (auto elim: CPrf.cases)
+unfolding CV_def Left by (auto elim: CPrf.cases)
 moreover
-have "\<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
+have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
-unfolding PT_def Left using Prf.intros(2) PosOrd_Left_eq by force
+unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force
 ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
 then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
 next
 case (Right v1')
-have "v1' \<in> CPT r2 s" using as2
+have "v1' \<in> CV r2 s" using as2
-unfolding CPT_def Right by (auto elim: CPrf.cases)
+unfolding CV_def Right by (auto elim: CPrf.cases)
 moreover
-have "\<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
+have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
-unfolding PT_def Right using Prf.intros(3) PosOrd_RightI by force
+unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force
 ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
 moreover
 { assume "s \<in> L r1"
-then obtain v' where "v' \<in>  PT r1 s"
+then obtain v' where "v' \<in>  LV r1 s"
-unfolding PT_def using L_flat_Prf2 by blast
+unfolding LV_def using L_flat_Prf2 by blast
-then have "Left v' \<in>  PT (ALT r1 r2) s"
+then have "Left v' \<in>  LV (ALT r1 r2) s"
-unfolding PT_def by (auto intro: Prf.intros)
+unfolding LV_def by (auto intro: Prf.intros)
 with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)"
-unfolding PT_def Right by (auto)
+unfolding LV_def Right by (auto)
 then have False using PosOrd_Left_Right Right by blast
 }
 then have "s \<notin> L r1" by rule
 ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros)
 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp
 qed
 next
 case (SEQ r1 r2 s v1)
-have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CPT r1 s; \<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
+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
-have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CPT r2 s; \<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
+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
-have as1: "\<forall>v2\<in>PT (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
+have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
-have as2: "v1 \<in> CPT (SEQ r1 r2) s" by fact
+have as2: "v1 \<in> CV (SEQ r1 r2) s" by fact
 then obtain
 v1a v1b where eqs:
 "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
-"v1a \<in> CPT r1 (flat v1a)" "v1b \<in> CPT r2 (flat v1b)"
+"v1a \<in> CV r1 (flat v1a)" "v1b \<in> CV r2 (flat v1b)"
-unfolding CPT_def by(auto elim: CPrf.cases)
+unfolding CV_def by(auto elim: CPrf.cases)
-have "\<forall>v2 \<in> PT r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
+have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
 proof
 fix v2
-assume "v2 \<in> PT r1 (flat v1a)"
+assume "v2 \<in> LV r1 (flat v1a)"
-with eqs(2,4) have "Seq v2 v1b \<in> PT (SEQ r1 r2) s"
+with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s"
-by (simp add: CPT_def PT_def Prf.intros(1) Prf_CPrf)
+by (simp add: CV_def LV_def Prf.intros(1) Prf_CPrf)
 with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)"
-using eqs by (simp add: PT_def)
+using eqs by (simp add: LV_def)
 then show "\<not> v2 :\<sqsubset>val v1a"
 using PosOrd_SeqI1 by blast
 qed
 then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp
 moreover
-have "\<forall>v2 \<in> PT r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
+have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
 proof
 fix v2
-assume "v2 \<in> PT r2 (flat v1b)"
+assume "v2 \<in> LV r2 (flat v1b)"
-with eqs(2,3,4) have "Seq v1a v2 \<in> PT (SEQ r1 r2) s"
+with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s"
-by (simp add: CPT_def PT_def Prf.intros Prf_CPrf)
+by (simp add: CV_def LV_def Prf.intros Prf_CPrf)
 with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b"
-using eqs by (simp add: PT_def)
+using eqs by (simp add: LV_def)
 then show "\<not> v2 :\<sqsubset>val v1b"
 using PosOrd_SeqI2 by auto
 qed
 then have "flat v1b \<in> r2 \<rightarrow> v1b" using IH2 eqs by simp
 moreover
 proof
 assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2"
 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
 then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<turnstile> vA : r1" "flat vB = s4" "\<turnstile> vB : r2"
 using L_flat_Prf2 by blast
-then have "Seq vA vB \<in> PT (SEQ r1 r2) s" unfolding eqs using q1
+then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1
-by (auto simp add: PT_def intro: Prf.intros)
+by (auto simp add: LV_def intro: Prf.intros)
 with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto
 then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto
 then show "False"
 using PosOrd_shorterI by blast
 qed
 ultimately
 show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs
 by (rule Posix.intros)
 next
 case (STAR r s v1)
-have IH: "\<And>s v1. \<lbrakk>v1 \<in> CPT r s; \<forall>v2\<in>PT r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
+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
-have as1: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
+have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
-have as2: "v1 \<in> CPT (STAR r) s" by fact
+have as2: "v1 \<in> CV (STAR r) s" by fact
 then obtain
 vs where eqs:
 "v1 = Stars vs" "s = flat (Stars vs)"
-"\<forall>v \<in> set vs. v \<in> CPT r (flat v)"
+"\<forall>v \<in> set vs. v \<in> CV r (flat v)"
-unfolding CPT_def by (auto elim: CPrf.cases dest!: CPrf_stars)
+unfolding CV_def by (auto elim: CPrf.cases)
 have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
 proof
 fix v
 assume a: "v \<in> set vs"
 then obtain pre post where e: "vs = pre @ [v] @ post"
 by (metis append_Cons append_Nil in_set_conv_decomp_first)
-then have q: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)"
+then have q: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)"
 using as1 unfolding eqs by simp
-have "\<forall>v2\<in>PT r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs
+have "\<forall>v2\<in>LV r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs
 proof (rule ballI, rule notI)
 fix v2
 assume w: "v2 :\<sqsubset>val v"
-assume "v2 \<in> PT r (flat v)"
+assume "v2 \<in> LV r (flat v)"
-then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s"
+then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s"
 using as2 unfolding e eqs
-apply(auto simp add: CPT_def PT_def intro!: Prf.intros)[1]
+apply(auto simp add: CV_def LV_def intro!: Prf.intros)[1]
-using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast
+using CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros apply blast
-by (meson CPrf_Stars_appendE CPrf_stars Prf_CPrf list.set_intros(2))
+by (metis CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros(2) val.inject(5))
 then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
 using q by simp
 with w show "False"
-using PT_def \<open>v2 \<in> PT r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq
+using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq
 PosOrd_StarsI PosOrd_Stars_appendI by auto
 qed
 with IH
-show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs
+show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs CV_def
-using eqs(3) by (smt CPT_def CPrf_stars mem_Collect_eq)
+by (auto elim: CPrf.cases)
 qed
 moreover
-have "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)"
+have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)"
 proof
-assume "\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
+assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
 then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
 "Stars vs2 :\<sqsubset>val Stars vs"
-unfolding PT_def
+unfolding LV_def
-apply(auto elim: Prf.cases)
+apply(auto)
 apply(erule Prf.cases)
 apply(auto intro: Prf.intros)
 done
 then show "False" using as1 unfolding eqs
 apply -
 apply(drule_tac x="Stars vs2" in bspec)
-apply(auto simp add: PT_def)
+apply(auto simp add: LV_def)
 done
 qed
 ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
 thm PosOrd_Posix_Stars
 by (rule PosOrd_Posix_Stars)

changeset 267	32b222d77fa0
parent 266	fff2e1b40dfc
child 268	6746f5e1f1f8