# HG changeset patch
# User nipkow
# Date 1502910851 -7200
# Node ID b9468503742a13c4d761de82d2dbc63219a735ff
# Parent  a6ec6c806a6c3a296bb0b7dd71ca4628a6dfa79b
more reorganization around sorted_wrt

diff -r a6ec6c806a6c -r b9468503742a src/HOL/Data_Structures/AList_Upd_Del.thy
--- a/src/HOL/Data_Structures/AList_Upd_Del.thy	Tue Aug 15 22:22:34 2017 +0100
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Wed Aug 16 21:14:11 2017 +0200
@@ -40,7 +40,7 @@
 by(induction ps)(auto)
 
 lemma map_of_None: "sorted (x # map fst ps) \<Longrightarrow> map_of ps x = None"
-by (induction ps) (auto simp: sorted_lems sorted_Cons_iff)
+by (induction ps) (fastforce simp: sorted_lems sorted_wrt_Cons)+
 
 lemma map_of_None2: "sorted (map fst ps @ [x]) \<Longrightarrow> map_of ps x = None"
 by (induction ps) (auto simp: sorted_lems)
@@ -51,11 +51,11 @@
 
 lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow>
    map_of ps x = None"
-by (meson less_trans map_of_None sorted_Cons_iff)
+by (simp add: map_of_None sorted_Cons_le)
 
 lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
   map_of ps x = None"
-by (meson le_less_trans map_of_None2 not_less sorted_snoc_iff)
+by (simp add: map_of_None2 sorted_snoc_le)
 
 lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc
 lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds
@@ -106,8 +106,8 @@
 apply(induction ps)
  apply simp
 apply(case_tac ps)
-apply auto
-by (meson order.strict_trans sorted_Cons_iff)
+apply (auto simp: sorted_Cons_le)
+done
 
 lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs"
 by (induct xs) auto
@@ -117,7 +117,7 @@
     (if x < a then del_list x ps @ (a,b) # qs
      else ps @ del_list x ((a,b) # qs))"
 by(induction ps)
-  (fastforce simp: sorted_lems sorted_Cons_iff intro!: del_list_idem)+
+  (fastforce simp: sorted_lems sorted_wrt_Cons intro!: del_list_idem)+
 
 text\<open>In principle, @{thm del_list_sorted} suffices, but the following
 corollaries speed up proofs.\<close>
@@ -156,7 +156,7 @@
 text\<open>Splay trees need two additional @{const del_list} lemmas:\<close>
 
 lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs"
-by(induction xs)(auto simp: sorted_Cons_iff)
+by(induction xs)(fastforce simp: sorted_wrt_Cons)+
 
 lemma del_list_sorted_app:
   "sorted(map fst xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
diff -r a6ec6c806a6c -r b9468503742a src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Tue Aug 15 22:22:34 2017 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Wed Aug 16 21:14:11 2017 +0200
@@ -19,12 +19,12 @@
 by (induction xs) auto
 
 lemma sorted_Cons_iff:
-  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> elems xs. x < y))"
-by(simp add: elems_eq_set Sorted_Less.sorted_Cons_iff)
+  "sorted(x # xs) = ((\<forall>y \<in> elems xs. x < y) \<and> sorted xs)"
+by(simp add: elems_eq_set sorted_wrt_Cons)
 
 lemma sorted_snoc_iff:
   "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
-by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff)
+by(simp add: elems_eq_set sorted_wrt_append)
 
 text{* The above two rules introduce quantifiers. It turns out
 that in practice this is not a problem because of the simplicity of
@@ -53,12 +53,12 @@
 by(induction xs) auto
 
 lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
-apply(induction xs rule: sorted.induct)
+apply(induction xs rule: sorted_wrt_induct)
 apply auto
 by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
 
 lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
-by(induction xs rule: sorted.induct) auto
+by(induction xs rule: sorted_wrt_induct) auto
 
 lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow>
   ins_list x (xs @ a # ys) =
@@ -105,7 +105,7 @@
 done
 
 lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
-apply(induction xs rule: sorted.induct)
+apply(induction xs rule: sorted_wrt_induct)
 apply auto
 by (meson order.strict_trans sorted_Cons_iff)
 
@@ -151,7 +151,7 @@
 text\<open>Splay trees need two additional @{const del_list} lemmas:\<close>
 
 lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs"
-by(induction xs)(auto simp: sorted_Cons_iff)
+by(induction xs)(fastforce simp: sorted_Cons_iff)+
 
 lemma del_list_sorted_app:
   "sorted(xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
diff -r a6ec6c806a6c -r b9468503742a src/HOL/Data_Structures/Sorted_Less.thy
--- a/src/HOL/Data_Structures/Sorted_Less.thy	Tue Aug 15 22:22:34 2017 +0100
+++ b/src/HOL/Data_Structures/Sorted_Less.thy	Wed Aug 16 21:14:11 2017 +0200
@@ -11,39 +11,29 @@
 text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?
 Could go into theory List under a name like @{term sorted_less}.\<close>
 
-fun sorted :: "'a::linorder list \<Rightarrow> bool" where
-"sorted [] = True" |
-"sorted [x] = True" |
-"sorted (x#y#zs) = (x < y \<and> sorted(y#zs))"
-
-lemma sorted_Cons_iff:
-  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x < y))"
-by(induction xs rule: sorted.induct) auto
-
-lemma sorted_snoc_iff:
-  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> set xs. y < x))"
-by(induction xs rule: sorted.induct) auto
+abbreviation sorted :: "'a::linorder list \<Rightarrow> bool" where
+"sorted \<equiv> sorted_wrt (op <)"
 
 lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
