src/HOL/Data_Structures/Brother12_Set.thy
author nipkow
Thu Jul 07 18:08:02 2016 +0200 (2016-07-07)
changeset 63411 e051eea34990
parent 62526 347150095fd2
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow@63411
     1
(* Author: Tobias Nipkow, Daniel Stüwe *)
nipkow@61784
     2
nipkow@62130
     3
section \<open>1-2 Brother Tree Implementation of Sets\<close>
nipkow@61784
     4
nipkow@61784
     5
theory Brother12_Set
nipkow@61784
     6
imports
nipkow@61784
     7
  Cmp
nipkow@61784
     8
  Set_by_Ordered
nipkow@63411
     9
  "~~/src/HOL/Number_Theory/Fib"
nipkow@61784
    10
begin
nipkow@61784
    11
nipkow@61784
    12
subsection \<open>Data Type and Operations\<close>
nipkow@61784
    13
nipkow@61784
    14
datatype 'a bro =
nipkow@61784
    15
  N0 |
nipkow@61784
    16
  N1 "'a bro" |
nipkow@61784
    17
  N2 "'a bro" 'a "'a bro" |
nipkow@61784
    18
  (* auxiliary constructors: *)
nipkow@61784
    19
  L2 'a |
nipkow@61784
    20
  N3 "'a bro" 'a "'a bro" 'a "'a bro"
nipkow@61784
    21
nipkow@61784
    22
fun inorder :: "'a bro \<Rightarrow> 'a list" where
nipkow@61784
    23
"inorder N0 = []" |
nipkow@61784
    24
"inorder (N1 t) = inorder t" |
nipkow@61784
    25
"inorder (N2 l a r) = inorder l @ a # inorder r" |
nipkow@61784
    26
"inorder (L2 a) = [a]" |
nipkow@61784
    27
"inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
nipkow@61784
    28
nipkow@63411
    29
fun isin :: "'a bro \<Rightarrow> 'a::linorder \<Rightarrow> bool" where
nipkow@61784
    30
"isin N0 x = False" |
nipkow@61784
    31
"isin (N1 t) x = isin t x" |
nipkow@61784
    32
"isin (N2 l a r) x =
nipkow@61784
    33
  (case cmp x a of
nipkow@61784
    34
     LT \<Rightarrow> isin l x |
nipkow@61784
    35
     EQ \<Rightarrow> True |
nipkow@61784
    36
     GT \<Rightarrow> isin r x)"
nipkow@61784
    37
nipkow@61784
    38
fun n1 :: "'a bro \<Rightarrow> 'a bro" where
nipkow@61784
    39
"n1 (L2 a) = N2 N0 a N0" |
nipkow@61784
    40
"n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
nipkow@61784
    41
"n1 t = N1 t"
nipkow@61784
    42
nipkow@61784
    43
hide_const (open) insert
nipkow@61784
    44
nipkow@61784
    45
locale insert
nipkow@61784
    46
begin
nipkow@61784
    47
nipkow@61784
    48
fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
nipkow@61784
    49
"n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
nipkow@61784
    50
"n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
nipkow@61784
    51
"n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
nipkow@61784
    52
"n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
nipkow@61784
    53
"n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
nipkow@61784
    54
"n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
nipkow@61784
    55
"n2 t1 a t2 = N2 t1 a t2"
nipkow@61784
    56
nipkow@63411
    57
fun ins :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
nipkow@61789
    58
"ins x N0 = L2 x" |
nipkow@61789
    59
"ins x (N1 t) = n1 (ins x t)" |
nipkow@61789
    60
"ins x (N2 l a r) =
nipkow@61789
    61
  (case cmp x a of
nipkow@61789
    62
     LT \<Rightarrow> n2 (ins x l) a r |
nipkow@61789
    63
     EQ \<Rightarrow> N2 l a r |
nipkow@61789
    64
     GT \<Rightarrow> n2 l a (ins x r))"
nipkow@61784
    65
nipkow@61784
    66
fun tree :: "'a bro \<Rightarrow> 'a bro" where
nipkow@61784
    67
"tree (L2 a) = N2 N0 a N0" |
nipkow@61784
    68
"tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
nipkow@61784
    69
"tree t = t"
nipkow@61784
    70
nipkow@63411
    71
definition insert :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
nipkow@61784
    72
"insert x t = tree(ins x t)"
nipkow@61784
    73
nipkow@61784
    74
end
nipkow@61784
    75
nipkow@61784
    76
locale delete
nipkow@61784
    77
begin
nipkow@61784
    78
nipkow@61784
    79
fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
nipkow@61784
    80
"n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
nipkow@61784
    81
"n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
nipkow@61784
    82
  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
nipkow@61784
    83
"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
nipkow@61784
    84
  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
nipkow@61784
    85
"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
nipkow@61784
    86
  N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" |
nipkow@61784
    87
"n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
nipkow@61784
    88
  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
nipkow@61784
    89
"n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
nipkow@61784
    90
  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
nipkow@61784
    91
"n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
nipkow@61784
    92
  N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
nipkow@61784
    93
"n2 t1 a1 t2 = N2 t1 a1 t2"
nipkow@61784
    94
nipkow@61784
    95
fun del_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
nipkow@61784
    96
"del_min N0 = None" |
nipkow@61784
    97
"del_min (N1 t) =
nipkow@61784
    98
  (case del_min t of
nipkow@61784
    99
     None \<Rightarrow> None |
nipkow@61784
   100
     Some (a, t') \<Rightarrow> Some (a, N1 t'))" |
nipkow@61784
   101
"del_min (N2 t1 a t2) =
nipkow@61784
   102
  (case del_min t1 of
nipkow@61784
   103
     None \<Rightarrow> Some (a, N1 t2) |
nipkow@61784
   104
     Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
nipkow@61784
   105
nipkow@63411
   106
fun del :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
nipkow@61784
   107
"del _ N0         = N0" |
nipkow@61784
   108
"del x (N1 t)     = N1 (del x t)" |
nipkow@61784
   109
"del x (N2 l a r) =
nipkow@61784
   110
  (case cmp x a of
nipkow@61784
   111
     LT \<Rightarrow> n2 (del x l) a r |
nipkow@61784
   112
     GT \<Rightarrow> n2 l a (del x r) |
nipkow@61784
   113
     EQ \<Rightarrow> (case del_min r of
nipkow@61784
   114
              None \<Rightarrow> N1 l |
nipkow@61784
   115
              Some (b, r') \<Rightarrow> n2 l b r'))"
nipkow@61784
   116
nipkow@61784
   117
fun tree :: "'a bro \<Rightarrow> 'a bro" where
nipkow@61784
   118
"tree (N1 t) = t" |
nipkow@61784
   119
"tree t = t"
nipkow@61784
   120
nipkow@63411
   121
definition delete :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
nipkow@61784
   122
"delete a t = tree (del a t)"
nipkow@61784
   123
nipkow@61784
   124
end
nipkow@61784
   125
nipkow@61784
   126
subsection \<open>Invariants\<close>
nipkow@61784
   127
nipkow@61784
   128
fun B :: "nat \<Rightarrow> 'a bro set"
nipkow@61784
   129
and U :: "nat \<Rightarrow> 'a bro set" where
nipkow@61784
   130
"B 0 = {N0}" |
nipkow@61784
   131
"B (Suc h) = { N2 t1 a t2 | t1 a t2. 
nipkow@61784
   132
  t1 \<in> B h \<union> U h \<and> t2 \<in> B h \<or> t1 \<in> B h \<and> t2 \<in> B h \<union> U h}" |
nipkow@61784
   133
"U 0 = {}" |
nipkow@61784
   134
"U (Suc h) = N1 ` B h"
nipkow@61784
   135
nipkow@61784
   136
abbreviation "T h \<equiv> B h \<union> U h"
nipkow@61784
   137
nipkow@61784
   138
fun Bp :: "nat \<Rightarrow> 'a bro set" where
nipkow@61784
   139
"Bp 0 = B 0 \<union> L2 ` UNIV" |
nipkow@61784
   140
"Bp (Suc 0) = B (Suc 0) \<union> {N3 N0 a N0 b N0|a b. True}" |
nipkow@61784
   141
"Bp (Suc(Suc h)) = B (Suc(Suc h)) \<union>
nipkow@61784
   142
  {N3 t1 a t2 b t3 | t1 a t2 b t3. t1 \<in> B (Suc h) \<and> t2 \<in> U (Suc h) \<and> t3 \<in> B (Suc h)}"
nipkow@61784
   143
nipkow@61784
   144
fun Um :: "nat \<Rightarrow> 'a bro set" where
nipkow@61784
   145
"Um 0 = {}" |
nipkow@61784
   146
"Um (Suc h) = N1 ` T h"
nipkow@61784
   147
nipkow@61784
   148
nipkow@61784
   149
subsection "Functional Correctness Proofs"
nipkow@61784
   150
nipkow@61784
   151
subsubsection "Proofs for isin"
nipkow@61784
   152
nipkow@61784
   153
lemma
nipkow@61784
   154
  "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
nipkow@61784
   155
by(induction h arbitrary: t) (fastforce simp: elems_simps1 split: if_splits)+
nipkow@61784
   156
nipkow@61784
   157
lemma isin_set: "t \<in> T h \<Longrightarrow>
nipkow@61784
   158
  sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
nipkow@61784
   159
by(induction h arbitrary: t) (auto simp: elems_simps2 split: if_splits)
nipkow@61784
   160
nipkow@61784
   161
subsubsection "Proofs for insertion"
nipkow@61784
   162
nipkow@61784
   163
lemma inorder_n1: "inorder(n1 t) = inorder t"
nipkow@62526
   164
by(cases t rule: n1.cases) (auto simp: sorted_lems)
nipkow@61784
   165
nipkow@61784
   166
context insert
nipkow@61784
   167
begin
nipkow@61784
   168
nipkow@61784
   169
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
nipkow@61784
   170
by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)
nipkow@61784
   171
