equal
deleted
inserted
replaced
31 lemma distinct_merge[simp]: "\<lbrakk> distinct xs; distinct ys; List.sorted xs; List.sorted ys \<rbrakk> \<Longrightarrow> distinct (merge xs ys)" |
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) |
32 by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons) |
33 |
33 |
34 text {* The remove function removes an element from a sorted list *} |
34 text {* The remove function removes an element from a sorted list *} |
35 |
35 |
36 fun remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
36 primrec remove :: "('a :: linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
37 where |
37 where |
38 "remove a [] = []" |
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))" |
39 | "remove a (x#xs) = (if a > x then (x # remove a xs) else (if a = x then xs else x#xs))" |
40 |
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}" |
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}" |
84 "sorted xs \<Longrightarrow> sorted (remove1 x xs)" |
84 "sorted xs \<Longrightarrow> sorted (remove1 x xs)" |
85 apply (induct xs) |
85 apply (induct xs) |
86 apply (auto simp add: sorted_Cons) |
86 apply (auto simp add: sorted_Cons) |
87 done |
87 done |
88 |
88 |
89 subsection {* Efficient member function for sorted lists: smem *} |
89 subsection {* Efficient member function for sorted lists *} |
90 |
90 |
91 fun smember :: "('a::linorder) \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "smem" 55) |
91 primrec smember :: "'a list \<Rightarrow> 'a::linorder \<Rightarrow> bool" where |
92 where |
92 "smember [] x \<longleftrightarrow> False" |
93 "x smem [] = False" |
93 | "smember (y#ys) x \<longleftrightarrow> x = y \<or> (x > y \<and> smember ys x)" |
94 | "x smem (y#ys) = (if x = y then True else (if (x > y) then x smem ys else False))" |
|
95 |
94 |
96 lemma "sorted xs \<Longrightarrow> x smem xs = (x \<in> set xs)" |
95 lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)" |
97 apply (induct xs) |
96 by (induct xs) (auto simp add: sorted_Cons) |
98 apply (auto simp add: sorted_Cons) |
|
99 done |
|
100 |
97 |
101 end |
98 end |