src/HOL/Data_Structures/Binomial_Heap.thy
author nipkow
Sun, 27 Aug 2017 16:56:25 +0200
changeset 66524 5fe7ed50d096
parent 66492 78a009ac91d2
child 66546 14a7d2a39336
permissions -rw-r--r--
tuning
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
66492
nipkow
parents: 66436
diff changeset
     9
  Base_FDS
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    10
  Complex_Main
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    11
  Priority_Queue
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
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    18
  The presentation is engineered for simplicity, and most 
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
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    31
  "mset_tree (Node _ a c) = {#a#} + (\<Sum>t\<in>#mset c. mset_tree t)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    32
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    33
definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    34
  "mset_heap c = (\<Sum>t\<in>#mset c. mset_tree t)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    35
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    36
lemma mset_tree_simp_alt[simp]: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    37
  "mset_tree (Node r a c) = {#a#} + mset_heap c"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    38
  unfolding mset_heap_def by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    39
declare mset_tree.simps[simp del]    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    40
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    41
lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}"  
66524
nipkow
parents: 66492
diff changeset
    42
by (cases t) auto
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    43
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    44
lemma mset_heap_Nil[simp]: 
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)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    50
  
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)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    53
    
66524
nipkow
parents: 66492
diff changeset
    54
lemma root_in_mset[simp]: "root t \<in># mset_tree t"
nipkow
parents: 66492
diff changeset
    55
by (cases t) auto    
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    56
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
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)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    59
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    60
subsubsection \<open>Invariants\<close>  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    61
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    62
text \<open>Binomial invariant\<close>  
66524
nipkow
parents: 66492
diff changeset
    63
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where
nipkow
parents: 66492
diff changeset
    64
"invar_btree (Node r x ts) \<longleftrightarrow> 
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
definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
66524
nipkow
parents: 66492
diff changeset
    68
"invar_bheap ts
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    69
  \<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (op <) (map rank ts))"
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>
66524
nipkow
parents: 66492
diff changeset
    72
fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where
nipkow
parents: 66492
diff changeset
    73
"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
    74
66524
nipkow
parents: 66492
diff changeset
    75
definition invar_oheap :: "'a::linorder heap \<Rightarrow> bool" where
nipkow
parents: 66492
diff changeset
    76
"invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    77
  
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
66524
nipkow
parents: 66492
diff changeset
    79
"invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    80
  
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>
66524
nipkow
parents: 66492
diff changeset
    82
lemma invar_oheap_children: 
nipkow
parents: 66492
diff changeset
    83
  "invar_otree (Node r v ts) \<Longrightarrow> invar_oheap (rev ts)"  
nipkow
parents: 66492
diff changeset
    84
by (auto simp: invar_oheap_def)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    85
66524
nipkow
parents: 66492
diff changeset
    86
lemma invar_bheap_children: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    87
  "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"  
66524
nipkow
parents: 66492
diff changeset
    88
by (auto simp: invar_bheap_def rev_map[symmetric])
nipkow
parents: 66492
diff changeset
    89
nipkow
parents: 66492
diff changeset
    90
nipkow
parents: 66492
diff changeset
    91
subsection \<open>Operations and Their Functional Correctness\<close>  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    92
    
66524
nipkow
parents: 66492
diff changeset
    93
subsubsection \<open>\<open>link\<close>\<close>
nipkow
parents: 66492
diff changeset
    94
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    95
definition link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    96
  "link t\<^sub>1 t\<^sub>2 = (case (t\<^sub>1,t\<^sub>2) of (Node r x\<^sub>1 c\<^sub>1, Node _ x\<^sub>2 c\<^sub>2) \<Rightarrow>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    97
    if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#c\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#c\<^sub>2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    98
  )"
66492
nipkow
parents: 66436
diff changeset
    99
66524
nipkow
parents: 66492
diff changeset
   100
lemma invar_btree_link:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   101
  assumes "invar_btree t\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   102
  assumes "invar_btree t\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   103
  assumes "rank t\<^sub>1 = rank t\<^sub>2"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   104
  shows "invar_btree (link t\<^sub>1 t\<^sub>2)"  
66524
nipkow
parents: 66492
diff changeset
   105
using assms 
nipkow
parents: 66492
diff changeset
   106
by (auto simp: link_def split: tree.split)
nipkow
parents: 66492
diff changeset
   107
nipkow
parents: 66492
diff changeset
   108
lemma invar_link_otree:      
nipkow
parents: 66492
diff changeset
   109
  assumes "invar_otree t\<^sub>1"
nipkow
parents: 66492
diff changeset
   110
  assumes "invar_otree t\<^sub>2"
nipkow
parents: 66492
diff changeset
   111
  shows "invar_otree (link t\<^sub>1 t\<^sub>2)"  