nipkow@61784
   172
lemma inorder_tree: "inorder(tree t) = inorder t"
nipkow@61784
   173
by(cases t) auto
nipkow@61784
   174
nipkow@61784
   175
lemma inorder_ins: "t \<in> T h \<Longrightarrow>
nipkow@61784
   176
  sorted(inorder t) \<Longrightarrow> inorder(ins a t) = ins_list a (inorder t)"
nipkow@61784
   177
by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)
nipkow@61784
   178
nipkow@61784
   179
lemma inorder_insert: "t \<in> T h \<Longrightarrow>
nipkow@61784
   180
  sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
nipkow@61784
   181
by(simp add: insert_def inorder_ins inorder_tree)
nipkow@61784
   182
nipkow@61784
   183
end
nipkow@61784
   184
nipkow@61784
   185
subsubsection \<open>Proofs for deletion\<close>
nipkow@61784
   186
nipkow@61784
   187
context delete
nipkow@61784
   188
begin
nipkow@61784
   189
nipkow@61784
   190
lemma inorder_tree: "inorder(tree t) = inorder t"
nipkow@61784
   191
by(cases t) auto
nipkow@61784
   192
nipkow@61784
   193
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
nipkow@62526
   194
by(cases "(l,a,r)" rule: n2.cases) (auto)
nipkow@61784
   195
nipkow@61784
   196
lemma inorder_del_min:
nipkow@61792
   197
  "t \<in> T h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
