Theory Sorted_List

(*  Title:      HOL/Imperative_HOL/ex/Sorted_List.thy
    Author:     Lukas Bulwahn, TU Muenchen
*)

section {* Sorted lists as representation of finite sets *}

theory Sorted_List
imports Main
begin

text {* Merge function for two distinct sorted lists to get compound distinct sorted list *}
   
fun merge :: "('a::linorder) list ⇒ 'a list ⇒ 'a list"
where
  "merge (x#xs) (y#ys) =
  (if x < y then x # merge xs (y#ys) else (if x > y then y # merge (x#xs) ys else x # merge xs ys))"
| "merge xs [] = xs"
| "merge [] ys = ys"

text {* The function package does not derive automatically the more general rewrite rule as follows: *}
lemma merge_Nil[simp]: "merge [] ys = ys"
by (cases ys) auto

lemma set_merge[simp]: "set (merge xs ys) = set xs ∪ set ys"
by (induct xs ys rule: merge.induct, auto)

lemma sorted_merge[simp]:
     "List.sorted (merge xs ys) = (List.sorted xs ∧ List.sorted ys)"
by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons)

lemma distinct_merge[simp]: "⟦ distinct xs; distinct ys; List.sorted xs; List.sorted ys ⟧ ⟹ distinct (merge xs ys)"
by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons)

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

primrec remove :: "('a :: linorder) ⇒ 'a list ⇒ 'a list"
where
  "remove a [] = []"
  |  "remove a (x#xs) = (if a > x then (x # remove a xs) else (if a = x then xs else x#xs))" 

lemma remove': "sorted xs ∧ distinct xs ⟹ sorted (remove a xs) ∧ distinct (remove a xs) ∧ set (remove a xs) = set xs - {a}"
apply (induct xs)
apply (auto simp add: sorted_Cons)
done

lemma set_remove[simp]: "⟦ sorted xs; distinct xs ⟧ ⟹ set (remove a xs) = set xs - {a}"
using remove' by auto

lemma sorted_remove[simp]: "⟦ sorted xs; distinct xs ⟧ ⟹ sorted (remove a xs)" 
using remove' by auto

lemma distinct_remove[simp]: "⟦ sorted xs; distinct xs ⟧ ⟹ distinct (remove a xs)" 
using remove' by auto

lemma remove_insort_cancel: "remove a (insort a xs) = xs"
apply (induct xs)
apply simp
apply auto
done

lemma remove_insort_commute: "⟦ a ≠ b; sorted xs ⟧ ⟹ remove b (insort a xs) = insort a (remove b xs)"
apply (induct xs)
apply auto
apply (auto simp add: sorted_Cons)
apply (case_tac xs)
apply auto
done

lemma notinset_remove: "x ∉ set xs ⟹ remove x xs = xs"
apply (induct xs)
apply auto
done

lemma remove1_eq_remove:
  "sorted xs ⟹ distinct xs ⟹ remove1 x xs = remove x xs"
apply (induct xs)
apply (auto simp add: sorted_Cons)
apply (subgoal_tac "x ∉ set xs")
apply (simp add: notinset_remove)
apply fastforce
done

lemma sorted_remove1:
  "sorted xs ⟹ sorted (remove1 x xs)"
apply (induct xs)
apply (auto simp add: sorted_Cons)
done

subsection {* Efficient member function for sorted lists *}

primrec smember :: "'a list ⇒ 'a::linorder ⇒ bool" where
  "smember [] x ⟷ False"
| "smember (y#ys) x ⟷ x = y ∨ (x > y ∧ smember ys x)"

lemma "sorted xs ⟹ smember xs x ⟷ (x ∈ set xs)" 
  by (induct xs) (auto simp add: sorted_Cons)

end