src/HOL/Data_Structures/Binomial_Heap.thy
author blanchet
Fri, 06 Nov 2020 12:48:31 +0100
changeset 72550 1d0ae7e578a0
parent 70607 b044a06ad0d6
child 72551 729d45c7ff33
permissions -rw-r--r--
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66522
nipkow
parents: 66491
diff changeset
     1
(* Author: Peter Lammich
nipkow
parents: 66491
diff changeset
     2
           Tobias Nipkow (tuning)
nipkow
parents: 66491
diff changeset
     3
*)
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     4
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     5
section \<open>Binomial Heap\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     6
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     7
theory Binomial_Heap
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     8
imports
70450
7c2724cefcb8 reduced dependencies
nipkow
parents: 69597
diff changeset
     9
  "HOL-Library.Pattern_Aliases"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    10
  Complex_Main
68492
c7e0a7bcacaf added lemmas; uniform names
nipkow
parents: 68109
diff changeset
    11
  Priority_Queue_Specs
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    12
begin
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    13
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    14
text \<open>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    15
  We formalize the binomial heap presentation from Okasaki's book.
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    16
  We show the functional correctness and complexity of all operations.
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    17
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    18
  The presentation is engineered for simplicity, and most
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    19
  proofs are straightforward and automatic.
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    20
\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    21
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    22
subsection \<open>Binomial Tree and Heap Datatype\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    23
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    24
datatype 'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    25
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    26
type_synonym 'a heap = "'a tree list"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    27
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    28
subsubsection \<open>Multiset of elements\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    29
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    30
fun mset_tree :: "'a::linorder tree \<Rightarrow> 'a multiset" where
70607
nipkow
parents: 70450
diff changeset
    31
  "mset_tree (Node _ a ts) = {#a#} + (\<Sum>t\<in>#mset ts. mset_tree t)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    32
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    33
definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where
70607
nipkow
parents: 70450
diff changeset
    34
  "mset_heap ts = (\<Sum>t\<in>#mset ts. mset_tree t)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    35
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    36
lemma mset_tree_simp_alt[simp]:
70607
nipkow
parents: 70450
diff changeset
    37
  "mset_tree (Node r a ts) = {#a#} + mset_heap ts"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    38
  unfolding mset_heap_def by auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    39
declare mset_tree.simps[simp del]
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    40
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    41
lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}"
66522
nipkow
parents: 66491
diff changeset
    42
by (cases t) auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    43
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    44
lemma mset_heap_Nil[simp]:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    45
  "mset_heap [] = {#}"
66522
nipkow
parents: 66491
diff changeset
    46
by (auto simp: mset_heap_def)
nipkow
parents: 66491
diff changeset
    47
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    48
lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts"
66522
nipkow
parents: 66491
diff changeset
    49
by (auto simp: mset_heap_def)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    50
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    51
lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]"
66522
nipkow
parents: 66491
diff changeset
    52
by (auto simp: mset_heap_def)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    53
66522
nipkow
parents: 66491
diff changeset
    54
lemma root_in_mset[simp]: "root t \<in># mset_tree t"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    55
by (cases t) auto
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    56
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    57
lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts"
66522
nipkow
parents: 66491
diff changeset
    58
by (auto simp: mset_heap_def)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    59
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    60
subsubsection \<open>Invariants\<close>
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    61
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    62
text \<open>Binomial invariant\<close>
66522
nipkow
parents: 66491
diff changeset
    63
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    64
"invar_btree (Node r x ts) \<longleftrightarrow>
66522
nipkow
parents: 66491
diff changeset
    65
   (\<forall>t\<in>set ts. invar_btree t) \<and> map rank ts = rev [0..<r]"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    66
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    67
definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
66522
nipkow
parents: 66491
diff changeset
    68
"invar_bheap ts
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66565
diff changeset
    69
  \<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (<) (map rank ts))"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    70
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    71
text \<open>Ordering (heap) invariant\<close>
66522
nipkow
parents: 66491
diff changeset
    72
fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where
nipkow
parents: 66491
diff changeset
    73
"invar_otree (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t \<and> x \<le> root t)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    74
66522
nipkow
parents: 66491
diff changeset
    75
definition invar_oheap :: "'a::linorder heap \<Rightarrow> bool" where
nipkow
parents: 66491
diff changeset
    76
"invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    77
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    78
definition invar :: "'a::linorder heap \<Rightarrow> bool" where
66522
nipkow
parents: 66491
diff changeset
    79
"invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap ts"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    80
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    81
text \<open>The children of a node are a valid heap\<close>
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    82
lemma invar_oheap_children:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    83
  "invar_otree (Node r v ts) \<Longrightarrow> invar_oheap (rev ts)"
66522
nipkow
parents: 66491
diff changeset
    84
