src/HOL/Data_Structures/Binomial_Heap.thy
author nipkow
Tue, 05 Jan 2021 11:24:35 +0100
changeset 73295 2138a4a9031a
parent 73182 8b92a2ab5370
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66524
nipkow
parents: 66492
diff changeset
     1
(* Author: Peter Lammich
nipkow
parents: 66492
diff changeset
     2
           Tobias Nipkow (tuning)
nipkow
parents: 66492
diff changeset
     3
*)
66436
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
70636
7c2724cefcb8 reduced dependencies
nipkow
parents: 69609
diff changeset
     9
  "HOL-Library.Pattern_Aliases"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    10
  Complex_Main
73048
caf2fd14e28b removed session name
Peter Lammich
parents: 73045
diff changeset
    11
  Priority_Queue_Specs
66436
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
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    18
  The presentation is engineered for simplicity, and most
66436
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
70793
nipkow
parents: 70636
diff changeset
    31
  "mset_tree (Node _ a ts) = {#a#} + (\<Sum>t\<in>#mset ts. mset_tree t)"
67485
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
70793
nipkow
parents: 70636
diff changeset
    34
  "mset_heap ts = (\<Sum>t\<in>#mset ts. mset_tree t)"
67485
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]:
70793
nipkow
parents: 70636
diff changeset
    37
  "mset_tree (Node r a ts) = {#a#} + mset_heap ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    38
  unfolding mset_heap_def by auto
67485
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> {#}"
66524
nipkow
parents: 66492
diff changeset
    42
by (cases t) auto
67485
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]:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    45
  "mset_heap [] = {#}"
66524
nipkow
parents: 66492
diff changeset
    46
by (auto simp: mset_heap_def)
nipkow
parents: 66492
diff changeset
    47
66436
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"
66524
nipkow
parents: 66492
diff changeset
    49
by (auto simp: mset_heap_def)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    50
66436
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=[]"
66524
nipkow
parents: 66492
diff changeset
    52
by (auto simp: mset_heap_def)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    53
66524
nipkow
parents: 66492
diff changeset
    54
lemma root_in_mset[simp]: "root t \<in># mset_tree t"
67485
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"
66524
nipkow
parents: 66492
diff changeset
    58
by (auto simp: mset_heap_def)
67485
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
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    62
text \<open>Binomial tree\<close>
66524
nipkow
parents: 66492
diff changeset
    63
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    64
"invar_btree (Node r x ts) \<longleftrightarrow>
66524
nipkow
parents: 66492
diff changeset
    65
   (\<forall>t\<in>set ts. invar_btree t) \<and> map rank ts = rev [0..<r]"
66436
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
text \<open>Ordering (heap) invariant\<close>
66524
nipkow
parents: 66492
diff changeset
    68
fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where
nipkow
parents: 66492
diff changeset
    69
"invar_otree (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t \<and> x \<le> root t)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    70
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    71
definition "invar_tree t \<longleftrightarrow> invar_btree t \<and> invar_otree t"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    72
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    73
text \<open>Binomial Heap invariant\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    74
definition "invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_tree t) \<and> (sorted_wrt (<) (map rank ts))"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    75
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    76
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    77
text \<open>The children of a node are a valid heap\<close>
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    78
lemma invar_children:
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    79
  "invar_tree (Node r v ts) \<Longrightarrow> invar (rev ts)"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    80
  by (auto simp: invar_tree_def invar_def rev_map[symmetric])
66524
nipkow
parents: 66492
diff changeset
    81
nipkow
parents: 66492
diff changeset
    82
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    83
subsection \<open>Operations and Their Functional Correctness\<close>
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    84
66524
nipkow
parents: 66492
diff changeset
    85
subsubsection \<open>\<open>link\<close>\<close>
nipkow
parents: 66492
diff changeset
    86
66549
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    87
context
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    88
includes pattern_aliases
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    89
begin
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    90
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    91
fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    92
  "link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) =
66550
b8a6f9337229 tuned names
nipkow
parents: 66549
diff changeset
    93
    (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))"
66549
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    94
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
    95
end
66492
nipkow
parents: 66436
diff changeset
    96
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    97
lemma invar_link:
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    98
  assumes "invar_tree t\<^sub>1"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
    99
  assumes "invar_tree t\<^sub>2"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   100
  assumes "rank t\<^sub>1 = rank t\<^sub>2"
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   101
  shows "invar_tree (link t\<^sub>1 t\<^sub>2)"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   102
