src/HOL/Data_Structures/AA_Set.thy
changeset 62130 90a3016a6c12
parent 61793 4c9e1e5a240e
child 62160 ff20b44b2fc8
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Mon Jan 11 18:27:27 2016 +0100
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Mon Jan 11 20:51:13 2016 +0100
     1.3 @@ -1,9 +1,10 @@
     1.4  (*
     1.5  Author: Tobias Nipkow
     1.6 -Invariants are under development
     1.7 +
     1.8 +Added trivial cases to function `adjust' to obviate invariants.
     1.9  *)
    1.10  
    1.11 -section \<open>An AA Tree Implementation of Sets\<close>
    1.12 +section \<open>AA Tree Implementation of Sets\<close>
    1.13  
    1.14  theory AA_Set
    1.15  imports
    1.16 @@ -16,13 +17,13 @@
    1.17  fun lvl :: "'a aa_tree \<Rightarrow> nat" where
    1.18  "lvl Leaf = 0" |
    1.19  "lvl (Node lv _ _ _) = lv"
    1.20 -
    1.21 +(*
    1.22  fun invar :: "'a aa_tree \<Rightarrow> bool" where
    1.23  "invar Leaf = True" |
    1.24  "invar (Node h l a r) =
    1.25   (invar l \<and> invar r \<and>
    1.26    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.27 -
    1.28 +*)
    1.29  fun skew :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.30  "skew (Node lva (Node lvb t1 b t2) a t3) =
    1.31    (if lva = lvb then Node lva t1 b (Node lva t2 a t3) else Node lva (Node lvb t1 b t2) a t3)" |
    1.32 @@ -105,8 +106,7 @@
    1.33  subsubsection "Proofs for delete"
    1.34  
    1.35  lemma del_maxD:
    1.36 -  "\<lbrakk> del_max t = (t',x); t \<noteq> Leaf; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    1.37 -   inorder t' @ [x] = inorder t"
    1.38 +  "\<lbrakk> del_max t = (t',x); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> inorder t' @ [x] = inorder t"
    1.39  by(induction t arbitrary: t' rule: del_max.induct)
    1.40    (auto simp: sorted_lems split: prod.splits)
    1.41