by (auto simp: invar_oheap_def)
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    85
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    86
lemma invar_bheap_children:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    87
  "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"
66522
nipkow
parents: 66491
diff changeset
    88
by (auto simp: invar_bheap_def rev_map[symmetric])
nipkow
parents: 66491
diff changeset
    89
nipkow
parents: 66491
diff changeset
    90
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    91
subsection \<open>Operations and Their Functional Correctness\<close>
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    92
66522
nipkow
parents: 66491
diff changeset
    93
subsubsection \<open>\<open>link\<close>\<close>
nipkow
parents: 66491
diff changeset
    94
66548
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    95
context
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    96
includes pattern_aliases
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    97
begin
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    98
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    99
fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   100
  "link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) =
66549
b8a6f9337229 tuned names
nipkow
parents: 66548
diff changeset
   101
    (if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#ts\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#ts\<^sub>2))"
66548
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   102
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   103
end
66491
nipkow
parents: 66434
diff changeset
   104
66522
nipkow
parents: 66491
diff changeset
   105
lemma invar_btree_link:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   106
  assumes "invar_btree t\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   107
  assumes "invar_btree t\<^sub>2"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   108
  assumes "rank t\<^sub>1 = rank t\<^sub>2"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   109
  shows "invar_btree (link t\<^sub>1 t\<^sub>2)"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   110
using assms
66548
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   111
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
66522
nipkow
parents: 66491
diff changeset
   112
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   113
lemma invar_link_otree:
66522
nipkow
parents: 66491
diff changeset
   114
  assumes "invar_otree t\<^sub>1"
nipkow
parents: 66491
diff changeset
   115
  assumes "invar_otree t\<^sub>2"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   116
  shows "invar_otree (link t\<^sub>1 t\<^sub>2)"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   117
using assms
66548
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   118
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto
66522
nipkow
parents: 66491
diff changeset
   119
nipkow
parents: 66491
diff changeset
   120
lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
66548
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   121
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   122
66522
nipkow
parents: 66491
diff changeset
   123
lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
66548
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   124
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   125
66522
nipkow
parents: 66491
diff changeset
   126
subsubsection \<open>\<open>ins_tree\<close>\<close>
nipkow
parents: 66491
diff changeset
   127
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   128
fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   129
  "ins_tree t [] = [t]"
66522
nipkow
parents: 66491
diff changeset
   130
| "ins_tree t\<^sub>1 (t\<^sub>2#ts) =
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   131
  (if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#ts else ins_tree (link t\<^sub>1 t\<^sub>2) ts)"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   132
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   133
lemma invar_bheap_Cons[simp]:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   134
  "invar_bheap (t#ts)
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   135
  \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
68109
cebf36c14226 new def of sorted and sorted_wrt
nipkow
parents: 68021
diff changeset
   136
by (auto simp: invar_bheap_def)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   137
66522
nipkow
parents: 66491
diff changeset
   138
lemma invar_btree_ins_tree:
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   139
  assumes "invar_btree t"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   140
  assumes "invar_bheap ts"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   141
  assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   142
  shows "invar_bheap (ins_tree t ts)"
66522
nipkow
parents: 66491
diff changeset
   143
using assms
nipkow
parents: 66491
diff changeset
   144
by (induction t ts rule: ins_tree.induct) (auto simp: invar_btree_link less_eq_Suc_le[symmetric])
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   145
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   146
lemma invar_oheap_Cons[simp]:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   147
  "invar_oheap (t#ts) \<longleftrightarrow> invar_otree t \<and> invar_oheap ts"
66522
nipkow
parents: 66491
diff changeset
   148
by (auto simp: invar_oheap_def)
nipkow
parents: 66491
diff changeset
   149
nipkow
parents: 66491
diff changeset
   150
lemma invar_oheap_ins_tree:
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   151
  assumes "invar_otree t"
66522
nipkow
parents: 66491
diff changeset
   152
  assumes "invar_oheap ts"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   153
  shows "invar_oheap (ins_tree t ts)"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   154
using assms
66522
nipkow
parents: 66491
diff changeset
   155
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   156
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   157
lemma mset_heap_ins_tree[simp]:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   158
  "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   159
by (induction t ts rule: ins_tree.induct) auto
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   160
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   161
lemma ins_tree_rank_bound:
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   162
  assumes "t' \<in> set (ins_tree t ts)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   163
  assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   164
  assumes "rank t\<^sub>0 < rank t"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   165
  shows "rank t\<^sub>0 < rank t'"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   166
using assms
66522
nipkow
parents: 66491
diff changeset
   167
by (induction t ts rule: ins_tree.induct) (auto split: if_splits)
nipkow
parents: 66491
diff changeset
   168
nipkow
parents: 66491
diff changeset
   169
subsubsection \<open>\<open>insert\<close>\<close>
nipkow
parents: 66491
diff changeset
   170
nipkow
parents: 66491
diff changeset
   171
hide_const (open) insert
nipkow
parents: 66491
diff changeset
   172
nipkow
parents: 66491
diff changeset
   173
definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
nipkow
parents: 66491
diff changeset
   174
"insert x ts = ins_tree (Node 0 x []) ts"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   175
66522
nipkow
parents: 66491
diff changeset
   176
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   177
by (auto intro!: invar_btree_ins_tree simp: invar_oheap_ins_tree insert_def invar_def)
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   178
66522
nipkow
parents: 66491
diff changeset
   179
lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"
nipkow
parents: 66491
diff changeset
   180
by(auto simp: insert_def)
nipkow
parents: 66491
diff changeset
   181
nipkow
parents: 66491
diff changeset
   182
subsubsection \<open>\<open>merge\<close>\<close>
66491
nipkow
parents: 66434
diff changeset
   183
70607
nipkow
parents: 70450
diff changeset
   184
context
nipkow
parents: 70450
diff changeset
   185
includes pattern_aliases
nipkow
parents: 70450
diff changeset
   186
begin
nipkow
parents: 70450
diff changeset
   187
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   188
fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   189
  "merge ts\<^sub>1 [] = ts\<^sub>1"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   190
| "merge [] ts\<^sub>2 = ts\<^sub>2"
70607
nipkow
parents: 70450
diff changeset
   191
| "merge (t\<^sub>1#ts\<^sub>1 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = (
nipkow
parents: 70450
diff changeset
   192
    if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 h\<^sub>2 else
nipkow
parents: 70450
diff changeset
   193
    if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge h\<^sub>1 ts\<^sub>2
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   194
    else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
66491
nipkow
parents: 66434
diff changeset
   195
  )"
nipkow
parents: 66434
diff changeset
   196
70607
nipkow
parents: 70450
diff changeset
   197
end
nipkow
parents: 70450
diff changeset
   198
66522
nipkow
parents: 66491
diff changeset
   199
lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2"
nipkow
parents: 66491
diff changeset
   200
by (cases ts\<^sub>2) auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   201
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   202
lemma merge_rank_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   203
  assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)"