using assms unfolding invar_tree_def
66549
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   103
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto
66524
nipkow
parents: 66492
diff changeset
   104
nipkow
parents: 66492
diff changeset
   105
lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
66549
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   106
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   107
66524
nipkow
parents: 66492
diff changeset
   108
lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
66549
253880668a43 simpler definition
nipkow
parents: 66547
diff changeset
   109
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   110
66524
nipkow
parents: 66492
diff changeset
   111
subsubsection \<open>\<open>ins_tree\<close>\<close>
nipkow
parents: 66492
diff changeset
   112
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   113
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
   114
  "ins_tree t [] = [t]"
66524
nipkow
parents: 66492
diff changeset
   115
| "ins_tree t\<^sub>1 (t\<^sub>2#ts) =
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   116
  (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
   117
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   118
lemma invar_tree0[simp]: "invar_tree (Node 0 x [])"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   119
unfolding invar_tree_def by auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   120
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   121
lemma invar_Cons[simp]:
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   122
  "invar (t#ts)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   123
  \<longleftrightarrow> invar_tree t \<and> invar ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   124
by (auto simp: invar_def)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   125
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   126
lemma invar_ins_tree:
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   127
  assumes "invar_tree t"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   128
  assumes "invar ts"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   129
  assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   130
  shows "invar (ins_tree t ts)"
66524
nipkow
parents: 66492
diff changeset
   131
using assms
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   132
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link less_eq_Suc_le[symmetric])
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   133
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   134
lemma mset_heap_ins_tree[simp]:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   135
  "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   136
by (induction t ts rule: ins_tree.induct) auto
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   137
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   138
lemma ins_tree_rank_bound:
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   139
  assumes "t' \<in> set (ins_tree t ts)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   140
  assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   141
  assumes "rank t\<^sub>0 < rank t"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   142
  shows "rank t\<^sub>0 < rank t'"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   143
using assms
66524
nipkow
parents: 66492
diff changeset
   144
by (induction t ts rule: ins_tree.induct) (auto split: if_splits)
nipkow
parents: 66492
diff changeset
   145
nipkow
parents: 66492
diff changeset
   146
subsubsection \<open>\<open>insert\<close>\<close>
nipkow
parents: 66492
diff changeset
   147
nipkow
parents: 66492
diff changeset
   148
hide_const (open) insert
nipkow
parents: 66492
diff changeset
   149
nipkow
parents: 66492
diff changeset
   150
definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
nipkow
parents: 66492
diff changeset
   151
"insert x ts = ins_tree (Node 0 x []) ts"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   152
66524
nipkow
parents: 66492
diff changeset
   153
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)"
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   154
by (auto intro!: invar_ins_tree simp: insert_def)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   155
66524
nipkow
parents: 66492
diff changeset
   156
lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"
nipkow
parents: 66492
diff changeset
   157
by(auto simp: insert_def)
nipkow
parents: 66492
diff changeset
   158
nipkow
parents: 66492
diff changeset
   159
subsubsection \<open>\<open>merge\<close>\<close>
66492
nipkow
parents: 66436
diff changeset
   160
70793
nipkow
parents: 70636
diff changeset
   161
context
nipkow
parents: 70636
diff changeset
   162
includes pattern_aliases
nipkow
parents: 70636
diff changeset
   163
begin
nipkow
parents: 70636
diff changeset
   164
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   165
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
   166
  "merge ts\<^sub>1 [] = ts\<^sub>1"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   167
| "merge [] ts\<^sub>2 = ts\<^sub>2"
70793
nipkow
parents: 70636
diff changeset
   168
| "merge (t\<^sub>1#ts\<^sub>1 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = (
nipkow
parents: 70636
diff changeset
   169
    if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 h\<^sub>2 else
nipkow
parents: 70636
diff changeset
   170
    if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge h\<^sub>1 ts\<^sub>2
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   171
    else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
66492
nipkow
parents: 66436
diff changeset
   172
  )"
nipkow
parents: 66436
diff changeset
   173
70793
nipkow
parents: 70636
diff changeset
   174
end
nipkow
parents: 70636
diff changeset
   175
66524
nipkow
parents: 66492
diff changeset
   176
lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2"
nipkow
parents: 66492
diff changeset
   177
by (cases ts\<^sub>2) auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   178
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   179
lemma merge_rank_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   180
  assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)"