nipkow
parents: 66492
diff changeset
   112
using assms 
nipkow
parents: 66492
diff changeset
   113
by (auto simp: link_def split: tree.split)
nipkow
parents: 66492
diff changeset
   114
nipkow
parents: 66492
diff changeset
   115
lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
nipkow
parents: 66492
diff changeset
   116
by (auto simp: link_def split: tree.split)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   117
    
66524
nipkow
parents: 66492
diff changeset
   118
lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
nipkow
parents: 66492
diff changeset
   119
by (auto simp: link_def split: tree.split)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   120
    
66524
nipkow
parents: 66492
diff changeset
   121
subsubsection \<open>\<open>ins_tree\<close>\<close>
nipkow
parents: 66492
diff changeset
   122
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   123
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
   124
  "ins_tree t [] = [t]"
66524
nipkow
parents: 66492
diff changeset
   125
| "ins_tree t\<^sub>1 (t\<^sub>2#ts) =
nipkow
parents: 66492
diff changeset
   126
  (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)"  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   127
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   128
lemma invar_bheap_Cons[simp]: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   129
  "invar_bheap (t#ts) 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   130
  \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
66524
nipkow
parents: 66492
diff changeset
   131
by (auto simp: sorted_wrt_Cons invar_bheap_def)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   132
  
66524
nipkow
parents: 66492
diff changeset
   133
lemma invar_btree_ins_tree:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   134
  assumes "invar_btree t" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   135
  assumes "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   136
  assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   137
  shows "invar_bheap (ins_tree t ts)"  
66524
nipkow
parents: 66492
diff changeset
   138
using assms
nipkow
parents: 66492
diff changeset
   139
by (induction t ts rule: ins_tree.induct) (auto simp: invar_btree_link less_eq_Suc_le[symmetric])
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   140
    
66524
nipkow
parents: 66492
diff changeset
   141
lemma invar_oheap_Cons[simp]: 
nipkow
parents: 66492
diff changeset
   142
  "invar_oheap (t#ts) \<longleftrightarrow> invar_otree t \<and> invar_oheap ts"    
nipkow
parents: 66492
diff changeset
   143
by (auto simp: invar_oheap_def)
nipkow
parents: 66492
diff changeset
   144
nipkow
parents: 66492
diff changeset
   145
lemma invar_oheap_ins_tree:
nipkow
parents: 66492
diff changeset
   146
  assumes "invar_otree t" 
nipkow
parents: 66492
diff changeset
   147
  assumes "invar_oheap ts"
nipkow
parents: 66492
diff changeset
   148
  shows "invar_oheap (ins_tree t ts)"  
nipkow
parents: 66492
diff changeset
   149
using assms  
nipkow
parents: 66492
diff changeset
   150
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   151
    
66524
nipkow
parents: 66492
diff changeset
   152
lemma mset_heap_ins_tree[simp]: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   153
  "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"    
66524
nipkow
parents: 66492
diff changeset
   154
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
   155
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   156
lemma ins_tree_rank_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   157
  assumes "t' \<in> set (ins_tree t ts)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   158
  assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   159
  assumes "rank t\<^sub>0 < rank t"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   160
  shows "rank t\<^sub>0 < rank t'"
66524
nipkow
parents: 66492
diff changeset
   161
using assms  
nipkow
parents: 66492
diff changeset
   162
by (induction t ts rule: ins_tree.induct) (auto split: if_splits)
nipkow
parents: 66492
diff changeset
   163
nipkow
parents: 66492
diff changeset
   164
subsubsection \<open>\<open>insert\<close>\<close>
nipkow
parents: 66492
diff changeset
   165
nipkow
parents: 66492
diff changeset
   166
hide_const (open) insert
nipkow
parents: 66492
diff changeset
   167
nipkow
parents: 66492
diff changeset
   168
definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
nipkow
parents: 66492
diff changeset
   169
"insert x ts = ins_tree (Node 0 x []) ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   170
  
66524
nipkow
parents: 66492
diff changeset
   171
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)"
nipkow
parents: 66492
diff changeset
   172
by (auto intro!: invar_btree_ins_tree simp: invar_oheap_ins_tree insert_def invar_def)  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   173
    
66524
nipkow
parents: 66492
diff changeset
   174
lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"
nipkow
parents: 66492
diff changeset
   175
by(auto simp: insert_def)
nipkow
parents: 66492
diff changeset
   176
nipkow
parents: 66492
diff changeset
   177
subsubsection \<open>\<open>merge\<close>\<close>
66492
nipkow
parents: 66436
diff changeset
   178
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   179
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
   180
  "merge ts\<^sub>1 [] = ts\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   181
| "merge [] ts\<^sub>2 = ts\<^sub>2"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   182
| "merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = (
66492
nipkow
parents: 66436
diff changeset
   183
    if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2) else
