author  nipkow 
Tue, 15 Aug 2017 19:47:08 +0200  
changeset 66434  5d7e770c7d5d 
child 66491  78a009ac91d2 
permissions  rwrr 
66434
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^k1" 
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 