src/HOL/Data_Structures/Leftist_Heap.thy
author nipkow
Thu, 11 Jul 2019 18:37:52 +0200
changeset 70363 6d96ee03b62e
parent 68600 bdd6536bd57c
child 70450 7c2724cefcb8
permissions -rw-r--r--
tuned
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
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
     6
imports
66491
nipkow
parents: 66425
diff changeset
     7
  Base_FDS
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
     8
  Tree2
68492
c7e0a7bcacaf added lemmas; uniform names
nipkow
parents: 68413
diff changeset
     9
  Priority_Queue_Specs
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
    10
  Complex_Main
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    11
begin
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    12
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    13
fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    14
"mset_tree Leaf = {#}" |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    15
"mset_tree (Node l a _ r) = {#a#} + mset_tree l + mset_tree r"
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    16
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    17
type_synonym 'a lheap = "('a,nat)tree"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    18
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    19
fun rank :: "'a lheap \<Rightarrow> nat" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    20
"rank Leaf = 0" |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    21
"rank (Node _ _ _ r) = rank r + 1"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    22
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    23
fun rk :: "'a lheap \<Rightarrow> nat" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    24
"rk Leaf = 0" |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    25
"rk (Node _ _ n _) = n"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    26
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 66565
diff changeset
    27
text\<open>The invariants:\<close>
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    28
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    29
fun (in linorder) heap :: "('a,'b) tree \<Rightarrow> bool" where
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    30
"heap Leaf = True" |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    31
"heap (Node l m _ r) =
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    32
  (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
    33
64973
nipkow
parents: 64971
diff changeset
    34
fun ltree :: "'a lheap \<Rightarrow> bool" where
nipkow
parents: 64971
diff changeset
    35
"ltree Leaf = True" |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    36
"ltree (Node l a n r) =
64973
nipkow
parents: 64971
diff changeset
    37
 (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    38
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    39
definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    40
"node l a r =
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    41
 (let rl = rk l; rr = rk r
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    42
  in if rl \<ge> rr then Node l a (rr+1) r else Node r a (rl+1) l)"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    43
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    44
fun get_min :: "'a lheap \<Rightarrow> 'a" where
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    45
"get_min(Node l a n r) = a"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    46
66499
nipkow
parents: 66491
diff changeset
    47
text \<open>For function \<open>merge\<close>:\<close>
nipkow
parents: 66491
diff changeset
    48
unbundle pattern_aliases
66491
nipkow
parents: 66425
diff changeset
    49
66499
nipkow
parents: 66491
diff changeset
    50
fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
    51
"merge Leaf t2 = t2" |
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
    52
"merge t1 Leaf = t1" |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    53
"merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
66491
nipkow
parents: 66425
diff changeset
    54
   (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
68600
bdd6536bd57c more symmetric
nipkow
parents: 68492
diff changeset
    55
    else node l2 a2 (merge t1 r2))"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    56
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
    57
lemma merge_code: "merge t1 t2 = (case (t1,t2) of
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    58
  (Leaf, _) \<Rightarrow> t2 |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    59
  (_, Leaf) \<Rightarrow> t1 |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    60
  (Node l1 a1 n1 r1, Node l2 a2 n2 r2) \<Rightarrow>
68600
bdd6536bd57c more symmetric
nipkow
parents: 68492
diff changeset
    61
    if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge t1 r2))"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
    62
by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    63
66522
nipkow
parents: 66499
diff changeset
    64
hide_const (open) insert
nipkow
parents: 66499
diff changeset
    65
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    66
definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    67
"insert x t = merge (Node Leaf x 1 Leaf) t"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    68
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
    69
fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
    70
"del_min Leaf = Leaf" |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
    71
"del_min (Node l x n r) = merge l r"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    72
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    73
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    74
subsection "Lemmas"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    75
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
    76
lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
    77
by(cases t) auto
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
    78
64973
nipkow
parents: 64971
diff changeset
    79
lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    80
by(cases t) auto
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    81
64973
nipkow
parents: 64971
diff changeset
    82
lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    83
by(auto simp add: node_def)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    84
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    85
lemma heap_node: "heap (node l a r) \<longleftrightarrow>
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    86
  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
    87
by(auto simp add: node_def)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    88
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    89
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    90
subsection "Functional Correctness"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    91
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
    92
lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2"
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
    93
by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    94
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    95
lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
    96
by (auto simp add: insert_def mset_merge)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    97
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
    98
lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
66425
8756322dc5de added Min_mset and Max_mset
nipkow
parents: 66419
diff changeset
    99
by (induction h) (auto simp add: eq_Min_iff)
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   100
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   101
lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   102
by (cases h) (auto simp: mset_merge)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   103
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   104
lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   105
proof(induction l r rule: merge.induct)
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   106
  case (3 l1 a1 n1 r1 l2 a2 n2 r2)
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   107
  show ?case (is "ltree(merge ?t1 ?t2)")
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   108
  proof cases
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   109
    assume "a1 \<le> a2"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   110
    hence "ltree (merge ?t1 ?t2) = ltree (node l1 a1 (merge r1 ?t2))" by simp
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   111
    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
64973
nipkow
parents: 64971
diff changeset
   112
      by(simp add: ltree_node)
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 66565
diff changeset
   113
    also have "..." using "3.prems" "3.IH"(1)[OF \<open>a1 \<le> a2\<close>] by (simp)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   114
    finally show ?thesis .
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   115
  next (* analogous but automatic *)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   116
    assume "\<not> a1 \<le> a2"
64973
nipkow
parents: 64971
diff changeset
   117
    thus ?thesis using 3 by(simp)(auto simp: ltree_node)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   118
  qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   119
qed simp_all
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   120
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   121
lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   122
proof(induction l r rule: merge.induct)
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   123
  case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un)
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   124
qed simp_all
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   125
64973
nipkow
parents: 64971
diff changeset
   126
lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   127
by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   128
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   129
lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   130
by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   131
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   132
lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   133
by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   134
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   135
lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   136
by(cases t)(auto simp add: heap_merge simp del: merge.simps)
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   137
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   138
text \<open>Last step of functional correctness proof: combine all the above lemmas
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   139
to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   140
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   141
interpretation lheap: Priority_Queue_Merge
64975
96b66d5c0fc1 added is_empty
nipkow
parents: 64973
diff changeset
   142
where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   143
and insert = insert and del_min = del_min
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   144
and get_min = get_min and merge = merge
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   145
and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   146
proof(standard, goal_cases)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   147
  case 1 show ?case by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   148
next
64975
96b66d5c0fc1 added is_empty
nipkow
parents: 64973
diff changeset
   149
  case (2 q) show ?case by (cases q) auto
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   150
next
64975
96b66d5c0fc1 added is_empty
nipkow
parents: 64973
diff changeset
   151
  case 3 show ?case by(rule mset_insert)
96b66d5c0fc1 added is_empty
nipkow
parents: 64973
diff changeset
   152
next
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   153
  case 4 show ?case by(rule mset_del_min)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   154
next
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   155
  case 5 thus ?case by(simp add: get_min mset_tree_empty)
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   156
next
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   157
  case 6 thus ?case by(simp)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   158
next
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   159
  case 7 thus ?case by(simp add: heap_insert ltree_insert)
64968
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   160
next
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   161
  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
66565
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   162
next
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   163
  case 9 thus ?case by (simp add: mset_merge)
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   164
next
ff561d9cb661 added PQ with merge
nipkow
parents: 66522
diff changeset
   165
  case 10 thus ?case by (simp add: heap_merge ltree_merge)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   166
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   167
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   168
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   169
subsection "Complexity"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   170
64973
nipkow
parents: 64971
diff changeset
   171
