src/HOL/Data_Structures/Leftist_Heap.thy
author nipkow
Mon, 03 May 2021 19:06:33 +0200
changeset 73875 0c8d6bec6491
parent 72773 8eabaf951e6b
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
66422
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
     6
imports
70636
7c2724cefcb8 reduced dependencies
nipkow
parents: 70548
diff changeset
     7
  "HOL-Library.Pattern_Aliases"
66422
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
     8
  Tree2
68493
c7e0a7bcacaf added lemmas; uniform names
nipkow
parents: 68414
diff changeset
     9
  Priority_Queue_Specs
66422
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
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    13
fun mset_tree :: "('a*'b) tree \<Rightarrow> 'a multiset" where
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    14
"mset_tree Leaf = {#}" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    15
"mset_tree (Node l (a, _) r) = {#a#} + mset_tree l + mset_tree r"
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    16
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    17
type_synonym 'a lheap = "('a*nat)tree"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    18
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
    19
fun mht :: "'a lheap \<Rightarrow> nat" where
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
    20
"mht Leaf = 0" |
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
    21
"mht (Node _ (_, n) _) = n"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    22
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 66564
diff changeset
    23
text\<open>The invariants:\<close>
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    24
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    25
fun (in linorder) heap :: "('a*'b) tree \<Rightarrow> bool" where
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    26
"heap Leaf = True" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    27
"heap (Node l (m, _) r) =
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
    28
  ((\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x) \<and> heap l \<and> heap r)"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    29
64973
nipkow
parents: 64971
diff changeset
    30
fun ltree :: "'a lheap \<Rightarrow> bool" where
nipkow
parents: 64971
diff changeset
    31
"ltree Leaf = True" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    32
"ltree (Node l (a, n) r) =
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
    33
 (min_height l \<ge> min_height r \<and> n = min_height r + 1 \<and> ltree l & ltree r)"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    34
70771
nipkow
parents: 70636
diff changeset
    35
definition empty :: "'a lheap" where
nipkow
parents: 70636
diff changeset
    36
"empty = Leaf"
nipkow
parents: 70636
diff changeset
    37
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    38
definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    39
"node l a r =
73875
nipkow
parents: 72773
diff changeset
    40
 (let mhl = mht l; mhr = mht r
nipkow
parents: 72773
diff changeset
    41
  in if mhl \<ge> mhr then Node l (a,mhr+1) r else Node r (a,mhl+1) l)"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    42
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    43
fun get_min :: "'a lheap \<Rightarrow> 'a" where
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    44
"get_min(Node l (a, n) r) = a"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    45
66502
nipkow
parents: 66492
diff changeset
    46
text \<open>For function \<open>merge\<close>:\<close>
nipkow
parents: 66492
diff changeset
    47
unbundle pattern_aliases
66492
nipkow
parents: 66424
diff changeset
    48
66502
nipkow
parents: 66492
diff changeset
    49
fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
70771
nipkow
parents: 70636
diff changeset
    50
"merge Leaf t = t" |
nipkow
parents: 70636
diff changeset
    51
"merge t Leaf = t" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    52
"merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) =
66492
nipkow
parents: 66424
diff changeset
    53
   (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
68600
bdd6536bd57c more symmetric
nipkow
parents: 68493
diff changeset
    54
    else node l2 a2 (merge t1 r2))"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    55
70771
nipkow
parents: 70636
diff changeset
    56
text \<open>Termination of @{const merge}: by sum or lexicographic product of the sizes
nipkow
parents: 70636
diff changeset
    57
of the two arguments. Isabelle uses a lexicographic product.\<close>
nipkow
parents: 70636
diff changeset
    58
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
    59
lemma merge_code: "merge t1 t2 = (case (t1,t2) of
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    60
  (Leaf, _) \<Rightarrow> t2 |
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    61
  (_, Leaf) \<Rightarrow> t1 |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    62
  (Node l1 (a1, n1) r1, Node l2 (a2, n2) r2) \<Rightarrow>
68600
bdd6536bd57c more symmetric
nipkow
parents: 68493
diff changeset
    63
    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
    64
by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    65
66524
nipkow
parents: 66502
diff changeset
    66
hide_const (open) insert
nipkow
parents: 66502
diff changeset
    67
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    68
definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    69
"insert x t = merge (Node Leaf (x,1) Leaf) t"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    70
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
    71
fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
    72
"del_min Leaf = Leaf" |
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
    73