nipkow
parents: 66436
diff changeset
   184
    if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   185
    else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
66492
nipkow
parents: 66436
diff changeset
   186
  )"
nipkow
parents: 66436
diff changeset
   187
66524
nipkow
parents: 66492
diff changeset
   188
lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2"
nipkow
parents: 66492
diff changeset
   189
by (cases ts\<^sub>2) auto
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   190
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   191
lemma merge_rank_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   192
  assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   193
  assumes "\<forall>t'\<in>set ts\<^sub>1. rank t < rank t'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   194
  assumes "\<forall>t'\<in>set ts\<^sub>2. rank t < rank t'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   195
  shows "rank t < rank t'"
66524
nipkow
parents: 66492
diff changeset
   196
using assms
nipkow
parents: 66492
diff changeset
   197
by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
nipkow
parents: 66492
diff changeset
   198
   (auto split: if_splits simp: ins_tree_rank_bound)
nipkow
parents: 66492
diff changeset
   199
nipkow
parents: 66492
diff changeset
   200
lemma invar_bheap_merge:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   201
  assumes "invar_bheap ts\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   202
  assumes "invar_bheap ts\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   203
  shows "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
   204
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   205
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
   206
  case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   207
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   208
  from "3.prems" have [simp]: "invar_btree t\<^sub>1" "invar_btree t\<^sub>2"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   209
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   210
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   211
  consider (LT) "rank t\<^sub>1 < rank t\<^sub>2" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   212
         | (GT) "rank t\<^sub>1 > rank t\<^sub>2" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   213
         | (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
   214
    using antisym_conv3 by blast
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   215
  then show ?case proof cases
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   216
    case LT
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   217
    then show ?thesis using 3
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   218
      by (force elim!: merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   219
  next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   220
    case GT
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   221
    then show ?thesis using 3
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   222
      by (force elim!: merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   223
  next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   224
    case [simp]: EQ
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   225
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   226
    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
   227
      by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   228
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   229
    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
   230
      using that
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   231
      apply (rule merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   232
      using "3.prems" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   233
    with EQ show ?thesis
66524
nipkow
parents: 66492
diff changeset
   234
      by (auto simp: Suc_le_eq invar_btree_ins_tree invar_btree_link)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   235
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   236
qed simp_all
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   237
  
66524
nipkow
parents: 66492
diff changeset
   238
lemma invar_oheap_merge:
nipkow
parents: 66492
diff changeset
   239
  assumes "invar_oheap ts\<^sub>1"
nipkow
parents: 66492
diff changeset
   240
  assumes "invar_oheap ts\<^sub>2"
nipkow
parents: 66492
diff changeset
   241
  shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)"  
nipkow
parents: 66492
diff changeset
   242
using assms
nipkow
parents: 66492
diff changeset
   243
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
nipkow
parents: 66492
diff changeset
   244
   (auto simp: invar_oheap_ins_tree invar_link_otree)  
nipkow
parents: 66492
diff changeset
   245
 
nipkow
parents: 66492
diff changeset
   246
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: 66492
diff changeset
   247
by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   248
    
66524
nipkow
parents: 66492
diff changeset
   249
lemma mset_heap_merge[simp]: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   250
  "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
66524
nipkow
parents: 66492
diff changeset
   251
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   252
    
66524
nipkow
parents: 66492
diff changeset
   253
subsubsection \<open>\<open>get_min\<close>\<close>
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   254
66524
nipkow
parents: 66492
diff changeset
   255
fun get_min :: "'a::linorder heap \<Rightarrow> 'a" where
nipkow
parents: 66492
diff changeset
   256
  "get_min [t] = root t"
nipkow
parents: 66492
diff changeset
   257
| "get_min (t#ts) = (let x = root t; 
nipkow
parents: 66492
diff changeset
   258
                          y = get_min ts
nipkow
parents: 66492
diff changeset
   259
                      in if x \<le> y then x else y)"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   260
  
66524
nipkow
parents: 66492
diff changeset
   261
lemma invar_otree_root_min:
nipkow
parents: 66492
diff changeset
   262
  assumes "invar_otree t"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   263
  assumes "x \<in># mset_tree t" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   264
  shows "root t \<le> x"  
66524
nipkow
parents: 66492
diff changeset
   265
using assms
nipkow
parents: 66492
diff changeset
   266
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def)
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
lemma get_min_mset_aux: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   269
  assumes "ts\<noteq>[]"    
66524
nipkow
parents: 66492
diff changeset
   270
  assumes "invar_oheap ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   271
  assumes "x \<in># mset_heap ts"  
66524
nipkow
parents: 66492
diff changeset
   272
  shows "get_min ts \<le> x"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   273
  using assms  
66524
nipkow
parents: 66492
diff changeset
   274
apply (induction ts arbitrary: x rule: get_min.induct)  
nipkow
parents: 66492
diff changeset
   275
apply (auto 
nipkow
parents: 66492
diff changeset
   276
      simp: invar_otree_root_min intro: order_trans;
nipkow
parents: 66492
diff changeset
   277
      meson linear order_trans invar_otree_root_min
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   278
      )+
66524
nipkow
parents: 66492
diff changeset
   279
done  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   280
66524
nipkow
parents: 66492
diff changeset
   281
lemma get_min_mset: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   282
  assumes "ts\<noteq>[]"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   283
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   284
  assumes "x \<in># mset_heap ts"  
66524
nipkow
parents: 66492
diff changeset
   285
  shows "get_min ts \<le> x"
nipkow
parents: 66492
diff changeset
   286
using assms by (auto simp: invar_def get_min_mset_aux)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   287
66524
nipkow
parents: 66492
diff changeset
   288
lemma get_min_member:    
nipkow
parents: 66492
diff changeset
   289
  "ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"  
nipkow
parents: 66492
diff changeset
   290
by (induction ts rule: get_min.induct) (auto)
nipkow
parents: 66492
diff changeset
   291
nipkow
parents: 66492
diff changeset
   292
lemma get_min:    
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   293
  assumes "mset_heap ts \<noteq> {#}"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   294
  assumes "invar ts"
66524
nipkow
parents: 66492
diff changeset
   295
  shows "get_min ts = Min_mset (mset_heap ts)"
nipkow
parents: 66492
diff changeset
   296
using assms get_min_member get_min_mset  
nipkow
parents: 66492
diff changeset
   297
by (auto simp: eq_Min_iff)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   298
    
66524
nipkow
parents: 66492
diff changeset
   299
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
   300
66524
nipkow
parents: 66492
diff changeset
   301
fun get_min_rest :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where
nipkow
parents: 66492
diff changeset
   302
  "get_min_rest [t] = (t,[])"
nipkow
parents: 66492
diff changeset
   303
| "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
   304
                     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
   305
66524
nipkow
parents: 66492
diff changeset
   306
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
   307
  assumes "ts\<noteq>[]"
66524
nipkow
parents: 66492
diff changeset
   308
  assumes "get_min_rest ts = (t',ts')"  
nipkow
parents: 66492
diff changeset
   309
  shows "root t' = get_min ts"  
nipkow
parents: 66492
diff changeset
   310
using assms  
nipkow
parents: 66492
diff changeset
   311
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits)
nipkow
parents: 66492
diff changeset
   312