lemma pow2_rank_size1: "ltree t \<Longrightarrow> 2 ^ rank t \<le> size1 t"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   172
proof(induction t)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   173
  case Leaf show ?case by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   174
next
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   175
  case (Node l a n r)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   176
  hence "rank r \<le> rank l" by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   177
  hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   178
  have "(2::nat) ^ rank \<langle>l, a, n, r\<rangle> = 2 ^ rank r + 2 ^ rank r"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   179
    by(simp add: mult_2)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   180
  also have "\<dots> \<le> size1 l + size1 r"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   181
    using Node * by (simp del: power_increasing_iff)
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   182
  also have "\<dots> = size1 \<langle>l, a, n, r\<rangle>" by simp
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   183
  finally show ?case .
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   184
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   185
66491
nipkow
parents: 66425
diff changeset
   186
text\<open>Explicit termination argument: sum of sizes\<close>
nipkow
parents: 66425
diff changeset
   187
66499
nipkow
parents: 66491
diff changeset
   188
fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   189
"t_merge Leaf t2 = 1" |
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   190
"t_merge t2 Leaf = 1" |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   191
"t_merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
66491
nipkow
parents: 66425
diff changeset
   192
  (if a1 \<le> a2 then 1 + t_merge r1 t2
68600
bdd6536bd57c more symmetric
nipkow
parents: 68492
diff changeset
   193
   else 1 + t_merge t1 r2)"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   194
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   195
definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   196
"t_insert x t = t_merge (Node Leaf x 1 Leaf) t"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   197
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   198
fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   199
"t_del_min Leaf = 1" |
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   200
"t_del_min (Node l a n r) = t_merge l r"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   201
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   202
lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   203
proof(induction l r rule: merge.induct)
68600
bdd6536bd57c more symmetric
nipkow
parents: 68492
diff changeset
   204
  case 3 thus ?case by(simp)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   205
qed simp_all
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   206
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   207
corollary t_merge_log: assumes "ltree l" "ltree r"
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   208
  shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   209
using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]]
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   210
  le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_merge_rank[of l r]
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   211
by linarith
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   212
64973
nipkow
parents: 64971
diff changeset
   213
corollary t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   214
using t_merge_log[of "Node Leaf x 1 Leaf" t]
62706
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
66491
nipkow
parents: 66425
diff changeset
   217
(* FIXME mv ? *)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   218
lemma ld_ld_1_less:
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   219
  assumes "x > 0" "y > 0" shows "log 2 x + log 2 y + 1 < 2 * log 2 (x+y)"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   220
proof -
66419
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   221
  have "2 powr (log 2 x + log 2 y + 1) = 2*x*y"
64977
50f2f10ab576 tuned proof
nipkow
parents: 64976
diff changeset
   222
    using assms by(simp add: powr_add)
50f2f10ab576 tuned proof
nipkow
parents: 64976
diff changeset
   223
  also have "\<dots> < (x+y)^2" using assms
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   224
    by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
64977
50f2f10ab576 tuned proof
nipkow
parents: 64976
diff changeset
   225
  also have "\<dots> = 2 powr (2 * log 2 (x+y))"
66491
nipkow
parents: 66425
diff changeset
   226
    using assms by(simp add: powr_add log_powr[symmetric])
64977
50f2f10ab576 tuned proof
nipkow
parents: 64976
diff changeset
   227
  finally show ?thesis by simp
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   228
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   229
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   230
corollary t_del_min_log: assumes "ltree t"
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   231
  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   232
proof(cases t)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   233
  case Leaf thus ?thesis using assms by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   234
next
68413
b56ed5010e69 tuned order of arguments
nipkow
parents: 68021
diff changeset
   235
  case [simp]: (Node t1 _ _ t2)
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   236
  have "t_del_min t = t_merge t1 t2" by simp
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   237
  also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   238
    using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   239
  also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   240
    using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp)
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   241
  finally show ?thesis .
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   242
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   243
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   244
end