70607
nipkow
parents: 70450
diff changeset
   204
  assumes "\<forall>t\<^sub>1\<in>set ts\<^sub>1. rank t < rank t\<^sub>1"
nipkow
parents: 70450
diff changeset
   205
  assumes "\<forall>t\<^sub>2\<in>set ts\<^sub>2. rank t < rank t\<^sub>2"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   206
  shows "rank t < rank t'"
66522
nipkow
parents: 66491
diff changeset
   207
using assms
nipkow
parents: 66491
diff changeset
   208
by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
nipkow
parents: 66491
diff changeset
   209
   (auto split: if_splits simp: ins_tree_rank_bound)
nipkow
parents: 66491
diff changeset
   210
nipkow
parents: 66491
diff changeset
   211
lemma invar_bheap_merge:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   212
  assumes "invar_bheap ts\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   213
  assumes "invar_bheap ts\<^sub>2"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   214
  shows "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   215
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   216
proof (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   217
  case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   218
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   219
  from "3.prems" have [simp]: "invar_btree t\<^sub>1" "invar_btree t\<^sub>2"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   220
    by auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   221
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   222
  consider (LT) "rank t\<^sub>1 < rank t\<^sub>2"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   223
         | (GT) "rank t\<^sub>1 > rank t\<^sub>2"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   224
         | (EQ) "rank t\<^sub>1 = rank t\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   225
    using antisym_conv3 by blast
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   226
  then show ?case proof cases
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   227
    case LT
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   228
    then show ?thesis using 3
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   229
      by (force elim!: merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   230
  next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   231
    case GT
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   232
    then show ?thesis using 3
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   233
      by (force elim!: merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   234
  next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   235
    case [simp]: EQ
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   236
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   237
    from "3.IH"(3) "3.prems" have [simp]: "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   238
      by auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   239
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   240
    have "rank t\<^sub>2 < rank t'" if "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" for t'
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   241
      using that
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   242
      apply (rule merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   243
      using "3.prems" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   244
    with EQ show ?thesis
66522
nipkow
parents: 66491
diff changeset
   245
      by (auto simp: Suc_le_eq invar_btree_ins_tree invar_btree_link)
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   246
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   247
qed simp_all
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   248
66522
nipkow
parents: 66491
diff changeset
   249
lemma invar_oheap_merge:
nipkow
parents: 66491
diff changeset
   250
  assumes "invar_oheap ts\<^sub>1"
nipkow
parents: 66491
diff changeset
   251
  assumes "invar_oheap ts\<^sub>2"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   252
  shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)"
66522
nipkow
parents: 66491
diff changeset
   253
using assms
nipkow
parents: 66491
diff changeset
   254
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   255
   (auto simp: invar_oheap_ins_tree invar_link_otree)
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   256
66522
nipkow
parents: 66491
diff changeset
   257
lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
nipkow
parents: 66491
diff changeset
   258
by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   259
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   260
lemma mset_heap_merge[simp]:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   261
  "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   262
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   263
66522
nipkow
parents: 66491
diff changeset
   264
subsubsection \<open>\<open>get_min\<close>\<close>
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   265
66522
nipkow
parents: 66491
diff changeset
   266
fun get_min :: "'a::linorder heap \<Rightarrow> 'a" where
nipkow
parents: 66491
diff changeset
   267
  "get_min [t] = root t"
66546
nipkow
parents: 66522
diff changeset
   268
| "get_min (t#ts) = min (root t) (get_min ts)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   269
66522
nipkow
parents: 66491
diff changeset
   270
lemma invar_otree_root_min:
nipkow
parents: 66491
diff changeset
   271
  assumes "invar_otree t"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   272
  assumes "x \<in># mset_tree t"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   273
  shows "root t \<le> x"
66522
nipkow
parents: 66491
diff changeset
   274
using assms
nipkow
parents: 66491
diff changeset
   275
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   276
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   277
lemma get_min_mset_aux:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   278
  assumes "ts\<noteq>[]"
66522
nipkow
parents: 66491
diff changeset
   279
  assumes "invar_oheap ts"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   280
  assumes "x \<in># mset_heap ts"
66522
nipkow
parents: 66491
diff changeset
   281
  shows "get_min ts \<le> x"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   282
  using assms
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   283
apply (induction ts arbitrary: x rule: get_min.induct)
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   284
apply (auto
66546
nipkow
parents: 66522
diff changeset
   285
      simp: invar_otree_root_min min_def intro: order_trans;
66522
nipkow
parents: 66491
diff changeset
   286
      meson linear order_trans invar_otree_root_min
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   287
      )+
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   288
done
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   289
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   290
lemma get_min_mset:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   291
  assumes "ts\<noteq>[]"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   292
  assumes "invar ts"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   293
  assumes "x \<in># mset_heap ts"
66522
nipkow
parents: 66491
diff changeset
   294
  shows "get_min ts \<le> x"
nipkow
parents: 66491
diff changeset
   295
using assms by (auto simp: invar_def get_min_mset_aux)
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   296
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   297
lemma get_min_member:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   298
  "ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"
66546
nipkow
parents: 66522
diff changeset
   299
by (induction ts rule: get_min.induct) (auto simp: min_def)
66522
nipkow
parents: 66491
diff changeset
   300
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   301
lemma get_min:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   302
  assumes "mset_heap ts \<noteq> {#}"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   303
  assumes "invar ts"
66522
nipkow
parents: 66491
diff changeset
   304
  shows "get_min ts = Min_mset (mset_heap ts)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   305
using assms get_min_member get_min_mset
66522
nipkow
parents: 66491
diff changeset
   306
by (auto simp: eq_Min_iff)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   307
66522
nipkow
parents: 66491
diff changeset
   308
subsubsection \<open>\<open>get_min_rest\<close>\<close>
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   309
66522
nipkow
parents: 66491
diff changeset
   310
fun get_min_rest :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where
nipkow
parents: 66491
diff changeset
   311
  "get_min_rest [t] = (t,[])"
nipkow
parents: 66491
diff changeset
   312
| "get_min_rest (t#ts) = (let (t',ts') = get_min_rest ts
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   313
                     in if root t \<le> root t' then (t,ts) else (t',t#ts'))"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   314
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   315
lemma get_min_rest_get_min_same_root:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   316
  assumes "ts\<noteq>[]"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   317
  assumes "get_min_rest ts = (t',ts')"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   318
  shows "root t' = get_min ts"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   319
using assms
66546
nipkow
parents: 66522
diff changeset
   320
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits)
66522
nipkow
parents: 66491
diff changeset
   321
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   322
lemma mset_get_min_rest:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   323
  assumes "get_min_rest ts = (t',ts')"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   324
  assumes "ts\<noteq>[]"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   325
  shows "mset ts = {#t'#} + mset ts'"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   326
using assms
66522
nipkow
parents: 66491
diff changeset
   327
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   328
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   329
lemma seT_get_min_rest:
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   330
  assumes "get_min_rest ts = (t', ts')"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   331
  assumes "ts\<noteq>[]"
66522
nipkow
parents: 66491
diff changeset
   332
  shows "set ts = Set.insert t' (set ts')"
nipkow
parents: 66491
diff changeset
   333
using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]]
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   334
by auto
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   335
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   336
lemma invar_bheap_get_min_rest:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   337
  assumes "get_min_rest ts = (t',ts')"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   338
  assumes "ts\<noteq>[]"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   339
  assumes "invar_bheap ts"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   340
  shows "invar_btree t'" and "invar_bheap ts'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   341
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   342
  have "invar_btree t' \<and> invar_bheap ts'"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   343
    using assms