nipkow
parents: 66492
diff changeset
   313
lemma mset_get_min_rest:    
nipkow
parents: 66492
diff changeset
   314
  assumes "get_min_rest ts = (t',ts')"  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   315
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   316
  shows "mset ts = {#t'#} + mset ts'"  
66524
nipkow
parents: 66492
diff changeset
   317
using assms  
nipkow
parents: 66492
diff changeset
   318
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   319
    
66524
nipkow
parents: 66492
diff changeset
   320
lemma set_get_min_rest:
nipkow
parents: 66492
diff changeset
   321
  assumes "get_min_rest ts = (t', ts')" 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   322
  assumes "ts\<noteq>[]"
66524
nipkow
parents: 66492
diff changeset
   323
  shows "set ts = Set.insert t' (set ts')"
nipkow
parents: 66492
diff changeset
   324
using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]]
nipkow
parents: 66492
diff changeset
   325
by auto  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   326
66524
nipkow
parents: 66492
diff changeset
   327
lemma invar_bheap_get_min_rest:    
nipkow
parents: 66492
diff changeset
   328
  assumes "get_min_rest ts = (t',ts')"  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   329
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   330
  assumes "invar_bheap ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   331
  shows "invar_btree t'" and "invar_bheap ts'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   332
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   333
  have "invar_btree t' \<and> invar_bheap ts'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   334
    using assms  
66524
nipkow
parents: 66492
diff changeset
   335
    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
   336
      case (2 t v va)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   337
      then show ?case
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   338
        apply (clarsimp split: prod.splits if_splits)
66524
nipkow
parents: 66492
diff changeset
   339
        apply (drule set_get_min_rest; fastforce)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   340
        done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   341
    qed auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   342
  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
   343
qed
66524
nipkow
parents: 66492
diff changeset
   344
nipkow
parents: 66492
diff changeset
   345
lemma invar_oheap_get_min_rest:    
nipkow
parents: 66492
diff changeset
   346
  assumes "get_min_rest ts = (t',ts')"  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   347
  assumes "ts\<noteq>[]"
66524
nipkow
parents: 66492
diff changeset
   348
  assumes "invar_oheap ts"  
