New subdirectory for functional data structures
authornipkow
Mon Sep 21 14:44:32 2015 +0200 (2015-09-21)
changeset 61203a8a8eca85801
parent 61202 9e37178084c5
child 61204 3e491e34a62e
New subdirectory for functional data structures
src/HOL/Data_Structures/AList_Upd_Del.thy
src/HOL/Data_Structures/Less_False.thy
src/HOL/Data_Structures/List_Ins_Del.thy
src/HOL/Data_Structures/Map_by_Ordered.thy
src/HOL/Data_Structures/Set_by_Ordered.thy
src/HOL/Data_Structures/Sorted_Less.thy
src/HOL/Data_Structures/Tree_Map.thy
src/HOL/Data_Structures/Tree_Set.thy
src/HOL/Data_Structures/document/root.bib
src/HOL/Data_Structures/document/root.tex
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Mon Sep 21 14:44:32 2015 +0200
     1.3 @@ -0,0 +1,139 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section {* Association List Update and Deletion *}
     1.7 +
     1.8 +theory AList_Upd_Del
     1.9 +imports Sorted_Less
    1.10 +begin
    1.11 +
    1.12 +abbreviation "sorted1 ps \<equiv> sorted(map fst ps)"
    1.13 +
    1.14 +text{* Define own @{text map_of} function to avoid pulling in an unknown
    1.15 +amount of lemmas implicitly (via the simpset). *}
    1.16 +
    1.17 +hide_const (open) map_of
    1.18 +
    1.19 +fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where
    1.20 +"map_of [] = (\<lambda>a. None)" |
    1.21 +"map_of ((x,y)#ps) = (\<lambda>a. if x=a then Some y else map_of ps a)"
    1.22 +
    1.23 +text \<open>Updating into an association list:\<close>
    1.24 +
    1.25 +fun upd_list :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) list \<Rightarrow> ('a*'b) list" where
    1.26 +"upd_list a b [] = [(a,b)]" |
    1.27 +"upd_list a b ((x,y)#ps) =
    1.28 +  (if a < x then (a,b)#(x,y)#ps else
    1.29 +  if a=x then (a,b)#ps else (x,y) # upd_list a b ps)"
    1.30 +
    1.31 +fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where
    1.32 +"del_list a [] = []" |
    1.33 +"del_list a ((x,y)#ps) = (if a=x then ps else (x,y) # del_list a ps)"
    1.34 +
    1.35 +
    1.36 +subsection \<open>Lemmas for @{const map_of}\<close>
    1.37 +
    1.38 +lemma map_of_ins_list: "map_of (upd_list a b ps) = (map_of ps)(a := Some b)"
    1.39 +by(induction ps) auto
    1.40 +
    1.41 +lemma map_of_append: "map_of (ps @ qs) a =
    1.42 +  (case map_of ps a of None \<Rightarrow> map_of qs a | Some b \<Rightarrow> Some b)"
    1.43 +by(induction ps)(auto)
    1.44 +
    1.45 +lemma map_of_None: "sorted (a # map fst ps) \<Longrightarrow> map_of ps a = None"
    1.46 +by (induction ps) (auto simp: sorted_lems sorted_Cons_iff)
    1.47 +
    1.48 +lemma map_of_None2: "sorted (map fst ps @ [a]) \<Longrightarrow> map_of ps a = None"
    1.49 +by (induction ps) (auto simp: sorted_lems)
    1.50 +
    1.51 +lemma map_of_del_list: "sorted1 ps \<Longrightarrow>
    1.52 +  map_of(del_list a ps) = (map_of ps)(a := None)"
    1.53 +by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff)
    1.54 +
    1.55 +lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow>
    1.56 +   map_of ps x = None"
    1.57 +by (meson less_trans map_of_None sorted_Cons_iff)
    1.58 +
    1.59 +lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
    1.60 +  map_of ps x = None"
    1.61 +by (meson le_less_trans map_of_None2 not_less sorted_snoc_iff)
    1.62 +
    1.63 +lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc
    1.64 +
    1.65 +
    1.66 +subsection \<open>Lemmas for @{const upd_list}\<close>
    1.67 +
    1.68 +lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list a b ps)"
    1.69 +apply(induction ps) 
    1.70 + apply simp
    1.71 +apply(case_tac ps)
    1.72 + apply auto
    1.73 +done
    1.74 +
    1.75 +lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [x]); a < x \<rbrakk> \<Longrightarrow>
    1.76 +  upd_list a b (ps @ (x,y) # qs) =  upd_list a b ps @ (x,y) # qs"
    1.77 +by(induction ps) (auto simp: sorted_lems)
    1.78 +
    1.79 +lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [x]); x \<le> a \<rbrakk> \<Longrightarrow>
    1.80 +  upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)"
    1.81 +by(induction ps) (auto simp: sorted_lems)
    1.82 +
    1.83 +lemmas upd_list_sorteds = upd_list_sorted1 upd_list_sorted2
    1.84 +
    1.85 +(*
    1.86 +lemma set_ins_list[simp]: "set (ins_list x xs) = insert x (set xs)"
    1.87 +by(induction xs) auto
    1.88 +
    1.89 +lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
    1.90 +apply(induction xs rule: sorted.induct)
    1.91 +apply auto
    1.92 +by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
    1.93 +
    1.94 +lemma set_del_list_eq [simp]: "distinct xs ==> set(del_list x xs) = set xs - {x}"
    1.95 +apply(induct xs)
    1.96 + apply simp
    1.97 +apply simp
    1.98 +apply blast
    1.99 +done
   1.100 +*)
   1.101 +
   1.102 +
   1.103 +subsection \<open>Lemmas for @{const del_list}\<close>
   1.104 +
   1.105 +lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)"
   1.106 +apply(induction ps)
   1.107 + apply simp
   1.108 +apply(case_tac ps)
   1.109 +apply auto
   1.110 +by (meson order.strict_trans sorted_Cons_iff)
   1.111 +
   1.112 +lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs"
   1.113 +by (induct xs) auto
   1.114 +
   1.115 +lemma del_list_sorted1: "sorted1 (xs @ [(x,y)]) \<Longrightarrow> x \<le> a \<Longrightarrow>
   1.116 +  del_list a (xs @ (x,y) # ys) = xs @ del_list a ((x,y) # ys)"
   1.117 +by (induction xs) (auto simp: sorted_mid_iff2)
   1.118 +
   1.119 +lemma del_list_sorted2: "sorted1 (xs @ (x,y) # ys) \<Longrightarrow> a < x \<Longrightarrow>
   1.120 +  del_list a (xs @ (x,y) # ys) = del_list a xs @ (x,y) # ys"
   1.121 +by (induction xs) (fastforce simp: sorted_Cons_iff intro!: del_list_idem)+
   1.122 +
   1.123 +lemma del_list_sorted3:
   1.124 +  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs) \<Longrightarrow> a < y \<Longrightarrow>
   1.125 +  del_list a (xs @ (x,x') # ys @ (y,y') # zs) = del_list a (xs @ (x,x') # ys) @ (y,y') # zs"
   1.126 +by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2 ball_Un)
   1.127 +
   1.128 +lemma del_list_sorted4:
   1.129 +  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) \<Longrightarrow> a < z \<Longrightarrow>
   1.130 +  del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) = del_list a (xs @ (x,x') # ys @ (y,y') # zs) @ (z,z') # us"
   1.131 +by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
   1.132 +
   1.133 +lemma del_list_sorted5:
   1.134 +  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) \<Longrightarrow> a < u \<Longrightarrow>
   1.135 +   del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) =
   1.136 +   del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) @ (u,u') # vs" 
   1.137 +by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
   1.138 +
   1.139 +lemmas del_list_sorted =
   1.140 +  del_list_sorted1 del_list_sorted2 del_list_sorted3 del_list_sorted4 del_list_sorted5
   1.141 +
   1.142 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Data_Structures/Less_False.thy	Mon Sep 21 14:44:32 2015 +0200
     2.3 @@ -0,0 +1,31 @@
     2.4 +(* Author: Tobias Nipkow *)
     2.5 +
     2.6 +section {* Improved Simproc for $<$ *}
     2.7 +
     2.8 +theory Less_False
     2.9 +imports Main
    2.10 +begin
    2.11 +
    2.12 +simproc_setup less_False ("(x::'a::order) < y") = {* fn _ => fn ctxt => fn ct =>
    2.13 +  let
    2.14 +    fun prp t thm = Thm.full_prop_of thm aconv t;
    2.15 +
    2.16 +    val eq_False_if_not = @{thm eq_False} RS iffD2
    2.17 +
    2.18 +    fun prove_less_False ((less as Const(_,T)) $ r $ s) =
    2.19 +      let val prems = Simplifier.prems_of ctxt;
    2.20 +          val le = Const (@{const_name less_eq}, T);
    2.21 +          val t = HOLogic.mk_Trueprop(le $ s $ r);
    2.22 +      in case find_first (prp t) prems of
    2.23 +           NONE =>
    2.24 +             let val t = HOLogic.mk_Trueprop(less $ s $ r)
    2.25 +             in case find_first (prp t) prems of
    2.26 +                  NONE => NONE
    2.27 +                | SOME thm => SOME(mk_meta_eq((thm RS @{thm less_not_sym}) RS eq_False_if_not))
    2.28 +             end
    2.29 +         | SOME thm => NONE
    2.30 +      end;
    2.31 +  in prove_less_False (Thm.term_of ct) end
    2.32 +*}
    2.33 +
    2.34 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Mon Sep 21 14:44:32 2015 +0200
     3.3 @@ -0,0 +1,122 @@
     3.4 +(* Author: Tobias Nipkow *)
     3.5 +
     3.6 +section {* List Insertion and Deletion *}
     3.7 +
     3.8 +theory List_Ins_Del
     3.9 +imports Sorted_Less
    3.10 +begin
    3.11 +
    3.12 +subsection \<open>Elements in a list\<close>
    3.13 +
    3.14 +fun elems :: "'a list \<Rightarrow> 'a set" where
    3.15 +"elems [] = {}" |
    3.16 +"elems (x#xs) = Set.insert x (elems xs)"
    3.17 +
    3.18 +lemma elems_app: "elems (xs @ ys) = (elems xs \<union> elems ys)"
    3.19 +by (induction xs) auto
    3.20 +
    3.21 +lemma elems_eq_set: "elems xs = set xs"
    3.22 +by (induction xs) auto
    3.23 +
    3.24 +lemma sorted_Cons_iff:
    3.25 +  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> elems xs. x < y))"
    3.26 +by(simp add: elems_eq_set Sorted_Less.sorted_Cons_iff)
    3.27 +
    3.28 +lemma sorted_snoc_iff:
    3.29 +  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
    3.30 +by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff)
    3.31 +
    3.32 +lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> y < x"
    3.33 +by (simp add: sorted_Cons_iff)
    3.34 +
    3.35 +lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> x < y"
    3.36 +by (simp add: sorted_snoc_iff)
    3.37 +
    3.38 +lemmas elems_simps0 = sorted_lems elems_app
    3.39 +lemmas elems_simps = elems_simps0 sorted_Cons_iff sorted_snoc_iff
    3.40 +lemmas sortedD = sorted_ConsD sorted_snocD
    3.41 +
    3.42 +
    3.43 +subsection \<open>Inserting into an ordered list without duplicates:\<close>
    3.44 +
    3.45 +fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    3.46 +"ins_list x [] = [x]" |
    3.47 +"ins_list x (y#zs) =
    3.48 +  (if x < y then x#y#zs else if x=y then x#zs else y # ins_list x zs)"
    3.49 +
    3.50 +lemma set_ins_list[simp]: "elems (ins_list x xs) = insert x (elems xs)"
    3.51 +by(induction xs) auto
    3.52 +
    3.53 +lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
    3.54 +apply(induction xs rule: sorted.induct)
    3.55 +apply auto
    3.56 +by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
    3.57 +
    3.58 +lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
    3.59 +by(induction xs rule: sorted.induct) auto
    3.60 +
    3.61 +lemma ins_list_sorted1: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow>
    3.62 +  ins_list x (xs @ y # ys) = xs @ ins_list x (y#ys)"
    3.63 +by(induction xs) (auto simp: sorted_lems)
    3.64 +
    3.65 +lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow>
    3.66 +  ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)"
    3.67 +by(induction xs) (auto simp: sorted_lems)
    3.68 +
    3.69 +lemmas ins_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
    3.70 +
    3.71 +
    3.72 +subsection \<open>Delete one occurrence of an element from a list:\<close>
    3.73 +
    3.74 +fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    3.75 +"del_list a [] = []" |
    3.76 +"del_list a (x#xs) = (if a=x then xs else x # del_list a xs)"
    3.77 +
    3.78 +lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs"
    3.79 +by (induct xs) simp_all
    3.80 +
    3.81 +lemma elems_del_list_eq [simp]:
    3.82 +  "distinct xs \<Longrightarrow> elems (del_list x xs) = elems xs - {x}"
    3.83 +apply(induct xs)
    3.84 + apply simp
    3.85 +apply (simp add: elems_eq_set)
    3.86 +apply blast
    3.87 +done
    3.88 +
    3.89 +lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
    3.90 +apply(induction xs rule: sorted.induct)
    3.91 +apply auto
    3.92 +by (meson order.strict_trans sorted_Cons_iff)
    3.93 +
    3.94 +lemma del_list_sorted1: "sorted (xs @ [x]) \<Longrightarrow> x \<le> y \<Longrightarrow>
    3.95 +  del_list y (xs @ x # ys) = xs @ del_list y (x # ys)"
    3.96 +by (induction xs) (auto simp: sorted_mid_iff2)
    3.97 +
    3.98 +lemma del_list_sorted2: "sorted (xs @ x # ys) \<Longrightarrow> y < x \<Longrightarrow>
    3.99 +  del_list y (xs @ x # ys) = del_list y xs @ x # ys"
   3.100 +by (induction xs) (auto simp: sorted_Cons_iff intro!: del_list_idem)
   3.101 +
   3.102 +lemma del_list_sorted3:
   3.103 +  "sorted (xs @ x # ys @ y # zs) \<Longrightarrow> a < y \<Longrightarrow>
   3.104 +  del_list a (xs @ x # ys @ y # zs) = del_list a (xs @ x # ys) @ y # zs"
   3.105 +by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2)
   3.106 +
   3.107 +lemma del_list_sorted4:
   3.108 +  "sorted (xs @ x # ys @ y # zs @ z # us) \<Longrightarrow> a < z \<Longrightarrow>
   3.109 +  del_list a (xs @ x # ys @ y # zs @ z # us) = del_list a (xs @ x # ys @ y # zs) @ z # us"
   3.110 +by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
   3.111 +
   3.112 +lemma del_list_sorted5:
   3.113 +  "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow>
   3.114 +   del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) =
   3.115 +   del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" 
   3.116 +by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
   3.117 +
   3.118 +lemmas del_simps = sorted_lems
   3.119 +  del_list_sorted1
   3.120 +  del_list_sorted2
   3.121 +  del_list_sorted3
   3.122 +  del_list_sorted4
   3.123 +  del_list_sorted5
   3.124 +
   3.125 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Mon Sep 21 14:44:32 2015 +0200
     4.3 @@ -0,0 +1,55 @@
     4.4 +(* Author: Tobias Nipkow *)
     4.5 +
     4.6 +section {* Implementing Ordered Maps *}
     4.7 +
     4.8 +theory Map_by_Ordered
     4.9 +imports AList_Upd_Del
    4.10 +begin
    4.11 +
    4.12 +locale Map =
    4.13 +fixes empty :: "'m"
    4.14 +fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
    4.15 +fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
    4.16 +fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
    4.17 +fixes invar :: "'m \<Rightarrow> bool"
    4.18 +assumes "map_of empty = (\<lambda>_. None)"
    4.19 +assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
    4.20 +assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
    4.21 +assumes "invar m \<Longrightarrow> invar(update a b m)"
    4.22 +assumes "invar m \<Longrightarrow> invar(delete a m)"
    4.23 +
    4.24 +locale Map_by_Ordered =
    4.25 +fixes empty :: "'t"
    4.26 +fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't"
    4.27 +fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    4.28 +fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
    4.29 +fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
    4.30 +fixes wf :: "'t \<Rightarrow> bool"
    4.31 +assumes empty: "inorder empty = []"
    4.32 +assumes lookup: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
    4.33 +  lookup t a = map_of (inorder t) a"
    4.34 +assumes update: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
    4.35 +  inorder(update a b t) = upd_list a b (inorder t)"
    4.36 +assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
    4.37 +  inorder(delete a t) = del_list a (inorder t)"
    4.38 +assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)"
    4.39 +assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)"
    4.40 +begin
    4.41 +
    4.42 +sublocale Map
    4.43 +  empty update delete "map_of o inorder" "\<lambda>t. wf t \<and> sorted1 (inorder t)"
    4.44 +proof(standard, goal_cases)
    4.45 +  case 1 show ?case by (auto simp: empty)
    4.46 +next
    4.47 +  case 2 thus ?case by(simp add: update map_of_ins_list)
    4.48 +next
    4.49 +  case 3 thus ?case by(simp add: delete map_of_del_list)
    4.50 +next
    4.51 +  case 4 thus ?case by(simp add: update wf_insert sorted_upd_list)
    4.52 +next
    4.53 +  case 5 thus ?case by (auto simp: delete wf_delete sorted_del_list)
    4.54 +qed
    4.55 +
    4.56 +end
    4.57 +
    4.58 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Mon Sep 21 14:44:32 2015 +0200
     5.3 @@ -0,0 +1,60 @@
     5.4 +(* Author: Tobias Nipkow *)
     5.5 +
     5.6 +section {* Implementing Ordered Sets *}
     5.7 +
     5.8 +theory Set_by_Ordered
     5.9 +imports List_Ins_Del
    5.10 +begin
    5.11 +
    5.12 +locale Set =
    5.13 +fixes empty :: "'s"
    5.14 +fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    5.15 +fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    5.16 +fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
    5.17 +fixes set :: "'s \<Rightarrow> 'a set"
    5.18 +fixes invar :: "'s \<Rightarrow> bool"
    5.19 +assumes "set empty = {}"
    5.20 +assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)"
    5.21 +assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)"
    5.22 +assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}"
    5.23 +assumes "invar s \<Longrightarrow> invar(insert a s)"
    5.24 +assumes "invar s \<Longrightarrow> invar(delete a s)"
    5.25 +
    5.26 +locale Set_by_Ordered =
    5.27 +fixes empty :: "'t"
    5.28 +fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
    5.29 +fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    5.30 +fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
    5.31 +fixes inorder :: "'t \<Rightarrow> 'a list"
    5.32 +fixes wf :: "'t \<Rightarrow> bool"
    5.33 +assumes empty: "inorder empty = []"
    5.34 +assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow>
    5.35 +  isin t a = (a \<in> elems (inorder t))"
    5.36 +assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow>
    5.37 +  inorder(insert a t) = ins_list a (inorder t)"
    5.38 +assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
    5.39 +  inorder(delete a t) = del_list a (inorder t)"
    5.40 +assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)"
    5.41 +assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)"
    5.42 +begin
    5.43 +
    5.44 +sublocale Set
    5.45 +  empty insert delete isin "elems o inorder" "\<lambda>t. wf t \<and> sorted(inorder t)"
    5.46 +proof(standard, goal_cases)
    5.47 +  case 1 show ?case by (auto simp: empty)
    5.48 +next
    5.49 +  case 2 thus ?case by(simp add: isin)
    5.50 +next
    5.51 +  case 3 thus ?case by(simp add: insert)
    5.52 +next
    5.53 +  case (4 s a) show ?case
    5.54 +    using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted)
    5.55 +next
    5.56 +  case 5 thus ?case by(simp add: insert wf_insert sorted_ins_list)
    5.57 +next
    5.58 +  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
    5.59 +qed
    5.60 +
    5.61 +end
    5.62 +
    5.63 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Data_Structures/Sorted_Less.thy	Mon Sep 21 14:44:32 2015 +0200
     6.3 @@ -0,0 +1,54 @@
     6.4 +(* Author: Tobias Nipkow *)
     6.5 +
     6.6 +section {* Lists Sorted wrt $<$ *}
     6.7 +
     6.8 +theory Sorted_Less
     6.9 +imports Less_False
    6.10 +begin
    6.11 +
    6.12 +hide_const sorted
    6.13 +
    6.14 +text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?
    6.15 +Could go into theory List under a name like @{term sorted_less}.\<close>
    6.16 +
    6.17 +fun sorted :: "'a::linorder list \<Rightarrow> bool" where
    6.18 +"sorted [] = True" |
    6.19 +"sorted [x] = True" |
    6.20 +"sorted (x#y#zs) = (x < y \<and> sorted(y#zs))"
    6.21 +
    6.22 +lemma sorted_Cons_iff:
    6.23 +  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x < y))"
    6.24 +by(induction xs rule: sorted.induct) auto
    6.25 +
    6.26 +lemma sorted_snoc_iff:
    6.27 +  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> set xs. y < x))"
    6.28 +by(induction xs rule: sorted.induct) auto
    6.29 +
    6.30 +lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
    6.31 +by(simp add: sorted_Cons_iff)
    6.32 +
    6.33 +lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs"
    6.34 +by(rule ASSUMPTION_D [THEN sorted_cons])
    6.35 +
    6.36 +lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs"
    6.37 +by(simp add: sorted_snoc_iff)
    6.38 +
    6.39 +lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs"
    6.40 +by(rule ASSUMPTION_D [THEN sorted_snoc])
    6.41 +
    6.42 +lemma sorted_mid_iff:
    6.43 +  "sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
    6.44 +by(induction xs rule: sorted.induct) auto
    6.45 +
    6.46 +lemma sorted_mid_iff2:
    6.47 +  "sorted(x # xs @ y # ys) =
    6.48 +  (sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
    6.49 +by(induction xs rule: sorted.induct) auto
    6.50 +
    6.51 +lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow>
    6.52 +  sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
    6.53 +by(rule sorted_mid_iff)
    6.54 +
    6.55 +lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'
    6.56 +
    6.57 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Mon Sep 21 14:44:32 2015 +0200
     7.3 @@ -0,0 +1,72 @@
     7.4 +(* Author: Tobias Nipkow *)
     7.5 +
     7.6 +section {* Unbalanced Tree as Map *}
     7.7 +
     7.8 +theory Tree_Map
     7.9 +imports
    7.10 +  "~~/src/HOL/Library/Tree"
    7.11 +  Map_by_Ordered
    7.12 +begin
    7.13 +
    7.14 +fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
    7.15 +"lookup Leaf x = None" |
    7.16 +"lookup (Node l (a,b) r) x = (if x < a then lookup l x else
    7.17 +  if x > a then lookup r x else Some b)"
    7.18 +
    7.19 +fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    7.20 +"update a b Leaf = Node Leaf (a,b) Leaf" |
    7.21 +"update a b (Node l (x,y) r) =
    7.22 +   (if a < x then Node (update a b l) (x,y) r
    7.23 +    else if a=x then Node l (a,b) r
    7.24 +    else Node l (x,y) (update a b r))"
    7.25 +
    7.26 +fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
    7.27 +"del_min (Node Leaf a r) = (a, r)" |
    7.28 +"del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))"
    7.29 +
    7.30 +fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
    7.31 +"delete k Leaf = Leaf" |
    7.32 +"delete k (Node l (a,b) r) = (if k<a then Node (delete k l) (a,b) r else
    7.33 +  if k > a then Node l (a,b) (delete k r) else
    7.34 +  if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
    7.35 +
    7.36 +
    7.37 +subsection "Functional Correctness Proofs"
    7.38 +
    7.39 +lemma lookup_eq: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    7.40 +apply (induction t)
    7.41 +apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
    7.42 +done
    7.43 +
    7.44 +
    7.45 +lemma inorder_update:
    7.46 +  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
    7.47 +by(induction t) (auto simp: upd_list_sorteds sorted_lems)
    7.48 +
    7.49 +
    7.50 +lemma del_minD:
    7.51 +  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
    7.52 +   x # inorder t' = inorder t"
    7.53 +by(induction t arbitrary: t' rule: del_min.induct)
    7.54 +  (auto simp: sorted_lems split: prod.splits)
    7.55 +
    7.56 +lemma inorder_delete:
    7.57 +  "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    7.58 +by(induction t)
    7.59 +  (auto simp: del_list_sorted sorted_lems dest!: del_minD split: prod.splits)
    7.60 +
    7.61 +
    7.62 +interpretation Map_by_Ordered
    7.63 +where empty = Leaf and lookup = lookup and update = update and delete = delete
    7.64 +and inorder = inorder and wf = "\<lambda>_. True"
    7.65 +proof (standard, goal_cases)
    7.66 +  case 1 show ?case by simp
    7.67 +next
    7.68 +  case 2 thus ?case by(simp add: lookup_eq)
    7.69 +next
    7.70 +  case 3 thus ?case by(simp add: inorder_update)
    7.71 +next
    7.72 +  case 4 thus ?case by(simp add: inorder_delete)
    7.73 +qed (rule TrueI)+
    7.74 +
    7.75 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Mon Sep 21 14:44:32 2015 +0200
     8.3 @@ -0,0 +1,75 @@
     8.4 +(* Author: Tobias Nipkow *)
     8.5 +
     8.6 +section {* Tree Implementation of Sets *}
     8.7 +
     8.8 +theory Tree_Set
     8.9 +imports
    8.10 +  "~~/src/HOL/Library/Tree"
    8.11 +  Set_by_Ordered
    8.12 +begin
    8.13 +
    8.14 +fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where
    8.15 +"isin Leaf x = False" |
    8.16 +"isin (Node l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"
    8.17 +
    8.18 +hide_const (open) insert
    8.19 +
    8.20 +fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    8.21 +"insert a Leaf = Node Leaf a Leaf" |
    8.22 +"insert a (Node l x r) =
    8.23 +   (if a < x then Node (insert a l) x r
    8.24 +    else if a=x then Node l x r
    8.25 +    else Node l x (insert a r))"
    8.26 +
    8.27 +fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
    8.28 +"del_min (Node Leaf a r) = (a, r)" |
    8.29 +"del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))"
    8.30 +
    8.31 +fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    8.32 +"delete k Leaf = Leaf" |
    8.33 +"delete k (Node l a r) = (if k<a then Node (delete k l) a r else
    8.34 +  if k > a then Node l a (delete k r) else
    8.35 +  if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
    8.36 +
    8.37 +
    8.38 +subsection "Functional Correctness Proofs"
    8.39 +
    8.40 +lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
    8.41 +by (induction t) (auto simp: elems_simps)
    8.42 +
    8.43 +lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
    8.44 +by (induction t) (auto simp: elems_simps0 dest: sortedD)
    8.45 +
    8.46 +
    8.47 +lemma inorder_insert:
    8.48 +  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    8.49 +by(induction t) (auto simp: ins_simps)
    8.50 +
    8.51 +
    8.52 +lemma del_minD:
    8.53 +  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
    8.54 +   x # inorder t' = inorder t"
    8.55 +by(induction t arbitrary: t' rule: del_min.induct)
    8.56 +  (auto simp: sorted_lems split: prod.splits)
    8.57 +
    8.58 +lemma inorder_delete:
    8.59 +  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    8.60 +by(induction t) (auto simp: del_simps del_minD split: prod.splits)
    8.61 +
    8.62 +
    8.63 +interpretation Set_by_Ordered
    8.64 +where empty = Leaf and isin = isin and insert = insert and delete = delete
    8.65 +and inorder = inorder and wf = "\<lambda>_. True"
    8.66 +proof (standard, goal_cases)
    8.67 +  case 1 show ?case by simp
    8.68 +next
    8.69 +  case 2 thus ?case by(simp add: isin_set)
    8.70 +next
    8.71 +  case 3 thus ?case by(simp add: inorder_insert)
    8.72 +next
    8.73 +  case 4 thus ?case by(simp add: inorder_delete)
    8.74 +next
    8.75 +  case 5 thus ?case by(simp)
    8.76 +qed
    8.77 +
    8.78 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Data_Structures/document/root.bib	Mon Sep 21 14:44:32 2015 +0200
     9.3 @@ -0,0 +1,20 @@
     9.4 +@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
     9.5 +@string{MIT="MIT Press"}
     9.6 +@string{Springer="Springer-Verlag"}
     9.7 +
     9.8 +@book{Nielson,author={Hanne Riis Nielson and Flemming Nielson},
     9.9 +title={Semantics with Applications},publisher={Wiley},year=1992}
    9.10 +
    9.11 +@book{Winskel,author={Glynn Winskel},
    9.12 +title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993}
    9.13 +
    9.14 +@inproceedings{Nipkow,author={Tobias Nipkow},
    9.15 +title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
    9.16 +booktitle=
    9.17 +{Foundations of Software Technology and Theoretical Computer Science},
    9.18 +editor={V. Chandru and V. Vinay},
    9.19 +publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
    9.20 +
    9.21 +@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
    9.22 +title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
    9.23 +note={To appear}}
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Data_Structures/document/root.tex	Mon Sep 21 14:44:32 2015 +0200
    10.3 @@ -0,0 +1,42 @@
    10.4 +\documentclass[11pt,a4paper]{article}
    10.5 +\usepackage{isabelle,isabellesym}
    10.6 +\usepackage{latexsym}
    10.7 +% this should be the last package used
    10.8 +\usepackage{pdfsetup}
    10.9 +
   10.10 +% snip
   10.11 +\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
   10.12 +\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
   10.13 +
   10.14 +\urlstyle{rm}
   10.15 +\isabellestyle{it}
   10.16 +
   10.17 +\renewcommand{\isacharunderscore}{\_}
   10.18 +\renewcommand{\isacharunderscorekeyword}{\_}
   10.19 +
   10.20 +% for uniform font size
   10.21 +\renewcommand{\isastyle}{\isastyleminor}
   10.22 +
   10.23 +\begin{document}
   10.24 +
   10.25 +\title{Functional Data Structures}
   10.26 +\author{Tobias Nipkow}
   10.27 +\maketitle
   10.28 +
   10.29 +\begin{abstract}
   10.30 +A collection of verified functional data structures. The emphasis is on
   10.31 +conciseness of algorithms and succinctness of proofs, more in the style
   10.32 +of a textbook than a library of efficient algorithms.
   10.33 +\end{abstract}
   10.34 +
   10.35 +\setcounter{tocdepth}{2}
   10.36 +\tableofcontents
   10.37 +\newpage
   10.38 +
   10.39 +% generated text of all theories
   10.40 +\input{session}
   10.41 +
   10.42 +%\bibliographystyle{abbrv}
   10.43 +%\bibliography{root}
   10.44 +
   10.45 +\end{document}
    11.1 --- a/src/HOL/ROOT	Mon Sep 21 11:31:56 2015 +0200
    11.2 +++ b/src/HOL/ROOT	Mon Sep 21 14:44:32 2015 +0200
    11.3 @@ -169,6 +169,15 @@
    11.4    options [document = false]
    11.5    theories EvenOdd
    11.6  
    11.7 +session "HOL-Data_Structures" in Data_Structures = HOL +
    11.8 +  options [document_variants = document]
    11.9 +  theories [document = false]
   11.10 +    "Less_False"
   11.11 +  theories
   11.12 +    Tree_Set
   11.13 +    Tree_Map
   11.14 +  document_files "root.tex"
   11.15 +
   11.16  session "HOL-Import" in Import = HOL +
   11.17    theories HOL_Light_Maps
   11.18    theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import