66522
nipkow
parents: 66491
diff changeset
   344
    proof (induction ts arbitrary: t' ts' rule: get_min.induct)
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   345
      case (2 t v va)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   346
      then show ?case
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   347
        apply (clarsimp split: prod.splits if_splits)
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   348
        apply (drule seT_get_min_rest; fastforce)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   349
        done
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   350
    qed auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   351
  thus "invar_btree t'" and "invar_bheap ts'" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   352
qed
66522
nipkow
parents: 66491
diff changeset
   353
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   354
lemma invar_oheap_get_min_rest:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   355
  assumes "get_min_rest ts = (t',ts')"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   356
  assumes "ts\<noteq>[]"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   357
  assumes "invar_oheap ts"
66522
nipkow
parents: 66491
diff changeset
   358
  shows "invar_otree t'" and "invar_oheap ts'"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   359
using assms
66522
nipkow
parents: 66491
diff changeset
   360
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
nipkow
parents: 66491
diff changeset
   361
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   362
subsubsection \<open>\<open>del_min\<close>\<close>
66522
nipkow
parents: 66491
diff changeset
   363
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   364
definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   365
"del_min ts = (case get_min_rest ts of
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   366
   (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   367
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   368
lemma invar_del_min[simp]:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   369
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   370
  assumes "invar ts"
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   371
  shows "invar (del_min ts)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   372
using assms
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   373
unfolding invar_def del_min_def
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   374
by (auto
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   375
      split: prod.split tree.split
66522
nipkow
parents: 66491
diff changeset
   376
      intro!: invar_bheap_merge invar_oheap_merge
nipkow
parents: 66491
diff changeset
   377
      dest: invar_bheap_get_min_rest invar_oheap_get_min_rest
nipkow
parents: 66491
diff changeset
   378
      intro!: invar_oheap_children invar_bheap_children
nipkow
parents: 66491
diff changeset
   379
    )
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   380
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   381
lemma mset_heap_del_min:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   382
  assumes "ts \<noteq> []"
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   383
  shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}"
