author nipkow Tue, 29 Aug 2017 16:54:54 +0200 changeset 66549 253880668a43 parent 66547 188c7853f84a child 66550 b8a6f9337229
simpler definition
```--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Aug 29 15:37:02 2017 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Tue Aug 29 16:54:54 2017 +0200
@@ -92,10 +92,15 @@

-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)
-  )"
+context
+includes pattern_aliases
+begin
+
+fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+  "link (Node r x\<^sub>1 c\<^sub>1 =: t\<^sub>1) (Node _ x\<^sub>2 c\<^sub>2 =: t\<^sub>2) =
+    (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))"
+
+end

assumes "invar_btree t\<^sub>1"
@@ -103,20 +108,20 @@
assumes "rank t\<^sub>1 = rank t\<^sub>2"
using assms
-by (auto simp: link_def split: tree.split)
+by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp

assumes "invar_otree t\<^sub>1"
assumes "invar_otree t\<^sub>2"
using assms
-by (auto simp: link_def split: tree.split)
+by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto