--- a/thys/Positions.thy Tue Jul 04 18:09:29 2017 +0100
+++ b/thys/Positions.thy Thu Jul 06 16:05:33 2017 +0100
@@ -57,15 +57,12 @@
lemma intlen_length:
shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
apply(induct xs arbitrary: ys)
-apply(auto)
-apply(case_tac ys)
-apply(simp_all)
-apply (smt intlen_bigger)
-apply (smt Suc_mono intlen.simps(2) length_Suc_conv less_antisym)
+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)
-
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)"
@@ -120,32 +117,23 @@
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> (\<not> y < x \<and> xs \<sqsubset>lex ys))"
-apply -
-apply (metis lex_irrfl lex_list.intros(1) list.exhaust)
-using lex_list.cases apply blast
-using lex_list.cases lex_list.intros(2) lex_list.intros(3) not_less_iff_gr_or_eq by fastforce
-
+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
lemma lex_trans:
fixes ps1 ps2 ps3 :: "nat list"
assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
shows "ps1 \<sqsubset>lex ps3"
using assms
-apply(induct arbitrary: ps3 rule: lex_list.induct)
-apply(erule lex_list.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule lex_list.cases)
-apply(simp_all)
-apply(erule lex_list.cases)
-apply(simp_all)
-done
+by (induct arbitrary: ps3 rule: lex_list.induct)
+ (auto elim: lex_list.cases)
+
lemma lex_trichotomous:
fixes p q :: "nat list"
@@ -164,10 +152,24 @@
definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
where
- "v1 \<sqsubset>val p v2 \<equiv> p \<in> Pos v1 \<and>
+ "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)
+
+
+(* some tests *)
+
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>
@@ -197,7 +199,7 @@
using assms
unfolding ValFlat_ord_def PosOrd_def
apply(clarify)
-done
+oops
definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
@@ -228,7 +230,7 @@
shows "v :\<sqsubset>val v'"
using assms
unfolding PosOrd_ex_def
-by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
+by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
lemma PosOrd_spreI:
assumes "(flat v') \<sqsubset>spre (flat v)"
@@ -243,7 +245,7 @@
unfolding PosOrd_ex_def
apply(rule_tac x="[0]" in exI)
using assms
-apply(auto simp add: PosOrd_def pflat_len_simps Pos_empty)
+apply(auto simp add: PosOrd_def pflat_len_simps)
apply(smt intlen_bigger)
done
@@ -275,13 +277,15 @@
using assms
apply(simp add: PosOrd_ex_def)
apply(erule exE)
-apply(case_tac "p = []")
+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(rule_tac x="ps" in exI)
+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)
@@ -289,6 +293,7 @@
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:
@@ -297,13 +302,18 @@
using assms
apply(simp add: PosOrd_ex_def)
apply(erule exE)
-apply(case_tac "p = []")
+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="ps" in exI)
+apply(rule_tac x="list" in exI)
apply(auto)
apply(drule_tac x="Suc 0#q" in bspec)
apply(simp)
@@ -325,8 +335,6 @@
apply(rule_tac x="0#p" in exI)
apply(subst PosOrd_def)
apply(rule conjI)
-apply(simp)
-apply(rule conjI)
apply(simp add: pflat_len_simps)
apply(rule ballI)
apply(rule impI)
@@ -349,8 +357,6 @@
apply(rule_tac x="Suc 0#p" in exI)
apply(subst PosOrd_def)
apply(rule conjI)
-apply(simp)
-apply(rule conjI)
apply(simp add: pflat_len_simps)
apply(rule ballI)
apply(rule impI)
@@ -393,10 +399,14 @@
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(simp add: PosOrd_def)
+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:
@@ -459,7 +469,7 @@
apply(simp)
apply(case_tac a)
apply(clarify)
-apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def)[1]
+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)
@@ -497,43 +507,41 @@
apply(auto)
done
-
lemma PosOrd_trans:
assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
shows "v1 :\<sqsubset>val v3"
-using assms
-unfolding PosOrd_ex_def
-apply(clarify)
-apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p")
-prefer 2
-apply(rule lex_trichotomous)
-apply(erule disjE)
-apply(simp)
-apply(rule_tac x="pa" in exI)
-apply(subst PosOrd_def)
-apply(rule conjI)
-apply(simp add: PosOrd_def)
-apply(auto)[1]
-apply(simp add: PosOrd_def)
-apply(simp add: PosOrd_def)
-apply(auto)[1]
-using outside_lemma apply blast
-apply(simp add: PosOrd_def)
-apply(auto)[1]
-using outside_lemma apply force
-apply auto[1]
-apply(simp add: PosOrd_def)
-apply(auto)[1]
-apply (metis (no_types, hide_lams) lex_trans outside_lemma)
-apply(simp add: PosOrd_def)
-apply(auto)[1]
-by (smt intlen_bigger lex_trans outside_lemma pflat_len_def)
+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
+ by (smt outside_lemma)
+ 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)
+ 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
-by(auto simp add: PosOrd_ex_def PosOrd_def)
+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))"
@@ -550,7 +558,7 @@
shows "False"
using assms
apply(auto simp add: PosOrd_ex_def PosOrd_def)
-using assms(1) assms(2) PosOrd_irrefl PosOrd_trans by blast
+using assms PosOrd_irrefl PosOrd_trans by blast
lemma WW2:
assumes "\<not>(v1 :\<sqsubset>val v2)"
@@ -842,29 +850,8 @@
assumes "s \<in> r \<rightarrow> v"
shows "v \<in> CPT r s"
using assms
-apply(induct rule: Posix.induct)
-apply(simp add: CPT_def)
-apply(rule CPrf.intros)
-apply(simp add: CPT_def)
-apply(rule CPrf.intros)
-apply(simp add: CPT_def)
-apply(rule CPrf.intros)
-apply(simp)
-apply(simp add: CPT_def)
-apply(rule CPrf.intros)
-apply(simp)
-apply(simp add: CPT_def)
-apply(rule CPrf.intros)
-apply(simp)
-apply(simp)
-apply(simp add: CPT_def)
-apply(rule CPrf.intros)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp add: CPT_def)
-apply(rule CPrf.intros)
-done
+by (induct rule: Posix.induct)
+ (auto simp add: CPT_def intro: CPrf.intros)
section {* The Posix Value is smaller than any other Value *}
@@ -954,7 +941,8 @@
qed
next
case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
- have as1: "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
+ 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
@@ -968,17 +956,17 @@
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 Posix1(2) as1(1) eqs by blast
+ 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_ex1_def
- by (metis PosOrd_SeqI1 PosOrd_SeqI2 Posix1(2) flat.simps(5))
+ unfolding PosOrd_ex1_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 as1: "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
+ 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
@@ -1000,13 +988,15 @@
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 Posix1(2) as1(1) NonEmpty(4) by blast
+ 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 :\<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
then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
unfolding PosOrd_ex1_def
- by (metis PosOrd_StarsI PosOrd_StarsI2 Posix1(2) flat.simps(7) val.inject(5))
+ 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
@@ -1032,7 +1022,8 @@
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)
+ with assms(1)
+ have "v1 :\<sqsubseteq>val v2" by (rule Posix_PosOrd)
}
moreover
{ assume "flat v2 \<sqsubset>spre s"
@@ -1074,7 +1065,7 @@
apply(auto simp add: CPT_def PT_def)[1]
apply(erule Prf.cases)
apply(simp_all)
-apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_PosOrd_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25))
+using CPrf_stars PosOrd_irrefl apply fastforce
apply(clarify)
apply(drule_tac x="Stars (a#v#vsa)" in spec)
apply(simp)
@@ -1123,23 +1114,7 @@
apply(subst (asm) (2) PosOrd_ex_def)
apply(simp)
apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def)
-proof -
- fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list"
- assume a1: "s\<^sub>3 \<noteq> []"
- assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)"
- assume a3: "flat vA = flat a @ s\<^sub>3"
- assume a4: "\<forall>p. \<not> (Stars (vA # vB) \<sqsubset>val p (Stars (a # vsa)))"
- have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs"
- by (meson drop_eq_Nil not_less)
- have f6: "\<not> length (flat vA) \<le> length (flat a)"
- using a3 a1 by simp
- have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))"
- using a3 a2 by simp
- then show False
- using f6 f5 a4 by (metis (full_types) drop_eq_Nil PosOrd_StarsI PosOrd_ex_def PosOrd_shorterI)
-qed
-
-
+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)
section {* The Smallest Value is indeed the Posix Value *}