src/HOL/Data_Structures/Leftist_Heap.thy
author nipkow
Tue, 31 Jan 2017 17:26:15 +0100
changeset 64969 a7ea55c1be52
parent 62706 49c6a54ceab6
child 64971 a7597a58d7d3
permissions -rw-r--r--
proper priority queue spec
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
     2
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
     3
section \<open>Leftist Heap\<close>
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
     4
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
     5
theory Leftist_Heap
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
     6
imports Tree2 "~~/src/HOL/Library/Multiset" Complex_Main
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
     7
begin
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
     8
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
     9
fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    10
"mset_tree Leaf = {#}" |
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    11
"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    12
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    13
type_synonym 'a lheap = "('a,nat)tree"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    14
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    15
fun rank :: "'a lheap \<Rightarrow> nat" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    16
"rank Leaf = 0" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    17
"rank (Node _ _ _ r) = rank r + 1"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    18
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    19
fun rk :: "'a lheap \<Rightarrow> nat" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    20
"rk Leaf = 0" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    21
"rk (Node n _ _ _) = n"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    22
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    23
text{* The invariants: *}
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    24
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    25
fun (in linorder) heap :: "('a,'b) tree \<Rightarrow> bool" where
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    26
"heap Leaf = True" |
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    27
"heap (Node _ l m r) =
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    28
  (heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). m \<le> x))"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    29
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    30
fun lheap :: "'a lheap \<Rightarrow> bool" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    31
"lheap Leaf = True" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    32
"lheap (Node n l a r) =
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    33
 (n = rank r + 1 \<and> rank l \<ge> rank r \<and> lheap l & lheap r)"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    34
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    35
definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    36
"node l a r =
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    37
 (let rl = rk l; rr = rk r
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    38
  in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    39
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    40
fun get_min :: "'a lheap \<Rightarrow> 'a" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    41
"get_min(Node n l a r) = a"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    42
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    43
function meld :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    44
"meld Leaf t2 = t2" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    45
"meld t1 Leaf = t1" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    46
"meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    47
   (if a1 \<le> a2 then node l1 a1 (meld r1 (Node n2 l2 a2 r2))
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    48
    else node l2 a2 (meld r2 (Node n1 l1 a1 r1)))"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    49
by pat_completeness auto
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    50
termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    51
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    52
lemma meld_code: "meld t1 t2 = (case (t1,t2) of
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    53
  (Leaf, _) \<Rightarrow> t2 |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    54
  (_, Leaf) \<Rightarrow> t1 |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    55
  (Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow>
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    56
    if a1 \<le> a2 then node l1 a1 (meld r1 t2) else node l2 a2 (meld r2 t1))"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    57
by(induction t1 t2 rule: meld.induct) (simp_all split: tree.split)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    58
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    59
definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    60
"insert x t = meld (Node 1 Leaf x Leaf) t"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    61
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    62
fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    63
"del_min Leaf = Leaf" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    64
"del_min (Node n l x r) = meld l r"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    65
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    66
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    67
subsection "Lemmas"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    68
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    69
declare Let_def [simp]
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    70
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    71
lemma rk_eq_rank[simp]: "lheap t \<Longrightarrow> rk t = rank t"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    72
by(cases t) auto
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    73
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    74
lemma lheap_node: "lheap (node l a r) \<longleftrightarrow> lheap l \<and> lheap r"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    75
by(auto simp add: node_def)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    76
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    77
lemma heap_node: "heap (node l a r) \<longleftrightarrow>
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    78
  heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). a \<le> x)"
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    79
by(auto simp add: node_def)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    80
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    81
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    82
subsection "Functional Correctness"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    83
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    84
locale Priority_Queue =
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    85
fixes empty :: "'pq"
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    86
and insert :: "'a::linorder \<Rightarrow> 'pq \<Rightarrow> 'pq"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    87
and get_min :: "'pq \<Rightarrow> 'a"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    88
and del_min :: "'pq \<Rightarrow> 'pq"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    89
and invar :: "'pq \<Rightarrow> bool"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    90
and mset :: "'pq \<Rightarrow> 'a multiset"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    91
assumes mset_empty: "mset empty = {#}"
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    92
and mset_insert: "invar pq \<Longrightarrow> mset (insert x pq) = mset pq + {#x#}"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    93
and mset_del_min: "invar pq \<Longrightarrow> mset (del_min pq) = mset pq - {#get_min pq#}"
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    94
and get_min: "invar pq \<Longrightarrow> pq \<noteq> empty \<Longrightarrow>
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    95
   get_min pq \<in> set_mset(mset pq) \<and> (\<forall>x \<in># mset pq. get_min pq \<le> x)"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    96
and invar_insert: "invar pq \<Longrightarrow> invar (insert x pq)"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    97
and invar_del_min: "invar pq \<Longrightarrow> invar (del_min pq)"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    98
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    99
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   100
lemma mset_meld: "mset_tree (meld h1 h2) = mset_tree h1 + mset_tree h2"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   101
by (induction h1 h2 rule: meld.induct) (auto simp add: node_def ac_simps)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   102
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   103
lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   104
by (auto simp add: insert_def mset_meld)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   105
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   106
lemma get_min:
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   107
  "heap h \<Longrightarrow> h \<noteq> Leaf \<Longrightarrow>
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   108
   get_min h \<in> set_mset(mset_tree h) \<and> (\<forall>x \<in># mset_tree h. get_min h \<le> x)"
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   109
by (induction h) (auto)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   110
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   111
lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   112
by (cases h) (auto simp: mset_meld)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   113
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   114
lemma lheap_meld: "\<lbrakk> lheap l; lheap r \<rbrakk> \<Longrightarrow> lheap (meld l r)"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   115
proof(induction l r rule: meld.induct)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   116
  case (3 n1 l1 a1 r1 n2 l2 a2 r2)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   117
  show ?case (is "lheap(meld ?t1 ?t2)")
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   118
  proof cases
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   119
    assume "a1 \<le> a2"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   120
    hence "lheap (meld ?t1 ?t2) = lheap (node l1 a1 (meld r1 ?t2))" by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   121
    also have "\<dots> = (lheap l1 \<and> lheap(meld r1 ?t2))"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   122
      by(simp add: lheap_node)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   123
    also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by (simp)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   124
    finally show ?thesis .
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   125
  next (* analogous but automatic *)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   126
    assume "\<not> a1 \<le> a2"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   127
    thus ?thesis using 3 by(simp)(auto simp: lheap_node)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   128
  qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   129
qed simp_all
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   130
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   131
lemma heap_meld: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (meld l r)"
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   132
proof(induction l r rule: meld.induct)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   133
  case 3 thus ?case by(auto simp: heap_node mset_meld ball_Un)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   134
qed simp_all
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   135
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   136
lemma lheap_insert: "lheap t \<Longrightarrow> lheap(insert x t)"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   137
by(simp add: insert_def lheap_meld del: meld.simps split: tree.split)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   138
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   139
lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   140
by(simp add: insert_def heap_meld del: meld.simps split: tree.split)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   141
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   142
lemma lheap_del_min: "lheap t \<Longrightarrow> lheap(del_min t)"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   143
by(cases t)(auto simp add: lheap_meld simp del: meld.simps)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   144
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   145
lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   146
by(cases t)(auto simp add: heap_meld simp del: meld.simps)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   147
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   148
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   149
interpretation lheap: Priority_Queue
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   150
where empty = Leaf and insert = insert and del_min = del_min
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   151
and get_min = get_min and invar = "\<lambda>h. heap h \<and> lheap h"
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   152
and mset = mset_tree
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   153
proof(standard, goal_cases)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   154
  case 1 show ?case by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   155
next
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   156
  case 2 show ?case by(rule mset_insert)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   157
next
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   158
  case 3 show ?case by(rule mset_del_min)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   159
next
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   160
  case 4 thus ?case by(simp add: get_min)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   161
next
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   162
  case 5 thus ?case by(simp add: heap_insert lheap_insert)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   163
next
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   164
  case 6 thus ?case by(simp add: heap_del_min lheap_del_min)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   165
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   166
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   167
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   168
subsection "Complexity"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   169
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   170
lemma pow2_rank_size1: "lheap t \<Longrightarrow> 2 ^ rank t \<le> size1 t"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   171
proof(induction t)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   172
  case Leaf show ?case by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   173
next
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   174
  case (Node n l a r)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   175
  hence "rank r \<le> rank l" by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   176
  hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   177
  have "(2::nat) ^ rank \<langle>n, l, a, r\<rangle> = 2 ^ rank r + 2 ^ rank r"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   178
    by(simp add: mult_2)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   179
  also have "\<dots> \<le> size1 l + size1 r"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   180
    using Node * by (simp del: power_increasing_iff)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   181
  also have "\<dots> = size1 \<langle>n, l, a, r\<rangle>" by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   182
  finally show ?case .
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   183
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   184
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   185
function t_meld :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   186
"t_meld Leaf t2 = 1" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   187
"t_meld t2 Leaf = 1" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   188
"t_meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   189
  (if a1 \<le> a2 then 1 + t_meld r1 (Node n2 l2 a2 r2)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   190
   else 1 + t_meld r2 (Node n1 l1 a1 r1))"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   191
by pat_completeness auto
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   192
termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   193
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   194
definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   195
"t_insert x t = t_meld (Node 1 Leaf x Leaf) t"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   196
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   197
fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   198
"t_del_min Leaf = 1" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   199
"t_del_min (Node n l a r) = t_meld l r"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   200
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   201
lemma t_meld_rank: "t_meld l r \<le> rank l + rank r + 1"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   202
proof(induction l r rule: meld.induct)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   203
  case 3 thus ?case
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   204
    by(simp)(fastforce split: tree.splits simp del: t_meld.simps)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   205
qed simp_all
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   206
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   207
corollary t_meld_log: assumes "lheap l" "lheap r"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   208
  shows "t_meld l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   209
using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]]
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   210
  le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_meld_rank[of l r]
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   211
by linarith
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   212
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   213
corollary t_insert_log: "lheap t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   214
using t_meld_log[of "Node 1 Leaf x Leaf" t]
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   215
by(simp add: t_insert_def split: tree.split)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   216
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   217
lemma ld_ld_1_less:
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   218
  assumes "x > 0" "y > 0" shows "1 + log 2 x + log 2 y < 2 * log 2 (x+y)"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   219
proof -
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   220
  have 1: "2*x*y < (x+y)^2" using assms
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   221
    by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   222
  show ?thesis
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   223
    apply(rule powr_less_cancel_iff[of 2, THEN iffD1])
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   224
     apply simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   225
    using assms 1 by(simp add: powr_add log_powr[symmetric] powr_numeral)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   226
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   227
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   228
corollary t_del_min_log: assumes "lheap t"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   229
  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   230
proof(cases t)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   231
  case Leaf thus ?thesis using assms by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   232
next
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   233
  case [simp]: (Node _ t1 _ t2)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   234
  have "t_del_min t = t_meld t1 t2" by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   235
  also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   236
    using \<open>lheap t\<close> by (auto simp: t_meld_log simp del: t_meld.simps)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   237
  also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   238
    using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   239
  finally show ?thesis .
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   240
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   241
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   242
end