equal
deleted
inserted
replaced
131 (if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#ts else ins_tree (link t\<^sub>1 t\<^sub>2) ts)" |
131 (if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#ts else ins_tree (link t\<^sub>1 t\<^sub>2) ts)" |
132 |
132 |
133 lemma invar_bheap_Cons[simp]: |
133 lemma invar_bheap_Cons[simp]: |
134 "invar_bheap (t#ts) |
134 "invar_bheap (t#ts) |
135 \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')" |
135 \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')" |
136 by (auto simp: sorted_wrt_Cons invar_bheap_def) |
136 by (auto simp: invar_bheap_def) |
137 |
137 |
138 lemma invar_btree_ins_tree: |
138 lemma invar_btree_ins_tree: |
139 assumes "invar_btree t" |
139 assumes "invar_btree t" |
140 assumes "invar_bheap ts" |
140 assumes "invar_bheap ts" |
141 assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'" |
141 assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'" |