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