-by(simp add: sorted_Cons_iff)
+by(simp add: sorted_wrt_Cons)
 
 lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs"
 by(rule ASSUMPTION_D [THEN sorted_cons])
 
 lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs"
-by(simp add: sorted_snoc_iff)
+by(simp add: sorted_wrt_append)
 
 lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs"
 by(rule ASSUMPTION_D [THEN sorted_snoc])
 
 lemma sorted_mid_iff:
   "sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
-by(induction xs rule: sorted.induct) auto
+by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)
 
 lemma sorted_mid_iff2:
   "sorted(x # xs @ y # ys) =
   (sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
-by(induction xs rule: sorted.induct) auto
+by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)
 
 lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow>
   sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
@@ -55,10 +45,10 @@
 
 lemma sorted_snoc_le:
   "ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
-by (auto simp add: Sorted_Less.sorted_snoc_iff ASSUMPTION_def)
+by (auto simp add: sorted_wrt_append ASSUMPTION_def)
 
 lemma sorted_Cons_le:
   "ASSUMPTION(sorted(x # xs)) \<Longrightarrow> y \<le> x \<Longrightarrow> sorted (y # xs)"
-by (auto simp add: Sorted_Less.sorted_Cons_iff ASSUMPTION_def)
+by (auto simp add: sorted_wrt_Cons ASSUMPTION_def)
 
 end
diff -r a6ec6c806a6c -r b9468503742a src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 15 22:22:34 2017 +0100
+++ b/src/HOL/List.thy	Wed Aug 16 21:14:11 2017 +0200
@@ -4915,6 +4915,14 @@
  apply simp
 by simp (blast intro: order_trans)
 
+lemma sorted_iff_wrt: "sorted xs = sorted_wrt (op \<le>) xs"
+proof
+  assume "sorted xs" thus "sorted_wrt (op \<le>) xs"
+  proof (induct xs rule: sorted.induct)
+    case (Cons xs x) thus ?case by (cases xs) simp_all
+  qed simp
+qed (induct xs rule: sorted_wrt_induct, simp_all)
+
 lemma sorted_tl:
   "sorted xs \<Longrightarrow> sorted (tl xs)"
 by (cases xs) (simp_all add: sorted_Cons)
diff -r a6ec6c806a6c -r b9468503742a src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Aug 15 22:22:34 2017 +0100
+++ b/src/HOL/Relation.thy	Wed Aug 16 21:14:11 2017 +0200
@@ -438,18 +438,22 @@
 lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
   by (simp add: transp_def)
 
-lemma transp_le[simp]: "transp (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
-by(auto simp add: transp_def)
+context preorder
+begin
 
-lemma transp_less[simp]: "transp (op < :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
-by(auto simp add: transp_def)
+lemma transp_le[simp]: "transp (op \<le>)"
+by(auto simp add: transp_def intro: order_trans)
 
-lemma transp_ge[simp]: "transp (op \<ge> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
-by(auto simp add: transp_def)
+lemma transp_less[simp]: "transp (op <)"
+by(auto simp add: transp_def intro: less_trans)
 
-lemma transp_gr[simp]: "transp (op > :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
-by(auto simp add: transp_def)
+lemma transp_ge[simp]: "transp (op \<ge>)"
+by(auto simp add: transp_def intro: order_trans)
 
+lemma transp_gr[simp]: "transp (op >)"
+by(auto simp add: transp_def intro: less_trans)
+
+end
 
 subsubsection \<open>Totality\<close>