theory Positions
imports "Lexer"
begin
section {* Positions in Values *}
fun
at :: "val \<Rightarrow> nat list \<Rightarrow> val"
where
"at v [] = v"
| "at (Left v) (0#ps)= at v ps"
| "at (Right v) (Suc 0#ps)= at v ps"
| "at (Seq v1 v2) (0#ps)= at v1 ps"
| "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
| "at (Stars vs) (n#ps)= at (nth vs n) ps"
fun Pos :: "val \<Rightarrow> (nat list) set"
where
"Pos (Void) = {[]}"
| "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)}"
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(simp add: insert_ident)
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_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)
lemma intlen_length:
shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
apply(induct xs arbitrary: ys)
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)
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)"
lemma pflat_len_simps:
shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"
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)"
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)
section {* Orderings *}
definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
where
"ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2"
definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60)
where
"ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2"
inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60)
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
by(induct rule: lex_list.induct)(auto)
lemma lex_simps [simp]:
fixes xs ys :: "nat list"
shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
and "xs \<sqsubset>lex [] \<longleftrightarrow> False"
and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))"
by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
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
by (induct arbitrary: ps3 rule: lex_list.induct)
(auto elim: lex_list.cases)
lemma lex_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 elim: lex_list.cases)
apply(case_tac q)
apply(auto)
done
section {* POSIX Ordering of Values According to Okui & Suzuki *}
definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
where
"v1 \<sqsubset>val p v2 \<equiv> 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)"
definition pflat_len2 :: "val \<Rightarrow> nat list => (bool * nat)"
where
"pflat_len2 v p \<equiv> (if p \<in> Pos v then (True, length (flat (at v p))) else (False, 0))"
instance prod :: (ord, ord) ord
by (rule Orderings.class.Orderings.ord.of_class.intro)
lemma "(0, 0) < (3::nat, 2::nat)"
definition PosOrd2:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val2 _ _" [60, 60, 59] 60)
where
"v1 \<sqsubset>val2 p v2 \<equiv> (fst (pflat_len2 v1 p) > fst (pflat_len2 v2 p) \<or>
snd (pflat_len2 v1 p) > fst (pflat_len2 v2 p)) \<and>
(\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
where
"v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
where
"v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
lemma PosOrd_shorterE:
assumes "v1 :\<sqsubset>val v2"
shows "length (flat v2) \<le> length (flat v1)"
using assms
apply(auto simp add: pflat_len_simps PosOrd_ex_def PosOrd_def)
apply(case_tac p)
apply(simp add: pflat_len_simps intlen_length)
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
unfolding PosOrd_ex_def
by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
lemma PosOrd_spreI:
assumes "flat v' \<sqsubset>spre flat v"
shows "v :\<sqsubset>val v'"
using assms
apply(rule_tac PosOrd_shorterI)
by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
lemma PosOrd_Left_Right:
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(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'"
using assms
unfolding PosOrd_ex_def
apply(auto)
apply(case_tac p)
apply(simp add: PosOrd_def pflat_len_simps)
apply(case_tac a)
apply(simp add: PosOrd_def pflat_len_simps)
apply(rule_tac x="list" in exI)
apply(auto simp add: PosOrd_def pflat_len_simps)[1]
apply (smt Un_def lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
apply (smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
apply(auto simp add: PosOrd_def pflat_len_outside)[1]
apply(rule_tac x="0#p" in exI)
apply(auto simp add: PosOrd_def pflat_len_simps)
done
lemma PosOrd_RightI:
assumes "v :\<sqsubset>val v'" "flat v = flat v'"
shows "(Right v) :\<sqsubset>val (Right v')"
using assms(1)
unfolding PosOrd_ex_def
apply(auto)
apply(rule_tac x="Suc 0#p" in exI)
using assms(2)
apply(auto simp add: PosOrd_def pflat_len_simps)
done
lemma PosOrd_RightE:
assumes "(Right v1) :\<sqsubset>val (Right v2)"
shows "v1 :\<sqsubset>val v2"
using assms
apply(simp add: PosOrd_ex_def)
apply(erule exE)
apply(case_tac p)
apply(simp add: PosOrd_def)
apply(auto simp add: pflat_len_simps)
apply(rule_tac x="[]" in exI)
apply(simp add: Pos_empty pflat_len_simps)
apply(case_tac a)
apply(simp add: pflat_len_def PosOrd_def)
apply(case_tac nat)
prefer 2
apply(simp add: pflat_len_def PosOrd_def)
apply(auto simp add: pflat_len_simps PosOrd_def)
apply(rule_tac x="list" in exI)
apply(auto)
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
done
lemma PosOrd_SeqI1:
assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')"
using assms(1)
apply(subst (asm) PosOrd_ex_def)
apply(subst (asm) PosOrd_def)
apply(clarify)
apply(subst PosOrd_ex_def)
apply(rule_tac x="0#p" in exI)
apply(subst PosOrd_def)
apply(rule conjI)
apply(simp add: pflat_len_simps)
apply(rule ballI)
apply(rule impI)
apply(simp only: Pos.simps)
apply(auto)[1]
apply(simp add: pflat_len_simps)
using assms(2)
apply(simp)
apply(auto simp add: pflat_len_simps)[2]
done
lemma PosOrd_SeqI2:
assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
shows "(Seq v v2) :\<sqsubset>val (Seq v v2')"
using assms(1)
apply(subst (asm) PosOrd_ex_def)
apply(subst (asm) PosOrd_def)
apply(clarify)
apply(subst PosOrd_ex_def)
apply(rule_tac x="Suc 0#p" in exI)
apply(subst PosOrd_def)
apply(rule conjI)
apply(simp add: pflat_len_simps)
apply(rule ballI)
apply(rule impI)
apply(simp only: Pos.simps)
apply(auto)[1]
apply(simp add: pflat_len_simps)
using assms(2)
apply(simp)
apply(auto simp add: pflat_len_simps)
done
lemma PosOrd_SeqE:
assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')"
shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'"
using assms
apply(simp add: PosOrd_ex_def)
apply(erule exE)
apply(case_tac p)
apply(simp add: PosOrd_def)
apply(auto simp add: pflat_len_simps intlen_append)[1]
apply(rule_tac x="[]" in exI)
apply(drule_tac x="[]" in spec)
apply(simp add: Pos_empty pflat_len_simps)
apply(case_tac a)
apply(rule disjI1)
apply(simp add: PosOrd_def)
apply(auto simp add: pflat_len_simps intlen_append)[1]
apply(rule_tac x="list" in exI)
apply(simp)
apply(rule ballI)
apply(rule impI)
apply(drule_tac x="0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
apply(case_tac nat)
apply(rule disjI2)
apply(simp add: PosOrd_def)
apply(auto simp add: pflat_len_simps intlen_append)
apply(rule_tac x="list" in exI)
apply(simp add: Pos_empty)
apply(rule ballI)
apply(rule impI)
apply(auto)[1]
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
apply(simp add: pflat_len_simps)
apply(simp add: PosOrd_def pflat_len_def)
done
lemma PosOrd_StarsI:
assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))"
using assms(1)
apply(subst (asm) PosOrd_ex_def)
apply(subst (asm) PosOrd_def)
apply(clarify)
apply(subst PosOrd_ex_def)
apply(subst PosOrd_def)
apply(rule_tac x="0#p" in exI)
apply(simp add: pflat_len_Stars_simps pflat_len_simps)
using assms(2)
apply(simp add: pflat_len_simps intlen_append)
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
done
lemma PosOrd_StarsI2:
assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"
shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))"
using assms(1)
apply(subst (asm) PosOrd_ex_def)
apply(subst (asm) PosOrd_def)
apply(clarify)
apply(subst PosOrd_ex_def)
apply(subst PosOrd_def)
apply(case_tac p)
apply(simp add: pflat_len_simps)
apply(rule_tac x="[]" in exI)
apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append)
apply(rule_tac x="Suc a#list" in exI)
apply(simp add: pflat_len_Stars_simps pflat_len_simps)
using assms(2)
apply(simp add: pflat_len_simps intlen_append)
apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
done
lemma PosOrd_Stars_appendI:
assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
using assms
apply(induct vs)
apply(simp)
apply(simp add: PosOrd_StarsI2)
done
lemma PosOrd_StarsE2:
assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
shows "Stars vs1 :\<sqsubset>val Stars vs2"
using assms
apply(subst (asm) PosOrd_ex_def)
apply(erule exE)
apply(case_tac p)
apply(simp)
apply(simp add: PosOrd_def pflat_len_simps intlen_append)
apply(subst PosOrd_ex_def)
apply(rule_tac x="[]" in exI)
apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
apply(simp)
apply(case_tac a)
apply(clarify)
apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
apply(clarify)
apply(simp add: PosOrd_ex_def)
apply(rule_tac x="nat#list" in exI)
apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
apply(case_tac q)
apply(simp add: PosOrd_def pflat_len_simps intlen_append)
apply(clarify)
apply(drule_tac x="Suc a # lista" in bspec)
apply(simp)
apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
apply(case_tac q)
apply(simp add: PosOrd_def pflat_len_simps intlen_append)
apply(clarify)
apply(drule_tac x="Suc a # lista" in bspec)
apply(simp)
apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
done
lemma PosOrd_Stars_appendE:
assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
shows "Stars vs1 :\<sqsubset>val Stars vs2"
using assms
apply(induct vs)
apply(simp)
apply(simp add: PosOrd_StarsE2)
done
lemma PosOrd_Stars_append_eq:
assumes "flat (Stars vs1) = flat (Stars vs2)"
shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2"
using assms
apply(rule_tac iffI)
apply(erule PosOrd_Stars_appendE)
apply(rule PosOrd_Stars_appendI)
apply(auto)
done
lemma PosOrd_trans:
assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
shows "v1 :\<sqsubset>val v3"
proof -
from assms obtain p p'
where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
by (rule lex_trichotomous)
moreover
{ assume "p = p'"
with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
by fastforce
then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
}
moreover
{ assume "p \<sqsubset>lex p'"
with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
by (smt Un_iff lex_trans)
then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
}
moreover
{ assume "p' \<sqsubset>lex p"
with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
by (smt Un_iff intlen_bigger lex_trans pflat_len_def)
then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
}
ultimately show "v1 :\<sqsubset>val v3" by blast
qed
lemma PosOrd_irrefl:
assumes "v :\<sqsubset>val v"
shows "False"
using assms unfolding PosOrd_ex_def PosOrd_def
by auto
lemma PosOrd_almost_trichotomous:
shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
apply(auto simp add: PosOrd_ex_def)
apply(auto simp add: PosOrd_def)
apply(rule_tac x="[]" in exI)
apply(auto simp add: Pos_empty pflat_len_simps)
apply(drule_tac x="[]" in spec)
apply(auto simp add: Pos_empty pflat_len_simps)
done
lemma WW1:
assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1"
shows "False"
using assms
apply(auto simp add: PosOrd_ex_def PosOrd_def)
using assms PosOrd_irrefl PosOrd_trans by blast
lemma PosOrd_SeqE2:
assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')"
using assms
apply(frule_tac PosOrd_SeqE)
apply(erule disjE)
apply(simp)
apply(case_tac "v1 :\<sqsubset>val v1'")
apply(simp)
apply(rule disjI2)
apply(rule conjI)
prefer 2
apply(simp)
apply(auto)
apply(auto simp add: PosOrd_ex_def)
apply(auto simp add: PosOrd_def pflat_len_simps)
apply(case_tac p)
apply(auto simp add: PosOrd_def pflat_len_simps)
apply(case_tac a)
apply(auto simp add: PosOrd_def pflat_len_simps)
apply (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
lemma PosOrd_SeqE4:
assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')"
using assms
apply(frule_tac PosOrd_SeqE)
apply(erule disjE)
apply(simp)
apply(case_tac "v1 :\<sqsubset>val v1'")
apply(simp)
apply(rule disjI2)
apply(rule conjI)
prefer 2
apply(simp)
apply(auto)
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 {* CPT and CPTpre *}
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"
| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
| "\<Turnstile> Void : ONE"
| "\<Turnstile> Char c : CHAR c"
| "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
lemma Prf_CPrf:
assumes "\<Turnstile> v : r"
shows "\<turnstile> v : r"
using assms
by (induct)(auto intro: Prf.intros)
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(erule_tac CPrf.cases)
apply(simp_all)
done
lemma CPrf_Stars_appendE:
assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r"
using assms
apply(erule_tac CPrf.cases)
apply(auto intro: CPrf.intros elim: Prf.cases)
done
definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
definition
"CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"
definition
"CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"
lemma CPT_CPTpre_subset:
shows "CPT r s \<subseteq> CPTpre r s"
by(auto simp add: CPT_def CPTpre_def)
lemma CPT_simps:
shows "CPT ZERO s = {}"
and "CPT ONE s = (if s = [] then {Void} else {})"
and "CPT (CHAR c) s = (if s = [c] then {Char c} else {})"
and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
and "CPT (SEQ r1 r2) s =
{Seq v1 v2 | v1 v2. flat v1 @ flat v2 = s \<and> v1 \<in> CPT r1 (flat v1) \<and> v2 \<in> CPT r2 (flat v2)}"
and "CPT (STAR r) s =
Stars ` {vs. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. v \<in> CPT r (flat v) \<and> flat v \<noteq> [])}"
apply -
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[6]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[6]
apply(erule CPrf.cases)
apply(simp_all)[6]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[6]
apply(erule CPrf.cases)
apply(simp_all)[6]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[6]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[6]
(* STAR case *)
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[6]
done
(*
lemma CPTpre_STAR_finite:
assumes "\<And>s. finite (CPT r s)"
shows "finite (CPT (STAR r) s)"
apply(induct s rule: length_induct)
apply(case_tac xs)
apply(simp)
apply(simp add: CPT_simps)
apply(auto)
apply(rule finite_imageI)
using assms
thm finite_Un
prefer 2
apply(simp add: CPT_simps)
apply(rule finite_imageI)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
apply(auto)[1]
apply(rule finite_imageI)
apply(simp add: Collect_case_prod_Sigma)
apply(rule finite_SigmaI)
apply(rule assms)
apply(case_tac "flat v = []")
apply(simp)
apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
apply(simp)
apply(auto)[1]
apply(rule test)
apply(simp)
done
lemma CPTpre_subsets:
"CPTpre ZERO s = {}"
"CPTpre ONE s \<subseteq> {Void}"
"CPTpre (CHAR c) s \<subseteq> {Char c}"
"CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
"CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
"CPTpre (STAR r) s \<subseteq> {Stars []} \<union>
{Stars (v#vs) | v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}"
"CPTpre (STAR r) [] = {Stars []}"
apply(auto simp add: CPTpre_def)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(rule CPrf.intros)
done
lemma CPTpre_simps:
shows "CPTpre ONE s = {Void}"
and "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})"
and "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
and "CPTpre (SEQ r1 r2) s =
{Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
apply -
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1]
apply(case_tac "c = d")
apply(simp)
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(simp)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
done
lemma CPT_simps:
shows "CPT ONE s = (if s = [] then {Void} else {})"
and "CPT (CHAR c) [d] = (if c = d then {Char c} else {})"
and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
and "CPT (SEQ r1 r2) s =
{Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}"
apply -
apply(rule subset_antisym)
apply(auto simp add: CPT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(clarify)
apply blast
apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
done
lemma test:
assumes "finite A"
shows "finite {vs. Stars vs \<in> A}"
using assms
apply(induct A)
apply(simp)
apply(auto)
apply(case_tac x)
apply(simp_all)
done
lemma CPTpre_STAR_finite:
assumes "\<And>s. finite (CPTpre r s)"
shows "finite (CPTpre (STAR r) s)"
apply(induct s rule: length_induct)
apply(case_tac xs)
apply(simp)
apply(simp add: CPTpre_subsets)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
apply(auto)[1]
apply(rule finite_imageI)
apply(simp add: Collect_case_prod_Sigma)
apply(rule finite_SigmaI)
apply(rule assms)
apply(case_tac "flat v = []")
apply(simp)
apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
apply(simp)
apply(auto)[1]
apply(rule test)
apply(simp)
done
lemma CPTpre_finite:
shows "finite (CPTpre r s)"
apply(induct r arbitrary: s)
apply(simp add: CPTpre_subsets)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2). v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset)
apply(auto)[1]
apply(rule finite_imageI)
apply(simp add: Collect_case_prod_Sigma)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
by (simp add: CPTpre_STAR_finite)
lemma CPT_finite:
shows "finite (CPT r s)"
apply(rule finite_subset)
apply(rule CPT_CPTpre_subset)
apply(rule CPTpre_finite)
done
*)
lemma Posix_CPT:
assumes "s \<in> r \<rightarrow> v"
shows "v \<in> CPT r s"
using assms
apply(induct rule: Posix.induct)
apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases)
apply(rotate_tac 5)
apply(erule CPrf.cases)
apply(simp_all)
apply(rule CPrf.intros)
apply(simp_all)
done
section {* The Posix Value is smaller than any other Value *}
lemma Posix_PosOrd:
assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT 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
then have "v = Void"
by (simp add: CPT_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
then have "v = Char c"
by (simp add: CPT_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 "v2 \<in> CPT (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)
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)
by (auto simp add: CPT_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"
by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
then show "Left v :\<sqsubseteq>val v2" unfolding Left .
next
case (Right v3)
have "flat v3 = flat v" using as1 Right(3)
by (simp add: Posix1(2))
then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1
by (auto simp add: PosOrd_ex_eq_def PosOrd_Left_Right)
then show "Left v :\<sqsubseteq>val v2" unfolding Right .
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 "v2 \<in> CPT (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)
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)
by (auto simp add: CPT_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
by (auto simp add: CPT_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)
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 IH2: "\<And>v3. v3 \<in> CPT 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
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)
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)
by (auto simp add: CPT_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 IH2: "\<And>v3. v3 \<in> CPT (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
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
apply(auto)
apply(erule CPrf.cases)
apply(simp_all)
apply(auto)[1]
apply(case_tac vs)
apply(auto)
using CPrf.intros(6) by blast
then show "Stars (v # vs) :\<sqsubseteq>val v3" (* HERE *)
proof (cases)
case (NonEmpty v3a vs3)
have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
unfolding prefix_list_def
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)"
using NonEmpty(2,3) by (auto simp add: CPT_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
by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) val.inject(5))
then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
next
case Empty
have "v3 = Stars []" by fact
then show "Stars (v # vs) :\<sqsubseteq>val v3"
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
then have "v2 = Stars []"
unfolding CPT_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)"
using assms
by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def
PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
(*
lemma PosOrd_Posix_Stars:
assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v"
and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs"
using assms
apply(induct vs)
apply(simp)
apply(rule Posix.intros)
apply(simp (no_asm))
apply(rule Posix.intros)
apply(auto)[1]
apply(auto simp add: CPT_def PT_def)[1]
defer
apply(simp)
apply(drule meta_mp)
apply(auto simp add: CPT_def PT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(drule meta_mp)
apply(auto simp add: CPT_def PT_def)[1]
apply(erule Prf.cases)
apply(simp_all)
using CPrf_stars PosOrd_irrefl apply fastforce
apply(clarify)
apply(drule_tac x="Stars (a#v#vsa)" in spec)
apply(simp)
apply(drule mp)
apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
apply(subst (asm) (2) PosOrd_ex_def)
apply(simp)
apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_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")
prefer 2
apply (meson L_flat_Prf2)
apply(subgoal_tac "\<exists>vB. flat (Stars vB) = s\<^sub>4 \<and> \<turnstile> (Stars vB) : (STAR r)")
apply(clarify)
apply(drule_tac x="Stars (vA # vB)" in spec)
apply(simp)
apply(drule mp)
using Prf.intros(7) apply blast
apply(subst (asm) (2) PosOrd_ex_def)
apply(simp)
prefer 2
apply(simp)
using Star_values_exists apply blast
prefer 2
apply(drule meta_mp)
apply(erule CPrf.cases)
apply(simp_all)
apply(drule meta_mp)
apply(auto)[1]
prefer 2
apply(simp)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)
apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) PosOrd_def PosOrd_ex_def)
apply(drule_tac x="Stars (v#va#vsb)" in spec)
apply(drule mp)
apply (simp add: Posix1a Prf.intros(7))
apply(simp)
apply(subst (asm) (2) PosOrd_ex_def)
apply(simp)
apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def)
by (metis PosOrd_StarsI PosOrd_ex_def PosOrd_spreI append_assoc append_self_conv flat.simps(7) flat_Stars prefix_list_def sprefix_list_def)
*)
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))"
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>
\<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 "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
apply(auto)
apply(subst (asm) (2) PT_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)
using Posix1a Prf.intros(6) calculation
apply(rule_tac Prf.intros)
apply(simp add:)
apply (simp add: PosOrd_StarsI2)
done
qed
moreover
have "flat v \<noteq> []" using as2 by simp
moreover
have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))"
using as3
apply(auto)
apply(drule L_flat_Prf2)
apply(erule exE)
apply(simp only: L.simps[symmetric])
apply(drule L_flat_Prf2)
apply(erule exE)
apply(clarify)
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(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)
qed
section {* The Smallest Value is indeed the Posix Value *}
text {*
The next lemma seems to require PT instead of CPT 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"
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
then show "s \<in> ZERO \<rightarrow> v1" unfolding CPT_def
by (auto elim: CPrf.cases)
next
case (ONE s v1)
have "v1 \<in> CPT ONE s" by fact
then show "s \<in> ONE \<rightarrow> v1" unfolding CPT_def
by(auto elim!: CPrf.cases intro: Posix.intros)
next
case (CHAR c s v1)
have "v1 \<in> CPT (CHAR c) s" by fact
then show "s \<in> CHAR c \<rightarrow> v1" unfolding CPT_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 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 as1: "\<forall>v2\<in>PT (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
have as2: "v1 \<in> CPT (ALT r1 r2) s" by fact
then consider
(Left) v1' where
"v1 = Left v1'" "s = flat v1'"
"v1' \<in> CPT r1 s"
| (Right) v1' where
"v1 = Right v1'" "s = flat v1'"
"v1' \<in> CPT r2 s"
unfolding CPT_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
unfolding CPT_def Left by (auto elim: CPrf.cases)
moreover
have "\<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
unfolding PT_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
unfolding CPT_def Right by (auto elim: CPrf.cases)
moreover
have "\<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
unfolding PT_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"
unfolding PT_def using L_flat_Prf2 by blast
then have "Left v' \<in> PT (ALT r1 r2) s"
unfolding PT_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)
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 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 as1: "\<forall>v2\<in>PT (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
have as2: "v1 \<in> CPT (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)"
unfolding CPT_def by(auto elim: CPrf.cases)
have "\<forall>v2 \<in> PT r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
proof
fix v2
assume "v2 \<in> PT r1 (flat v1a)"
with eqs(2,4) have "Seq v2 v1b \<in> PT (SEQ r1 r2) s"
by (simp add: CPT_def PT_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)
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"
proof
fix v2
assume "v2 \<in> PT r2 (flat v1b)"
with eqs(2,3,4) have "Seq v1a v2 \<in> PT (SEQ r1 r2) s"
by (simp add: CPT_def PT_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)
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
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)"
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
by (auto simp add: PT_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 as1: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
have as2: "v1 \<in> CPT (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)"
unfolding CPT_def by (auto elim: CPrf.cases dest!: CPrf_stars)
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)"
using as1 unfolding eqs by simp
have "\<forall>v2\<in>PT 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)"
then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s"
using as2 unfolding e eqs
apply(auto simp add: CPT_def PT_def intro!: Prf.intros)[1]
using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast
by (meson CPrf_Stars_appendE CPrf_stars Prf_CPrf list.set_intros(2))
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
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
using eqs(3) by (smt CPT_def CPrf_stars mem_Collect_eq)
qed
moreover
have "\<not> (\<exists>vs2\<in>PT (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"
then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
"Stars vs2 :\<sqsubset>val Stars vs"
unfolding PT_def
apply(auto elim: Prf.cases)
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)
done
qed
ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
thm PosOrd_Posix_Stars
by (rule PosOrd_Posix_Stars)
then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
qed
unused_thms
end