# HG changeset patch
# User nipkow
# Date 1558028601 -7200
# Node ID acc1749c2be98a2232baf95c89a9d973e0b35915
# Parent  1d564a895296e3ea3c8a35b321c131502a060fd9
tuned name

diff -r 1d564a895296 -r acc1749c2be9 src/HOL/Data_Structures/Tree23.thy
--- a/src/HOL/Data_Structures/Tree23.thy	Thu May 16 12:59:37 2019 +0200
+++ b/src/HOL/Data_Structures/Tree23.thy	Thu May 16 19:43:21 2019 +0200
@@ -34,13 +34,13 @@
 
 text \<open>Balanced:\<close>
 
-fun bal :: "'a tree23 \<Rightarrow> bool" where
-"bal Leaf = True" |
-"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
-"bal (Node3 l _ m _ r) =
-  (bal l & bal m & bal r & height l = height m & height m = height r)"
+fun complete :: "'a tree23 \<Rightarrow> bool" where
+"complete Leaf = True" |
+"complete (Node2 l _ r) = (complete l & complete r & height l = height r)" |
+"complete (Node3 l _ m _ r) =
+  (complete l & complete m & complete r & height l = height m & height m = height r)"
 
-lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
+lemma ht_sz_if_complete: "complete t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
 by (induction t) auto
 
 end
diff -r 1d564a895296 -r acc1749c2be9 src/HOL/Data_Structures/Tree23_Map.thy
--- a/src/HOL/Data_Structures/Tree23_Map.thy	Thu May 16 12:59:37 2019 +0200
+++ b/src/HOL/Data_Structures/Tree23_Map.thy	Thu May 16 19:43:21 2019 +0200
@@ -86,42 +86,42 @@
 by(simp add: update_def inorder_upd)
 
 
-lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+lemma inorder_del: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
 by(induction t rule: del.induct)
   (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
 
-corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+corollary inorder_delete: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(delete x t) = del_list x (inorder t)"
 by(simp add: delete_def inorder_del)
 
 
 subsection \<open>Balancedness\<close>
 
-lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
+lemma complete_upd: "complete t \<Longrightarrow> complete (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
 by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *)
 
-corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)"
-by (simp add: update_def bal_upd)
+corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)"
+by (simp add: update_def complete_upd)
 
 
-lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
 by(induction x t rule: del.induct)
   (auto simp add: heights max_def height_split_min split: prod.split)
 
-lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
+lemma complete_tree\<^sub>d_del: "complete t \<Longrightarrow> complete(tree\<^sub>d(del x t))"
 by(induction x t rule: del.induct)
-  (auto simp: bals bal_split_min height_del height_split_min split: prod.split)
+  (auto simp: completes complete_split_min height_del height_split_min split: prod.split)
 
-corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
-by(simp add: delete_def bal_tree\<^sub>d_del)
+corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)"
+by(simp add: delete_def complete_tree\<^sub>d_del)
 
 
 subsection \<open>Overall Correctness\<close>
 
 interpretation M: Map_by_Ordered
 where empty = empty and lookup = lookup and update = update and delete = delete
-and inorder = inorder and inv = bal
+and inorder = inorder and inv = complete
 proof (standard, goal_cases)
   case 1 thus ?case by(simp add: empty_def)
 next
@@ -133,9 +133,9 @@
 next
   case 5 thus ?case by(simp add: empty_def)
 next
-  case 6 thus ?case by(simp add: bal_update)
+  case 6 thus ?case by(simp add: complete_update)
 next
-  case 7 thus ?case by(simp add: bal_delete)
+  case 7 thus ?case by(simp add: complete_delete)
 qed
 
 end
diff -r 1d564a895296 -r acc1749c2be9 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu May 16 12:59:37 2019 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu May 16 19:43:21 2019 +0200
@@ -188,17 +188,17 @@
   inorder_node31 inorder_node32 inorder_node33
 
 lemma split_minD:
-  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
+  "split_min t = (x,t') \<Longrightarrow> complete t \<Longrightarrow> height t > 0 \<Longrightarrow>
   x # inorder(tree\<^sub>d t') = inorder t"
 by(induction t arbitrary: t' rule: split_min.induct)
   (auto simp: inorder_nodes split: prod.splits)
 
-lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+lemma inorder_del: "\<lbrakk> complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
 by(induction t rule: del.induct)
   (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
 
-lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+lemma inorder_delete: "\<lbrakk> complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(delete x t) = del_list x (inorder t)"
 by(simp add: delete_def inorder_del)
 
@@ -208,7 +208,7 @@
 
 subsubsection "Proofs for insert"
 
-text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>bal\<close>.\<close>
+text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>complete\<close>.\<close>
 
 instantiation up\<^sub>i :: (type)height
 begin
@@ -221,7 +221,7 @@
 
 end
 
-lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
+lemma complete_ins: "complete t \<Longrightarrow> complete (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
 by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
 
 text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
@@ -257,14 +257,14 @@
 lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
   by (induct set: full, simp_all)
 
-lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
+lemma full_imp_complete: "full n t \<Longrightarrow> complete t"
   by (induct set: full, auto dest: full_imp_height)
 
-lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
+lemma complete_imp_full: "complete t \<Longrightarrow> full (height t) t"
   by (induct t, simp_all)
 
-lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
-  by (auto elim!: bal_imp_full full_imp_bal)
+lemma complete_iff_full: "complete t \<longleftrightarrow> (\<exists>n. full n t)"
+  by (auto elim!: complete_imp_full full_imp_complete)
 
 text \<open>The \<^const>\<open>insert\<close> function either preserves the height of the
 tree, or increases it by one. The constructor returned by the \<^term>\<open>insert\<close> function determines which: A return value of the form \<^term>\<open>T\<^sub>i t\<close> indicates that the height will be the same. A value of the
@@ -277,10 +277,10 @@
 lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
 by (induct rule: full.induct) (auto split: up\<^sub>i.split)
 
-text \<open>The \<^const>\<open>insert\<close> operation preserves balance.\<close>
+text \<open>The \<^const>\<open>insert\<close> operation preserves completeance.\<close>
 
-lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
-unfolding bal_iff_full insert_def
+lemma complete_insert: "complete t \<Longrightarrow> complete (insert a t)"
+unfolding complete_iff_full insert_def
 apply (erule exE)
 apply (drule full\<^sub>i_ins [of _ _ a])
 apply (cases "ins a t")
@@ -301,31 +301,31 @@
 
 end
 
-lemma bal_tree\<^sub>d_node21:
-  "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))"
+lemma complete_tree\<^sub>d_node21:
+  "\<lbrakk>complete r; complete (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d (node21 l' a r))"
 by(induct l' a r rule: node21.induct) auto
 
-lemma bal_tree\<^sub>d_node22:
-  "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))"
+lemma complete_tree\<^sub>d_node22:
+  "\<lbrakk>complete(tree\<^sub>d r'); complete l; height r' = height l \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d (node22 l a r'))"
 by(induct l a r' rule: node22.induct) auto
 
-lemma bal_tree\<^sub>d_node31:
-  "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))"
+lemma complete_tree\<^sub>d_node31:
+  "\<lbrakk> complete (tree\<^sub>d l'); complete m; complete r; height l' = height r; height m = height r \<rbrakk>
+  \<Longrightarrow> complete (tree\<^sub>d (node31 l' a m b r))"
 by(induct l' a m b r rule: node31.induct) auto
 
-lemma bal_tree\<^sub>d_node32:
-  "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))"
+lemma complete_tree\<^sub>d_node32:
+  "\<lbrakk> complete l; complete (tree\<^sub>d m'); complete r; height l = height r; height m' = height r \<rbrakk>
+  \<Longrightarrow> complete (tree\<^sub>d (node32 l a m' b r))"
 by(induct l a m' b r rule: node32.induct) auto
 
-lemma bal_tree\<^sub>d_node33:
-  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
-  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))"
+lemma complete_tree\<^sub>d_node33:
+  "\<lbrakk> complete l; complete m; complete(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
+  \<Longrightarrow> complete (tree\<^sub>d (node33 l a m b r'))"
 by(induct l a m b r' rule: node33.induct) auto
 
-lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
-  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
+lemmas completes = complete_tree\<^sub>d_node21 complete_tree\<^sub>d_node22
+  complete_tree\<^sub>d_node31 complete_tree\<^sub>d_node32 complete_tree\<^sub>d_node33
 
 lemma height'_node21:
    "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
@@ -354,32 +354,32 @@
   height'_node31 height'_node32 height'_node33
 
 lemma height_split_min:
-  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
+  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> height t' = height t"
 by(induct t arbitrary: x t' rule: split_min.induct)
   (auto simp: heights split: prod.splits)
 
-lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
 by(induction x t rule: del.induct)
   (auto simp: heights max_def height_split_min split: prod.splits)
 
-lemma bal_split_min:
-  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
+lemma complete_split_min:
+  "\<lbrakk> split_min t = (x, t'); complete t; height t > 0 \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d t')"
 by(induct t arbitrary: x t' rule: split_min.induct)
-  (auto simp: heights height_split_min bals split: prod.splits)
+  (auto simp: heights height_split_min completes split: prod.splits)
 
-lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
+lemma complete_tree\<^sub>d_del: "complete t \<Longrightarrow> complete(tree\<^sub>d(del x t))"
 by(induction x t rule: del.induct)
-  (auto simp: bals bal_split_min height_del height_split_min split: prod.splits)
+  (auto simp: completes complete_split_min height_del height_split_min split: prod.splits)
 
-corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
-by(simp add: delete_def bal_tree\<^sub>d_del)
+corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)"
+by(simp add: delete_def complete_tree\<^sub>d_del)
 
 
 subsection \<open>Overall Correctness\<close>
 
 interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
-and inorder = inorder and inv = bal
+and inorder = inorder and inv = complete
 proof (standard, goal_cases)
   case 2 thus ?case by(simp add: isin_set)
 next
@@ -387,9 +387,9 @@
 next
   case 4 thus ?case by(simp add: inorder_delete)
 next
-  case 6 thus ?case by(simp add: bal_insert)
+  case 6 thus ?case by(simp add: complete_insert)
 next
-  case 7 thus ?case by(simp add: bal_delete)
+  case 7 thus ?case by(simp add: complete_delete)
 qed (simp add: empty_def)+
 
 end