# 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 \<open>Balancedness\<close>
 
-lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> height(upd x y t) = height t"
+lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> 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 \<Longrightarrow> complete (update x y t)"
 by (simp add: update_def complete_upd)
 
 
-lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> 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 \<Rightarrow> TI (Node2 l x r) |
+      EQ \<Rightarrow> TI (Node2 l a r) |
       GT \<Rightarrow>
         (case ins x r of
            TI r' => TI (Node2 l a r') |
@@ -210,18 +210,11 @@
 
 text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>complete\<close>.\<close>
 
-instantiation upI :: (type)height
-begin
+fun hI :: "'a upI \<Rightarrow> nat" where
+"hI (TI t) = height t" |
+"hI (OF l a r) = height l"
 
-fun height_upI :: "'a upI \<Rightarrow> nat" where
-"height (TI t) = height t" |
-"height (OF l a r) = height l"
-
-instance ..
-
-end
-
-lemma complete_ins: "complete t \<Longrightarrow> complete (treeI(ins a t)) \<and> height(ins a t) = height t"
+lemma complete_ins: "complete t \<Longrightarrow> complete (treeI(ins a t)) \<and> hI(ins a t) = height t"
 by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *)
 
 text\<open>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 \<Rightarrow> nat" where
-"height (TD t) = height t" |
-"height (UF t) = height t + 1"
-
-instance ..
-
-end
+fun hD :: "'a upD \<Rightarrow> nat" where
+"hD (TD t) = height t" |
+"hD (UF t) = height t + 1"
 
 lemma complete_treeD_node21:
-  "\<lbrakk>complete r; complete (treeD l'); height r = height l' \<rbrakk> \<Longrightarrow> complete (treeD (node21 l' a r))"
+  "\<lbrakk>complete r; complete (treeD l'); height r = hD l' \<rbrakk> \<Longrightarrow> complete (treeD (node21 l' a r))"
 by(induct l' a r rule: node21.induct) auto
 
 lemma complete_treeD_node22:
-  "\<lbrakk>complete(treeD r'); complete l; height r' = height l \<rbrakk> \<Longrightarrow> complete (treeD (node22 l a r'))"
+  "\<lbrakk>complete(treeD r'); complete l; hD r' = height l \<rbrakk> \<Longrightarrow> complete (treeD (node22 l a r'))"
 by(induct l a r' rule: node22.induct) auto
 
 lemma complete_treeD_node31:
-  "\<lbrakk> complete (treeD l'); complete m; complete r; height l' = height r; height m = height r \<rbrakk>
+  "\<lbrakk> complete (treeD l'); complete m; complete r; hD l' = height r; height m = height r \<rbrakk>
   \<Longrightarrow> complete (treeD (node31 l' a m b r))"
 by(induct l' a m b r rule: node31.induct) auto
 
 lemma complete_treeD_node32:
-  "\<lbrakk> complete l; complete (treeD m'); complete r; height l = height r; height m' = height r \<rbrakk>
+  "\<lbrakk> complete l; complete (treeD m'); complete r; height l = height r; hD m' = height r \<rbrakk>
   \<Longrightarrow> complete (treeD (node32 l a m' b r))"
 by(induct l a m' b r rule: node32.induct) auto
 
 lemma complete_treeD_node33:
-  "\<lbrakk> complete l; complete m; complete(treeD r'); height l = height r'; height m = height r' \<rbrakk>
+  "\<lbrakk> complete l; complete m; complete(treeD r'); height l = hD r'; height m = hD r' \<rbrakk>
   \<Longrightarrow> 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 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
+   "height r > 0 \<Longrightarrow> 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 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1"
+   "height l > 0 \<Longrightarrow> 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 \<Longrightarrow> height(node31 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
+  "height m > 0 \<Longrightarrow> 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 \<Longrightarrow> height(node32 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
+  "height r > 0 \<Longrightarrow> 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 \<Longrightarrow> height(node33 l a m b r) =
-   max (height l) (max (height m) (height r)) + 1"
+  "height m > 0 \<Longrightarrow> 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') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> height t' = height t"
+  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> 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 \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> hD(del x t) = height t"
 by(induction x t rule: del.induct)
   (auto simp: heights max_def height_split_min split: prod.splits)