90 |
90 |
91 subsection \<open>Operations and Their Functional Correctness\<close> |
91 subsection \<open>Operations and Their Functional Correctness\<close> |
92 |
92 |
93 subsubsection \<open>\<open>link\<close>\<close> |
93 subsubsection \<open>\<open>link\<close>\<close> |
94 |
94 |
95 definition link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
95 context |
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> |
96 includes pattern_aliases |
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) |
97 begin |
98 )" |
98 |
|
99 fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
100 "link (Node r x\<^sub>1 c\<^sub>1 =: t\<^sub>1) (Node _ x\<^sub>2 c\<^sub>2 =: t\<^sub>2) = |
|
101 (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))" |
|
102 |
|
103 end |
99 |
104 |
100 lemma invar_btree_link: |
105 lemma invar_btree_link: |
101 assumes "invar_btree t\<^sub>1" |
106 assumes "invar_btree t\<^sub>1" |
102 assumes "invar_btree t\<^sub>2" |
107 assumes "invar_btree t\<^sub>2" |
103 assumes "rank t\<^sub>1 = rank t\<^sub>2" |
108 assumes "rank t\<^sub>1 = rank t\<^sub>2" |
104 shows "invar_btree (link t\<^sub>1 t\<^sub>2)" |
109 shows "invar_btree (link t\<^sub>1 t\<^sub>2)" |
105 using assms |
110 using assms |
106 by (auto simp: link_def split: tree.split) |
111 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp |
107 |
112 |
108 lemma invar_link_otree: |
113 lemma invar_link_otree: |
109 assumes "invar_otree t\<^sub>1" |
114 assumes "invar_otree t\<^sub>1" |
110 assumes "invar_otree t\<^sub>2" |
115 assumes "invar_otree t\<^sub>2" |
111 shows "invar_otree (link t\<^sub>1 t\<^sub>2)" |
116 shows "invar_otree (link t\<^sub>1 t\<^sub>2)" |
112 using assms |
117 using assms |
113 by (auto simp: link_def split: tree.split) |
118 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto |
114 |
119 |
115 lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1" |
120 lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1" |
116 by (auto simp: link_def split: tree.split) |
121 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp |
117 |
122 |
118 lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2" |
123 lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2" |
119 by (auto simp: link_def split: tree.split) |
124 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp |
120 |
125 |
121 subsubsection \<open>\<open>ins_tree\<close>\<close> |
126 subsubsection \<open>\<open>ins_tree\<close>\<close> |
122 |
127 |
123 fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where |
128 fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where |
124 "ins_tree t [] = [t]" |
129 "ins_tree t [] = [t]" |