tuned name default tip
authornipkow
Thu May 16 19:43:21 2019 +0200 (3 days ago ago)
changeset 70457acc1749c2be9
parent 70456 1d564a895296
tuned name
src/HOL/Data_Structures/Tree23.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
     1.1 --- a/src/HOL/Data_Structures/Tree23.thy	Thu May 16 12:59:37 2019 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree23.thy	Thu May 16 19:43:21 2019 +0200
     1.3 @@ -34,13 +34,13 @@
     1.4  
     1.5  text \<open>Balanced:\<close>
     1.6  
     1.7 -fun bal :: "'a tree23 \<Rightarrow> bool" where
     1.8 -"bal Leaf = True" |
     1.9 -"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
    1.10 -"bal (Node3 l _ m _ r) =
    1.11 -  (bal l & bal m & bal r & height l = height m & height m = height r)"
    1.12 +fun complete :: "'a tree23 \<Rightarrow> bool" where
    1.13 +"complete Leaf = True" |
    1.14 +"complete (Node2 l _ r) = (complete l & complete r & height l = height r)" |
    1.15 +"complete (Node3 l _ m _ r) =
    1.16 +  (complete l & complete m & complete r & height l = height m & height m = height r)"
    1.17  
    1.18 -lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
    1.19 +lemma ht_sz_if_complete: "complete t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
    1.20  by (induction t) auto
    1.21  
    1.22  end
     2.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Thu May 16 12:59:37 2019 +0200
     2.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Thu May 16 19:43:21 2019 +0200
     2.3 @@ -86,42 +86,42 @@
     2.4  by(simp add: update_def inorder_upd)
     2.5  
     2.6  
     2.7 -lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
     2.8 +lemma inorder_del: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
     2.9    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    2.10  by(induction t rule: del.induct)
    2.11    (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
    2.12  
    2.13 -corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    2.14 +corollary inorder_delete: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    2.15    inorder(delete x t) = del_list x (inorder t)"
    2.16  by(simp add: delete_def inorder_del)
    2.17  
    2.18  
    2.19  subsection \<open>Balancedness\<close>
    2.20  
    2.21 -lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
    2.22 +lemma complete_upd: "complete t \<Longrightarrow> complete (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
    2.23  by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *)
    2.24  
    2.25 -corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)"
    2.26 -by (simp add: update_def bal_upd)
    2.27 +corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)"
    2.28 +by (simp add: update_def complete_upd)
    2.29  
    2.30  
    2.31 -lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
    2.32 +lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
    2.33  by(induction x t rule: del.induct)
    2.34    (auto simp add: heights max_def height_split_min split: prod.split)
    2.35  
    2.36 -lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
    2.37 +lemma complete_tree\<^sub>d_del: "complete t \<Longrightarrow> complete(tree\<^sub>d(del x t))"
    2.38  by(induction x t rule: del.induct)
    2.39 -  (auto simp: bals bal_split_min height_del height_split_min split: prod.split)
    2.40 +  (auto simp: completes complete_split_min height_del height_split_min split: prod.split)
    2.41  
    2.42 -corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
    2.43 -by(simp add: delete_def bal_tree\<^sub>d_del)
    2.44 +corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)"
    2.45 +by(simp add: delete_def complete_tree\<^sub>d_del)
    2.46  
    2.47  
    2.48  subsection \<open>Overall Correctness\<close>
    2.49  
    2.50  interpretation M: Map_by_Ordered
    2.51  where empty = empty and lookup = lookup and update = update and delete = delete
    2.52 -and inorder = inorder and inv = bal
    2.53 +and inorder = inorder and inv = complete
    2.54  proof (standard, goal_cases)
    2.55    case 1 thus ?case by(simp add: empty_def)
    2.56  next
    2.57 @@ -133,9 +133,9 @@
    2.58  next
    2.59    case 5 thus ?case by(simp add: empty_def)
    2.60  next
    2.61 -  case 6 thus ?case by(simp add: bal_update)
    2.62 +  case 6 thus ?case by(simp add: complete_update)
    2.63  next
    2.64 -  case 7 thus ?case by(simp add: bal_delete)
    2.65 +  case 7 thus ?case by(simp add: complete_delete)
    2.66  qed
    2.67  
    2.68  end
     3.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu May 16 12:59:37 2019 +0200
     3.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu May 16 19:43:21 2019 +0200
     3.3 @@ -188,17 +188,17 @@
     3.4    inorder_node31 inorder_node32 inorder_node33
     3.5  
     3.6  lemma split_minD:
     3.7 -  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
     3.8 +  "split_min t = (x,t') \<Longrightarrow> complete t \<Longrightarrow> height t > 0 \<Longrightarrow>
     3.9    x # inorder(tree\<^sub>d t') = inorder t"
    3.10  by(induction t arbitrary: t' rule: split_min.induct)
    3.11    (auto simp: inorder_nodes split: prod.splits)
    3.12  
    3.13 -lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    3.14 +lemma inorder_del: "\<lbrakk> complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    3.15    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    3.16  by(induction t rule: del.induct)
    3.17    (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
    3.18  
    3.19 -lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    3.20 +lemma inorder_delete: "\<lbrakk> complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    3.21    inorder(delete x t) = del_list x (inorder t)"
    3.22  by(simp add: delete_def inorder_del)
    3.23  
    3.24 @@ -208,7 +208,7 @@
    3.25  
    3.26  subsubsection "Proofs for insert"
    3.27  
    3.28 -text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>bal\<close>.\<close>
    3.29 +text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>complete\<close>.\<close>
    3.30  
    3.31  instantiation up\<^sub>i :: (type)height
    3.32  begin
    3.33 @@ -221,7 +221,7 @@
    3.34  
    3.35  end
    3.36  
    3.37 -lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
    3.38 +lemma complete_ins: "complete t \<Longrightarrow> complete (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
    3.39  by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
    3.40  
    3.41  text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
    3.42 @@ -257,14 +257,14 @@
    3.43  lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
    3.44    by (induct set: full, simp_all)
    3.45  
    3.46 -lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
    3.47 +lemma full_imp_complete: "full n t \<Longrightarrow> complete t"
    3.48    by (induct set: full, auto dest: full_imp_height)
    3.49  
    3.50 -lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
    3.51 +lemma complete_imp_full: "complete t \<Longrightarrow> full (height t) t"
    3.52    by (induct t, simp_all)
    3.53  
    3.54 -lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
    3.55 -  by (auto elim!: bal_imp_full full_imp_bal)
    3.56 +lemma complete_iff_full: "complete t \<longleftrightarrow> (\<exists>n. full n t)"
    3.57 +  by (auto elim!: complete_imp_full full_imp_complete)
    3.58  
    3.59  text \<open>The \<^const>\<open>insert\<close> function either preserves the height of the
    3.60  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
    3.61 @@ -277,10 +277,10 @@
    3.62  lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
    3.63  by (induct rule: full.induct) (auto split: up\<^sub>i.split)
    3.64  
    3.65 -text \<open>The \<^const>\<open>insert\<close> operation preserves balance.\<close>
    3.66 +text \<open>The \<^const>\<open>insert\<close> operation preserves completeance.\<close>
    3.67  
    3.68 -lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
    3.69 -unfolding bal_iff_full insert_def
    3.70 +lemma complete_insert: "complete t \<Longrightarrow> complete (insert a t)"
    3.71 +unfolding complete_iff_full insert_def
    3.72  apply (erule exE)
    3.73  apply (drule full\<^sub>i_ins [of _ _ a])
    3.74  apply (cases "ins a t")
    3.75 @@ -301,31 +301,31 @@
    3.76  
    3.77  end
    3.78  
    3.79 -lemma bal_tree\<^sub>d_node21:
    3.80 -  "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))"
    3.81 +lemma complete_tree\<^sub>d_node21:
    3.82 +  "\<lbrakk>complete r; complete (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d (node21 l' a r))"
    3.83  by(induct l' a r rule: node21.induct) auto
    3.84  
    3.85 -lemma bal_tree\<^sub>d_node22:
    3.86 -  "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))"
    3.87 +lemma complete_tree\<^sub>d_node22:
    3.88 +  "\<lbrakk>complete(tree\<^sub>d r'); complete l; height r' = height l \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d (node22 l a r'))"
    3.89  by(induct l a r' rule: node22.induct) auto
    3.90  
    3.91 -lemma bal_tree\<^sub>d_node31:
    3.92 -  "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk>
    3.93 -  \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))"
    3.94 +lemma complete_tree\<^sub>d_node31:
    3.95 +  "\<lbrakk> complete (tree\<^sub>d l'); complete m; complete r; height l' = height r; height m = height r \<rbrakk>
    3.96 +  \<Longrightarrow> complete (tree\<^sub>d (node31 l' a m b r))"
    3.97  by(induct l' a m b r rule: node31.induct) auto
    3.98  
    3.99 -lemma bal_tree\<^sub>d_node32:
   3.100 -  "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk>
   3.101 -  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))"
   3.102 +lemma complete_tree\<^sub>d_node32:
   3.103 +  "\<lbrakk> complete l; complete (tree\<^sub>d m'); complete r; height l = height r; height m' = height r \<rbrakk>
   3.104 +  \<Longrightarrow> complete (tree\<^sub>d (node32 l a m' b r))"
   3.105  by(induct l a m' b r rule: node32.induct) auto
   3.106  
   3.107 -lemma bal_tree\<^sub>d_node33:
   3.108 -  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
   3.109 -  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))"
   3.110 +lemma complete_tree\<^sub>d_node33:
   3.111 +  "\<lbrakk> complete l; complete m; complete(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
   3.112 +  \<Longrightarrow> complete (tree\<^sub>d (node33 l a m b r'))"
   3.113  by(induct l a m b r' rule: node33.induct) auto
   3.114  
   3.115 -lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
   3.116 -  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
   3.117 +lemmas completes = complete_tree\<^sub>d_node21 complete_tree\<^sub>d_node22
   3.118 +  complete_tree\<^sub>d_node31 complete_tree\<^sub>d_node32 complete_tree\<^sub>d_node33
   3.119  
   3.120  lemma height'_node21:
   3.121     "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
   3.122 @@ -354,32 +354,32 @@
   3.123    height'_node31 height'_node32 height'_node33
   3.124  
   3.125  lemma height_split_min:
   3.126 -  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
   3.127 +  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> height t' = height t"
   3.128  by(induct t arbitrary: x t' rule: split_min.induct)
   3.129    (auto simp: heights split: prod.splits)
   3.130  
   3.131 -lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   3.132 +lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
   3.133  by(induction x t rule: del.induct)
   3.134    (auto simp: heights max_def height_split_min split: prod.splits)
   3.135  
   3.136 -lemma bal_split_min:
   3.137 -  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
   3.138 +lemma complete_split_min:
   3.139 +  "\<lbrakk> split_min t = (x, t'); complete t; height t > 0 \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d t')"
   3.140  by(induct t arbitrary: x t' rule: split_min.induct)
   3.141 -  (auto simp: heights height_split_min bals split: prod.splits)
   3.142 +  (auto simp: heights height_split_min completes split: prod.splits)
   3.143  
   3.144 -lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   3.145 +lemma complete_tree\<^sub>d_del: "complete t \<Longrightarrow> complete(tree\<^sub>d(del x t))"
   3.146  by(induction x t rule: del.induct)
   3.147 -  (auto simp: bals bal_split_min height_del height_split_min split: prod.splits)
   3.148 +  (auto simp: completes complete_split_min height_del height_split_min split: prod.splits)
   3.149  
   3.150 -corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   3.151 -by(simp add: delete_def bal_tree\<^sub>d_del)
   3.152 +corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)"
   3.153 +by(simp add: delete_def complete_tree\<^sub>d_del)
   3.154  
   3.155  
   3.156  subsection \<open>Overall Correctness\<close>
   3.157  
   3.158  interpretation S: Set_by_Ordered
   3.159  where empty = empty and isin = isin and insert = insert and delete = delete
   3.160 -and inorder = inorder and inv = bal
   3.161 +and inorder = inorder and inv = complete
   3.162  proof (standard, goal_cases)
   3.163    case 2 thus ?case by(simp add: isin_set)
   3.164  next
   3.165 @@ -387,9 +387,9 @@
   3.166  next
   3.167    case 4 thus ?case by(simp add: inorder_delete)
   3.168  next
   3.169 -  case 6 thus ?case by(simp add: bal_insert)
   3.170 +  case 6 thus ?case by(simp add: complete_insert)
   3.171  next
   3.172 -  case 7 thus ?case by(simp add: bal_delete)
   3.173 +  case 7 thus ?case by(simp add: complete_delete)
   3.174  qed (simp add: empty_def)+
   3.175  
   3.176  end