61640
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section {* Lists Sorted wrt $<$ *}
|
|
4 |
|
|
5 |
theory Sorted_Less
|
|
6 |
imports Less_False
|
|
7 |
begin
|
|
8 |
|
|
9 |
hide_const sorted
|
|
10 |
|
|
11 |
text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?
|
|
12 |
Could go into theory List under a name like @{term sorted_less}.\<close>
|
|
13 |
|
66441
|
14 |
abbreviation sorted :: "'a::linorder list \<Rightarrow> bool" where
|
|
15 |
"sorted \<equiv> sorted_wrt (op <)"
|
61640
|
16 |
|
|
17 |
lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
|
66441
|
18 |
by(simp add: sorted_wrt_Cons)
|
61640
|
19 |
|
|
20 |
lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs"
|
|
21 |
by(rule ASSUMPTION_D [THEN sorted_cons])
|
|
22 |
|
|
23 |
lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs"
|
66441
|
24 |
by(simp add: sorted_wrt_append)
|
61640
|
25 |
|
|
26 |
lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs"
|
|
27 |
by(rule ASSUMPTION_D [THEN sorted_snoc])
|
|
28 |
|
|
29 |
lemma sorted_mid_iff:
|
|
30 |
"sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
|
66441
|
31 |
by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)
|
61640
|
32 |
|
|
33 |
lemma sorted_mid_iff2:
|
|
34 |
"sorted(x # xs @ y # ys) =
|
|
35 |
(sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
|
66441
|
36 |
by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)
|
61640
|
37 |
|
|
38 |
lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow>
|
|
39 |
sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
|
|
40 |
by(rule sorted_mid_iff)
|
|
41 |
|
|
42 |
lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'
|
|
43 |
|
61696
|
44 |
text\<open>Splay trees need two additional @{const sorted} lemmas:\<close>
|
|
45 |
|
|
46 |
lemma sorted_snoc_le:
|
|
47 |
"ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
|
66441
|
48 |
by (auto simp add: sorted_wrt_append ASSUMPTION_def)
|
61696
|
49 |
|
|
50 |
lemma sorted_Cons_le:
|
|
51 |
"ASSUMPTION(sorted(x # xs)) \<Longrightarrow> y \<le> x \<Longrightarrow> sorted (y # xs)"
|
66441
|
52 |
by (auto simp add: sorted_wrt_Cons ASSUMPTION_def)
|
61696
|
53 |
|
61640
|
54 |
end
|