equal
deleted
inserted
replaced
70 "delete x t = tree\<^sub>d(del x t)" |
70 "delete x t = tree\<^sub>d(del x t)" |
71 |
71 |
72 |
72 |
73 subsection \<open>Functional Correctness\<close> |
73 subsection \<open>Functional Correctness\<close> |
74 |
74 |
75 lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
75 lemma lookup_map_of: |
|
76 "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
76 by (induction t) (auto simp: map_of_simps split: option.split) |
77 by (induction t) (auto simp: map_of_simps split: option.split) |
77 |
78 |
78 |
79 |
79 lemma inorder_upd: |
80 lemma inorder_upd: |
80 "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)" |
81 "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)" |
116 by(simp add: delete_def bal_tree\<^sub>d_del) |
117 by(simp add: delete_def bal_tree\<^sub>d_del) |
117 |
118 |
118 |
119 |
119 subsection \<open>Overall Correctness\<close> |
120 subsection \<open>Overall Correctness\<close> |
120 |
121 |
121 interpretation T23_Map: Map_by_Ordered |
122 interpretation Map_by_Ordered |
122 where empty = Leaf and lookup = lookup and update = update and delete = delete |
123 where empty = Leaf and lookup = lookup and update = update and delete = delete |
123 and inorder = inorder and inv = bal |
124 and inorder = inorder and inv = bal |
124 proof (standard, goal_cases) |
125 proof (standard, goal_cases) |
125 case 2 thus ?case by(simp add: lookup) |
126 case 2 thus ?case by(simp add: lookup_map_of) |
126 next |
127 next |
127 case 3 thus ?case by(simp add: inorder_update) |
128 case 3 thus ?case by(simp add: inorder_update) |
128 next |
129 next |
129 case 4 thus ?case by(simp add: inorder_delete) |
130 case 4 thus ?case by(simp add: inorder_delete) |
130 next |
131 next |