equal
deleted
inserted
replaced
134 by(cases t)(auto simp add: ltree_merge simp del: merge.simps) |
134 by(cases t)(auto simp add: ltree_merge simp del: merge.simps) |
135 |
135 |
136 lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)" |
136 lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)" |
137 by(cases t)(auto simp add: heap_merge simp del: merge.simps) |
137 by(cases t)(auto simp add: heap_merge simp del: merge.simps) |
138 |
138 |
139 |
139 text \<open>Last step of functional correctness proof: combine all the above lemmas |
140 interpretation lheap: Priority_Queue |
140 to show that leftist heaps satisfy the specification of priority queues with merge.\<close> |
|
141 |
|
142 interpretation lheap: Priority_Queue_Merge |
141 where empty = Leaf and is_empty = "\<lambda>h. h = Leaf" |
143 where empty = Leaf and is_empty = "\<lambda>h. h = Leaf" |
142 and insert = insert and del_min = del_min |
144 and insert = insert and del_min = del_min |
143 and get_min = get_min and invar = "\<lambda>h. heap h \<and> ltree h" |
145 and get_min = get_min and merge = merge |
144 and mset = mset_tree |
146 and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree |
145 proof(standard, goal_cases) |
147 proof(standard, goal_cases) |
146 case 1 show ?case by simp |
148 case 1 show ?case by simp |
147 next |
149 next |
148 case (2 q) show ?case by (cases q) auto |
150 case (2 q) show ?case by (cases q) auto |
149 next |
151 next |
156 case 6 thus ?case by(simp) |
158 case 6 thus ?case by(simp) |
157 next |
159 next |
158 case 7 thus ?case by(simp add: heap_insert ltree_insert) |
160 case 7 thus ?case by(simp add: heap_insert ltree_insert) |
159 next |
161 next |
160 case 8 thus ?case by(simp add: heap_del_min ltree_del_min) |
162 case 8 thus ?case by(simp add: heap_del_min ltree_del_min) |
|
163 next |
|
164 case 9 thus ?case by (simp add: mset_merge) |
|
165 next |
|
166 case 10 thus ?case by (simp add: heap_merge ltree_merge) |
161 qed |
167 qed |
162 |
168 |
163 |
169 |
164 subsection "Complexity" |
170 subsection "Complexity" |
165 |
171 |