66522
nipkow
parents: 66491
diff changeset
   384
using assms
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   385
unfolding del_min_def
66522
nipkow
parents: 66491
diff changeset
   386
apply (clarsimp split: tree.split prod.split)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   387
apply (frule (1) get_min_rest_get_min_same_root)
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   388
apply (frule (1) mset_get_min_rest)
66522
nipkow
parents: 66491
diff changeset
   389
apply (auto simp: mset_heap_def)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   390
done
66522
nipkow
parents: 66491
diff changeset
   391
nipkow
parents: 66491
diff changeset
   392
nipkow
parents: 66491
diff changeset
   393
subsubsection \<open>Instantiating the Priority Queue Locale\<close>
nipkow
parents: 66491
diff changeset
   394
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   395
text \<open>Last step of functional correctness proof: combine all the above lemmas
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   396
to show that binomial heaps satisfy the specification of priority queues with merge.\<close>
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   397
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   398
interpretation binheap: Priority_Queue_Merge
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66565
diff changeset
   399
  where empty = "[]" and is_empty = "(=) []" and insert = insert
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   400
  and get_min = get_min and del_min = del_min and merge = merge
66522
nipkow
parents: 66491
diff changeset
   401
  and invar = invar and mset = mset_heap
nipkow
parents: 66491
diff changeset
   402
proof (unfold_locales, goal_cases)
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   403
  case 1 thus ?case by simp
66522
nipkow
parents: 66491
diff changeset
   404
next
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   405
  case 2 thus ?case by auto
66522
nipkow
parents: 66491
diff changeset
   406
next
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   407
  case 3 thus ?case by auto
66522
nipkow
parents: 66491
diff changeset
   408
next
nipkow
parents: 66491
diff changeset
   409
  case (4 q)
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   410
  thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>]
66522
nipkow
parents: 66491
diff changeset
   411
    by (auto simp: union_single_eq_diff)
nipkow
parents: 66491
diff changeset
   412
next
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   413
  case (5 q) thus ?case using get_min[of q] by auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   414
next
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   415
  case 6 thus ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   416
next
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   417
  case 7 thus ?case by simp
66522
nipkow
parents: 66491
diff changeset
   418
next
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   419
  case 8 thus ?case by simp
