--- 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"
--- 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"
--- 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
--- 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)
--- 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>