equal
deleted
inserted
replaced
354 |
354 |
355 subsection \<open>Overall Correctness\<close> |
355 subsection \<open>Overall Correctness\<close> |
356 |
356 |
357 interpretation Set_by_Ordered |
357 interpretation Set_by_Ordered |
358 where empty = Leaf and isin = isin and insert = insert and delete = delete |
358 where empty = Leaf and isin = isin and insert = insert and delete = delete |
359 and inorder = inorder and wf = bal |
359 and inorder = inorder and inv = bal |
360 proof (standard, goal_cases) |
360 proof (standard, goal_cases) |
361 case 2 thus ?case by(simp add: isin_set) |
361 case 2 thus ?case by(simp add: isin_set) |
362 next |
362 next |
363 case 3 thus ?case by(simp add: inorder_insert) |
363 case 3 thus ?case by(simp add: inorder_insert) |
364 next |
364 next |