66522
nipkow
parents: 66491
diff changeset
   420
next
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   421
  case 9 thus ?case by simp
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   422
next
ff561d9cb661 added PQ with merge
nipkow
parents: 66549
diff changeset
   423
  case 10 thus ?case by simp
66522
nipkow
parents: 66491
diff changeset
   424
qed
nipkow
parents: 66491
diff changeset
   425
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   426
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   427
subsection \<open>Complexity\<close>
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   428
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   429
text \<open>The size of a binomial tree is determined by its rank\<close>
66522
nipkow
parents: 66491
diff changeset
   430
lemma size_mset_btree:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   431
  assumes "invar_btree t"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   432
  shows "size (mset_tree t) = 2^rank t"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   433
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   434
proof (induction t)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   435
  case (Node r v ts)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   436
  hence IH: "size (mset_tree t) = 2^rank t" if "t \<in> set ts" for t
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   437
    using that by auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   438
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   439
  from Node have COMPL: "map rank ts = rev [0..<r]" by auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   440
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   441
  have "size (mset_heap ts) = (\<Sum>t\<leftarrow>ts. size (mset_tree t))"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   442
    by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   443
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   444
    by (auto cong: map_cong)
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   445
  also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   446
    by (induction ts) auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   447
  also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   448
    unfolding COMPL
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   449
    by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   450
  also have "\<dots> = 2^r - 1"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   451
    by (induction r) auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   452
  finally show ?case
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   453
    by (simp)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   454
qed
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   455
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   456
text \<open>The length of a binomial heap is bounded by the number of its elements\<close>
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   457
lemma size_mset_bheap:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   458
  assumes "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   459
  shows "2^length ts \<le> size (mset_heap ts) + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   460
proof -
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   461
  from \<open>invar_bheap ts\<close> have
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66565
diff changeset
   462
    ASC: "sorted_wrt (<) (map rank ts)" and
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   463
    TINV: "\<forall>t\<in>set ts. invar_btree t"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   464
    unfolding invar_bheap_def by auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   465
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   466
  have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   467
    by (simp add: sum_power2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   468
  also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66565
diff changeset
   469
    using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "(^) (2::nat)"]
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   470
    using power_increasing[where a="2::nat"]
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   471
    by (auto simp: o_def)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   472
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   473
    by (auto cong: map_cong simp: size_mset_btree)
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   474
  also have "\<dots> = size (mset_heap ts) + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   475
    unfolding mset_heap_def by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   476
  finally show ?thesis .
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   477
qed
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   478
66522
nipkow
parents: 66491
diff changeset
   479
subsubsection \<open>Timing Functions\<close>
nipkow
parents: 66491
diff changeset
   480
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   481
text \<open>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   482
  We define timing functions for each operation, and provide
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   483
  estimations of their complexity.
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   484
\<close>
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   485
definition T_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   486
[simp]: "T_link _ _ = 1"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   487
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   488
fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   489
  "T_ins_tree t [] = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   490
| "T_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = (
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   491
    (if rank t\<^sub>1 < rank t\<^sub>2 then 1
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   492
     else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) rest)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   493
  )"
66522
nipkow
parents: 66491
diff changeset
   494
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   495
definition T_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   496
"T_insert x ts = T_ins_tree (Node 0 x []) ts"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   497
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   498
lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   499
by (induction t ts rule: T_ins_tree.induct) auto
66522
nipkow
parents: 66491
diff changeset
   500
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   501
subsubsection \<open>\<open>T_insert\<close>\<close>
66522
nipkow
parents: 66491
diff changeset
   502
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   503
lemma T_insert_bound:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   504
  assumes "invar ts"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   505
  shows "T_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   506
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   507
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   508
  have 1: "T_insert x ts \<le> length ts + 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   509
    unfolding T_insert_def by (rule T_ins_tree_simple_bound)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   510
  also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   511
  proof -
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   512
    from size_mset_bheap[of ts] assms
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   513
    have "2 ^ length ts \<le> size (mset_heap ts) + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   514
      unfolding invar_def by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   515
    hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   516
    thus ?thesis using le_log2_of_power by blast
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   517
  qed
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   518
  finally show ?thesis
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   519
    by (simp only: log_mult of_nat_mult) auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   520
qed
66522
nipkow
parents: 66491
diff changeset
   521
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   522
subsubsection \<open>\<open>T_merge\<close>\<close>
66522
nipkow
parents: 66491
diff changeset
   523
70607
nipkow
parents: 70450
diff changeset
   524
context
nipkow
parents: 70450
diff changeset
   525
includes pattern_aliases
nipkow
parents: 70450
diff changeset
   526
begin
nipkow
parents: 70450
diff changeset
   527
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   528
fun T_merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   529
  "T_merge ts\<^sub>1 [] = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   530