70793
nipkow
parents: 70636
diff changeset
   181
  assumes "\<forall>t\<^sub>1\<in>set ts\<^sub>1. rank t < rank t\<^sub>1"
nipkow
parents: 70636
diff changeset
   182
  assumes "\<forall>t\<^sub>2\<in>set ts\<^sub>2. rank t < rank t\<^sub>2"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   183
  shows "rank t < rank t'"
66524
nipkow
parents: 66492
diff changeset
   184
using assms
nipkow
parents: 66492
diff changeset
   185
by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
nipkow
parents: 66492
diff changeset
   186
   (auto split: if_splits simp: ins_tree_rank_bound)
nipkow
parents: 66492
diff changeset
   187
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   188
lemma invar_merge[simp]:
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   189
  assumes "invar ts\<^sub>1"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   190
  assumes "invar ts\<^sub>2"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   191
  shows "invar (merge ts\<^sub>1 ts\<^sub>2)"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   192
using assms
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   193
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   194
   (auto 0 3 simp: Suc_le_eq intro!: invar_ins_tree invar_link elim!: merge_rank_bound)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   195
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   196
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   197
text \<open>Longer, more explicit proof of @{thm [source] invar_merge}, 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   198
      to illustrate the application of the @{thm [source] merge_rank_bound} lemma.\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   199
lemma 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   200
  assumes "invar ts\<^sub>1"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   201
  assumes "invar ts\<^sub>2"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   202
  shows "invar (merge ts\<^sub>1 ts\<^sub>2)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   203
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   204
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
   205
  case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2)
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   206
  \<comment> \<open>Invariants of the parts can be shown automatically\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   207
  from "3.prems" have [simp]: 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   208
    "invar_tree t\<^sub>1" "invar_tree t\<^sub>2"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   209
    (*"invar (merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2)" 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   210
    "invar (merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2))"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   211
    "invar (merge ts\<^sub>1 ts\<^sub>2)"*)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   212
    by auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   213
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   214
  \<comment> \<open>These are the three cases of the @{const merge} function\<close>
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   215
  consider (LT) "rank t\<^sub>1 < rank t\<^sub>2"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   216
         | (GT) "rank t\<^sub>1 > rank t\<^sub>2"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   217
         | (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
   218
    using antisym_conv3 by blast
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   219
  then show ?case proof cases
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   220
    case LT 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   221
    \<comment> \<open>@{const merge} takes the first tree from the left heap\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   222
    then have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)" by simp
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   223
    also have "invar \<dots>" proof (simp, intro conjI)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   224
      \<comment> \<open>Invariant follows from induction hypothesis\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   225
      show "invar (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2))"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   226
        using LT "3.IH" "3.prems" by simp
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   227
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   228
      \<comment> \<open>It remains to show that \<open>t\<^sub>1\<close> has smallest rank.\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   229
      show "\<forall>t'\<in>set (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)). rank t\<^sub>1 < rank t'"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   230
        \<comment> \<open>Which is done by auxiliary lemma @{thm [source] merge_rank_bound}\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   231
        using LT "3.prems" by (force elim!: merge_rank_bound)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   232
    qed
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   233
    finally show ?thesis .
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   234
  next
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   235
    \<comment> \<open>@{const merge} takes the first tree from the right heap\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   236
    case GT 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   237
    \<comment> \<open>The proof is anaologous to the \<open>LT\<close> case\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   238
    then show ?thesis using "3.prems" "3.IH" by (force elim!: merge_rank_bound)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   239
  next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   240
    case [simp]: EQ
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   241
    \<comment> \<open>@{const merge} links both first trees, and inserts them into the merged remaining heaps\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   242
    have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)" by simp
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   243
    also have "invar \<dots>" proof (intro invar_ins_tree invar_link) 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   244
      \<comment> \<open>Invariant of merged remaining heaps follows by IH\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   245
      show "invar (merge ts\<^sub>1 ts\<^sub>2)"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   246
        using EQ "3.prems" "3.IH" by auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   247
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   248
      \<comment> \<open>For insertion, we have to show that the rank of the linked tree is \<open>\<le>\<close> the 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   249
          ranks in the merged remaining heaps\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   250
      show "\<forall>t'\<in>set (merge ts\<^sub>1 ts\<^sub>2). rank (link t\<^sub>1 t\<^sub>2) \<le> rank t'"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   251
      proof -
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   252
        \<comment> \<open>Which is, again, done with the help of @{thm [source] merge_rank_bound}\<close>
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   253
        have "rank (link t\<^sub>1 t\<^sub>2) = Suc (rank t\<^sub>2)" by simp
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   254
        thus ?thesis using "3.prems" by (auto simp: Suc_le_eq elim!: merge_rank_bound)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   255
      qed
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   256
    qed simp_all
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   257
    finally show ?thesis .
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   258
  qed
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   259
qed auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   260
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   261
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   262
lemma mset_heap_merge[simp]:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   263
  "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   264
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   265
66524
nipkow
parents: 66492
diff changeset
   266
