src/HOL/Data_Structures/AA_Set.thy
 author nipkow Mon Jan 11 20:51:13 2016 +0100 (2016-01-11) changeset 62130 90a3016a6c12 parent 61793 4c9e1e5a240e child 62160 ff20b44b2fc8 permissions -rw-r--r--
```     1 (*
```
```     2 Author: Tobias Nipkow
```
```     3
```
```     4 Added trivial cases to function `adjust' to obviate invariants.
```
```     5 *)
```
```     6
```
```     7 section \<open>AA Tree Implementation of Sets\<close>
```
```     8
```
```     9 theory AA_Set
```
```    10 imports
```
```    11   Isin2
```
```    12   Cmp
```
```    13 begin
```
```    14
```
```    15 type_synonym 'a aa_tree = "('a,nat) tree"
```
```    16
```
```    17 fun lvl :: "'a aa_tree \<Rightarrow> nat" where
```
```    18 "lvl Leaf = 0" |
```
```    19 "lvl (Node lv _ _ _) = lv"
```
```    20 (*
```
```    21 fun invar :: "'a aa_tree \<Rightarrow> bool" where
```
```    22 "invar Leaf = True" |
```
```    23 "invar (Node h l a r) =
```
```    24  (invar l \<and> invar r \<and>
```
```    25   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)))"
```
```    26 *)
```
```    27 fun skew :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
```
```    28 "skew (Node lva (Node lvb t1 b t2) a t3) =
```
```    29   (if lva = lvb then Node lva t1 b (Node lva t2 a t3) else Node lva (Node lvb t1 b t2) a t3)" |
```
```    30 "skew t = t"
```
```    31
```
```    32 fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
```
```    33 "split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
```
```    34    (if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
```
```    35     then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
```
```    36     else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
```
```    37 "split t = t"
```
```    38
```
```    39 hide_const (open) insert
```
```    40
```
```    41 fun insert :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
```
```    42 "insert x Leaf = Node 1 Leaf x Leaf" |
```
```    43 "insert x (Node lv t1 a t2) =
```
```    44   (case cmp x a of
```
```    45      LT \<Rightarrow> split (skew (Node lv (insert x t1) a t2)) |
```
```    46      GT \<Rightarrow> split (skew (Node lv t1 a (insert x t2))) |
```
```    47      EQ \<Rightarrow> Node lv t1 x t2)"
```
```    48
```
```    49 (* wrong in paper! *)
```
```    50 fun del_max :: "'a aa_tree \<Rightarrow> 'a aa_tree * 'a" where
```
```    51 "del_max (Node lv l a Leaf) = (l,a)" |
```
```    52 "del_max (Node lv l a r) = (let (r',b) = del_max r in (Node lv l a r', b))"
```
```    53
```
```    54 fun sngl :: "'a aa_tree \<Rightarrow> bool" where
```
```    55 "sngl Leaf = False" |
```
```    56 "sngl (Node _ _ _ Leaf) = True" |
```
```    57 "sngl (Node lva _ _ (Node lvb _ _ _)) = (lva > lvb)"
```
```    58
```
```    59 definition adjust :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
```
```    60 "adjust t =
```
```    61  (case t of
```
```    62   Node lv l x r \<Rightarrow>
```
```    63    (if lvl l >= lv-1 \<and> lvl r >= lv-1 then t else
```
```    64     if lvl r < lv-1 \<and> sngl l then skew (Node (lv-1) l x r) else
```
```    65     if lvl r < lv-1
```
```    66     then case l of
```
```    67            Node lva t1 a (Node lvb t2 b t3)
```
```    68              \<Rightarrow> Node (lvb+1) (Node lva t1 a t2) b (Node (lv-1) t3 x r) |
```
```    69            _ \<Rightarrow> t (* unreachable *)
```
```    70     else
```
```    71     if lvl r < lv then split (Node (lv-1) l x r)
```
```    72     else
```
```    73       case r of
```
```    74         Leaf \<Rightarrow> Leaf (* unreachable *) |
```
```    75         Node _ t1 b t4 \<Rightarrow>
```
```    76           (case t1 of
```
```    77              Node lva t2 a t3
```
```    78                \<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
```
```    79                     (split (Node (if sngl t1 then lva-1 else lva) t3 b t4))
```
```    80            | _ \<Rightarrow> t (* unreachable *))))"
```
```    81
```
```    82 fun delete :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
```
```    83 "delete _ Leaf = Leaf" |
```
```    84 "delete x (Node lv l a r) =
```
```    85   (case cmp x a of
```
```    86      LT \<Rightarrow> adjust (Node lv (delete x l) a r) |
```
```    87      GT \<Rightarrow> adjust (Node lv l a (delete x r)) |
```
```    88      EQ \<Rightarrow> (if l = Leaf then r
```
```    89             else let (l',b) = del_max l in adjust (Node lv l' b r)))"
```
```    90
```
```    91
```
```    92 subsection "Functional Correctness"
```
```    93
```
```    94 subsubsection "Proofs for insert"
```
```    95
```
```    96 lemma inorder_split: "inorder(split t) = inorder t"
```
```    97 by(cases t rule: split.cases) (auto)
```
```    98
```
```    99 lemma inorder_skew: "inorder(skew t) = inorder t"
```
```   100 by(cases t rule: skew.cases) (auto)
```
```   101
```
```   102 lemma inorder_insert:
```
```   103   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
```
```   104 by(induction t) (auto simp: ins_list_simps inorder_split inorder_skew)
```
```   105
```
```   106 subsubsection "Proofs for delete"
```
```   107
```
```   108 lemma del_maxD:
```
```   109   "\<lbrakk> del_max t = (t',x); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> 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`