| "T_merge [] ts\<^sub>2 = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   531
| "T_merge (t\<^sub>1#ts\<^sub>1 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = 1 + (
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   532
    if rank t\<^sub>1 < rank t\<^sub>2 then T_merge ts\<^sub>1 h\<^sub>2
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   533
    else if rank t\<^sub>2 < rank t\<^sub>1 then T_merge h\<^sub>1 ts\<^sub>2
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   534
    else T_ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) + T_merge ts\<^sub>1 ts\<^sub>2
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   535
  )"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   536
70607
nipkow
parents: 70450
diff changeset
   537
end
nipkow
parents: 70450
diff changeset
   538
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   539
text \<open>A crucial idea is to estimate the time in correlation with the
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   540
  result length, as each carry reduces the length of the result.\<close>
66522
nipkow
parents: 66491
diff changeset
   541
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   542
lemma T_ins_tree_length:
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   543
  "T_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   544
by (induction t ts rule: ins_tree.induct) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   545
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   546
lemma T_merge_length:
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   547
  "length (merge ts\<^sub>1 ts\<^sub>2) + T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   548
by (induction ts\<^sub>1 ts\<^sub>2 rule: T_merge.induct)
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   549
   (auto simp: T_ins_tree_length algebra_simps)
66522
nipkow
parents: 66491
diff changeset
   550
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   551
text \<open>Finally, we get the desired logarithmic bound\<close>
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   552
lemma T_merge_bound_aux:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   553
  fixes ts\<^sub>1 ts\<^sub>2
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   554
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   555
  defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   556
  assumes BINVARS: "invar_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   557
  shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   558
proof -
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   559
  define n where "n = n\<^sub>1 + n\<^sub>2"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   560
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   561
  from T_merge_length[of ts\<^sub>1 ts\<^sub>2]
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   562
  have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" by auto
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   563
  hence "(2::nat)^T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   564
    by (rule power_increasing) auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   565
  also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   566
    by (auto simp: algebra_simps power_add power_mult)
66547
nipkow
parents: 66546
diff changeset
   567
  also note BINVARS(1)[THEN size_mset_bheap]
nipkow
parents: 66546
diff changeset
   568
  also note BINVARS(2)[THEN size_mset_bheap]
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   569
  finally have "2 ^ T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   570
    by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   571
  from le_log2_of_power[OF this] have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   572
    by simp
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   573
  also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   574
    by (simp add: log_mult log_nat_power)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   575
  also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   576
  finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n + 1)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   577
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   578
  also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   579
  finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   580
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   581
  also have "log 2 2 \<le> 2" by auto
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   582
  finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   583
  thus ?thesis unfolding n_def by (auto simp: algebra_simps)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   584
qed
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   585
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   586
lemma T_merge_bound:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   587
  fixes ts\<^sub>1 ts\<^sub>2
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   588
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   589
  defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   590
  assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   591
  shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   592
using assms T_merge_bound_aux unfolding invar_def by blast
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   593
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   594
subsubsection \<open>\<open>T_get_min\<close>\<close>
66522
nipkow
parents: 66491
diff changeset
   595
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   596
fun T_get_min :: "'a::linorder heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   597
  "T_get_min [t] = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   598
| "T_get_min (t#ts) = 1 + T_get_min ts"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   599
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   600
lemma T_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   601
by (induction ts rule: T_get_min.induct) auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   602
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   603
lemma T_get_min_bound:
66522
nipkow
parents: 66491
diff changeset
   604
  assumes "invar ts"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   605
  assumes "ts\<noteq>[]"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   606
  shows "T_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   607
proof -
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   608
  have 1: "T_get_min ts = length ts" using assms T_get_min_estimate by auto
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   609
  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   610
  proof -
66547
nipkow
parents: 66546
diff changeset
   611
    from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
66522
nipkow
parents: 66491
diff changeset
   612
      unfolding invar_def by auto
nipkow
parents: 66491
diff changeset
   613
    thus ?thesis using le_log2_of_power by blast
nipkow
parents: 66491
diff changeset
   614
  qed
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   615
  finally show ?thesis by auto
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   616
qed
66522
nipkow
parents: 66491
diff changeset
   617
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   618
subsubsection \<open>\<open>T_del_min\<close>\<close>
66522
nipkow
parents: 66491
diff changeset
   619
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   620
fun T_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   621
  "T_get_min_rest [t] = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   622
| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"
66522
nipkow
parents: 66491
diff changeset
   623
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   624
lemma T_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min_rest ts = length ts"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   625
  by (induction ts rule: T_get_min_rest.induct) auto
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   626
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   627
lemma T_get_min_rest_bound_aux:
66522
nipkow
parents: 66491
diff changeset
   628
  assumes "invar_bheap ts"