subsubsection \<open>\<open>get_min\<close>\<close>
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   267
66524
nipkow
parents: 66492
diff changeset
   268
fun get_min :: "'a::linorder heap \<Rightarrow> 'a" where
nipkow
parents: 66492
diff changeset
   269
  "get_min [t] = root t"
66546
nipkow
parents: 66524
diff changeset
   270
| "get_min (t#ts) = min (root t) (get_min ts)"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   271
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   272
lemma invar_tree_root_min:
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   273
  assumes "invar_tree t"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   274
  assumes "x \<in># mset_tree t"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   275
  shows "root t \<le> x"
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   276
using assms unfolding invar_tree_def
66524
nipkow
parents: 66492
diff changeset
   277
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   278
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   279
lemma get_min_mset:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   280
  assumes "ts\<noteq>[]"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   281
  assumes "invar ts"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   282
  assumes "x \<in># mset_heap ts"
66524
nipkow
parents: 66492
diff changeset
   283
  shows "get_min ts \<le> x"
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   284
  using assms
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   285
apply (induction ts arbitrary: x rule: get_min.induct)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   286
apply (auto
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   287
      simp: invar_tree_root_min min_def intro: order_trans;
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   288
      meson linear order_trans invar_tree_root_min
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   289
      )+
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   290
done
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   291
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   292
lemma get_min_member:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   293
  "ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"
66546
nipkow
parents: 66524
diff changeset
   294
by (induction ts rule: get_min.induct) (auto simp: min_def)
66524
nipkow
parents: 66492
diff changeset
   295
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   296
lemma get_min:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   297
  assumes "mset_heap ts \<noteq> {#}"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   298
  assumes "invar ts"
66524
nipkow
parents: 66492
diff changeset
   299
  shows "get_min ts = Min_mset (mset_heap ts)"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   300
using assms get_min_member get_min_mset
66524
nipkow
parents: 66492
diff changeset
   301
by (auto simp: eq_Min_iff)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   302
66524
nipkow
parents: 66492
diff changeset
   303
subsubsection \<open>\<open>get_min_rest\<close>\<close>
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   304
66524
nipkow
parents: 66492
diff changeset
   305
fun get_min_rest :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where
nipkow
parents: 66492
diff changeset
   306
  "get_min_rest [t] = (t,[])"
nipkow
parents: 66492
diff changeset
   307
| "get_min_rest (t#ts) = (let (t',ts') = get_min_rest ts
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   308
                     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
   309
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   310
lemma get_min_rest_get_min_same_root:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   311
  assumes "ts\<noteq>[]"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   312
  assumes "get_min_rest ts = (t',ts')"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   313
  shows "root t' = get_min ts"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   314
using assms
66546
nipkow
parents: 66524
diff changeset
   315
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits)
66524
nipkow
parents: 66492
diff changeset
   316
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   317
lemma mset_get_min_rest:
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   318
  assumes "get_min_rest ts = (t',ts')"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   319
  assumes "ts\<noteq>[]"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   320
  shows "mset ts = {#t'#} + mset ts'"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   321
using assms
66524
nipkow
parents: 66492
diff changeset
   322
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   323
72784
729d45c7ff33 undid renaming accident
blanchet
parents: 72783
diff changeset
   324
lemma set_get_min_rest:
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   325
  assumes "get_min_rest ts = (t', ts')"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   326
  assumes "ts\<noteq>[]"
66524
nipkow
parents: 66492
diff changeset
   327
  shows "set ts = Set.insert t' (set ts')"
nipkow
parents: 66492
diff changeset
   328
using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]]
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   329
by auto
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   330
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   331
lemma invar_get_min_rest:
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   332
  assumes "get_min_rest ts = (t',ts')"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   333
  assumes "ts\<noteq>[]"
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   334
  assumes "invar ts"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   335
  shows "invar_tree t'" and "invar ts'"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   336
