author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 44890 | 22f665a2e91c |
child 62390 | 842917225d56 |
permissions | -rw-r--r-- |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/Imperative_HOL/ex/Sorted_List.thy |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
3 |
*) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
4 |
|
58889 | 5 |
section {* Sorted lists as representation of finite sets *} |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
6 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
7 |
theory Sorted_List |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
8 |
imports Main |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
9 |
begin |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
10 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
11 |
text {* Merge function for two distinct sorted lists to get compound distinct sorted list *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
12 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
13 |
fun merge :: "('a::linorder) list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
14 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
15 |
"merge (x#xs) (y#ys) = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
16 |
(if x < y then x # merge xs (y#ys) else (if x > y then y # merge (x#xs) ys else x # merge xs ys))" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
17 |
| "merge xs [] = xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
18 |
| "merge [] ys = ys" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
19 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
20 |
text {* The function package does not derive automatically the more general rewrite rule as follows: *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
21 |
lemma merge_Nil[simp]: "merge [] ys = ys" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
22 |
by (cases ys) auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
23 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
24 |
lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
25 |
by (induct xs ys rule: merge.induct, auto) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
26 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
27 |
lemma sorted_merge[simp]: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
28 |
"List.sorted (merge xs ys) = (List.sorted xs \<and> List.sorted ys)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
29 |
by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
30 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
31 |
lemma distinct_merge[simp]: "\<lbrakk> distinct xs; distinct ys; List.sorted xs; List.sorted ys \<rbrakk> \<Longrightarrow> distinct (merge xs ys)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
32 |
by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
33 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
34 |
text {* The remove function removes an element from a sorted list *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
35 |
|
37726 | 36 |
primrec remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
37 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
38 |
"remove a [] = []" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
39 |
| "remove a (x#xs) = (if a > x then (x # remove a xs) else (if a = x then xs else x#xs))" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
40 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
41 |
lemma remove': "sorted xs \<and> distinct xs \<Longrightarrow> sorted (remove a xs) \<and> distinct (remove a xs) \<and> set (remove a xs) = set xs - {a}" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
42 |
apply (induct xs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
43 |
apply (auto simp add: sorted_Cons) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
44 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
45 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
46 |
lemma set_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> set (remove a xs) = set xs - {a}" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
47 |
using remove' by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
48 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
49 |
lemma sorted_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> sorted (remove a xs)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
50 |
using remove' by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
51 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
52 |
lemma distinct_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> distinct (remove a xs)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
53 |
using remove' by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
54 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
55 |
lemma remove_insort_cancel: "remove a (insort a xs) = xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
56 |
apply (induct xs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
57 |
apply simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
58 |
apply auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
59 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
60 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
61 |
lemma remove_insort_commute: "\<lbrakk> a \<noteq> b; sorted xs \<rbrakk> \<Longrightarrow> remove b (insort a xs) = insort a (remove b xs)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
62 |
apply (induct xs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
63 |
apply auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
64 |
apply (auto simp add: sorted_Cons) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
65 |
apply (case_tac xs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
66 |
apply auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
67 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
68 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
69 |
lemma notinset_remove: "x \<notin> set xs \<Longrightarrow> remove x xs = xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
70 |
apply (induct xs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
71 |
apply auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
72 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
73 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
74 |
lemma remove1_eq_remove: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
75 |
"sorted xs \<Longrightarrow> distinct xs \<Longrightarrow> remove1 x xs = remove x xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
76 |
apply (induct xs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
77 |
apply (auto simp add: sorted_Cons) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
78 |
apply (subgoal_tac "x \<notin> set xs") |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
79 |
apply (simp add: notinset_remove) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
37726
diff
changeset
|
80 |
apply fastforce |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
81 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
82 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
83 |
lemma sorted_remove1: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
84 |
"sorted xs \<Longrightarrow> sorted (remove1 x xs)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
85 |
apply (induct xs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
86 |
apply (auto simp add: sorted_Cons) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
87 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
88 |
|
37726 | 89 |
subsection {* Efficient member function for sorted lists *} |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
90 |
|
37726 | 91 |
primrec smember :: "'a list \<Rightarrow> 'a::linorder \<Rightarrow> bool" where |
92 |
"smember [] x \<longleftrightarrow> False" |
|
93 |
| "smember (y#ys) x \<longleftrightarrow> x = y \<or> (x > y \<and> smember ys x)" |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
94 |
|
37726 | 95 |
lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)" |
96 |
by (induct xs) (auto simp add: sorted_Cons) |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
97 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
98 |
end |