1(* Author: Tobias Nipkow *)
2
3section \<open>Lists Sorted wrt $<$\<close>
4
5theory Sorted_Less
6imports Less_False
7begin
8
9hide_const sorted
10
11text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?.\<close>
12
13abbreviation sorted :: "'a::linorder list \<Rightarrow> bool" where
14"sorted \<equiv> sorted_wrt (<)"
15
16lemmas sorted_wrt_Cons = sorted_wrt.simps(2)
17
18text \<open>The definition of @{const sorted_wrt} relates each element to all the elements after it.
19This causes a blowup of the formulas. Thus we simplify matters by only comparing adjacent elements.\<close>
20
21declare
22  sorted_wrt.simps(2)[simp del]
23  sorted_wrt1[simp] sorted_wrt2[OF transp_less, simp]
24
25lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
26by(simp add: sorted_wrt_Cons)
27
28lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs"
29by(rule ASSUMPTION_D [THEN sorted_cons])
30
31lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs"
32by(simp add: sorted_wrt_append)
33
34lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs"
35by(rule ASSUMPTION_D [THEN sorted_snoc])
36
37lemma sorted_mid_iff:
38  "sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
39by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)
40
41lemma sorted_mid_iff2:
42  "sorted(x # xs @ y # ys) =
43  (sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
44by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)
45
46lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow>
47  sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
48by(rule sorted_mid_iff)
49
50lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'
51
52text\<open>Splay trees need two additional @{const sorted} lemmas:\<close>
53
54lemma sorted_snoc_le:
55  "ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
56by (auto simp add: sorted_wrt_append ASSUMPTION_def)
57
58lemma sorted_Cons_le:
59  "ASSUMPTION(sorted(x # xs)) \<Longrightarrow> y \<le> x \<Longrightarrow> sorted (y # xs)"
60by (auto simp add: sorted_wrt_Cons ASSUMPTION_def)
61
62end
63