# HG changeset patch
# User wenzelm
# Date 1442864589 -7200
# Node ID bf194f7c4c8eb2d2745681a4b61c3cbe164d0b7b
# Parent  3e491e34a62e23edc0a865197d5ba751d33d99a4# Parent  1bb5a10b8ce029e20431263ef67a4d1c1bd69451
merged

diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/AList_Upd_Del.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,139 @@
+(* Author: Tobias Nipkow *)
+
+section {* Association List Update and Deletion *}
+
+theory AList_Upd_Del
+imports Sorted_Less
+begin
+
+abbreviation "sorted1 ps \<equiv> sorted(map fst ps)"
+
+text{* Define own @{text map_of} function to avoid pulling in an unknown
+amount of lemmas implicitly (via the simpset). *}
+
+hide_const (open) map_of
+
+fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where
+"map_of [] = (\<lambda>a. None)" |
+"map_of ((x,y)#ps) = (\<lambda>a. if x=a then Some y else map_of ps a)"
+
+text \<open>Updating into an association list:\<close>
+
+fun upd_list :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) list \<Rightarrow> ('a*'b) list" where
+"upd_list a b [] = [(a,b)]" |
+"upd_list a b ((x,y)#ps) =
+  (if a < x then (a,b)#(x,y)#ps else
+  if a=x then (a,b)#ps else (x,y) # upd_list a b ps)"
+
+fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where
+"del_list a [] = []" |
+"del_list a ((x,y)#ps) = (if a=x then ps else (x,y) # del_list a ps)"
+
+
+subsection \<open>Lemmas for @{const map_of}\<close>
+
+lemma map_of_ins_list: "map_of (upd_list a b ps) = (map_of ps)(a := Some b)"
+by(induction ps) auto
+
+lemma map_of_append: "map_of (ps @ qs) a =
+  (case map_of ps a of None \<Rightarrow> map_of qs a | Some b \<Rightarrow> Some b)"
+by(induction ps)(auto)
+
+lemma map_of_None: "sorted (a # map fst ps) \<Longrightarrow> map_of ps a = None"
+by (induction ps) (auto simp: sorted_lems sorted_Cons_iff)
+
+lemma map_of_None2: "sorted (map fst ps @ [a]) \<Longrightarrow> map_of ps a = None"
+by (induction ps) (auto simp: sorted_lems)
+
+lemma map_of_del_list: "sorted1 ps \<Longrightarrow>
+  map_of(del_list a ps) = (map_of ps)(a := None)"
+by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff)
+
+lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow>
+   map_of ps x = None"
+by (meson less_trans map_of_None sorted_Cons_iff)
+
+lemma map_of_sorted_snoc: "sorted (map fst ps @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+  map_of ps x = None"
+by (meson le_less_trans map_of_None2 not_less sorted_snoc_iff)
+
+lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc
+
+
+subsection \<open>Lemmas for @{const upd_list}\<close>
+
+lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list a b ps)"
+apply(induction ps) 
+ apply simp
+apply(case_tac ps)
+ apply auto
+done
+
+lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [x]); a < x \<rbrakk> \<Longrightarrow>
+  upd_list a b (ps @ (x,y) # qs) =  upd_list a b ps @ (x,y) # qs"
+by(induction ps) (auto simp: sorted_lems)
+
+lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [x]); x \<le> a \<rbrakk> \<Longrightarrow>
+  upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)"
+by(induction ps) (auto simp: sorted_lems)
+
+lemmas upd_list_sorteds = upd_list_sorted1 upd_list_sorted2
+
+(*
+lemma set_ins_list[simp]: "set (ins_list x xs) = insert x (set xs)"
+by(induction xs) auto
+
+lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
+apply(induction xs rule: sorted.induct)
+apply auto
+by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
+
+lemma set_del_list_eq [simp]: "distinct xs ==> set(del_list x xs) = set xs - {x}"
+apply(induct xs)
+ apply simp
+apply simp
+apply blast
+done
+*)
+
+
+subsection \<open>Lemmas for @{const del_list}\<close>
+
+lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)"
+apply(induction ps)
+ apply simp
+apply(case_tac ps)
+apply auto
+by (meson order.strict_trans sorted_Cons_iff)
+
+lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs"
+by (induct xs) auto
+
+lemma del_list_sorted1: "sorted1 (xs @ [(x,y)]) \<Longrightarrow> x \<le> a \<Longrightarrow>
+  del_list a (xs @ (x,y) # ys) = xs @ del_list a ((x,y) # ys)"
+by (induction xs) (auto simp: sorted_mid_iff2)
+
+lemma del_list_sorted2: "sorted1 (xs @ (x,y) # ys) \<Longrightarrow> a < x \<Longrightarrow>
+  del_list a (xs @ (x,y) # ys) = del_list a xs @ (x,y) # ys"
+by (induction xs) (fastforce simp: sorted_Cons_iff intro!: del_list_idem)+
+
+lemma del_list_sorted3:
+  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs) \<Longrightarrow> a < y \<Longrightarrow>
+  del_list a (xs @ (x,x') # ys @ (y,y') # zs) = del_list a (xs @ (x,x') # ys) @ (y,y') # zs"
+by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2 ball_Un)
+
+lemma del_list_sorted4:
+  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) \<Longrightarrow> a < z \<Longrightarrow>
+  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"
+by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
+
+lemma del_list_sorted5:
+  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) \<Longrightarrow> a < u \<Longrightarrow>
+   del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) =
+   del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) @ (u,u') # vs" 
+by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
+
+lemmas del_list_sorted =
+  del_list_sorted1 del_list_sorted2 del_list_sorted3 del_list_sorted4 del_list_sorted5
+
+end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/Less_False.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Less_False.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,31 @@
+(* Author: Tobias Nipkow *)
+
+section {* Improved Simproc for $<$ *}
+
+theory Less_False
+imports Main
+begin
+
+simproc_setup less_False ("(x::'a::order) < y") = {* fn _ => fn ctxt => fn ct =>
+  let
+    fun prp t thm = Thm.full_prop_of thm aconv t;
+
+    val eq_False_if_not = @{thm eq_False} RS iffD2
+
+    fun prove_less_False ((less as Const(_,T)) $ r $ s) =
+      let val prems = Simplifier.prems_of ctxt;
+          val le = Const (@{const_name less_eq}, T);
+          val t = HOLogic.mk_Trueprop(le $ s $ r);
+      in case find_first (prp t) prems of
+           NONE =>
+             let val t = HOLogic.mk_Trueprop(less $ s $ r)
+             in case find_first (prp t) prems of
+                  NONE => NONE
+                | SOME thm => SOME(mk_meta_eq((thm RS @{thm less_not_sym}) RS eq_False_if_not))
+             end
+         | SOME thm => NONE
+      end;
+  in prove_less_False (Thm.term_of ct) end
+*}
+
+end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/List_Ins_Del.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,122 @@
+(* Author: Tobias Nipkow *)
+
+section {* List Insertion and Deletion *}
+
+theory List_Ins_Del
+imports Sorted_Less
+begin
+
+subsection \<open>Elements in a list\<close>
+
+fun elems :: "'a list \<Rightarrow> 'a set" where
+"elems [] = {}" |
+"elems (x#xs) = Set.insert x (elems xs)"
+
+lemma elems_app: "elems (xs @ ys) = (elems xs \<union> elems ys)"
+by (induction xs) auto
+
+lemma elems_eq_set: "elems xs = set xs"
+by (induction xs) auto
+
+lemma sorted_Cons_iff:
+  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> elems xs. x < y))"
+by(simp add: elems_eq_set Sorted_Less.sorted_Cons_iff)
+
+lemma sorted_snoc_iff:
+  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
+by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff)
+
+lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> y < x"
+by (simp add: sorted_Cons_iff)
+
+lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> x < y"
+by (simp add: sorted_snoc_iff)
+
+lemmas elems_simps0 = sorted_lems elems_app
+lemmas elems_simps = elems_simps0 sorted_Cons_iff sorted_snoc_iff
+lemmas sortedD = sorted_ConsD sorted_snocD
+
+
+subsection \<open>Inserting into an ordered list without duplicates:\<close>
+
+fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"ins_list x [] = [x]" |
+"ins_list x (y#zs) =
+  (if x < y then x#y#zs else if x=y then x#zs else y # ins_list x zs)"
+
+lemma set_ins_list[simp]: "elems (ins_list x xs) = insert x (elems xs)"
+by(induction xs) auto
+
+lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
+apply(induction xs rule: sorted.induct)
+apply auto
+by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
+
+lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
+by(induction xs rule: sorted.induct) auto
+
+lemma ins_list_sorted1: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow>
+  ins_list x (xs @ y # ys) = xs @ ins_list x (y#ys)"
+by(induction xs) (auto simp: sorted_lems)
+
+lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow>
+  ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)"
+by(induction xs) (auto simp: sorted_lems)
+
+lemmas ins_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
+
+
+subsection \<open>Delete one occurrence of an element from a list:\<close>
+
+fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"del_list a [] = []" |
+"del_list a (x#xs) = (if a=x then xs else x # del_list a xs)"
+
+lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs"
+by (induct xs) simp_all
+
+lemma elems_del_list_eq [simp]:
+  "distinct xs \<Longrightarrow> elems (del_list x xs) = elems xs - {x}"
+apply(induct xs)
+ apply simp
+apply (simp add: elems_eq_set)
+apply blast
+done
+
+lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
+apply(induction xs rule: sorted.induct)
+apply auto
+by (meson order.strict_trans sorted_Cons_iff)
+
+lemma del_list_sorted1: "sorted (xs @ [x]) \<Longrightarrow> x \<le> y \<Longrightarrow>
+  del_list y (xs @ x # ys) = xs @ del_list y (x # ys)"
+by (induction xs) (auto simp: sorted_mid_iff2)
+
+lemma del_list_sorted2: "sorted (xs @ x # ys) \<Longrightarrow> y < x \<Longrightarrow>
+  del_list y (xs @ x # ys) = del_list y xs @ x # ys"
+by (induction xs) (auto simp: sorted_Cons_iff intro!: del_list_idem)
+
+lemma del_list_sorted3:
+  "sorted (xs @ x # ys @ y # zs) \<Longrightarrow> a < y \<Longrightarrow>
+  del_list a (xs @ x # ys @ y # zs) = del_list a (xs @ x # ys) @ y # zs"
+by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2)
+
+lemma del_list_sorted4:
+  "sorted (xs @ x # ys @ y # zs @ z # us) \<Longrightarrow> a < z \<Longrightarrow>
+  del_list a (xs @ x # ys @ y # zs @ z # us) = del_list a (xs @ x # ys @ y # zs) @ z # us"
+by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
+
+lemma del_list_sorted5:
+  "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow>
+   del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) =
+   del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" 
+by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
+
+lemmas del_simps = sorted_lems
+  del_list_sorted1
+  del_list_sorted2
+  del_list_sorted3
+  del_list_sorted4
+  del_list_sorted5
+
+end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/Map_by_Ordered.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,55 @@
+(* Author: Tobias Nipkow *)
+
+section {* Implementing Ordered Maps *}
+
+theory Map_by_Ordered
+imports AList_Upd_Del
+begin
+
+locale Map =
+fixes empty :: "'m"
+fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm"
+fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm"
+fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option"
+fixes invar :: "'m \<Rightarrow> bool"
+assumes "map_of empty = (\<lambda>_. None)"
+assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
+assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
+assumes "invar m \<Longrightarrow> invar(update a b m)"
+assumes "invar m \<Longrightarrow> invar(delete a m)"
+
+locale Map_by_Ordered =
+fixes empty :: "'t"
+fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't"
+fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
+fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option"
+fixes inorder :: "'t \<Rightarrow> ('a * 'b) list"
+fixes wf :: "'t \<Rightarrow> bool"
+assumes empty: "inorder empty = []"
+assumes lookup: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+  lookup t a = map_of (inorder t) a"
+assumes update: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+  inorder(update a b t) = upd_list a b (inorder t)"
+assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
+  inorder(delete a t) = del_list a (inorder t)"
+assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)"
+assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)"
+begin
+
+sublocale Map
+  empty update delete "map_of o inorder" "\<lambda>t. wf t \<and> sorted1 (inorder t)"
+proof(standard, goal_cases)
+  case 1 show ?case by (auto simp: empty)
+next
+  case 2 thus ?case by(simp add: update map_of_ins_list)
+next
+  case 3 thus ?case by(simp add: delete map_of_del_list)
+next
+  case 4 thus ?case by(simp add: update wf_insert sorted_upd_list)
+next
+  case 5 thus ?case by (auto simp: delete wf_delete sorted_del_list)
+qed
+
+end
+
+end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/Set_by_Ordered.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,60 @@
+(* Author: Tobias Nipkow *)
+
+section {* Implementing Ordered Sets *}
+
+theory Set_by_Ordered
+imports List_Ins_Del
+begin
+
+locale Set =
+fixes empty :: "'s"
+fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
+fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
+fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
+fixes set :: "'s \<Rightarrow> 'a set"
+fixes invar :: "'s \<Rightarrow> bool"
+assumes "set empty = {}"
+assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)"
+assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)"
+assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}"
+assumes "invar s \<Longrightarrow> invar(insert a s)"
+assumes "invar s \<Longrightarrow> invar(delete a s)"
+
+locale Set_by_Ordered =
+fixes empty :: "'t"
+fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
+fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
+fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
+fixes inorder :: "'t \<Rightarrow> 'a list"
+fixes wf :: "'t \<Rightarrow> bool"
+assumes empty: "inorder empty = []"
+assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow>
+  isin t a = (a \<in> elems (inorder t))"
+assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow>
+  inorder(insert a t) = ins_list a (inorder t)"
+assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
+  inorder(delete a t) = del_list a (inorder t)"
+assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)"
+assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)"
+begin
+
+sublocale Set
+  empty insert delete isin "elems o inorder" "\<lambda>t. wf t \<and> sorted(inorder t)"
+proof(standard, goal_cases)
+  case 1 show ?case by (auto simp: empty)
+next
+  case 2 thus ?case by(simp add: isin)
+next
+  case 3 thus ?case by(simp add: insert)
+next
+  case (4 s a) show ?case
+    using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted)
+next
+  case 5 thus ?case by(simp add: insert wf_insert sorted_ins_list)
+next
+  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
+qed
+
+end
+
+end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/Sorted_Less.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Sorted_Less.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,54 @@
+(* Author: Tobias Nipkow *)
+
+section {* Lists Sorted wrt $<$ *}
+
+theory Sorted_Less
+imports Less_False
+begin
+
+hide_const sorted
+
+text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?
+Could go into theory List under a name like @{term sorted_less}.\<close>
+
+fun sorted :: "'a::linorder list \<Rightarrow> bool" where
+"sorted [] = True" |
+"sorted [x] = True" |
+"sorted (x#y#zs) = (x < y \<and> sorted(y#zs))"
+
+lemma sorted_Cons_iff:
+  "sorted(x # xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x < y))"
+by(induction xs rule: sorted.induct) auto
+
+lemma sorted_snoc_iff:
+  "sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> set xs. y < x))"
+by(induction xs rule: sorted.induct) auto
+
+lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
+by(simp add: sorted_Cons_iff)
+
+lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs"
+by(rule ASSUMPTION_D [THEN sorted_cons])
+
+lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs"
+by(simp add: sorted_snoc_iff)
+
+lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs"
+by(rule ASSUMPTION_D [THEN sorted_snoc])
+
+lemma sorted_mid_iff:
+  "sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
+by(induction xs rule: sorted.induct) auto
+
+lemma sorted_mid_iff2:
+  "sorted(x # xs @ y # ys) =
+  (sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
+by(induction xs rule: sorted.induct) auto
+
+lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow>
+  sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
+by(rule sorted_mid_iff)
+
+lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'
+
+end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/Tree_Map.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,72 @@
+(* Author: Tobias Nipkow *)
+
+section {* Unbalanced Tree as Map *}
+
+theory Tree_Map
+imports
+  "~~/src/HOL/Library/Tree"
+  Map_by_Ordered
+begin
+
+fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
+"lookup Leaf x = None" |
+"lookup (Node l (a,b) r) x = (if x < a then lookup l x else
+  if x > a then lookup r x else Some b)"
+
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"update a b Leaf = Node Leaf (a,b) Leaf" |
+"update a b (Node l (x,y) r) =
+   (if a < x then Node (update a b l) (x,y) r
+    else if a=x then Node l (a,b) r
+    else Node l (x,y) (update a b r))"
+
+fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
+"del_min (Node Leaf a r) = (a, r)" |
+"del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))"
+
+fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"delete k Leaf = Leaf" |
+"delete k (Node l (a,b) r) = (if k<a then Node (delete k l) (a,b) r else
+  if k > a then Node l (a,b) (delete k r) else
+  if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
+
+
+subsection "Functional Correctness Proofs"
+
+lemma lookup_eq: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+apply (induction t)
+apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
+done
+
+
+lemma inorder_update:
+  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
+by(induction t) (auto simp: upd_list_sorteds sorted_lems)
+
+
+lemma del_minD:
+  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
+   x # inorder t' = inorder t"
+by(induction t arbitrary: t' rule: del_min.induct)
+  (auto simp: sorted_lems split: prod.splits)
+
+lemma inorder_delete:
+  "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
+by(induction t)
+  (auto simp: del_list_sorted sorted_lems dest!: del_minD split: prod.splits)
+
+
+interpretation Map_by_Ordered
+where empty = Leaf and lookup = lookup and update = update and delete = delete
+and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by(simp add: lookup_eq)
+next
+  case 3 thus ?case by(simp add: inorder_update)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+qed (rule TrueI)+
+
+end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/Tree_Set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,75 @@
+(* Author: Tobias Nipkow *)
+
+section {* Tree Implementation of Sets *}
+
+theory Tree_Set
+imports
+  "~~/src/HOL/Library/Tree"
+  Set_by_Ordered
+begin
+
+fun isin :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> bool" where
+"isin Leaf x = False" |
+"isin (Node l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"
+
+hide_const (open) insert
+
+fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"insert a Leaf = Node Leaf a Leaf" |
+"insert a (Node l x r) =
+   (if a < x then Node (insert a l) x r
+    else if a=x then Node l x r
+    else Node l x (insert a r))"
+
+fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
+"del_min (Node Leaf a r) = (a, r)" |
+"del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))"
+
+fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"delete k Leaf = Leaf" |
+"delete k (Node l a r) = (if k<a then Node (delete k l) a r else
+  if k > a then Node l a (delete k r) else
+  if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
+
+
+subsection "Functional Correctness Proofs"
+
+lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (induction t) (auto simp: elems_simps)
+
+lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (induction t) (auto simp: elems_simps0 dest: sortedD)
+
+
+lemma inorder_insert:
+  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
+by(induction t) (auto simp: ins_simps)
+
+
+lemma del_minD:
+  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
+   x # inorder t' = inorder t"
+by(induction t arbitrary: t' rule: del_min.induct)
+  (auto simp: sorted_lems split: prod.splits)
+
+lemma inorder_delete:
+  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
+by(induction t) (auto simp: del_simps del_minD split: prod.splits)
+
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by(simp add: isin_set)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+next
+  case 5 thus ?case by(simp)
+qed
+
+end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/document/root.bib	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,20 @@
+@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
+@string{MIT="MIT Press"}
+@string{Springer="Springer-Verlag"}
+
+@book{Nielson,author={Hanne Riis Nielson and Flemming Nielson},
+title={Semantics with Applications},publisher={Wiley},year=1992}
+
+@book{Winskel,author={Glynn Winskel},
+title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993}
+
+@inproceedings{Nipkow,author={Tobias Nipkow},
+title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
+booktitle=
+{Foundations of Software Technology and Theoretical Computer Science},
+editor={V. Chandru and V. Vinay},
+publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
+
+@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
+title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
+note={To appear}}
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Data_Structures/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/document/root.tex	Mon Sep 21 21:43:09 2015 +0200
@@ -0,0 +1,42 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+\usepackage{latexsym}
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% snip
+\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
+\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
+
+\urlstyle{rm}
+\isabellestyle{it}
+
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharunderscorekeyword}{\_}
+
+% for uniform font size
+\renewcommand{\isastyle}{\isastyleminor}
+
+\begin{document}
+
+\title{Functional Data Structures}
+\author{Tobias Nipkow}
+\maketitle
+
+\begin{abstract}
+A collection of verified functional data structures. The emphasis is on
+conciseness of algorithms and succinctness of proofs, more in the style
+of a textbook than a library of efficient algorithms.
+\end{abstract}
+
+\setcounter{tocdepth}{2}
+\tableofcontents
+\newpage
+
+% generated text of all theories
+\input{session}
+
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Deriv.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -644,6 +644,18 @@
     ((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
   by (auto simp: has_vector_derivative_def scaleR_diff_right)
 
+lemma has_vector_derivative_add_const:
+     "((\<lambda>t. g t + z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
+apply (intro iffI)
+apply (drule has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const], simp)
+apply (drule has_vector_derivative_add [OF _ has_vector_derivative_const], simp)
+done
+
+lemma has_vector_derivative_diff_const:
+     "((\<lambda>t. g t - z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
+using has_vector_derivative_add_const [where z = "-z"]
+by simp
+
 lemma (in bounded_linear) has_vector_derivative:
   assumes "(g has_vector_derivative g') F"
   shows "((\<lambda>x. f (g x)) has_vector_derivative f g') F"
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Fun.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -69,7 +69,7 @@
 
 lemma comp_eq_elim:
   "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
-  by (simp add: fun_eq_iff) 
+  by (simp add: fun_eq_iff)
 
 lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
   by clarsimp
@@ -833,7 +833,7 @@
   thus False by best
 qed
 
-subsection \<open>Setup\<close> 
+subsection \<open>Setup\<close>
 
 subsubsection \<open>Proof tools\<close>
 
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -1691,6 +1691,32 @@
 \<close>
 
 
+text{* Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
+not to simplify the argument and to solve it by an assumption. *}
+
+definition ASSUMPTION :: "bool \<Rightarrow> bool" where
+"ASSUMPTION A \<equiv> A"
+
+lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
+by (rule refl)
+
+lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
+by(simp add: ASSUMPTION_def)
+
+lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
+by(simp add: ASSUMPTION_def)
+
+setup {*
+let
+  val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
+    resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
+    resolve_tac ctxt (Simplifier.prems_of ctxt))
+in
+  map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
+end
+*}
+
+
 subsection \<open>Code generator setup\<close>
 
 subsubsection \<open>Generic code generator preprocessor setup\<close>
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Int.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -518,7 +518,7 @@
 lemma int_cases3 [case_names zero pos neg]:
   fixes k :: int
   assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
-    and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P" 
+    and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
   shows "P"
 proof (cases k "0::int" rule: linorder_cases)
   case equal with assms(1) show P by simp
@@ -890,7 +890,7 @@
   moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
     using that by induct simp
   ultimately show ?thesis by blast
-qed  
+qed
 
 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
 apply (rule sym)
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -4,58 +4,6 @@
 imports Complex_Transcendental Weierstrass
 begin
 
-(*FIXME migrate into libraries*)
-
-lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)"
-  by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
-
-lemma continuous_on_strong_cong:
-  "s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
-  by (simp add: simp_implies_def)
-
-thm image_affinity_atLeastAtMost_div_diff
-lemma image_affinity_atLeastAtMost_div:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {a/m + c .. b/m + c}
-            else {b/m + c .. a/m + c})"
-  using image_affinity_atLeastAtMost [of "inverse m" c a b]
-  by (simp add: field_class.field_divide_inverse algebra_simps)
-
-thm continuous_on_closed_Un
-lemma continuous_on_open_Un:
-  "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
-  using continuous_on_open_Union [of "{s,t}"] by auto
-
-thm continuous_on_eq (*REPLACE*)
-lemma continuous_on_eq:
-  "\<lbrakk>continuous_on s f; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on s g"
-  unfolding continuous_on_def tendsto_def eventually_at_topological
-  by simp
-
-thm vector_derivative_add_at
-lemma vector_derivative_mult_at [simp]:
-  fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
-  shows  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
-   \<Longrightarrow> vector_derivative (\<lambda>x. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a"
-  by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric])
-
-lemma vector_derivative_scaleR_at [simp]:
-    "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
-   \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a"
-apply (rule vector_derivative_at)
-apply (rule has_vector_derivative_scaleR)
-apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
-done
-
-thm Derivative.vector_diff_chain_at
-lemma vector_derivative_chain_at:
-  assumes "f differentiable at x" "(g differentiable at (f x))"
-  shows "vector_derivative (g \<circ> f) (at x) =
-         vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
-by (metis Derivative.vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
-
-
 subsection \<open>Piecewise differentiable functions\<close>
 
 definition piecewise_differentiable_on
@@ -89,6 +37,9 @@
 by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def
          intro: differentiable_within_subset)
 
+lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on s"
+  by (simp add: differentiable_imp_piecewise_differentiable)
+
 lemma piecewise_differentiable_compose:
     "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s);
       \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
@@ -466,7 +417,7 @@
     by (auto simp: piecewise_C1_differentiable_on_def continuous_on_add)
 qed
 
-lemma piecewise_C1_differentiable_C1_diff:
+lemma piecewise_C1_differentiable_diff:
     "\<lbrakk>f piecewise_C1_differentiable_on s;  g piecewise_C1_differentiable_on s\<rbrakk>
      \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_C1_differentiable_on s"
   unfolding diff_conv_add_uminus
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -2277,6 +2277,20 @@
    \<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
   by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
 
+lemma vector_derivative_mult_at [simp]:
+  fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
+  shows  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+   \<Longrightarrow> vector_derivative (\<lambda>x. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a"
+  by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric])
+
+lemma vector_derivative_scaleR_at [simp]:
+    "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+   \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a"
+apply (rule vector_derivative_at)
+apply (rule has_vector_derivative_scaleR)
+apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
+done
+
 lemma vector_derivative_within_closed_interval:
   assumes "a < b"
     and "x \<in> cbox a b"
@@ -2356,4 +2370,10 @@
     a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
 using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
 
+lemma vector_derivative_chain_at:
+  assumes "f differentiable at x" "(g differentiable at (f x))"
+  shows "vector_derivative (g \<circ> f) (at x) =
+         vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
+by (metis vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
+
 end
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -496,6 +496,9 @@
 lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
   by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
 
+lemma abs_eq_content: "abs (y - x) = (if x\<le>y then content {x .. y} else content {y..x})"
+  by (auto simp: content_real)
+
 lemma content_singleton[simp]: "content {a} = 0"
 proof -
   have "content (cbox a a) = 0"
@@ -6414,133 +6417,75 @@
   apply (rule has_integral_const)
   done
 
+lemma integral_has_vector_derivative_continuous_at:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes f: "f integrable_on {a..b}"
+      and x: "x \<in> {a..b}"
+      and fx: "continuous (at x within {a..b}) f"
+  shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
+proof -
+  let ?I = "\<lambda>a b. integral {a..b} f"
+  { fix e::real 
+    assume "e > 0"
+    obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
+      using `e>0` fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
+    have "norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+           if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < d" for y  
+    proof (cases "y < x")
+      case False
+      have "f integrable_on {a..y}"
+        using f y by (simp add: integrable_subinterval_real)
+      then have Idiff: "?I a y - ?I a x = ?I x y" 
+        using False x by (simp add: algebra_simps integral_combine)
+      have fux_int: "((\<lambda>u. f u - f x) has_integral integral {x..y} f - (y - x) *\<^sub>R f x) {x..y}"
+        apply (rule has_integral_sub)
+        using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
+        using has_integral_const_real [of "f x" x y] False
+        apply (simp add: )
+        done
+      show ?thesis
+        using False
+        apply (simp add: abs_eq_content del: content_real_if)
+        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
+        using yx False d x y `e>0` apply (auto simp add: Idiff fux_int)
+        done
+    next
+      case True
+      have "f integrable_on {a..x}"
+        using f x by (simp add: integrable_subinterval_real)
+      then have Idiff: "?I a x - ?I a y = ?I y x" 
+        using True x y by (simp add: algebra_simps integral_combine)
+      have fux_int: "((\<lambda>u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}"
+        apply (rule has_integral_sub)
+        using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
+        using has_integral_const_real [of "f x" y x] True
+        apply (simp add: )
+        done
+      have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+        using True
+        apply (simp add: abs_eq_content del: content_real_if)
+        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
+        using yx True d x y `e>0` apply (auto simp add: Idiff fux_int)
+        done
+      then show ?thesis
+        by (simp add: algebra_simps norm_minus_commute)
+    qed
+    then have "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+      using `d>0` by blast 
+  } 
+  then show ?thesis
+    by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
+qed
+
 lemma integral_has_vector_derivative:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes "continuous_on {a .. b} f"
     and "x \<in> {a .. b}"
   shows "((\<lambda>u. integral {a .. u} f) has_vector_derivative f(x)) (at x within {a .. b})"
-  unfolding has_vector_derivative_def has_derivative_within_alt
-  apply safe
-  apply (rule bounded_linear_scaleR_left)
-proof -
-  fix e :: real
-  assume e: "e > 0"
-  note compact_uniformly_continuous[OF assms(1) compact_Icc,unfolded uniformly_continuous_on_def]
-  from this[rule_format,OF e] guess d by (elim conjE exE) note d=this[rule_format]
-  let ?I = "\<lambda>a b. integral {a .. b} f"
-  show "\<exists>d>0. \<forall>y\<in>{a .. b}. norm (y - x) < d \<longrightarrow>
-    norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)"
-  proof (rule, rule, rule d, safe, goal_cases)
-    case prems: (1 y)
-    show ?case
-    proof (cases "y < x")
-      case False
-      have "f integrable_on {a .. y}"
-        apply (rule integrable_subinterval_real,rule integrable_continuous_real)
-        apply (rule assms)
-        unfolding not_less
-        using assms(2) prems
-        apply auto
-        done
-      then have *: "?I a y - ?I a x = ?I x y"
-        unfolding algebra_simps
-        apply (subst eq_commute)
-        apply (rule integral_combine)
-        using False
-        unfolding not_less
-        using assms(2) prems
-        apply auto
-        done
-      have **: "norm (y - x) = content {x .. y}"
-        using False by (auto simp: content_real)
-      show ?thesis
-        unfolding **
-        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
-        unfolding *
-        defer
-        apply (rule has_integral_sub)
-        apply (rule integrable_integral)
-        apply (rule integrable_subinterval_real)
-        apply (rule integrable_continuous_real)
-        apply (rule assms)+
-      proof -
-        show "{x .. y} \<subseteq> {a .. b}"
-          using prems assms(2) by auto
-        have *: "y - x = norm (y - x)"
-          using False by auto
-        show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x .. y}"
-          apply (subst *)
-          unfolding **
-          by blast
-        show "\<forall>xa\<in>{x .. y}. norm (f xa - f x) \<le> e"
-          apply safe
-          apply (rule less_imp_le)
-          apply (rule d(2)[unfolded dist_norm])
-          using assms(2)
-          using prems
-          apply auto
-          done
-      qed (insert e, auto)
-    next
-      case True
-      have "f integrable_on cbox a x"
-        apply (rule integrable_subinterval,rule integrable_continuous)
-        unfolding box_real
-        apply (rule assms)+
-        unfolding not_less
-        using assms(2) prems
-        apply auto
-        done
-      then have *: "?I a x - ?I a y = ?I y x"
-        unfolding algebra_simps
-        apply (subst eq_commute)
-        apply (rule integral_combine)
-        using True using assms(2) prems
-        apply auto
-        done
-      have **: "norm (y - x) = content {y .. x}"
-        apply (subst content_real)
-        using True
-        unfolding not_less
-        apply auto
-        done
-      have ***: "\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)"
-        unfolding scaleR_left.diff by auto
-      show ?thesis
-        apply (subst ***)
-        unfolding norm_minus_cancel **
-        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
-        unfolding *
-        unfolding o_def
-        defer
-        apply (rule has_integral_sub)
-        apply (subst minus_minus[symmetric])
-        unfolding minus_minus
-        apply (rule integrable_integral)
-        apply (rule integrable_subinterval_real,rule integrable_continuous_real)
-        apply (rule assms)+
-      proof -
-        show "{y .. x} \<subseteq> {a .. b}"
-          using prems assms(2) by auto
-        have *: "x - y = norm (y - x)"
-          using True by auto
-        show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y .. x}"
-          apply (subst *)
-          unfolding **
-          apply blast
-          done
-        show "\<forall>xa\<in>{y .. x}. norm (f xa - f x) \<le> e"
-          apply safe
-          apply (rule less_imp_le)
-          apply (rule d(2)[unfolded dist_norm])
-          using assms(2)
-          using prems
-          apply auto
-          done
-      qed (insert e, auto)
-    qed
-  qed
-qed
+apply (rule integral_has_vector_derivative_continuous_at [OF integrable_continuous_real])
+using assms
+apply (auto simp: continuous_on_eq_continuous_within)
+done
 
 lemma antiderivative_continuous:
   fixes q b :: real
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -437,11 +437,8 @@
   apply (auto simp: continuous_on_op_minus)
   done
 
