# HG changeset patch
# User nipkow
# Date 1503513675 -7200
# Node ID 78a009ac91d24d591d0bf7ee816c8d795daaf30e
# Parent  cc66ab2373ce87fe32b3a8610d8dff2fbaf06efc
reorg

diff -r cc66ab2373ce -r 78a009ac91d2 src/HOL/Data_Structures/Base_FDS.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Base_FDS.thy	Wed Aug 23 20:41:15 2017 +0200
@@ -0,0 +1,22 @@
+theory Base_FDS
+imports "../Library/Pattern_Aliases"
+begin
+
+declare Let_def [simp]
+
+text \<open>Lemma \<open>size_prod_measure\<close>, when declared with the \<open>measure_function\<close> attribute,
+enables \<open>fun\<close> to prove termination of a larger class of functions automatically.
+By default, \<open>fun\<close> only tries lexicographic combinations of the sizes of the parameters.
+With \<open>size_prod_measure\<close> enabled it also tries measures based on the sum of the sizes
+of different parameters.
+
+To alert the reader whenever such a more subtle termination proof is taking place
+the lemma is not enabled all the time but only locally in a \<open>context\<close> block
+around such function definitions.
+\<close>
+
+lemma size_prod_measure: 
+  "is_measure f \<Longrightarrow> is_measure g \<Longrightarrow> is_measure (size_prod f g)"
+by (rule is_measure_trivial)
+
+end
\ No newline at end of file
diff -r cc66ab2373ce -r 78a009ac91d2 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Aug 23 18:28:56 2017 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Aug 23 20:41:15 2017 +0200
@@ -4,13 +4,11 @@
 
 theory Binomial_Heap
 imports
+  Base_FDS
   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.
@@ -96,7 +94,7 @@
   "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"
@@ -104,7 +102,7 @@
   shows "invar_btree (link t\<^sub>1 t\<^sub>2)"  
   using assms  
   unfolding link_def
-  by (force split: tree.split )
+  by (force split: tree.split)
     
 lemma link_otree_invar:      
   assumes "otree_invar t\<^sub>1"
@@ -179,17 +177,17 @@
     
 lemma ins_mset[simp]: "mset_heap (ins x t) = {#x#} + mset_heap t"
   unfolding ins_def
-  by auto  
-  
+  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
+    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:
@@ -281,7 +279,7 @@
   using assms  
   apply (induction ts arbitrary: x rule: find_min.induct)  
   apply (auto 
-      simp: Let_def otree_invar_root_min intro: order_trans;
+      simp: otree_invar_root_min intro: order_trans;
       meson linear order_trans otree_invar_root_min
       )+
   done  
@@ -300,7 +298,7 @@
   shows "find_min ts \<in># mset_heap ts"  
   using assms  
   apply (induction ts rule: find_min.induct)  
-  apply (auto simp: Let_def)
+  apply (auto)
   done  
 
 lemma find_min:    
@@ -323,8 +321,8 @@
   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  
+  apply (auto split: prod.splits)
+  done
   
 lemma get_min_mset:    
   assumes "get_min ts = (t',ts')"  
diff -r cc66ab2373ce -r 78a009ac91d2 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Aug 23 18:28:56 2017 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Aug 23 20:41:15 2017 +0200
@@ -4,15 +4,13 @@
 
 theory Leftist_Heap
 imports
+  Base_FDS
   Tree2
   Priority_Queue
   Complex_Main
 begin
 
-(* FIXME mv Base *)
-lemma size_prod_measure[measure_function]: 
-  "is_measure f \<Longrightarrow> is_measure g \<Longrightarrow> is_measure (size_prod f g)"
-by (rule is_measure_trivial)
+unbundle pattern_aliases
 
 fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
 "mset_tree Leaf = {#}" |
@@ -48,12 +46,16 @@
 fun get_min :: "'a lheap \<Rightarrow> 'a" where
 "get_min(Node n l a r) = a"
 
-fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
+text\<open>Explicit termination argument: sum of sizes\<close>
+
+function merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "merge Leaf t2 = t2" |
 "merge t1 Leaf = t1" |
-"merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
-   (if a1 \<le> a2 then node l1 a1 (merge r1 (Node n2 l2 a2 r2))
-    else node l2 a2 (merge r2 (Node n1 l1 a1 r1)))"
+"merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
+   (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
+    else node l2 a2 (merge r2 t1))"
+by pat_completeness auto
+termination by (relation "measure (\<lambda>(t1,t2). size t1 + size t2)") auto
 
 lemma merge_code: "merge t1 t2 = (case (t1,t2) of
   (Leaf, _) \<Rightarrow> t2 |
@@ -72,9 +74,6 @@
 
 subsection "Lemmas"
 
-(* FIXME mv DS_Base *)
-declare Let_def [simp]
-
 lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
@@ -179,12 +178,16 @@
   finally show ?case .
 qed
 
-fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
+text\<open>Explicit termination argument: sum of sizes\<close>
+
+function t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
 "t_merge Leaf t2 = 1" |
 "t_merge t2 Leaf = 1" |
-"t_merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
-  (if a1 \<le> a2 then 1 + t_merge r1 (Node n2 l2 a2 r2)
-   else 1 + t_merge r2 (Node n1 l1 a1 r1))"
+"t_merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
+  (if a1 \<le> a2 then 1 + t_merge r1 t2
+   else 1 + t_merge r2 t1)"
+by pat_completeness auto
+termination by (relation "measure (\<lambda>(t1,t2). size t1 + size t2)") auto
 
 definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
 "t_insert x t = t_merge (Node 1 Leaf x Leaf) t"
@@ -209,7 +212,7 @@
 using t_merge_log[of "Node 1 Leaf x Leaf" t]
 by(simp add: t_insert_def split: tree.split)
 
-(* FIXME mv Lemmas_log *)
+(* FIXME mv ? *)
 lemma ld_ld_1_less:
   assumes "x > 0" "y > 0" shows "log 2 x + log 2 y + 1 < 2 * log 2 (x+y)"
 proof -
@@ -218,7 +221,7 @@
   also have "\<dots> < (x+y)^2" using assms
     by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
   also have "\<dots> = 2 powr (2 * log 2 (x+y))"
-    using assms by(simp add: powr_add log_powr[symmetric] powr_numeral)
+    using assms by(simp add: powr_add log_powr[symmetric])
   finally show ?thesis by simp
 qed