proof -
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   337
  have "invar_tree t' \<and> invar ts'"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   338
    using assms
66524
nipkow
parents: 66492
diff changeset
   339
    proof (induction ts arbitrary: t' ts' rule: get_min.induct)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   340
      case (2 t v va)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   341
      then show ?case
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   342
        apply (clarsimp split: prod.splits if_splits)
72784
729d45c7ff33 undid renaming accident
blanchet
parents: 72783
diff changeset
   343
        apply (drule set_get_min_rest; fastforce)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   344
        done
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   345
    qed auto
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   346
  thus "invar_tree t'" and "invar ts'" by auto
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   347
qed
66524
nipkow
parents: 66492
diff changeset
   348
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   349
subsubsection \<open>\<open>del_min\<close>\<close>
66524
nipkow
parents: 66492
diff changeset
   350
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   351
definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   352
"del_min ts = (case get_min_rest ts of
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   353
   (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   354
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   355
lemma invar_del_min[simp]:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   356
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   357
  assumes "invar ts"
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   358
  shows "invar (del_min ts)"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   359
using assms
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   360
unfolding del_min_def
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   361
by (auto
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   362
      split: prod.split tree.split
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   363
      intro!: invar_merge invar_children 
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   364
      dest: invar_get_min_rest
66524
nipkow
parents: 66492
diff changeset
   365
    )
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   366
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   367
lemma mset_heap_del_min:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   368
  assumes "ts \<noteq> []"
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   369
  shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}"
66524
nipkow
parents: 66492
diff changeset
   370
using assms
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   371
unfolding del_min_def
66524
nipkow
parents: 66492
diff changeset
   372
apply (clarsimp split: tree.split prod.split)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   373
apply (frule (1) get_min_rest_get_min_same_root)
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   374
apply (frule (1) mset_get_min_rest)
66524
nipkow
parents: 66492
diff changeset
   375
apply (auto simp: mset_heap_def)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   376
done
66524
nipkow
parents: 66492
diff changeset
   377
nipkow
parents: 66492
diff changeset
   378
nipkow
parents: 66492
diff changeset
   379
subsubsection \<open>Instantiating the Priority Queue Locale\<close>
nipkow
parents: 66492
diff changeset
   380
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   381
text \<open>Last step of functional correctness proof: combine all the above lemmas
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   382
to show that binomial heaps satisfy the specification of priority queues with merge.\<close>
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   383
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   384
interpretation binheap: Priority_Queue_Merge
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66564
diff changeset
   385
  where empty = "[]" and is_empty = "(=) []" and insert = insert
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   386
  and get_min = get_min and del_min = del_min and merge = merge
66524
nipkow
parents: 66492
diff changeset
   387
  and invar = invar and mset = mset_heap
nipkow
parents: 66492
diff changeset
   388
proof (unfold_locales, goal_cases)
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   389
  case 1 thus ?case by simp
66524
nipkow
parents: 66492
diff changeset
   390
next
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   391
  case 2 thus ?case by auto
66524
nipkow
parents: 66492
diff changeset
   392
next
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   393
  case 3 thus ?case by auto
66524
nipkow
parents: 66492
diff changeset
   394
next
nipkow
parents: 66492
diff changeset
   395
  case (4 q)
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   396
  thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>]
66524
nipkow
parents: 66492
diff changeset
   397
    by (auto simp: union_single_eq_diff)
nipkow
parents: 66492
diff changeset
   398
next
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   399
  case (5 q) thus ?case using get_min[of q] by auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   400
next
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   401
  case 6 thus ?case by (auto simp add: invar_def)
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   402
next
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   403
  case 7 thus ?case by simp
66524
nipkow
parents: 66492
diff changeset
   404
next
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   405
  case 8 thus ?case by simp
66524
nipkow
parents: 66492
diff changeset
   406
next
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   407
  case 9 thus ?case by simp
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   408
next
ff561d9cb661 added PQ with merge
nipkow
parents: 66550
diff changeset
   409
  case 10 thus ?case by simp
66524
nipkow
parents: 66492
diff changeset
   410
qed
nipkow
parents: 66492
diff changeset
   411
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   412
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   413
subsection \<open>Complexity\<close>
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   414
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   415
text \<open>The size of a binomial tree is determined by its rank\<close>
66524
nipkow
parents: 66492
diff changeset
   416
