# HG changeset patch # User nipkow # Date 1607084689 -3600 # Node ID 976d656ed31e8a654d62f887daf1fd08d74df208 # Parent d7393c35aa5dc290b97cd341250c954295d4e3f2 tuned diff -r d7393c35aa5d -r 976d656ed31e src/HOL/Data_Structures/Tree23_Map.thy --- a/src/HOL/Data_Structures/Tree23_Map.thy Thu Dec 03 23:00:23 2020 +0100 +++ b/src/HOL/Data_Structures/Tree23_Map.thy Fri Dec 04 13:24:49 2020 +0100 @@ -98,14 +98,14 @@ subsection \Balancedness\ -lemma complete_upd: "complete t \ complete (treeI(upd x y t)) \ height(upd x y t) = height t" +lemma complete_upd: "complete t \ complete (treeI(upd x y t)) \ hI(upd x y t) = height t" by (induct t) (auto split!: if_split upI.split)(* 16 secs in 2015 *) corollary complete_update: "complete t \ complete (update x y t)" by (simp add: update_def complete_upd) -lemma height_del: "complete t \ height(del x t) = height t" +lemma height_del: "complete t \ hD(del x t) = height t" by(induction x t rule: del.induct) (auto simp add: heights max_def height_split_min split: prod.split) diff -r d7393c35aa5d -r 976d656ed31e src/HOL/Data_Structures/Tree23_Set.thy --- a/src/HOL/Data_Structures/Tree23_Set.thy Thu Dec 03 23:00:23 2020 +0100 +++ b/src/HOL/Data_Structures/Tree23_Set.thy Fri Dec 04 13:24:49 2020 +0100 @@ -45,7 +45,7 @@ (case ins x l of TI l' => TI (Node2 l' a r) | OF l1 b l2 => TI (Node3 l1 b l2 a r)) | - EQ \ TI (Node2 l x r) | + EQ \ TI (Node2 l a r) | GT \ (case ins x r of TI r' => TI (Node2 l a r') | @@ -210,18 +210,11 @@ text\First a standard proof that \<^const>\ins\ preserves \<^const>\complete\.\ -instantiation upI :: (type)height -begin +fun hI :: "'a upI \ nat" where +"hI (TI t) = height t" | +"hI (OF l a r) = height l" -fun height_upI :: "'a upI \ nat" where -"height (TI t) = height t" | -"height (OF l a r) = height l" - -instance .. - -end - -lemma complete_ins: "complete t \ complete (treeI(ins a t)) \ height(ins a t) = height t" +lemma complete_ins: "complete t \ complete (treeI(ins a t)) \ hI(ins a t) = height t" by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *) text\Now an alternative proof (by Brian Huffman) that runs faster because @@ -290,37 +283,30 @@ subsection "Proofs for delete" -instantiation upD :: (type)height -begin - -fun height_upD :: "'a upD \ nat" where -"height (TD t) = height t" | -"height (UF t) = height t + 1" - -instance .. - -end +fun hD :: "'a upD \ nat" where +"hD (TD t) = height t" | +"hD (UF t) = height t + 1" lemma complete_treeD_node21: - "\complete r; complete (treeD l'); height r = height l' \ \ complete (treeD (node21 l' a r))" + "\complete r; complete (treeD l'); height r = hD l' \ \ complete (treeD (node21 l' a r))" by(induct l' a r rule: node21.induct) auto lemma complete_treeD_node22: - "\complete(treeD r'); complete l; height r' = height l \ \ complete (treeD (node22 l a r'))" + "\complete(treeD r'); complete l; hD r' = height l \ \ complete (treeD (node22 l a r'))" by(induct l a r' rule: node22.induct) auto lemma complete_treeD_node31: - "\ complete (treeD l'); complete m; complete r; height l' = height r; height m = height r \ + "\ complete (treeD l'); complete m; complete r; hD l' = height r; height m = height r \ \ complete (treeD (node31 l' a m b r))" by(induct l' a m b r rule: node31.induct) auto lemma complete_treeD_node32: - "\ complete l; complete (treeD m'); complete r; height l = height r; height m' = height r \ + "\ complete l; complete (treeD m'); complete r; height l = height r; hD m' = height r \ \ complete (treeD (node32 l a m' b r))" by(induct l a m' b r rule: node32.induct) auto lemma complete_treeD_node33: - "\ complete l; complete m; complete(treeD r'); height l = height r'; height m = height r' \ + "\ complete l; complete m; complete(treeD r'); height l = hD r'; height m = hD r' \ \ complete (treeD (node33 l a m b r'))" by(induct l a m b r' rule: node33.induct) auto @@ -328,37 +314,37 @@ complete_treeD_node31 complete_treeD_node32 complete_treeD_node33 lemma height'_node21: - "height r > 0 \ height(node21 l' a r) = max (height l') (height r) + 1" + "height r > 0 \ hD(node21 l' a r) = max (hD l') (height r) + 1" by(induct l' a r rule: node21.induct)(simp_all) lemma height'_node22: - "height l > 0 \ height(node22 l a r') = max (height l) (height r') + 1" + "height l > 0 \ hD(node22 l a r') = max (height l) (hD r') + 1" by(induct l a r' rule: node22.induct)(simp_all) lemma height'_node31: - "height m > 0 \ height(node31 l a m b r) = - max (height l) (max (height m) (height r)) + 1" + "height m > 0 \ hD(node31 l a m b r) = + max (hD l) (max (height m) (height r)) + 1" by(induct l a m b r rule: node31.induct)(simp_all add: max_def) lemma height'_node32: - "height r > 0 \ height(node32 l a m b r) = - max (height l) (max (height m) (height r)) + 1" + "height r > 0 \ hD(node32 l a m b r) = + max (height l) (max (hD m) (height r)) + 1" by(induct l a m b r rule: node32.induct)(simp_all add: max_def) lemma height'_node33: - "height m > 0 \ height(node33 l a m b r) = - max (height l) (max (height m) (height r)) + 1" + "height m > 0 \ hD(node33 l a m b r) = + max (height l) (max (height m) (hD r)) + 1" by(induct l a m b r rule: node33.induct)(simp_all add: max_def) lemmas heights = height'_node21 height'_node22 height'_node31 height'_node32 height'_node33 lemma height_split_min: - "split_min t = (x, t') \ height t > 0 \ complete t \ height t' = height t" + "split_min t = (x, t') \ height t > 0 \ complete t \ hD t' = height t" by(induct t arbitrary: x t' rule: split_min.induct) (auto simp: heights split: prod.splits) -lemma height_del: "complete t \ height(del x t) = height t" +lemma height_del: "complete t \ hD(del x t) = height t" by(induction x t rule: del.induct) (auto simp: heights max_def height_split_min split: prod.splits)