--- a/Slides/Binomial_Tree_Slides.thy Thu Jul 06 14:57:19 2017 +0200
+++ b/Slides/Binomial_Tree_Slides.thy Thu Jul 06 15:00:28 2017 +0200
@@ -2,10 +2,21 @@
theory Binomial_Tree_Slides
imports
Tree_Notation
- "../Thys/BinHeap"
+ "../../Public/Thys/BinHeap"
begin
+
+thm btree_invar.simps[unfolded compl_descending_def]
+
+lemmas merge_simps = merge.simps(1) merge_simp2 merge.simps(3)
+
+thm get_min.simps
+
+lemma find_min_alt: "ts\<noteq>[] \<Longrightarrow> find_min ts = Min (set (map root ts))"
+ by (induction ts rule: find_min.induct) (auto simp: Let_def min_def)
-
+abbreviation (latex) sz_tree ("|_|") where "sz_tree t \<equiv> size (mset_tree t)"
+abbreviation (latex) sz_heap ("|_|") where "sz_heap t \<equiv> size (mset_heap t)"
+
(*>*)
text_raw{*
\end{isabellebody}%
@@ -15,12 +26,12 @@
%-------------------------------------------------------------
-\begin{frame}{Numerical Method}
+\begin{frame}{Numerical Method}{See \emph{Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999}}
Only use trees \<open>t\<^sub>i\<close> of size \<open>2\<^sup>i\<close>\\
- \bigskip\pause
+ \smallskip\pause
- E.g., to store \<open>0b1001\<close> elements: \<open>[t\<^sub>0,0,0,t\<^sub>3]\<close>\\
- \bigskip\pause
+ E.g., to store \<open>0b11001\<close> elements: \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close>\\
+ \smallskip\pause
Meld: Addition with carry. \\
\smallskip\pause
@@ -28,45 +39,119 @@
\end{frame}
\begin{frame}{Organization of Trees}
- Tree of size \<open>2\<^sup>i\<close> has \emph{rank} \<open>i\<close>\\
- \bigskip\pause
+ \high{@{theory_text \<open>(*<*)datatype (*>*)'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")\<close>}}\\
+ \smallskip\pause
+
+ Node with rank \<open>i\<close> has successors \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close>
+ with ranks \<open>[i-1,\<dots>,0]\<close>
+ \high{@{thm [display] btree_invar.simps[unfolded compl_descending_def]}}
+ \smallskip\pause
- Node with rank \<open>i\<close> has successors \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close>
- with ranks \<open>[i-1,\<dots>,0]\<close>\\
+ Tree has exactly @{term \<open>(2::nat)^rank t\<close>} nodes
+ \high{@{thm [display] size_btree}}
\end{frame}
-\begin{frame}{Sparse Binary Numbers}
- Using sparse binary numbers: \\
- \<open>[t\<^sub>0,0,0,t\<^sub>3]\<close> represented as \<open>[ (0,t\<^sub>0), (3,t\<^sub>3) ]\<close>
+\begin{frame}{Linking two Trees}
+ Given two trees of rank \<open>i\<close>, join them to tree of rank \<open>i+1\<close>.\\
+ \smallskip\pause
+
+ Idea: Insert one tree under root of other tree
+ \smallskip\pause
+
+ \high{@{thm[display] link_def}}
\end{frame}
\begin{frame}{Heap Datatype}
- \high{\<open>'a tree\<close>\\~~~\<open>= Node (rank: nat) (root: 'a) (children: "'a tree list")\<close>}\\
- \high{\<open>'a heap = 'a tree list\<close>}\\
+ Using sparse representation for binary numbers: \\
+ \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close> represented as \<open>[ (0,t\<^sub>0), (3,t\<^sub>3),(4,t\<^sub>4) ]\<close>
\bigskip\pause
- \high{@{thm btree_invar.simps}}\\
+ \high{@{theory_text \<open>(*<*)type_synonym (*>*)'a heap = "'a tree list"\<close>}}
\smallskip\pause
- Ranks of successors in \high{descending} order\\
- \smallskip\pause
- Sparse implementation has no advantage here, but code gets more readable [Okasaki]\\
- \bigskip\pause
\high{@{thm bheap_invar_def}}\\
Ranks in \high{ascending} order\\
\end{frame}
\begin{frame}{Inserting a Tree}
- \high{@{thm ins_tree.simps}}\\
+ \high{@{thm [display, margin=60] ins_tree.simps}}
+ \smallskip\pause
+
+ Intuition: Handle a carry
+ \smallskip\pause
+
+ Precondition:\\
+ Rank of inserted tree \<open>\<le>\<close> ranks of trees in heap \\
+\end{frame}
+
+\begin{frame}{Merge}
+ \high{@{thm [display] merge_simps}}
+ \smallskip\pause
+
+ Intuition: Addition of binary numbers
\smallskip\pause
- Precondition: Rank of inserted tree \<open>\<le>\<close> ranks of trees in heap \\
+
+ Note: Handling of carry after recursive call
+\end{frame}
+
+\begin{frame}{Find/Delete Minimum Element}
+ All trees are min-heaps
+ \smallskip\pause
+
+ Smallest element may be any root node
+ \high{@{thm [display] find_min_alt}}
+ \smallskip\pause
+
+ Similar: \high{@{term_type get_min}} \\
+ Returns tree with minimal root, and other trees
+
\smallskip\pause
- Intuition: Increment, handle carry \\
- \bigskip\pause
- Link: One tree inserted under root of other\\
- \high{@{thm link_def}}\\
+ Delete via merge
+ \high{@{thm [display, margin=60] delete_min_def}}
+ Note the \<open>rev\<close>!
+
+\end{frame}
+
+\begin{frame}{Complexity}
+ Recall: @{term \<open>size (mset_tree t) = 2^rank t\<close>}
+ \smallskip\pause
+
+ Similarly for heap: @{term \<open>size (mset_heap h) \<ge> 2^length h\<close>}
+ \smallskip\pause
+
+ Complexity of operations: linear in length of heap\\ \pause
+ i.e., logarithmic in number of elements
+ \smallskip\pause
+
+ Proofs: \pause straightforward\pause ?
\end{frame}
+\begin{frame}{Complexity of Merge}
+ \high{@{thm [display] merge_simps(3)}}
+ \smallskip\pause
+
+ Complexity of @{const ins_tree} call depends on length of result of recursive call.
+ \smallskip\pause
+
+ Naive: @{term \<open>length (merge ts\<^sub>1 ts\<^sub>2) \<le> length ts\<^sub>1 + length ts\<^sub>2\<close>}
+ \smallskip\pause
+
+ Yields (roughly) \<open>m n = m (n-2) + n\<close> \pause quadratic!
+\end{frame}
+
+\begin{frame}{Complexity of Merge}
+ \high{@{thm [display] merge_simps(3)}}
+ \smallskip\pause
+
+ Idea: Estimate cost and length of result:
+ \high{@{thm [display, margin=60] l_ins_tree_estimate l_merge_estimate}}
+
+ \smallskip\pause
+ Yields desired linear bound!
+\end{frame}
+
+
+
\begin{isabellebody}%
*}
(*<*)
--- a/Thys/BinHeap.thy Thu Jul 06 14:57:19 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,836 +0,0 @@
-(* Author: Peter Lammich *)
-section \<open>Binomial Heaps\<close>
-theory BinHeap
-imports Complex_Main
- "../../Public/Thys/Priority_Queue"
- "Heap_Prelim"
-begin
-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 btree_invar :: "'a::linorder tree \<Rightarrow> bool"
- where
- "btree_invar (Node r _ c) \<longleftrightarrow>
- (\<forall>t\<in>set c. btree_invar t)
- \<and> (compl_descending r (map rank c))
-"
-
-definition bheap_invar :: "'a::linorder heap \<Rightarrow> bool" where
- "bheap_invar c
- \<longleftrightarrow> (\<forall>t\<in>set c. btree_invar t) \<and> (strictly_ascending (map rank c))"
-
-text \<open>Ordering (heap) invariant\<close>
-fun otree_invar :: "'a::linorder tree \<Rightarrow> bool"
- where
- "otree_invar (Node _ x c) \<longleftrightarrow> (\<forall>t\<in>set c. otree_invar t \<and> x \<le> root t)"
-
-definition oheap_invar :: "'a::linorder heap \<Rightarrow> bool" where
- "oheap_invar c \<longleftrightarrow> (\<forall>t\<in>set c. otree_invar t)"
-
-definition invar :: "'a::linorder heap \<Rightarrow> bool" where
- "invar ts \<longleftrightarrow> bheap_invar 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_bheap_invar:
- "btree_invar (Node r v ts) \<Longrightarrow> bheap_invar (rev ts)"
- by (auto
- simp: bheap_invar_def
- simp: rev_map[symmetric]
- dest: compl_is_strictly_descending
- )
-
-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_btree_invar:
- assumes "btree_invar t\<^sub>1"
- assumes "btree_invar t\<^sub>2"
- assumes "rank t\<^sub>1 = rank t\<^sub>2"
- shows "btree_invar (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#rest) = (
- if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#rest else ins_tree (link t\<^sub>1 t\<^sub>2) rest
- )"
-
-lemma bheap_invar_Cons[simp]:
- "bheap_invar (t#ts)
- \<longleftrightarrow> btree_invar t \<and> bheap_invar ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
- unfolding bheap_invar_def
- by auto
-
-lemma ins_tree_btree_invar:
- assumes "btree_invar t"
- assumes "bheap_invar ts"
- assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"
- shows "bheap_invar (ins_tree t ts)"
- using assms
- apply (induction t ts rule: ins_tree.induct)
- apply (auto simp: link_btree_invar 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_btree_invar 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_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_bheap_invar:
- assumes "bheap_invar ts\<^sub>1"
- assumes "bheap_invar ts\<^sub>2"
- shows "bheap_invar (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]: "btree_invar t\<^sub>1" "btree_invar 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]: "bheap_invar (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_btree_invar link_btree_invar)
- 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_bheap_invar 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)"
- apply rule
- using assms find_min_member find_min_mset
- by auto
-
-
-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_bheap_invar:
- assumes "get_min ts = (t',ts')"
- assumes "ts\<noteq>[]"
- assumes "bheap_invar ts"
- shows "btree_invar t'" and "bheap_invar ts'"
-proof -
- have "btree_invar t' \<and> bheap_invar 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 "btree_invar t'" and "bheap_invar 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 delete_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap"
- where
- "delete_min ts = (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
- \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2
- )"
-
-lemma delete_min_invar[simp]:
- assumes "ts \<noteq> []"
- assumes "invar ts"
- shows "invar (delete_min ts)"
- using assms
- unfolding invar_def delete_min_def
- by (auto
- split: prod.split tree.split
- intro!: merge_bheap_invar merge_oheap_invar
- dest: get_min_bheap_invar get_min_oheap_invar
- intro!: children_oheap_invar children_bheap_invar
- )
-
-lemma delete_min_mset:
- assumes "ts \<noteq> []"
- shows "mset_heap ts = mset_heap (delete_min ts) + {# find_min ts #}"
- using assms
- unfolding delete_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 "btree_invar 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_descending r (map rank ts)" by auto
- hence COMPL: "map rank ts = rev [0..<r]" unfolding compl_descending_def .
-
- 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 "bheap_invar ts"
- shows "2^length ts \<le> size (mset_heap ts) + 1"
-proof -
- from \<open>bheap_invar ts\<close> have
- ASC: "strictly_ascending (map rank ts)" and
- TINV: "\<forall>t\<in>set ts. btree_invar t"
- unfolding bheap_invar_def by auto
-
- have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1"
- by (simp add: power2sum)
- also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
- using strictly_ascending_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_bound:
- assumes "invar ts"
- shows "t_ins x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
-proof -
- have 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
-
- 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: "bheap_invar ts\<^sub>1" "bheap_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"
-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 "bheap_invar 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_delete_min :: "'a::linorder heap \<Rightarrow> nat"
- where
- "t_delete_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: "bheap_invar (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_delete_min_bound_aux:
- fixes ts
- defines "n \<equiv> size (mset_heap ts)"
- assumes BINVAR: "bheap_invar ts"
- assumes "ts\<noteq>[]"
- shows "t_delete_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_bheap_invar[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
- hence BINVAR1: "bheap_invar (rev ts\<^sub>1)" by (blast intro: children_bheap_invar)
-
- 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_delete_min ts = t_get_min ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
- unfolding t_delete_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>bheap_invar (rev ts\<^sub>1)\<close> \<open>bheap_invar 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_delete_min ts \<le> 6 * log 2 (n+1) + 3"
- by auto
- thus ?thesis by (simp add: algebra_simps)
-qed
-
-lemma t_delete_min_bound:
- fixes ts
- defines "n \<equiv> size (mset_heap ts)"
- assumes "invar ts"
- assumes "ts\<noteq>[]"
- shows "t_delete_min ts \<le> 6 * log 2 (n+1) + 3"
- using assms t_delete_min_bound_aux unfolding invar_def by blast
-
-subsection \<open>Instantiating the Priority Queue Locale\<close>
-
-interpretation binheap:
- Priority_Queue "[]" "op = []" ins find_min delete_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 delete_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 bheap_invar_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, delete_min ts)"
- unfolding pop_min_def delete_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 delete_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 delete_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] delete_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: "bheap_invar 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_bheap_invar[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
- hence BINVAR1: "bheap_invar (rev ts\<^sub>1)" by (blast intro: children_bheap_invar)
-
- 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>bheap_invar (rev ts\<^sub>1)\<close> \<open>bheap_invar 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/Thys/Heap_Prelim.thy Thu Jul 06 14:57:19 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-section \<open>Preliminaries for Heap Formalization\<close>
-theory Heap_Prelim
-imports Complex_Main
-begin
-lemma power2sum: "(\<Sum>i\<in>{0..<k}. (2::nat)^i) = 2^k-1"
- by (induction k) auto
-
-subsection \<open>Strictly Ascending and Descending Sequences\<close>
-definition strictly_ascending :: "'a::linorder list \<Rightarrow> bool"
- where
- "strictly_ascending xs \<equiv> sorted xs \<and> distinct xs"
-
-definition strictly_descending :: "'a::linorder list \<Rightarrow> bool"
- where
- "strictly_descending xs \<equiv> sorted (rev xs) \<and> distinct xs"
-
-text \<open>The sequence \<open>[r-1,\<dots>,0]\<close>: \<close>
-definition compl_descending :: "nat \<Rightarrow> nat list \<Rightarrow> bool" where
- "compl_descending r ns \<longleftrightarrow> (ns = rev [0..<r])"
-
-lemma strictly_descending_alt:
- "strictly_descending = strictly_ascending o rev"
- unfolding strictly_descending_def strictly_ascending_def by auto
-
-lemma strictly_ascending_Nil[simp, intro!]: "strictly_ascending []"
- unfolding strictly_ascending_def by auto
-
-lemma strictly_ascending_Cons[simp]:
- "strictly_ascending (x#xs) \<longleftrightarrow> strictly_ascending xs \<and> (\<forall>y\<in>set xs. x<y)"
- unfolding strictly_ascending_def using le_neq_trans
- by (auto simp: sorted_Cons)
-
-lemma strictly_ascending_append[simp]:
- "strictly_ascending (xs@ys)
- \<longleftrightarrow> strictly_ascending xs \<and> strictly_ascending ys
- \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. x<y)"
- by (induction xs) auto
-
-lemma strictly_descending_Nil[simp, intro!]: "strictly_descending []"
- unfolding strictly_descending_def by auto
-
-lemma strictly_descending_Cons[simp]:
- "strictly_descending (x#xs) \<longleftrightarrow> strictly_descending xs \<and> (\<forall>y\<in>set xs. x>y)"
- unfolding strictly_descending_alt
- by (auto)
-
-lemma strictly_descending_append[simp]:
- "strictly_descending (xs@ys)
- \<longleftrightarrow> strictly_descending xs \<and> strictly_descending ys
- \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. x>y)"
- unfolding strictly_descending_alt by auto
-
-lemma strictly_ascending_rev[simp]:
- "strictly_ascending (rev xs) \<longleftrightarrow> strictly_descending xs"
- unfolding strictly_descending_alt by auto
-
-lemma strictly_descending_rev[simp]:
- "strictly_descending (rev xs) \<longleftrightarrow> strictly_ascending xs"
- unfolding strictly_descending_alt by auto
-
-lemma compl_descending_Nil[simp]:
- "compl_descending 0 []"
- "compl_descending r [] \<longleftrightarrow> r = 0"
- "compl_descending 0 ns \<longleftrightarrow> ns=[]"
- unfolding compl_descending_def by auto
-
-lemma compl_descending_Cons[simp]:
- "compl_descending r (n#ns) \<longleftrightarrow> (r = Suc n \<and> compl_descending n ns)"
- unfolding compl_descending_def
- by (cases r) (auto)
-
-lemma compl_is_strictly_descending:
- "compl_descending r ns \<Longrightarrow> strictly_descending ns"
- unfolding compl_descending_def strictly_descending_def
- by auto
-
-subsubsection \<open>Strictly Ascending Sequences of Natural Numbers\<close>
-
-text \<open>Each element is greater or equal to its index\<close>
-lemma strictly_ascending_idx:
- assumes "strictly_ascending ns"
- shows "\<forall>i<length ns. i\<le>ns!i"
- using assms
- apply (induction ns rule: rev_induct)
- subgoal by simp
- subgoal
- apply (clarsimp simp: nth_append)
- by (metis less_antisym not_less nth_mem)
- done
-
-text \<open>Summation of a strictly ascending sequence with length \<open>n\<close>
- can be estimated by summation over \<open>{0..<n}\<close>.
-\<close>
-lemma strictly_ascending_sum_mono_lowerbound:
- fixes f :: "nat \<Rightarrow> ('b::ordered_comm_monoid_add)"
- assumes "strictly_ascending ns"
- assumes MONO: "\<And>x y. x\<le>y \<Longrightarrow> f x \<le> f y"
- shows "(\<Sum>i\<in>{0..<length ns}. f i) \<le> (\<Sum>i\<leftarrow>ns. f i)"
- using assms
-proof (induction ns rule: rev_induct)
- case Nil
- then show ?case by simp
-next
- case (snoc n ns)
- hence IH: "sum f {0..<length ns} \<le> sum_list (map f ns)"
- by auto
-
- from strictly_ascending_idx[OF snoc.prems(1), THEN spec[of _ "length ns"]]
- have NGE: "length ns \<le> n" by auto
-
- have "sum f {0..<length (ns @ [n])}
- = sum f {0..<length ns} + f (length ns)"
- by simp
- also note IH
- also note NGE
- 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
-
-end