diff -r 6746f5e1f1f8 -r 12772d537b71 thys/Positions.thy
--- a/thys/Positions.thy	Fri Aug 18 14:51:29 2017 +0100
+++ b/thys/Positions.thy	Fri Aug 25 15:05:20 2017 +0200
@@ -38,6 +38,7 @@
   shows "[] \<in> Pos v"
 by (induct v rule: Pos.induct)(auto)
 
+
 abbreviation
   "intlen vs \<equiv> int (length vs)"
 
@@ -133,6 +134,14 @@
   "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:
+  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>
+         (\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
+unfolding PosOrd_def
+apply(auto)
+done
 
 
 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
@@ -233,8 +242,6 @@
 by auto
 
 
-
-
 lemma PosOrd_shorterE:
   assumes "v1 :\<sqsubset>val v2" 
   shows "length (flat v2) \<le> length (flat v1)"
@@ -257,73 +264,70 @@
 unfolding prefix_list_def sprefix_list_def
 by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear)
 
+lemma pflat_len_inside:
+  assumes "pflat_len v2 p < pflat_len v1 p"
+  shows "p \<in> Pos v1"
+using assms 
+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" 
 unfolding PosOrd_ex_def
 apply(rule_tac x="[0]" in exI)
-using assms 
-apply(auto simp add: PosOrd_def pflat_len_simps)
+apply(auto simp add: PosOrd_def pflat_len_simps assms)
 done
 
+lemma PosOrd_LeftE:
+  assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2"
+  shows "v1 :\<sqsubset>val v2"
+using assms
+unfolding PosOrd_ex_def test
+apply(auto simp add: pflat_len_simps)
+apply(frule pflat_len_inside)
+apply(auto simp add: pflat_len_simps)
+by (metis lex_simps(3) pflat_len_simps(3))
+
+lemma PosOrd_LeftI:
+  assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
+  shows  "Left v1 :\<sqsubset>val Left v2"
+using assms
+unfolding PosOrd_ex_def test
+apply(auto simp add: pflat_len_simps)
+by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3))
+
 lemma PosOrd_Left_eq:
-  assumes "flat v = flat v'"
-  shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" 
+  assumes "flat v1 = flat v2"
+  shows "Left v1 :\<sqsubset>val Left v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" 
+using assms PosOrd_LeftE PosOrd_LeftI
+by blast
+
+
+lemma PosOrd_RightE:
+  assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2"
+  shows "v1 :\<sqsubset>val v2"
 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
-
+unfolding PosOrd_ex_def test
+apply(auto simp add: pflat_len_simps)
+apply(frule pflat_len_inside)
+apply(auto simp add: pflat_len_simps)
+by (metis lex_simps(3) pflat_len_simps(5))
 
 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"
+  assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2"
+  shows  "Right v1 :\<sqsubset>val Right v2"
 using assms
-apply(simp add: PosOrd_ex_def)
-apply(erule exE)
-apply(case_tac p)
-apply(simp add: PosOrd_def)
+unfolding PosOrd_ex_def test
 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
+by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5))
+
+
+lemma PosOrd_Right_eq:
+  assumes "flat v1 = flat v2"
+  shows "Right v1 :\<sqsubset>val Right v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" 
+using assms PosOrd_RightE PosOrd_RightI
+by blast
 
 
 lemma PosOrd_SeqI1: