# HG changeset patch # User wenzelm # Date 1606411926 -3600 # Node ID 178de0e275a12252e2d5fee87b3cedd6b453ad7f # Parent 35d1fc20df224532fb4b9d76644dcd4aa0da1b28# Parent 01c9b303303611c549ca64e86f8f67f690ab37a5 merged diff -r 01c9b3033036 -r 178de0e275a1 src/HOL/Data_Structures/Binomial_Heap.thy --- a/src/HOL/Data_Structures/Binomial_Heap.thy Thu Nov 26 18:05:24 2020 +0100 +++ b/src/HOL/Data_Structures/Binomial_Heap.thy Thu Nov 26 18:32:06 2020 +0100 @@ -110,7 +110,7 @@ using assms by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp -lemma invar_link_otree: +lemma invar_otree_link: assumes "invar_otree t\<^sub>1" assumes "invar_otree t\<^sub>2" shows "invar_otree (link t\<^sub>1 t\<^sub>2)" @@ -152,7 +152,7 @@ assumes "invar_oheap ts" shows "invar_oheap (ins_tree t ts)" using assms -by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree) +by (induction t ts rule: ins_tree.induct) (auto simp: invar_otree_link) lemma mset_heap_ins_tree[simp]: "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts" @@ -252,7 +252,7 @@ shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)" using assms by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) - (auto simp: invar_oheap_ins_tree invar_link_otree) + (auto simp: invar_oheap_ins_tree invar_otree_link) lemma invar_merge[simp]: "\ invar ts\<^sub>1; invar ts\<^sub>2 \ \ invar (merge ts\<^sub>1 ts\<^sub>2)" by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)