84 corollary inorder_update: |
84 corollary inorder_update: |
85 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
85 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
86 by(simp add: update_def inorder_upd) |
86 by(simp add: update_def inorder_upd) |
87 |
87 |
88 |
88 |
89 lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
89 lemma inorder_del: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
90 inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" |
90 inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" |
91 by(induction t rule: del.induct) |
91 by(induction t rule: del.induct) |
92 (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) |
92 (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) |
93 |
93 |
94 corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
94 corollary inorder_delete: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
95 inorder(delete x t) = del_list x (inorder t)" |
95 inorder(delete x t) = del_list x (inorder t)" |
96 by(simp add: delete_def inorder_del) |
96 by(simp add: delete_def inorder_del) |
97 |
97 |
98 |
98 |
99 subsection \<open>Balancedness\<close> |
99 subsection \<open>Balancedness\<close> |
100 |
100 |
101 lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t" |
101 lemma complete_upd: "complete t \<Longrightarrow> complete (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t" |
102 by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *) |
102 by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *) |
103 |
103 |
104 corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)" |
104 corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)" |
105 by (simp add: update_def bal_upd) |
105 by (simp add: update_def complete_upd) |
106 |
106 |
107 |
107 |
108 lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t" |
108 lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t" |
109 by(induction x t rule: del.induct) |
109 by(induction x t rule: del.induct) |
110 (auto simp add: heights max_def height_split_min split: prod.split) |
110 (auto simp add: heights max_def height_split_min split: prod.split) |
111 |
111 |
112 lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))" |
112 lemma complete_tree\<^sub>d_del: "complete t \<Longrightarrow> complete(tree\<^sub>d(del x t))" |
113 by(induction x t rule: del.induct) |
113 by(induction x t rule: del.induct) |
114 (auto simp: bals bal_split_min height_del height_split_min split: prod.split) |
114 (auto simp: completes complete_split_min height_del height_split_min split: prod.split) |
115 |
115 |
116 corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)" |
116 corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)" |
117 by(simp add: delete_def bal_tree\<^sub>d_del) |
117 by(simp add: delete_def complete_tree\<^sub>d_del) |
118 |
118 |
119 |
119 |
120 subsection \<open>Overall Correctness\<close> |
120 subsection \<open>Overall Correctness\<close> |
121 |
121 |
122 interpretation M: Map_by_Ordered |
122 interpretation M: Map_by_Ordered |
123 where empty = empty and lookup = lookup and update = update and delete = delete |
123 where empty = empty and lookup = lookup and update = update and delete = delete |
124 and inorder = inorder and inv = bal |
124 and inorder = inorder and inv = complete |
125 proof (standard, goal_cases) |
125 proof (standard, goal_cases) |
126 case 1 thus ?case by(simp add: empty_def) |
126 case 1 thus ?case by(simp add: empty_def) |
127 next |
127 next |
128 case 2 thus ?case by(simp add: lookup_map_of) |
128 case 2 thus ?case by(simp add: lookup_map_of) |
129 next |
129 next |