src/HOL/Data_Structures/Binomial_Heap.thy
author nipkow
Tue, 15 Aug 2017 19:47:08 +0200
changeset 66436 5d7e770c7d5d
child 66492 78a009ac91d2
permissions -rw-r--r--
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66436
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     1
(* Author: Peter Lammich *)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     2
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     3
section \<open>Binomial Heap\<close>
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
theory Binomial_Heap
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     6
imports
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     7
  Complex_Main
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     8
  Priority_Queue
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
     9
begin
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    10
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    11
lemma sum_power2: "(\<Sum>i\<in>{0..<k}. (2::nat)^i) = 2^k-1"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    12
by (induction k) auto
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> {#}"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    42
  by (cases t) auto
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 [] = {#}"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    46
  unfolding mset_heap_def 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    47
  by auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    48
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    49
lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    50
  unfolding mset_heap_def by auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    51
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    52
lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    53
  unfolding mset_heap_def by auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    54
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    55
lemma root_in_mset[simp]: "root t \<in># mset_tree t" by (cases t) auto    
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"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    58
  unfolding mset_heap_def by auto
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>  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    63
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    64
  where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    65
    "invar_btree (Node r x ts) \<longleftrightarrow> 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    66
      (\<forall>t\<in>set ts. invar_btree t) 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    67
    \<and> (map rank ts = rev [0..<r])"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    68
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    69
definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    70
  "invar_bheap ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    71
  \<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
    72
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    73
text \<open>Ordering (heap) invariant\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    74
fun otree_invar :: "'a::linorder tree \<Rightarrow> bool"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    75
  where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    76
    "otree_invar (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. otree_invar t \<and> x \<le> root t)"
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 oheap_invar :: "'a::linorder heap \<Rightarrow> bool" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    79
  "oheap_invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. otree_invar t)"
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
definition invar :: "'a::linorder heap \<Rightarrow> bool" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    82
  "invar ts \<longleftrightarrow> invar_bheap ts \<and> oheap_invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    83
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    84
text \<open>The children of a node are a valid heap\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    85
lemma children_oheap_invar: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    86
  "otree_invar (Node r v ts) \<Longrightarrow> oheap_invar (rev ts)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    87
  by (auto simp: oheap_invar_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    88
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    89
lemma children_invar_bheap: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    90
  "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    91
  by (auto simp: invar_bheap_def rev_map[symmetric])
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    92
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    93
subsection \<open>Operations\<close>  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    94
    
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
  )"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
    99
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   100
lemma link_invar_btree:
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)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   105
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   106
  unfolding link_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   107
  by (force split: tree.split )
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   108
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   109
lemma link_otree_invar:      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   110
  assumes "otree_invar t\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   111
  assumes "otree_invar t\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   112
  shows "otree_invar (link t\<^sub>1 t\<^sub>2)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   113
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   114
  unfolding link_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   115
  by (auto split: tree.split)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   116
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   117
lemma link_rank[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   118
  unfolding link_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   119
  by (auto split: tree.split)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   120
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   121
lemma link_mset[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   122
  unfolding link_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   123
  by (auto split: tree.split)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   124
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   125
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
   126
  "ins_tree t [] = [t]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   127
| "ins_tree t\<^sub>1 (t\<^sub>2#ts) = (
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   128
    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
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   129
  )"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   130
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   131
lemma invar_bheap_Cons[simp]: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   132
  "invar_bheap (t#ts) 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   133
  \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   134
  unfolding invar_bheap_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   135
  by (auto simp: sorted_wrt_Cons)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   136
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   137
lemma ins_tree_invar_btree:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   138
  assumes "invar_btree t" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   139
  assumes "invar_bheap ts"
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 \<le> rank t'"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   141
  shows "invar_bheap (ins_tree t ts)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   142
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   143
  apply (induction t ts rule: ins_tree.induct)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   144
  apply (auto simp: link_invar_btree less_eq_Suc_le[symmetric])
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   145
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   146
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   147
lemma oheap_invar_Cons[simp]: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   148
  "oheap_invar (t#ts) \<longleftrightarrow> otree_invar t \<and> oheap_invar ts"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   149
  unfolding oheap_invar_def by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   150
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   151
lemma ins_tree_otree_invar:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   152
  assumes "otree_invar t" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   153
  assumes "oheap_invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   154
  shows "oheap_invar (ins_tree t ts)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   155
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   156
  apply (induction t ts rule: ins_tree.induct)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   157
  apply (auto simp: link_otree_invar)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   158
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   159
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   160
lemma ins_tree_mset[simp]: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   161
  "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   162
  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
   163
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   164
lemma ins_tree_rank_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   165
  assumes "t' \<in> set (ins_tree t ts)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   166
  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
   167
  assumes "rank t\<^sub>0 < rank t"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   168
  shows "rank t\<^sub>0 < rank t'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   169
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   170
  by (induction t ts rule: ins_tree.induct) (auto split: if_splits)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   171
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   172
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   173
definition ins :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   174
  "ins x ts = ins_tree (Node 0 x []) ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   175
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   176
lemma ins_invar[simp]: "invar t \<Longrightarrow> invar (ins x t)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   177
  unfolding ins_def invar_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   178
  by (auto intro!: ins_tree_invar_btree simp: ins_tree_otree_invar)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   179
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   180
lemma ins_mset[simp]: "mset_heap (ins x t) = {#x#} + mset_heap t"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   181
  unfolding ins_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   182
  by auto  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   183
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   184
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
   185
  "merge ts\<^sub>1 [] = ts\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   186
| "merge [] ts\<^sub>2 = ts\<^sub>2"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   187
| "merge (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
   188
    if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#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
   189
    else if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2#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
   190
    else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   191
  )"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   192
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   193
lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" by (cases ts\<^sub>2) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   194
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   195
lemma merge_rank_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   196
  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
   197
  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
   198
  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
   199
  shows "rank t < rank t'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   200
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   201
  apply (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   202
  apply (auto split: if_splits simp: ins_tree_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   203
  done
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   204
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   205
lemma merge_invar_bheap:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   206
  assumes "invar_bheap ts\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   207
  assumes "invar_bheap ts\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   208
  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
   209
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   210
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
   211
  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
   212
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   213
  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
   214
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   215
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   216
  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
   217
         | (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
   218
         | (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
   219
    using antisym_conv3 by blast
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   220
  then show ?case proof cases
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   221
    case LT
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   222
    then show ?thesis using 3
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   223
      by (force elim!: merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   224
  next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   225
    case GT
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   226
    then show ?thesis using 3
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   227
      by (force elim!: merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   228
  next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   229
    case [simp]: EQ
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   230
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   231
    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
   232
      by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   233
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   234
    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
   235
      using that
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   236
      apply (rule merge_rank_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   237
      using "3.prems" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   238
    with EQ show ?thesis
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   239
      by (auto simp: Suc_le_eq ins_tree_invar_btree link_invar_btree)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   240
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   241
qed simp_all
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   242
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   243
lemma merge_oheap_invar:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   244
  assumes "oheap_invar ts\<^sub>1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   245
  assumes "oheap_invar ts\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   246
  shows "oheap_invar (merge ts\<^sub>1 ts\<^sub>2)"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   247
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   248
  apply (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
   249
  apply (auto simp: ins_tree_otree_invar link_otree_invar)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   250
  done
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   251
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   252
lemma merge_invar[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   253
  unfolding invar_def by (auto simp: merge_invar_bheap merge_oheap_invar)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   254
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   255
lemma merge_mset[simp]: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   256
  "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   257
  by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   258
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   259
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   260
fun find_min :: "'a::linorder heap \<Rightarrow> 'a" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   261
  "find_min [t] = root t"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   262
| "find_min (t#ts) = (let x=root t; 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   263
                          y=find_min ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   264
                      in if x\<le>y then x else y)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   265
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   266
lemma otree_invar_root_min:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   267
  assumes "otree_invar t"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   268
  assumes "x \<in># mset_tree t" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   269
  shows "root t \<le> x"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   270
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   271
  apply (induction t arbitrary: x rule: mset_tree.induct)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   272
  apply (force simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   273
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   274
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   275
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   276
lemma find_min_mset_aux: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   277
  assumes "ts\<noteq>[]"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   278
  assumes "oheap_invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   279
  assumes "x \<in># mset_heap ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   280
  shows "find_min ts \<le> x"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   281
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   282
  apply (induction ts arbitrary: x rule: find_min.induct)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   283
  apply (auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   284
      simp: Let_def otree_invar_root_min intro: order_trans;
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   285
      meson linear order_trans otree_invar_root_min
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   286
      )+
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   287
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   288
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   289
lemma find_min_mset: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   290
  assumes "ts\<noteq>[]"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   291
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   292
  assumes "x \<in># mset_heap ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   293
  shows "find_min ts \<le> x"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   294
  using assms unfolding invar_def 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   295
  by (auto simp: find_min_mset_aux)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   296
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   297
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   298
lemma find_min_member:    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   299
  assumes "ts\<noteq>[]"    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   300
  shows "find_min ts \<in># mset_heap ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   301
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   302
  apply (induction ts rule: find_min.induct)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   303
  apply (auto simp: Let_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   304
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   305
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   306
lemma find_min:    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   307
  assumes "mset_heap ts \<noteq> {#}"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   308
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   309
  shows "find_min ts = Min_mset (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   310
  using assms find_min_member find_min_mset  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   311
  by (auto simp: eq_Min_iff)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   312
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   313
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   314
fun get_min :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   315
  "get_min [t] = (t,[])"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   316
| "get_min (t#ts) = (let (t',ts') = get_min ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   317
                     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
   318
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   319
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   320
lemma get_min_find_min_same_root: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   321
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   322
  assumes "get_min ts = (t',ts')"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   323
  shows "root t' = find_min ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   324
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   325
  apply (induction ts arbitrary: t' ts' rule: find_min.induct)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   326
  apply (auto simp: Let_def split: prod.splits)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   327
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   328
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   329
lemma get_min_mset:    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   330
  assumes "get_min ts = (t',ts')"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   331
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   332
  shows "mset ts = {#t'#} + mset ts'"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   333
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   334
  apply (induction ts arbitrary: t' ts' rule: find_min.induct)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   335
  apply (auto split: prod.splits if_splits)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   336
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   337
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   338
lemma get_min_set:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   339
  assumes "get_min ts = (t', ts')" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   340
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   341
  shows "set ts = insert t' (set ts')" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   342
  using get_min_mset[OF assms, THEN arg_cong[where f=set_mset]]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   343
  by auto  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   344
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   345
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   346
lemma get_min_invar_bheap:    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   347
  assumes "get_min ts = (t',ts')"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   348
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   349
  assumes "invar_bheap ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   350
  shows "invar_btree t'" and "invar_bheap ts'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   351
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   352
  have "invar_btree t' \<and> invar_bheap ts'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   353
    using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   354
    proof (induction ts arbitrary: t' ts' rule: find_min.induct)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   355
      case (2 t v va)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   356
      then show ?case
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   357
        apply (clarsimp split: prod.splits if_splits)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   358
        apply (drule get_min_set; fastforce)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   359
        done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   360
    qed auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   361
  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
   362
qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   363
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   364
lemma get_min_oheap_invar:    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   365
  assumes "get_min ts = (t',ts')"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   366
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   367
  assumes "oheap_invar ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   368
  shows "otree_invar t'" and "oheap_invar ts'"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   369
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   370
  apply (induction ts arbitrary: t' ts' rule: find_min.induct)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   371
  apply (auto split: prod.splits if_splits)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   372
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   373
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   374
definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   375
"del_min ts = (case get_min ts of
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   376
   (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
   377
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   378
lemma del_min_invar[simp]:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   379
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   380
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   381
  shows "invar (del_min ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   382
  using assms  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   383
  unfolding invar_def del_min_def  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   384
  by (auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   385
      split: prod.split tree.split 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   386
      intro!: merge_invar_bheap merge_oheap_invar
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   387
      dest: get_min_invar_bheap get_min_oheap_invar
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   388
      intro!: children_oheap_invar children_invar_bheap
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   389
      )
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   390
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   391
lemma del_min_mset: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   392
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   393
  shows "mset_heap ts = mset_heap (del_min ts) + {# find_min ts #}"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   394
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   395
  unfolding del_min_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   396
  apply (clarsimp split: tree.split prod.split)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   397
  apply (frule (1) get_min_find_min_same_root)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   398
  apply (frule (1) get_min_mset)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   399
  apply (auto simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   400
  done  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   401
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   402
subsection \<open>Complexity\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   403
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   404
text \<open>The size of a binomial tree is determined by its rank\<close>  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   405
lemma size_btree:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   406
  assumes "invar_btree t"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   407
  shows "size (mset_tree t) = 2^rank t"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   408
  using assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   409
proof (induction t)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   410
  case (Node r v ts)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   411
  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
   412
    using that by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   413
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   414
  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
   415
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   416
  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
   417
    by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   418
  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
   419
    by (auto cong: sum_list_cong)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   420
  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
   421
    by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   422
  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
   423
    unfolding COMPL 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   424
    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
   425
  also have "\<dots> = 2^r - 1" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   426
    by (induction r) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   427
  finally show ?case 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   428
    by (simp)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   429
qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   430
   
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   431
text \<open>The length of a binomial heap is bounded by the number of its elements\<close>  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   432
lemma size_bheap:      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   433
  assumes "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   434
  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
   435
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   436
  from \<open>invar_bheap ts\<close> have 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   437
    ASC: "sorted_wrt (op <) (map rank ts)" and
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   438
    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
   439
    unfolding invar_bheap_def by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   440
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   441
  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
   442
    by (simp add: sum_power2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   443
  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
   444
    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
   445
    using power_increasing[where a="2::nat"]  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   446
    by (auto simp: o_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   447
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV   
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   448
    by (auto cong: sum_list_cong simp: size_btree)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   449
  also have "\<dots> = size (mset_heap ts) + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   450
    unfolding mset_heap_def by (induction ts) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   451
  finally show ?thesis .
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   452
qed      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   453
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   454
subsubsection \<open>Timing Functions\<close>  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   455
text \<open>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   456
  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
   457
  estimations of their complexity.
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   458
\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   459
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
   460
[simp]: "t_link _ _ = 1"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   461
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   462
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
   463
  "t_ins_tree t [] = 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   464
| "t_ins_tree t\<^sub>1 (t\<^sub>2#rest) = (
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   465
    (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
   466
     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
   467
  )"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   468
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   469
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   470
definition t_ins :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   471
  "t_ins x ts = t_ins_tree (Node 0 x []) ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   472
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   473
lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1" for t 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   474
  by (induction t ts rule: t_ins_tree.induct) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   475
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   476
lemma t_ins_bound: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   477
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   478
  shows "t_ins x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   479
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   480
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   481
  have 1: "t_ins x ts \<le> length ts + 1" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   482
    unfolding t_ins_def by (rule t_ins_tree_simple_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   483
  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
   484
  proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   485
    from size_bheap[of ts] assms 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   486
    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
   487
      unfolding invar_def by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   488
    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
   489
    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
   490
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   491
  finally show ?thesis 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   492
    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
   493
qed      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   494
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   495
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
   496
  "t_merge ts\<^sub>1 [] = 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   497
| "t_merge [] ts\<^sub>2 = 1"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   498
| "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
   499
    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
   500
    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
   501
    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
   502
  )"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   503
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   504
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
   505
  result length, as each carry reduces the length of the result.\<close>  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   506
lemma l_ins_tree_estimate: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   507
  "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
   508
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
   509
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   510
lemma l_merge_estimate: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   511
  "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"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   512
  apply (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct)  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   513
  apply (auto simp: l_ins_tree_estimate algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   514
  done
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   515
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   516
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
   517
lemma t_merge_bound_aux:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   518
  fixes ts\<^sub>1 ts\<^sub>2
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   519
  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
   520
  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
   521
  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
   522
  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
   523
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   524
  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
   525
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   526
  from l_merge_estimate[of ts\<^sub>1 ts\<^sub>2] 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   527
  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
   528
  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
   529
    by (rule power_increasing) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   530
  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
   531
    by (auto simp: algebra_simps power_add power_mult)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   532
  also note BINVARS(1)[THEN size_bheap]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   533
  also note BINVARS(2)[THEN size_bheap]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   534
  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
   535
    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
   536
  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
   537
    by simp
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   538
  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
   539
    by (simp add: log_mult log_nat_power)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   540
  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
   541
  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
   542
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   543
  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
   544
  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
   545
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   546
  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
   547
  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
   548
  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
   549
qed      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   550
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   551
lemma t_merge_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   552
  fixes ts\<^sub>1 ts\<^sub>2
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   553
  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
   554
  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
   555
  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
   556
  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
   557
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
   558
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   559
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   560
fun t_find_min :: "'a::linorder heap \<Rightarrow> nat" where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   561
  "t_find_min [t] = 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   562
| "t_find_min (t#ts) = 1 + t_find_min ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   563
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   564
lemma t_find_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_find_min ts = length ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   565
by (induction ts rule: t_find_min.induct) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   566
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   567
lemma t_find_min_bound: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   568
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   569
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   570
  shows "t_find_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
   571
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   572
  have 1: "t_find_min ts = length ts" using assms t_find_min_estimate by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   573
  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
   574
  proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   575
    from size_bheap[of ts] assms 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
   576
      unfolding invar_def by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   577
    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
   578
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   579
  finally show ?thesis by auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   580
qed  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   581
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   582
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
   583
  "t_get_min [t] = 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   584
| "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
   585
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   586
lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   587
  by (induction ts rule: t_get_min.induct) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   588
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   589
lemma t_get_min_bound_aux: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   590
  assumes "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   591
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   592
  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
   593
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   594
  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
   595
  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
   596
  proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   597
    from size_bheap[of ts] assms 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
   598
      by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   599
    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
   600
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   601
  finally show ?thesis by auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   602
qed  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   603
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   604
lemma t_get_min_bound: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   605
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   606
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   607
  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
   608
  using assms t_get_min_bound_aux unfolding invar_def by blast  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   609
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   610
thm fold_simps -- \<open>Theorems used by code generator\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   611
fun t_fold :: "('a \<Rightarrow> 'b \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> nat" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   612
  where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   613
  "t_fold t_f f [] s = 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   614
| "t_fold t_f f (x # xs) s = t_f x s + t_fold t_f f xs (f x s)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   615
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   616
text \<open>Estimation for constant function is enough for our purpose\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   617
lemma t_fold_const_bound:  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   618
  shows "t_fold (\<lambda>_ _. K) f l s = K*length l + 1"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   619
  by (induction l arbitrary: s) auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   620
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   621
lemma t_fold_bounded_bound:  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   622
  assumes "\<forall>x s. x\<in>set l \<longrightarrow> t_f x s \<le> K"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   623
  shows "t_fold t_f f l s \<le> K*length l + 1"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   624
  using assms 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   625
  apply (induction l arbitrary: s)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   626
  apply (simp; fail)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   627
  using add_mono
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   628
  by (fastforce simp: algebra_simps) 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   629
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   630
thm rev_conv_fold -- \<open>Theorem used by code generator\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   631
definition "t_rev xs = t_fold (\<lambda>_ _. 1) op # xs []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   632
lemma t_rev_bound: "t_rev xs = length xs + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   633
  unfolding t_rev_def t_fold_const_bound by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   634
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   635
definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   636
  where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   637
  "t_del_min ts = t_get_min ts + (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   638
                    \<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
   639
  )"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   640
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   641
lemma t_rev_ts1_bound_aux: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   642
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   643
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   644
  assumes BINVAR: "invar_bheap (rev ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   645
  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
   646
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   647
  have "t_rev ts = length ts + 1"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   648
    by (auto simp: t_rev_bound)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   649
  hence "2^t_rev ts = 2*2^length ts" by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   650
  also have "\<dots> \<le> 2*n+2" using size_bheap[OF BINVAR] by (auto simp: n_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   651
  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
   652
  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
   653
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   654
  also have "\<dots> = 1 + log 2 (n+1)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   655
    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
   656
  finally show ?thesis by (auto simp: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   657
qed    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   658
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   659
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   660
lemma t_del_min_bound_aux:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   661
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   662
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   663
  assumes BINVAR: "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   664
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   665
  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
   666
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   667
  obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   668
    by (metis surj_pair tree.exhaust_sel)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   669
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   670
  note BINVAR' = get_min_invar_bheap[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   671
  hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: children_invar_bheap)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   672
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   673
  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
   674
  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
   675
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   676
  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
   677
  proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   678
    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
   679
    also have "n\<^sub>1 \<le> n" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   680
      unfolding n\<^sub>1_def n_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   681
      using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   682
      by (auto simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   683
    finally show ?thesis by (auto simp: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   684
  qed    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   685
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   686
  have "t_del_min ts = t_get_min ts + 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
   687
    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
   688
  also have "\<dots> \<le> log 2 (n+1) + 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
   689
    using t_get_min_bound_aux[OF assms(2-)] by (auto simp: n_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   690
  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
   691
    using t_rev_ts1_bound by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   692
  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
   693
    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
   694
    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
   695
  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
   696
    unfolding n\<^sub>1_def n\<^sub>2_def n_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   697
    using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   698
    by (auto simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   699
  finally 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
   700
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   701
  thus ?thesis by (simp add: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   702
qed      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   703
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   704
lemma t_del_min_bound:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   705
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   706
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   707
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   708
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   709
  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
   710
  using assms t_del_min_bound_aux unfolding invar_def by blast
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   711
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   712
subsection \<open>Instantiating the Priority Queue Locale\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   713
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   714
interpretation binheap: 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   715
  Priority_Queue "[]" "op = []" ins find_min del_min invar mset_heap
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   716
proof (unfold_locales, goal_cases)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   717
  case 1
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   718
  then show ?case by simp
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   719
next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   720
  case (2 q)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   721
  then show ?case by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   722
next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   723
  case (3 q x)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   724
  then show ?case by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   725
next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   726
  case (4 q)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   727
  then show ?case using del_min_mset[of q] find_min[OF _ \<open>invar q\<close>] 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   728
    by (auto simp: union_single_eq_diff)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   729
next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   730
  case (5 q)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   731
  then show ?case using find_min[of q] by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   732
next 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   733
  case 6 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   734
  then show ?case by (auto simp add: invar_def invar_bheap_def oheap_invar_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   735
next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   736
  case (7 q x)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   737
  then show ?case by simp
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   738
next
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   739
  case (8 q)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   740
  then show ?case by simp
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   741
qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   742
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   743
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   744
(* Exercise? *)    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   745
subsection \<open>Combined Find and Delete Operation\<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   746
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   747
text \<open>We define an operation that returns the minimum element and 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   748
  a heap with this element removed. \<close>
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   749
definition pop_min :: "'a::linorder heap \<Rightarrow> 'a \<times> 'a::linorder heap" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   750
  where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   751
  "pop_min ts = (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2) 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   752
                    \<Rightarrow> (x,merge (rev ts\<^sub>1) ts\<^sub>2)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   753
  )"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   754
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   755
lemma pop_min_refine:  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   756
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   757
  shows "pop_min ts = (find_min ts, del_min ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   758
  unfolding pop_min_def del_min_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   759
  by (auto 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   760
      split: prod.split tree.split 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   761
      dest: get_min_find_min_same_root[OF assms])
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   762
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   763
lemma pop_min_invar:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   764
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   765
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   766
  assumes "pop_min ts = (x,ts')"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   767
  shows "invar ts'"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   768
  using del_min_invar[of ts] pop_min_refine[of ts] assms by simp
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   769
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   770
lemma pop_min_mset:    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   771
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   772
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   773
  assumes "pop_min ts = (x,ts')"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   774
  shows "mset_heap ts = add_mset x (mset_heap ts')"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   775
  using del_min_mset[of ts] pop_min_refine[of ts] assms by simp 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   776
  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   777
lemma pop_min_min:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   778
  assumes "ts \<noteq> []"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   779
  assumes "invar ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   780
  assumes "pop_min ts = (x,ts')"  
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   781
  shows "\<forall>y\<in>#mset_heap ts'. x\<le>y"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   782
  using pop_min_refine[of ts] del_min_mset[of ts] find_min_mset[of ts] assms
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   783
  by (auto simp del: binheap.mset_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   784
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   785
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   786
definition t_pop_min :: "'a::linorder heap \<Rightarrow> nat" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   787
  where
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   788
  "t_pop_min ts = t_get_min ts + (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2) 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   789
                    \<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
   790
  )"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   791
    
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   792
lemma t_pop_min_bound_aux:
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   793
  fixes ts
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   794
  defines "n \<equiv> size (mset_heap ts)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   795
  assumes BINVAR: "invar_bheap ts"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   796
  assumes "ts\<noteq>[]"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   797
  shows "t_pop_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
   798
proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   799
  obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   800
    by (metis surj_pair tree.exhaust_sel)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   801
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   802
  note BINVAR' = get_min_invar_bheap[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   803
  hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: children_invar_bheap)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   804
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   805
  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
   806
  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
   807
      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   808
  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
   809
  proof -
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   810
    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
   811
    also have "n\<^sub>1 \<le> n" 
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   812
      unfolding n\<^sub>1_def n_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   813
      using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   814
      by (auto simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   815
    finally show ?thesis by (auto simp: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   816
  qed
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   817
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   818
  have "t_pop_min ts = t_get_min ts + 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
   819
    unfolding t_pop_min_def by (simp add: GM)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   820
  also have "\<dots> \<le> log 2 (n+1) + 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
   821
    using t_get_min_bound_aux[OF assms(2-)] by (auto simp: n_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   822
  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
   823
    using t_rev_ts1_bound by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   824
  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
   825
    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
   826
    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
   827
  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
   828
    unfolding n\<^sub>1_def n\<^sub>2_def n_def
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   829
    using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>]
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   830
    by (auto simp: mset_heap_def)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   831
  finally have "t_pop_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
   832
    by auto
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   833
  thus ?thesis by (simp add: algebra_simps)
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   834
qed      
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   835
5d7e770c7d5d added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff changeset
   836
end