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