nipkow@61784
   198
  (del_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
nipkow@61784
   199
by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
nipkow@61784
   200
nipkow@61784
   201
lemma inorder_del:
nipkow@61792
   202
  "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
nipkow@61792
   203
by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
nipkow@61792
   204
     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
nipkow@61792
   205
nipkow@61792
   206
lemma inorder_delete:
nipkow@61792
   207
  "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
nipkow@61792
   208
by(simp add: delete_def inorder_del inorder_tree)
nipkow@61784
   209
nipkow@61784
   210
end
nipkow@61784
   211
nipkow@61784
   212
nipkow@61784
   213
subsection \<open>Invariant Proofs\<close>
nipkow@61784
   214
nipkow@61789
   215
subsubsection \<open>Proofs for insertion\<close>
nipkow@61784
   216
nipkow@61784
   217
lemma n1_type: "t \<in> Bp h \<Longrightarrow> n1 t \<in> T (Suc h)"
nipkow@61784
   218
by(cases h rule: Bp.cases) auto
nipkow@61784
   219
nipkow@61784
   220
context insert
nipkow@61784
   221
begin
nipkow@61784
   222
nipkow@61809
   223
lemma tree_type: "t \<in> Bp h \<Longrightarrow> tree t \<in> B h \<union> B (Suc h)"
nipkow@61784
   224
by(cases h rule: Bp.cases) auto
nipkow@61784
   225
nipkow@61784
   226
lemma n2_type:
nipkow@61784
   227
  "(t1 \<in> Bp h \<and> t2 \<in> T h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h)) \<and>
nipkow@61784
   228
   (t1 \<in> T h \<and> t2 \<in> Bp h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h))"
nipkow@61784
   229
apply(cases h rule: Bp.cases)
nipkow@61784
   230
apply (auto)[2]
nipkow@61784
   231
apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
nipkow@61784
   232
done
nipkow@61784
   233
nipkow@61784
   234
lemma Bp_if_B: "t \<in> B h \<Longrightarrow> t \<in> Bp h"
nipkow@61784
   235
by (cases h rule: Bp.cases) simp_all
nipkow@61784
   236
nipkow@61784
   237
text{* An automatic proof: *}
nipkow@61784
   238
nipkow@61784
   239
lemma
nipkow@61784
   240
  "(t \<in> B h \<longrightarrow> ins x t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> ins x t \<in> T h)"
nipkow@61784
   241
apply(induction h arbitrary: t)
nipkow@61784
   242
 apply (simp)
nipkow@61784
   243
apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
nipkow@61784
   244
done
nipkow@61784
   245
nipkow@61784
   246
text{* A detailed proof: *}
nipkow@61784
   247
nipkow@61784
   248
lemma ins_type:
nipkow@61784
   249
shows "t \<in> B h \<Longrightarrow> ins x t \<in> Bp h" and "t \<in> U h \<Longrightarrow> ins x t \<in> T h"
nipkow@61784
   250
proof(induction h arbitrary: t)
nipkow@61784
   251
  case 0
nipkow@61784
   252
  { case 1 thus ?case by simp
nipkow@61784
   253
  next
nipkow@61784
   254
    case 2 thus ?case by simp }
nipkow@61784
   255
next
nipkow@61784
   256
  case (Suc h)
nipkow@61784
   257
  { case 1
nipkow@61784
   258
    then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
nipkow@61784
   259
      t1: "t1 \<in> T h" and t2: "t2 \<in> T h" and t12: "t1 \<in> B h \<or> t2 \<in> B h"
nipkow@61784
   260
      by auto
nipkow@61784
   261
    { assume "x < a"
nipkow@61784
   262
      hence "?case \<longleftrightarrow> n2 (ins x t1) a t2 \<in> Bp (Suc h)" by simp
nipkow@61784
   263
      also have "\<dots>"
nipkow@61784
   264
      proof cases
nipkow@61784
   265
        assume "t1 \<in> B h"
nipkow@61784
   266
        with t2 show ?thesis by (simp add: Suc.IH(1) n2_type)
nipkow@61784
   267
      next
nipkow@61784
   268
        assume "t1 \<notin> B h"
nipkow@61784
   269
        hence 1: "t1 \<in> U h" and 2: "t2 \<in> B h" using t1 t12 by auto
nipkow@61784
   270
        show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type)
nipkow@61784
   271
      qed
nipkow@61784
   272
      finally have ?case .
nipkow@61784
   273
    }
nipkow@61784
   274
    moreover
nipkow@61784
   275
    { assume "a < x"
nipkow@61784
   276
      hence "?case \<longleftrightarrow> n2 t1 a (ins x t2) \<in> Bp (Suc h)" by simp
nipkow@61784
   277
      also have "\<dots>"
nipkow@61784
   278
      proof cases
nipkow@61784
   279
        assume "t2 \<in> B h"
nipkow@61784
   280
        with t1 show ?thesis by (simp add: Suc.IH(1) n2_type)
nipkow@61784
   281
      next
nipkow@61784
   282
        assume "t2 \<notin> B h"
nipkow@61784
   283
        hence 1: "t1 \<in> B h" and 2: "t2 \<in> U h" using t2 t12 by auto
nipkow@61784
   284
        show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type)
