--- a/ANNOUNCE Sat Jul 07 15:07:37 2018 +0100
+++ b/ANNOUNCE Sat Jul 07 15:07:46 2018 +0100
@@ -27,7 +27,7 @@
You may get Isabelle2018 from the following mirror sites:
- Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle
- Munich (Germany) http://isabelle.in.tum.de
+ Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle
+ Munich (Germany) https://isabelle.in.tum.de
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle
- Potsdam, NY (USA) http://mirror.clarkson.edu/isabelle
+ Potsdam, NY (USA) https://mirror.clarkson.edu/isabelle
--- a/src/HOL/Data_Structures/Leftist_Heap.thy Sat Jul 07 15:07:37 2018 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Sat Jul 07 15:07:46 2018 +0100
@@ -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"