diff -r f16019b11179 -r e85099ac4c6c thys/Positions.thy
--- a/thys/Positions.thy	Sun Aug 27 00:03:31 2017 +0300
+++ b/thys/Positions.thy	Wed Sep 06 00:52:08 2017 +0100
@@ -134,7 +134,7 @@
   "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)"
 
-lemma test:
+lemma PosOrd_def2:
   shows "v1 \<sqsubset>val p v2 \<longleftrightarrow> 
          pflat_len v1 p > pflat_len v2 p \<and>
          (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and>
@@ -246,9 +246,13 @@
   assumes "v1 :\<sqsubset>val v2" 
   shows "length (flat v2) \<le> length (flat v1)"
 using assms unfolding PosOrd_ex_def PosOrd_def
-apply(auto simp add: pflat_len_def split: if_splits)
-apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le)
-by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear)
+apply(auto)
+apply(case_tac p)
+apply(simp add: pflat_len_simps)
+apply(drule_tac x="[]" in bspec)
+apply(simp add: Pos_empty)
+apply(simp add: pflat_len_simps)
+done
 
 lemma PosOrd_shorterI:
   assumes "length (flat v2) < length (flat v1)"
@@ -271,6 +275,7 @@
 unfolding pflat_len_def
 by (auto split: if_splits)
 
+
 lemma PosOrd_Left_Right:
   assumes "flat v1 = flat v2"
   shows "Left v1 :\<sqsubset>val Right v2" 
@@ -283,7 +288,7 @@
   assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2"
   shows "v1 :\<sqsubset>val v2"
 using assms
-unfolding PosOrd_ex_def test
+unfolding PosOrd_ex_def PosOrd_def2
 apply(auto simp add: pflat_len_simps)
 apply(frule pflat_len_inside)
 apply(auto simp add: pflat_len_simps)
@@ -293,7 +298,7 @@
   assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
   shows  "Left v1 :\<sqsubset>val Left v2"
 using assms
-unfolding PosOrd_ex_def test
+unfolding PosOrd_ex_def PosOrd_def2
 apply(auto simp add: pflat_len_simps)
 by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3))
 
@@ -308,7 +313,7 @@
   assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2"
   shows "v1 :\<sqsubset>val v2"
 using assms
-unfolding PosOrd_ex_def test
+unfolding PosOrd_ex_def PosOrd_def2
 apply(auto simp add: pflat_len_simps)
 apply(frule pflat_len_inside)
 apply(auto simp add: pflat_len_simps)
@@ -318,7 +323,7 @@
   assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
   shows  "Right v1 :\<sqsubset>val Right v2"
 using assms
-unfolding PosOrd_ex_def test
+unfolding PosOrd_ex_def PosOrd_def2
 apply(auto simp add: pflat_len_simps)
 by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5))
 
@@ -331,8 +336,8 @@
 
 
 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'" 
+  assumes "v1 :\<sqsubset>val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)"
+  shows "Seq v1 v2 :\<sqsubset>val Seq w1 w2" 
 using assms(1)
 apply(subst (asm) PosOrd_ex_def)
 apply(subst (asm) PosOrd_def)
@@ -347,14 +352,15 @@
 apply(simp only: Pos.simps)
 apply(auto)[1]
 apply(simp add: pflat_len_simps)
+apply(auto simp add: pflat_len_simps)
 using assms(2)
 apply(simp)
-apply(auto simp add: pflat_len_simps)
-by (metis length_append of_nat_add)
+apply(metis length_append of_nat_add)
+done
 
 lemma PosOrd_SeqI2:
-  assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
-  shows "Seq v v2 :\<sqsubset>val Seq v v2'" 
+  assumes "v2 :\<sqsubset>val w2" "flat v2 = flat w2"
+  shows "Seq v v2 :\<sqsubset>val Seq v w2" 
 using assms(1)
 apply(subst (asm) PosOrd_ex_def)
 apply(subst (asm) PosOrd_def)
@@ -374,47 +380,31 @@
 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
+lemma PosOrd_Seq_eq:
+  assumes "flat v2 = flat w2"
+  shows "(Seq v v2) :\<sqsubset>val (Seq v w2) \<longleftrightarrow> v2 :\<sqsubset>val w2"
+using assms 
+apply(auto)
+prefer 2
+apply(simp add: PosOrd_SeqI2)
 apply(simp add: PosOrd_ex_def)
-apply(erule exE)
+apply(auto)
 apply(case_tac p)
-apply(simp add: PosOrd_def)
-apply(auto simp add: pflat_len_simps)[1]
-apply(rule_tac x="[]" in exI)
-apply(drule_tac x="[]" in spec)
-apply(simp add: Pos_empty pflat_len_simps)
+apply(simp add: PosOrd_def pflat_len_simps)
 apply(case_tac a)
-apply(rule disjI1)
-apply(simp add: PosOrd_def)
-apply(auto simp add: pflat_len_simps)[1]
+apply(simp add: PosOrd_def pflat_len_simps)
+apply(clarify)
+apply(case_tac nat)
+prefer 2
+apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside)
 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)
-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)
+apply(auto simp add: PosOrd_def2 pflat_len_simps)
+apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
+apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2))
 done
 
+
+
 lemma PosOrd_StarsI:
   assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)"
   shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" 
@@ -499,17 +489,17 @@
 done
 
 lemma PosOrd_Stars_append_eq:
-  assumes "flat (Stars vs1) = flat (Stars vs2)"
+  assumes "flats vs1 = flats 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
+done  
 
 lemma PosOrd_almost_trichotomous:
-  shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
+  shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (length (flat v1) = length (flat v2))"
 apply(auto simp add: PosOrd_ex_def)
 apply(auto simp add: PosOrd_def)
 apply(rule_tac x="[]" in exI)
@@ -519,48 +509,6 @@
 done
 
 
-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_def PosOrd_ex_def PosOrd_shorterI PosOrd_assym assms less_linear)
-by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def PosOrd_assym assms of_nat_eq_iff)
-
-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 PosOrd_assym antisym_conv3 append_eq_append_conv assms(2))
-
-
 
 section {* The Posix Value is smaller than any other Value *}
 
@@ -671,8 +619,7 @@
     by (auto simp add: LV_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
-    thm PosOrd_SeqI1 PosOrd_SeqI2
-    unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
+    unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq) 
   then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
 next 
   case (Posix_STAR1 s1 r v s2 vs v3) 
@@ -775,6 +722,16 @@
 
 lemma Least_existence1:
   assumes "LV r s \<noteq> {}"
+  shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v"
+using Least_existence[OF assms] assms
+using PosOrdeq_antisym by blast
+
+
+
+
+
+lemma Least_existence1_pre:
+  assumes "LV r s \<noteq> {}"
   shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v"
 using Least_existence[OF assms] assms
 apply -