src/HOL/Imperative_HOL/ex/Sorted_List.thy
 author haftmann Fri Jul 23 10:58:13 2010 +0200 (2010-07-23) changeset 37947 844977c7abeb parent 37726 17b05b104390 child 44890 22f665a2e91c permissions -rw-r--r--
```     1 (*  Title:      HOL/Imperative_HOL/ex/Sorted_List.thy
```
```     2     Author:     Lukas Bulwahn, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Sorted lists as representation of finite sets *}
```
```     6
```
```     7 theory Sorted_List
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 text {* Merge function for two distinct sorted lists to get compound distinct sorted list *}
```
```    12
```
```    13 fun merge :: "('a::linorder) list \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```    14 where
```
```    15   "merge (x#xs) (y#ys) =
```
```    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))"
```
```    17 | "merge xs [] = xs"
```
```    18 | "merge [] ys = ys"
```
```    19
```
```    20 text {* The function package does not derive automatically the more general rewrite rule as follows: *}
```
```    21 lemma merge_Nil[simp]: "merge [] ys = ys"
```
```    22 by (cases ys) auto
```
```    23
```
```    24 lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
```
```    25 by (induct xs ys rule: merge.induct, auto)
```
```    26
```
```    27 lemma sorted_merge[simp]:
```
```    28      "List.sorted (merge xs ys) = (List.sorted xs \<and> List.sorted ys)"
```
```    29 by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons)
```
```    30
```
```    31 lemma distinct_merge[simp]: "\<lbrakk> distinct xs; distinct ys; List.sorted xs; List.sorted ys \<rbrakk> \<Longrightarrow> distinct (merge xs ys)"
```
```    32 by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons)
```
```    33
```
```    34 text {* The remove function removes an element from a sorted list *}
```
```    35
```
```    36 primrec remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```    37 where
```
```    38   "remove a [] = []"
```
```    39   |  "remove a (x#xs) = (if a > x then (x # remove a xs) else (if a = x then xs else x#xs))"
```
```    40
```
```    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}"
```
```    42 apply (induct xs)
```
```    43 apply (auto simp add: sorted_Cons)
```
```    44 done
```
```    45
```
```    46 lemma set_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> set (remove a xs) = set xs - {a}"
```
```    47 using remove' by auto
```
```    48
```
```    49 lemma sorted_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> sorted (remove a xs)"
```
```    50 using remove' by auto
```
```    51
```
```    52 lemma distinct_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> distinct (remove a xs)"
```
```    53 using remove' by auto
```
```    54
```
```    55 lemma remove_insort_cancel: "remove a (insort a xs) = xs"
```
```    56 apply (induct xs)
```
```    57 apply simp
```
```    58 apply auto
```
```    59 done
```
```    60
```
```    61 lemma remove_insort_commute: "\<lbrakk> a \<noteq> b; sorted xs \<rbrakk> \<Longrightarrow> remove b (insort a xs) = insort a (remove b xs)"
```
```    62 apply (induct xs)
```
```    63 apply auto
```
```    64 apply (auto simp add: sorted_Cons)
```
```    65 apply (case_tac xs)
```
```    66 apply auto
```
```    67 done
```
```    68
```
```    69 lemma notinset_remove: "x \<notin> set xs \<Longrightarrow> remove x xs = xs"
```
```    70 apply (induct xs)
```
```    71 apply auto
```
```    72 done
```
```    73
```
```    74 lemma remove1_eq_remove:
```
```    75   "sorted xs \<Longrightarrow> distinct xs \<Longrightarrow> remove1 x xs = remove x xs"
```
```    76 apply (induct xs)
```
```    77 apply (auto simp add: sorted_Cons)
```
```    78 apply (subgoal_tac "x \<notin> set xs")
```
```    79 apply (simp add: notinset_remove)
```
```    80 apply fastsimp
```
```    81 done
```
```    82
```
```    83 lemma sorted_remove1:
```
```    84   "sorted xs \<Longrightarrow> sorted (remove1 x xs)"
```
```    85 apply (induct xs)
```
```    86 apply (auto simp add: sorted_Cons)
```
```    87 done
```
```    88
```
```    89 subsection {* Efficient member function for sorted lists *}
```
```    90
```
```    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)"
```
```    94
```
```    95 lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)"
```
```    96   by (induct xs) (auto simp add: sorted_Cons)
```
```    97
```
`    98 end`