diff -r 146b4817aebd -r 9deaff82e0c5 thys/Positions.thy
--- a/thys/Positions.thy	Thu Jun 29 17:57:41 2017 +0100
+++ b/thys/Positions.thy	Fri Jun 30 17:41:45 2017 +0100
@@ -61,30 +61,9 @@
 apply(case_tac ys)
 apply(simp_all)
 apply (smt intlen_bigger)
-(* HERE *)
-oops
-
-
-lemma intlen_length:
-  assumes "length xs < length ys"
-  shows "intlen xs < intlen ys"
-using assms
-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)
 by (smt Suc_lessE intlen.simps(2) length_Suc_conv)
 
-lemma length_intlen:
-  assumes "intlen xs < intlen ys"
-  shows "length xs < length ys"
-using assms
-apply(induct xs arbitrary: ys)
-apply(auto)
-apply(case_tac ys)
-apply(simp_all)
-by (smt intlen_bigger)
 
 
 definition pflat_len :: "val \<Rightarrow> nat list => int"
@@ -120,15 +99,15 @@
 section {* Orderings *}
 
 
-definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _")
+definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
 where
   "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2"
 
-definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _")
+definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60)
 where
   "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2"
 
-inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
+inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60)
 where
   "[] \<sqsubset>lex (p#ps)"
 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
@@ -139,9 +118,8 @@
   assumes "ps1 \<sqsubset>lex ps2"
   shows "ps1 \<noteq> ps2"
 using assms
-apply(induct rule: lex_list.induct)
-apply(auto)
-done
+by(induct rule: lex_list.induct)(auto)
+
 
 lemma lex_simps [simp]:
   fixes xs ys :: "nat list"
@@ -169,8 +147,7 @@
 apply(simp_all)
 done
 
-
-lemma trichotomous:
+lemma lex_trichotomous:
   fixes p q :: "nat list"
   shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
 apply(induct p arbitrary: q)
@@ -196,9 +173,6 @@
 where
   "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"
 
-
-
-
 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _")
 where
   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
@@ -210,7 +184,7 @@
 apply(auto simp add: val_ord_ex_def val_ord_def)
 apply(case_tac p)
 apply(simp add: pflat_len_simps)
-apply(drule length_intlen)
+apply(simp add: intlen_length)
 apply(simp)
 apply(drule_tac x="[]" in bspec)
 apply(simp add: Pos_empty)
@@ -493,7 +467,7 @@
 apply(clarify)
 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p")
 prefer 2
-apply(rule trichotomous)
+apply(rule lex_trichotomous)
 apply(erule disjE)
 apply(simp)
 apply(rule_tac x="pa" in exI)
@@ -885,7 +859,7 @@
 apply(simp (no_asm) add: val_ord_def)
 apply(rule_tac x="[]" in exI)
 apply(simp add: pflat_len_simps)
-apply(rule intlen_length)
+apply(simp only: intlen_length)
 apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le)
 apply(subgoal_tac "length (flat v1a) \<le> length s1")
 prefer 2