lemma size_mset_btree:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   417
  assumes "invar_btree t"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   418
  shows "size (mset_tree t) = 2^rank t"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   419
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   420
proof (induction t)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   421
  case (Node r v ts)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   422
  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
   423
    using that by auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   424
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   425
  from Node have COMPL: "map rank ts = rev [0..<r]" by auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   426
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   427
  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
   428
    by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   429
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   430
    by (auto cong: map_cong)
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   431
  also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   432
    by (induction ts) auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   433
  also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   434
    unfolding COMPL
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   435
    by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   436
  also have "\<dots> = 2^r - 1"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   437
    by (induction r) auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   438
  finally show ?case
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   439
    by (simp)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   440
qed
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   441
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   442
lemma size_mset_tree:
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   443
  assumes "invar_tree t"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   444
  shows "size (mset_tree t) = 2^rank t"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   445
using assms unfolding invar_tree_def
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   446
by (simp add: size_mset_btree)
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   447
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   448
text \<open>The length of a binomial heap is bounded by the number of its elements\<close>
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   449
lemma size_mset_heap:
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   450
  assumes "invar ts"
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   451
  shows "length ts \<le> log 2 (size (mset_heap ts) + 1)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   452
proof -
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   453
  from \<open>invar ts\<close> have
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66564
diff changeset
   454
    ASC: "sorted_wrt (<) (map rank ts)" and
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   455
    TINV: "\<forall>t\<in>set ts. invar_tree t"
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   456
    unfolding invar_def by auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   457
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   458
  have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   459
    by (simp add: sum_power2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   460
  also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 66564
diff changeset
   461
    using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "(^) (2::nat)"]
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   462
    using power_increasing[where a="2::nat"]
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   463
    by (auto simp: o_def)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   464
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   465
    by (auto cong: map_cong simp: size_mset_tree)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   466
  also have "\<dots> = size (mset_heap ts) + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   467
    unfolding mset_heap_def by (induction ts) auto
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   468
  finally have "2^length ts \<le> size (mset_heap ts) + 1" .
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   469
  then show ?thesis using le_log2_of_power by blast
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   470
qed
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   471
66524
nipkow
parents: 66492
diff changeset
   472
subsubsection \<open>Timing Functions\<close>
nipkow
parents: 66492
diff changeset
   473
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   474
text \<open>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   475
  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
   476
  estimations of their complexity.
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   477
\<close>
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   478
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: 70793
diff changeset
   479
[simp]: "T_link _ _ = 1"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   480
73182
8b92a2ab5370 tuned running time functions
Peter Lammich
parents: 73176
diff changeset
   481
text \<open>This function is non-canonical: we omitted a \<open>+1\<close> in the \<open>else\<close>-part,
8b92a2ab5370 tuned running time functions
Peter Lammich
parents: 73176
diff changeset
   482
  to keep the following analysis simpler and more to the point.
8b92a2ab5370 tuned running time functions
Peter Lammich
parents: 73176
diff changeset
   483
\<close>
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   484
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: 70793
diff changeset
   485
  "T_ins_tree t [] = 1"
73295
nipkow
parents: 73182
diff changeset
   486
| "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = (
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   487
    (if rank t\<^sub>1 < rank t\<^sub>2 then 1
73295
nipkow
parents: 73182
diff changeset
   488
     else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   489
  )"
66524
nipkow
parents: 66492
diff changeset
   490
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   491
definition T_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
73175
aa86651805e0 added missing +1 to T_insert (for function call)
Peter Lammich
parents: 73150
diff changeset
   492
"T_insert x ts = T_ins_tree (Node 0 x []) ts + 1"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   493
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   494
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: 70793
diff changeset
   495
by (induction t ts rule: T_ins_tree.induct) auto
66524
nipkow
parents: 66492
diff changeset
   496
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   497
subsubsection \<open>\<open>T_insert\<close>\<close>
66524
nipkow
parents: 66492
diff changeset
   498
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   499
lemma T_insert_bound:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   500
  assumes "invar ts"
73175
aa86651805e0 added missing +1 to T_insert (for function call)
Peter Lammich
parents: 73150
diff changeset
   501
  shows "T_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 2"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   502
proof -
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   503
  have "real (T_insert x ts) \<le> real (length ts) + 2"
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   504
    unfolding T_insert_def using T_ins_tree_simple_bound 
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   505
    using of_nat_mono by fastforce
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   506
  also note size_mset_heap[OF \<open>invar ts\<close>]
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   507
  finally show ?thesis by simp
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   508
qed
66524
nipkow
parents: 66492
diff changeset
   509
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   510
subsubsection \<open>\<open>T_merge\<close>\<close>
66524
nipkow
parents: 66492
diff changeset
   511