-lemma forall_01_trivial: "(\<forall>x\<in>{0..1}. x \<le> 0 \<longrightarrow> P x) \<longleftrightarrow> P (0::real)"
-  by auto
-
-lemma forall_half1_trivial: "(\<forall>x\<in>{1/2..1}. x * 2 \<le> 1 \<longrightarrow> P x) \<longleftrightarrow> P (1/2::real)"
-  by auto (metis add_divide_distrib mult_2_right real_sum_of_halves)
+lemma half_bounded_equal: "1 \<le> x * 2 \<Longrightarrow> x * 2 \<le> 1 \<longleftrightarrow> x = (1/2::real)"
+  by simp
 
 lemma continuous_on_joinpaths:
   assumes "continuous_on {0..1} g1" "continuous_on {0..1} g2" "pathfinish g1 = pathstart g2"
@@ -451,17 +448,17 @@
     by auto
   have gg: "g2 0 = g1 1"
     by (metis assms(3) pathfinish_def pathstart_def)
-  have 1: "continuous_on {0..1 / 2} (g1 +++ g2)"
+  have 1: "continuous_on {0..1/2} (g1 +++ g2)"
     apply (rule continuous_on_eq [of _ "g1 o (\<lambda>x. 2*x)"])
-    apply (simp add: joinpaths_def)
-    apply (rule continuous_intros | simp add: assms)+
+    apply (rule continuous_intros | simp add: joinpaths_def assms)+
     done