nipkow
parents: 66492
diff changeset
   349
  shows "invar_otree t'" and "invar_oheap ts'"
nipkow
parents: 66492
diff changeset
   350
using assms  
nipkow
parents: 66492
diff changeset
   351
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
nipkow
parents: 66492
diff changeset
   352
nipkow
parents: 66492
diff changeset
   353
subsubsection \<open>\<open>del_min\<close>\<close>
nipkow
parents: 66492
diff changeset
   354
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   355
definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
66524
nipkow
parents: 66492
diff changeset
   356
"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
   357
   (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   358
  
66524
nipkow
parents: 66492
diff changeset
   359
lemma invar_del_min[simp]:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   360
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   361
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   362
  shows "invar (del_min ts)"
66524
nipkow
parents: 66492
diff changeset
   363
using assms  
nipkow
parents: 66492
diff changeset
   364
unfolding invar_def del_min_def  
nipkow
parents: 66492
diff changeset
   365
by (auto 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   366
      split: prod.split tree.split 
66524
nipkow
parents: 66492
diff changeset
   367
      intro!: invar_bheap_merge invar_oheap_merge
nipkow
parents: 66492
diff changeset
   368
      dest: invar_bheap_get_min_rest invar_oheap_get_min_rest
nipkow
parents: 66492
diff changeset
   369
      intro!: invar_oheap_children invar_bheap_children
nipkow
parents: 66492
diff changeset
   370
    )
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   371
    
66524
nipkow
parents: 66492
diff changeset
   372
lemma mset_heap_del_min: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   373
  assumes "ts \<noteq> []"
66524
nipkow
parents: 66492
diff changeset
   374
  shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}"
nipkow
parents: 66492
diff changeset
   375
using assms
nipkow
parents: 66492
diff changeset
   376
unfolding del_min_def
nipkow
parents: 66492
diff changeset
   377
apply (clarsimp split: tree.split prod.split)
nipkow
parents: 66492
diff changeset
   378
apply (frule (1) get_min_rest_get_min_same_root)  
nipkow
parents: 66492
diff changeset
   379
apply (frule (1) mset_get_min_rest)  
nipkow
parents: 66492
diff changeset
   380
apply (auto simp: mset_heap_def)
nipkow
parents: 66492
diff changeset
   381
done  
nipkow
parents: 66492
diff changeset
   382
nipkow
parents: 66492
diff changeset
   383
nipkow
parents: 66492
diff changeset
   384
subsubsection \<open>Instantiating the Priority Queue Locale\<close>
nipkow
parents: 66492
diff changeset
   385
nipkow
parents: 66492
diff changeset
   386
interpretation binheap: Priority_Queue
nipkow
parents: 66492
diff changeset
   387
  where empty = "[]" and is_empty = "op = []" and insert = insert
nipkow
parents: 66492
diff changeset
   388
  and get_min = get_min and del_min = del_min
nipkow
parents: 66492
diff changeset
   389
  and invar = invar and mset = mset_heap
nipkow
parents: 66492
diff changeset
   390
proof (unfold_locales, goal_cases)
nipkow
parents: 66492
diff changeset
   391
  case 1
nipkow
parents: 66492
diff changeset
   392
  then show ?case by simp
nipkow
parents: 66492
diff changeset
   393
next
nipkow
parents: 66492
diff changeset
   394
  case (2 q)
nipkow
parents: 66492
diff changeset
   395
  then show ?case by auto
nipkow
parents: 66492
diff changeset
   396
next
nipkow
parents: 66492
diff changeset
   397
  case (3 q x)
nipkow
parents: 66492
diff changeset
   398
  then show ?case by auto
nipkow
parents: 66492
diff changeset
   399
next
nipkow
parents: 66492
diff changeset
   400
  case (4 q)
nipkow
parents: 66492
diff changeset
   401
  then show ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>] 
nipkow
parents: 66492
diff changeset
   402
    by (auto simp: union_single_eq_diff)
nipkow
parents: 66492
diff changeset
   403
next
nipkow
parents: 66492
diff changeset
   404
  case (5 q)
nipkow
parents: 66492
diff changeset
   405
  then show ?case using get_min[of q] by auto
nipkow
parents: 66492
diff changeset
   406
next 
nipkow
parents: 66492
diff changeset
   407
  case 6 
nipkow
parents: 66492
diff changeset
   408
  then show ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
nipkow
parents: 66492
diff changeset
   409
next
nipkow
parents: 66492
diff changeset
   410
  case (7 q x)
nipkow
parents: 66492
diff changeset
   411
  then show ?case by simp
nipkow
parents: 66492
diff changeset
   412
next
nipkow
parents: 66492
diff changeset
   413
  case (8 q)
nipkow
parents: 66492
diff changeset
   414
  then show ?case by simp
nipkow
parents: 66492
diff changeset
   415
