--- a/thys/Positions.thy Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Positions.thy Tue Jul 18 18:39:20 2017 +0100
@@ -3,8 +3,7 @@
imports "Lexer"
begin
-
-section {* Position in values *}
+section {* Positions in Values *}
fun
at :: "val \<Rightarrow> nat list \<Rightarrow> val"
@@ -16,6 +15,8 @@
| "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) = {[]}"
@@ -26,15 +27,13 @@
| "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)
apply(simp add: insert_ident)
apply(rule subset_antisym)
-apply(auto)
-apply(auto)[1]
using less_Suc_eq_0_disj by auto
lemma Pos_empty:
@@ -44,7 +43,7 @@
fun intlen :: "'a list \<Rightarrow> int"
where
"intlen [] = 0"
-| "intlen (x#xs) = 1 + intlen xs"
+| "intlen (x # xs) = 1 + intlen xs"
lemma intlen_bigger:
shows "0 \<le> intlen xs"
@@ -62,6 +61,15 @@
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
@@ -87,9 +95,9 @@
apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
done
-lemma outside_lemma:
- assumes "p \<notin> Pos v1 \<union> Pos v2"
- shows "pflat_len v1 p = pflat_len v2 p"
+lemma pflat_len_outside:
+ assumes "p \<notin> Pos v1"
+ shows "pflat_len v1 p = -1 "
using assms by (auto simp add: pflat_len_def)
@@ -121,10 +129,8 @@
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> (\<not> y < x \<and> xs \<sqsubset>lex ys))"
-apply(auto elim: lex_list.cases intro: lex_list.intros)
-apply(auto simp add: neq_Nil_conv not_less_iff_gr_or_eq intro: lex_list.intros)
-done
+ 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"
@@ -139,7 +145,7 @@
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(auto elim: lex_list.cases)
apply(case_tac q)
apply(auto)
done
@@ -147,7 +153,7 @@
-section {* Ordering of values according to Okui & Suzuki *}
+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)
@@ -155,111 +161,95 @@
"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 PosOrd2:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val2 _ _" [60, 60, 59] 60)
-where
- "v1 \<sqsubset>val2 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)"
+
-lemma XXX:
- "v1 \<sqsubset>val p v2 \<longleftrightarrow> v1 \<sqsubset>val2 p v2"
-apply(auto simp add: PosOrd_def PosOrd2_def)
-apply(auto simp add: pflat_len_def split: if_splits)
-by (smt intlen_bigger)
+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)
-(* some tests *)
+lemma "(0, 0) < (3::nat, 2::nat)"
-definition ValFlat_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>fval _ _")
-where
- "v1 \<sqsubset>fval p v2 \<equiv> p \<in> Pos v1 \<and>
- (p \<notin> Pos v2 \<or> flat (at v2 p) \<sqsubset>spre flat (at v1 p)) \<and>
- (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> (pflat_len v1 q = pflat_len v2 q))"
+
+
-lemma
- assumes "v1 \<sqsubset>fval p v2"
- shows "v1 \<sqsubset>val p v2"
-using assms
-unfolding ValFlat_ord_def PosOrd_def
-apply(clarify)
-apply(simp add: pflat_len_def)
-apply(auto)[1]
-apply(smt intlen_bigger)
-apply(simp add: sprefix_list_def prefix_list_def)
-apply(auto)[1]
-apply(drule sym)
-apply(simp add: intlen_append)
-apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3))
-apply(smt intlen_bigger)
-done
-
-lemma
- assumes "v1 \<sqsubset>val p v2" "flat (at v2 p) \<sqsubset>spre flat (at v1 p)"
- shows "v1 \<sqsubset>fval p v2"
-using assms
-unfolding ValFlat_ord_def PosOrd_def
-apply(clarify)
-oops
+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)"
+ "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
-definition PosOrd_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
+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: PosOrd_ex_def PosOrd_def)
+apply(auto simp add: pflat_len_simps PosOrd_ex_def PosOrd_def)
apply(case_tac p)
-apply(simp add: pflat_len_simps)
-apply(simp add: intlen_length)
+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)
-by (metis intlen_length le_less less_irrefl linear)
-
+apply(simp add: pflat_len_simps le_less intlen_length_eq)
+done
lemma PosOrd_shorterI:
- assumes "length (flat v') < length (flat v)"
- shows "v :\<sqsubset>val v'"
+ 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)"
+ 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
+using assms
apply(auto simp add: PosOrd_def pflat_len_simps)
apply(smt intlen_bigger)
done
-lemma PosOrd_LeftI:
- assumes "v :\<sqsubset>val v'" "flat v = flat v'"
- shows "(Left v) :\<sqsubset>val (Left v')"
-using assms(1)
+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)
-using assms(2)
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')"
@@ -271,31 +261,6 @@
apply(auto simp add: PosOrd_def pflat_len_simps)
done
-lemma PosOrd_LeftE:
- assumes "(Left v1) :\<sqsubset>val (Left 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(auto simp add: pflat_len_simps PosOrd_def)
-apply(case_tac a)
-apply(auto simp add: pflat_len_simps)[1]
-apply(rule_tac x="list" in exI)
-apply(auto)
-apply(drule_tac x="0#q" in bspec)
-apply(simp)
-apply(simp add: pflat_len_simps)
-apply(drule_tac x="0#q" in bspec)
-apply(simp)
-apply(simp add: pflat_len_simps)
-apply(simp add: pflat_len_def)
-done
-
lemma PosOrd_RightE:
assumes "(Right v1) :\<sqsubset>val (Right v2)"
shows "v1 :\<sqsubset>val v2"
@@ -517,14 +482,14 @@
by (rule lex_trichotomous)
moreover
{ assume "p = p'"
- with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def
- by (smt outside_lemma)
+ 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
- by (metis lex_trans outside_lemma)
+ 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
@@ -560,26 +525,47 @@
apply(auto simp add: PosOrd_ex_def PosOrd_def)
using assms PosOrd_irrefl PosOrd_trans by blast
-lemma WW2:
- assumes "\<not>(v1 :\<sqsubset>val v2)"
- shows "v1 = v2 \<or> v2 :\<sqsubset>val v1"
-using assms
-oops
-
lemma PosOrd_SeqE2:
- assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')"
- shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')"
+ 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(auto)
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(case_tac "v1 = v1'")
+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)
-oops
+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 *}
@@ -592,84 +578,19 @@
| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
| "\<Turnstile> Void : ONE"
| "\<Turnstile> Char c : CHAR c"
-| "\<Turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
+| "\<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 pflat_len_equal_iff:
- assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
- and "\<forall>p. pflat_len v1 p = pflat_len v2 p"
- shows "v1 = v2"
-using assms
-apply(induct v1 r arbitrary: v2 rule: CPrf.induct)
-apply(rotate_tac 4)
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis pflat_len_simps(1) pflat_len_simps(2))
-apply(rotate_tac 2)
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis pflat_len_simps(3))
-apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
-apply(rotate_tac 2)
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
-apply (metis pflat_len_simps(5))
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv neq_Nil_conv not_less_iff_gr_or_eq pflat_len_simps(9))
-apply(rotate_tac 5)
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv list.distinct(1) list.exhaust not_less_iff_gr_or_eq pflat_len_simps(9))
-apply(auto)
-apply (metis pflat_len_simps(8))
-apply(subgoal_tac "v = va")
-prefer 2
-apply (metis pflat_len_simps(8))
-apply(simp)
-apply(rotate_tac 3)
-apply(drule_tac x="Stars vsa" in meta_spec)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(rule allI)
-apply(case_tac p)
-apply(simp add: pflat_len_simps)
-apply(drule_tac x="[]" in spec)
-apply(simp add: pflat_len_simps intlen_append)
-apply(drule_tac x="Suc a#list" in spec)
-apply(simp add: pflat_len_simps intlen_append)
-apply(simp)
-done
-
-lemma PosOrd_trichotomous_stronger:
- assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
- shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (v1 = v2)"
-oops
+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(induct vs)
-apply(auto)
-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(erule_tac CPrf.cases)
apply(simp_all)
done
@@ -677,11 +598,8 @@
assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r"
using assms
-apply(induct vs1 arbitrary: vs2)
-apply(auto intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(auto intro: CPrf.intros)
+apply(erule_tac CPrf.cases)
+apply(auto intro: CPrf.intros elim: Prf.cases)
done
definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
@@ -697,6 +615,74 @@
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}"
@@ -717,6 +703,7 @@
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
+
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
@@ -845,13 +832,21 @@
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
-by (induct rule: Posix.induct)
- (auto simp add: CPT_def intro: CPrf.intros)
+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 *}
@@ -866,14 +861,14 @@
then have "v = Void"
by (simp add: CPT_simps)
then show "Void :\<sqsubseteq>val v"
- by (simp add: PosOrd_ex1_def)
+ 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_ex1_def)
+ 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
@@ -895,14 +890,14 @@
have "flat v3 = flat v" using as1 Left(3)
by (simp add: Posix1(2))
ultimately have "Left v :\<sqsubseteq>val Left v3"
- by (auto simp add: PosOrd_ex1_def PosOrd_LeftI)
+ 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_ex1_def PosOrd_Left_Right)
+ by (auto simp add: PosOrd_ex_eq_def PosOrd_Left_Right)
then show "Left v :\<sqsubseteq>val v2" unfolding Right .
qed
next
@@ -927,7 +922,7 @@
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_ex1_def PosOrd_RightI)
+ by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
then show "Right v :\<sqsubseteq>val v2" unfolding Right .
next
case (Left v3)
@@ -961,7 +956,7 @@
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_ex1_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2)
+ 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)
@@ -972,13 +967,20 @@
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"
+ 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 []"
- by (force simp add: CPT_def elim: CPrf.cases)
- then show "Stars (v # vs) :\<sqsubseteq>val v3"
+ 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) .
@@ -993,16 +995,16 @@
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_ex1_def by auto
+ unfolding PosOrd_ex_eq_def by auto
then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
- unfolding PosOrd_ex1_def
+ 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_ex1_def using cond2
+ unfolding PosOrd_ex_eq_def using cond2
by (simp add: PosOrd_shorterI)
qed
next
@@ -1011,7 +1013,7 @@
then have "v2 = Stars []"
unfolding CPT_def by (auto elim: CPrf.cases)
then show "Stars [] :\<sqsubseteq>val v2"
- by (simp add: PosOrd_ex1_def)
+ by (simp add: PosOrd_ex_eq_def)
qed
lemma Posix_PosOrd_stronger:
@@ -1030,7 +1032,7 @@
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_ex1_def PosOrd_spreI)
+ by (simp add: PosOrd_ex_eq_def PosOrd_spreI)
}
ultimately show "v1 :\<sqsubseteq>val v2" by blast
qed
@@ -1040,9 +1042,9 @@
shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)"
using assms
by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def
- PosOrd_ex1_def PosOrd_ex_def PosOrd_trans)
+ 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))"
@@ -1115,12 +1117,93 @@
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>v2 \<in> PT r s. \<not> v2 :\<sqsubset>val v1"
+ 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)
@@ -1159,7 +1242,7 @@
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_LeftI by force
+ 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
@@ -1248,10 +1331,7 @@
"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 "Stars vs \<in> CPT (STAR r) (flat (Stars vs))"
- using as2 unfolding eqs .
- moreover
- have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v"
+ 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"
@@ -1266,7 +1346,7 @@
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_Stars)[1]
+ 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)"
@@ -1276,8 +1356,8 @@
PosOrd_StarsI PosOrd_Stars_appendI by auto
qed
with IH
- show "flat v \<in> r \<rightarrow> v" using a as2 unfolding eqs
- using eqs(3) by blast
+ 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)"
@@ -1289,12 +1369,6 @@
apply(auto elim: Prf.cases)
apply(erule Prf.cases)
apply(auto intro: Prf.intros)
- apply(drule_tac x="[]" in meta_spec)
- apply(simp)
- apply(drule meta_mp)
- apply(auto intro: Prf.intros)
- apply(drule_tac x="(v#vsa)" in meta_spec)
- apply(auto intro: Prf.intros)
done
then show "False" using as1 unfolding eqs
apply -
@@ -1302,7 +1376,8 @@
apply(auto simp add: PT_def)
done
qed
- ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
+ 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