--- a/NEWS Tue Aug 15 18:15:04 2017 +0200
+++ b/NEWS Tue Aug 15 22:23:28 2017 +0200
@@ -131,8 +131,11 @@
* Material on infinite products in HOL-Analysis
-* "sublist" from theory List renamed to "nths" in analogy with "nth".
-"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
+* Theory List:
+ "sublist" renamed to "nths" in analogy with "nth".
+ "sublisteq" renamed to "subseq".
+ Minor INCOMPATIBILITY.
+ New generic function "sorted_wrt"
* Theories "GCD" and "Binomial" are already included in "Main" (instead
of "Complex_Main").
--- a/src/Doc/Main/Main_Doc.thy Tue Aug 15 18:15:04 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy Tue Aug 15 22:23:28 2017 +0200
@@ -563,6 +563,7 @@
@{const List.shuffle} & @{typeof List.shuffle}\\
@{const List.sort} & @{typeof List.sort}\\
@{const List.sorted} & @{typeof List.sorted}\\
+@{const List.sorted_wrt} & @{typeof List.sorted_wrt}\\
@{const List.splice} & @{typeof List.splice}\\
@{const List.take} & @{typeof List.take}\\
@{const List.takeWhile} & @{typeof List.takeWhile}\\
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Tue Aug 15 22:23:28 2017 +0200
@@ -0,0 +1,836 @@
+(* Author: Peter Lammich *)
+
+section \<open>Binomial Heap\<close>
+
+theory Binomial_Heap
+imports
+ Complex_Main
+ Priority_Queue
+begin
+
+lemma sum_power2: "(\<Sum>i\<in>{0..<k}. (2::nat)^i) = 2^k-1"
+by (induction k) auto
+
+text \<open>
+ We formalize the binomial heap presentation from Okasaki's book.
+ We show the functional correctness and complexity of all operations.
+
+ The presentation is engineered for simplicity, and most
+ proofs are straightforward and automatic.
+\<close>
+
+subsection \<open>Binomial Tree and Heap Datatype\<close>
+
+datatype 'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")
+
+type_synonym 'a heap = "'a tree list"
+
+subsubsection \<open>Multiset of elements\<close>
+
+fun mset_tree :: "'a::linorder tree \<Rightarrow> 'a multiset" where
+ "mset_tree (Node _ a c) = {#a#} + (\<Sum>t\<in>#mset c. mset_tree t)"
+
+definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where
+ "mset_heap c = (\<Sum>t\<in>#mset c. mset_tree t)"
+
+lemma mset_tree_simp_alt[simp]:
+ "mset_tree (Node r a c) = {#a#} + mset_heap c"
+ unfolding mset_heap_def by auto
+declare mset_tree.simps[simp del]
+
+lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}"
+ by (cases t) auto
+
+lemma mset_heap_Nil[simp]:
+ "mset_heap [] = {#}"
+ unfolding mset_heap_def
+ by auto
+
+lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts"
+ unfolding mset_heap_def by auto
+
+lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]"
+ unfolding mset_heap_def by auto
+
+lemma root_in_mset[simp]: "root t \<in># mset_tree t" by (cases t) auto
+
+lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts"
+ unfolding mset_heap_def by auto
+
+subsubsection \<open>Invariants\<close>
+
+text \<open>Binomial invariant\<close>
+fun invar_btree :: "'a::linorder tree \<Rightarrow> bool"
+ where
+ "invar_btree (Node r x ts) \<longleftrightarrow>
+ (\<forall>t\<in>set ts. invar_btree t)
+ \<and> (map rank ts = rev [0..<r])"
+
+definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
+ "invar_bheap ts
+ \<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (op <) (map rank ts))"
+
+text \<open>Ordering (heap) invariant\<close>
+fun otree_invar :: "'a::linorder tree \<Rightarrow> bool"
+ where
+ "otree_invar (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. otree_invar t \<and> x \<le> root t)"
+
+definition oheap_invar :: "'a::linorder heap \<Rightarrow> bool" where
+ "oheap_invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. otree_invar t)"
+
+definition invar :: "'a::linorder heap \<Rightarrow> bool" where
+ "invar ts \<longleftrightarrow> invar_bheap ts \<and> oheap_invar ts"
+
+text \<open>The children of a node are a valid heap\<close>
+lemma children_oheap_invar:
+ "otree_invar (Node r v ts) \<Longrightarrow> oheap_invar (rev ts)"
+ by (auto simp: oheap_invar_def)
+
+lemma children_invar_bheap:
+ "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"
+ by (auto simp: invar_bheap_def rev_map[symmetric])
+
+subsection \<open>Operations\<close>
+
+definition link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+ "link t\<^sub>1 t\<^sub>2 = (case (t\<^sub>1,t\<^sub>2) of (Node r x\<^sub>1 c\<^sub>1, Node _ x\<^sub>2 c\<^sub>2) \<Rightarrow>
+ if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#c\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#c\<^sub>2)
+ )"
+
+lemma link_invar_btree:
+ assumes "invar_btree t\<^sub>1"
+ assumes "invar_btree t\<^sub>2"
+ assumes "rank t\<^sub>1 = rank t\<^sub>2"
+ shows "invar_btree (link t\<^sub>1 t\<^sub>2)"
+ using assms
+ unfolding link_def
+ by (force split: tree.split )
+
+lemma link_otree_invar:
+ assumes "otree_invar t\<^sub>1"
+ assumes "otree_invar t\<^sub>2"
+ shows "otree_invar (link t\<^sub>1 t\<^sub>2)"
+ using assms
+ unfolding link_def
+ by (auto split: tree.split)
+
+lemma link_rank[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
+ unfolding link_def
+ by (auto split: tree.split)
+
+lemma link_mset[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
+ unfolding link_def
+ by (auto split: tree.split)
+
+fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+ "ins_tree t [] = [t]"
+| "ins_tree t\<^sub>1 (t\<^sub>2#ts) = (
+ if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#ts else ins_tree (link t\<^sub>1 t\<^sub>2) ts
+ )"
+
+lemma invar_bheap_Cons[simp]:
+ "invar_bheap (t#ts)
+ \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
+ unfolding invar_bheap_def
+ by (auto simp: sorted_wrt_Cons)
+
+lemma ins_tree_invar_btree:
+ assumes "invar_btree t"
+ assumes "invar_bheap ts"
+ assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"
+ shows "invar_bheap (ins_tree t ts)"
+ using assms
+ apply (induction t ts rule: ins_tree.induct)
+ apply (auto simp: link_invar_btree less_eq_Suc_le[symmetric])
+ done
+
+lemma oheap_invar_Cons[simp]:
+ "oheap_invar (t#ts) \<longleftrightarrow> otree_invar t \<and> oheap_invar ts"
+ unfolding oheap_invar_def by auto
+
+lemma ins_tree_otree_invar:
+ assumes "otree_invar t"
+ assumes "oheap_invar ts"
+ shows "oheap_invar (ins_tree t ts)"
+ using assms
+ apply (induction t ts rule: ins_tree.induct)
+ apply (auto simp: link_otree_invar)
+ done
+
+lemma ins_tree_mset[simp]:
+ "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"
+ by (induction t ts rule: ins_tree.induct) auto
+
+lemma ins_tree_rank_bound:
+ assumes "t' \<in> set (ins_tree t ts)"
+ assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'"
+ assumes "rank t\<^sub>0 < rank t"
+ shows "rank t\<^sub>0 < rank t'"
+ using assms
+ by (induction t ts rule: ins_tree.induct) (auto split: if_splits)
+
+
+definition ins :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+ "ins x ts = ins_tree (Node 0 x []) ts"
+
+lemma ins_invar[simp]: "invar t \<Longrightarrow> invar (ins x t)"
+ unfolding ins_def invar_def
+ by (auto intro!: ins_tree_invar_btree simp: ins_tree_otree_invar)
+
+lemma ins_mset[simp]: "mset_heap (ins x t) = {#x#} + mset_heap t"
+ unfolding ins_def
+ by auto
+
+fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+ "merge ts\<^sub>1 [] = ts\<^sub>1"
+| "merge [] ts\<^sub>2 = ts\<^sub>2"
+| "merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = (
+ if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2)
+ else if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2#merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
+ else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
+ )"
+
+lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" by (cases ts\<^sub>2) auto
+
+lemma merge_rank_bound:
+ assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)"
+ assumes "\<forall>t'\<in>set ts\<^sub>1. rank t < rank t'"
+ assumes "\<forall>t'\<in>set ts\<^sub>2. rank t < rank t'"
+ shows "rank t < rank t'"
+ using assms
+ apply (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
+ apply (auto split: if_splits simp: ins_tree_rank_bound)
+ done
+
+lemma merge_invar_bheap:
+ assumes "invar_bheap ts\<^sub>1"
+ assumes "invar_bheap ts\<^sub>2"
+ shows "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
+ using assms
+proof (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
+ case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2)
+
+ from "3.prems" have [simp]: "invar_btree t\<^sub>1" "invar_btree t\<^sub>2"
+ by auto
+
+ consider (LT) "rank t\<^sub>1 < rank t\<^sub>2"
+ | (GT) "rank t\<^sub>1 > rank t\<^sub>2"
+ | (EQ) "rank t\<^sub>1 = rank t\<^sub>2"
+ using antisym_conv3 by blast
+ then show ?case proof cases
+ case LT
+ then show ?thesis using 3
+ by (force elim!: merge_rank_bound)
+ next
+ case GT
+ then show ?thesis using 3
+ by (force elim!: merge_rank_bound)
+ next
+ case [simp]: EQ
+
+ from "3.IH"(3) "3.prems" have [simp]: "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
+ by auto
+
+ have "rank t\<^sub>2 < rank t'" if "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" for t'
+ using that
+ apply (rule merge_rank_bound)
+ using "3.prems" by auto
+ with EQ show ?thesis
+ by (auto simp: Suc_le_eq ins_tree_invar_btree link_invar_btree)
+ qed
+qed simp_all
+
+lemma merge_oheap_invar:
+ assumes "oheap_invar ts\<^sub>1"
+ assumes "oheap_invar ts\<^sub>2"
+ shows "oheap_invar (merge ts\<^sub>1 ts\<^sub>2)"
+ using assms
+ apply (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
+ apply (auto simp: ins_tree_otree_invar link_otree_invar)
+ done
+
+lemma merge_invar[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
+ unfolding invar_def by (auto simp: merge_invar_bheap merge_oheap_invar)
+
+lemma merge_mset[simp]:
+ "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
+ by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto
+
+
+fun find_min :: "'a::linorder heap \<Rightarrow> 'a" where
+ "find_min [t] = root t"
+| "find_min (t#ts) = (let x=root t;
+ y=find_min ts
+ in if x\<le>y then x else y)"
+
+lemma otree_invar_root_min:
+ assumes "otree_invar t"
+ assumes "x \<in># mset_tree t"
+ shows "root t \<le> x"
+ using assms
+ apply (induction t arbitrary: x rule: mset_tree.induct)
+ apply (force simp: mset_heap_def)
+ done
+
+
+lemma find_min_mset_aux:
+ assumes "ts\<noteq>[]"
+ assumes "oheap_invar ts"
+ assumes "x \<in># mset_heap ts"
+ shows "find_min ts \<le> x"
+ using assms
+ apply (induction ts arbitrary: x rule: find_min.induct)
+ apply (auto
+ simp: Let_def otree_invar_root_min intro: order_trans;
+ meson linear order_trans otree_invar_root_min
+ )+
+ done
+
+lemma find_min_mset:
+ assumes "ts\<noteq>[]"
+ assumes "invar ts"
+ assumes "x \<in># mset_heap ts"
+ shows "find_min ts \<le> x"
+ using assms unfolding invar_def
+ by (auto simp: find_min_mset_aux)
+
+
+lemma find_min_member:
+ assumes "ts\<noteq>[]"
+ shows "find_min ts \<in># mset_heap ts"
+ using assms
+ apply (induction ts rule: find_min.induct)
+ apply (auto simp: Let_def)
+ done
+
+lemma find_min:
+ assumes "mset_heap ts \<noteq> {#}"
+ assumes "invar ts"
+ shows "find_min ts = Min_mset (mset_heap ts)"
+ using assms find_min_member find_min_mset
+ by (auto simp: eq_Min_iff)
+
+
+fun get_min :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where
+ "get_min [t] = (t,[])"
+| "get_min (t#ts) = (let (t',ts') = get_min ts
+ in if root t \<le> root t' then (t,ts) else (t',t#ts'))"
+
+
+lemma get_min_find_min_same_root:
+ assumes "ts\<noteq>[]"
+ assumes "get_min ts = (t',ts')"
+ shows "root t' = find_min ts"
+ using assms
+ apply (induction ts arbitrary: t' ts' rule: find_min.induct)
+ apply (auto simp: Let_def split: prod.splits)
+ done
+
+lemma get_min_mset:
+ assumes "get_min ts = (t',ts')"
+ assumes "ts\<noteq>[]"
+ shows "mset ts = {#t'#} + mset ts'"
+ using assms
+ apply (induction ts arbitrary: t' ts' rule: find_min.induct)
+ apply (auto split: prod.splits if_splits)
+ done
+
+lemma get_min_set:
+ assumes "get_min ts = (t', ts')"
+ assumes "ts\<noteq>[]"
+ shows "set ts = insert t' (set ts')"
+ using get_min_mset[OF assms, THEN arg_cong[where f=set_mset]]
+ by auto
+
+
+lemma get_min_invar_bheap:
+ assumes "get_min ts = (t',ts')"
+ assumes "ts\<noteq>[]"
+ assumes "invar_bheap ts"
+ shows "invar_btree t'" and "invar_bheap ts'"
+proof -
+ have "invar_btree t' \<and> invar_bheap ts'"
+ using assms
+ proof (induction ts arbitrary: t' ts' rule: find_min.induct)
+ case (2 t v va)
+ then show ?case
+ apply (clarsimp split: prod.splits if_splits)
+ apply (drule get_min_set; fastforce)
+ done
+ qed auto
+ thus "invar_btree t'" and "invar_bheap ts'" by auto
+qed
+
+lemma get_min_oheap_invar:
+ assumes "get_min ts = (t',ts')"
+ assumes "ts\<noteq>[]"
+ assumes "oheap_invar ts"
+ shows "otree_invar t'" and "oheap_invar ts'"
+ using assms
+ apply (induction ts arbitrary: t' ts' rule: find_min.induct)
+ apply (auto split: prod.splits if_splits)
+ done
+
+definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
+"del_min ts = (case get_min ts of
+ (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
+
+lemma del_min_invar[simp]:
+ assumes "ts \<noteq> []"
+ assumes "invar ts"
+ shows "invar (del_min ts)"
+ using assms
+ unfolding invar_def del_min_def
+ by (auto
+ split: prod.split tree.split
+ intro!: merge_invar_bheap merge_oheap_invar
+ dest: get_min_invar_bheap get_min_oheap_invar
+ intro!: children_oheap_invar children_invar_bheap
+ )
+
+lemma del_min_mset:
+ assumes "ts \<noteq> []"
+ shows "mset_heap ts = mset_heap (del_min ts) + {# find_min ts #}"
+ using assms
+ unfolding del_min_def
+ apply (clarsimp split: tree.split prod.split)
+ apply (frule (1) get_min_find_min_same_root)
+ apply (frule (1) get_min_mset)
+ apply (auto simp: mset_heap_def)
+ done
+
+subsection \<open>Complexity\<close>
+
+text \<open>The size of a binomial tree is determined by its rank\<close>
+lemma size_btree:
+ assumes "invar_btree t"
+ shows "size (mset_tree t) = 2^rank t"
+ using assms
+proof (induction t)
+ case (Node r v ts)
+ hence IH: "size (mset_tree t) = 2^rank t" if "t \<in> set ts" for t
+ using that by auto
+
+ from Node have COMPL: "map rank ts = rev [0..<r]" by auto
+
+ have "size (mset_heap ts) = (\<Sum>t\<leftarrow>ts. size (mset_tree t))"
+ by (induction ts) auto
+ also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH
+ by (auto cong: sum_list_cong)
+ also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)"
+ by (induction ts) auto
+ also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)"
+ unfolding COMPL
+ by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat)
+ also have "\<dots> = 2^r - 1"
+ by (induction r) auto
+ finally show ?case
+ by (simp)
+qed
+
+text \<open>The length of a binomial heap is bounded by the number of its elements\<close>
+lemma size_bheap:
+ assumes "invar_bheap ts"
+ shows "2^length ts \<le> size (mset_heap ts) + 1"
+proof -
+ from \<open>invar_bheap ts\<close> have
+ ASC: "sorted_wrt (op <) (map rank ts)" and
+ TINV: "\<forall>t\<in>set ts. invar_btree t"
+ unfolding invar_bheap_def by auto
+
+ have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1"
+ by (simp add: sum_power2)
+ also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
+ using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "op ^ (2::nat)"]
+ using power_increasing[where a="2::nat"]
+ by (auto simp: o_def)
+ also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV
+ by (auto cong: sum_list_cong simp: size_btree)
+ also have "\<dots> = size (mset_heap ts) + 1"
+ unfolding mset_heap_def by (induction ts) auto
+ finally show ?thesis .
+qed
+
+subsubsection \<open>Timing Functions\<close>
+text \<open>
+ We define timing functions for each operation, and provide
+ estimations of their complexity.
+\<close>
+definition t_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
+[simp]: "t_link _ _ = 1"
+
+fun t_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
+ "t_ins_tree t [] = 1"
+| "t_ins_tree t\<^sub>1 (t\<^sub>2#rest) = (
+ (if rank t\<^sub>1 < rank t\<^sub>2 then 1
+ else t_link t\<^sub>1 t\<^sub>2 + t_ins_tree (link t\<^sub>1 t\<^sub>2) rest)
+ )"
+
+
+definition t_ins :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
+ "t_ins x ts = t_ins_tree (Node 0 x []) ts"
+
+lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1" for t
+ by (induction t ts rule: t_ins_tree.induct) auto
+
+lemma t_ins_bound:
+ assumes "invar ts"
+ shows "t_ins x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
+proof -
+
+ have 1: "t_ins x ts \<le> length ts + 1"
+ unfolding t_ins_def by (rule t_ins_tree_simple_bound)
+ also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))"
+ proof -
+ from size_bheap[of ts] assms
+ have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+ unfolding invar_def by auto
+ hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto
+ thus ?thesis using le_log2_of_power by blast
+ qed
+ finally show ?thesis
+ by (simp only: log_mult of_nat_mult) auto
+qed
+
+fun t_merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> nat" where
+ "t_merge ts\<^sub>1 [] = 1"
+| "t_merge [] ts\<^sub>2 = 1"
+| "t_merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = 1 + (
+ if rank t\<^sub>1 < rank t\<^sub>2 then t_merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2)
+ else if rank t\<^sub>2 < rank t\<^sub>1 then t_merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
+ else t_ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) + t_merge ts\<^sub>1 ts\<^sub>2
+ )"
+
+text \<open>A crucial idea is to estimate the time in correlation with the
+ result length, as each carry reduces the length of the result.\<close>
+lemma l_ins_tree_estimate:
+ "t_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
+by (induction t ts rule: ins_tree.induct) auto
+
+lemma l_merge_estimate:
+ "length (merge ts\<^sub>1 ts\<^sub>2) + t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1"
+ apply (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct)
+ apply (auto simp: l_ins_tree_estimate algebra_simps)
+ done
+
+text \<open>Finally, we get the desired logarithmic bound\<close>
+lemma t_merge_bound_aux:
+ fixes ts\<^sub>1 ts\<^sub>2
+ defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
+ defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
+ assumes BINVARS: "invar_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2"
+ shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
+proof -
+ define n where "n = n\<^sub>1 + n\<^sub>2"
+
+ from l_merge_estimate[of ts\<^sub>1 ts\<^sub>2]
+ have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" by auto
+ hence "(2::nat)^t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)"
+ by (rule power_increasing) auto
+ also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2"
+ by (auto simp: algebra_simps power_add power_mult)
+ also note BINVARS(1)[THEN size_bheap]
+ also note BINVARS(2)[THEN size_bheap]
+ finally have "2 ^ t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2"
+ by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
+ from le_log2_of_power[OF this] have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>"
+ by simp
+ also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)"
+ by (simp add: log_mult log_nat_power)
+ also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
+ finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n + 1)"
+ by auto
+ also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
+ finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
+ by auto
+ also have "log 2 2 \<le> 2" by auto
+ finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
+ thus ?thesis unfolding n_def by (auto simp: algebra_simps)
+qed
+
+lemma t_merge_bound:
+ fixes ts\<^sub>1 ts\<^sub>2
+ defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
+ defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
+ assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
+ shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
+using assms t_merge_bound_aux unfolding invar_def by blast
+
+
+fun t_find_min :: "'a::linorder heap \<Rightarrow> nat" where
+ "t_find_min [t] = 1"
+| "t_find_min (t#ts) = 1 + t_find_min ts"
+
+lemma t_find_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_find_min ts = length ts"
+by (induction ts rule: t_find_min.induct) auto
+
+lemma t_find_min_bound:
+ assumes "invar ts"
+ assumes "ts\<noteq>[]"
+ shows "t_find_min ts \<le> log 2 (size (mset_heap ts) + 1)"
+proof -
+ have 1: "t_find_min ts = length ts" using assms t_find_min_estimate by auto
+ also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
+ proof -
+ from size_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+ unfolding invar_def by auto
+ thus ?thesis using le_log2_of_power by blast
+ qed
+ finally show ?thesis by auto
+qed
+
+fun t_get_min :: "'a::linorder heap \<Rightarrow> nat" where
+ "t_get_min [t] = 1"
+| "t_get_min (t#ts) = 1 + t_get_min ts"
+
+lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts"
+ by (induction ts rule: t_get_min.induct) auto
+
+lemma t_get_min_bound_aux:
+ assumes "invar_bheap ts"
+ assumes "ts\<noteq>[]"
+ shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
+proof -
+ have 1: "t_get_min ts = length ts" using assms t_get_min_estimate by auto
+ also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
+ proof -
+ from size_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+ by auto
+ thus ?thesis using le_log2_of_power by blast
+ qed
+ finally show ?thesis by auto
+qed
+
+lemma t_get_min_bound:
+ assumes "invar ts"
+ assumes "ts\<noteq>[]"
+ shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
+ using assms t_get_min_bound_aux unfolding invar_def by blast
+
+thm fold_simps -- \<open>Theorems used by code generator\<close>
+fun t_fold :: "('a \<Rightarrow> 'b \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> nat"
+ where
+ "t_fold t_f f [] s = 1"
+| "t_fold t_f f (x # xs) s = t_f x s + t_fold t_f f xs (f x s)"
+
+text \<open>Estimation for constant function is enough for our purpose\<close>
+lemma t_fold_const_bound:
+ shows "t_fold (\<lambda>_ _. K) f l s = K*length l + 1"
+ by (induction l arbitrary: s) auto
+
+lemma t_fold_bounded_bound:
+ assumes "\<forall>x s. x\<in>set l \<longrightarrow> t_f x s \<le> K"
+ shows "t_fold t_f f l s \<le> K*length l + 1"
+ using assms
+ apply (induction l arbitrary: s)
+ apply (simp; fail)
+ using add_mono
+ by (fastforce simp: algebra_simps)
+
+thm rev_conv_fold -- \<open>Theorem used by code generator\<close>
+definition "t_rev xs = t_fold (\<lambda>_ _. 1) op # xs []"
+lemma t_rev_bound: "t_rev xs = length xs + 1"
+ unfolding t_rev_def t_fold_const_bound by auto
+
+definition t_del_min :: "'a::linorder heap \<Rightarrow> nat"
+ where
+ "t_del_min ts = t_get_min ts + (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
+ \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2
+ )"
+
+lemma t_rev_ts1_bound_aux:
+ fixes ts
+ defines "n \<equiv> size (mset_heap ts)"
+ assumes BINVAR: "invar_bheap (rev ts)"
+ shows "t_rev ts \<le> 1 + log 2 (n+1)"
+proof -
+ have "t_rev ts = length ts + 1"
+ by (auto simp: t_rev_bound)
+ hence "2^t_rev ts = 2*2^length ts" by auto
+ also have "\<dots> \<le> 2*n+2" using size_bheap[OF BINVAR] by (auto simp: n_def)
+ finally have "2 ^ t_rev ts \<le> 2 * n + 2" .
+ from le_log2_of_power[OF this] have "t_rev ts \<le> log 2 (2 * (n + 1))"
+ by auto
+ also have "\<dots> = 1 + log 2 (n+1)"
+ by (simp only: of_nat_mult log_mult) auto
+ finally show ?thesis by (auto simp: algebra_simps)
+qed
+
+
+lemma t_del_min_bound_aux:
+ fixes ts
+ defines "n \<equiv> size (mset_heap ts)"
+ assumes BINVAR: "invar_bheap ts"
+ assumes "ts\<noteq>[]"
+ shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
+proof -
+ obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
+ by (metis surj_pair tree.exhaust_sel)
+
+ note BINVAR' = get_min_invar_bheap[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
+ hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: children_invar_bheap)
+
+ define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
+ define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
+
+ have t_rev_ts1_bound: "t_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)"
+ proof -
+ note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def]
+ also have "n\<^sub>1 \<le> n"
+ unfolding n\<^sub>1_def n_def
+ using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
+ by (auto simp: mset_heap_def)
+ finally show ?thesis by (auto simp: algebra_simps)
+ qed
+
+ have "t_del_min ts = t_get_min ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
+ unfolding t_del_min_def by (simp add: GM)
+ also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
+ using t_get_min_bound_aux[OF assms(2-)] by (auto simp: n_def)
+ also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
+ using t_rev_ts1_bound by auto
+ also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
+ using t_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
+ by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
+ also have "n\<^sub>1 + n\<^sub>2 \<le> n"
+ unfolding n\<^sub>1_def n\<^sub>2_def n_def
+ using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
+ by (auto simp: mset_heap_def)
+ finally have "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
+ by auto
+ thus ?thesis by (simp add: algebra_simps)
+qed
+
+lemma t_del_min_bound:
+ fixes ts
+ defines "n \<equiv> size (mset_heap ts)"
+ assumes "invar ts"
+ assumes "ts\<noteq>[]"
+ shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
+ using assms t_del_min_bound_aux unfolding invar_def by blast
+
+subsection \<open>Instantiating the Priority Queue Locale\<close>
+
+interpretation binheap:
+ Priority_Queue "[]" "op = []" ins find_min del_min invar mset_heap
+proof (unfold_locales, goal_cases)
+ case 1
+ then show ?case by simp
+next
+ case (2 q)
+ then show ?case by auto
+next
+ case (3 q x)
+ then show ?case by auto
+next
+ case (4 q)
+ then show ?case using del_min_mset[of q] find_min[OF _ \<open>invar q\<close>]
+ by (auto simp: union_single_eq_diff)
+next
+ case (5 q)
+ then show ?case using find_min[of q] by auto
+next
+ case 6
+ then show ?case by (auto simp add: invar_def invar_bheap_def oheap_invar_def)
+next
+ case (7 q x)
+ then show ?case by simp
+next
+ case (8 q)
+ then show ?case by simp
+qed
+
+
+(* Exercise? *)
+subsection \<open>Combined Find and Delete Operation\<close>
+
+text \<open>We define an operation that returns the minimum element and
+ a heap with this element removed. \<close>
+definition pop_min :: "'a::linorder heap \<Rightarrow> 'a \<times> 'a::linorder heap"
+ where
+ "pop_min ts = (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
+ \<Rightarrow> (x,merge (rev ts\<^sub>1) ts\<^sub>2)
+ )"
+
+lemma pop_min_refine:
+ assumes "ts \<noteq> []"
+ shows "pop_min ts = (find_min ts, del_min ts)"
+ unfolding pop_min_def del_min_def
+ by (auto
+ split: prod.split tree.split
+ dest: get_min_find_min_same_root[OF assms])
+
+lemma pop_min_invar:
+ assumes "ts \<noteq> []"
+ assumes "invar ts"
+ assumes "pop_min ts = (x,ts')"
+ shows "invar ts'"
+ using del_min_invar[of ts] pop_min_refine[of ts] assms by simp
+
+lemma pop_min_mset:
+ assumes "ts \<noteq> []"
+ assumes "invar ts"
+ assumes "pop_min ts = (x,ts')"
+ shows "mset_heap ts = add_mset x (mset_heap ts')"
+ using del_min_mset[of ts] pop_min_refine[of ts] assms by simp
+
+lemma pop_min_min:
+ assumes "ts \<noteq> []"
+ assumes "invar ts"
+ assumes "pop_min ts = (x,ts')"
+ shows "\<forall>y\<in>#mset_heap ts'. x\<le>y"
+ using pop_min_refine[of ts] del_min_mset[of ts] find_min_mset[of ts] assms
+ by (auto simp del: binheap.mset_simps)
+
+
+definition t_pop_min :: "'a::linorder heap \<Rightarrow> nat"
+ where
+ "t_pop_min ts = t_get_min ts + (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
+ \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2
+ )"
+
+lemma t_pop_min_bound_aux:
+ fixes ts
+ defines "n \<equiv> size (mset_heap ts)"
+ assumes BINVAR: "invar_bheap ts"
+ assumes "ts\<noteq>[]"
+ shows "t_pop_min ts \<le> 6 * log 2 (n+1) + 3"
+proof -
+ obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
+ by (metis surj_pair tree.exhaust_sel)
+
+ note BINVAR' = get_min_invar_bheap[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
+ hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: children_invar_bheap)
+
+ define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
+ define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
+
+ have t_rev_ts1_bound: "t_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)"
+ proof -
+ note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def]
+ also have "n\<^sub>1 \<le> n"
+ unfolding n\<^sub>1_def n_def
+ using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
+ by (auto simp: mset_heap_def)
+ finally show ?thesis by (auto simp: algebra_simps)
+ qed
+
+ have "t_pop_min ts = t_get_min ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
+ unfolding t_pop_min_def by (simp add: GM)
+ also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
+ using t_get_min_bound_aux[OF assms(2-)] by (auto simp: n_def)
+ also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
+ using t_rev_ts1_bound by auto
+ also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
+ using t_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
+ by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
+ also have "n\<^sub>1 + n\<^sub>2 \<le> n"
+ unfolding n\<^sub>1_def n\<^sub>2_def n_def
+ using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
+ by (auto simp: mset_heap_def)
+ finally have "t_pop_min ts \<le> 6 * log 2 (n+1) + 3"
+ by auto
+ thus ?thesis by (simp add: algebra_simps)
+qed
+
+end
--- a/src/HOL/Groups_List.thy Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/Groups_List.thy Tue Aug 15 22:23:28 2017 +0200
@@ -286,6 +286,31 @@
with assms(1) show ?thesis by simp
qed
+text \<open>Summation of a strictly ascending sequence with length \<open>n\<close>
+ can be upper-bounded by summation over \<open>{0..<n}\<close>.\<close>
+
+lemma sorted_wrt_less_sum_mono_lowerbound:
+ fixes f :: "nat \<Rightarrow> ('b::ordered_comm_monoid_add)"
+ assumes mono: "\<And>x y. x\<le>y \<Longrightarrow> f x \<le> f y"
+ shows "sorted_wrt (op <) ns \<Longrightarrow>
+ (\<Sum>i\<in>{0..<length ns}. f i) \<le> (\<Sum>i\<leftarrow>ns. f i)"
+proof (induction ns rule: rev_induct)
+ case Nil
+ then show ?case by simp
+next
+ case (snoc n ns)
+ have "sum f {0..<length (ns @ [n])}
+ = sum f {0..<length ns} + f (length ns)"
+ by simp
+ also have "sum f {0..<length ns} \<le> sum_list (map f ns)"
+ using snoc by (auto simp: sorted_wrt_append)
+ also have "length ns \<le> n"
+ using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto
+ finally have "sum f {0..<length (ns @ [n])} \<le> sum_list (map f ns) + f n"
+ using mono add_mono by blast
+ thus ?case by simp
+qed
+
subsection \<open>Further facts about @{const List.n_lists}\<close>
--- a/src/HOL/Library/Multiset.thy Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Aug 15 22:23:28 2017 +0200
@@ -2086,7 +2086,7 @@
lemma set_sorted_list_of_multiset [simp]:
"set (sorted_list_of_multiset M) = set_mset M"
-by (induct M) (simp_all add: set_insort)
+by (induct M) (simp_all add: set_insort_key)
lemma sorted_list_of_mset_set [simp]:
"sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
--- a/src/HOL/List.thy Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/List.thy Tue Aug 15 22:23:28 2017 +0200
@@ -333,6 +333,17 @@
text\<open>The following simple sort functions are intended for proofs,
not for efficient implementations.\<close>
+text \<open>A sorted predicate w.r.t. a relation:\<close>
+
+fun sorted_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+"sorted_wrt P [] = True" |
+"sorted_wrt P [x] = True" |
+"sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
+
+(* FIXME: define sorted in terms of sorted_wrt *)
+
+text \<open>A class-based sorted predicate:\<close>
+
context linorder
begin
@@ -4844,73 +4855,69 @@
subsection \<open>Sorting\<close>
-text\<open>Currently it is not shown that @{const sort} returns a
-permutation of its input because the nicest proof is via multisets,
-which are not yet available. Alternatively one could define a function
-that counts the number of occurrences of an element in a list and use
-that instead of multisets to state the correctness property.\<close>
+
+subsubsection \<open>@{const sorted_wrt}\<close>
+
+lemma sorted_wrt_induct:
+ "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma sorted_wrt_Cons:
+assumes "transp P"
+shows "sorted_wrt P (x # xs) = ((\<forall>y \<in> set xs. P x y) \<and> sorted_wrt P xs)"
+by(induction xs arbitrary: x)(auto intro: transpD[OF assms])
+
+lemma sorted_wrt_ConsI:
+ "\<lbrakk> transp P; \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow>
+ sorted_wrt P (x # xs)"
+by (simp add: sorted_wrt_Cons)
+
+lemma sorted_wrt_append:
+assumes "transp P"
+shows "sorted_wrt P (xs @ ys) \<longleftrightarrow>
+ sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"
+by (induction xs) (auto simp: sorted_wrt_Cons[OF assms])
+
+lemma sorted_wrt_rev: assumes "transp P"
+shows "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
+proof(induction xs rule: sorted_wrt_induct)
+ case 3 thus ?case
+ by(simp add: sorted_wrt_append sorted_wrt_Cons assms)
+ (meson assms transpD)
+qed simp_all
+
+text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
+
+lemma sorted_wrt_upt[simp]: "sorted_wrt (op <) [0..<n]"
+by(induction n) (auto simp: sorted_wrt_append)
+
+text \<open>Each element is greater or equal to its index:\<close>
+
+lemma sorted_wrt_less_idx:
+ "sorted_wrt (op <) ns \<Longrightarrow> i < length ns \<Longrightarrow> i \<le> ns!i"
+proof (induction ns arbitrary: i rule: rev_induct)
+ case Nil thus ?case by simp
+next
+ case snoc
+ thus ?case
+ by (auto simp: nth_append sorted_wrt_append)
+ (metis less_antisym not_less nth_mem)
+qed
+
+
+subsubsection \<open>@{const sorted}\<close>
context linorder
begin
-lemma set_insort_key:
- "set (insort_key f x xs) = insert x (set xs)"
- by (induct xs) auto
-
-lemma length_insort [simp]:
- "length (insort_key f x xs) = Suc (length xs)"
- by (induct xs) simp_all
-
-lemma insort_key_left_comm:
- assumes "f x \<noteq> f y"
- shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
- by (induct xs) (auto simp add: assms dest: antisym)
-
-lemma insort_left_comm:
- "insort x (insort y xs) = insort y (insort x xs)"
- by (cases "x = y") (auto intro: insort_key_left_comm)
-
-lemma comp_fun_commute_insort:
- "comp_fun_commute insort"
-proof
-qed (simp add: insort_left_comm fun_eq_iff)
-
-lemma sort_key_simps [simp]:
- "sort_key f [] = []"
- "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
- by (simp_all add: sort_key_def)
-
-lemma (in linorder) sort_key_conv_fold:
- assumes "inj_on f (set xs)"
- shows "sort_key f xs = fold (insort_key f) xs []"
-proof -
- have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
- proof (rule fold_rev, rule ext)
- fix zs
- fix x y
- assume "x \<in> set xs" "y \<in> set xs"
- with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
- have **: "x = y \<longleftrightarrow> y = x" by auto
- show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
- by (induct zs) (auto intro: * simp add: **)
- qed
- then show ?thesis by (simp add: sort_key_def foldr_conv_fold)
-qed
-
-lemma (in linorder) sort_conv_fold:
- "sort xs = fold insort xs []"
- by (rule sort_key_conv_fold) simp
-
-lemma length_sort[simp]: "length (sort_key f xs) = length xs"
-by (induct xs, auto)
-
-lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
-apply(induct xs arbitrary: x) apply simp
+lemma sorted_Cons: "sorted (x#xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x \<le> y))"
+apply(induction xs arbitrary: x)
+ apply simp
by simp (blast intro: order_trans)
lemma sorted_tl:
"sorted xs \<Longrightarrow> sorted (tl xs)"
- by (cases xs) (simp_all add: sorted_Cons)
+by (cases xs) (simp_all add: sorted_Cons)
lemma sorted_append:
"sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
@@ -4954,86 +4961,22 @@
"sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
by (auto intro: sorted_nth_monoI sorted_nth_mono)
-lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"
-by (induct xs) auto
-
-lemma set_sort[simp]: "set(sort_key f xs) = set xs"
-by (induct xs) (simp_all add:set_insort)
-
-lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
-by(induct xs)(auto simp:set_insort)
-
-lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
- by (induct xs) (simp_all add: distinct_insort)
-
-lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
- by (induct xs) (auto simp:sorted_Cons set_insort)
-
-lemma sorted_insort: "sorted (insort x xs) = sorted xs"
- using sorted_insort_key [where f="\<lambda>x. x"] by simp
-
-theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
- by (induct xs) (auto simp:sorted_insort_key)
-
-theorem sorted_sort [simp]: "sorted (sort xs)"
- using sorted_sort_key [where f="\<lambda>x. x"] by simp
+lemma sorted_map_remove1:
+ "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
+by (induct xs) (auto simp add: sorted_Cons)
+
+lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
+using sorted_map_remove1 [of "\<lambda>x. x"] by simp
lemma sorted_butlast:
assumes "xs \<noteq> []" and "sorted xs"
shows "sorted (butlast xs)"
proof -
- from \<open>xs \<noteq> []\<close> obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
+ from \<open>xs \<noteq> []\<close> obtain ys y where "xs = ys @ [y]"
+ by (cases xs rule: rev_cases) auto
with \<open>sorted xs\<close> show ?thesis by (simp add: sorted_append)
qed
-lemma insort_not_Nil [simp]:
- "insort_key f a xs \<noteq> []"
- by (induct xs) simp_all
-
-lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
-by (cases xs) auto
-
-lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
- by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
-
-lemma sorted_map_remove1:
- "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
- by (induct xs) (auto simp add: sorted_Cons)
-
-lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
- using sorted_map_remove1 [of "\<lambda>x. x"] by simp
-
-lemma insort_key_remove1:
- assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
- shows "insort_key f a (remove1 a xs) = xs"
-using assms proof (induct xs)
- case (Cons x xs)
- then show ?case
- proof (cases "x = a")
- case False
- then have "f x \<noteq> f a" using Cons.prems by auto
- then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
- with \<open>f x \<noteq> f a\<close> show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
- qed (auto simp: sorted_Cons insort_is_Cons)
-qed simp
-
-lemma insort_remove1:
- assumes "a \<in> set xs" and "sorted xs"
- shows "insort a (remove1 a xs) = xs"
-proof (rule insort_key_remove1)
- define n where "n = length (filter (op = a) xs) - 1"
- from \<open>a \<in> set xs\<close> show "a \<in> set xs" .
- from \<open>sorted xs\<close> show "sorted (map (\<lambda>x. x) xs)" by simp
- from \<open>a \<in> set xs\<close> have "a \<in> set (filter (op = a) xs)" by auto
- then have "set (filter (op = a) xs) \<noteq> {}" by auto
- then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty)
- then have "length (filter (op = a) xs) > 0" by simp
- then have n: "Suc n = length (filter (op = a) xs)" by (simp add: n_def)
- moreover have "replicate (Suc n) a = a # replicate n a"
- by simp
- ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter)
-qed
-
lemma sorted_remdups[simp]:
"sorted l \<Longrightarrow> sorted (remdups l)"
by (induct l) (auto simp: sorted_Cons)
@@ -5069,14 +5012,6 @@
by (blast intro: map_inj_on)
qed
-lemma finite_sorted_distinct_unique:
-shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
-apply(drule finite_distinct_list)
-apply clarify
-apply(rule_tac a="sort xs" in ex1I)
-apply (auto simp: sorted_distinct_set_unique)
-done
-
lemma
assumes "sorted xs"
shows sorted_take: "sorted (take n xs)"
@@ -5133,6 +5068,155 @@
finally show "\<not> t < f x" by simp
qed
+lemma sorted_map_same:
+ "sorted (map f [x\<leftarrow>xs. f x = g xs])"
+proof (induct xs arbitrary: g)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs)
+ then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
+ moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
+ ultimately show ?case by (simp_all add: sorted_Cons)
+qed
+
+lemma sorted_same:
+ "sorted [x\<leftarrow>xs. x = g xs]"
+using sorted_map_same [of "\<lambda>x. x"] by simp
+
+end
+
+
+subsubsection \<open>Sorting functions\<close>
+
+text\<open>Currently it is not shown that @{const sort} returns a
+permutation of its input because the nicest proof is via multisets,
+which are not yet available. Alternatively one could define a function
+that counts the number of occurrences of an element in a list and use
+that instead of multisets to state the correctness property.\<close>
+
+context linorder
+begin
+
+lemma set_insort_key:
+ "set (insort_key f x xs) = insert x (set xs)"
+by (induct xs) auto
+
+lemma length_insort [simp]:
+ "length (insort_key f x xs) = Suc (length xs)"
+by (induct xs) simp_all
+
+lemma insort_key_left_comm:
+ assumes "f x \<noteq> f y"
+ shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
+by (induct xs) (auto simp add: assms dest: antisym)
+
+lemma insort_left_comm:
+ "insort x (insort y xs) = insort y (insort x xs)"
+by (cases "x = y") (auto intro: insort_key_left_comm)
+
+lemma comp_fun_commute_insort: "comp_fun_commute insort"
+proof
+qed (simp add: insort_left_comm fun_eq_iff)
+
+lemma sort_key_simps [simp]:
+ "sort_key f [] = []"
+ "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
+by (simp_all add: sort_key_def)
+
+lemma sort_key_conv_fold:
+ assumes "inj_on f (set xs)"
+ shows "sort_key f xs = fold (insort_key f) xs []"
+proof -
+ have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
+ proof (rule fold_rev, rule ext)
+ fix zs
+ fix x y
+ assume "x \<in> set xs" "y \<in> set xs"
+ with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
+ have **: "x = y \<longleftrightarrow> y = x" by auto
+ show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
+ by (induct zs) (auto intro: * simp add: **)
+ qed
+ then show ?thesis by (simp add: sort_key_def foldr_conv_fold)
+qed
+
+lemma sort_conv_fold:
+ "sort xs = fold insort xs []"
+by (rule sort_key_conv_fold) simp
+
+lemma length_sort[simp]: "length (sort_key f xs) = length xs"
+by (induct xs, auto)
+
+lemma set_sort[simp]: "set(sort_key f xs) = set xs"
+by (induct xs) (simp_all add: set_insort_key)
+
+lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
+by(induct xs)(auto simp: set_insort_key)
+
+lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
+by (induct xs) (simp_all add: distinct_insort)
+
+lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
+by (induct xs) (auto simp: sorted_Cons set_insort_key)
+
+lemma sorted_insort: "sorted (insort x xs) = sorted xs"
+using sorted_insort_key [where f="\<lambda>x. x"] by simp
+
+theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
+by (induct xs) (auto simp:sorted_insort_key)
+
+theorem sorted_sort [simp]: "sorted (sort xs)"
+using sorted_sort_key [where f="\<lambda>x. x"] by simp
+
+lemma insort_not_Nil [simp]:
+ "insort_key f a xs \<noteq> []"
+by (induction xs) simp_all
+
+lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
+by (cases xs) auto
+
+lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
+by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
+
+lemma insort_key_remove1:
+ assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
+ shows "insort_key f a (remove1 a xs) = xs"
+using assms proof (induct xs)
+ case (Cons x xs)
+ then show ?case
+ proof (cases "x = a")
+ case False
+ then have "f x \<noteq> f a" using Cons.prems by auto
+ then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
+ with \<open>f x \<noteq> f a\<close> show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
+ qed (auto simp: sorted_Cons insort_is_Cons)
+qed simp
+
+lemma insort_remove1:
+ assumes "a \<in> set xs" and "sorted xs"
+ shows "insort a (remove1 a xs) = xs"
+proof (rule insort_key_remove1)
+ define n where "n = length (filter (op = a) xs) - 1"
+ from \<open>a \<in> set xs\<close> show "a \<in> set xs" .
+ from \<open>sorted xs\<close> show "sorted (map (\<lambda>x. x) xs)" by simp
+ from \<open>a \<in> set xs\<close> have "a \<in> set (filter (op = a) xs)" by auto
+ then have "set (filter (op = a) xs) \<noteq> {}" by auto
+ then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty)
+ then have "length (filter (op = a) xs) > 0" by simp
+ then have n: "Suc n = length (filter (op = a) xs)" by (simp add: n_def)
+ moreover have "replicate (Suc n) a = a # replicate n a"
+ by simp
+ ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter)
+qed
+
+lemma finite_sorted_distinct_unique:
+shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
+apply(drule finite_distinct_list)
+apply clarify
+apply(rule_tac a="sort xs" in ex1I)
+apply (auto simp: sorted_distinct_set_unique)
+done
+
lemma insort_insert_key_triv:
"f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
by (simp add: insort_insert_key_def)
@@ -5151,12 +5235,12 @@
lemma set_insort_insert:
"set (insort_insert x xs) = insert x (set xs)"
- by (auto simp add: insort_insert_key_def set_insort)
+ by (auto simp add: insort_insert_key_def set_insort_key)
lemma distinct_insort_insert:
assumes "distinct xs"
shows "distinct (insort_insert_key f x xs)"
- using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort)
+using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort_key)
lemma sorted_insort_insert_key:
assumes "sorted (map f xs)"
@@ -5180,21 +5264,6 @@
"filter P (sort_key f xs) = sort_key f (filter P xs)"
by (induct xs) (simp_all add: filter_insort_triv filter_insort)
-lemma sorted_map_same:
- "sorted (map f [x\<leftarrow>xs. f x = g xs])"
-proof (induct xs arbitrary: g)
- case Nil then show ?case by simp
-next
- case (Cons x xs)
- then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
- moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
- ultimately show ?case by (simp_all add: sorted_Cons)
-qed
-
-lemma sorted_same:
- "sorted [x\<leftarrow>xs. x = g xs]"
- using sorted_map_same [of "\<lambda>x. x"] by simp
-
lemma remove1_insort [simp]:
"remove1 x (insort x xs) = xs"
by (induct xs) simp_all
@@ -5391,13 +5460,6 @@
sets to lists but one should convert in the other direction (via
@{const set}).\<close>
-subsubsection \<open>\<open>sorted_list_of_set\<close>\<close>
-
-text\<open>This function maps (finite) linearly ordered sets to sorted
-lists. Warning: in most cases it is not a good idea to convert from
-sets to lists but one should convert in the other direction (via
-@{const set}).\<close>
-
context linorder
begin
@@ -5428,7 +5490,8 @@
lemma sorted_list_of_set [simp]:
"finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
\<and> distinct (sorted_list_of_set A)"
- by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
+by(induct A rule: finite_induct)
+ (simp_all add: set_insort_key sorted_insort distinct_insort)
lemma distinct_sorted_list_of_set:
"distinct (sorted_list_of_set A)"
--- a/src/HOL/ROOT Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/ROOT Tue Aug 15 22:23:28 2017 +0200
@@ -213,6 +213,7 @@
AA_Map
Splay_Map
Leftist_Heap
+ Binomial_Heap
document_files "root.tex" "root.bib"
session "HOL-Import" in Import = HOL +
--- a/src/HOL/Relation.thy Tue Aug 15 18:15:04 2017 +0200
+++ b/src/HOL/Relation.thy Tue Aug 15 22:23:28 2017 +0200
@@ -438,6 +438,18 @@
lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
by (simp add: transp_def)
+lemma transp_le[simp]: "transp (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+by(auto simp add: transp_def)
+
+lemma transp_less[simp]: "transp (op < :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+by(auto simp add: transp_def)
+
+lemma transp_ge[simp]: "transp (op \<ge> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+by(auto simp add: transp_def)
+
+lemma transp_gr[simp]: "transp (op > :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+by(auto simp add: transp_def)
+
subsubsection \<open>Totality\<close>