added AA trees
authornipkow
Sun Dec 06 17:27:42 2015 +0100 (2015-12-06)
changeset 617934c9e1e5a240e
parent 61792 8dd150a50acc
child 61794 4c232a2ddeab
added AA trees
src/HOL/Data_Structures/AA_Set.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Sun Dec 06 17:27:42 2015 +0100
     1.3 @@ -0,0 +1,138 @@
     1.4 +(*
     1.5 +Author: Tobias Nipkow
     1.6 +Invariants are under development
     1.7 +*)
     1.8 +
     1.9 +section \<open>An AA Tree Implementation of Sets\<close>
    1.10 +
    1.11 +theory AA_Set
    1.12 +imports
    1.13 +  Isin2
    1.14 +  Cmp
    1.15 +begin
    1.16 +
    1.17 +type_synonym 'a aa_tree = "('a,nat) tree"
    1.18 +
    1.19 +fun lvl :: "'a aa_tree \<Rightarrow> nat" where
    1.20 +"lvl Leaf = 0" |
    1.21 +"lvl (Node lv _ _ _) = lv"
    1.22 +
    1.23 +fun invar :: "'a aa_tree \<Rightarrow> bool" where
    1.24 +"invar Leaf = True" |
    1.25 +"invar (Node h l a r) =
    1.26 + (invar l \<and> invar r \<and>
    1.27 +  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.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 +"skew t = t"
    1.33 +
    1.34 +fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.35 +"split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
    1.36 +   (if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
    1.37 +    then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
    1.38 +    else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
    1.39 +"split t = t"
    1.40 +
    1.41 +hide_const (open) insert
    1.42 +
    1.43 +fun insert :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.44 +"insert x Leaf = Node 1 Leaf x Leaf" |
    1.45 +"insert x (Node lv t1 a t2) =
    1.46 +  (case cmp x a of
    1.47 +     LT \<Rightarrow> split (skew (Node lv (insert x t1) a t2)) |
    1.48 +     GT \<Rightarrow> split (skew (Node lv t1 a (insert x t2))) |
    1.49 +     EQ \<Rightarrow> Node lv t1 x t2)"
    1.50 +
    1.51 +(* wrong in paper! *)
    1.52 +fun del_max :: "'a aa_tree \<Rightarrow> 'a aa_tree * 'a" where
    1.53 +"del_max (Node lv l a Leaf) = (l,a)" |
    1.54 +"del_max (Node lv l a r) = (let (r',b) = del_max r in (Node lv l a r', b))"
    1.55 +
    1.56 +fun sngl :: "'a aa_tree \<Rightarrow> bool" where
    1.57 +"sngl Leaf = False" |
    1.58 +"sngl (Node _ _ _ Leaf) = True" |
    1.59 +"sngl (Node lva _ _ (Node lvb _ _ _)) = (lva > lvb)"
    1.60 +
    1.61 +definition adjust :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.62 +"adjust t =
    1.63 + (case t of
    1.64 +  Node lv l x r \<Rightarrow>
    1.65 +   (if lvl l >= lv-1 \<and> lvl r >= lv-1 then t else
    1.66 +    if lvl r < lv-1 \<and> sngl l then skew (Node (lv-1) l x r) else
    1.67 +    if lvl r < lv-1
    1.68 +    then case l of
    1.69 +           Node lva t1 a (Node lvb t2 b t3)
    1.70 +             \<Rightarrow> Node (lvb+1) (Node lva t1 a t2) b (Node (lv-1) t3 x r) |
    1.71 +           _ \<Rightarrow> t (* unreachable *)
    1.72 +    else
    1.73 +    if lvl r < lv then split (Node (lv-1) l x r)
    1.74 +    else
    1.75 +      case r of
    1.76 +        Leaf \<Rightarrow> Leaf (* unreachable *) |
    1.77 +        Node _ t1 b t4 \<Rightarrow>
    1.78 +          (case t1 of
    1.79 +             Node lva t2 a t3
    1.80 +               \<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
    1.81 +                    (split (Node (if sngl t1 then lva-1 else lva) t3 b t4))
    1.82 +           | _ \<Rightarrow> t (* unreachable *))))"
    1.83 +
    1.84 +fun delete :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.85 +"delete _ Leaf = Leaf" |
    1.86 +"delete x (Node lv l a r) =
    1.87 +  (case cmp x a of
    1.88 +     LT \<Rightarrow> adjust (Node lv (delete x l) a r) |
    1.89 +     GT \<Rightarrow> adjust (Node lv l a (delete x r)) |
    1.90 +     EQ \<Rightarrow> (if l = Leaf then r
    1.91 +            else let (l',b) = del_max l in adjust (Node lv l' b r)))"
    1.92 +
    1.93 +
    1.94 +subsection "Functional Correctness"
    1.95 +
    1.96 +subsubsection "Proofs for insert"
    1.97 +
    1.98 +lemma inorder_split: "inorder(split t) = inorder t"
    1.99 +by(cases t rule: split.cases) (auto)
   1.100 +
   1.101 +lemma inorder_skew: "inorder(skew t) = inorder t"
   1.102 +by(cases t rule: skew.cases) (auto)
   1.103 +
   1.104 +lemma inorder_insert:
   1.105 +  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
   1.106 +by(induction t) (auto simp: ins_list_simps inorder_split inorder_skew)
   1.107 +
   1.108 +subsubsection "Proofs for delete"
   1.109 +
   1.110 +lemma del_maxD:
   1.111 +  "\<lbrakk> del_max t = (t',x); t \<noteq> Leaf; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   1.112 +   inorder t' @ [x] = inorder t"
   1.113 +by(induction t arbitrary: t' rule: del_max.induct)
   1.114 +  (auto simp: sorted_lems split: prod.splits)
   1.115 +
   1.116 +lemma inorder_adjust: "t \<noteq> Leaf \<Longrightarrow> inorder(adjust t) = inorder t"
   1.117 +by(induction t)
   1.118 +  (auto simp: adjust_def inorder_skew inorder_split split: tree.splits)
   1.119 +
   1.120 +lemma inorder_delete:
   1.121 +  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
   1.122 +by(induction t)
   1.123 +  (auto simp: del_list_simps inorder_adjust del_maxD split: prod.splits)
   1.124 +
   1.125 +
   1.126 +subsection "Overall correctness"
   1.127 +
   1.128 +interpretation Set_by_Ordered
   1.129 +where empty = Leaf and isin = isin and insert = insert and delete = delete
   1.130 +and inorder = inorder and inv = "\<lambda>_. True"
   1.131 +proof (standard, goal_cases)
   1.132 +  case 1 show ?case by simp
   1.133 +next
   1.134 +  case 2 thus ?case by(simp add: isin_set)
   1.135 +next
   1.136 +  case 3 thus ?case by(simp add: inorder_insert)
   1.137 +next
   1.138 +  case 4 thus ?case by(simp add: inorder_delete)
   1.139 +qed auto
   1.140 +
   1.141 +end
   1.142 \ No newline at end of file
     2.1 --- a/src/HOL/ROOT	Sun Dec 06 11:26:38 2015 +0100
     2.2 +++ b/src/HOL/ROOT	Sun Dec 06 17:27:42 2015 +0100
     2.3 @@ -179,6 +179,7 @@
     2.4      Tree23_Map
     2.5      Tree234_Map
     2.6      Brother12_Map
     2.7 +    AA_Set
     2.8      Splay_Map
     2.9    document_files "root.tex" "root.bib"
    2.10