61203
|
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 |
|
|
14 |
fun sorted :: "'a::linorder list \<Rightarrow> bool" where
|
|
15 |
"sorted [] = True" |
|
|
16 |
"sorted [x] = True" |
|
|
17 |
"sorted (x#y#zs) = (x < y \<and> sorted(y#zs))"
|
|
18 |
|
|
19 |
lemma sorted_Cons_iff:
|
|
20 |
"sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x < y))"
|
|
21 |
by(induction xs rule: sorted.induct) auto
|
|
22 |
|
|
23 |
lemma sorted_snoc_iff:
|
|
24 |
"sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> set xs. y < x))"
|
|
25 |
by(induction xs rule: sorted.induct) auto
|
|
26 |
|
|
27 |
lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
|
|
28 |
by(simp add: sorted_Cons_iff)
|
|
29 |
|
|
30 |
lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs"
|
|
31 |
by(rule ASSUMPTION_D [THEN sorted_cons])
|
|
32 |
|
|
33 |
lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs"
|
|
34 |
by(simp add: sorted_snoc_iff)
|
|
35 |
|
|
36 |
lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs"
|
|
37 |
by(rule ASSUMPTION_D [THEN sorted_snoc])
|
|
38 |
|
|
39 |
lemma sorted_mid_iff:
|
|
40 |
"sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
|
|
41 |
by(induction xs rule: sorted.induct) auto
|
|
42 |
|
|
43 |
lemma sorted_mid_iff2:
|
|
44 |
"sorted(x # xs @ y # ys) =
|
|
45 |
(sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
|
|
46 |
by(induction xs rule: sorted.induct) auto
|
|
47 |
|
|
48 |
lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow>
|
|
49 |
sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
|
|
50 |
by(rule sorted_mid_iff)
|
|
51 |
|
|
52 |
lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'
|
|
53 |
|
|
54 |
end
|