qed
nipkow
parents: 66492
diff changeset
   416
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   417
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   418
subsection \<open>Complexity\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   419
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   420
text \<open>The size of a binomial tree is determined by its rank\<close>  
66524
nipkow
parents: 66492
diff changeset
   421
lemma size_mset_btree:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   422
  assumes "invar_btree t"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   423
  shows "size (mset_tree t) = 2^rank t"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   424
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   425
proof (induction t)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   426
  case (Node r v ts)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   427
  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
   428
    using that by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   429
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   430
  from Node have COMPL: "map rank ts = rev [0..<r]" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   431
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   432
  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
   433
    by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   434
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   435
    by (auto cong: sum_list_cong)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   436
  also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   437
    by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   438
  also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   439
    unfolding COMPL 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   440
    by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   441
  also have "\<dots> = 2^r - 1" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   442
    by (induction r) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   443
  finally show ?case 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   444
    by (simp)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   445
qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   446
   
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   447
text \<open>The length of a binomial heap is bounded by the number of its elements\<close>  
66524
nipkow
parents: 66492
diff changeset
   448
lemma size_mset_heap:      
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   449
  assumes "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   450
  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
   451
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   452
  from \<open>invar_bheap ts\<close> have 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   453
    ASC: "sorted_wrt (op <) (map rank ts)" and
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   454
    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
   455
    unfolding invar_bheap_def by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   456
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   457
  have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   458
    by (simp add: sum_power2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   459
  also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   460
    using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "op ^ (2::nat)"]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   461
    using power_increasing[where a="2::nat"]  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   462
    by (auto simp: o_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   463
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV   
66524
nipkow
parents: 66492
diff changeset
   464
    by (auto cong: sum_list_cong simp: size_mset_btree)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   465
  also have "\<dots> = size (mset_heap ts) + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   466
    unfolding mset_heap_def by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   467
  finally show ?thesis .
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   468
qed      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   469
  
66524
nipkow
parents: 66492
diff changeset
   470
subsubsection \<open>Timing Functions\<close>
nipkow
parents: 66492
diff changeset
   471
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   472
text \<open>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   473
  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
   474
  estimations of their complexity.
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   475
\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   476
definition t_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   477
[simp]: "t_link _ _ = 1"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   478
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   479
fun t_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   480
  "t_ins_tree t [] = 1"
66524
nipkow
parents: 66492
diff changeset
   481
| "t_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = (
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   482
    (if rank t\<^sub>1 < rank t\<^sub>2 then 1 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   483
     else t_link t\<^sub>1 t\<^sub>2 + t_ins_tree (link t\<^sub>1 t\<^sub>2) rest)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   484
  )"  
66524
nipkow
parents: 66492
diff changeset
   485
nipkow
parents: 66492
diff changeset
   486
definition t_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
nipkow
parents: 66492
diff changeset
   487
"t_insert x ts = t_ins_tree (Node 0 x []) ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   488
66524
nipkow
parents: 66492
diff changeset
   489
lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1"
nipkow
parents: 66492
diff changeset
   490
by (induction t ts rule: t_ins_tree.induct) auto
nipkow
parents: 66492
diff changeset
   491
nipkow
parents: 66492
diff changeset
   492
subsubsection \<open>\<open>t_insert\<close>\<close>
nipkow
parents: 66492
diff changeset
   493
nipkow
parents: 66492
diff changeset
   494
lemma t_insert_bound: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   495
  assumes "invar ts"
66524
nipkow
parents: 66492
diff changeset
   496
  shows "t_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   497
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   498
66524
nipkow
parents: 66492
diff changeset
   499
  have 1: "t_insert x ts \<le> length ts + 1" 
nipkow
parents: 66492
diff changeset
   500
    unfolding t_insert_def by (rule t_ins_tree_simple_bound)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   501
  also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   502
  proof -
66524
nipkow
parents: 66492
diff changeset
   503
    from size_mset_heap[of ts] assms 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   504
    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
   505
      unfolding invar_def by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   506
    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
   507
    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
   508
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   509
  finally show ?thesis 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   510
    by (simp only: log_mult of_nat_mult) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   511
qed      
66524
nipkow
parents: 66492
diff changeset
   512
nipkow
parents: 66492
diff changeset
   513
subsubsection \<open>\<open>t_merge\<close>\<close>
nipkow
parents: 66492
diff changeset
   514
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   515
fun t_merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> nat" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   516
  "t_merge ts\<^sub>1 [] = 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   517
| "t_merge [] ts\<^sub>2 = 1"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   518
| "t_merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = 1 + (
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   519
    if rank t\<^sub>1 < rank t\<^sub>2 then t_merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   520
    else if rank t\<^sub>2 < rank t\<^sub>1 then t_merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   521
    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
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   522
  )"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   523
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   524
text \<open>A crucial idea is to estimate the time in correlation with the 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   525
  result length, as each carry reduces the length of the result.\<close>  
