src/HOL/Data_Structures/AA_Set.thy
changeset 68413 b56ed5010e69
parent 68023 75130777ece4
child 68431 b294e095f64c
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Mon Jun 11 16:29:27 2018 +0200
     1.3 @@ -14,60 +14,60 @@
     1.4  
     1.5  fun lvl :: "'a aa_tree \<Rightarrow> nat" where
     1.6  "lvl Leaf = 0" |
     1.7 -"lvl (Node lv _ _ _) = lv"
     1.8 +"lvl (Node _ _ lv _) = lv"
     1.9  
    1.10  fun invar :: "'a aa_tree \<Rightarrow> bool" where
    1.11  "invar Leaf = True" |
    1.12 -"invar (Node h l a r) =
    1.13 +"invar (Node l a h r) =
    1.14   (invar l \<and> invar r \<and>
    1.15 -  h = lvl l + 1 \<and> (h = lvl r + 1 \<or> (\<exists>lr b rr. r = Node h lr b rr \<and> h = lvl rr + 1)))"
    1.16 +  h = lvl l + 1 \<and> (h = lvl r + 1 \<or> (\<exists>lr b rr. r = Node lr b h rr \<and> h = lvl rr + 1)))"
    1.17  
    1.18  fun skew :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.19 -"skew (Node lva (Node lvb t1 b t2) a t3) =
    1.20 -  (if lva = lvb then Node lva t1 b (Node lva t2 a t3) else Node lva (Node lvb t1 b t2) a t3)" |
    1.21 +"skew (Node (Node t1 b lvb t2) a lva t3) =
    1.22 +  (if lva = lvb then Node t1 b lvb (Node t2 a lva t3) else Node (Node t1 b lvb t2) a lva t3)" |
    1.23  "skew t = t"
    1.24  
    1.25  fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.26 -"split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
    1.27 +"split (Node t1 a lva (Node t2 b lvb (Node t3 c lvc t4))) =
    1.28     (if lva = lvb \<and> lvb = lvc \<comment> \<open>\<open>lva = lvc\<close> suffices\<close>
    1.29 -    then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
    1.30 -    else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
    1.31 +    then Node (Node t1 a lva t2) b (lva+1) (Node t3 c lva t4)
    1.32 +    else Node t1 a lva (Node t2 b lvb (Node t3 c lvc t4)))" |
    1.33  "split t = t"
    1.34  
    1.35  hide_const (open) insert
    1.36  
    1.37  fun insert :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.38 -"insert x Leaf = Node 1 Leaf x Leaf" |
    1.39 -"insert x (Node lv t1 a t2) =
    1.40 +"insert x Leaf = Node Leaf x 1 Leaf" |
    1.41 +"insert x (Node t1 a lv t2) =
    1.42    (case cmp x a of
    1.43 -     LT \<Rightarrow> split (skew (Node lv (insert x t1) a t2)) |
    1.44 -     GT \<Rightarrow> split (skew (Node lv t1 a (insert x t2))) |
    1.45 -     EQ \<Rightarrow> Node lv t1 x t2)"
    1.46 +     LT \<Rightarrow> split (skew (Node (insert x t1) a lv t2)) |
    1.47 +     GT \<Rightarrow> split (skew (Node t1 a lv (insert x t2))) |
    1.48 +     EQ \<Rightarrow> Node t1 x lv t2)"
    1.49  
    1.50  fun sngl :: "'a aa_tree \<Rightarrow> bool" where
    1.51  "sngl Leaf = False" |
    1.52  "sngl (Node _ _ _ Leaf) = True" |
    1.53 -"sngl (Node lva _ _ (Node lvb _ _ _)) = (lva > lvb)"
    1.54 +"sngl (Node _ _ lva (Node _ _ lvb _)) = (lva > lvb)"
    1.55  
    1.56  definition adjust :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.57  "adjust t =
    1.58   (case t of
    1.59 -  Node lv l x r \<Rightarrow>
    1.60 +  Node l x lv r \<Rightarrow>
    1.61     (if lvl l >= lv-1 \<and> lvl r >= lv-1 then t else
    1.62 -    if lvl r < lv-1 \<and> sngl l then skew (Node (lv-1) l x r) else
    1.63 +    if lvl r < lv-1 \<and> sngl l then skew (Node l x (lv-1) r) else
    1.64      if lvl r < lv-1
    1.65      then case l of
    1.66 -           Node lva t1 a (Node lvb t2 b t3)
    1.67 -             \<Rightarrow> Node (lvb+1) (Node lva t1 a t2) b (Node (lv-1) t3 x r) 
    1.68 +           Node t1 a lva (Node t2 b lvb t3)
    1.69 +             \<Rightarrow> Node (Node t1 a lva t2) b (lvb+1) (Node t3 x (lv-1) r) 
    1.70      else
    1.71 -    if lvl r < lv then split (Node (lv-1) l x r)
    1.72 +    if lvl r < lv then split (Node l x (lv-1) r)
    1.73      else
    1.74        case r of
    1.75 -        Node lvb t1 b t4 \<Rightarrow>
    1.76 +        Node t1 b lvb t4 \<Rightarrow>
    1.77            (case t1 of
    1.78 -             Node lva t2 a t3
    1.79 -               \<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
    1.80 -                    (split (Node (if sngl t1 then lva else lva+1) t3 b t4)))))"
    1.81 +             Node t2 a lva t3
    1.82 +               \<Rightarrow> Node (Node l x (lv-1) t2) a (lva+1)
    1.83 +                    (split (Node t3 b (if sngl t1 then lva else lva+1) t4)))))"
    1.84  
    1.85  text\<open>In the paper, the last case of @{const adjust} is expressed with the help of an
    1.86  incorrect auxiliary function \texttt{nlvl}.
    1.87 @@ -78,20 +78,20 @@
    1.88  is not restored.\<close>
    1.89  
    1.90  fun split_max :: "'a aa_tree \<Rightarrow> 'a aa_tree * 'a" where
    1.91 -"split_max (Node lv l a Leaf) = (l,a)" |
    1.92 -"split_max (Node lv l a r) = (let (r',b) = split_max r in (adjust(Node lv l a r'), b))"
    1.93 +"split_max (Node l a lv Leaf) = (l,a)" |
    1.94 +"split_max (Node l a lv r) = (let (r',b) = split_max r in (adjust(Node l a lv r'), b))"
    1.95  
    1.96  fun delete :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.97  "delete _ Leaf = Leaf" |
    1.98 -"delete x (Node lv l a r) =
    1.99 +"delete x (Node l a lv r) =
   1.100    (case cmp x a of
   1.101 -     LT \<Rightarrow> adjust (Node lv (delete x l) a r) |
   1.102 -     GT \<Rightarrow> adjust (Node lv l a (delete x r)) |
   1.103 +     LT \<Rightarrow> adjust (Node (delete x l) a lv r) |
   1.104 +     GT \<Rightarrow> adjust (Node l a lv (delete x r)) |
   1.105       EQ \<Rightarrow> (if l = Leaf then r
   1.106 -            else let (l',b) = split_max l in adjust (Node lv l' b r)))"
   1.107 +            else let (l',b) = split_max l in adjust (Node l' b lv r)))"
   1.108  
   1.109  fun pre_adjust where
   1.110 -"pre_adjust (Node lv l a r) = (invar l \<and> invar r \<and>
   1.111 +"pre_adjust (Node l a lv r) = (invar l \<and> invar r \<and>
   1.112      ((lv = lvl l + 1 \<and> (lv = lvl r + 1 \<or> lv = lvl r + 2 \<or> lv = lvl r \<and> sngl r)) \<or>
   1.113       (lv = lvl l + 2 \<and> (lv = lvl r + 1 \<or> lv = lvl r \<and> sngl r))))"
   1.114  
   1.115 @@ -100,23 +100,23 @@
   1.116  subsection "Auxiliary Proofs"
   1.117  
   1.118  lemma split_case: "split t = (case t of
   1.119 -  Node lvx a x (Node lvy b y (Node lvz c z d)) \<Rightarrow>
   1.120 +  Node t1 x lvx (Node t2 y lvy (Node t3 z lvz t4)) \<Rightarrow>
   1.121     (if lvx = lvy \<and> lvy = lvz
   1.122 -    then Node (lvx+1) (Node lvx a x b) y (Node lvx c z d)
   1.123 +    then Node (Node t1 x lvx t2) y (lvx+1) (Node t3 z lvx t4)
   1.124      else t)
   1.125    | t \<Rightarrow> t)"
   1.126  by(auto split: tree.split)
   1.127  
   1.128  lemma skew_case: "skew t = (case t of
   1.129 -  Node lvx (Node lvy a y b) x c \<Rightarrow>
   1.130 -  (if lvx = lvy then Node lvx a y (Node lvx b x c) else t)
   1.131 +  Node (Node t1 y lvy t2) x lvx t3 \<Rightarrow>
   1.132 +  (if lvx = lvy then Node t1 y lvx (Node t2 x lvx t3) else t)
   1.133   | t \<Rightarrow> t)"
   1.134  by(auto split: tree.split)
   1.135  
   1.136  lemma lvl_0_iff: "invar t \<Longrightarrow> lvl t = 0 \<longleftrightarrow> t = Leaf"
   1.137  by(cases t) auto
   1.138  
   1.139 -lemma lvl_Suc_iff: "lvl t = Suc n \<longleftrightarrow> (\<exists> l a r. t = Node (Suc n) l a r)"
   1.140 +lemma lvl_Suc_iff: "lvl t = Suc n \<longleftrightarrow> (\<exists> l a r. t = Node l a (Suc n) r)"
   1.141  by(cases t) auto
   1.142  
   1.143  lemma lvl_skew: "lvl (skew t) = lvl t"
   1.144 @@ -125,16 +125,16 @@
   1.145  lemma lvl_split: "lvl (split t) = lvl t \<or> lvl (split t) = lvl t + 1 \<and> sngl (split t)"
   1.146  by(cases t rule: split.cases) auto
   1.147  
   1.148 -lemma invar_2Nodes:"invar (Node lv l x (Node rlv rl rx rr)) =
   1.149 -     (invar l \<and> invar \<langle>rlv, rl, rx, rr\<rangle> \<and> lv = Suc (lvl l) \<and>
   1.150 +lemma invar_2Nodes:"invar (Node l x lv (Node rl rx rlv rr)) =
   1.151 +     (invar l \<and> invar \<langle>rl, rx, rlv, rr\<rangle> \<and> lv = Suc (lvl l) \<and>
   1.152       (lv = Suc rlv \<or> rlv = lv \<and> lv = Suc (lvl rr)))"
   1.153  by simp
   1.154  
   1.155  lemma invar_NodeLeaf[simp]:
   1.156 -  "invar (Node lv l x Leaf) = (invar l \<and> lv = Suc (lvl l) \<and> lv = Suc 0)"
   1.157 +  "invar (Node l x lv Leaf) = (invar l \<and> lv = Suc (lvl l) \<and> lv = Suc 0)"
   1.158  by simp
   1.159  
   1.160 -lemma sngl_if_invar: "invar (Node n l a r) \<Longrightarrow> n = lvl r \<Longrightarrow> sngl r"
   1.161 +lemma sngl_if_invar: "invar (Node l a n r) \<Longrightarrow> n = lvl r \<Longrightarrow> sngl r"
   1.162  by(cases r rule: sngl.cases) clarsimp+
   1.163  
   1.164  
   1.165 @@ -156,7 +156,7 @@
   1.166  
   1.167  lemma lvl_insert_sngl: "invar t \<Longrightarrow> sngl t \<Longrightarrow> lvl(insert x t) = lvl t"
   1.168  proof (induction t rule: insert.induct)
   1.169 -  case (2 x lv t1 a t2)
   1.170 +  case (2 x t1 a lv t2)
   1.171    consider (LT) "x < a" | (GT) "x > a" | (EQ) "x = a" 
   1.172      using less_linear by blast 
   1.173    thus ?case proof cases
   1.174 @@ -180,20 +180,20 @@
   1.175  by(cases t rule: split.cases) clarsimp+
   1.176  
   1.177  lemma invar_NodeL:
   1.178 -  "\<lbrakk> invar(Node n l x r); invar l'; lvl l' = lvl l \<rbrakk> \<Longrightarrow> invar(Node n l' x r)"
   1.179 +  "\<lbrakk> invar(Node l x n r); invar l'; lvl l' = lvl l \<rbrakk> \<Longrightarrow> invar(Node l' x n r)"
   1.180  by(auto)
   1.181  
   1.182  lemma invar_NodeR:
   1.183 -  "\<lbrakk> invar(Node n l x r); n = lvl r + 1; invar r'; lvl r' = lvl r \<rbrakk> \<Longrightarrow> invar(Node n l x r')"
   1.184 +  "\<lbrakk> invar(Node l x n r); n = lvl r + 1; invar r'; lvl r' = lvl r \<rbrakk> \<Longrightarrow> invar(Node l x n r')"
   1.185  by(auto)
   1.186  
   1.187  lemma invar_NodeR2:
   1.188 -  "\<lbrakk> invar(Node n l x r); sngl r'; n = lvl r + 1; invar r'; lvl r' = n \<rbrakk> \<Longrightarrow> invar(Node n l x r')"
   1.189 +  "\<lbrakk> invar(Node l x n r); sngl r'; n = lvl r + 1; invar r'; lvl r' = n \<rbrakk> \<Longrightarrow> invar(Node l x n r')"
   1.190  by(cases r' rule: sngl.cases) clarsimp+
   1.191  
   1.192  
   1.193  lemma lvl_insert_incr_iff: "(lvl(insert a t) = lvl t + 1) \<longleftrightarrow>
   1.194 -  (\<exists>l x r. insert a t = Node (lvl t + 1) l x r \<and> lvl l = lvl r)"
   1.195 +  (\<exists>l x r. insert a t = Node l x (lvl t + 1) r \<and> lvl l = lvl r)"
   1.196  apply(cases t)
   1.197  apply(auto simp add: skew_case split_case split: if_splits)
   1.198  apply(auto split: tree.splits if_splits)
   1.199 @@ -201,11 +201,11 @@
   1.200  
   1.201  lemma invar_insert: "invar t \<Longrightarrow> invar(insert a t)"
   1.202  proof(induction t)
   1.203 -  case N: (Node n l x r)
   1.204 +  case N: (Node l x n r)
   1.205    hence il: "invar l" and ir: "invar r" by auto
   1.206    note iil = N.IH(1)[OF il]
   1.207    note iir = N.IH(2)[OF ir]
   1.208 -  let ?t = "Node n l x r"
   1.209 +  let ?t = "Node l x n r"
   1.210    have "a < x \<or> a = x \<or> x < a" by auto
   1.211    moreover
   1.212    have ?case if "a < x"
   1.213 @@ -215,13 +215,13 @@
   1.214        by (simp add: skew_invar split_invar del: invar.simps)
   1.215    next
   1.216      case (Incr)
   1.217 -    then obtain t1 w t2 where ial[simp]: "insert a l = Node n t1 w t2"
   1.218 +    then obtain t1 w t2 where ial[simp]: "insert a l = Node t1 w n t2"
   1.219        using N.prems by (auto simp: lvl_Suc_iff)
   1.220      have l12: "lvl t1 = lvl t2"
   1.221        by (metis Incr(1) ial lvl_insert_incr_iff tree.inject)
   1.222 -    have "insert a ?t = split(skew(Node n (insert a l) x r))"
   1.223 +    have "insert a ?t = split(skew(Node (insert a l) x n r))"
   1.224        by(simp add: \<open>a<x\<close>)
   1.225 -    also have "skew(Node n (insert a l) x r) = Node n t1 w (Node n t2 x r)"
   1.226 +    also have "skew(Node (insert a l) x n r) = Node t1 w n (Node t2 x n r)"
   1.227        by(simp)
   1.228      also have "invar(split \<dots>)"
   1.229      proof (cases r)
   1.230 @@ -229,7 +229,7 @@
   1.231        hence "l = Leaf" using N.prems by(auto simp: lvl_0_iff)
   1.232        thus ?thesis using Leaf ial by simp
   1.233      next
   1.234 -      case [simp]: (Node m t3 y t4)
   1.235 +      case [simp]: (Node t3 y m t4)
   1.236        show ?thesis (*using N(3) iil l12 by(auto)*)
   1.237        proof cases
   1.238          assume "m = n" thus ?thesis using N(3) iil by(auto)
   1.239 @@ -246,14 +246,14 @@
   1.240      thus ?case
   1.241      proof
   1.242        assume 0: "n = lvl r"
   1.243 -      have "insert a ?t = split(skew(Node n l x (insert a r)))"
   1.244 +      have "insert a ?t = split(skew(Node l x n (insert a r)))"
   1.245          using \<open>a>x\<close> by(auto)
   1.246 -      also have "skew(Node n l x (insert a r)) = Node n l x (insert a r)"
   1.247 +      also have "skew(Node l x n (insert a r)) = Node l x n (insert a r)"
   1.248          using N.prems by(simp add: skew_case split: tree.split)
   1.249        also have "invar(split \<dots>)"
   1.250        proof -
   1.251          from lvl_insert_sngl[OF ir sngl_if_invar[OF \<open>invar ?t\<close> 0], of a]
   1.252 -        obtain t1 y t2 where iar: "insert a r = Node n t1 y t2"
   1.253 +        obtain t1 y t2 where iar: "insert a r = Node t1 y n t2"
   1.254            using N.prems 0 by (auto simp: lvl_Suc_iff)
   1.255          from N.prems iar 0 iir
   1.256          show ?thesis by (auto simp: split_case split: tree.splits)
   1.257 @@ -282,21 +282,21 @@
   1.258  
   1.259  subsubsection "Proofs for delete"
   1.260  
   1.261 -lemma invarL: "ASSUMPTION(invar \<langle>lv, l, a, r\<rangle>) \<Longrightarrow> invar l"
   1.262 +lemma invarL: "ASSUMPTION(invar \<langle>l, a, lv, r\<rangle>) \<Longrightarrow> invar l"
   1.263  by(simp add: ASSUMPTION_def)
   1.264  
   1.265  lemma invarR: "ASSUMPTION(invar \<langle>lv, l, a, r\<rangle>) \<Longrightarrow> invar r"
   1.266  by(simp add: ASSUMPTION_def)
   1.267  
   1.268  lemma sngl_NodeI:
   1.269 -  "sngl (Node lv l a r) \<Longrightarrow> sngl (Node lv l' a' r)"
   1.270 +  "sngl (Node l a lv r) \<Longrightarrow> sngl (Node l' a' lv r)"
   1.271  by(cases r) (simp_all)
   1.272  
   1.273  
   1.274  declare invarL[simp] invarR[simp]
   1.275  
   1.276  lemma pre_cases:
   1.277 -assumes "pre_adjust (Node lv l x r)"
   1.278 +assumes "pre_adjust (Node l x lv r)"
   1.279  obtains
   1.280   (tSngl) "invar l \<and> invar r \<and>
   1.281      lv = Suc (lvl r) \<and> lvl l = lvl r" |
   1.282 @@ -314,38 +314,38 @@
   1.283  declare invar.simps(2)[simp del] invar_2Nodes[simp add]
   1.284  
   1.285  lemma invar_adjust:
   1.286 -  assumes pre: "pre_adjust (Node lv l a r)"
   1.287 -  shows  "invar(adjust (Node lv l a r))"
   1.288 +  assumes pre: "pre_adjust (Node l a lv r)"
   1.289 +  shows  "invar(adjust (Node l a lv r))"
   1.290  using pre proof (cases rule: pre_cases)
   1.291    case (tDouble) thus ?thesis unfolding adjust_def by (cases r) (auto simp: invar.simps(2)) 
   1.292  next 
   1.293    case (rDown)
   1.294 -  from rDown obtain llv ll la lr where l: "l = Node llv ll la lr" by (cases l) auto
   1.295 +  from rDown obtain llv ll la lr where l: "l = Node ll la llv lr" by (cases l) auto
   1.296    from rDown show ?thesis unfolding adjust_def by (auto simp: l invar.simps(2) split: tree.splits)
   1.297  next
   1.298    case (lDown_tDouble)
   1.299 -  from lDown_tDouble obtain rlv rr ra rl where r: "r = Node rlv rl ra rr" by (cases r) auto
   1.300 +  from lDown_tDouble obtain rlv rr ra rl where r: "r = Node rl ra rlv rr" by (cases r) auto
   1.301    from lDown_tDouble and r obtain rrlv rrr rra rrl where
   1.302 -    rr :"rr = Node rrlv rrr rra rrl" by (cases rr) auto
   1.303 +    rr :"rr = Node rrr rra rrlv rrl" by (cases rr) auto
   1.304    from  lDown_tDouble show ?thesis unfolding adjust_def r rr
   1.305      apply (cases rl) apply (auto simp add: invar.simps(2) split!: if_split)
   1.306      using lDown_tDouble by (auto simp: split_case lvl_0_iff  elim:lvl.elims split: tree.split)
   1.307  qed (auto simp: split_case invar.simps(2) adjust_def split: tree.splits)
   1.308  
   1.309  lemma lvl_adjust:
   1.310 -  assumes "pre_adjust (Node lv l a r)"
   1.311 -  shows "lv = lvl (adjust(Node lv l a r)) \<or> lv = lvl (adjust(Node lv l a r)) + 1"
   1.312 +  assumes "pre_adjust (Node l a lv r)"
   1.313 +  shows "lv = lvl (adjust(Node l a lv r)) \<or> lv = lvl (adjust(Node l a lv r)) + 1"
   1.314  using assms(1) proof(cases rule: pre_cases)
   1.315    case lDown_tSngl thus ?thesis
   1.316 -    using lvl_split[of "\<langle>lvl r, l, a, r\<rangle>"] by (auto simp: adjust_def)
   1.317 +    using lvl_split[of "\<langle>l, a, lvl r, r\<rangle>"] by (auto simp: adjust_def)
   1.318  next
   1.319    case lDown_tDouble thus ?thesis
   1.320      by (auto simp: adjust_def invar.simps(2) split: tree.split)
   1.321  qed (auto simp: adjust_def split: tree.splits)
   1.322  
   1.323 -lemma sngl_adjust: assumes "pre_adjust (Node lv l a r)"
   1.324 -  "sngl \<langle>lv, l, a, r\<rangle>" "lv = lvl (adjust \<langle>lv, l, a, r\<rangle>)"
   1.325 -  shows "sngl (adjust \<langle>lv, l, a, r\<rangle>)" 
   1.326 +lemma sngl_adjust: assumes "pre_adjust (Node l a lv r)"
   1.327 +  "sngl \<langle>l, a, lv, r\<rangle>" "lv = lvl (adjust \<langle>l, a, lv, r\<rangle>)"
   1.328 +  shows "sngl (adjust \<langle>l, a, lv, r\<rangle>)" 
   1.329  using assms proof (cases rule: pre_cases)
   1.330    case rDown
   1.331    thus ?thesis using assms(2,3) unfolding adjust_def
   1.332 @@ -363,13 +363,13 @@
   1.333    (auto simp: pre_adjust.simps post_del_def invar.simps(2) elim: sngl.elims)
   1.334  
   1.335  lemma pre_adj_if_postL:
   1.336 -  "invar\<langle>lv, l, a, r\<rangle> \<Longrightarrow> post_del l l' \<Longrightarrow> pre_adjust \<langle>lv, l', b, r\<rangle>"
   1.337 +  "invar\<langle>l, a, lv, r\<rangle> \<Longrightarrow> post_del l l' \<Longrightarrow> pre_adjust \<langle>l', b, lv, r\<rangle>"
   1.338  by(cases "sngl r")
   1.339    (auto simp: pre_adjust.simps post_del_def invar.simps(2) elim: sngl.elims)
   1.340  
   1.341  lemma post_del_adjL:
   1.342 -  "\<lbrakk> invar\<langle>lv, l, a, r\<rangle>; pre_adjust \<langle>lv, l', b, r\<rangle> \<rbrakk>
   1.343 -  \<Longrightarrow> post_del \<langle>lv, l, a, r\<rangle> (adjust \<langle>lv, l', b, r\<rangle>)"
   1.344 +  "\<lbrakk> invar\<langle>l, a, lv, r\<rangle>; pre_adjust \<langle>l', b, lv, r\<rangle> \<rbrakk>
   1.345 +  \<Longrightarrow> post_del \<langle>l, a, lv, r\<rangle> (adjust \<langle>l', b, lv, r\<rangle>)"
   1.346  unfolding post_del_def
   1.347  by (metis invar_adjust lvl_adjust sngl_NodeI sngl_adjust lvl.simps(2))
   1.348  
   1.349 @@ -412,10 +412,10 @@
   1.350  
   1.351  theorem post_delete: "invar t \<Longrightarrow> post_del t (delete x t)"
   1.352  proof (induction t)
   1.353 -  case (Node lv l a r)
   1.354 +  case (Node l a lv r)
   1.355  
   1.356    let ?l' = "delete x l" and ?r' = "delete x r"
   1.357 -  let ?t = "Node lv l a r" let ?t' = "delete x ?t"
   1.358 +  let ?t = "Node l a lv r" let ?t' = "delete x ?t"
   1.359  
   1.360    from Node.prems have inv_l: "invar l" and inv_r: "invar r" by (auto)
   1.361