--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Biendarra_Julian_julian.biendarra@tum.de_613/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,73 @@
+(*<*)
+theory hw13
+imports "~~/src/HOL/Library/Multiset"
+begin
+(*>*)
+
+text \<open>
+ \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+"get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge h None = h" |
+"merge None h = h" |
+"merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ Some (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = Some h"
+| "merge_pairs (h1 # h2 # hs) = merge (merge (Some h1) (Some h2)) (merge_pairs hs)"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs hs"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+"php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun pheap :: "('a :: linorder) heap \<Rightarrow> bool" where
+"pheap None = True" |
+"pheap (Some h) = php h"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+"mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+"mset_heap None = {#}" |
+"mset_heap (Some h) = mset_hp h"
+
+lemma get_min_in: "get_min (Some h) \<in> set_hp(h)"
+by(cases h)(auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+by(cases h)(auto)
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_hp(mset hs))"
+by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge)
+
+lemma mset_del_min: "mset_heap (del_min (Some h)) = mset_hp h - {#get_min (Some h)#}"
+by(cases h) (auto simp: mset_merge_pairs)
+
+(*<*)
+end
+(*>*)
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Biendarra_Julian_julian.biendarra@tum.de_613/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Erhard_Julian_ga48kog@mytum.de_623/Ex13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,120 @@
+theory Ex13
+imports "~~/src/HOL/Library/Multiset"
+begin
+
+subsection \<open>Definitions\<close>
+
+text
+\<open>This implementation follows Okasaki \cite{Okasaki}.
+It satisfies the invariant that \<open>Empty\<close> only occurs
+at the root of a pairing heap. The functional correctness proof does not
+require the invariant but the amortized analysis (elsewhere) makes use of it.\<close>
+
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+"get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge h None = h" |
+"merge None h = h" |
+"merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then (Some (Hp x (Hp y ly # lx))) else (Some (Hp y (Hp x lx # ly))))"
+
+hide_const (open) insert
+
+fun insert :: "'a \<Rightarrow> ('a :: linorder) heap \<Rightarrow> 'a heap" where
+"insert x h = merge (Some (Hp x [])) h"
+
+fun merge_pairs :: "('a :: linorder) heap list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = h"
+| "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs (map Some hs)"
+
+
+subsection \<open>Correctness Proofs\<close>
+
+subsubsection \<open>Invariants\<close>
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+"php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+(*
+lemma pheap_merge: "php h1 \<Longrightarrow> php h2 \<Longrightarrow> php (merge (Some h1) (Some h2))"
+ sorry (*
+by (induction h1 h2 rule: merge.induct) fastforce+
+*)
+lemma pheap_insert: "pheap h \<Longrightarrow> pheap (insert x h)"
+ sorry (*
+by (auto simp: pheap_merge)
+*)
+lemma pheap_merge_pairs: "\<forall>h \<in> set hs. php h \<Longrightarrow> php (merge_pairs (map Some hs))"
+ sorry(*
+by(induction hs rule: merge_pairs.induct) (auto simp: pheap_merge)
+*)
+lemma pheap_del_min: "pheap h \<Longrightarrow> pheap (del_min h)"
+by(cases h) (auto intro!: pheap_merge_pairs)
+*)
+
+subsubsection \<open>Functional Correctness\<close>
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+"mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+"mset_heap None = {#}" |
+"mset_heap (Some (Hp x hs)) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+lemma get_min_in: "get_min (Some h) \<in> set_hp(h)"
+by(cases h)(auto)
+
+lemma get_min_min: "\<lbrakk>php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+by(cases h)(auto)
+
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_insert: "mset_heap (insert a h) = {#a#} + mset_heap h"
+by(cases h) (auto simp add: mset_merge insert_def add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_heap(mset hs))"
+by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge)
+
+lemma mset_heap_mset_hp: "mset_heap (Some h) = mset_hp h"
+ by (cases h) auto
+lemma mset_hp_mset_heap: "mset_hp h = mset_heap (Some h)"
+ by (cases h) auto
+
+lemma image_mset_heap_mset_hp: "image_mset mset_heap(mset (map Some xs)) = image_mset mset_hp(mset xs)"
+proof (induction xs)
+ case Nil
+ then show ?case by auto
+next
+ case (Cons a xs)
+ then show ?case
+ by (simp add: mset_heap_mset_hp)
+qed
+
+thm "mset_hp.simps"
+
+lemma mset_del_min: "mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+proof (cases h)
+ case (Hp x xs)
+ have a: "mset_hp (Hp x xs) = {#x#} + \<Union>#mset (map mset_hp xs) " by simp
+ from a have c: "mset_hp (Hp x xs) - {#get_min(Some (Hp x xs))#} = \<Union>#mset (map mset_hp xs)" by simp
+
+ have "mset_heap (del_min (Some (Hp x xs))) = mset_heap (merge_pairs (map Some xs)) " by simp
+ also have "... = Union_mset(image_mset mset_heap(mset (map Some xs)))" by (auto simp add: mset_merge_pairs)
+ also have "... = Union_mset(image_mset mset_hp(mset xs))" using image_mset_heap_mset_hp by metis
+ also have "... = \<Union>#mset (map mset_hp xs) " by auto
+
+ finally show ?thesis using c Hp by simp
+qed
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Erhard_Julian_ga48kog@mytum.de_623/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Gnther_Jochen_jochen.guenther@mytum.de_624/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,84 @@
+(*<*)
+theory hw13
+imports "~~/src/HOL/Library/Multiset"
+begin
+(*>*)
+
+text \<open>Homework Pairing Heap
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+subsection \<open>Definitions\<close>
+
+text
+\<open>This implementation follows Okasaki \cite{Okasaki}.
+It satisfies the invariant that \<open>Empty\<close> only occurs
+at the root of a pairing heap. The functional correctness proof does not
+require the invariant but the amortized analysis (elsewhere) makes use of it.\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge h None = h" |
+"merge None h = h" |
+"merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then Some (Hp x (Hp y ly # lx)) else Some (Hp y (Hp x lx # ly)))"
+
+fun merge_pairs :: "('a :: linorder) heap list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = h"
+| "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs (map Some hs)"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+ "mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}" |
+ "mset_heap (Some (Hp x hs)) = mset_hp (Hp x hs)"
+
+
+(* HINT: Start with a copy of the original lemmas, and modify as needed *)
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+ by(cases h)(auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by(cases h)(auto)
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+ by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_heap(mset hs))"
+ by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge)
+
+lemma aux: "image_mset mset_heap (image_mset Some (mset x2)) = image_mset mset_hp (mset x2)"
+ by (metis (no_types, hide_lams) hp.exhaust image_mset_cong mset_heap.simps(2) multiset.map_comp o_apply)
+(* by (metis image_mset_cong mset_heap.simps(2) mset_hp.cases multiset.map_comp o_apply) *)
+
+lemma mset_del_min:
+ "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ by(cases h) (auto simp: mset_merge_pairs aux)
+
+(*<*)
+end
+(*>*)
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Gnther_Jochen_jochen.guenther@mytum.de_624/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Groer_Markus_markus.grosser@tum.de_635/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,67 @@
+(* Original Author: Tobias Nipkow *)
+
+theory hw13
+ imports "~~/src/HOL/Library/Multiset"
+begin
+
+subsection \<open>Definitions\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min None = undefined"
+| "get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+ "merge h None = h"
+| "merge None h = h"
+| "merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then Some (Hp x (Hp y ly # lx)) else Some (Hp y (Hp x lx # ly)))"
+
+fun merge_pairs :: "('a :: linorder) heap list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = h"
+| "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs (map Some hs)"
+
+subsection \<open>Correctness Proofs\<close>
+
+subsubsection \<open>Invariants\<close>
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+subsubsection \<open>Functional Correctness\<close>
+
+fun mset_hp :: "'a hp \<Rightarrow> 'a multiset" where
+ "mset_hp (Hp x hs) = {#x#} + Union_mset (mset (map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}"
+| "mset_heap (Some h) = mset_hp h"
+
+lemma get_min_in: "get_min (Some h) \<in> set_hp h"
+ by (cases h) auto
+
+lemma get_min_min: "\<lbrakk>php h; x \<in> set_hp h\<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by (cases h) auto
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+ by (induction h1 h2 rule: merge.induct) (auto simp: add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_heap(mset hs))"
+ by (induction hs rule: merge_pairs.induct) (auto simp: mset_merge)
+
+lemma mset_del_min: "mset_heap (del_min (Some h)) = mset_hp h - {#get_min (Some h)#}"
+ apply (cases h)
+ apply (simp add: mset_merge_pairs multiset.map_comp)
+ apply (metis comp_apply[of mset_heap Some] mset_heap.simps(2))
+ done \<comment> \<open>I am not very happy with this proof\<close>
+
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Groer_Markus_markus.grosser@tum.de_635/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Haslbeck_Maximilian_max.haslbeck@mytum.de_622/ex13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,136 @@
+(*<*)
+theory ex13
+imports "../Thys/Skew_Heap"
+begin
+(*>*)
+
+text {* \ExerciseSheet{13}{21.~7.~2017} *}
+
+
+text \<open>
+\Exercise{Double-Ended Queues}
+
+Design a double-ended queue where all operations have constant-time amortized
+complexity. Prove functional correctness and constant-time amortized complexity.
+
+For your proofs, it is enough to count the number of newly allocated list cells.
+You may assume that operations @{term \<open>rev xs\<close>} and @{term \<open>xs@ys\<close>} allocate \<open>O(|xs|)\<close>
+cells.
+
+Explanation: A double-ended queue is like a queue with two further operations:
+Function \<open>enq_front\<close> adds an element at the front (whereas \<open>enq\<close> adds an element at the back).
+Function \<open>deq_back\<close> removes an element at the back (whereas \<open>deq\<close> removes an element at the front).
+Here is a formal specification where the double ended queue is just a list:
+\<close>
+
+abbreviation (input) enq_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"enq_list x xs \<equiv> xs @ [x]"
+
+abbreviation (input) enq_front_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"enq_front_list x xs \<equiv> x # xs"
+
+abbreviation (input) deq_list :: "'a list \<Rightarrow> 'a list" where
+"deq_list xs \<equiv> tl xs"
+
+abbreviation (input) deq_back_list :: "'a list \<Rightarrow> 'a list" where
+"deq_back_list xs \<equiv> butlast xs"
+
+text\<open>
+Hint: You may want to start with the \<open>Queue\<close> implementation in \<open>Thys/Amortized_Examples\<close>.\<close>
+
+type_synonym 'a queue = unit
+
+consts list_of :: "'a queue \<Rightarrow> 'a list"
+
+(* Definitions *)
+
+consts
+ init :: "'a queue"
+ enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue"
+ enq_front :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue"
+ deq :: "'a queue \<Rightarrow> 'a queue"
+ deq_back :: "'a queue \<Rightarrow> 'a queue"
+
+lemma "list_of init = []" oops
+
+lemma "list_of(enq x q) = enq_list x (list_of q)" oops
+
+lemma "list_of(enq_front x q) = enq_front_list x (list_of q)" oops
+
+lemma "list_of q \<noteq> [] \<Longrightarrow> list_of(deq q) = deq_list (list_of q)" oops
+
+lemma "list_of q \<noteq> [] \<Longrightarrow> list_of(deq_back q) = deq_back_list (list_of q)" oops
+
+
+(* Define timing functions, counting number of allocated list cells *)
+
+(* Define \<Phi>, and show the standard lemmas, and estimate the amortized
+ complexity of the operations to be constant time *)
+
+
+text \<open>
+ \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) hp \<Rightarrow> 'a hp \<Rightarrow> 'a hp" where
+"merge (Hp x lx) (Hp y ly) =
+ (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a hp" where
+ "merge_pairs [h] = h" |
+ "merge_pairs (h1 # h2 # []) = (merge h1 h2)" |
+ "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+ "del_min None = None" |
+ "del_min (Some (Hp x [])) = None" |
+ "del_min (Some (Hp x hs)) = Some (merge_pairs hs)"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+ "mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}" |
+ "mset_heap (Some h) = mset_hp h"
+
+(* HINT: Start with a copy of the original lemmas, and modify as needed *)
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+ by (induction h) (auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by (induction h) (auto)
+
+lemma mset_hp_merge: "mset_hp (merge h1 h2) = mset_hp h1 + mset_hp h2"
+ by (induction h1 h2 rule: merge.induct) (auto)
+
+lemma mset_hp_merge_pairs:
+ "hs \<noteq> [] \<Longrightarrow> mset_hp (merge_pairs hs) = Union_mset(mset(map mset_hp hs))"
+ by (induction hs rule: merge_pairs.induct) (auto simp add: mset_hp_merge)
+
+lemma mset_del_min:
+ "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ by (induction "Some h" rule: del_min.induct) (auto simp add: mset_hp_merge_pairs)
+
+(*<*)
+end
+(*>*)
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Haslbeck_Maximilian_max.haslbeck@mytum.de_622/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hellauer_Fabian_f.hellauer@tum.de_616/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,73 @@
+theory hw13
+ imports "../../../Public/Thys/Skew_Heap"
+begin
+
+text \<open>
+ \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp a _)) = a"
+
+fun merge :: "('a :: linorder) hp \<Rightarrow> 'a hp \<Rightarrow> 'a hp" where
+"merge (Hp x lx) (Hp y ly) = (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))"
+
+fun insert :: "'a \<Rightarrow> ('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "insert x None = Some (Hp x [])" |
+ "insert x (Some hp) = Some (merge (Hp x []) hp)"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a hp" where
+ "merge_pairs [h] = h"
+| "merge_pairs [h1,h2] = merge h1 h2"
+| "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = (if hs = [] then None else Some (merge_pairs hs))"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+ "mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}" |
+ "mset_heap (Some hp) = mset_hp hp"
+
+(* HINT: Start with a copy of the original lemmas, and modify as needed *)
+
+theorem get_min_in: "get_min (Some h) \<in> set_hp(h)"
+ by (cases h) auto
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by (cases h) auto
+
+lemma mset_merge: "mset_hp (merge h1 h2) = mset_hp h1 + mset_hp h2"
+ by(induction h1 h2 rule: merge.induct) auto
+
+lemma mset_merge_pairs: "hs \<noteq> [] \<Longrightarrow> mset_hp (merge_pairs hs) = Union_mset(image_mset mset_hp(mset hs))"
+ apply (induction hs rule: merge_pairs.induct)
+ apply (auto simp: mset_merge)
+ done
+
+lemma mset_del_min:
+ "mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ apply (cases h)
+ apply (auto simp: mset_merge_pairs)
+ done
+
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hellauer_Fabian_f.hellauer@tum.de_616/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hu_Shuwei_shuwei.hu@tum.de_614/Homework13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,51 @@
+theory Homework13
+imports "material/Thys/Skew_Heap"
+begin
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x hs)) = x"
+
+fun merge :: "('a :: linorder) hp \<Rightarrow> 'a hp \<Rightarrow> 'a hp" where
+"merge (Hp x lx) (Hp y ly) =
+ (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a hp" where
+ "merge_pairs [h] = h"
+| "merge_pairs [h1, h2] = merge h1 h2"
+| "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+ "del_min (Some (Hp x hs)) = (if hs=[] then None else Some (merge_pairs hs))"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) \<longleftrightarrow> (\<forall>h\<in>set hs. (\<forall>y\<in>set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+ "mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}"
+| "mset_heap (Some h) = mset_hp h"
+
+(* HINT: Start with a copy of the original lemmas, and modify as needed *)
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+ by (cases h) auto
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by (cases h) auto
+
+lemma mset_merge: "mset_hp (merge h1 h2) = mset_hp h1 + mset_hp h2"
+ by (induction h1 h2 rule: merge.induct) (auto simp: add_ac)
+
+lemma mset_merge_pairs: "hs \<noteq> [] \<Longrightarrow> mset_hp (merge_pairs hs) = Union_mset(image_mset mset_hp (mset hs))"
+ by (induction hs rule: merge_pairs.induct) (auto simp: mset_merge)
+
+lemma mset_del_min:
+ "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ by (cases h) (auto simp: mset_merge_pairs)
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hu_Shuwei_shuwei.hu@tum.de_614/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hutzler_Matthias_ga95luy@mytum.de_650/ex13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,23 @@
+theory ex13
+ imports Complex_Main
+ "~~/src/HOL/Library/Multiset"
+begin
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x _)) = x"
+
+fun mset_hp :: "'a hp \<Rightarrow> 'a multiset" where
+ "mset_hp (Hp x l) = {#x#} + Union_mset(mset(map mset_hp l))"
+
+fun mset_heap :: "'a heap \<Rightarrow> 'a multiset" where
+ "mset_heap None = {#}" |
+ "mset_heap (Some hp) = mset_hp hp"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x l) = (\<forall>h\<in> set l. (\<forall>y\<in>#mset_hp h. x\<le>y) \<and> php h)"
+
+fun set_hp :: "'a hp \<Rightarrow> 'a set" where
+ "set_hp h = set_mset (mset_hp h)"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hutzler_Matthias_ga95luy@mytum.de_650/user_error_log.txt Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,4 @@
+Using temporary directory '/tmp/tmp.xhsmymVQmJ'
+Files in /tmp/eval-650-4okIhk: ex13.thy
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Keinholz_Jonas_jonas.keinholz@tum.de_612/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,60 @@
+theory hw13
+ imports "~~/src/HOL/Library/Multiset"
+begin
+
+subsection \<open>Definitions\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge h None = h" |
+"merge None h = h" |
+"merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then Some (Hp x (Hp y ly # lx)) else Some (Hp y (Hp x lx # ly)))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = Some h"
+| "merge_pairs (h1 # h2 # hs) = merge (merge (Some h1) (Some h2)) (merge_pairs hs)"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs hs"
+
+subsection \<open>Correctness Proofs\<close>
+
+subsubsection \<open>Invariants\<close>
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) \<longleftrightarrow> (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+subsubsection \<open>Functional Correctness\<close>
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+ "mset_hp (Hp x hs) = {#x#} + Union_mset (mset (map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}"
+| "mset_heap (Some h) = mset_hp h"
+
+lemma get_min_in: "get_min (Some h) \<in> set_hp h"
+ by (cases h) (auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp h \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by (cases h) (auto)
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+ by(induction h1 h2 rule: merge.induct) (auto simp: add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset (image_mset mset_hp (mset hs))"
+ by (induction hs rule: merge_pairs.induct) (auto simp: mset_merge)
+
+lemma mset_del_min: "mset_heap (del_min (Some h)) = mset_hp h - {#get_min (Some h)#}"
+ by (cases h) (auto simp: mset_merge_pairs)
+
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Keinholz_Jonas_jonas.keinholz@tum.de_612/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Kurz_Friedrich_friedrich.kurz@tum.de_645/hw_13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,153 @@
+(*<*)
+theory hw_13
+imports "../../../Public/Thys/Skew_Heap"
+begin
+(*>*)
+
+text {* \ExerciseSheet{13}{21.~7.~2017} *}
+
+
+text \<open>
+\Exercise{Double-Ended Queues}
+
+Design a double-ended queue where all operations have constant-time amortized
+complexity. Prove functional correctness and constant-time amortized complexity.
+
+For your proofs, it is enough to count the number of newly allocated list cells.
+You may assume that operations @{term \<open>rev xs\<close>} and @{term \<open>xs@ys\<close>} allocate \<open>O(|xs|)\<close>
+cells.
+
+Explanation: A double-ended queue is like a queue with two further operations:
+Function \<open>enq_front\<close> adds an element at the front (whereas \<open>enq\<close> adds an element at the back).
+Function \<open>deq_back\<close> removes an element at the back (whereas \<open>deq\<close> removes an element at the front).
+Here is a formal specification where the double ended queue is just a list:
+\<close>
+
+abbreviation (input) enq_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"enq_list x xs \<equiv> xs @ [x]"
+
+abbreviation (input) enq_front_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"enq_front_list x xs \<equiv> x # xs"
+
+abbreviation (input) deq_list :: "'a list \<Rightarrow> 'a list" where
+"deq_list xs \<equiv> tl xs"
+
+abbreviation (input) deq_back_list :: "'a list \<Rightarrow> 'a list" where
+"deq_back_list xs \<equiv> butlast xs"
+
+text\<open>
+Hint: You may want to start with the \<open>Queue\<close> implementation in \<open>Thys/Amortized_Examples\<close>.\<close>
+
+type_synonym 'a queue = unit
+
+consts list_of :: "'a queue \<Rightarrow> 'a list"
+
+(* Definitions *)
+
+consts
+ init :: "'a queue"
+ enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue"
+ enq_front :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue"
+ deq :: "'a queue \<Rightarrow> 'a queue"
+ deq_back :: "'a queue \<Rightarrow> 'a queue"
+
+lemma "list_of init = []" oops
+
+lemma "list_of(enq x q) = enq_list x (list_of q)" oops
+
+lemma "list_of(enq_front x q) = enq_front_list x (list_of q)" oops
+
+lemma "list_of q \<noteq> [] \<Longrightarrow> list_of(deq q) = deq_list (list_of q)" oops
+
+lemma "list_of q \<noteq> [] \<Longrightarrow> list_of(deq_back q) = deq_back_list (list_of q)" oops
+
+
+(* Define timing functions, counting number of allocated list cells *)
+
+(* Define \<Phi>, and show the standard lemmas, and estimate the amortized
+ complexity of the operations to be constant time *)
+
+text \<open>
+ \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+(*
+fun get min :: “ ( ′a :: linorder ) heap \<Rightarrow> ′a†where
+fun del min :: “ ′a :: linorder heap \<Rightarrow> ′a heapâ€
+where fun php :: “(′a :: linorder) hp \<Rightarrow> bool†where
+fun mset hp :: “ ′a hp \<Rightarrow>′a multiset†where
+fun mset heap :: “ ′a heap \<Rightarrow>′a multiset†where
+*)
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min None = undefined"
+ | "get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+ "merge None h = h"
+| "merge h None = h"
+| "merge (Some (Hp x1 l1)) (Some (Hp x2 l2)) = (if x1 < x2
+ then (Some (Hp x1 (Hp x2 l2 # l1)))
+ else (Some (Hp x2 (Hp x1 l1 # l2)))
+)"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = (Some h)"
+| "merge_pairs (h1 # h2 # hs) = (merge (merge (Some h1) (Some h2)) (merge_pairs hs))"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+ "del_min None = undefined"
+ | "del_min (Some (Hp x l)) = merge_pairs l"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow> 'a multiset" where
+ "mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}"
+| "mset_heap (Some h) = mset_hp h"
+
+
+(* HINT: Start with a copy of the original lemmas, and modify as needed *)
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+ apply(induction h)
+ apply(auto)
+ done
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ apply(induction h)
+ apply(auto)
+ done
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_hp(mset hs))"
+ unfolding image_mset_def
+ apply(induction hs rule: merge_pairs.induct)
+ subgoal by simp
+ subgoal by (metis comp_def comp_fun_commute.fold_mset_add_mset comp_fun_commute_mset_image fold_mset_empty merge_pairs.simps(2) mset_heap.simps(2) mset_single_iff_right sum_mset.singleton)
+ subgoal sorry
+ done
+
+lemma mset_del_min:
+ "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ apply(induction h)
+ apply(auto simp add: mset_merge_pairs)
+ done
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Kurz_Friedrich_friedrich.kurz@tum.de_645/user_error_log.txt Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,6 @@
+Using temporary directory '/tmp/tmp.Wv6lTfCF2D'
+Files in /tmp/eval-645-OjgXvL: hw_13.thy
+Submission did not check in Isabelle!
+Test case check_build: Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Madge_Pimentel_Fabio_fabio.madge@tum.de_626/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Madge_Pimentel_Fabio_fabio.madge@tum.de_626/tmpl13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,80 @@
+(*<*)
+theory tmpl13
+imports "Skew_Heap"
+begin
+(*>*)
+
+text \<open>
+ \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp m _)) = m"
+
+fun merge :: "('a :: linorder) hp \<Rightarrow> 'a hp \<Rightarrow> 'a hp" where
+ "merge (Hp l xs) (Hp r ys) = (if l \<le> r then Hp r (Hp l [] # xs @ ys) else Hp l (Hp r [] # xs @ ys))"
+
+fun merge_list :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_list [] = None" |
+ "merge_list (x#xs) = combine_options merge (Some x) (merge_list xs)"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+ "del_min None = None" |
+ "del_min (Some (Hp m r)) = merge_list r"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+ "mset_hp (Hp m r) = {#m#} + Union_mset(mset(map mset_hp r))"
+
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = Mempty" |
+ "mset_heap (Some hp) = mset_hp hp"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+ (* HINT: Start with a copy of the original lemmas, and modify as needed *)
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+ by(cases h)(auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp h \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by (cases h) auto
+
+lemma mset_merge: "mset_hp (merge h1 h2) = mset_hp h1 + mset_hp h2"
+ by (induction h1 h2 rule: merge.induct) auto
+
+lemma mset_merge_pairs: "mset_heap (merge_list hs) = Union_mset(image_mset mset_hp (mset hs))"
+ apply (induction hs rule: merge_list.induct)
+ apply simp_all
+proof -
+ fix x :: "'a hp" and xs :: "'a hp list"
+ assume a1: "mset_heap (merge_list xs) = \<Union>#image_mset mset_hp (mset xs)"
+ have f2: "\<And>h ha. mset_heap (combine_options merge (Some (h::'a hp)) (Some ha)) = mset_hp h + mset_hp ha"
+ by (simp add: mset_merge)
+ have "None = merge_list xs \<longrightarrow> mset_heap (combine_options merge (Some x) (merge_list xs)) = {#} + mset_hp x"
+ by simp
+ then show "mset_heap (combine_options merge (Some x) (merge_list xs)) = mset_hp x + \<Union>#image_mset mset_hp (mset xs)"
+ using a1 f2 by (metis mset_heap.simps option.exhaust union_commute)
+qed
+
+lemma mset_del_min:
+ "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ by (cases h) (auto simp: mset_merge_pairs)
+
+(*<*)
+end
+(*>*)
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Ouyang_Lena_ga96vup@mytum.de_627/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,317 @@
+theory hw13
+imports Complex_Main
+ "~~/src/HOL/Library/Multiset"
+ "../../../../Desktop/fds/Thys/Priority_Queue"
+ "../../../../Desktop/fds/Thys/Heap_Prelim"
+begin
+subsection \<open>Pairing_Heap\<close>
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+(*renamed some functions with a two as a hack to prevent same name function clashes*)
+fun get_min2 :: "('a :: linorder) heap \<Rightarrow> 'a" where
+"get_min2 (Some (Hp x y)) = x"
+fun merge2 :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge2 h None = h" |
+"merge2 None h = h" |
+"merge2 (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then Some (Hp x (Hp y ly # lx)) else Some (Hp y (Hp x lx # ly)))"
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = Some h"
+| "merge_pairs (h1 # h2 # hs) = merge2 (merge2 (Some h1) (Some h2)) (merge_pairs hs)"
+fun del_min2 :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min2 None = None"
+| "del_min2 (Some (Hp x hs)) = merge_pairs hs"
+
+subsection \<open>Correctness Proofs\<close>
+subsubsection \<open>Invariants\<close>
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+"php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+(*no preservation of invariant lemmas needed*)
+
+subsubsection \<open>Functional Correctness\<close>
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+"mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+fun mset_heap2 :: "'a heap \<Rightarrow>'a multiset" where
+"mset_heap2 None = {#}" |
+"mset_heap2 (Some (Hp x hs)) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+theorem get_min_in: "get_min2 (Some h) \<in> set_hp(h)"
+ by(cases h)(auto)
+lemma get_min_min: "\<lbrakk>php h; x \<in> set_hp(h)\<rbrakk> \<Longrightarrow> get_min2 (Some h) \<le> x"
+ by(cases h)(auto)
+lemma mset_merge: "mset_heap2 (merge2 h1 h2) = mset_heap2 h1 + mset_heap2 h2"
+ by(induction h1 h2 rule: merge2.induct)(auto simp: add_ac)
+lemma aux: "mset_heap2 (Some h1) = mset_hp h1"
+ by (cases h1) auto
+lemma mset_merge_pairs: "mset_heap2 (merge_pairs hs) = Union_mset(image_mset mset_hp(mset hs))"
+ by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge aux)
+lemma mset_del_min: "mset_heap2 (del_min2 (Some h)) = mset_hp h - {#get_min2 (Some h)#}"
+ by(cases h) (auto simp: mset_merge_pairs)
+
+text \<open>Project\<close>
+section \<open>Fibonacci Heaps\<close>
+datatype 'a Node = Node (rank: nat) (root: 'a) (children: "'a Node list")
+type_synonym 'a Heap = "'a Node list"
+
+subsection \<open>Multiset\<close>
+fun mset_node :: "'a::linorder Node \<Rightarrow> 'a multiset" where
+ "mset_node (Node _ a c) = {#a#} + (\<Sum>t\<in>#mset c. mset_node t)"
+fun mset_heap :: "'a::linorder Heap \<Rightarrow> 'a multiset" where
+ "mset_heap x = (\<Sum>t\<in>#mset x. mset_node t)"
+
+lemma mset_node[simp]: "mset_node (Node r a c) = {#a#} + mset_heap c" by auto
+lemma mset_node_nonempty[simp]: "mset_node t \<noteq> {#}" by (cases t) auto
+lemma mset_heap_nil[simp]: "mset_heap [] = {#}" by auto
+lemma mset_heap_cons[simp]: "mset_heap (t#ts) = mset_node t + mset_heap ts" by auto
+lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]" by auto
+lemma root_in_mset[simp]: "root t \<in># mset_node t" by (cases t) auto
+lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts" by auto
+
+subsection \<open>Invariants\<close>
+text \<open>FibHeap invariant:
+In a Fibonacci Heap the first element is the minimum,
+the rest doesn't have to be sorted after rank nor root\<close>
+fun "node_invar" :: "'a::linorder Node \<Rightarrow> bool" where
+ "node_invar (Node r a []) = (\<forall>t\<in>#mset []. node_invar t \<and> a \<le> root t)"|
+ "node_invar (Node r a (x#xs)) = (\<forall>t\<in>#mset (x#xs). node_invar t \<and> a \<le> root t \<and> root x \<le> root t)"
+fun heap_invar :: "'a::linorder Heap \<Rightarrow> bool" where
+ "heap_invar [] = True"|
+ "heap_invar (x#xs) = (\<forall>t\<in>#mset (x#xs). node_invar t \<and> root x \<le> root t)"
+definition invar :: "'a::linorder Heap \<Rightarrow> bool" where
+ "invar x = heap_invar x"
+
+subsection \<open>Operations\<close>
+fun insert :: "'a::linorder \<Rightarrow> 'a Heap \<Rightarrow> 'a Heap" where
+ "insert a ((Node r x c)#xs) = (if a < x then (Node 0 a [])#(Node r x c)#xs else (Node r x c)#(Node 0 a [])#xs)"|
+ "insert a [] = [(Node 0 a [])]"
+
+lemma insert_heap_invar: "heap_invar ts \<Longrightarrow> heap_invar (insert t ts)"
+ by (induction t ts rule: insert.induct)(auto simp:less_eq_Suc_le[symmetric])
+lemma children_heap_invar:"node_invar (Node r a ts) \<Longrightarrow> heap_invar ts" by (cases ts) auto
+lemma heap_invar_cons: "heap_invar (x#xs) \<Longrightarrow> node_invar x \<and> (\<forall>t\<in>#mset (x#xs). root x \<le> root t)" by auto
+lemma insert_mset: "mset_heap (insert t ts) = {#t#} + mset_heap ts" by (induction t ts rule: insert.induct) auto
+lemma insert_invar: "invar t \<Longrightarrow> invar (insert x t)" unfolding invar_def by (auto simp: insert_heap_invar)
+
+fun merge :: "'a::linorder Heap \<Rightarrow> 'a Heap \<Rightarrow> 'a Heap" where
+ "merge xs [] = xs"
+| "merge [] xs = xs"
+| "merge (x#xs) (y#ys) = (if root x < root y then x#xs@y#ys else y#ys@x#xs)"
+
+lemma merge_simp2: "merge [] xs = xs" by (cases xs) auto
+lemma merge_heap_invar:
+ assumes "heap_invar xs"
+ assumes "heap_invar ys"
+ shows "heap_invar (merge xs ys)"
+ using assms by (induction xs ys rule: merge.induct) auto
+lemma merge_invar: "\<lbrakk> invar xs; invar ys \<rbrakk> \<Longrightarrow> invar (merge xs ys)"
+ unfolding invar_def by (auto simp: merge_heap_invar)
+lemma merge_mset: "mset_heap (merge xs ys) = mset_heap xs + mset_heap ys"
+ by (induction xs ys rule: merge.induct) auto
+
+fun get_min :: "'a::linorder Heap \<Rightarrow> 'a" where
+ "get_min (t#ts) = root t"
+
+lemma node_invar_root_min:
+ assumes "node_invar t"
+ assumes "x \<in># mset_node t"
+ shows "root t \<le> x"
+ using assms
+ proof (induction t arbitrary: x rule: mset_node.induct)
+ case (1 uu a c)
+ then show ?case sorry
+ (*proof -
+ have a: "node_invar (Node uu a c) \<Longrightarrow> (\<forall>t\<in>#mset c. a \<le> root t)" by (smt Node.sel(2) Node.sel(3) node_invar.elims(2))
+ then have "mset_node (Node uu a c) = {#a#} + (\<Sum>t\<in>#mset c. mset_node t)"
+ by (meson mset_node.simps)
+ also have "... = {#a#} + mset_heap c" by simp
+ also have "... = {#a#} + (\<Sum>t\<in>#mset c. mset_node t)" by simp
+ then have "x \<in># mset_node (Node uu a c) \<Longrightarrow> x \<in># {#a#} + (\<Sum>t\<in>#mset c. mset_node t)"
+ using "1.prems"(2) by auto
+ then have "(x \<in># {#a#}) \<or> (x \<in># (\<Sum>t\<in>#mset c. mset_node t))"
+ using "1.prems"(2) by auto
+ then show ?thesis
+ proof
+ assume "x \<in># {#a#}"
+ then have ?thesis by simp
+ next
+ assume "x \<in># (\<Sum>t\<in>#mset c. mset_node t)"
+ then have ?thesis using 1 a sorry
+ qed*)
+ qed
+
+lemma get_min_mset_aux:
+ assumes "ts\<noteq>[]"
+ assumes "heap_invar ts"
+ assumes "x \<in># mset_heap ts"
+ shows "get_min ts \<le> x"
+ using assms
+ by (induction ts arbitrary: x rule: get_min.induct)
+ (auto simp: node_invar_root_min intro: order_trans;
+ meson linear order_trans node_invar_root_min)+
+lemma get_min_mset:
+ assumes "ts\<noteq>[]"
+ assumes "invar ts"
+ assumes "x \<in># mset_heap ts"
+ shows "get_min ts \<le> x"
+ using assms unfolding invar_def by (auto simp: get_min_mset_aux)
+lemma get_min_member:
+ assumes "ts\<noteq>[]"
+ shows "get_min ts \<in># mset_heap ts"
+ using assms by (induction ts rule: get_min.induct) auto
+lemma get_min:
+ assumes "mset_heap ts \<noteq> {#}"
+ assumes "invar ts"
+ shows "get_min ts = Min_mset (mset_heap ts)"
+ apply rule
+ using assms get_min_member get_min_mset by auto
+
+fun merge_node ::"'a::linorder Node \<Rightarrow> 'a Node \<Rightarrow> 'a Node " where
+ "merge_node (Node r a c) (Node s b d) = (if a < b then (Node (s+1) a ((Node s b d)#c)) else
+ (Node (r+1) b ((Node r a c)#d)))"
+fun lookup :: "nat \<Rightarrow> 'a Node list \<Rightarrow> 'a Node option" where
+ "lookup x [] = None"|
+ "lookup x ((Node r a c)#xs) = (if r = x then Some (Node r a c) else lookup x xs)"
+fun consolidate :: "'a::linorder Heap \<Rightarrow> 'a Node list \<Rightarrow> 'a Heap" where
+ "consolidate [] l = l"|
+ "consolidate (x#xs) l = (
+ case lookup (rank x) l of None \<Rightarrow> consolidate xs (x#l)
+ |Some t \<Rightarrow> consolidate xs ((merge_node x t)#(filter (\<lambda>q. rank q \<noteq> rank x) l))
+ )"
+fun update_min :: "'a::linorder Heap \<Rightarrow>'a::linorder Heap \<Rightarrow> 'a Node \<Rightarrow> 'a::linorder Heap" where
+ "update_min h [] a = (a#h)"|
+ "update_min h (x#xs) a = (if root x < root a then update_min (a#h) xs x else update_min (x#h) xs a)"
+fun delete_min :: "'a::linorder Heap \<Rightarrow> 'a::linorder Heap" where
+ "delete_min [] = []"|
+ "delete_min (x#xs) = update_min [] (tl (consolidate ((children x)@xs) [])) (hd (consolidate ((children x)@xs) []))"
+lemma update_min_invar: "(\<forall>t\<in>#mset (xs). node_invar t) \<and> (\<forall>t\<in>#mset (h). node_invar t \<and> root t \<ge> root x) \<and> node_invar x
+ \<Longrightarrow> invar (update_min h xs x)"
+ unfolding invar_def apply (induction h xs x rule: update_min.induct)
+ by auto fastforce
+lemma delete_min_invar[simp]:
+ assumes "ts \<noteq> []"
+ assumes "invar ts"
+ shows "invar (delete_min ts)"
+ using assms update_min_invar unfolding invar_def sorry
+lemma delete_min_mset:
+ assumes "ts \<noteq> []"
+ shows "mset_heap ts = mset_heap (delete_min ts) + {# find_min ts #}"
+ using assms sorry
+
+subsection \<open>Complexity\<close>
+fun t_insert :: "'a::linorder \<Rightarrow> 'a Heap \<Rightarrow> nat" where
+ "t_insert a ((Node r x c)#xs) = 1"| (*(if, Node cons, # cons, Node cons, # cons)*)
+ "t_insert a [] = 1"
+lemma t_insert_simple_bound: "t_insert t ts \<le> 5" for t
+ by (induction t ts rule: t_insert.induct) auto
+fun t_merge :: "'a::linorder Heap \<Rightarrow> 'a Heap \<Rightarrow> nat" where
+ "t_merge xs [] = 1"
+| "t_merge [] xs = 1"
+| "t_merge (x#xs) (y#ys) = 4" (*(if, # cons, @ cons, # cons)*)
+lemma l_merge_estimate:
+ "t_merge xs ys \<le> 4"
+ apply (induction xs ys rule: t_merge.induct)
+ apply auto
+ done
+fun t_get_min :: "'a::linorder Heap \<Rightarrow> nat" where
+ "t_get_min (t#ts) = 1"
+fun t_merge_node ::"'a::linorder Node \<Rightarrow> 'a Node \<Rightarrow> nat" where
+ "t_merge_node a b = 1"
+fun t_lookup :: "nat \<Rightarrow> 'a Node list \<Rightarrow> nat" where
+ "t_lookup x [] = 1"|
+ "t_lookup x ((Node r a c)#xs) = 1 + (if r = x then 0 else t_lookup x xs)"
+fun t_consolidate :: "'a::linorder Heap \<Rightarrow> 'a Node list \<Rightarrow> nat" where
+ "t_consolidate [] l = 1"|
+ "t_consolidate (x#xs) l = t_lookup (rank x) l + (
+ case lookup (rank x) l of None \<Rightarrow> 1 + t_consolidate xs (x#l)
+ |Some t \<Rightarrow> 1 + t_consolidate xs ((merge_node x t)#(filter (\<lambda>q. rank q \<noteq> rank x) l))
+ )"
+fun t_update_min :: "'a::linorder Heap \<Rightarrow>'a::linorder Heap \<Rightarrow> 'a Node \<Rightarrow> nat" where
+ "t_update_min h [] a = 1"|
+ "t_update_min h (x#xs) a = 1 + (if root x < root a then t_update_min (a#h) xs x else t_update_min (x#h) xs a)"
+fun t_delete_min :: "'a::linorder Heap \<Rightarrow> nat" where
+ "t_delete_min [] = 1"|
+ "t_delete_min (x#xs) = 1 + t_consolidate ((children x)@xs) [] + t_update_min [] (tl (consolidate ((children x)@xs) [])) (hd (consolidate ((children x)@xs) []))"
+lemma sumrule:
+ fixes n::nat
+ shows"(\<Sum>i=0..n. i) = n*(n+1) div 2"
+ proof (induct n)
+ case 0
+ have "(\<Sum>i=0..0. i) = (0::nat)" by simp
+ also have "... = 0*(0+1) div 2" by simp
+ finally show ?case .
+ next
+ case (Suc n)
+ have "(\<Sum>i=0..Suc n. i) = (\<Sum>i=0..n. i) + (n+1)" by simp
+ also have "... = n*(n+1) div 2 + (n+1)" by (simp add : Suc.hyps)
+ also have "... = (n*(n+1) + 2 *(n+1)) div 2" by simp
+ also have "... = (Suc n*(Suc n+1)) div 2" by simp
+ finally show ?case .
+qed
+lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = 1"
+ by (induction ts rule: t_get_min.induct) auto
+lemma t_merge_node_estimate[simp]: "t_merge_node x y = 1" by auto
+lemma t_lookup_estimate[simp]: "t_lookup x l \<le> 1 + size l" apply (induction x l rule: t_lookup.induct) apply auto done
+lemma t_consolidate_estimate[simp]: "t_consolidate x l \<le> 1 + size l + 1 + (size x)^3"
+proof (induction x l rule: t_consolidate.induct)
+ case (1 l)
+ then show ?case by auto
+next
+ case (2 x xs l)
+ thm "2.IH"
+ then show ?case
+ proof (cases "lookup (rank x) l")
+ case None
+ then have "t_consolidate (x#xs) l \<le> 1 + size l + 1 + t_consolidate xs (x#l)" using t_lookup_estimate by auto
+ then show ?thesis sorry
+next
+ case (Some a)
+ then show ?thesis sorry
+qed
+ (*"t_consolidate (x#xs) l = t_lookup (rank x) l + (
+ case lookup (rank x) l of None \<Rightarrow> 1 + t_consolidate xs (x#l)
+ |Some t \<Rightarrow> 1 + t_consolidate xs ((merge_node x t)#(filter (\<lambda>q. rank q \<noteq> rank x) l))
+ )"*)
+qed
+lemma t_update_min_estimate:"t_update_min h x a \<le> 1 + size x"
+ by(induction h x a rule: t_update_min.induct) auto
+lemma t_delete_min_estimate:
+ fixes ts
+ defines "n \<equiv> size (mset_heap ts)"
+ assumes "invar ts"
+ assumes "ts\<noteq>[]"
+ shows "t_delete_min (x#xs) = 4 + (size ((children x)@xs))^3 + size ((children x)@xs)"
+ using assms unfolding invar_def sorry
+
+(*TODO: amortized*)
+
+subsection \<open>Instantiating the Priority Queue Locale\<close>
+interpretation fibheap:
+ Priority_Queue "[]" "op = []" insert get_min delete_min invar mset_heap
+proof (unfold_locales, goal_cases)
+ case 1
+ then show ?case by simp
+next
+ case (2 q)
+ then show ?case by auto
+next
+ case (3 q x)
+ then show ?case using insert_mset by auto
+next
+ case (4 q)
+ then show ?case using delete_min_mset sorry
+next
+ case (5 q)
+ then show ?case using get_min[of q] by auto
+next
+ case 6
+ then show ?case by (auto simp add: invar_def)
+next
+ case (7 q x)
+ then show ?case by (auto simp: insert_invar)
+next
+ case (8 q)
+ then show ?case by auto
+qed
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Ouyang_Lena_ga96vup@mytum.de_627/user_error_log.txt Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,6 @@
+Using temporary directory '/tmp/tmp.LQO20FAA1T'
+Files in /tmp/eval-627-tKoPGK: hw13.thy
+Submission did not check in Isabelle!
+Test case check_build: Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Rdle_Karl_Jonas_jonas.raedle@tum.de_621/hw13_sub.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,71 @@
+(*<*)
+theory hw13_sub
+ imports "../../../Public/Thys/Skew_Heap"
+begin
+(*>*)
+
+text \<open>
+ \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+ "merge h None = h" |
+ "merge None h = h" |
+ "merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then Some (Hp x ((Hp y ly)# lx))
+ else Some (Hp y ((Hp x lx)# ly)))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None" |
+ "merge_pairs [h] = Some h" |
+ "merge_pairs (h1 # h2 # hs) = merge (merge (Some h1) (Some h2)) (merge_pairs hs)"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None" |
+ "del_min (Some (Hp x hs)) = merge_pairs hs"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall> h \<in> set hs. (\<forall> y \<in> set_hp h. x < y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+ "mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}" |
+ "mset_heap (Some hp) = mset_hp hp"
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+ by (cases h) (auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+apply (cases h) by fastforce
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+by (induction h1 h2 rule: merge.induct) (auto simp: add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_hp(mset hs))"
+by (induction hs rule: merge_pairs.induct) (auto simp: mset_merge)
+
+lemma mset_del_min:
+ "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ by(cases h) (auto simp: mset_merge_pairs)
+
+(*<*)
+end
+(*>*)
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Rdle_Karl_Jonas_jonas.raedle@tum.de_621/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Rokopf_Simon_simon.rosskopf@tum.de_630/Pairing_Heap.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,75 @@
+
+theory Pairing_Heap
+imports "~~/src/HOL/Library/Multiset"
+begin
+
+subsection \<open>Definitions\<close>
+
+text
+\<open>This implementation follows Okasaki \cite{Okasaki}.
+It satisfies the invariant that \<open>Empty\<close> only occurs
+at the root of a pairing heap. The functional correctness proof does not
+require the invariant but the amortized analysis (elsewhere) makes use of it.\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+fun set_heap :: "'a heap \<Rightarrow> 'a set" where
+ "set_heap None = {}"
+| "set_heap (Some hp) = set_hp hp"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+"get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge h None = h" |
+"merge None h = h" |
+"merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then Some (Hp x (Hp y ly # lx)) else Some (Hp y (Hp x lx # ly)))"
+
+hide_const (open) insert
+
+fun merge_pairs :: "('a :: linorder) heap list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = h"
+| "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs (map Some hs)"
+
+
+subsection \<open>Correctness Proofs\<close>
+
+subsubsection \<open>Invariants\<close>
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+
+subsubsection \<open>Functional Correctness\<close>
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+"mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+"mset_heap None = {#}" |
+"mset_heap (Some (Hp x hs)) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+lemma get_min_in: "get_min (Some h) \<in> set_hp(h)"
+by(cases h)(auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+by(cases h)(auto)
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_heap(mset hs))"
+by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge)
+
+lemma mset_del_min: "mset_heap (del_min (Some h)) = mset_hp h - {#get_min (Some h)#}"
+apply (cases h) apply (auto simp: mset_merge_pairs) (* lol *)
+ by (smt image_mset.compositionality image_mset_cong mset_heap.elims mset_hp.simps o_def option.sel option.simps(3))
+
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Rokopf_Simon_simon.rosskopf@tum.de_630/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Saporta_Antoine_Jacques_antoine.saporta@tum.de_620/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,84 @@
+(*<*)
+theory hw13
+imports "~~/src/HOL/Library/Multiset"
+begin
+(*>*)
+text \<open>
+ \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+"get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge h None = h" |
+"merge None h = h" |
+"merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then Some (Hp x (Hp y ly # lx)) else Some (Hp y (Hp x lx # ly)))"
+
+hide_const (open) insert
+
+fun insert :: "'a \<Rightarrow> ('a :: linorder) heap \<Rightarrow> 'a heap" where
+"insert x h = merge (Some (Hp x [])) h"
+
+fun merge_pairs :: "('a :: linorder) heap list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = h"
+| "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs (map (\<lambda>h. Some h) hs)"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+"php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow> 'a multiset" where
+"mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow> 'a multiset" where
+"mset_heap None = {#}" |
+"mset_heap (Some hp) = mset_hp hp"
+
+(* HINT: Start with a copy of the original lemmas, and modify as needed *)
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+ by(cases h)(auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by(cases h)(auto)
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_insert: "mset_heap (insert a h) = {#a#} + mset_heap h"
+by(cases h) (auto simp add: mset_merge insert_def add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_heap(mset hs))"
+by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge)
+
+lemma aux: "image_mset mset_heap (image_mset Some (mset hs)) = image_mset mset_hp (mset hs)"
+using multiset.map_comp comp_def multiset.map_cong mset_heap.simps(2)
+by metis
+
+lemma mset_del_min:
+ "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+by(cases h) (auto simp: mset_merge_pairs aux)
+
+
+(*<*)
+end
+(*>*)
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Saporta_Antoine_Jacques_antoine.saporta@tum.de_620/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_643/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,58 @@
+theory hw13
+imports "~~/src/HOL/Library/Multiset"
+begin
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x l)) = x"
+| "get_min None = undefined"
+
+fun merge :: "('a :: linorder) hp \<Rightarrow> 'a hp \<Rightarrow> 'a hp" where
+"merge (Hp x lx) (Hp y ly) =
+ (if x < y then (Hp x (Hp y ly # lx)) else (Hp y (Hp x lx # ly)))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = Some h"
+| "merge_pairs (h1 # h2 # hs) =
+ (case (merge_pairs hs) of None \<Rightarrow> (Some (merge h1 h2))
+ | Some h \<Rightarrow> Some (merge (merge h1 h2) h))"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs hs"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+"php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> (php h))"
+
+fun mset_hp :: "'a hp \<Rightarrow> 'a multiset" where
+"mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+"mset_heap None = {#}"
+|"mset_heap (Some h) = mset_hp h"
+
+theorem get_min_in: "get_min (Some h) \<in> set_hp(h)"
+ apply (induction h)
+ by auto
+
+lemma get_min_min: "php h \<Longrightarrow> x\<in>set_hp(h) \<Longrightarrow> get_min (Some h) \<le> x"
+ apply (induction h) by (auto)
+
+lemma mset_merge: "mset_hp (merge h1 h2) = mset_hp h1 + mset_hp h2"
+ apply (induction h1 h2 rule: merge.induct) by auto
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_hp(mset hs))"
+ apply (induction hs rule: merge_pairs.induct)
+ apply (auto split: option.split)
+ apply (smt add_cancel_right_right comm_monoid_mset.distrib image_mset_cong mset_merge set_mset_mset sum_mset.comm_monoid_mset_axioms sum_mset_def)
+ by (simp add: mset_merge)
+
+lemma mset_del_min: "mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ apply (induction h rule: mset_hp.induct)
+ by (simp add: mset_merge_pairs)
+
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_643/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/FiboHeap.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,430 @@
+section \<open>Fibonacci Heap\<close>
+
+text\<open>for the whole file: theorems are important things to show, lemmas are
+ auxiliary used by larger theorems \<close>
+
+theory FiboHeap
+
+imports
+ Complex_Main
+ "Demos/BinHeap"
+ "~~/src/HOL/Library/Rewrite"
+begin
+text \<open>A Fibonacci Heap is technically like a Binomial
+ Heap, just a bit more relaxed. In detail:
+ - We still have a collection of Binomial Trees
+ - The Heap property is fulfilled in every tree
+ - We can have more than one tree of the same size
+ - The Binomial Trees do not have to be completely filled
+
+ Point 1 and 2 are pretty clear, we won't look at them in
+ detail right now.
+
+ Point 3 is important in the merge function. In the result
+ we can have several trees of the same size, and they will
+ not be ordered in descending (or ascending) order.
+
+ Point 4 is only important for the Decrese Key function (which
+ will be ignored here). In detail, the Decrese Key is
+ realized by just cutting the decresed node, and its children,
+ from the tree, and inserting it into the list of trees. In some
+ cases the parent itself will also be cutted. Since we do not
+ implement this function we can ignore the problem. From this
+ also follows, that we only work with fully filled Binomial
+ Heaps, introduced in the lesson and implemented in BinHeap.thy
+
+ Everything further important will be introduced (and maybe
+ prooven) at the corresponding section.\<close>
+
+subsection Datatype
+text \<open>The heap itself is a collection of (Binomial) trees.
+ usually the tree with the minimal root is saved with a
+ pointer. We will save it as a second parameter. Some functions
+ (like get min or delete min) will get simpler, others (deconsolidate)
+ will get harder) \<close>
+datatype 'a fibHeap = Empty (*sometimes needed, mostly for del_min*)
+ | Heap (min:"'a tree") (trees:"'a tree list")
+definition init:: "'a fibHeap" where "init = Empty" (*for \<Phi> function *)
+
+
+subsection Multiset
+text\<open>Before looking on the invariants we look at creating sets\<close>
+
+fun mset_heap:: "'a::linorder fibHeap \<Rightarrow> 'a multiset" where
+ "mset_heap (Heap n t) = mset_tree n + (\<Sum>tree\<in>#mset t. mset_tree tree)"
+ |"mset_heap Empty = {#}"
+
+text\<open>We have following invariants:
+ - EVERY tree fulfills the heap property
+ - the min-tree has the smallest root
+ - if the min-tree is Empty the whole tree must be Empty (which is given by
+ the fact, that an 'a tree structure can't be empty...\<close>
+
+fun invar_heaptrees_list:: "'a::linorder tree list \<Rightarrow> bool" where
+ "invar_heaptrees_list [] = True"
+ |"invar_heaptrees_list (x#xs) = (otree_invar x \<and> invar_heaptrees_list xs)"
+
+fun invar_heaptrees:: "'a::linorder fibHeap \<Rightarrow> bool" where
+ "invar_heaptrees (Heap n t) = ((invar_heaptrees_list t) \<and> (otree_invar n))"
+|"invar_heaptrees Empty = True"
+
+fun invar_min_smallest:: "'a::linorder fibHeap \<Rightarrow> bool" where
+ "invar_min_smallest Empty = True"
+ |"invar_min_smallest (Heap (Node rk a chld) t) \<longleftrightarrow>
+ (\<forall>x\<in>#mset_heap (Heap (Node rk a chld) t). a \<le> x)"
+
+definition invar:: "'a::linorder fibHeap \<Rightarrow> bool" where
+ "invar h \<longleftrightarrow> invar_heaptrees h \<and> invar_min_smallest h"
+
+(* often needed: if x is in a list of correct heaps x is correct *)
+lemma invar_list[simp]:
+ assumes "invar_heaptrees_list xs"
+ assumes "x\<in># mset xs"
+ shows "otree_invar x"
+ using assms
+ apply(induction xs arbitrary:x)
+ apply(auto)
+ done
+
+lemma invar_list2:"(\<forall>x\<in>#mset xs. otree_invar x) = invar_heaptrees_list xs"
+ by(induction xs) auto
+
+lemma invar_list_combine[simp]:
+ assumes "invar_heaptrees_list xs"
+ assumes "invar_heaptrees_list ys"
+ shows "invar_heaptrees_list (xs@ys)"
+ using assms by(induction xs arbitrary:ys)auto
+
+lemma invar_list_children:
+ "otree_invar (Node rk a chlds) \<Longrightarrow> invar_heaptrees_list chlds"
+ by(induction chlds arbitrary:rk a) auto
+
+
+subsection Functions
+text \<open>most important for a heap; get the minimal element\<close>
+fun getMin:: "'a fibHeap \<Rightarrow> 'a" where
+ "getMin (Heap (Node _ a _) _) = a"
+|"getMin Empty = undefined"
+
+theorem getMin_finds_min:
+ assumes "h \<noteq> Empty"
+ assumes "invar h"
+ assumes "x\<in>#mset_heap h"
+ shows "getMin h \<le> x"
+proof(cases h)
+ case Empty
+ then show ?thesis using assms(1) by auto
+next
+ case (Heap nde ts)
+ (* idea: show that get-min returns element from min-tree, show that this must be
+ smallest element (invariant) and combine *)
+ obtain rk a chld where node: "nde = Node rk a chld"
+ using tree.exhaust_sel by blast
+
+ then have min: "getMin h = a" using Heap by auto
+
+ have "invar_min_smallest h" using assms(2) unfolding invar_def by auto
+ then have "\<forall>x\<in>#mset_heap h. a \<le> x" using node Heap invar_min_smallest.simps by blast
+
+ then show ?thesis using assms(3) min by blast
+qed
+
+text\<open>before doing anything else; we merge two Heaps.
+ Merging is simple and fast: the tree lists become one and the
+ min-pointer shows to the smaller of the two trees.
+
+ Since we do not work with a pointer we check which heap had
+ the smaller min-element. This one gets the min-position, the
+ other tree is added to the tree list\<close>
+fun merge:: "'a::linorder fibHeap \<Rightarrow> 'a fibHeap \<Rightarrow> 'a fibHeap" where
+ "merge (Heap (Node r1 a1 t1) tl1) (Heap (Node r2 a2 t2) tl2)
+ = (if a1 < a2 then (Heap (Node r1 a1 t1) ((Node r2 a2 t2) # tl1 @ tl2))
+ else (Heap (Node r2 a2 t2) ((Node r1 a1 t1) # tl1 @ tl2))
+ )"
+ |"merge Empty h = h"
+ |"merge h Empty = h"
+
+lemma merge_invar1_aux:
+ assumes "invar_heaptrees_list tl1"
+ assumes "invar_heaptrees_list tl2"
+ shows "invar_heaptrees_list (tl1@tl2)"
+ using assms
+ by(induction tl1 arbitrary:tl2) auto
+
+lemma merge_invar1:
+ assumes "invar_heaptrees h1"
+ assumes "invar_heaptrees h2"
+ shows "invar_heaptrees (merge h1 h2)"
+ using assms
+ by(induction h1 h2 rule:merge.induct) (auto simp:merge_invar1_aux)
+
+lemma merge_invar2:
+ assumes "invar_min_smallest h1"
+ assumes "invar_min_smallest h2"
+ shows "invar_min_smallest (merge h1 h2)"
+ using assms
+ apply(induction h1 h2 rule:merge.induct)
+ apply(auto)
+ apply force+
+ done
+
+theorem merge_invar:
+ assumes "invar h1"
+ assumes "invar h2"
+ shows "invar (merge h1 h2)"
+ using assms
+ unfolding invar_def
+ by(auto simp:merge_invar1 merge_invar2)
+
+theorem merge_combines_msets[simp]:
+ shows "mset_heap h1 + mset_heap h2 = mset_heap (merge h1 h2)"
+ by(induction h1 h2 rule:merge.induct) auto
+
+text \<open>Inputting an element is simply merging a singleton with the list\<close>
+definition insert:: "'a::linorder fibHeap \<Rightarrow> 'a \<Rightarrow> 'a fibHeap" where
+ "insert h i = merge h (Heap (Node 1 i []) [])"
+
+theorem insert_invar:
+ assumes "invar h"
+ shows "invar (insert h x)"
+proof -
+ (*you have to show isabelle that the created singleton fullfills the invar ... *)
+ have singleton_invar: "invar (Heap (Node 1 x []) [])"
+ unfolding invar_def by auto
+
+
+ thus ?thesis using singleton_invar assms
+ unfolding insert_def
+ by(auto simp:merge_invar)
+qed
+
+
+text\<open>After deleting the minimum we have to consolidate the list. This
+ means we combine the trees of same size. The movement reminds of the
+ binary addition of binomial trees.
+
+ This works as follows: We have an array (realized as list), with exactly
+ one space for every size of a tree. Then we iterate over the trees, one
+ by one. If the corresponding field in the array is free the current
+ tree gets inserted. If not, we merge the trees and re-insert them into
+ the list of the heap (so later it gets inserted as larger tree)
+
+ For the function: The first list is the list of the Heap, the second
+ list represents the array (which should be empty at the beginning).\<close>
+
+
+fun option_to_trees:: "(('a tree option) list) \<Rightarrow> 'a tree list" where
+"option_to_trees [] = []"
+|"option_to_trees (x#xs) = (case x of None \<Rightarrow> option_to_trees xs
+ | Some t \<Rightarrow> t#option_to_trees xs)"
+
+function insert_carry:: "'a::linorder tree \<Rightarrow> ('a tree option) list \<Rightarrow> ('a tree option) list" where
+"insert_carry t lst = (
+ if rank t < length lst then
+ case (lst! (rank t)) of
+ None \<Rightarrow> lst[rank t:= Some t]
+ |Some t2 \<Rightarrow> insert_carry (link t t2) (lst[rank t:=None])
+ else undefined)"
+ by pat_completeness auto
+termination
+ apply (relation "measure (\<lambda>(t,lst). length (filter (op\<noteq>None) lst))")
+ apply simp
+ apply clarsimp
+ subgoal for t lst x2
+ apply (rewrite in "_ < \<hole>" id_take_nth_drop[of _ lst], assumption)
+ apply (rewrite in "\<hole> < _" id_take_nth_drop[of _ lst], assumption)
+ apply (simp add: upd_conv_take_nth_drop ord_class.min_def)
+ done
+ done
+
+fun consolidate:: "'a::linorder tree list \<Rightarrow> ('a tree option) list \<Rightarrow> 'a tree list" where
+ "consolidate [] list = option_to_trees list"
+ |"consolidate (t#ts) list = consolidate ts (insert_carry t list)"
+
+text \<open>we need to know how large the array for consolidate has to be. Worst case is that
+ every tree in the list has the same size (rank). An Array of (highest rank + log_2 (n))
+ must be enough.\<close>
+fun num_nones:: "'a::linorder tree list \<Rightarrow> nat" where
+ "num_nones [] = 1"
+|"num_nones xs = Max (\<Union>t\<in>set xs. {rank t}) + nat (floor(log 2 (length xs)))"
+
+text \<open>The following functions could've been combined, but this would
+ make everything much more complicated\<close>
+
+fun find_smallest_tree:: "'a::linorder tree list \<Rightarrow> 'a tree \<times> 'a tree list" where
+ "find_smallest_tree [t] = (t,[])"
+ |"find_smallest_tree (t#ts) = (let (t',ts') = find_smallest_tree ts
+ in if root t \<le> root t' then (t,t'#ts') else (t',t#ts'))"
+ |"find_smallest_tree [] = undefined"
+
+lemma mset_find_smallest_tree:
+ assumes "find_smallest_tree va = (x,xs)"
+ assumes "va \<noteq> []"
+ shows "mset va = mset xs + {# x #}"
+ using assms
+ by(induction va arbitrary:x xs rule:find_smallest_tree.induct)(auto split:if_splits prod.splits)
+
+fun find_min:: "'a::linorder tree list \<Rightarrow> 'a fibHeap" where
+ "find_min [] = Empty"
+|"find_min x = (let (t,ts) = find_smallest_tree x in Heap t ts)"
+
+fun delmin:: "'a::linorder fibHeap \<Rightarrow> 'a fibHeap" where
+ "delmin (Heap (Node rk a chlds) tlst) =
+ find_min
+ (consolidate
+ (chlds@tlst) (* combine children of min with rest of list *)
+ (replicate (num_nones (chlds@tlst)) None) (*create 'array' for consolidate *)
+ )"
+|"delmin Empty = undefined"
+
+fun correctOpts:: "(('a::linorder) tree option) list \<Rightarrow> bool" where
+ "correctOpts [] = True"
+ |"correctOpts (x#xs) = (case x of None \<Rightarrow> correctOpts xs
+ |Some t \<Rightarrow> (otree_invar t \<and> correctOpts xs))"
+
+lemma delmin_invar_aux3:
+ assumes "find_smallest_tree lst = (x,xs)"
+ assumes "lst \<noteq> []"
+ shows "x\<in># mset lst"
+ using assms
+by(induction lst arbitrary: x xs rule:find_smallest_tree.induct)(auto split:if_splits prod.splits)
+
+lemma delmin_invar_aux2:
+ assumes "invar_heaptrees_list tlst"
+ shows "invar_heaptrees (find_min tlst)"
+ using assms
+proof (induction tlst)
+ case Nil
+ then show ?case using assms by auto
+next
+ case (Cons t ts)
+ obtain x lst where A: "find_smallest_tree (t # ts) = (x,lst)"
+ using Cons assms
+ by (meson surj_pair) (* why the f*** did i need sledgehammer for this o.O *)
+
+ have B: "t#ts \<noteq> []"
+ by simp
+ have "x \<in># mset (t#ts)" using A B
+ using delmin_invar_aux3 by fastforce
+ then have otree_x: "otree_invar x" using Cons
+ by(auto)
+
+ have a: "\<forall>y \<in># mset (t#ts). otree_invar y" using Cons
+ by(auto)
+ have b: "mset lst = mset (t#ts) - {#x#}" using Cons a assms
+ using A mset_find_smallest_tree by fastforce
+ have c: "\<forall>y \<in># mset(lst). otree_invar y" using a b Cons assms
+ using in_diffD by force
+
+ have invar_lst: "invar_heaptrees_list lst"
+ using c invar_list2 by auto
+
+ show ?case using Cons A
+ by(auto split:prod.split simp:otree_x invar_lst)
+ qed
+
+(* As it took too long I had to give up, and I did not even try to proove correctness *)
+lemma delmin_invar_aux4:
+ assumes "invar_heaptrees_list lst"
+ assumes "\<forall>t\<in>set lst. rank t < length nones"
+ shows "invar_heaptrees_list(consolidate lst nones)"
+ using assms
+ sorry
+
+theorem delmin_invar:
+ assumes "invar_heaptrees h"
+ assumes "h \<noteq> Empty"
+ shows "invar_heaptrees (delmin h)"
+ using assms
+ proof(induction h rule:delmin.induct) (*dont ask why i took induction. But when i realized it was to much to change...*)
+ case (1 rk a chlds tlst)
+ have a: "invar_heaptrees_list tlst" using assms 1 by auto
+ have "otree_invar (Node rk a chlds)" using 1 by auto
+ then have b: "invar_heaptrees_list chlds"
+ using invar_list_children by blast
+
+ have A: "invar_heaptrees_list (chlds@tlst)" using a b by auto
+
+ have B: "\<forall>t \<in> set (chlds@tlst). rank t < length (replicate (num_nones (chlds @ tlst)) None)"
+ sorry
+
+ show ?case using assms A 1 B
+ apply(auto)
+ apply(auto simp:delmin_invar_aux2 delmin_invar_aux4)
+ done
+ next
+ case 2
+ then show ?case using assms by auto
+ qed
+
+theorem delmin_corr:
+ assumes "invar_heaptrees h"
+ assumes "h \<noteq> Empty"
+ shows "mset_heap (delmin h) = mset_heap h - {#getMin h#}"
+ using assms
+ proof (cases h)
+ case Empty
+ then show ?thesis using assms by auto
+ next
+ case (Heap x21 x22)
+ obtain rk a chlds where asNode: "Node rk a chlds = x21"
+ by (metis otree_invar.cases)
+ have "a = getMin h" using Heap asNode by auto
+
+ show ?thesis using Heap
+ apply(auto) (*mainly show that helper functions do not change mset*)
+ sorry
+ qed
+
+subsection \<open>Complexity\<close>
+
+subsection \<open>Timing functions\<close>
+text\<open>The Fibonacci Heap has amortized complexity, so we will need timing functions
+ for the operations and we will need an amortizing function. After defining them
+ we will show the time complexity, but not for the delMin function (as it is definitely
+ too complicated by now...)\<close>
+
+text\<open>Normally the potential function is t(S)+2m(S) where t(S) is the number of trees
+ and m(S) is the number of marked nodes. Since we never mark nodes we simply can
+ use the number of trees:\<close>
+fun \<Phi>:: "'a fibHeap \<Rightarrow> int" where
+ "\<Phi> Empty = 0"
+ |"\<Phi> (Heap _ ts) = 1 + length ts"
+
+(*showing \<Phi> lemmas is simple: *)
+theorem \<Phi>_non_neg: "\<Phi> hp \<ge> 0"
+by(cases hp) auto
+
+theorem \<Phi>_init: "\<Phi> init = 0" unfolding init_def by simp
+
+
+text \<open>In the timing functions sometimes we have to 'cheat. Concretely:
+ - We assume double linked lists with constant linking time\<close>
+
+fun t_getMin :: "'a fibHeap \<Rightarrow> nat" where
+ "t_getMin (Heap n lst) = 1"
+|"t_getMin Empty = 1" (*simpler than saying undef*)
+
+text \<open>getMin constant (does not change the heap so amortizing not necessarry)\<close>
+theorem "t_getMin h \<le> 1" by (cases h) auto
+
+fun t_merge:: "'a::linorder fibHeap \<Rightarrow> 'a fibHeap \<Rightarrow> int" where
+ "t_merge (Heap (Node r1 a1 t1) tl1) (Heap (Node r2 a2 t2) tl2)
+ = (if a1 < a2 then 2 else 2)+1" (* both cases just have one list-insert + one list-append *)
+ |"t_merge Empty h = 1"
+ |"t_merge h Empty = 1"
+
+text\<open>merge amortized constant\<close>
+theorem "t_merge a b + \<Phi>(merge a b) - (\<Phi> a + \<Phi> b) \<le> 3"
+ by(induction a b rule:t_merge.induct) auto
+
+definition t_insert:: "'a::linorder fibHeap \<Rightarrow> 'a \<Rightarrow> int" where
+"t_insert h i = t_merge h (Heap (Node 1 i []) [])"
+
+theorem "t_insert h a + \<Phi>(insert h a) - \<Phi> h \<le> 4"
+ unfolding t_insert_def insert_def
+ by(induction h "(Heap (Node 1 a [])[])" rule:t_merge.induct)auto
+
+
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,142 @@
+(* Author: Tobias Nipkow *)
+
+theory hw13
+imports "~~/src/HOL/Library/Multiset"
+begin
+
+(*
+to clarify:
+ I just copied the Pairing_Heap theory and updated the datatype.
+ Then I 'corrected' the functions, lemmas and theories s.t. they
+ fit the new definitions.
+ The two aux-lemmas were my helpers for the delete-lemmas...
+*)
+
+subsection \<open>Definitions\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x _)) = x"
+| "get_min _ = undefined"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge h None = h" |
+"merge None h = h" |
+"merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then (Some (Hp x (Hp y ly # lx)))
+ else (Some (Hp y (Hp x lx # ly))))"
+
+hide_const (open) insert
+
+fun insert :: "'a \<Rightarrow> ('a :: linorder) heap \<Rightarrow> 'a heap" where
+"insert x h = merge (Some (Hp x [])) h"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = Some h"
+| "merge_pairs (h1 # h2 # hs) =
+ merge (merge (Some h1) (Some h2)) (merge_pairs hs)"
+
+fun del_min :: "('a :: linorder) heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs hs"
+
+
+subsection \<open>Correctness Proofs\<close>
+
+subsubsection \<open>Invariants\<close>
+
+fun pheap :: "('a :: linorder) heap \<Rightarrow> bool" where
+"pheap None = True" |
+"pheap (Some (Hp x hs))
+ = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> pheap (Some h))"
+
+lemma pheap_merge: "pheap h1 \<Longrightarrow> pheap h2 \<Longrightarrow> pheap (merge h1 h2)"
+by (induction h1 h2 rule: merge.induct) fastforce+
+
+lemma pheap_insert: "pheap h \<Longrightarrow> pheap (insert x h)"
+by (auto simp: pheap_merge)
+
+lemma pheap_merge_pairs: "\<forall>h \<in> set hs. pheap (Some h) \<Longrightarrow> pheap (merge_pairs hs)"
+by(induction hs rule: merge_pairs.induct) (auto simp: pheap_merge)
+
+lemma aux: "pheap (Some (Hp x hs)) \<Longrightarrow> \<forall>h \<in> set hs. pheap (Some h)"
+ by(cases "Some (Hp x hs)") auto
+
+lemma pheap_del_min:
+ assumes "pheap h"
+shows "pheap (del_min h)"
+proof (cases h)
+ case None
+ then show ?thesis by auto
+next
+ case (Some a)
+ then obtain hp hs where intro_hs:"a = (Hp hp hs)"
+ by (meson option.inject option.simps(3) pheap.elims(2) pheap.elims(3))
+ (* oh i love sledgehammer *)
+
+ have "\<forall>h\<in>set hs. pheap (Some h)"
+ using Some assms intro_hs by auto
+
+ thus ?thesis using Some intro_hs pheap_merge_pairs[of hs]
+ by auto
+qed
+
+subsubsection \<open>Functional Correctness\<close>
+
+(* We need to make the hp to heaps. used by mapping for the hp list *)
+fun hp_to_Heap:: "'a hp \<Rightarrow> 'a hp option" where
+ "hp_to_Heap h = Some h"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+"mset_heap None = {#}" |
+"mset_heap (Some (Hp x hs)) =
+ {#x#} + Union_mset(mset(map mset_heap (map hp_to_Heap hs)))"
+
+lemma get_min_in: "get_min (Some h) \<in> set_hp(h)"
+by(cases h)(auto)
+
+lemma get_min_min: "\<lbrakk>pheap (Some h); x \<in> set_hp(h)\<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by(cases h)(auto)
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_insert: "mset_heap (insert a h) = {#a#} + mset_heap h"
+by(cases h) (auto simp add: mset_merge insert_def add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs)
+ = Union_mset(image_mset mset_heap (mset (map hp_to_Heap hs)))"
+by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge)
+
+lemma aux2 : "mset_heap (Some (Hp x hs))
+ = mset_heap (merge_pairs hs) + {#x#}"
+ apply(induction hs rule:merge_pairs.induct)
+ apply(auto simp:mset_merge)
+ done
+
+lemma mset_del_min: "mset_heap (del_min h)
+ = mset_heap h - {#get_min h#}"
+proof (cases h)
+ case None
+ then show ?thesis by auto
+next
+ case (Some a)
+ obtain x hs where hs_def: "a = Hp x hs"
+ by (meson get_min_in hp.set_cases)
+ then show ?thesis using aux2[of x hs] hs_def Some by auto
+
+qed
+
+(* only realized at the end that i'm missing this fun: *)
+
+fun mset_hp:: "'a hp \<Rightarrow> 'a multiset" where
+ "mset_hp (Hp x hs) = {#x#}
+ + Union_mset(mset(map mset_hp hs))"
+
+(* maybe doing mset_heap first would've simplify the proofs
+whatever... *)
+end
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/user_error_log.txt Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,5 @@
+Using temporary directory '/tmp/tmp.Ax0inQokM6'
+Files in /tmp/eval-625-2zyZiJ: FiboHeap.thy hw13.thy
+More than one submission file
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Stevens_Lukas_lukas.stevens@tum.de_617/Ex13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,72 @@
+(*<*)
+theory Ex13
+ imports "../Thys/Skew_Heap"
+begin
+(*>*)
+
+text \<open>
+ \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp a _)) = a"
+
+fun merge :: "('a :: linorder) hp \<Rightarrow> 'a hp \<Rightarrow> 'a hp" where
+ "merge (Hp x lx) (Hp y ly) =
+ (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = Some h"
+| "merge_pairs (h1 # h2 # hs) =
+ (case (merge_pairs hs) of
+ None \<Rightarrow> Some (merge h1 h2) |
+ Some hp \<Rightarrow> Some (merge hp (merge h1 h2)))"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+ "del_min None = None" |
+ "del_min (Some (Hp a list)) = merge_pairs list"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+ "php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+ "mset_hp (Hp a list) = {#a#} + Union_mset (mset (map mset_hp list))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = {#}" |
+ "mset_heap (Some hp) = mset_hp hp"
+
+(* HINT: Start with a copy of the original lemmas, and modify as needed *)
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+ by(cases h) auto
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+ by(cases h) auto
+
+lemma mset_merge: "mset_hp (merge h1 h2) = mset_hp h1 + mset_hp h2"
+ by(induction h1 h2 rule: merge.induct) auto
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset (image_mset mset_hp (mset hs))"
+ by(induction hs rule: merge_pairs.induct) (auto simp add: mset_merge split: option.split)
+
+lemma mset_del_min: "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+ by(cases h) (auto simp add: mset_merge_pairs)
+
+(*<*)
+end
+(*>*)
+
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Stevens_Lukas_lukas.stevens@tum.de_617/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Stwe_Daniel_daniel.stuewe@tum.de_649/HW13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,51 @@
+theory HW13
+ imports "Thys/Pairing_Heap"
+begin
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+ "get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) hp \<Rightarrow> 'a hp \<Rightarrow> 'a hp" where
+"merge (Hp x lx) (Hp y ly) =
+ (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+ "merge_pairs [] = None"
+| "merge_pairs [h] = Some h"
+| "merge_pairs (h1 # h2 # hs) = Some (case merge_pairs hs of
+ Some h \<Rightarrow> merge (merge h1 h2) h | None \<Rightarrow> merge h1 h2)"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+ "del_min None = None"
+| "del_min (Some (Hp x hs)) = merge_pairs hs"
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+"php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+"mset_hp (Hp x hs) = {#x#} + \<Union># mset (map mset_hp hs)"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+ "mset_heap None = 0"
+| "mset_heap (Some h) = mset_hp h"
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+by (induction h) auto
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+by (induction h) auto
+
+lemma mset_merge[simp]: "mset_hp (merge h1 h2) = mset_hp h1 + mset_hp h2"
+by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_merge_pairs[simp]: "mset_heap (merge_pairs hs) = \<Union># mset (map mset_hp hs)"
+by(induction hs rule: merge_pairs.induct)(auto split: option.splits)
+
+lemma mset_del_min:
+ "mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+by(induction h) auto
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Stwe_Daniel_daniel.stuewe@tum.de_649/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Wauligmann_Martin_martin.wauligmann@tum.de_641/hw13.thy Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,55 @@
+theory hw13
+imports "~~/src/HOL/Library/Tree_Multiset"
+begin
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+fun get_min :: "('a :: linorder) heap \<Rightarrow> 'a" where
+"get_min (Some (Hp x _)) = x"
+
+fun merge :: "('a :: linorder) heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
+"merge h None = h" |
+"merge None h = h" |
+"merge (Some (Hp x lx)) (Some (Hp y ly)) =
+ (if x < y then Some (Hp x (Hp y ly # lx)) else Some( Hp y (Hp x lx # ly)))"
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+"merge_pairs [] = None" |
+"merge_pairs [h] = Some h" |
+"merge_pairs (h1 # h2 # hs) = merge (merge (Some h1) (Some h2)) (merge_pairs hs)"
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+"del_min None = None" |
+"del_min (Some (Hp x hs)) = merge_pairs hs"
+
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+"php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+"mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+"mset_heap None = {#}" |
+"mset_heap (Some h) = mset_hp h"
+
+
+theorem get_min_in: "php h \<Longrightarrow> get_min (Some h) \<in> set_hp(h)"
+by(cases h)(auto)
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+by(cases h)(auto)
+
+
+lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
+by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_hp(mset hs))"
+by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge)
+
+lemma mset_del_min:
+ "php h \<Longrightarrow> mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+by(cases h) (auto simp: mset_merge_pairs)
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Wauligmann_Martin_martin.wauligmann@tum.de_641/testoutput.html Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/meta.csv Sat Jul 29 19:34:17 2017 +0200
@@ -0,0 +1,20 @@
+"612","jonas.keinholz@tum.de","Keinholz","Jonas","http://vmnipkow3.in.tum.de/web/submissions/612"
+"613","julian.biendarra@tum.de","Biendarra","Julian","http://vmnipkow3.in.tum.de/web/submissions/613"
+"614","shuwei.hu@tum.de","Hu","Shuwei","http://vmnipkow3.in.tum.de/web/submissions/614"
+"616","f.hellauer@tum.de","Hellauer","Fabian","http://vmnipkow3.in.tum.de/web/submissions/616"
+"617","lukas.stevens@tum.de","Stevens","Lukas","http://vmnipkow3.in.tum.de/web/submissions/617"
+"620","antoine.saporta@tum.de","Saporta","Antoine Jacques","http://vmnipkow3.in.tum.de/web/submissions/620"
+"621","jonas.raedle@tum.de","Rädle","Karl Jonas","http://vmnipkow3.in.tum.de/web/submissions/621"
+"622","max.haslbeck@mytum.de","Haslbeck","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/622"
+"623","ga48kog@mytum.de","Erhard","Julian","http://vmnipkow3.in.tum.de/web/submissions/623"
+"624","jochen.guenther@mytum.de","Günther","Jochen","http://vmnipkow3.in.tum.de/web/submissions/624"
+"625","daniel.somogyi@tum.de","Somogyi","Daniel","http://vmnipkow3.in.tum.de/web/submissions/625"
+"626","fabio.madge@tum.de","Madge Pimentel","Fabio","http://vmnipkow3.in.tum.de/web/submissions/626"
+"627","ga96vup@mytum.de","Ouyang","Lena","http://vmnipkow3.in.tum.de/web/submissions/627"
+"630","simon.rosskopf@tum.de","Roßkopf","Simon","http://vmnipkow3.in.tum.de/web/submissions/630"
+"635","markus.grosser@tum.de","Großer","Markus","http://vmnipkow3.in.tum.de/web/submissions/635"
+"641","martin.wauligmann@tum.de","Wauligmann","Martin","http://vmnipkow3.in.tum.de/web/submissions/641"
+"643","maximilian.schaeffeler@tum.de","Schäffeler","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/643"
+"645","friedrich.kurz@tum.de","Kurz","Friedrich","http://vmnipkow3.in.tum.de/web/submissions/645"
+"649","daniel.stuewe@tum.de","Stüwe","Daniel","http://vmnipkow3.in.tum.de/web/submissions/649"
+"650","ga95luy@mytum.de","Hutzler","Matthias","http://vmnipkow3.in.tum.de/web/submissions/650"