-  have 2: "continuous_on {1 / 2..1} (g1 +++ g2)"
-    apply (rule continuous_on_eq [of _ "g2 o (\<lambda>x. 2*x-1)"])
-    apply (simp add: joinpaths_def)
-    apply (rule continuous_intros | simp add: forall_half1_trivial gg)+
-    apply (rule continuous_on_subset)
-    apply (rule assms, auto)
+  have "continuous_on {1/2..1} (g2 o (\<lambda>x. 2*x-1))"
+    apply (rule continuous_on_subset [of "{1/2..1}"])
+    apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff assms)+
+    done
+  then have 2: "continuous_on {1/2..1} (g1 +++ g2)"
+    apply (rule continuous_on_eq [of "{1/2..1}" "g2 o (\<lambda>x. 2*x-1)"])
+    apply (rule assms continuous_intros | simp add: joinpaths_def mult.commute half_bounded_equal gg)+
     done
   show ?thesis
     apply (subst *)
@@ -800,7 +797,6 @@
     apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"])
     prefer 3
     apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"])
-    defer
     prefer 3
     apply (rule continuous_intros)+
     prefer 2
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -2309,13 +2309,7 @@
 
 subsection \<open>More properties of closed balls\<close>
 
-lemma closed_vimage: (* TODO: move to Topological_Spaces.thy *)
-  assumes "closed s" and "continuous_on UNIV f"
-  shows "closed (vimage f s)"
-  using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
-  by simp
-
-lemma closed_cball: "closed (cball x e)"
+lemma closed_cball [iff]: "closed (cball x e)"
 proof -
   have "closed (dist x -` {..e})"
     by (intro closed_vimage closed_atMost continuous_intros)
