diff -r 72d19e588e97 -r 90a3016a6c12 src/HOL/Data_Structures/AA_Set.thy --- a/src/HOL/Data_Structures/AA_Set.thy Mon Jan 11 18:27:27 2016 +0100 +++ b/src/HOL/Data_Structures/AA_Set.thy Mon Jan 11 20:51:13 2016 +0100 @@ -1,9 +1,10 @@ (* Author: Tobias Nipkow -Invariants are under development + +Added trivial cases to function `adjust' to obviate invariants. *) -section \An AA Tree Implementation of Sets\ +section \AA Tree Implementation of Sets\ theory AA_Set imports @@ -16,13 +17,13 @@ fun lvl :: "'a aa_tree \ nat" where "lvl Leaf = 0" | "lvl (Node lv _ _ _) = lv" - +(* fun invar :: "'a aa_tree \ bool" where "invar Leaf = True" | "invar (Node h l a r) = (invar l \ invar r \ h = lvl l + 1 \ (h = lvl r + 1 \ (\lr b rr. r = Node h lr b rr \ h = lvl rr + 1)))" - +*) fun skew :: "'a aa_tree \ 'a aa_tree" where "skew (Node lva (Node lvb t1 b t2) a t3) = (if lva = lvb then Node lva t1 b (Node lva t2 a t3) else Node lva (Node lvb t1 b t2) a t3)" | @@ -105,8 +106,7 @@ subsubsection "Proofs for delete" lemma del_maxD: - "\ del_max t = (t',x); t \ Leaf; sorted(inorder t) \ \ - inorder t' @ [x] = inorder t" + "\ del_max t = (t',x); t \ Leaf \ \ inorder t' @ [x] = inorder t" by(induction t arbitrary: t' rule: del_max.induct) (auto simp: sorted_lems split: prod.splits)