author nipkow Tue, 29 Aug 2017 15:07:15 +0200 changeset 66546 14a7d2a39336 parent 66545 97c441c8665d child 66547 188c7853f84a
tuned
```--- 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')"  ```