# HG changeset patch
# User nipkow
# Date 1504012035 -7200
# Node ID 14a7d2a3933682dc4cc1bd91fd3538d7f23cec66
# Parent  97c441c8665d6b63ab0db669178fa729b323d871
tuned

diff -r 97c441c8665d -r 14a7d2a39336 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Aug 29 13:56:15 2017 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Aug 29 15:07:15 2017 +0200
@@ -254,9 +254,7 @@
 
 fun get_min :: "'a::linorder heap \<Rightarrow> 'a" where
   "get_min [t] = root t"
-| "get_min (t#ts) = (let x = root t; 
-                          y = get_min ts
-                      in if x \<le> y then x else y)"
+| "get_min (t#ts) = min (root t) (get_min ts)"
   
 lemma invar_otree_root_min:
   assumes "invar_otree t"
@@ -273,7 +271,7 @@
   using assms  
 apply (induction ts arbitrary: x rule: get_min.induct)  
 apply (auto 
-      simp: invar_otree_root_min intro: order_trans;
+      simp: invar_otree_root_min min_def intro: order_trans;
       meson linear order_trans invar_otree_root_min
       )+
 done  
@@ -287,7 +285,7 @@
 
 lemma get_min_member:    
   "ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"  
-by (induction ts rule: get_min.induct) (auto)
+by (induction ts rule: get_min.induct) (auto simp: min_def)
 
 lemma get_min:    
   assumes "mset_heap ts \<noteq> {#}"
@@ -308,7 +306,7 @@
   assumes "get_min_rest ts = (t',ts')"  
   shows "root t' = get_min ts"  
 using assms  
-by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits)
+by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits)
 
 lemma mset_get_min_rest:    
   assumes "get_min_rest ts = (t',ts')"