author nipkow Fri, 06 Jul 2018 22:52:49 +0200 changeset 68600 bdd6536bd57c parent 68599 cc7b5e0355a5 child 68602 7605d3998e9f
more symmetric
```--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Fri Jul 06 21:19:24 2018 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Fri Jul 06 22:52:49 2018 +0200
@@ -53,13 +53,13 @@
"merge t1 Leaf = t1" |
"merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
(if a1 \<le> a2 then node l1 a1 (merge r1 t2)
-    else node l2 a2 (merge r2 t1))"
+    else node l2 a2 (merge t1 r2))"

lemma merge_code: "merge t1 t2 = (case (t1,t2) of
(Leaf, _) \<Rightarrow> t2 |
(_, Leaf) \<Rightarrow> t1 |
(Node l1 a1 n1 r1, Node l2 a2 n2 r2) \<Rightarrow>
-    if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))"
+    if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge t1 r2))"
by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)

hide_const (open) insert
@@ -191,7 +191,7 @@
"t_merge t2 Leaf = 1" |
"t_merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
(if a1 \<le> a2 then 1 + t_merge r1 t2
-   else 1 + t_merge r2 t1)"
+   else 1 + t_merge t1 r2)"

definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
"t_insert x t = t_merge (Node Leaf x 1 Leaf) t"
@@ -202,8 +202,7 @@

lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
proof(induction l r rule: merge.induct)
-  case 3 thus ?case
-    by(simp)(fastforce split: tree.splits simp del: t_merge.simps)
+  case 3 thus ?case by(simp)
qed simp_all

corollary t_merge_log: assumes "ltree l" "ltree r"```