66524
nipkow
parents: 66492
diff changeset
   526
nipkow
parents: 66492
diff changeset
   527
lemma t_ins_tree_length:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   528
  "t_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   529
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
   530
66524
nipkow
parents: 66492
diff changeset
   531
lemma t_merge_length: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   532
  "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"
66524
nipkow
parents: 66492
diff changeset
   533
by (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct)  
nipkow
parents: 66492
diff changeset
   534
   (auto simp: t_ins_tree_length algebra_simps)
nipkow
parents: 66492
diff changeset
   535
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   536
text \<open>Finally, we get the desired logarithmic bound\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   537
lemma t_merge_bound_aux:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   538
  fixes ts\<^sub>1 ts\<^sub>2
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   539
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   540
  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
   541
  assumes BINVARS: "invar_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   542
  shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   543
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   544
  define n where "n = n\<^sub>1 + n\<^sub>2"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   545
      
66524
nipkow
parents: 66492
diff changeset
   546
  from t_merge_length[of ts\<^sub>1 ts\<^sub>2] 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   547
  have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   548
  hence "(2::nat)^t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   549
    by (rule power_increasing) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   550
  also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   551
    by (auto simp: algebra_simps power_add power_mult)
66524
nipkow
parents: 66492
diff changeset
   552
  also note BINVARS(1)[THEN size_mset_heap]
nipkow
parents: 66492
diff changeset
   553
  also note BINVARS(2)[THEN size_mset_heap]
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   554
  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" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   555
    by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   556
  from le_log2_of_power[OF this] have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   557
    by simp
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   558
  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
   559
    by (simp add: log_mult log_nat_power)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   560
  also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   561
  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)"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   562
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   563
  also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   564
  finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   565
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   566
  also have "log 2 2 \<le> 2" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   567
  finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   568
  thus ?thesis unfolding n_def by (auto simp: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   569
qed      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   570
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   571
lemma t_merge_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   572
  fixes ts\<^sub>1 ts\<^sub>2
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   573
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   574
  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
   575
  assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   576
  shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   577
using assms t_merge_bound_aux unfolding invar_def by blast  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   578
66524
nipkow
parents: 66492
diff changeset
   579
subsubsection \<open>\<open>t_get_min\<close>\<close>
nipkow
parents: 66492
diff changeset
   580
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   581
fun t_get_min :: "'a::linorder heap \<Rightarrow> nat" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   582
  "t_get_min [t] = 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   583
| "t_get_min (t#ts) = 1 + t_get_min ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   584
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   585
lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts"  
66524
nipkow
parents: 66492
diff changeset
   586
by (induction ts rule: t_get_min.induct) auto
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   587
  
66524
nipkow
parents: 66492
diff changeset
   588
lemma t_get_min_bound: 
nipkow
parents: 66492
diff changeset
   589
  assumes "invar ts"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   590
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   591
  shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   592
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   593
  have 1: "t_get_min ts = length ts" using assms t_get_min_estimate by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   594
  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
   595
  proof -
66524
nipkow
parents: 66492
diff changeset
   596
    from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
nipkow
parents: 66492
diff changeset
   597
      unfolding invar_def by auto
nipkow
parents: 66492
diff changeset
   598
    thus ?thesis using le_log2_of_power by blast
nipkow
parents: 66492
diff changeset
   599
  qed
nipkow
parents: 66492
diff changeset
   600
  finally show ?thesis by auto 
nipkow
parents: 66492
diff changeset
   601
qed  
nipkow
parents: 66492
diff changeset
   602
nipkow
parents: 66492
diff changeset
   603
subsubsection \<open>\<open>t_del_min\<close>\<close>
nipkow
parents: 66492
diff changeset
   604
nipkow
parents: 66492
diff changeset
   605
fun t_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where
nipkow
parents: 66492
diff changeset
   606
  "t_get_min_rest [t] = 1"
nipkow
parents: 66492
diff changeset
   607
| "t_get_min_rest (t#ts) = 1 + t_get_min_rest ts"
nipkow
parents: 66492
diff changeset
   608
nipkow
parents: 66492
diff changeset
   609
lemma t_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min_rest ts = length ts"  
nipkow
parents: 66492
diff changeset
   610
  by (induction ts rule: t_get_min_rest.induct) auto
nipkow
parents: 66492
diff changeset
   611
  
nipkow
parents: 66492
diff changeset
   612
lemma t_get_min_rest_bound_aux: 
nipkow
parents: 66492
diff changeset
   613
  assumes "invar_bheap ts"
nipkow
parents: 66492
diff changeset
   614
  assumes "ts\<noteq>[]"
nipkow
parents: 66492
diff changeset
   615
  shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
nipkow
parents: 66492
diff changeset
   616
proof -
nipkow
parents: 66492
diff changeset
   617
  have 1: "t_get_min_rest ts = length ts" using assms t_get_min_rest_estimate by auto
nipkow
parents: 66492
diff changeset
   618
  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
nipkow
parents: 66492
diff changeset
   619
  proof -
nipkow
parents: 66492
diff changeset
   620
    from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   621
      by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   622
    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
   623
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   624
  finally show ?thesis by auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   625
qed  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   626
66524
nipkow
parents: 66492
diff changeset
   627
lemma t_get_min_rest_bound: 
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   628
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   629
  assumes "ts\<noteq>[]"
66524
nipkow
parents: 66492
diff changeset
   630
  shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
nipkow
parents: 66492
diff changeset
   631
using assms t_get_min_rest_bound_aux unfolding invar_def by blast  
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   632
66524
nipkow
parents: 66492
diff changeset
   633
text\<open>Note that although the definition of function @{const rev} has quadratic complexity,
nipkow
parents: 66492
diff changeset
   634
it can and is implemented (via suitable code lemmas) as a linear time function.
nipkow
parents: 66492
diff changeset
   635
Thus the following definition is justified:\<close>
nipkow
parents: 66492
diff changeset
   636
nipkow
parents: 66492
diff changeset
   637
definition "t_rev xs = length xs + 1"
nipkow
parents: 66492
diff changeset
   638
nipkow
parents: 66492
diff changeset
   639
definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" where
nipkow
parents: 66492
diff changeset
   640
  "t_del_min ts = t_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   641
                    \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   642
  )"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   643
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   644
lemma t_rev_ts1_bound_aux: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   645
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   646
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   647
  assumes BINVAR: "invar_bheap (rev ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   648
  shows "t_rev ts \<le> 1 + log 2 (n+1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   649
proof -
66524
nipkow
parents: 66492
diff changeset
   650
  have "t_rev ts = length ts + 1" by (auto simp: t_rev_def)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   651
  hence "2^t_rev ts = 2*2^length ts" by auto
66524
nipkow
parents: 66492
diff changeset
   652
  also have "\<dots> \<le> 2*n+2" using size_mset_heap[OF BINVAR] by (auto simp: n_def)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   653
  finally have "2 ^ t_rev ts \<le> 2 * n + 2" .
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   654
  from le_log2_of_power[OF this] have "t_rev ts \<le> log 2 (2 * (n + 1))"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   655
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   656
  also have "\<dots> = 1 + log 2 (n+1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   657
    by (simp only: of_nat_mult log_mult) auto  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   658
  finally show ?thesis by (auto simp: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   659
qed    
66524
nipkow
parents: 66492
diff changeset
   660
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   661
lemma t_del_min_bound_aux:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   662
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   663
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   664
  assumes BINVAR: "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   665
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   666
  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   667
proof -
66524
nipkow
parents: 66492
diff changeset
   668
  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
   669
    by (metis surj_pair tree.exhaust_sel)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   670
66524
nipkow
parents: 66492
diff changeset
   671
  note BINVAR' = invar_bheap_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
nipkow
parents: 66492
diff changeset
   672
  hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: invar_bheap_children)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   673
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   674
  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
   675
  define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   676
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   677
  have t_rev_ts1_bound: "t_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   678
  proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   679
    note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   680
    also have "n\<^sub>1 \<le> n" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   681
      unfolding n\<^sub>1_def n_def
66524
nipkow
parents: 66492
diff changeset
   682
      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
   683
      by (auto simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   684
    finally show ?thesis by (auto simp: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   685
  qed    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   686
    
66524
nipkow
parents: 66492
diff changeset
   687
  have "t_del_min ts = t_get_min_rest ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   688
    unfolding t_del_min_def by (simp add: GM)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   689
  also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
66524
nipkow
parents: 66492
diff changeset
   690
    using t_get_min_rest_bound_aux[OF assms(2-)] by (auto simp: n_def)
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   691
  also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   692
    using t_rev_ts1_bound by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   693
  also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   694
    using t_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   695
    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
   696
  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
   697
    unfolding n\<^sub>1_def n\<^sub>2_def n_def
66524
nipkow
parents: 66492
diff changeset
   698
    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
   699
    by (auto simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   700
  finally have "t_del_min ts \<le> 6 * log 2 (n+1) + 3" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   701
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   702
  thus ?thesis by (simp add: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   703
qed      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   704
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   705
lemma t_del_min_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   706
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   707
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   708
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   709
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   710
  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"  
66524
nipkow
parents: 66492
diff changeset
   711
using assms t_del_min_bound_aux unfolding invar_def by blast
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   712
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   713
end