hw 13 submissions draft
authorlammich <lammich@in.tum.de>
Sat, 29 Jul 2017 19:34:17 +0200
changeset 69874 f30fdac78cce
parent 69873 9a1629ac93f4
child 69875 dff3ec88324d
hw 13 submissions
Exercises/hwsubm/13/Biendarra_Julian_julian.biendarra@tum.de_613/hw13.thy
Exercises/hwsubm/13/Biendarra_Julian_julian.biendarra@tum.de_613/testoutput.html
Exercises/hwsubm/13/Erhard_Julian_ga48kog@mytum.de_623/Ex13.thy
Exercises/hwsubm/13/Erhard_Julian_ga48kog@mytum.de_623/testoutput.html
Exercises/hwsubm/13/Gnther_Jochen_jochen.guenther@mytum.de_624/hw13.thy
Exercises/hwsubm/13/Gnther_Jochen_jochen.guenther@mytum.de_624/testoutput.html
Exercises/hwsubm/13/Groer_Markus_markus.grosser@tum.de_635/hw13.thy
Exercises/hwsubm/13/Groer_Markus_markus.grosser@tum.de_635/testoutput.html
Exercises/hwsubm/13/Haslbeck_Maximilian_max.haslbeck@mytum.de_622/ex13.thy
Exercises/hwsubm/13/Haslbeck_Maximilian_max.haslbeck@mytum.de_622/testoutput.html
Exercises/hwsubm/13/Hellauer_Fabian_f.hellauer@tum.de_616/hw13.thy
Exercises/hwsubm/13/Hellauer_Fabian_f.hellauer@tum.de_616/testoutput.html
Exercises/hwsubm/13/Hu_Shuwei_shuwei.hu@tum.de_614/Homework13.thy
Exercises/hwsubm/13/Hu_Shuwei_shuwei.hu@tum.de_614/testoutput.html
Exercises/hwsubm/13/Hutzler_Matthias_ga95luy@mytum.de_650/ex13.thy
Exercises/hwsubm/13/Hutzler_Matthias_ga95luy@mytum.de_650/user_error_log.txt
Exercises/hwsubm/13/Keinholz_Jonas_jonas.keinholz@tum.de_612/hw13.thy
Exercises/hwsubm/13/Keinholz_Jonas_jonas.keinholz@tum.de_612/testoutput.html
Exercises/hwsubm/13/Kurz_Friedrich_friedrich.kurz@tum.de_645/hw_13.thy
Exercises/hwsubm/13/Kurz_Friedrich_friedrich.kurz@tum.de_645/user_error_log.txt
Exercises/hwsubm/13/Madge_Pimentel_Fabio_fabio.madge@tum.de_626/testoutput.html
Exercises/hwsubm/13/Madge_Pimentel_Fabio_fabio.madge@tum.de_626/tmpl13.thy
Exercises/hwsubm/13/Ouyang_Lena_ga96vup@mytum.de_627/hw13.thy
Exercises/hwsubm/13/Ouyang_Lena_ga96vup@mytum.de_627/user_error_log.txt
Exercises/hwsubm/13/Rdle_Karl_Jonas_jonas.raedle@tum.de_621/hw13_sub.thy
Exercises/hwsubm/13/Rdle_Karl_Jonas_jonas.raedle@tum.de_621/testoutput.html
Exercises/hwsubm/13/Rokopf_Simon_simon.rosskopf@tum.de_630/Pairing_Heap.thy
Exercises/hwsubm/13/Rokopf_Simon_simon.rosskopf@tum.de_630/testoutput.html
Exercises/hwsubm/13/Saporta_Antoine_Jacques_antoine.saporta@tum.de_620/hw13.thy
Exercises/hwsubm/13/Saporta_Antoine_Jacques_antoine.saporta@tum.de_620/testoutput.html
Exercises/hwsubm/13/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_643/hw13.thy
Exercises/hwsubm/13/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_643/testoutput.html
Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/FiboHeap.thy
Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/hw13.thy
Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/user_error_log.txt
Exercises/hwsubm/13/Stevens_Lukas_lukas.stevens@tum.de_617/Ex13.thy
Exercises/hwsubm/13/Stevens_Lukas_lukas.stevens@tum.de_617/testoutput.html
Exercises/hwsubm/13/Stwe_Daniel_daniel.stuewe@tum.de_649/HW13.thy
Exercises/hwsubm/13/Stwe_Daniel_daniel.stuewe@tum.de_649/testoutput.html
Exercises/hwsubm/13/Wauligmann_Martin_martin.wauligmann@tum.de_641/hw13.thy
Exercises/hwsubm/13/Wauligmann_Martin_martin.wauligmann@tum.de_641/testoutput.html
Exercises/hwsubm/13/meta.csv
--- /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","Rdle","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","Gnther","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","Rokopf","Simon","http://vmnipkow3.in.tum.de/web/submissions/630"
+"635","markus.grosser@tum.de","Groer","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","Schffeler","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","Stwe","Daniel","http://vmnipkow3.in.tum.de/web/submissions/649"
+"650","ga95luy@mytum.de","Hutzler","Matthias","http://vmnipkow3.in.tum.de/web/submissions/650"