nipkow@61784
   285
      qed
nipkow@61784
   286
    }
nipkow@61784
   287
    moreover 
nipkow@61784
   288
    { assume "x = a"
nipkow@61784
   289
      from 1 have "t \<in> Bp (Suc h)" by(rule Bp_if_B)
nipkow@61784
   290
      hence "?case" using `x = a` by simp
nipkow@61784
   291
    }
nipkow@61784
   292
    ultimately show ?case by auto
nipkow@61784
   293
  next
nipkow@61784
   294
    case 2 thus ?case using Suc(1) n1_type by fastforce }
nipkow@61784
   295
qed
nipkow@61784
   296
nipkow@61784
   297
lemma insert_type:
nipkow@61809
   298
  "t \<in> B h \<Longrightarrow> insert x t \<in> B h \<union> B (Suc h)"
nipkow@61809
   299
unfolding insert_def by (metis ins_type(1) tree_type)
nipkow@61784
   300
nipkow@61784
   301
end
nipkow@61784
   302
nipkow@61789
   303
subsubsection "Proofs for deletion"
nipkow@61784
   304
nipkow@61784
   305
lemma B_simps[simp]: 
nipkow@61784
   306
  "N1 t \<in> B h = False"
nipkow@61784
   307
  "L2 y \<in> B h = False"
nipkow@61784
   308
  "(N3 t1 a1 t2 a2 t3) \<in> B h = False"
nipkow@61784
   309
  "N0 \<in> B h \<longleftrightarrow> h = 0"
nipkow@61784
   310
by (cases h, auto)+
nipkow@61784
   311
nipkow@61784
   312
context delete
nipkow@61784
   313
begin
nipkow@61784
   314
nipkow@61784
   315
lemma n2_type1:
nipkow@61784
   316
  "\<lbrakk>t1 \<in> Um h; t2 \<in> B h\<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
nipkow@61784
   317
apply(cases h rule: Bp.cases)
nipkow@61784
   318
apply auto[2]
nipkow@61784
   319
apply(erule exE bexE conjE imageE | simp | erule disjE)+
nipkow@61784
   320
done
nipkow@61784
   321
nipkow@61784
   322
lemma n2_type2:
nipkow@61784
   323
  "\<lbrakk>t1 \<in> B h ; t2 \<in> Um h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
nipkow@61784
   324
apply(cases h rule: Bp.cases)
nipkow@61784
   325
apply auto[2]
nipkow@61784
   326
apply(erule exE bexE conjE imageE | simp | erule disjE)+
nipkow@61784
   327
done
nipkow@61784
   328
nipkow@61784
   329
lemma n2_type3:
nipkow@61784
   330
  "\<lbrakk>t1 \<in> T h ; t2 \<in> T h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
nipkow@61784
   331
apply(cases h rule: Bp.cases)
nipkow@61784
   332
apply auto[2]
nipkow@61784
   333
apply(erule exE bexE conjE imageE | simp | erule disjE)+
nipkow@61784
   334
done
nipkow@61784
   335
nipkow@61784
   336
lemma del_minNoneN0: "\<lbrakk>t \<in> B h; del_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
nipkow@61784
   337
by (cases t) (auto split: option.splits)
nipkow@61784
   338
nipkow@61784
   339
lemma del_minNoneN1 : "\<lbrakk>t \<in> U h; del_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
nipkow@61784
   340
by (cases h) (auto simp: del_minNoneN0  split: option.splits)
nipkow@61784
   341
nipkow@61784
   342
lemma del_min_type:
nipkow@61784
   343
  "t \<in> B h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
nipkow@61784
   344
  "t \<in> U h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
nipkow@61784
   345