"del_min (Node l _ r) = merge l r"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    74
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    75
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    76
subsection "Lemmas"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    77
66422
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
    78
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
    79
by(cases t) auto
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
    80
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
    81
lemma mht_eq_min_height: "ltree t \<Longrightarrow> mht t = min_height t"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    82
by(cases t) auto
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    83
64973
nipkow
parents: 64971
diff changeset
    84
lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
    85
by(auto simp add: node_def mht_eq_min_height)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    86
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    87
lemma heap_node: "heap (node l a r) \<longleftrightarrow>
70771
nipkow
parents: 70636
diff changeset
    88
  heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. a \<le> x)"
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    89
by(auto simp add: node_def)
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    90
70771
nipkow
parents: 70636
diff changeset
    91
lemma set_tree_mset: "set_tree t = set_mset(mset_tree t)"
nipkow
parents: 70636
diff changeset
    92
by(induction t) auto
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    93
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    94
subsection "Functional Correctness"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    95
72513
nipkow
parents: 70944
diff changeset
    96
lemma mset_merge: "mset_tree (merge t1 t2) = mset_tree t1 + mset_tree t2"
nipkow
parents: 70944
diff changeset
    97
by (induction t1 t2 rule: merge.induct) (auto simp add: node_def ac_simps)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
    98
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
    99
lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   100
by (auto simp add: insert_def mset_merge)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   101
72513
nipkow
parents: 70944
diff changeset
   102
lemma get_min: "\<lbrakk> heap t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min t = Min(set_tree t)"
nipkow
parents: 70944
diff changeset
   103
by (cases t) (auto simp add: eq_Min_iff)
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   104
72513
nipkow
parents: 70944
diff changeset
   105
lemma mset_del_min: "mset_tree (del_min t) = mset_tree t - {# get_min t #}"
nipkow
parents: 70944
diff changeset
   106
by (cases t) (auto simp: mset_merge)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   107
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   108
lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
72513
nipkow
parents: 70944
diff changeset
   109
by(induction l r rule: merge.induct)(auto simp: ltree_node)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   110
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   111
lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   112
proof(induction l r rule: merge.induct)
70771
nipkow
parents: 70636
diff changeset
   113
  case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un set_tree_mset)
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   114
qed simp_all
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   115
64973
nipkow
parents: 64971
diff changeset
   116
lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   117
by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   118
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   119
lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   120
by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   121
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   122
lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   123
by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   124
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   125
lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   126
by(cases t)(auto simp add: heap_merge simp del: merge.simps)
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   127
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66524
diff changeset
   128
text \<open>Last step of functional correctness proof: combine all the above lemmas
ff561d9cb661 added PQ with merge
nipkow
parents: 66524
diff changeset
   129
to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   130
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66524
diff changeset
   131
interpretation lheap: Priority_Queue_Merge
72513
nipkow
parents: 70944
diff changeset
   132
where empty = empty and is_empty = "\<lambda>t. t = Leaf"
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   133
and insert = insert and del_min = del_min
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66524
diff changeset
   134
and get_min = get_min and merge = merge
72513
nipkow
parents: 70944
diff changeset
   135
and invar = "\<lambda>t. heap t \<and> ltree t" and mset = mset_tree
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   136
proof(standard, goal_cases)
70771
nipkow
parents: 70636
diff changeset
   137
  case 1 show ?case by (simp add: empty_def)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   138
next
64975
96b66d5c0fc1 added is_empty
nipkow
parents: 64973
diff changeset
   139
  case (2 q) show ?case by (cases q) auto
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   140
next
64975
96b66d5c0fc1 added is_empty
nipkow
parents: 64973
diff changeset
   141
  case 3 show ?case by(rule mset_insert)
96b66d5c0fc1 added is_empty
nipkow
parents: 64973
diff changeset
   142
next
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   143
  case 4 show ?case by(rule mset_del_min)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   144
next
70771
nipkow
parents: 70636
diff changeset
   145
  case 5 thus ?case by(simp add: get_min mset_tree_empty set_tree_mset)
66422
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   146
next
70771
nipkow
parents: 70636
diff changeset
   147
  case 6 thus ?case by(simp add: empty_def)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   148
next
66422
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   149
  case 7 thus ?case by(simp add: heap_insert ltree_insert)
64969
a7ea55c1be52 proper priority queue spec
nipkow
parents: 62706
diff changeset
   150
next
68021
b91a043c0dcb dont rename PQ.del_min
nipkow
parents: 68020
diff changeset
   151
  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
66564
ff561d9cb661 added PQ with merge
nipkow
parents: 66524
diff changeset
   152
