equal
deleted
inserted
replaced
32 |
32 |
33 theorem inorder_delete: |
33 theorem inorder_delete: |
34 "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
34 "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
35 by(induction t) |
35 by(induction t) |
36 (auto simp: del_list_simps inorder_balL inorder_balR |
36 (auto simp: del_list_simps inorder_balL inorder_balR |
37 inorder_del_root inorder_del_maxD split: prod.splits) |
37 inorder_del_root inorder_split_maxD split: prod.splits) |
38 |
38 |
39 interpretation Map_by_Ordered |
39 interpretation Map_by_Ordered |
40 where empty = Leaf and lookup = lookup and update = update and delete = delete |
40 where empty = Leaf and lookup = lookup and update = update and delete = delete |
41 and inorder = inorder and inv = "\<lambda>_. True" |
41 and inorder = inorder and inv = "\<lambda>_. True" |
42 proof (standard, goal_cases) |
42 proof (standard, goal_cases) |