70793
nipkow
parents: 70636
diff changeset
   512
context
nipkow
parents: 70636
diff changeset
   513
includes pattern_aliases
nipkow
parents: 70636
diff changeset
   514
begin
nipkow
parents: 70636
diff changeset
   515
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   516
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: 70793
diff changeset
   517
  "T_merge ts\<^sub>1 [] = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   518
| "T_merge [] ts\<^sub>2 = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   519
| "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: 70793
diff changeset
   520
    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: 70793
diff changeset
   521
    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: 70793
diff changeset
   522
    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
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   523
  )"
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   524
70793
nipkow
parents: 70636
diff changeset
   525
end
nipkow
parents: 70636
diff changeset
   526
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   527
text \<open>A crucial idea is to estimate the time in correlation with the
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   528
  result length, as each carry reduces the length of the result.\<close>
66524
nipkow
parents: 66492
diff changeset
   529
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   530
lemma T_ins_tree_length:
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   531
  "T_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   532
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
   533
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   534
lemma T_merge_length:
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   535
  "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: 70793
diff changeset
   536
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: 70793
diff changeset
   537
   (auto simp: T_ins_tree_length algebra_simps)
66524
nipkow
parents: 66492
diff changeset
   538
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   539
text \<open>Finally, we get the desired logarithmic bound\<close>
73150
c145be662fbd removed redundant T_xxx_bound_aux lemmas
Peter Lammich
parents: 73048
diff changeset
   540
lemma T_merge_bound:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   541
  fixes ts\<^sub>1 ts\<^sub>2
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   542
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   543
  defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
73150
c145be662fbd removed redundant T_xxx_bound_aux lemmas
Peter Lammich
parents: 73048
diff changeset
   544
  assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   545
  shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   546
proof -
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   547
  note n_defs = assms(1,2)
73150
c145be662fbd removed redundant T_xxx_bound_aux lemmas
Peter Lammich
parents: 73048
diff changeset
   548
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   549
  have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * real (length ts\<^sub>1) + 2 * real (length ts\<^sub>2) + 1"
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   550
    using T_merge_length[of ts\<^sub>1 ts\<^sub>2] by simp
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   551
  also note size_mset_heap[OF \<open>invar ts\<^sub>1\<close>]
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   552
  also note size_mset_heap[OF \<open>invar ts\<^sub>2\<close>]
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   553
  finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * log 2 (n\<^sub>1 + 1) + 2 * log 2 (n\<^sub>2 + 1) + 1"
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   554
    unfolding n_defs by (simp add: algebra_simps)
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   555
  also have "log 2 (n\<^sub>1 + 1) \<le> log 2 (n\<^sub>1 + n\<^sub>2 + 1)" 
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   556
    unfolding n_defs by (simp add: algebra_simps)
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   557
  also have "log 2 (n\<^sub>2 + 1) \<le> log 2 (n\<^sub>1 + n\<^sub>2 + 1)" 
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   558
    unfolding n_defs by (simp add: algebra_simps)
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   559
  finally show ?thesis by (simp add: algebra_simps)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   560
qed
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   561
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   562
subsubsection \<open>\<open>T_get_min\<close>\<close>
66524
nipkow
parents: 66492
diff changeset
   563
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   564
fun T_get_min :: "'a::linorder heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   565
  "T_get_min [t] = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   566
| "T_get_min (t#ts) = 1 + T_get_min ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   567
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   568
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: 70793
diff changeset
   569
by (induction ts rule: T_get_min.induct) auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   570
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   571
lemma T_get_min_bound:
66524
nipkow
parents: 66492
diff changeset
   572
  assumes "invar ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   573
  assumes "ts\<noteq>[]"
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   574
  shows "T_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   575
proof -
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   576
  have 1: "T_get_min ts = length ts" using assms T_get_min_estimate by auto
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   577
  also note size_mset_heap[OF \<open>invar ts\<close>]
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   578
  finally show ?thesis .
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   579
qed
66524
nipkow
parents: 66492
diff changeset
   580
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   581
subsubsection \<open>\<open>T_del_min\<close>\<close>
66524
nipkow
parents: 66492
diff changeset
   582
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   583
fun T_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   584
  "T_get_min_rest [t] = 1"
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   585
| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"
66524
nipkow
parents: 66492
diff changeset
   586
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   587
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: 70793
diff changeset
   588
  by (induction ts rule: T_get_min_rest.induct) auto
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   589
73150
c145be662fbd removed redundant T_xxx_bound_aux lemmas
Peter Lammich
parents: 73048
diff changeset
   590