nipkow
parents: 66491
diff changeset
   629
  assumes "ts\<noteq>[]"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   630
  shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
66522
nipkow
parents: 66491
diff changeset
   631
proof -
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   632
  have 1: "T_get_min_rest ts = length ts" using assms T_get_min_rest_estimate by auto
66522
nipkow
parents: 66491
diff changeset
   633
  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
nipkow
parents: 66491
diff changeset
   634
  proof -
66547
nipkow
parents: 66546
diff changeset
   635
    from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   636
      by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   637
    thus ?thesis using le_log2_of_power by blast
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   638
  qed
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   639
  finally show ?thesis by auto
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   640
qed
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   641
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   642
lemma T_get_min_rest_bound:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   643
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   644
  assumes "ts\<noteq>[]"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   645
  shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   646
using assms T_get_min_rest_bound_aux unfolding invar_def by blast
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   647
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 68492
diff changeset
   648
text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity,
66522
nipkow
parents: 66491
diff changeset
   649
it can and is implemented (via suitable code lemmas) as a linear time function.
nipkow
parents: 66491
diff changeset
   650
Thus the following definition is justified:\<close>
nipkow
parents: 66491
diff changeset
   651
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   652
definition "T_rev xs = length xs + 1"
66522
nipkow
parents: 66491
diff changeset
   653
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   654
definition T_del_min :: "'a::linorder heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   655
  "T_del_min ts = T_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   656
                    \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   657
  )"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   658
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   659
lemma T_rev_ts1_bound_aux:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   660
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   661
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   662
  assumes BINVAR: "invar_bheap (rev ts)"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   663
  shows "T_rev ts \<le> 1 + log 2 (n+1)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   664
proof -
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   665
  have "T_rev ts = length ts + 1" by (auto simp: T_rev_def)
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   666
  hence "2^T_rev ts = 2*2^length ts" by auto
66547
nipkow
parents: 66546
diff changeset
   667
  also have "\<dots> \<le> 2*n+2" using size_mset_bheap[OF BINVAR] by (auto simp: n_def)
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   668
  finally have "2 ^ T_rev ts \<le> 2 * n + 2" .
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   669
  from le_log2_of_power[OF this] have "T_rev ts \<le> log 2 (2 * (n + 1))"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   670
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   671
  also have "\<dots> = 1 + log 2 (n+1)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   672
    by (simp only: of_nat_mult log_mult) auto
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   673
  finally show ?thesis by (auto simp: algebra_simps)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   674
qed
66522
nipkow
parents: 66491
diff changeset
   675
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   676
lemma T_del_min_bound_aux:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   677
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   678
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   679
  assumes BINVAR: "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   680
  assumes "ts\<noteq>[]"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   681
  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   682
proof -
66522
nipkow
parents: 66491
diff changeset
   683
  obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   684
    by (metis surj_pair tree.exhaust_sel)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   685
66522
nipkow
parents: 66491
diff changeset
   686
  note BINVAR' = invar_bheap_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
nipkow
parents: 66491
diff changeset
   687
  hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: invar_bheap_children)
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   688
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   689
  define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   690
  define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   691
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   692
  have T_rev_ts1_bound: "T_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   693
  proof -
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   694
    note T_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def]
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   695
    also have "n\<^sub>1 \<le> n"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   696
      unfolding n\<^sub>1_def n_def
66522
nipkow
parents: 66491
diff changeset
   697
      using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   698
      by (auto simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   699
    finally show ?thesis by (auto simp: algebra_simps)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   700
  qed
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   701
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   702
  have "T_del_min ts = T_get_min_rest ts + T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   703
    unfolding T_del_min_def by (simp add: GM)
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   704
  also have "\<dots> \<le> log 2 (n+1) + T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   705
    using T_get_min_rest_bound_aux[OF assms(2-)] by (auto simp: n_def)
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   706
  also have "\<dots> \<le> 2*log 2 (n+1) + T_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   707
    using T_rev_ts1_bound by auto
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   708
  also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   709
    using T_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   710
    by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   711
  also have "n\<^sub>1 + n\<^sub>2 \<le> n"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   712
    unfolding n\<^sub>1_def n\<^sub>2_def n_def
66522
nipkow
parents: 66491
diff changeset
   713
    using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   714
    by (auto simp: mset_heap_def)
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   715
  finally have "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   716
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   717
  thus ?thesis by (simp add: algebra_simps)
67486
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   718
qed
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   719
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   720
lemma T_del_min_bound:
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   721
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   722
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   723
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   724
  assumes "ts\<noteq>[]"
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   725
  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   726
using assms T_del_min_bound_aux unfolding invar_def by blast
66434
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   727
72550
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70607
diff changeset
   728
end