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.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
```