lemma T_get_min_rest_bound:
73045
ba65dc3e35af summarized structural and ordering invariant for trees
Peter Lammich
parents: 72952
diff changeset
   591
  assumes "invar ts"
66524
nipkow
parents: 66492
diff changeset
   592
  assumes "ts\<noteq>[]"
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   593
  shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
66524
nipkow
parents: 66492
diff changeset
   594
proof -
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   595
  have 1: "T_get_min_rest ts = length ts" using assms T_get_min_rest_estimate by auto
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   596
  also note size_mset_heap[OF \<open>invar ts\<close>]
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   597
  finally show ?thesis .
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   598
qed
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   599
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 68493
diff changeset
   600
text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity,
66524
nipkow
parents: 66492
diff changeset
   601
it can and is implemented (via suitable code lemmas) as a linear time function.
nipkow
parents: 66492
diff changeset
   602
Thus the following definition is justified:\<close>
nipkow
parents: 66492
diff changeset
   603
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   604
definition "T_rev xs = length xs + 1"
66524
nipkow
parents: 66492
diff changeset
   605
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   606
definition T_del_min :: "'a::linorder heap \<Rightarrow> nat" where
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   607
  "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: 70793
diff changeset
   608
                    \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2
73182
8b92a2ab5370 tuned running time functions
Peter Lammich
parents: 73176
diff changeset
   609
  ) + 1"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   610
73150
c145be662fbd removed redundant T_xxx_bound_aux lemmas
Peter Lammich
parents: 73048
diff changeset
   611
lemma T_del_min_bound:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   612
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   613
  defines "n \<equiv> size (mset_heap ts)"
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   614
  assumes "invar ts" and "ts\<noteq>[]"
73182
8b92a2ab5370 tuned running time functions
Peter Lammich
parents: 73176
diff changeset
   615
  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   616
proof -
66524
nipkow
parents: 66492
diff changeset
   617
  obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   618
    by (metis surj_pair tree.exhaust_sel)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   619
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   620
  have I1: "invar (rev ts\<^sub>1)" and I2: "invar ts\<^sub>2"
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   621
    using invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> \<open>invar ts\<close>] invar_children
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   622
    by auto
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   623
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   624
  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
   625
  define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   626
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   627
  have "n\<^sub>1 \<le> n" "n\<^sub>1 + n\<^sub>2 \<le> n" unfolding n_def n\<^sub>1_def n\<^sub>2_def
66524
nipkow
parents: 66492
diff changeset
   628
    using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   629
    by (auto simp: mset_heap_def)
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   630
73182
8b92a2ab5370 tuned running time functions
Peter Lammich
parents: 73176
diff changeset
   631
  have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2) + 1"
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   632
    unfolding T_del_min_def GM
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   633
    by simp
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   634
  also have "T_get_min_rest ts \<le> log 2 (n+1)" 
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   635
    using T_get_min_rest_bound[OF \<open>invar ts\<close> \<open>ts\<noteq>[]\<close>] unfolding n_def by simp
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   636
  also have "T_rev ts\<^sub>1 \<le> 1 + log 2 (n\<^sub>1 + 1)"
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   637
    unfolding T_rev_def n\<^sub>1_def using size_mset_heap[OF I1] by simp
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   638
  also have "T_merge (rev ts\<^sub>1) ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1"
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   639
    unfolding n\<^sub>1_def n\<^sub>2_def using T_merge_bound[OF I1 I2] by (simp add: algebra_simps)
73182
8b92a2ab5370 tuned running time functions
Peter Lammich
parents: 73176
diff changeset
   640
  finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 3"
73176
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   641
    by (simp add: algebra_simps)
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   642
  also note \<open>n\<^sub>1 + n\<^sub>2 \<le> n\<close>
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   643
  also note \<open>n\<^sub>1 \<le> n\<close>
1dc01c11aa86 simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents: 73175
diff changeset
   644
  finally show ?thesis by (simp add: algebra_simps)
67485
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   645
qed
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   646
72783
1d0ae7e578a0 renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents: 70793
diff changeset
   647
end