diff -r 00c9a95d492e -r e2828c4a1e23 thys/Positions.thy
--- 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 *}