equal
deleted
inserted
replaced
59 "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
59 "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
60 by(induction t) (auto simp: del_list_simps del_minD split: prod.splits) |
60 by(induction t) (auto simp: del_list_simps del_minD split: prod.splits) |
61 |
61 |
62 interpretation Set_by_Ordered |
62 interpretation Set_by_Ordered |
63 where empty = Leaf and isin = isin and insert = insert and delete = delete |
63 where empty = Leaf and isin = isin and insert = insert and delete = delete |
64 and inorder = inorder and wf = "\<lambda>_. True" |
64 and inorder = inorder and inv = "\<lambda>_. True" |
65 proof (standard, goal_cases) |
65 proof (standard, goal_cases) |
66 case 1 show ?case by simp |
66 case 1 show ?case by simp |
67 next |
67 next |
68 case 2 thus ?case by(simp add: isin_set) |
68 case 2 thus ?case by(simp add: isin_set) |
69 next |
69 next |