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