next
ff561d9cb661 added PQ with merge
nipkow
parents: 66524
diff changeset
   153
  case 9 thus ?case by (simp add: mset_merge)
ff561d9cb661 added PQ with merge
nipkow
parents: 66524
diff changeset
   154
next
ff561d9cb661 added PQ with merge
nipkow
parents: 66524
diff changeset
   155
  case 10 thus ?case by (simp add: heap_merge ltree_merge)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   156
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   157
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   158
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   159
subsection "Complexity"
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   160
66492
nipkow
parents: 66424
diff changeset
   161
text\<open>Explicit termination argument: sum of sizes\<close>
nipkow
parents: 66424
diff changeset
   162
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   163
fun T_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   164
"T_merge Leaf t = 1" |
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   165
"T_merge t Leaf = 1" |
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   166
"T_merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) =
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   167
  (if a1 \<le> a2 then T_merge r1 t2
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   168
   else T_merge t1 r2) + 1"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   169
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   170
definition T_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   171
"T_insert x t = T_merge (Node Leaf (x, 1) Leaf) t + 1"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   172
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   173
fun T_del_min :: "'a::ord lheap \<Rightarrow> nat" where
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   174
"T_del_min Leaf = 1" |
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   175
"T_del_min (Node l _ r) = T_merge l r + 1"
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   176
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   177
lemma T_merge_min_height: "ltree l \<Longrightarrow> ltree r \<Longrightarrow> T_merge l r \<le> min_height l + min_height r + 1"
64976
1a4cb9403a10 renaming
nipkow
parents: 64975
diff changeset
   178
proof(induction l r rule: merge.induct)
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   179
  case 3 thus ?case by(auto)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   180
qed simp_all
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   181
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   182
corollary T_merge_log: assumes "ltree l" "ltree r"
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   183
  shows "T_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   184
using le_log2_of_power[OF min_height_size1[of l]]
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   185
  le_log2_of_power[OF min_height_size1[of r]] T_merge_min_height[of l r] assms
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   186
by linarith
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   187
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   188
corollary T_insert_log: "ltree t \<Longrightarrow> T_insert x t \<le> log 2 (size1 t) + 3"
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   189
using T_merge_log[of "Node Leaf (x, 1) Leaf" t]
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   190
by(simp add: T_insert_def split: tree.split)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   191
66492
nipkow
parents: 66424
diff changeset
   192
(* FIXME mv ? *)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   193
lemma ld_ld_1_less:
66422
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   194
  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
   195
proof -
66422
8194ed7cf2cb separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents: 64977
diff changeset
   196
  have "2 powr (log 2 x + log 2 y + 1) = 2*x*y"
64977
50f2f10ab576 tuned proof
nipkow
parents: 64976
diff changeset
   197
    using assms by(simp add: powr_add)
50f2f10ab576 tuned proof
nipkow
parents: 64976
diff changeset
   198
  also have "\<dots> < (x+y)^2" using assms
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   199
    by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
64977
50f2f10ab576 tuned proof
nipkow
parents: 64976
diff changeset
   200
  also have "\<dots> = 2 powr (2 * log 2 (x+y))"
66492
nipkow
parents: 66424
diff changeset
   201
    using assms by(simp add: powr_add log_powr[symmetric])
64977
50f2f10ab576 tuned proof
nipkow
parents: 64976
diff changeset
   202
  finally show ?thesis by simp
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   203
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   204
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   205
corollary T_del_min_log: assumes "ltree t"
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   206
  shows "T_del_min t \<le> 2 * log 2 (size1 t) + 1"
70944
3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents: 70771
diff changeset
   207
proof(cases t rule: tree2_cases)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   208
  case Leaf thus ?thesis using assms by simp
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   209
next
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   210
  case [simp]: (Node l _ _ r)
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   211
  have "T_del_min t = T_merge l r + 1" by simp
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   212
  also have "\<dots> \<le> log 2 (size1 l) + log 2 (size1 r) + 2"
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   213
    using \<open>ltree t\<close> T_merge_log[of l r] by (auto simp del: T_merge.simps)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   214
  also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
72773
8eabaf951e6b use min_height as in (much of?) the literature
nipkow
parents: 72513
diff changeset
   215
    using ld_ld_1_less[of "size1 l" "size1 r"] by (simp)
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   216
  finally show ?thesis .
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   217
qed
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   218
49c6a54ceab6 added Leftist_Heap
nipkow
parents:
diff changeset
   219
end