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