src/HOL/Data_Structures/AA_Set.thy
author nipkow
Sun Dec 06 17:27:42 2015 +0100 (2015-12-06)
changeset 61793 4c9e1e5a240e
child 62130 90a3016a6c12
permissions -rw-r--r--
added AA trees
     1 (*
     2 Author: Tobias Nipkow
     3 Invariants are under development
     4 *)
     5 
     6 section \<open>An AA Tree Implementation of Sets\<close>
     7 
     8 theory AA_Set
     9 imports
    10   Isin2
    11   Cmp
    12 begin
    13 
    14 type_synonym 'a aa_tree = "('a,nat) tree"
    15 
    16 fun lvl :: "'a aa_tree \<Rightarrow> nat" where
    17 "lvl Leaf = 0" |
    18 "lvl (Node lv _ _ _) = lv"
    19 
    20 fun invar :: "'a aa_tree \<Rightarrow> bool" where
    21 "invar Leaf = True" |
    22 "invar (Node h l a r) =
    23  (invar l \<and> invar r \<and>
    24   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)))"
    25 
    26 fun skew :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    27 "skew (Node lva (Node lvb t1 b t2) a t3) =
    28   (if lva = lvb then Node lva t1 b (Node lva t2 a t3) else Node lva (Node lvb t1 b t2) a t3)" |
    29 "skew t = t"
    30 
    31 fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    32 "split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
    33    (if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
    34     then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
    35     else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
    36 "split t = t"
    37 
    38 hide_const (open) insert
    39 
    40 fun insert :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    41 "insert x Leaf = Node 1 Leaf x Leaf" |
    42 "insert x (Node lv t1 a t2) =
    43   (case cmp x a of
    44      LT \<Rightarrow> split (skew (Node lv (insert x t1) a t2)) |
    45      GT \<Rightarrow> split (skew (Node lv t1 a (insert x t2))) |
    46      EQ \<Rightarrow> Node lv t1 x t2)"
    47 
    48 (* wrong in paper! *)
    49 fun del_max :: "'a aa_tree \<Rightarrow> 'a aa_tree * 'a" where
    50 "del_max (Node lv l a Leaf) = (l,a)" |
    51 "del_max (Node lv l a r) = (let (r',b) = del_max r in (Node lv l a r', b))"
    52 
    53 fun sngl :: "'a aa_tree \<Rightarrow> bool" where
    54 "sngl Leaf = False" |
    55 "sngl (Node _ _ _ Leaf) = True" |
    56 "sngl (Node lva _ _ (Node lvb _ _ _)) = (lva > lvb)"
    57 
    58 definition adjust :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    59 "adjust t =
    60  (case t of
    61   Node lv l x r \<Rightarrow>
    62    (if lvl l >= lv-1 \<and> lvl r >= lv-1 then t else
    63     if lvl r < lv-1 \<and> sngl l then skew (Node (lv-1) l x r) else
    64     if lvl r < lv-1
    65     then case l of
    66            Node lva t1 a (Node lvb t2 b t3)
    67              \<Rightarrow> Node (lvb+1) (Node lva t1 a t2) b (Node (lv-1) t3 x r) |
    68            _ \<Rightarrow> t (* unreachable *)
    69     else
    70     if lvl r < lv then split (Node (lv-1) l x r)
    71     else
    72       case r of
    73         Leaf \<Rightarrow> Leaf (* unreachable *) |
    74         Node _ t1 b t4 \<Rightarrow>
    75           (case t1 of
    76              Node lva t2 a t3
    77                \<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
    78                     (split (Node (if sngl t1 then lva-1 else lva) t3 b t4))
    79            | _ \<Rightarrow> t (* unreachable *))))"
    80 
    81 fun delete :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    82 "delete _ Leaf = Leaf" |
    83 "delete x (Node lv l a r) =
    84   (case cmp x a of
    85      LT \<Rightarrow> adjust (Node lv (delete x l) a r) |
    86      GT \<Rightarrow> adjust (Node lv l a (delete x r)) |
    87      EQ \<Rightarrow> (if l = Leaf then r
    88             else let (l',b) = del_max l in adjust (Node lv l' b r)))"
    89 
    90 
    91 subsection "Functional Correctness"
    92 
    93 subsubsection "Proofs for insert"
    94 
    95 lemma inorder_split: "inorder(split t) = inorder t"
    96 by(cases t rule: split.cases) (auto)
    97 
    98 lemma inorder_skew: "inorder(skew t) = inorder t"
    99 by(cases t rule: skew.cases) (auto)
   100 
   101 lemma inorder_insert:
   102   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
   103 by(induction t) (auto simp: ins_list_simps inorder_split inorder_skew)
   104 
   105 subsubsection "Proofs for delete"
   106 
   107 lemma del_maxD:
   108   "\<lbrakk> del_max t = (t',x); t \<noteq> Leaf; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   109    inorder t' @ [x] = inorder t"
   110 by(induction t arbitrary: t' rule: del_max.induct)
   111   (auto simp: sorted_lems split: prod.splits)
   112 
   113 lemma inorder_adjust: "t \<noteq> Leaf \<Longrightarrow> inorder(adjust t) = inorder t"
   114 by(induction t)
   115   (auto simp: adjust_def inorder_skew inorder_split split: tree.splits)
   116 
   117 lemma inorder_delete:
   118   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
   119 by(induction t)
   120   (auto simp: del_list_simps inorder_adjust del_maxD split: prod.splits)
   121 
   122 
   123 subsection "Overall correctness"
   124 
   125 interpretation Set_by_Ordered
   126 where empty = Leaf and isin = isin and insert = insert and delete = delete
   127 and inorder = inorder and inv = "\<lambda>_. True"
   128 proof (standard, goal_cases)
   129   case 1 show ?case by simp
   130 next
   131   case 2 thus ?case by(simp add: isin_set)
   132 next
   133   case 3 thus ?case by(simp add: inorder_insert)
   134 next
   135   case 4 thus ?case by(simp add: inorder_delete)
   136 qed auto
   137 
   138 end