@@ -4663,7 +4657,7 @@
   by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE)
 
 lemma continuous_on_eq:
-  "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
+  "\<lbrakk>continuous_on s f; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on s g"
   unfolding continuous_on_def tendsto_def eventually_at_topological
   by simp
 
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/ROOT	Mon Sep 21 21:43:09 2015 +0200
@@ -169,6 +169,15 @@
   options [document = false]
   theories EvenOdd
 
+session "HOL-Data_Structures" in Data_Structures = HOL +
+  options [document_variants = document]
+  theories [document = false]
+    "Less_False"
+  theories
+    Tree_Set
+    Tree_Map
+  document_files "root.tex"
+
 session "HOL-Import" in Import = HOL +
   theories HOL_Light_Maps
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Real.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -22,6 +22,13 @@
 
 subsection \<open>Preliminary lemmas\<close>
 
+lemma inj_add_left [simp]: 
+  fixes x :: "'a::cancel_semigroup_add" shows "inj (op+ x)"
+by (meson add_left_imp_eq injI)
+
+lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)"
+  by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
+
 lemma add_diff_add:
   fixes a b c d :: "'a::ab_group_add"
   shows "(a + c) - (b + d) = (a - b) + (c - d)"
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -863,6 +863,14 @@
   using image_affinity_atLeastAtMost [of m "-c" a b]
   by simp
 
+lemma image_affinity_atLeastAtMost_div:
+  fixes c :: "'a::linordered_field"
+  shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {a/m + c .. b/m + c}
+            else {b/m + c .. a/m + c})"
+  using image_affinity_atLeastAtMost [of "inverse m" c a b]
+  by (simp add: field_class.field_divide_inverse algebra_simps)
+    
 lemma image_affinity_atLeastAtMost_div_diff:
   fixes c :: "'a::linordered_field"
   shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
diff -r 1bb5a10b8ce0 -r bf194f7c4c8e src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Sep 21 20:45:57 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Sep 21 21:43:09 2015 +0200
@@ -1392,6 +1392,10 @@
   "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
   unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
 
+lemma continuous_on_open_Un:
+  "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
+  using continuous_on_open_Union [of "{s,t}"] by auto
+
 lemma continuous_on_closed_Un:
   "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
   by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)