summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Imperative_HOL/ex/Sorted_List.thy

author | huffman |

Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) | |

changeset 47255 | 30a1692557b0 |

parent 44890 | 22f665a2e91c |

child 58889 | 5b7a9633cfa8 |

permissions | -rw-r--r-- |

removed Nat_Numeral.thy, moving all theorems elsewhere

1 (* Title: HOL/Imperative_HOL/ex/Sorted_List.thy

2 Author: Lukas Bulwahn, TU Muenchen

3 *)

5 header {* Sorted lists as representation of finite sets *}

7 theory Sorted_List

8 imports Main

9 begin

11 text {* Merge function for two distinct sorted lists to get compound distinct sorted list *}

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"

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

24 lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"

25 by (induct xs ys rule: merge.induct, auto)

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)

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)

34 text {* The remove function removes an element from a sorted list *}

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

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

46 lemma set_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> set (remove a xs) = set xs - {a}"

47 using remove' by auto

49 lemma sorted_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> sorted (remove a xs)"

50 using remove' by auto

52 lemma distinct_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> distinct (remove a xs)"

53 using remove' by auto

55 lemma remove_insort_cancel: "remove a (insort a xs) = xs"

56 apply (induct xs)

57 apply simp

58 apply auto

59 done

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

69 lemma notinset_remove: "x \<notin> set xs \<Longrightarrow> remove x xs = xs"

70 apply (induct xs)

71 apply auto

72 done

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 fastforce

81 done

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

89 subsection {* Efficient member function for sorted lists *}

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

95 lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)"

96 by (induct xs) (auto simp add: sorted_Cons)

98 end