tuned names
authornipkow
Mon May 20 17:33:13 2019 +0200 (8 weeks ago ago)
changeset 704587daa65d45462
parent 70457 acc1749c2be9
child 70459 0d9135dc3460
child 70460 91a2f79b546b
tuned names
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
     1.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Thu May 16 19:43:21 2019 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Mon May 20 17:33:13 2019 +0200
     1.3 @@ -22,37 +22,37 @@
     1.4            EQ \<Rightarrow> Some b2 |
     1.5            GT \<Rightarrow> lookup r x))"
     1.6  
     1.7 -fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
     1.8 -"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
     1.9 +fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) upI" where
    1.10 +"upd x y Leaf = OF Leaf (x,y) Leaf" |
    1.11  "upd x y (Node2 l ab r) = (case cmp x (fst ab) of
    1.12     LT \<Rightarrow> (case upd x y l of
    1.13 -           T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
    1.14 -         | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) |
    1.15 -   EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
    1.16 +           TI l' => TI (Node2 l' ab r)
    1.17 +         | OF l1 ab' l2 => TI (Node3 l1 ab' l2 ab r)) |
    1.18 +   EQ \<Rightarrow> TI (Node2 l (x,y) r) |
    1.19     GT \<Rightarrow> (case upd x y r of
    1.20 -           T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
    1.21 -         | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" |
    1.22 +           TI r' => TI (Node2 l ab r')
    1.23 +         | OF r1 ab' r2 => TI (Node3 l ab r1 ab' r2)))" |
    1.24  "upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
    1.25     LT \<Rightarrow> (case upd x y l of
    1.26 -           T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
    1.27 -         | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) |
    1.28 -   EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
    1.29 +           TI l' => TI (Node3 l' ab1 m ab2 r)
    1.30 +         | OF l1 ab' l2 => OF (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) |
    1.31 +   EQ \<Rightarrow> TI (Node3 l (x,y) m ab2 r) |
    1.32     GT \<Rightarrow> (case cmp x (fst ab2) of
    1.33             LT \<Rightarrow> (case upd x y m of
    1.34 -                   T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
    1.35 -                 | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) |
    1.36 -           EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
    1.37 +                   TI m' => TI (Node3 l ab1 m' ab2 r)
    1.38 +                 | OF m1 ab' m2 => OF (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) |
    1.39 +           EQ \<Rightarrow> TI (Node3 l ab1 m (x,y) r) |
    1.40             GT \<Rightarrow> (case upd x y r of
    1.41 -                   T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
    1.42 -                 | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))"
    1.43 +                   TI r' => TI (Node3 l ab1 m ab2 r')
    1.44 +                 | OF r1 ab' r2 => OF (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))"
    1.45  
    1.46  definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
    1.47 -"update a b t = tree\<^sub>i(upd a b t)"
    1.48 +"update a b t = treeI(upd a b t)"
    1.49  
    1.50 -fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
    1.51 -"del x Leaf = T\<^sub>d Leaf" |
    1.52 -"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
    1.53 -"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
    1.54 +fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) upD" where
    1.55 +"del x Leaf = TD Leaf" |
    1.56 +"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then UF Leaf else TD(Node2 Leaf ab1 Leaf))" |
    1.57 +"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = TD(if x=fst ab1 then Node2 Leaf ab2 Leaf
    1.58    else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" |
    1.59  "del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
    1.60    LT \<Rightarrow> node21 (del x l) ab1 r |
    1.61 @@ -67,7 +67,7 @@
    1.62             GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
    1.63  
    1.64  definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
    1.65 -"delete x t = tree\<^sub>d(del x t)"
    1.66 +"delete x t = treeD(del x t)"
    1.67  
    1.68  
    1.69  subsection \<open>Functional Correctness\<close>
    1.70 @@ -78,8 +78,8 @@
    1.71  
    1.72  
    1.73  lemma inorder_upd:
    1.74 -  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)"
    1.75 -by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
    1.76 +  "sorted1(inorder t) \<Longrightarrow> inorder(treeI(upd x y t)) = upd_list x y (inorder t)"
    1.77 +by(induction t) (auto simp: upd_list_simps split: upI.splits)
    1.78  
    1.79  corollary inorder_update:
    1.80    "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    1.81 @@ -87,7 +87,7 @@
    1.82  
    1.83  
    1.84  lemma inorder_del: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    1.85 -  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    1.86 +  inorder(treeD (del x t)) = del_list x (inorder t)"
    1.87  by(induction t rule: del.induct)
    1.88    (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
    1.89  
    1.90 @@ -98,8 +98,8 @@
    1.91  
    1.92  subsection \<open>Balancedness\<close>
    1.93  
    1.94 -lemma complete_upd: "complete t \<Longrightarrow> complete (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
    1.95 -by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *)
    1.96 +lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> height(upd x y t) = height t"
    1.97 +by (induct t) (auto split!: if_split upI.split)(* 16 secs in 2015 *)
    1.98  
    1.99  corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)"
   1.100  by (simp add: update_def complete_upd)
   1.101 @@ -109,12 +109,12 @@
   1.102  by(induction x t rule: del.induct)
   1.103    (auto simp add: heights max_def height_split_min split: prod.split)
   1.104  
   1.105 -lemma complete_tree\<^sub>d_del: "complete t \<Longrightarrow> complete(tree\<^sub>d(del x t))"
   1.106 +lemma complete_treeD_del: "complete t \<Longrightarrow> complete(treeD(del x t))"
   1.107  by(induction x t rule: del.induct)
   1.108    (auto simp: completes complete_split_min height_del height_split_min split: prod.split)
   1.109  
   1.110  corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)"
   1.111 -by(simp add: delete_def complete_tree\<^sub>d_del)
   1.112 +by(simp add: delete_def complete_treeD_del)
   1.113  
   1.114  
   1.115  subsection \<open>Overall Correctness\<close>
     2.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu May 16 19:43:21 2019 +0200
     2.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Mon May 20 17:33:13 2019 +0200
     2.3 @@ -31,97 +31,97 @@
     2.4            EQ \<Rightarrow> True |
     2.5            GT \<Rightarrow> isin r x))"
     2.6  
     2.7 -datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
     2.8 +datatype 'a upI = TI "'a tree23" | OF "'a tree23" 'a "'a tree23"
     2.9  
    2.10 -fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
    2.11 -"tree\<^sub>i (T\<^sub>i t) = t" |
    2.12 -"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
    2.13 +fun treeI :: "'a upI \<Rightarrow> 'a tree23" where
    2.14 +"treeI (TI t) = t" |
    2.15 +"treeI (OF l a r) = Node2 l a r"
    2.16  
    2.17 -fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
    2.18 -"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
    2.19 +fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a upI" where
    2.20 +"ins x Leaf = OF Leaf x Leaf" |
    2.21  "ins x (Node2 l a r) =
    2.22     (case cmp x a of
    2.23        LT \<Rightarrow>
    2.24          (case ins x l of
    2.25 -           T\<^sub>i l' => T\<^sub>i (Node2 l' a r) |
    2.26 -           Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
    2.27 -      EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
    2.28 +           TI l' => TI (Node2 l' a r) |
    2.29 +           OF l1 b l2 => TI (Node3 l1 b l2 a r)) |
    2.30 +      EQ \<Rightarrow> TI (Node2 l x r) |
    2.31        GT \<Rightarrow>
    2.32          (case ins x r of
    2.33 -           T\<^sub>i r' => T\<^sub>i (Node2 l a r') |
    2.34 -           Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
    2.35 +           TI r' => TI (Node2 l a r') |
    2.36 +           OF r1 b r2 => TI (Node3 l a r1 b r2)))" |
    2.37  "ins x (Node3 l a m b r) =
    2.38     (case cmp x a of
    2.39        LT \<Rightarrow>
    2.40          (case ins x l of
    2.41 -           T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) |
    2.42 -           Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
    2.43 -      EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    2.44 +           TI l' => TI (Node3 l' a m b r) |
    2.45 +           OF l1 c l2 => OF (Node2 l1 c l2) a (Node2 m b r)) |
    2.46 +      EQ \<Rightarrow> TI (Node3 l a m b r) |
    2.47        GT \<Rightarrow>
    2.48          (case cmp x b of
    2.49             GT \<Rightarrow>
    2.50               (case ins x r of
    2.51 -                T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') |
    2.52 -                Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
    2.53 -           EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    2.54 +                TI r' => TI (Node3 l a m b r') |
    2.55 +                OF r1 c r2 => OF (Node2 l a m) b (Node2 r1 c r2)) |
    2.56 +           EQ \<Rightarrow> TI (Node3 l a m b r) |
    2.57             LT \<Rightarrow>
    2.58               (case ins x m of
    2.59 -                T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) |
    2.60 -                Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
    2.61 +                TI m' => TI (Node3 l a m' b r) |
    2.62 +                OF m1 c m2 => OF (Node2 l a m1) c (Node2 m2 b r))))"
    2.63  
    2.64  hide_const insert
    2.65  
    2.66  definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
    2.67 -"insert x t = tree\<^sub>i(ins x t)"
    2.68 +"insert x t = treeI(ins x t)"
    2.69  
    2.70 -datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
    2.71 +datatype 'a upD = TD "'a tree23" | UF "'a tree23"
    2.72  
    2.73 -fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
    2.74 -"tree\<^sub>d (T\<^sub>d t) = t" |
    2.75 -"tree\<^sub>d (Up\<^sub>d t) = t"
    2.76 +fun treeD :: "'a upD \<Rightarrow> 'a tree23" where
    2.77 +"treeD (TD t) = t" |
    2.78 +"treeD (UF t) = t"
    2.79  
    2.80  (* Variation: return None to signal no-change *)
    2.81  
    2.82 -fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    2.83 -"node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" |
    2.84 -"node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" |
    2.85 -"node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
    2.86 +fun node21 :: "'a upD \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
    2.87 +"node21 (TD t1) a t2 = TD(Node2 t1 a t2)" |
    2.88 +"node21 (UF t1) a (Node2 t2 b t3) = UF(Node3 t1 a t2 b t3)" |
    2.89 +"node21 (UF t1) a (Node3 t2 b t3 c t4) = TD(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
    2.90  
    2.91 -fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
    2.92 -"node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" |
    2.93 -"node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" |
    2.94 -"node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
    2.95 +fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a upD \<Rightarrow> 'a upD" where
    2.96 +"node22 t1 a (TD t2) = TD(Node2 t1 a t2)" |
    2.97 +"node22 (Node2 t1 b t2) a (UF t3) = UF(Node3 t1 b t2 a t3)" |
    2.98 +"node22 (Node3 t1 b t2 c t3) a (UF t4) = TD(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
    2.99  
   2.100 -fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
   2.101 -"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
   2.102 -"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
   2.103 -"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"
   2.104 +fun node31 :: "'a upD \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
   2.105 +"node31 (TD t1) a t2 b t3 = TD(Node3 t1 a t2 b t3)" |
   2.106 +"node31 (UF t1) a (Node2 t2 b t3) c t4 = TD(Node2 (Node3 t1 a t2 b t3) c t4)" |
   2.107 +"node31 (UF t1) a (Node3 t2 b t3 c t4) d t5 = TD(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"
   2.108  
   2.109 -fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
   2.110 -"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
   2.111 -"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
   2.112 -"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
   2.113 +fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a upD \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
   2.114 +"node32 t1 a (TD t2) b t3 = TD(Node3 t1 a t2 b t3)" |
   2.115 +"node32 t1 a (UF t2) b (Node2 t3 c t4) = TD(Node2 t1 a (Node3 t2 b t3 c t4))" |
   2.116 +"node32 t1 a (UF t2) b (Node3 t3 c t4 d t5) = TD(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
   2.117  
   2.118 -fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
   2.119 -"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
   2.120 -"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
   2.121 -"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
   2.122 +fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a upD \<Rightarrow> 'a upD" where
   2.123 +"node33 l a m b (TD r) = TD(Node3 l a m b r)" |
   2.124 +"node33 t1 a (Node2 t2 b t3) c (UF t4) = TD(Node2 t1 a (Node3 t2 b t3 c t4))" |
   2.125 +"node33 t1 a (Node3 t2 b t3 c t4) d (UF t5) = TD(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
   2.126  
   2.127 -fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
   2.128 -"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
   2.129 -"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
   2.130 +fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a upD" where
   2.131 +"split_min (Node2 Leaf a Leaf) = (a, UF Leaf)" |
   2.132 +"split_min (Node3 Leaf a Leaf b Leaf) = (a, TD(Node2 Leaf b Leaf))" |
   2.133  "split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
   2.134  "split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
   2.135  
   2.136  text \<open>In the base cases of \<open>split_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
   2.137  in which case balancedness implies that so are the others. Exercise.\<close>
   2.138  
   2.139 -fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
   2.140 -"del x Leaf = T\<^sub>d Leaf" |
   2.141 +fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
   2.142 +"del x Leaf = TD Leaf" |
   2.143  "del x (Node2 Leaf a Leaf) =
   2.144 -  (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
   2.145 +  (if x = a then UF Leaf else TD(Node2 Leaf a Leaf))" |
   2.146  "del x (Node3 Leaf a Leaf b Leaf) =
   2.147 -  T\<^sub>d(if x = a then Node2 Leaf b Leaf else
   2.148 +  TD(if x = a then Node2 Leaf b Leaf else
   2.149       if x = b then Node2 Leaf a Leaf
   2.150       else Node3 Leaf a Leaf b Leaf)" |
   2.151  "del x (Node2 l a r) =
   2.152 @@ -140,7 +140,7 @@
   2.153            GT \<Rightarrow> node33 l a m b (del x r)))"
   2.154  
   2.155  definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   2.156 -"delete x t = tree\<^sub>d(del x t)"
   2.157 +"delete x t = treeD(del x t)"
   2.158  
   2.159  
   2.160  subsection "Functional Correctness"
   2.161 @@ -154,8 +154,8 @@
   2.162  subsubsection "Proofs for insert"
   2.163  
   2.164  lemma inorder_ins:
   2.165 -  "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
   2.166 -by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits)
   2.167 +  "sorted(inorder t) \<Longrightarrow> inorder(treeI(ins x t)) = ins_list x (inorder t)"
   2.168 +by(induction t) (auto simp: ins_list_simps split: upI.splits)
   2.169  
   2.170  lemma inorder_insert:
   2.171    "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
   2.172 @@ -165,23 +165,23 @@
   2.173  subsubsection "Proofs for delete"
   2.174  
   2.175  lemma inorder_node21: "height r > 0 \<Longrightarrow>
   2.176 -  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
   2.177 +  inorder (treeD (node21 l' a r)) = inorder (treeD l') @ a # inorder r"
   2.178  by(induct l' a r rule: node21.induct) auto
   2.179  
   2.180  lemma inorder_node22: "height l > 0 \<Longrightarrow>
   2.181 -  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
   2.182 +  inorder (treeD (node22 l a r')) = inorder l @ a # inorder (treeD r')"
   2.183  by(induct l a r' rule: node22.induct) auto
   2.184  
   2.185  lemma inorder_node31: "height m > 0 \<Longrightarrow>
   2.186 -  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
   2.187 +  inorder (treeD (node31 l' a m b r)) = inorder (treeD l') @ a # inorder m @ b # inorder r"
   2.188  by(induct l' a m b r rule: node31.induct) auto
   2.189  
   2.190  lemma inorder_node32: "height r > 0 \<Longrightarrow>
   2.191 -  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
   2.192 +  inorder (treeD (node32 l a m' b r)) = inorder l @ a # inorder (treeD m') @ b # inorder r"
   2.193  by(induct l a m' b r rule: node32.induct) auto
   2.194  
   2.195  lemma inorder_node33: "height m > 0 \<Longrightarrow>
   2.196 -  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
   2.197 +  inorder (treeD (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (treeD r')"
   2.198  by(induct l a m b r' rule: node33.induct) auto
   2.199  
   2.200  lemmas inorder_nodes = inorder_node21 inorder_node22
   2.201 @@ -189,12 +189,12 @@
   2.202  
   2.203  lemma split_minD:
   2.204    "split_min t = (x,t') \<Longrightarrow> complete t \<Longrightarrow> height t > 0 \<Longrightarrow>
   2.205 -  x # inorder(tree\<^sub>d t') = inorder t"
   2.206 +  x # inorder(treeD t') = inorder t"
   2.207  by(induction t arbitrary: t' rule: split_min.induct)
   2.208    (auto simp: inorder_nodes split: prod.splits)
   2.209  
   2.210  lemma inorder_del: "\<lbrakk> complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   2.211 -  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   2.212 +  inorder(treeD (del x t)) = del_list x (inorder t)"
   2.213  by(induction t rule: del.induct)
   2.214    (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
   2.215  
   2.216 @@ -210,19 +210,19 @@
   2.217  
   2.218  text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>complete\<close>.\<close>
   2.219  
   2.220 -instantiation up\<^sub>i :: (type)height
   2.221 +instantiation upI :: (type)height
   2.222  begin
   2.223  
   2.224 -fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
   2.225 -"height (T\<^sub>i t) = height t" |
   2.226 -"height (Up\<^sub>i l a r) = height l"
   2.227 +fun height_upI :: "'a upI \<Rightarrow> nat" where
   2.228 +"height (TI t) = height t" |
   2.229 +"height (OF l a r) = height l"
   2.230  
   2.231  instance ..
   2.232  
   2.233  end
   2.234  
   2.235 -lemma complete_ins: "complete t \<Longrightarrow> complete (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
   2.236 -by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
   2.237 +lemma complete_ins: "complete t \<Longrightarrow> complete (treeI(ins a t)) \<and> height(ins a t) = height t"
   2.238 +by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *)
   2.239  
   2.240  text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
   2.241  two properties (balance and height) are combined in one predicate.\<close>
   2.242 @@ -267,15 +267,15 @@
   2.243    by (auto elim!: complete_imp_full full_imp_complete)
   2.244  
   2.245  text \<open>The \<^const>\<open>insert\<close> function either preserves the height of the
   2.246 -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
   2.247 -form \<^term>\<open>Up\<^sub>i l p r\<close> indicates an increase in height.\<close>
   2.248 +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>TI t\<close> indicates that the height will be the same. A value of the
   2.249 +form \<^term>\<open>OF l p r\<close> indicates an increase in height.\<close>
   2.250  
   2.251 -fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
   2.252 -"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
   2.253 -"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
   2.254 +fun full\<^sub>i :: "nat \<Rightarrow> 'a upI \<Rightarrow> bool" where
   2.255 +"full\<^sub>i n (TI t) \<longleftrightarrow> full n t" |
   2.256 +"full\<^sub>i n (OF l p r) \<longleftrightarrow> full n l \<and> full n r"
   2.257  
   2.258  lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
   2.259 -by (induct rule: full.induct) (auto split: up\<^sub>i.split)
   2.260 +by (induct rule: full.induct) (auto split: upI.split)
   2.261  
   2.262  text \<open>The \<^const>\<open>insert\<close> operation preserves completeance.\<close>
   2.263  
   2.264 @@ -290,42 +290,42 @@
   2.265  
   2.266  subsection "Proofs for delete"
   2.267  
   2.268 -instantiation up\<^sub>d :: (type)height
   2.269 +instantiation upD :: (type)height
   2.270  begin
   2.271  
   2.272 -fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
   2.273 -"height (T\<^sub>d t) = height t" |
   2.274 -"height (Up\<^sub>d t) = height t + 1"
   2.275 +fun height_upD :: "'a upD \<Rightarrow> nat" where
   2.276 +"height (TD t) = height t" |
   2.277 +"height (UF t) = height t + 1"
   2.278  
   2.279  instance ..
   2.280  
   2.281  end
   2.282  
   2.283 -lemma complete_tree\<^sub>d_node21:
   2.284 -  "\<lbrakk>complete r; complete (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d (node21 l' a r))"
   2.285 +lemma complete_treeD_node21:
   2.286 +  "\<lbrakk>complete r; complete (treeD l'); height r = height l' \<rbrakk> \<Longrightarrow> complete (treeD (node21 l' a r))"
   2.287  by(induct l' a r rule: node21.induct) auto
   2.288  
   2.289 -lemma complete_tree\<^sub>d_node22:
   2.290 -  "\<lbrakk>complete(tree\<^sub>d r'); complete l; height r' = height l \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d (node22 l a r'))"
   2.291 +lemma complete_treeD_node22:
   2.292 +  "\<lbrakk>complete(treeD r'); complete l; height r' = height l \<rbrakk> \<Longrightarrow> complete (treeD (node22 l a r'))"
   2.293  by(induct l a r' rule: node22.induct) auto
   2.294  
   2.295 -lemma complete_tree\<^sub>d_node31:
   2.296 -  "\<lbrakk> complete (tree\<^sub>d l'); complete m; complete r; height l' = height r; height m = height r \<rbrakk>
   2.297 -  \<Longrightarrow> complete (tree\<^sub>d (node31 l' a m b r))"
   2.298 +lemma complete_treeD_node31:
   2.299 +  "\<lbrakk> complete (treeD l'); complete m; complete r; height l' = height r; height m = height r \<rbrakk>
   2.300 +  \<Longrightarrow> complete (treeD (node31 l' a m b r))"
   2.301  by(induct l' a m b r rule: node31.induct) auto
   2.302  
   2.303 -lemma complete_tree\<^sub>d_node32:
   2.304 -  "\<lbrakk> complete l; complete (tree\<^sub>d m'); complete r; height l = height r; height m' = height r \<rbrakk>
   2.305 -  \<Longrightarrow> complete (tree\<^sub>d (node32 l a m' b r))"
   2.306 +lemma complete_treeD_node32:
   2.307 +  "\<lbrakk> complete l; complete (treeD m'); complete r; height l = height r; height m' = height r \<rbrakk>
   2.308 +  \<Longrightarrow> complete (treeD (node32 l a m' b r))"
   2.309  by(induct l a m' b r rule: node32.induct) auto
   2.310  
   2.311 -lemma complete_tree\<^sub>d_node33:
   2.312 -  "\<lbrakk> complete l; complete m; complete(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
   2.313 -  \<Longrightarrow> complete (tree\<^sub>d (node33 l a m b r'))"
   2.314 +lemma complete_treeD_node33:
   2.315 +  "\<lbrakk> complete l; complete m; complete(treeD r'); height l = height r'; height m = height r' \<rbrakk>
   2.316 +  \<Longrightarrow> complete (treeD (node33 l a m b r'))"
   2.317  by(induct l a m b r' rule: node33.induct) auto
   2.318  
   2.319 -lemmas completes = complete_tree\<^sub>d_node21 complete_tree\<^sub>d_node22
   2.320 -  complete_tree\<^sub>d_node31 complete_tree\<^sub>d_node32 complete_tree\<^sub>d_node33
   2.321 +lemmas completes = complete_treeD_node21 complete_treeD_node22
   2.322 +  complete_treeD_node31 complete_treeD_node32 complete_treeD_node33
   2.323  
   2.324  lemma height'_node21:
   2.325     "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
   2.326 @@ -363,16 +363,16 @@
   2.327    (auto simp: heights max_def height_split_min split: prod.splits)
   2.328  
   2.329  lemma complete_split_min:
   2.330 -  "\<lbrakk> split_min t = (x, t'); complete t; height t > 0 \<rbrakk> \<Longrightarrow> complete (tree\<^sub>d t')"
   2.331 +  "\<lbrakk> split_min t = (x, t'); complete t; height t > 0 \<rbrakk> \<Longrightarrow> complete (treeD t')"
   2.332  by(induct t arbitrary: x t' rule: split_min.induct)
   2.333    (auto simp: heights height_split_min completes split: prod.splits)
   2.334  
   2.335 -lemma complete_tree\<^sub>d_del: "complete t \<Longrightarrow> complete(tree\<^sub>d(del x t))"
   2.336 +lemma complete_treeD_del: "complete t \<Longrightarrow> complete(treeD(del x t))"
   2.337  by(induction x t rule: del.induct)
   2.338    (auto simp: completes complete_split_min height_del height_split_min split: prod.splits)
   2.339  
   2.340  corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)"
   2.341 -by(simp add: delete_def complete_tree\<^sub>d_del)
   2.342 +by(simp add: delete_def complete_treeD_del)
   2.343  
   2.344  
   2.345  subsection \<open>Overall Correctness\<close>