proof (induction h arbitrary: t a t')
nipkow@61784
   346
  case (Suc h)
nipkow@61784
   347
  { case 1
nipkow@61784
   348
    then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
nipkow@61784
   349
      t12: "t1 \<in> T h" "t2 \<in> T h" "t1 \<in> B h \<or> t2 \<in> B h"
nipkow@61784
   350
      by auto
nipkow@61784
   351
    show ?case
nipkow@61784
   352
    proof (cases "del_min t1")
nipkow@61784
   353
      case None
nipkow@61784
   354
      show ?thesis
nipkow@61784
   355
      proof cases
nipkow@61784
   356
        assume "t1 \<in> B h"
nipkow@61784
   357
        with del_minNoneN0[OF this None] 1 show ?thesis by(auto)
nipkow@61784
   358
      next
nipkow@61784
   359
        assume "t1 \<notin> B h"
nipkow@61784
   360
        thus ?thesis using 1 None by (auto)
nipkow@61784
   361
      qed
nipkow@61784
   362
    next
nipkow@61784
   363
      case [simp]: (Some bt')
nipkow@61784
   364
      obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
nipkow@61784
   365
      show ?thesis
nipkow@61784
   366
      proof cases
nipkow@61784
   367
        assume "t1 \<in> B h"
nipkow@61784
   368
        from Suc.IH(1)[OF this] 1 have "t1' \<in> T h" by simp
nipkow@61784
   369
        from n2_type3[OF this t12(2)] 1 show ?thesis by auto
nipkow@61784
   370
      next
nipkow@61784
   371
        assume "t1 \<notin> B h"
nipkow@61784
   372
        hence t1: "t1 \<in> U h" and t2: "t2 \<in> B h" using t12 by auto
nipkow@61784
   373
        from Suc.IH(2)[OF t1] have "t1' \<in> Um h" by simp
nipkow@61784
   374
        from n2_type1[OF this t2] 1 show ?thesis by auto
nipkow@61784
   375
      qed
nipkow@61784
   376
    qed
nipkow@61784
   377
  }
nipkow@61784
   378
  { case 2
nipkow@61784
   379
    then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \<in> B h" by auto
nipkow@61784
   380
    show ?case
nipkow@61784
   381
    proof (cases "del_min t1")
nipkow@61784
   382
      case None
nipkow@61784
   383
      with del_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
nipkow@61784
   384
    next
nipkow@61784
   385
      case [simp]: (Some bt')
nipkow@61784
   386
      obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
nipkow@61784
   387
      from Suc.IH(1)[OF t1] have "t1' \<in> T h" by simp
nipkow@61784
   388
      thus ?thesis using 2 by auto
nipkow@61784
   389
    qed
nipkow@61784
   390
  }
nipkow@61784
   391
qed auto
nipkow@61784
   392
nipkow@61784
   393
lemma del_type:
nipkow@61784
   394
  "t \<in> B h \<Longrightarrow> del x t \<in> T h"
nipkow@61784
   395
  "t \<in> U h \<Longrightarrow> del x t \<in> Um h"
nipkow@61784
   396
proof (induction h arbitrary: x t)
nipkow@61784
   397
  case (Suc h)
nipkow@61784
   398
  { case 1
nipkow@61784
   399
    then obtain l a r where [simp]: "t = N2 l a r" and
nipkow@61784
   400
      lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
nipkow@61784
   401
    { assume "x < a"
nipkow@61784
   402
      have ?case
nipkow@61784
   403
      proof cases
nipkow@61784
   404
        assume "l \<in> B h"
nipkow@61784
   405
        from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
nipkow@61784
   406
        show ?thesis using `x<a` by(simp)
nipkow@61784
   407
      next
nipkow@61784
   408
        assume "l \<notin> B h"
nipkow@61784
   409
        hence "l \<in> U h" "r \<in> B h" using lr by auto
nipkow@61784
   410
        from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
nipkow@61784
   411
        show ?thesis using `x<a` by(simp)
nipkow@61784
   412
      qed
nipkow@61784
   413
    } moreover
nipkow@61784
   414
    { assume "x > a"
nipkow@61784
   415
      have ?case
nipkow@61784
   416
      proof cases
nipkow@61784
   417
        assume "r \<in> B h"
nipkow@61784
   418
        from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
nipkow@61784
   419
        show ?thesis using `x>a` by(simp)
nipkow@61784
   420
      next
nipkow@61784
   421
        assume "r \<notin> B h"
nipkow@61784
   422
        hence "l \<in> B h" "r \<in> U h" using lr by auto
nipkow@61784
   423
        from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
nipkow@61784
   424
        show ?thesis using `x>a` by(simp)
nipkow@61784
   425
      qed
nipkow@61784
   426
    } moreover
nipkow@61784
   427
    { assume [simp]: "x=a"
nipkow@61784
   428
      have ?case
nipkow@61784
   429
      proof (cases "del_min r")
nipkow@61784
   430
        case None
nipkow@61784
   431
        show ?thesis
nipkow@61784
   432
        proof cases
nipkow@61784
   433
          assume "r \<in> B h"
nipkow@61784
   434
          with del_minNoneN0[OF this None] lr show ?thesis by(simp)
nipkow@61784
   435
        next
nipkow@61784
   436
          assume "r \<notin> B h"
nipkow@61784
   437
          hence "r \<in> U h" using lr by auto
nipkow@61784
   438
          with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
nipkow@61784
   439
        qed
nipkow@61784
   440
      next
nipkow@61784
   441
        case [simp]: (Some br')
nipkow@61784
   442
        obtain b r' where [simp]: "br' = (b,r')" by fastforce
nipkow@61784
   443
        show ?thesis
nipkow@61784
   444
        proof cases
nipkow@61784
   445
          assume "r \<in> B h"
nipkow@61784
   446
          from del_min_type(1)[OF this] n2_type3[OF lr(1)]
nipkow@61784
   447
          show ?thesis by simp
nipkow@61784
   448
        next
nipkow@61784
   449
          assume "r \<notin> B h"
nipkow@61784
   450
          hence "l \<in> B h" and "r \<in> U h" using lr by auto
nipkow@61784
   451
          from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
nipkow@61784
   452
          show ?thesis by simp
nipkow@61784
   453
        qed
nipkow@61784
   454
      qed
nipkow@61784
   455
    } ultimately show ?case by auto
nipkow@61784
   456
  }
nipkow@61784
   457
  { case 2 with Suc.IH(1) show ?case by auto }
nipkow@61784
   458
qed auto
nipkow@61784
   459
nipkow@61809
   460
lemma tree_type: "t \<in> T (h+1) \<Longrightarrow> tree t : B (h+1) \<union> B h"
nipkow@61784
   461
by(auto)
nipkow@61784
   462
nipkow@61809
   463
lemma delete_type: "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"
nipkow@61784
   464
unfolding delete_def
nipkow@61809
   465
by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
nipkow@61784
   466
nipkow@61784
   467
end
nipkow@61784
   468
nipkow@61789
   469
nipkow@61784
   470
subsection "Overall correctness"
nipkow@61784
   471
nipkow@61784
   472
interpretation Set_by_Ordered
nipkow@61789
   473
where empty = N0 and isin = isin and insert = insert.insert
nipkow@61809
   474
and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
nipkow@61784
   475
proof (standard, goal_cases)
nipkow@61784
   476
  case 2 thus ?case by(auto intro!: isin_set)
nipkow@61784
   477
next
nipkow@61784
   478
  case 3 thus ?case by(auto intro!: insert.inorder_insert)
nipkow@61784
   479
next
nipkow@61792
   480
  case 4 thus ?case by(auto intro!: delete.inorder_delete)
nipkow@61784
   481
next
nipkow@61784
   482
  case 6 thus ?case using insert.insert_type by blast
nipkow@61784
   483
next
nipkow@61784
   484
  case 7 thus ?case using delete.delete_type by blast
nipkow@61784
   485
qed auto
nipkow@61784
   486
nipkow@63411
   487
nipkow@63411
   488
subsection \<open>Height-Size Relation\<close>
nipkow@63411
   489
nipkow@63411
   490
text \<open>By Daniel St\"uwe\<close>
nipkow@63411
   491
nipkow@63411
   492
fun fib_tree :: "nat \<Rightarrow> unit bro" where
nipkow@63411
   493
  "fib_tree 0 = N0" 
nipkow@63411
   494
| "fib_tree (Suc 0) = N2 N0 () N0"
nipkow@63411
   495
| "fib_tree (Suc(Suc h)) = N2 (fib_tree (h+1)) () (N1 (fib_tree h))"
nipkow@63411
   496
nipkow@63411
   497
fun fib' :: "nat \<Rightarrow> nat" where
nipkow@63411
   498
  "fib' 0 = 0" 
nipkow@63411
   499
| "fib' (Suc 0) = 1"
nipkow@63411
   500
| "fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h"
nipkow@63411
   501
nipkow@63411
   502
fun size :: "'a bro \<Rightarrow> nat" where
nipkow@63411
   503
  "size N0 = 0" 
nipkow@63411
   504
| "size (N1 t) = size t"
nipkow@63411
   505
| "size (N2 t1 _ t2) = 1 + size t1 + size t2"
nipkow@63411
   506
nipkow@63411
   507
lemma fib_tree_B: "fib_tree h \<in> B h"
nipkow@63411
   508
by (induction h rule: fib_tree.induct) auto
nipkow@63411
   509
nipkow@63411
   510
declare [[names_short]]
nipkow@63411
   511
nipkow@63411
   512
lemma size_fib': "size (fib_tree h) = fib' h"
nipkow@63411
   513
by (induction h rule: fib_tree.induct) auto
nipkow@63411
   514
nipkow@63411
   515
lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))"
nipkow@63411
   516
by (induction h rule: fib_tree.induct) auto
nipkow@63411
   517
nipkow@63411
   518
lemma B_N2_cases[consumes 1]:
nipkow@63411
   519
assumes "N2 t1 a t2 \<in> B (Suc n)"
nipkow@63411
   520
obtains 
nipkow@63411
   521
  (BB) "t1 \<in> B n" and "t2 \<in> B n" |
nipkow@63411
   522
  (UB) "t1 \<in> U n" and "t2 \<in> B n" |
nipkow@63411
   523
  (BU) "t1 \<in> B n" and "t2 \<in> U n"
nipkow@63411
   524
using assms by auto
nipkow@63411
   525
nipkow@63411
   526
lemma size_bounded: "t \<in> B h \<Longrightarrow> size t \<ge> size (fib_tree h)"
nipkow@63411
   527
unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct)
nipkow@63411
   528
case (3 h t')
nipkow@63411
   529
  note main = 3
nipkow@63411
   530
  then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto
nipkow@63411
   531
  with main have "N2 t1 a t2 \<in> B (Suc (Suc h))" by auto
nipkow@63411
   532
  thus ?case proof (cases rule: B_N2_cases)
nipkow@63411
   533
    case BB
nipkow@63411
   534
    then obtain x y z where t2: "t2 = N2 x y z \<or> t2 = N2 z y x" "x \<in> B h" by auto
nipkow@63411
   535
    show ?thesis unfolding t' using main(1)[OF BB(1)] main(2)[OF t2(2)] t2(1) by auto
nipkow@63411
   536
  next
nipkow@63411
   537
    case UB
nipkow@63411
   538
    then obtain t11 where t1: "t1 = N1 t11" "t11 \<in> B h" by auto
nipkow@63411
   539
    show ?thesis unfolding t' t1(1) using main(2)[OF t1(2)] main(1)[OF UB(2)] by simp
nipkow@63411
   540
  next
nipkow@63411
   541
    case BU
nipkow@63411
   542
    then obtain t22 where t2: "t2 = N1 t22" "t22 \<in> B h" by auto
nipkow@63411
   543
    show ?thesis unfolding t' t2(1) using main(2)[OF t2(2)] main(1)[OF BU(1)] by simp
nipkow@63411
   544
  qed
nipkow@63411
   545
qed auto
nipkow@63411
   546
nipkow@63411
   547
theorem "t \<in> B h \<Longrightarrow> fib (h + 2) \<le> size t + 1"
nipkow@63411
   548
using size_bounded
nipkow@63411
   549
by (simp add: size_fib' fibfib[symmetric] del: fib.simps)
nipkow@63411
   550
nipkow@61784
   551
end