author lammich Thu, 13 Jul 2017 15:33:16 +0200 changeset 69847 2510274a20a5 parent 69846 4bd3ade120e9 child 69848 5a47947a89db
correction10
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Biendarra_Julian_julian.biendarra@tum.de_512/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+julian.biendarra@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Biendarra_Julian_julian.biendarra@tum.de_512/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,97 @@
+(** Score: 10/10
+*)
+(*<*)
+theory hw10
+imports
+    "../../../Public/Thys/Leftist_Heap"
+begin
+(*>*)
+text {* \ExerciseSheet{10}{30.~6.~2017} *}
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+fun merge_list :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "merge_list [] = []" |
+  "merge_list [h] = [h]" |
+  "merge_list (h\<^sub>1 # h\<^sub>2 # hs) = merge h\<^sub>1 h\<^sub>2 # merge_list hs"
+
+lemma length_merge_list: "length (merge_list hs) < Suc (length hs)"
+  by (induction hs rule: merge_list.induct) auto
+
+function merge_heaps :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+  "merge_heaps [] = Leaf" |
+  "merge_heaps [h] = h" |
+  "merge_heaps (h\<^sub>1#h\<^sub>2#hs) = merge_heaps (merge_list (h\<^sub>1#h\<^sub>2#hs))"
+by pat_completeness auto
+
+termination merge_heaps
+by (relation "measure (\<lambda>hs. length hs)") (auto simp: length_merge_list)
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list as = merge_heaps (map (\<lambda>a. Node 1 Leaf a Leaf) as)"
+
+
+lemma mset_merge_list: "fold (op +) (map mset_tree (merge_list hs)) A = fold (op +) (map mset_tree hs) A"
+  apply (induction hs arbitrary: A rule: merge_list.induct)
+  apply (auto simp: mset_merge union_assoc union_lcomm)
+  done
+
+lemma mset_merge_heaps: "mset_tree (merge_heaps hs) + A = fold (op +) (map mset_tree hs) A"
+proof (induction hs arbitrary: A rule: merge_heaps.induct)
+  case (3 h\<^sub>1 h\<^sub>2 hl)
+  then show ?case
+    using mset_merge_list[of "h\<^sub>1#h\<^sub>2#hl"]
+    by simp
+qed auto
+
+lemma mset_list: "fold op + (map (\<lambda>a. {#a#}) xs) A = mset xs + A"
+  by (induction xs arbitrary: A) auto
+
+lemma mset_heap_list: "fold op + (map (mset_tree \<circ> (\<lambda>a. Node 1 Leaf a Leaf)) xs) {#} = mset xs"
+  by (induction xs) (auto simp: mset_list)
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+  using mset_merge_heaps[of "map (\<lambda>a. Node 1 Leaf a Leaf) xs" "{#}"]
+  apply auto
+  apply (induction xs)
+  apply (auto simp: mset_list)
+  done
+
+lemma heap_merge_list: "\<forall>h\<in>set hs. heap h \<Longrightarrow> \<forall>h\<in>set (merge_list hs). heap h"
+  by (induction hs rule: merge_list.induct) (auto simp: heap_merge)
+
+lemma heap_merge_heaps: "\<forall>h\<in>set hs. heap h \<Longrightarrow> heap (merge_heaps hs)"
+  by (induction hs rule: merge_heaps.induct) (auto simp: heap_merge_list)
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def
+  by (auto simp: heap_merge_heaps)
+
+lemma ltree_merge_list: "\<forall>h\<in>set hs. ltree h \<Longrightarrow> \<forall>h\<in>set (merge_list hs). ltree h"
+  by (induction hs rule: merge_list.induct) (auto simp: ltree_merge)
+
+lemma ltree_merge_heaps: "\<forall>h\<in>set hs. ltree h \<Longrightarrow> ltree (merge_heaps hs)"
+  by (induction hs rule: merge_heaps.induct) (auto simp: ltree_merge_list)
+
+lemma ltree_heap_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def
+  by (auto simp: ltree_merge_heaps)
+
+(*<*)
+end
+(*>*)
\ No newline at end of file```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Biendarra_Julian_julian.biendarra@tum.de_512/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Erhard_Julian_ga48kog@mytum.de_543/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+ga48kog@mytum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Erhard_Julian_ga48kog@mytum.de_543/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,87 @@
+(** Score: 2/10
+
+  The shrink has a very complicated control flow. Perhaps, splitting it
+  into two functions, one to do a single shrink pass, and another to iterate
+  the first function until a single heap is left, would have simplified the structure/proofs.
+*)
+
+(*<*)
+theory hw10
+imports
+    "../fds_ss17/Thys/Leftist_Heap"
+begin
+(*>*)
+text {* \ExerciseSheet{10}{30.~6.~2017} *}
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+fun shrink :: "('a::ord lheap) list \<Rightarrow> ('a lheap) list \<Rightarrow> 'a lheap" where
+  "shrink [] [] = Leaf" |
+  "shrink [h] [] = h" |
+  "shrink l [] = shrink [] l" |
+  "shrink [] [h] = h" |
+  "shrink (a#t) [h]  = shrink [(merge a h)] t" | (* Do this so that termination proof works *)
+  "shrink l (a#(b#t)) = shrink ((merge a b)#l) t"
+(*
+lemma shrink : "fold (\<lambda> a b . (mset_tree a) + b) (shrink l1 l2) Leaf = fold (\<lambda> a b . a + b) ((map mset_tree l1) + (map mset_tree l2)) "
+  *)
+(*
+fun shrink2 :: "('a::ord lheap) list \<Rightarrow> ('a lheap) list" where
+"shrink2 [] = [Leaf]" |
+"shrink2 [h] = [h]" |
+"shrink2 (a#b#t) = shrink2 ((merge a b)#(shrink2 t))"
+*)
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list list  = shrink [] (map (\<lambda>a . insert a Leaf) list )"
+
+ (* :-( *)
+lemma mset_h_o_l: "mset_tree (shrink acc (map (\<lambda>a . insert a Leaf) xs))  = mset xs + (fold (\<lambda> a b . mset_tree  a + b) acc {#})  "
+proof (induction acc "map (\<lambda>a . insert a Leaf) xs"  rule:shrink.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 h)
+  then show ?case by simp
+next
+  case (3 v vb vc)
+  then show ?case sorry
+next
+  case (4 h)
+  then show ?case
+  by (smt Nil_is_map_conv add.commute fold_simps(1) map_eq_Cons_conv mset.simps(1) mset.simps(2) mset_insert mset_tree.simps(1) shrink.simps(4))
+next
+  case (5 a t h)
+  then show ?case sorry
+next
+  case (6 l a b t)
+  then show ?case sorry
+qed
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  sorry
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  sorry
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Erhard_Julian_ga48kog@mytum.de_543/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Groer_Markus_markus.grosser@tum.de_513/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+markus.grosser@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Groer_Markus_markus.grosser@tum.de_513/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,88 @@
+(** Score: 10/10
+  Your solution is actually quite simple, and along the lines of our solution.
+  Instead of a termination proof, we used a simp lemma, see below.
+*)
+(*<*)
+theory hw10
+  imports
+    "../../repo/Thys/Leftist_Heap"
+begin
+  (*>*)
+text {* \ExerciseSheet{10}{30.~6.~2017} *}
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+(* There's gotta be a simpler solution for all of this, considering my implementation required a
+termination proof \<dots> *)
+
+fun heap_of_list_pass :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "heap_of_list_pass (h1#h2#hs) = merge h1 h2 # heap_of_list_pass hs"
+| "heap_of_list_pass hs = hs"
+
+lemma heap_of_list_pass_length_mono: "length hs \<ge> length (heap_of_list_pass hs)"
+  by (induction hs rule: heap_of_list_pass.induct) auto
+
+(** Simp lemma to get automatic termination *)
+lemma [simp]: "length (heap_of_list_pass hs) = (length hs + 1) div 2"
+  by (induction hs rule: heap_of_list_pass.induct) auto
+
+
+function (sequential) heap_of_list_iter :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+  "heap_of_list_iter [h] = h"
+| "heap_of_list_iter (h#hs) = heap_of_list_iter (heap_of_list_pass (h#hs))"
+| "heap_of_list_iter [] = Leaf"
+  using heap_of_list_pass.cases by blast+
+termination
+  by lexicographic_order (** You could also use fun now ... *)
+  (**
+  by (relation "measure length")
+    (auto simp: le_imp_less_Suc[OF heap_of_list_pass_length_mono])
+  *)
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list l = heap_of_list_iter (map (\<lambda>x. insert x Leaf) l)"
+
+lemma mset_heap_of_list_pass[simp]: "\<Union>#{#mset_tree h. h \<in># mset (heap_of_list_pass l)#} = \<Union>#{#mset_tree h. h \<in># mset l#}"
+  by (induction l rule: heap_of_list_pass.induct) (auto simp: mset_merge)
+
+lemma mset_heap_of_list_iter: "mset_tree (heap_of_list_iter l) = \<Union>#{#mset_tree h. h \<in># mset l#}"
+  by (induction l rule: heap_of_list_iter.induct) (auto simp: mset_merge algebra_simps)
+
+lemma ltree_heap_of_list_pass: "\<forall>h \<in> set l. ltree h \<Longrightarrow> \<forall>h \<in> set (heap_of_list_pass l). ltree h"
+  by (induction l rule: heap_of_list_pass.induct) (auto simp: ltree_merge)
+
+lemma heap_heap_of_list_pass: "\<forall>h \<in> set l. heap h \<Longrightarrow> \<forall>h \<in> set (heap_of_list_pass l). heap h"
+  by (induction l rule: heap_of_list_pass.induct) (auto simp: heap_merge)
+
+lemma heap_heap_of_list_iter: "\<forall>h \<in> set l. heap h \<Longrightarrow> heap (heap_of_list_iter l)"
+  by (induction l rule: heap_of_list_iter.induct) (auto simp: heap_merge heap_heap_of_list_pass)
+
+lemma ltree_heap_of_list_iter: "\<forall>h \<in> set l. ltree h \<Longrightarrow>ltree (heap_of_list_iter l)"
+  by (induction l rule: heap_of_list_iter.induct) (auto simp: ltree_merge ltree_heap_of_list_pass)
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def by (induction xs) (auto simp: mset_heap_of_list_iter mset_insert)
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def by (simp add: heap_insert heap_heap_of_list_iter)
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def by (simp add: ltree_insert ltree_heap_of_list_iter)
+
+    (*<*)
+end
+  (*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Groer_Markus_markus.grosser@tum.de_513/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Haslbeck_Maximilian_max.haslbeck@mytum.de_511/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+max.haslbeck@mytum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Haslbeck_Maximilian_max.haslbeck@mytum.de_511/ex10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,114 @@
+(** Score: 10/10
+*)
+(*<*)
+theory ex10
+imports
+    "../Thys/Leftist_Heap"
+begin
+(*>*)
+text {* \ExerciseSheet{10}{30.~6.~2017} *}
+
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+fun merge_list' :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "merge_list' [] = []" |
+  "merge_list' [x] = [x]" |
+  "merge_list' (x#x'#xs) = ((merge x x')#(merge_list' xs))"
+
+lemma merge_list'_measure: "xs = x#x'#xs' \<Longrightarrow> length (merge_list' xs) < length xs"
+proof(induction xs arbitrary: x x' xs' rule: merge_list'.induct)
+  case (3 y y' ys)
+  then show ?case
+    apply(subst merge_list'.simps)
+    apply(rule merge_list'.cases[of ys])
+      apply(simp)
+     apply(force)
+    by fastforce
+qed (auto)
+
+function merge_list :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+  "merge_list [] = Leaf" |
+  "merge_list [x] = x" |
+  "merge_list (x#x'#xs') = merge_list (merge_list' (x#x'#xs'))"
+by pat_completeness auto
+termination
+  apply(relation "measure length")
+   apply(simp)
+  using merge_list'_measure by fastforce
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list xs = merge_list (map (\<lambda>x. insert x Leaf) xs)"
+
+lemma mset_merge_of_list': "Union_mset (mset (map mset_tree (merge_list' xs))) =
+                            Union_mset (mset (map mset_tree xs))"
+  by (induction xs rule: merge_list'.induct) (auto simp add: mset_merge)
+
+lemma mset_merge_of_list: "mset_tree (merge_list xs) =
+                            Union_mset (mset (map mset_tree xs))"
+  proof(induction xs rule: merge_list.induct)
+    case (3 x x' xs')
+    then show ?case
+      apply(subst merge_list.simps)
+      apply(subst 3(1))
+        using mset_merge_of_list' by blast
+  qed (auto)
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+  apply(induction xs)
+  by (auto simp add: mset_insert)
+
+lemma heap_merge_list': "\<forall>x \<in> set xs. heap x \<Longrightarrow> y \<in> set (merge_list' xs) \<Longrightarrow> heap y"
+  apply(induction xs arbitrary: y rule: merge_list'.induct)
+    apply(force)
+   apply(simp)
+  using heap_merge by (auto)
+
+lemma heap_merge_list: "\<forall>x \<in> set xs. heap x \<Longrightarrow> heap (merge_list xs)"
+  proof(induction xs rule: merge_list.induct)
+    case (3 x x' xs')
+    show ?case apply(subst merge_list.simps)
+      apply(rule 3(1))
+    using heap_merge_list' 3(2) by blast
+qed (auto)
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def apply(rule heap_merge_list) by auto
+
+
+lemma ltree_merge_list': "\<forall>x \<in> set xs. ltree x \<Longrightarrow> y \<in> set (merge_list' xs) \<Longrightarrow> ltree y"
+  apply(induction xs arbitrary: y rule: merge_list'.induct)
+    apply(force)
+   apply(simp)
+  using ltree_merge by (auto)
+
+lemma ltree_merge_list: "\<forall>x \<in> set xs. ltree x \<Longrightarrow> ltree (merge_list xs)"
+  proof(induction xs rule: merge_list.induct)
+    case (3 x x' xs')
+    show ?case apply(subst merge_list.simps)
+      apply(rule 3(1))
+    using ltree_merge_list' 3(2) by blast
+qed (auto)
+
+(* Shouldn't that be ltree_heap_of_list? :) *) (** Yes, actually it should be named like this. *)
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+    unfolding heap_of_list_def apply(rule ltree_merge_list) by (auto simp add: ltree_insert)
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Haslbeck_Maximilian_max.haslbeck@mytum.de_511/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Hellauer_Fabian_f.hellauer@tum.de_484/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+f.hellauer@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Hellauer_Fabian_f.hellauer@tum.de_484/ex10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,125 @@
+(** Score: 10/10
+*)
+(*<*)
+theory ex10
+imports
+    "../../../Public/Thys/Leftist_Heap"
+begin
+(*>*)
+text {* \ExerciseSheet{10}{30.~6.~2017} *}
+
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+fun merge_fold :: "'a::ord lheap list \<Rightarrow> 'a::ord lheap list" where
+  "merge_fold (t1#t2#ts) = merge t1 t2 # merge_fold ts" |
+  "merge_fold [t] = [t]" |
+  "merge_fold [] = []"
+
+lemma merge_fold_ok[simp]: "fold (op +) (map mset_tree (merge_fold xs)) = fold (op +) (map mset_tree xs)"
+  apply (induction xs rule: merge_fold.induct)
+    apply (simp_all add: mset_merge algebra_simps)
+   done
+
+lemma [termination_simp]: "length (merge_fold ts) \<le> length ts"
+  by (induction ts rule: merge_fold.induct) simp_all
+
+fun main_loop :: "'a::ord lheap list \<Rightarrow> 'a::ord lheap list" where
+  "main_loop [] = [Leaf]" |
+  "main_loop [t] = [t]" |
+  "main_loop ts = main_loop (merge_fold ts)"
+
+lemma main_loop_ok[simp]: "fold (op +) (map mset_tree (main_loop xs)) = fold (op +) (map mset_tree xs)"
+  apply (induction xs rule: main_loop.induct)
+    apply (simp_all add: mset_merge algebra_simps)
+   done
+
+lemma main_loop_singleton[simp]: "length (main_loop ts) = 1"
+  apply (induction ts rule: main_loop.induct)
+    apply auto
+  done
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list l = hd (main_loop (map (\<lambda>a. Node 1 Leaf a Leaf) l))"
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+proof -
+  obtain x where "[x] = main_loop (map (\<lambda>a. Node 1 Leaf a Leaf) xs)" using main_loop_singleton
+    by (metis (no_types, lifting) One_nat_def length_0_conv length_Suc_conv)
+  note main_loop_ok[of "map (\<lambda>a. \<langle>1, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>) xs",
+      folded this, simplified]
+  also have "fold op + (map (mset_tree \<circ> (\<lambda>a. \<langle>Suc 0, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>)) xs) = op + (mset xs)"
+    apply (induction xs)
+     apply auto
+    done
+  finally show ?thesis
+    unfolding heap_of_list_def
+    by (metis \<open>[x] = main_loop (map (\<lambda>a. \<langle>1, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>) xs)\<close> add.right_neutral list.sel(1))
+qed
+
+lemma heap_merge_fold: "list_all heap xs \<Longrightarrow> list_all heap (merge_fold xs)"
+  apply (induction xs rule: merge_fold.induct)
+    apply (auto simp: heap_merge)
+    done
+
+lemma heap_main_loop: "list_all heap xs \<Longrightarrow> list_all heap (main_loop xs)"
+  apply (induction xs rule: main_loop.induct)
+    apply (auto simp: heap_merge_fold heap_merge)
+    done
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+proof -
+  obtain x where "[x] = main_loop (map (\<lambda>a. Node 1 Leaf a Leaf) xs)" using main_loop_singleton
+    by (metis (no_types, lifting) One_nat_def length_0_conv length_Suc_conv)
+  note heap_main_loop[of "map (\<lambda>a. \<langle>1, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>) xs",
+      folded this, simplified]
+  moreover have "list_all heap
+   (map (\<lambda>a. \<langle>Suc 0, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>) xs)"
+    apply (induction xs)
+     apply auto
+    done
+  ultimately show ?thesis
+    unfolding heap_of_list_def
+    by (metis \<open>[x] = main_loop (map (\<lambda>a. \<langle>1, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>) xs)\<close> list.sel(1))
+qed
+
+lemma ltree_merge_fold: "list_all ltree xs \<Longrightarrow> list_all ltree (merge_fold xs)"
+  apply (induction xs rule: merge_fold.induct)
+    apply (auto simp: ltree_merge)
+    done
+
+lemma ltree_main_loop: "list_all ltree xs \<Longrightarrow> list_all ltree (main_loop xs)"
+  apply (induction xs rule: main_loop.induct)
+    apply (auto simp: ltree_merge_fold ltree_merge)
+    done
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+proof -
+  obtain x where "[x] = main_loop (map (\<lambda>a. Node 1 Leaf a Leaf) xs)" using main_loop_singleton
+    by (metis (no_types, lifting) One_nat_def length_0_conv length_Suc_conv)
+  note ltree_main_loop[of "map (\<lambda>a. \<langle>1, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>) xs",
+      folded this, simplified]
+  moreover have "list_all ltree
+   (map (\<lambda>a. \<langle>Suc 0, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>) xs)"
+    apply (induction xs)
+     apply auto
+    done
+  ultimately show ?thesis
+    unfolding heap_of_list_def
+    by (metis \<open>[x] = main_loop (map (\<lambda>a. \<langle>1, \<langle>\<rangle>, a, \<langle>\<rangle>\<rangle>) xs)\<close> list.sel(1))
+qed
+
+end
\ No newline at end of file```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Hellauer_Fabian_f.hellauer@tum.de_484/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Hu_Shuwei_shuwei.hu@tum.de_482/Homework10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,69 @@
+(** Score: 10/10
+*)
+(* Author: Shuwei Hu *)
+
+theory Homework10
+  imports "../../../Public/Thys/Leftist_Heap"
+begin
+
+fun squeeze :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "squeeze (h0#h1#hs) = merge h0 h1 # squeeze hs"
+| "squeeze hs = hs"
+term 0 (**)
+
+lemma [simp]: "size (squeeze hs) < Suc (size hs)"
+  by (induction hs rule: squeeze.induct) auto
+
+fun squeeze_fix :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "squeeze_fix (h0#h1#hs) = squeeze_fix (squeeze (h0#h1#hs))"
+| "squeeze_fix hs = hs"
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list xs = hd (squeeze_fix (Leaf # [Node 1 Leaf x Leaf. x \<leftarrow> xs]))"
+term 0 (**)
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+proof -
+  let ?M="sum_mset \<circ> mset \<circ> map mset_tree"
+  have a:"?M (Leaf # [Node 1 Leaf x Leaf. x\<leftarrow>xs]) = mset xs"
+    by (induction xs) auto
+  have b:"?M (squeeze hs) = ?M hs" for hs
+    by (induction hs rule: squeeze.induct) (auto cong: mset_merge)
+  have c:"?M (squeeze_fix hs) = ?M (squeeze hs)" for hs
+    by (induction hs rule: squeeze_fix.induct) (auto cong: b[unfolded comp_def])
+  have d:"hs\<noteq>[] \<Longrightarrow> mset_tree (hd (squeeze_fix hs)) = ?M (squeeze_fix hs)" for hs
+    by (induction hs rule: squeeze_fix.induct) auto
+  show ?thesis
+    unfolding heap_of_list_def d[OF list.distinct(2)] c b a ..
+qed
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+proof -
+  have a:"\<forall>h\<in>set (Leaf # [Node 1 Leaf x Leaf. x \<leftarrow> xs]). heap h"
+    by simp
+  have b:"\<forall>h\<in>set hs. heap h \<Longrightarrow> \<forall>h\<in>set (squeeze hs). heap h" for hs
+    by (induction hs rule: squeeze.induct) (auto intro: heap_merge)
+  have c:"\<forall>h\<in>set (squeeze hs). heap h \<Longrightarrow> \<forall>h\<in>set (squeeze_fix hs). heap h" for hs
+    by (induction hs rule: squeeze_fix.induct) (auto simp: b)
+  have d:"hs\<noteq>[] \<Longrightarrow> \<forall>h\<in>set (squeeze_fix hs). heap h \<Longrightarrow> heap (hd (squeeze_fix hs))" for hs
+    by (induction hs rule: squeeze_fix.induct) auto
+  show ?thesis
+    by (unfold heap_of_list_def) (intro a b c d list.distinct(2))
+qed
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+proof -
+  have a:"\<forall>h\<in>set (Leaf # [Node 1 Leaf x Leaf. x \<leftarrow> xs]). ltree h"
+    by simp
+  have b:"\<forall>h\<in>set hs. ltree h \<Longrightarrow> \<forall>h\<in>set (squeeze hs). ltree h" for hs
+    by (induction hs rule: squeeze.induct) (auto intro: ltree_merge)
+  have c:"\<forall>h\<in>set (squeeze hs). ltree h \<Longrightarrow> \<forall>h\<in>set (squeeze_fix hs). ltree h" for hs
+    by (induction hs rule: squeeze_fix.induct) (auto simp: b)
+  have d:"hs\<noteq>[] \<Longrightarrow> \<forall>h\<in>set (squeeze_fix hs). ltree h \<Longrightarrow> ltree (hd (squeeze_fix hs))" for hs
+    by (induction hs rule: squeeze_fix.induct) auto
+  show ?thesis
+    by (unfold heap_of_list_def) (intro a b c d list.distinct(2))
+qed
+
+end
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Hu_Shuwei_shuwei.hu@tum.de_482/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+shuwei.hu@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Hu_Shuwei_shuwei.hu@tum.de_482/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Hutzler_Matthias_ga95luy@mytum.de_489/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+ga95luy@mytum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Hutzler_Matthias_ga95luy@mytum.de_489/ex10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,90 @@
+(** Score: 10/10
+*)
+theory ex10
+imports
+    "../fds_ss17/Thys/Leftist_Heap"
+begin
+
+
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+fun singleton_heap :: "('a::ord) \<Rightarrow> 'a lheap" where
+  "singleton_heap x = Node 1 Leaf x Leaf"
+
+fun mergepass :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow>'a list \<Rightarrow> 'a list" where
+  "mergepass f [] = []" |
+  "mergepass f [a] = [a]" |
+  "mergepass f (a#b#cs) = f a b # mergepass f cs"
+
+lemma aux_length_mergepass: "length (mergepass f xs) \<le> length xs"
+  by (induction f xs rule: mergepass.induct) auto
+
+lemma mergepass_preserves:
+  "(\<forall>x y. P x \<and> P y \<longrightarrow> P (f x y)) \<Longrightarrow>
+  \<forall>x\<in>set xs. P x \<Longrightarrow> x\<in>set (mergepass f xs) \<Longrightarrow> P x"
+  by (induction f xs rule: mergepass.induct) auto
+
+lemma mergepass_accumulates:
+  "(\<forall>x y. g (f x y) = (g x + g y ::'a::comm_monoid_add)) \<Longrightarrow>
+  fold (op +) (map g (mergepass f xs)) n = fold (op +) (map g xs) n"
+  apply (induction f xs arbitrary: n rule: mergepass.induct)
+  by (auto simp add: algebra_simps)
+
+function (sequential) mergelist :: "'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow>'a list \<Rightarrow> 'a" where
+  "mergelist d f [] = d" |
+  "mergelist d f [a] = a" |
+  "mergelist d f l = mergelist d f (mergepass f l)"
+  by pat_completeness auto
+termination
+  apply (relation "measure (%(d, f, l). length l)")
+  by (auto simp add: aux_length_mergepass order.strict_trans1[OF _ Nat.lessI])
+
+lemma mergelist_preserves:
+  "P d \<Longrightarrow> (\<forall>x y. P x \<and> P y \<longrightarrow> P (f x y)) \<Longrightarrow>
+  \<forall>x\<in>set xs. P x \<Longrightarrow> P (mergelist d f xs)"
+  apply (induction d f xs rule: mergelist.induct)
+  by (auto intro: mergepass_preserves)
+
+lemma mergelist_accumulates:
+  "g d = (0::'a::comm_monoid_add) \<Longrightarrow> (\<forall>x y. g (f x y) = g x + g y) \<Longrightarrow>
+  g (mergelist d f xs) = fold (op +) (map g xs) 0"
+  apply (induction d f xs rule: mergelist.induct)
+  by (auto simp add: mergepass_accumulates algebra_simps)
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap" where
+  "heap_of_list = mergelist Leaf merge \<circ> map singleton_heap"
+
+lemma mset_heap_of_list_aux1: "mset_tree (mergelist \<langle>\<rangle> merge xs) = fold (op +) (map mset_tree xs) {#}"
+  apply (rule mergelist_accumulates)
+
+lemma mset_heap_of_list_aux2: "fold (op +) (map (mset_tree \<circ> singleton_heap) xs) s = mset xs + s"
+  by (induction xs arbitrary: s) auto
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  by (simp add: heap_of_list_def mset_heap_of_list_aux1 mset_heap_of_list_aux2)
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  apply (rule mergelist_preserves)
+  by (auto simp add: heap_merge)
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  apply (rule mergelist_preserves)
+  by (auto simp add: ltree_merge)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Hutzler_Matthias_ga95luy@mytum.de_489/user_error_log.txt	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,6 @@
+Using temporary directory '/tmp/tmp.XTVXA1QBtQ'
+Files in /tmp/eval-489-gaI3D9: ex10.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/10/Keinholz_Jonas_jonas.keinholz@tum.de_510/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+jonas.keinholz@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Keinholz_Jonas_jonas.keinholz@tum.de_510/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,256 @@
+(** Score: 10/10
+*)
+theory hw10
+  imports
+    "../../../Public/Thys/Leftist_Heap"
+begin
+
+section \<open>Homework 10 Constructing a Heap from a List of Elements\<close>
+
+subsection \<open>Singleton heap\<close>
+
+text \<open>Creates a heap consisting of a single element\<close>
+
+definition single_heap :: "'a \<Rightarrow> 'a lheap" where
+  "single_heap x = \<langle>1, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle>"
+
+lemma mset_tree_single_heap: "mset_tree (single_heap x) = {#x#}"
+  unfolding single_heap_def by auto
+
+lemma heap_single_heap: "heap (single_heap x)"
+  unfolding single_heap_def by auto
+
+lemma ltree_single_heap: "ltree (single_heap x)"
+  unfolding single_heap_def by auto
+
+subsection \<open>Lists of multisets\<close>
+
+text \<open>
+  Our functions will act on heap lists. To formalize properties about the multisets described by
+  these heap lists, we will use @{term sum_list} to sum over the multisets of the heaps. For that,
+  we need some auxiliary lemmas.
+\<close>
+
+lemma sum_list_singles:
+  fixes xs :: "'a::ord list"
+  shows "sum_list (map (\<lambda>x. {#x#}) xs) = mset xs"
+proof -
+  have "sum_list (map (\<lambda>x. {#x#}) xs) = fold plus (map (\<lambda>x. {#x#}) xs) {#}"
+  also have "\<dots> = fold (plus o (\<lambda>x. {#x#})) xs {#}"
+    using fold_map[where f = "(\<lambda>x::'a::ord. {#x#})" and g = plus] by auto
+  also have "\<dots> = fold (\<lambda>x A. {#x#} + A) xs {#}"
+    unfolding comp_def by blast
+  also have "\<dots> = mset xs"
+  proof -
+    have "\<And>A. fold (\<lambda>x A. {#x#} + A) xs A = A + mset xs"
+      by (induction xs) auto
+    then show ?thesis by auto
+  qed
+  finally show ?thesis .
+qed
+
+lemma sum_list_single_heaps:
+  fixes xs :: "'a::ord list"
+  shows "sum_list (map mset_tree (map single_heap xs)) = mset xs"
+proof -
+  have "sum_list (map mset_tree (map single_heap xs)) = sum_list (map (mset_tree o single_heap) xs)"
+    by auto
+  also have "\<dots> = sum_list (map (\<lambda>x. {#x#}) xs)"
+  proof -
+    have "mset_tree o single_heap = (\<lambda>x. {#x#})" using mset_tree_single_heap by fastforce
+    then show ?thesis by (rule arg_cong)
+  qed
+  also have "\<dots> = mset xs" using sum_list_singles by auto
+  finally show ?thesis .
+qed
+
+
+text \<open>Iterates over a heap list and merges adjacent heaps.\<close>
+
+fun merge_adjacent :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "merge_adjacent (t\<^sub>1 # t\<^sub>2 # ts) = merge t\<^sub>1 t\<^sub>2 # merge_adjacent ts"
+
+lemma mset_merge_adjacent: "sum_list (map mset_tree (merge_adjacent ts)) = sum_list (map mset_tree ts)"
+  case (1 t\<^sub>1 t\<^sub>2 ts)
+  have "sum_list (map mset_tree (merge_adjacent (t\<^sub>1 # t\<^sub>2 # ts))) = sum_list (mset_tree (merge t\<^sub>1 t\<^sub>2) # map mset_tree (merge_adjacent ts))"
+    by auto
+  also have "\<dots> = mset_tree (merge t\<^sub>1 t\<^sub>2) + sum_list (map mset_tree (merge_adjacent ts))"
+    by auto
+  also have "\<dots> = mset_tree t\<^sub>1 + mset_tree t\<^sub>2 + sum_list (map mset_tree (merge_adjacent ts))"
+    using mset_merge by auto
+  also have "\<dots> = sum_list (map mset_tree (t\<^sub>1 # t\<^sub>2 # ts))"
+    using 1 by auto
+  finally show ?case .
+qed auto
+
+  assumes "\<And>t. t \<in> set ts \<Longrightarrow> heap t"
+  shows "t \<in> set (merge_adjacent ts) \<Longrightarrow> heap t"
+  using assms
+  case (1 t\<^sub>1 t\<^sub>2 ts)
+  then show ?case using heap_merge by auto
+qed auto
+
+  assumes "\<And>t. t \<in> set ts \<Longrightarrow> ltree t"
+  shows "t \<in> set (merge_adjacent ts) \<Longrightarrow> ltree t"
+  using assms
+  case (1 t\<^sub>1 t\<^sub>2 ts)
+  then show ?case using ltree_merge by auto
+qed auto
+
+
+lemma length_merge_adjacent_lt: "length ts \<ge> 2 \<Longrightarrow> length (merge_adjacent ts) < length ts"
+  case (1 t\<^sub>1 t\<^sub>2 ts)
+  moreover have "length (merge_adjacent ts) \<le> length ts"
+    by (induct rule: merge_adjacent.induct) auto
+  ultimately show ?case by auto
+qed auto
+
+text \<open>
+  Repeatedly merge adjacent heaps (using @{term merge_adjacent}) as long as there are at least two
+  heaps left. Needs a termination proof.
+\<close>
+
+function heap_of_list' :: "'a::ord lheap list \<Rightarrow> 'a::ord lheap list" where
+  "heap_of_list' ts = (if length ts \<le> 1 then ts else heap_of_list' (merge_adjacent ts))"
+  by auto
+
+lemma heap_of_list'_singleton: "ts \<noteq> [] \<Longrightarrow> \<exists>t. heap_of_list' ts = [t]"
+proof (induct ts rule: length_induct)
+  case (1 ts)
+  then obtain t\<^sub>1 ts' where ts: "ts = t\<^sub>1 # ts'" using list.exhaust by blast
+  show ?case
+  proof (cases ts')
+    case Nil
+    then show ?thesis using ts by auto
+  next
+    case (Cons t\<^sub>2 ts'')
+    then have "length ts \<ge> 2" using ts by auto
+    then have
+      "length (merge_adjacent ts) < length ts"
+      "heap_of_list' ts = heap_of_list' (merge_adjacent ts)"
+    then show ?thesis using 1 by auto
+  qed
+qed
+
+lemma mset_heap_of_list': "sum_list (map mset_tree (heap_of_list' ts)) = sum_list (map mset_tree ts)"
+proof (induct rule: heap_of_list'.induct)
+  case (1 ts)
+  show ?case
+  proof (cases "length ts \<le> 1")
+    case False
+    then have "sum_list (map mset_tree (heap_of_list' ts)) = sum_list (map mset_tree (merge_adjacent ts))"
+      using 1[OF False] by auto
+    also have "\<dots> = sum_list (map mset_tree ts)"
+    finally show ?thesis .
+  qed auto
+qed
+
+lemma heap_heap_of_list':
+  assumes "\<And>t. t \<in> set ts \<Longrightarrow> heap t"
+  shows "t \<in> set (heap_of_list' ts) \<Longrightarrow> heap t"
+  using assms
+proof (induct rule: heap_of_list'.induct)
+  case (1 ts)
+  then show ?case
+    by (cases "length ts \<le> 1") auto
+qed
+
+lemma ltree_heap_of_list':
+  assumes "\<And>t. t \<in> set ts \<Longrightarrow> ltree t"
+  shows "t \<in> set (heap_of_list' ts) \<Longrightarrow> ltree t"
+  using assms
+proof (induct rule: heap_of_list'.induct)
+  case (1 ts)
+  then show ?case
+    by (cases "length ts \<le> 1") auto
+qed
+
+subsection \<open>Heap of list\<close>
+
+text \<open>Invokes @{term "heap_of_list'"} with singleton heaps.\<close>
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap" where
+  "heap_of_list xs = (if xs = [] then Leaf else hd (heap_of_list' (map single_heap xs)))"
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+proof (cases xs)
+  case Nil
+  then show ?thesis unfolding heap_of_list_def by auto
+next
+  case (Cons x xs')
+  let ?ts = "map single_heap xs"
+
+  obtain t where t: "heap_of_list' ?ts = [t]"
+    using Cons heap_of_list'_singleton by blast
+  then have "heap_of_list xs = t"
+    unfolding heap_of_list_def by auto
+  moreover have "mset_tree t = mset xs"
+  proof -
+    have "mset_tree t = sum_list (map mset_tree [t])" by auto
+    also have "\<dots> = sum_list (map mset_tree ?ts)"
+      using t mset_heap_of_list'[of ?ts] by auto
+    also have "\<dots> = mset xs"
+      using sum_list_single_heaps by auto
+    finally show ?thesis .
+  qed
+  ultimately show ?thesis by auto
+qed
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+proof (cases xs)
+  case Nil
+  then show ?thesis unfolding heap_of_list_def by auto
+next
+  case (Cons x xs')
+  let ?ts = "map single_heap xs"
+
+  obtain t where t: "heap_of_list' ?ts = [t]"
+    using Cons heap_of_list'_singleton by blast
+  then have "heap_of_list xs = t"
+    unfolding heap_of_list_def by auto
+  moreover have "heap t"
+    using heap_heap_of_list'[where t = t and ts = ?ts] heap_single_heap t by auto
+  ultimately show ?thesis by auto
+qed
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+ proof (cases xs)
+  case Nil
+  then show ?thesis unfolding heap_of_list_def by auto
+next
+  case (Cons x xs')
+  let ?ts = "map single_heap xs"
+
+  obtain t where t: "heap_of_list' ?ts = [t]"
+    using Cons heap_of_list'_singleton by blast
+  then have "heap_of_list xs = t"
+    unfolding heap_of_list_def by auto
+  moreover have "ltree t"
+  proof -
+    have "\<And>t. t \<in> set ?ts \<Longrightarrow> ltree t"
+      using ltree_single_heap by fastforce
+    then show ?thesis
+      using ltree_heap_of_list'[where t = t and ts = ?ts] t by auto
+  qed
+  ultimately show ?thesis by auto
+qed
+
+end
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Keinholz_Jonas_jonas.keinholz@tum.de_510/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Kurz_Friedrich_friedrich.kurz@tum.de_544/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+friedrich.kurz@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Kurz_Friedrich_friedrich.kurz@tum.de_544/hw_10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,120 @@
+(** Score: 2/10
+  Too many \<open>sorry\<close>s in proofs.
+
+*)
+(*<*)
+theory hw_10
+  imports
+    "../../../Public/Thys/Leftist_Heap"
+begin
+(*>*)
+text {* \ExerciseSheet{10}{30.~6.~2017} *}
+
+
+(**
+ * HW 10
+ *)
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+fun split :: "'a list \<Rightarrow> 'a list * 'a list" where
+  "split [] = ([], [])"
+  | "split xs = (let n = length xs in
+    (take (divide n 2) xs, drop (divide n 2) xs)
+  )"
+
+lemma split_heap_list: "\<lbrakk>\<forall> x \<in> set xs. heap x; (ys, zs) = split xs\<rbrakk> \<Longrightarrow> (\<forall> y \<in> set ys. heap y)"
+  sorry
+
+value "split []"
+value "split [1]"
+value "split [1,2,3,4,5,6,7,8::int]"
+value "split [1,2,3,4,5,6,7,8,9::int]"
+
+fun heap_of_list' :: "'a::ord lheap list \<Rightarrow> 'a::ord lheap" where
+  "heap_of_list' [] = \<langle>\<rangle>"
+  | "heap_of_list' [a] = a"
+  | "heap_of_list' xs = (let (ys, zs) = split xs in
+    merge (heap_of_list' ys) (heap_of_list' zs)
+  )"
+
+fun singleton_heaps :: "('a::ord) list \<Rightarrow> ('a::ord) lheap list" where
+  "singleton_heaps [] = []"
+| "singleton_heaps (x # xs) =  \<langle>1, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle> # singleton_heaps xs"
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap" where
+  "heap_of_list xs = heap_of_list' (singleton_heaps xs)"
+
+value "heap_of_list [1,2,2,2,3,3,3,4,5::int]"
+value "mset_tree (heap_of_list [1,2,2,2,3,3,3,4,5::int]) = mset [1,2,2,2,3,3,3,4,5::int]"
+
+lemma hw_10_a[simp]: "\<forall> x \<in> set (singleton_heaps xs). heap x"
+  apply(induction xs rule: singleton_heaps.induct)
+  apply(auto simp: heap_merge)
+  done
+
+lemma hw_10_b: "\<lbrakk>\<forall>x\<in> set xs. heap x\<rbrakk> \<Longrightarrow> heap (heap_of_list' xs)"
+  apply(induction xs rule: heap_of_list'.induct)
+  apply(auto simp: heap_merge)
+  sorry
+
+thm merge.simps
+thm node_def
+thm mset_tree.simps
+thm split.induct
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+  sorry
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def
+proof -
+  obtain xs' where A: "xs' = singleton_heaps xs"
+    by auto
+  from hw_10_a and this have "\<forall>x \<in> set xs'. heap x"
+    by (auto)
+  thus "heap (heap_of_list' (singleton_heaps xs))"
+    using A hw_10_b
+    by blast
+qed
+
+
+lemma hw_10_c[simp]: "\<forall> x \<in> set (singleton_heaps xs). ltree x"
+  apply(induction xs rule: singleton_heaps.induct)
+  apply(auto simp: heap_merge)
+  done
+
+lemma hw_10_d: "\<lbrakk>\<forall>x\<in> set xs. ltree x\<rbrakk> \<Longrightarrow> ltree (heap_of_list' xs)"
+  apply(induction xs rule: heap_of_list'.induct)
+  apply(auto simp: heap_merge)
+  sorry
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def
+proof -
+  obtain xs' where A: "xs' = singleton_heaps xs"
+    by auto
+      from hw_10_c and this have "\<forall>x \<in> set xs'. ltree x"
+    by (auto)
+  thus "ltree (heap_of_list' (singleton_heaps xs))"
+    using A hw_10_d
+    by blast
+qed
+
+(*<*)
+end
+(*>*)
\ No newline at end of file```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Kurz_Friedrich_friedrich.kurz@tum.de_544/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -0,0 +1,1 @@
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -0,0 +1,148 @@
+(** Score: 10/10
+*)
+(*<*)
+theory tmpl10
+  imports "Leftist_Heap"
+begin
+(*>*)
+text {* \ExerciseSheet{10}{30.~6.~2017} *}
+
+text \<open>
+  \Exercise{Insert for Leftist Heap}
+
+  \<^item> Define a function to directly insert an element into a leftist heap.
+    Do not construct an intermediate heap like insert via meld does!
+
+  \<^item> Show that your function is correct
+
+  \<^item> Define a timing function for your insert function, and show that it is
+    linearly bounded by the rank of the tree.
+\<close>
+
+fun lh_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap"
+  where
+  "lh_insert x \<langle>\<rangle> = \<langle>1,\<langle>\<rangle>,x,\<langle>\<rangle>\<rangle>" |
+  "lh_insert x \<langle>n,l,a,r\<rangle> = (if rk r < rk l
+    then let r = lh_insert (max x a) r; n = rk r + 1 in \<langle>n,l,min x a,r\<rangle>
+    else \<langle>n,lh_insert (max x a) l,min x a,r\<rangle>)"
+
+lemma mset_lh_insert: "mset_tree (lh_insert x t) = mset_tree t + {# x #}"
+  by (induct x t rule: lh_insert.induct) (auto simp add: max_def min_def)
+
+lemma "heap t \<Longrightarrow> heap (lh_insert x t)"
+  apply (induct x t rule: lh_insert.induct,simp)
+  apply (auto simp add: max_def min_def)[1]
+       apply (meson UnCI order_trans)
+      apply (metis (no_types, lifting) Un_iff antisym_conv2 emptyE insertE less_le_trans linear mset_lh_insert set_mset_add_mset_insert set_mset_empty set_mset_union)
+     apply (metis (no_types, lifting) UnCI UnE antisym_conv2 emptyE insertE less_le_trans linear mset_lh_insert set_mset_add_mset_insert set_mset_empty set_mset_union)
+    apply (meson UnCI order_trans)
+  by (metis Un_iff emptyE insertE linear mset_lh_insert set_mset_add_mset_insert set_mset_empty set_mset_union)+
+
+lemma rank_insert_upper: "rank (lh_insert x t) \<le> rank t + 1"
+  by (induct x t rule: lh_insert.induct,simp) auto
+
+lemma rank_insert_lower: "rank t \<le> rank (lh_insert x t)"
+    by (induct x t rule: lh_insert.induct,simp) auto
+
+lemma "ltree t \<Longrightarrow> ltree (lh_insert x t)"
+  apply (induct x t rule: lh_insert.induct,simp)
+  apply (auto simp add: max_def min_def rank_insert_lower)[1]
+
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+definition for_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "for_all f xs = Ball (set xs) f"
+
+definition singleton :: "'a::ord \<Rightarrow> 'a::ord lheap" where
+  "singleton e = \<langle>1, \<langle>\<rangle>, e, \<langle>\<rangle>\<rangle>"
+
+fun reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "reduce _ [] = []" |
+  "reduce _ [x] = [x]" |
+  "reduce f (x1#x2#xs) = (f x1 x2) # (reduce f xs)"
+
+lemma reduce_smaller: "length (reduce f xs) < Suc (length xs)" by (induct f xs rule: reduce.induct) auto
+
+function (sequential) run :: "('a::ord) lheap list \<Rightarrow> 'a lheap" where
+  "run [] = Leaf" |
+  "run [x] = x" |
+  "run xs = run (reduce merge xs)"
+by pat_completeness auto
+termination by (relation "measure size") (auto simp add: reduce_smaller)
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list = run o map singleton"
+
+definition merge_l :: "'a::ord lheap list \<Rightarrow> 'a lheap"
+  where "merge_l xs = fold merge xs Leaf"
+
+
+lemma mset_merge_l_h: "mset_tree (fold merge xs t) = fold (\<lambda>x. op + (mset_tree x)) xs (mset_tree t)"
+  by (induct xs arbitrary: t, simp) (auto simp add: mset_merge)
+
+lemma mset_merge_l: "mset_tree (merge_l xs) = fold (\<lambda>x. op + (mset_tree x)) xs {#}" unfolding merge_l_def
+
+lemma add_assoc: "fold (\<lambda>x. op + (mset_tree x)) xs s = s + fold (\<lambda>x. op + (mset_tree x)) xs {#}"
+  by (induct xs arbitrary: s, simp) (metis (no_types, lifting) add.assoc fold_simps(2) union_commute)
+
+
+lemma mset_reduce: "f = merge \<Longrightarrow> mset_tree (merge_l (reduce f xs)) = mset_tree (merge_l xs)" unfolding for_all_def
+  by (induct f xs rule: reduce.induct,simp_all) (smt add.assoc add_assoc fold_simps(2) mset_merge mset_merge_l)
+
+lemma mset_run: "mset_tree (run xs) = mset_tree (merge_l xs)" unfolding merge_l_def
+  apply (induct xs rule: run.induct)
+    apply simp
+   apply (auto simp add: mset_merge)[1]
+  by (metis mset_merge_l mset_merge_l_h mset_reduce mset_tree.simps(1) run.simps(3))
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def singleton_def
+  apply (induct xs, simp)
+  by (smt add_assoc add_mset_add_single comp_def fold_simps(2) lh_insert.simps(1) list.simps(9) merge_l_def mset.simps(2) mset_lh_insert mset_merge_l mset_merge_l_h mset_run union_commute union_lcomm)
+
+
+lemma heap_reduce: "f = merge \<Longrightarrow> for_all heap xs \<Longrightarrow> for_all heap (reduce f xs)" unfolding for_all_def
+  by (induct f xs rule: reduce.induct) (auto simp add: heap_merge)
+
+lemma heap_run: "for_all heap xs \<Longrightarrow> heap (run xs)" unfolding for_all_def
+  apply (induct xs  rule: run.induct)
+    apply (auto simp add: heap_merge)
+  by (metis for_all_def heap_reduce)
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def
+  by (induct xs, simp) (auto simp add: for_all_def heap_run singleton_def)
+
+
+lemma ltree_reduce: "f = merge \<Longrightarrow> for_all ltree xs \<Longrightarrow> for_all ltree (reduce f xs)" unfolding for_all_def
+  by (induct f xs rule: reduce.induct) (auto simp add: ltree_merge)
+
+lemma ltree_run: "for_all ltree xs \<Longrightarrow> ltree (run xs)" unfolding for_all_def
+  apply (induct xs rule: run.induct)
+    apply (auto simp add: ltree_merge)
+  by (metis for_all_def ltree_reduce)
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def
+  by (induct xs, simp)  (auto simp add: for_all_def ltree_run singleton_def)
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Ouyang_Lena_ga96vup@mytum.de_523/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+ga96vup@mytum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Ouyang_Lena_ga96vup@mytum.de_523/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,123 @@
+(** Score: 2/10
+  too many sorries
+*)
+(*<*)
+theory hw10
+imports
+    "../../../../Desktop/fds/Thys/Leftist_Heap"
+begin
+(*>*)
+  fun lh_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap"
+  where
+  "lh_insert a \<langle>\<rangle> = \<langle>1,\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>"
+| "lh_insert a \<langle>h,l,b,r\<rangle> = (
+    if a\<le>b then
+      node l a (lh_insert b r)
+    else
+      node l b (lh_insert a r)
+    )"
+
+find_theorems node ltree
+find_theorems node heap
+find_theorems node mset_tree
+
+lemma mset_tree_node[simp]:
+  "mset_tree (node l a r) = mset_tree l + {#a#} + mset_tree r"
+  unfolding node_def by auto
+
+lemma mset_lh_insert[simp]:
+  shows "mset_tree (lh_insert x t) = mset_tree t + {# x #}"
+  apply (induction x t rule: lh_insert.induct)
+  apply (auto)
+  done
+
+declare heap_node[simp]
+
+lemma heap_lh_insert[intro, simp]: "heap t \<Longrightarrow> heap (lh_insert x t)"
+  by (induction x t rule: lh_insert.induct) force+
+
+lemma "heap t \<Longrightarrow> heap (lh_insert x t)"
+  apply (induction x t rule: lh_insert.induct)
+  subgoal by (simp)
+  subgoal by (force)
+  done
+
+declare ltree_node[simp]
+
+lemma "ltree t \<Longrightarrow> ltree (lh_insert x t)"
+  by (induction x t rule: lh_insert.induct) auto
+
+
+fun t_lh_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat"
+  where
+  "t_lh_insert a \<langle>\<rangle> = 1"
+| "t_lh_insert a \<langle>h,l,b,r\<rangle> = 1 + (
+    if a\<le>b then
+      1+t_lh_insert b r
+    else
+      1+t_lh_insert a r
+    )"
+
+lemma "t_lh_insert x t \<le> 2*rank t + 1"
+  by (induction x t rule: lh_insert.induct) auto
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+The naive solution of starting with the empty heap and inserting the elements one by one can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps. Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+fun heap_list :: "'a::ord list \<Rightarrow> 'a::ord lheap list" where
+  "heap_list [] = []"|
+  "heap_list (x#xs) = (\<langle>1,\<langle>\<rangle>,x,\<langle>\<rangle>\<rangle>)#(heap_list xs)"
+function (sequential) heap_list_to_heap :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "heap_list_to_heap [] = []"|
+  "heap_list_to_heap [x] = [x]"|
+  "heap_list_to_heap (x#y#z) = heap_list_to_heap((merge x y)#(heap_list_to_heap z))"
+  by pat_completeness auto
+termination sorry
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list x = (case (heap_list_to_heap (heap_list x)) of [] \<Rightarrow> \<langle>\<rangle>| [y] \<Rightarrow> y)"
+
+lemma a[simp]:"y \<noteq> [] \<Longrightarrow> heap_list_to_heap (y) \<noteq> []"
+  apply (induction y rule:heap_list_to_heap.induct)
+  by auto
+
+lemma b[simp]:"heap_list_to_heap (x) \<noteq> x21 # x21a # x22a"
+  apply (induction x rule: heap_list_to_heap.induct)
+  by auto
+lemma c[simp]:"heap_list_to_heap (x # heap_list xs) = [x21a] \<Longrightarrow> mset_tree x21a = (mset_tree x) + (mset xs)"
+  apply (induction xs arbitrary: x)
+   apply (auto simp: split:if_splits)
+  sorry
+
+find_theorems node mset_tree
+
+lemma mset_heap_of_list[simp]: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+  apply (induction xs)
+    by (auto split:list.splits)
+
+lemma heap_heap_of_list[simp]: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def
+  apply (auto split:list.splits)
+   apply (induction xs)
+   apply auto
+    sorry
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def
+  apply (auto split:list.splits)
+  apply (induction xs)
+   apply auto
+
+    sorry
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Ouyang_Lena_ga96vup@mytum.de_523/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Rdle_Karl_Jonas_jonas.raedle@tum.de_514/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+jonas.raedle@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Rdle_Karl_Jonas_jonas.raedle@tum.de_514/hw10_sub.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,100 @@
+(** Score: 10/10
+*)
+theory hw10_sub
+imports
+    "../../../Public/Thys/Leftist_Heap"
+begin
+
+fun heap_of_list_singletons :: "'a::ord list \<Rightarrow> 'a lheap list" where
+  "heap_of_list_singletons [] = []" |
+  "heap_of_list_singletons (x#xs) = (insert x Leaf) # (heap_of_list_singletons xs)"
+
+fun heap_of_list_merge :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "heap_of_list_merge [] = []" |
+  "heap_of_list_merge [x] = [x]" |
+  "heap_of_list_merge (x#y#ys) = (merge x y) # (heap_of_list_merge ys)"
+
+lemma length_merge_help : "length xs < 1 \<Longrightarrow> length (heap_of_list_merge xs) = length xs"
+  by simp
+
+lemma length_merge: "length (heap_of_list_merge xs) < Suc (length xs)"
+  apply(induction xs rule: heap_of_list_merge.induct) by auto
+
+function heap_of_list_build :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+  "heap_of_list_build [] = Leaf" |
+  "heap_of_list_build [x] = x" |
+  "heap_of_list_build (x#y#xs) = heap_of_list_build (heap_of_list_merge (x#y#xs))"
+by pat_completeness auto
+termination by (relation "measure (%(xs). length xs)") (auto simp add: length_merge)
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap" where
+  "heap_of_list xs = heap_of_list_build (heap_of_list_singletons xs)"
+
+lemma mset_heap_merge: "fold (op +) (map mset_tree (heap_of_list_merge xs)) {#} = fold (op +) (map mset_tree xs) {#}"
+  proof(induction xs rule: heap_of_list_merge.induct)
+    case 1
+    then show ?case by simp
+  next
+    case (2 x)
+    then show ?case by simp
+  next
+    case (3 x y ys)
+    have "fold (op +) (map mset_tree (heap_of_list_merge (x # y # ys))) {#} =
+      fold (op +) (map mset_tree (merge x y # heap_of_list_merge ys)) {#}" by simp
+    also have "\<dots> = fold (op +) (mset_tree (merge x y) # (map mset_tree (heap_of_list_merge ys))) {#}"
+      by simp
+    also have "\<dots> = (mset_tree (merge x y)) + (fold (op +) (map mset_tree (heap_of_list_merge ys)) {#})"
+    also have "\<dots> = (mset_tree (merge x y)) + (fold op + (map mset_tree ys) {#})" using "3.IH" by simp
+    also have "\<dots> = fold op + ((mset_tree (merge x y)) # map mset_tree ys) {#}"
+    finally have "fold (op +) (map mset_tree (heap_of_list_merge (x # y # ys))) {#}
+      = fold op + (map mset_tree (x # y # ys)) {#}" by (simp add: mset_merge union_commute)
+    then show ?case by simp
+  qed
+
+lemma mset_heap_build: "mset_tree (heap_of_list_build xs) = fold (op +) (map mset_tree xs) {#}"
+  apply (induction xs rule: heap_of_list_build.induct)
+    apply (simp, simp)
+  by (metis heap_of_list_build.simps(3) mset_heap_merge)
+
+lemma mset_heap_singletons: "mset xs = fold (op +) (map mset_tree (heap_of_list_singletons xs)) {#}"
+  apply(induction xs rule: heap_of_list_singletons.induct)
+  by (auto simp add: mset_insert fold_plus_sum_list_rev)
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+  using mset_heap_build mset_heap_singletons by metis
+
+lemma heap_heap_singletons: "x \<in> set (heap_of_list_singletons xs) \<Longrightarrow> heap x"
+  apply(induction xs rule: heap_of_list_singletons.induct) by auto
+
+lemma heap_heap_merge: "(\<forall> x. (x \<in> set xs \<longrightarrow> heap x)) \<Longrightarrow> (\<forall> x. (x \<in> set (heap_of_list_merge xs) \<longrightarrow> heap x))"
+  apply(induction xs rule: heap_of_list_merge.induct) by (auto simp add: heap_merge)
+
+lemma heap_heap_build: "(\<forall> x. (x \<in> set xs \<longrightarrow> heap x)) \<Longrightarrow> heap (heap_of_list_build xs)"
+  apply(induction xs rule: heap_of_list_build.induct)
+    apply (simp, simp)
+  by (metis heap_of_list_build.simps(3) heap_heap_merge)
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def
+  using heap_heap_singletons heap_heap_build by blast
+
+lemma ltree_ltree_singletons: "x \<in> set (heap_of_list_singletons xs) \<Longrightarrow> ltree x"
+  apply(induction xs rule: heap_of_list_singletons.induct) using ltree_insert by force+
+
+lemma ltree_ltree_merge: "(\<forall> x. (x \<in> set xs \<longrightarrow> ltree x)) \<Longrightarrow> (\<forall> x. (x \<in> set (heap_of_list_merge xs) \<longrightarrow> ltree x))"
+  apply(induction xs rule: heap_of_list_merge.induct) by (auto simp add: ltree_merge)
+
+lemma ltree_ltree_build: "(\<forall> x. (x \<in> set xs \<longrightarrow> ltree x)) \<Longrightarrow> ltree (heap_of_list_build xs)"
+  apply(induction xs rule: heap_of_list_build.induct)
+    apply (simp, simp)
+  by (metis heap_of_list_build.simps(3) ltree_ltree_merge)
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def
+  using ltree_ltree_singletons ltree_ltree_build by blast
+
+end
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Rdle_Karl_Jonas_jonas.raedle@tum.de_514/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Rokopf_Simon_simon.rosskopf@tum.de_515/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+simon.rosskopf@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Rokopf_Simon_simon.rosskopf@tum.de_515/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Rokopf_Simon_simon.rosskopf@tum.de_515/tmpl10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,202 @@
+(** Score: 10/10
+*)
+(*<*)
+theory tmpl10
+imports
+    "~~/src/HOL/Data_Structures/Tree2"
+    "~~/src/HOL/Library/Multiset"
+    Complex_Main
+begin
+
+(* Inlining Leftist_Heap *)
+
+fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
+
+type_synonym 'a lheap = "('a,nat)tree"
+
+fun rank :: "'a lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "'a lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "('a,'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l m r) =
+  (heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). m \<le> x))"
+
+fun ltree :: "'a lheap \<Rightarrow> bool" where
+"ltree Leaf = True" |
+"ltree (Node n l a r) =
+ (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
+
+definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
+"node l a r =
+ (let rl = rk l; rr = rk r
+  in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)"
+
+fun get_min :: "'a lheap \<Rightarrow> 'a" where
+"get_min(Node n l a r) = a"
+
+lemma size_prod_measure[measure_function]:
+  "is_measure f \<Longrightarrow> is_measure g \<Longrightarrow> is_measure (size_prod f g)"
+  by (rule is_measure_trivial)
+
+fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
+   (if a1 \<le> a2 then node l1 a1 (merge r1 (Node n2 l2 a2 r2))
+    else node l2 a2 (merge r2 (Node n1 l1 a1 r1)))"
+(*by pat_completeness auto
+termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto
+*)
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow>
+    if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+subsection "Lemmas"
+
+declare Let_def [simp]
+
+lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
+by(cases t) auto
+
+lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"
+
+lemma heap_node: "heap (node l a r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). a \<le> x)"
+
+subsection "Functional Correctness"
+
+lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2"
+by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps)
+
+lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
+by (auto simp add: insert_def mset_merge)
+
+lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
+by (cases h) (auto simp: mset_merge)
+
+lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
+proof(induction l r rule: merge.induct)
+  case (3 n1 l1 a1 r1 n2 l2 a2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 a1 (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+    also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> a1 \<le> a2"
+    thus ?thesis using 3 by(simp)(auto simp: ltree_node)
+  qed
+qed simp_all
+
+lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"
+proof(induction l r rule: merge.induct)
+  case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un)
+qed simp_all
+
+lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)"
+by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)
+
+lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
+by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
+
+lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
+by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
+
+lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
+by(cases t)(auto simp add: heap_merge simp del: merge.simps)
+
+
+
+
+(* Homework begins here *)
+
+lemma mset_tree_node[simp]: "mset_tree (node l a r) = mset_tree l + {#a#} + mset_tree r"
+  unfolding node_def by auto
+
+fun singletons :: "'a::ord list \<Rightarrow> 'a lheap list" where
+  "singletons xs = map (\<lambda>x. node \<langle>\<rangle> x \<langle>\<rangle>) xs"
+
+lemma mset_tree_singletons: "foldr (\<lambda>x y . mset_tree x + y) (singletons xs) {#} = mset xs"
+  by (induction xs) simp_all
+
+lemma heap_singletons: "list_all heap (singletons xs)"
+  by (induction xs) (simp_all add: heap_node)
+
+lemma ltree_singletons: "list_all ltree (singletons xs)"
+  by (induction xs) (simp_all add: ltree_node)
+
+fun onePass :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "onePass [] = []"
+| "onePass [x] = [x]"
+| "onePass (x1#x2#xs) = merge x1 x2 # onePass xs"
+
+lemma length_onePass: "length (onePass xs) < (Suc ((length xs)))"
+  by (induction xs rule: onePass.induct) simp_all
+
+lemma mset_tree_onePass: "foldr (\<lambda>x y . mset_tree x + y) (onePass xs) {#} = foldr (\<lambda>x y . mset_tree x + y) xs {#}"
+  by (induction rule: onePass.induct) (simp_all add: mset_merge)
+
+lemma heap_onePass: "list_all heap xs \<Longrightarrow> list_all heap (onePass xs)"
+  by (induction xs rule: onePass.induct) (simp_all add: heap_merge)
+
+lemma ltree_onePass: "list_all ltree xs \<Longrightarrow> list_all ltree (onePass xs)"
+  by (induction xs rule: onePass.induct) (simp_all add: ltree_merge)
+
+function imp :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+  "imp [] = \<langle>\<rangle>"
+| "imp [x] = x"
+| "imp (x1#x2#xs) = imp (onePass (x1#x2#xs))"
+  by pat_completeness simp_all
+termination by (relation "measure length") (simp_all add: length_onePass)
+
+lemma mset_tree_imp: "mset_tree (imp xs) = foldr (\<lambda>x y . mset_tree x + y) xs {#}"
+  by (induction xs rule: imp.induct)  (simp_all add: mset_merge mset_tree_onePass)
+
+lemma heap_imp: "list_all heap xs \<Longrightarrow> heap (imp xs)"
+  by (induction xs rule: imp.induct) (simp_all add: heap_merge heap_onePass)
+
+lemma ltree_imp: "list_all ltree xs \<Longrightarrow> ltree (imp xs)"
+  by (induction xs rule: imp.induct) (simp_all add: ltree_merge ltree_onePass)
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list  = imp o singletons"
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def using mset_tree_singletons mset_tree_imp by (metis comp_apply)
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def using heap_imp heap_singletons by auto
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def using ltree_imp ltree_singletons by auto
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Saporta_Antoine_Jacques_antoine.saporta@tum.de_517/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+antoine.saporta@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Saporta_Antoine_Jacques_antoine.saporta@tum.de_517/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,63 @@
+(** Score: 2/10
+  No proofs, slightly problematic heap_from_heap_list definition.
+*)
+(*<*)
+theory hw10
+imports
+    "../../../Public/Thys/Leftist_Heap"
+begin
+(*>*)
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+definition list_of_heaps :: "'a::ord list \<Rightarrow> 'a lheap list" where
+"list_of_heaps xs = map (\<lambda>x. Node 1 Leaf x Leaf) xs"
+
+fun merge_heaps :: "'a::ord lheap list \<Rightarrow> 'a::ord lheap list" where
+"merge_heaps [t] = [t]" |
+"merge_heaps (t1#t2#ts) = merge_heaps (ts @ [merge t1 t2])"
+
+fun heap_from_heap_list :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+"heap_from_heap_list [] = Leaf" |
+"heap_from_heap_list [t] = t" |
+"heap_from_heap_list (t1#t2#ts) = heap_from_heap_list(ts @ [merge t1 t2])"
+(** You are implicitly using the ordering of the list to control the sequence of merges.
+  For the desired complexity, the \<open>op @\<close> may be problematic.
+*)
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+where "heap_of_list xs = heap_from_heap_list (list_of_heaps xs)"
+
+(* Couldn't prove the lemmas, probably because of the function definition *)
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  apply(induction xs)
+  apply (auto simp: list_of_heaps_def heap_of_list_def)
+sorry
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  apply(induction xs)
+  apply (auto simp: list_of_heaps_def heap_of_list_def)
+sorry
+
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  apply(induction xs)
+  apply (auto simp: list_of_heaps_def heap_of_list_def)
+sorry
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Saporta_Antoine_Jacques_antoine.saporta@tum.de_517/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_541/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+maximilian.schaeffeler@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_541/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,73 @@
+(** Score: 5/10
+  proved correct wrong function.
+*)
+(*<*)
+theory hw10
+imports
+    "../../../Public/Thys/Leftist_Heap"
+begin
+(*>*)
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+(** The name map_pairs of this function is misleading, as it actually only maps the **first** pair.
+  Thus, your compress_heap does not behave as required, but builds up the heap by iterated
+  merging from the beginning of the list!
+*)
+fun map_pairs :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "map_pairs f [] = []" |
+  "map_pairs f [x] = [x]" |
+  "map_pairs f (x#y#xs) = (f x y) #xs"
+
+fun compress_heap :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+  "compress_heap (h1#(h2#hs)) = compress_heap (map_pairs merge (h1#h2#hs))" |
+  "compress_heap [] = Leaf" |
+  "compress_heap [h] = h"
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list l = compress_heap(map (\<lambda> x. (insert x Leaf)) l)"
+
+
+lemma [simp]: "mset_tree (compress_heap (merge x y # hs)) =
+               mset_tree x + mset_tree (compress_heap (y # hs))"
+  apply (induction hs arbitrary: x y) by (auto simp add: mset_merge)
+
+lemma [simp]: "mset_tree (compress_heap (x#xs)) = mset_tree x + mset_tree(compress_heap xs)"
+  apply (induction xs arbitrary: x rule: compress_heap.induct) by (auto simp add: mset_merge)
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  apply (induction xs) by (auto simp add: insert_def heap_of_list_def)
+
+
+lemma [simp]: "\<forall>h\<in>(set hs). heap h \<Longrightarrow> heap (compress_heap hs)"
+  apply (induction hs rule: compress_heap.induct)
+  apply auto
+  using heap_merge by blast
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  apply (induction xs) by (auto simp add: heap_of_list_def)
+
+
+lemma ltree_list_imp_ltree_compressed: "\<forall>h\<in>(set hs). ltree h \<Longrightarrow> ltree (compress_heap hs)"
+  apply (induction hs rule: compress_heap.induct) by (auto simp add: ltree_merge)
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  apply (induction xs)
+  by (auto simp add: ltree_list_imp_ltree_compressed heap_of_list_def ltree_insert)
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_541/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Somogyi_Daniel_daniel.somogyi@tum.de_542/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+daniel.somogyi@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Somogyi_Daniel_daniel.somogyi@tum.de_542/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,123 @@
+(** Score: 10/10
+*)
+theory hw10
+imports
+    "Demos/Leftist_Heap"
+begin
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+fun singletons :: "'a::ord list \<Rightarrow> ('a lheap) list"
+  where "singletons [] = []"
+  | "singletons (x#xs) = (Node 1 \<langle>\<rangle> x \<langle>\<rangle> )#singletons xs"
+
+fun merging_round :: "('a::ord lheap) list \<Rightarrow> ('a lheap) list" where
+  "merging_round [] = []"
+  | "merging_round [x] = [x]"
+  | "merging_round (x#y#xs) = (Leftist_Heap.merge x y) # (merging_round xs)"
+
+
+(*needed because otherwise isabelle cant proof the termination of merge_them*)
+lemma [simp]:"length (merging_round xs) \<le> length xs"
+  by(induction xs rule:merging_round.induct) auto
+
+fun merge_them:: "('a:: ord lheap) list \<Rightarrow> ('a lheap)" where
+ "merge_them [] = \<langle>\<rangle>"
+| "merge_them [x] = x"
+| "merge_them (x#xs) = merge_them (merging_round (x#xs))"
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list xs = merge_them (singletons xs)"
+
+
+(* ---------------------- MSET PROPERTY ------------------------- *)
+lemma mset_aux1: "(\<Sum>t\<in>#mset (singletons xs). mset_tree t) = mset xs"
+  by(induction xs rule:singletons.induct)auto
+
+lemma mset_aux2: "(\<Sum>t\<in>#mset (merging_round xs). mset_tree t)
+  = (\<Sum>t\<in># mset(xs). mset_tree t)"
+  by(induction xs rule:merging_round.induct)(auto simp:mset_merge)
+
+lemma mset_aux3:"mset_tree (merge_them xs)  = (\<Sum>t\<in># mset(xs). mset_tree t)"
+  by(induction xs rule:merge_them.induct)(auto simp:mset_aux2 mset_merge)
+
+
+theorem mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+  proof -
+  obtain singles where s_def:"singles = singletons xs" by auto
+  hence "(\<Sum>t\<in>#mset (singles). mset_tree t) = mset xs"
+    using mset_aux1 by auto
+
+  thus "mset_tree (merge_them (singletons xs)) = mset xs"
+    using mset_aux3[of singles] by (auto simp:s_def)
+  qed
+
+
+(* ---------------------- HEAP PROPERTY ------------------------- *)
+(* singletons are heaps*)
+lemma heap_aux1: "x \<in> set (singletons xs) \<Longrightarrow> heap x"
+  by(induction xs rule:singletons.induct) auto
+
+(* merging round makes heaps IF it gets a list of heaps *)
+lemma heap_aux2: "\<forall> x\<in> set(xs). heap x
+    \<Longrightarrow> \<forall> y\<in> set (merging_round xs). heap y"
+  by(induction xs rule:merging_round.induct)
+    (auto simp:heap_merge)
+
+(* merge_them finishes in 1 element *)
+lemma heap_aux3: "\<forall> x\<in> set(xs). heap x
+    \<Longrightarrow> heap (merge_them xs)"
+  by(induction xs rule:merge_them.induct) (auto simp:heap_aux2)
+
+theorem heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def
+proof -
+  obtain singles where s_def:"singles = singletons xs" by auto
+  hence "\<forall>x\<in> set(singles) . heap x" using heap_aux1 by auto
+
+  thus "heap (merge_them (singletons xs))" using heap_aux3[of singles]
+      by(auto simp: s_def)
+  qed
+
+
+(* ---------------------- LTREE PROPERTY ------------------------- *)
+lemma ltree_aux1: "x \<in> set (singletons xs) \<Longrightarrow> ltree x"
+  by(induction xs rule:singletons.induct) auto
+
+lemma ltree_aux2: "\<forall> x\<in> set(xs). ltree x
+    \<Longrightarrow> \<forall> y\<in> set (merging_round xs). ltree y"
+  by(induction xs rule:merging_round.induct)
+    (auto simp:ltree_merge)
+
+lemma ltree_aux3: "\<forall> x\<in> set(xs). ltree x
+    \<Longrightarrow> ltree (merge_them xs)"
+  by(induction xs rule:merge_them.induct) (auto simp:ltree_aux2)
+
+theorem ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def
+proof -
+  obtain singles where s_def:"singles = singletons xs" by auto
+  hence "\<forall>x\<in> set(singles) . ltree x" using ltree_aux1 by auto
+
+  thus "ltree (merge_them (singletons xs))" using ltree_aux3[of singles]
+      by(auto simp: s_def)
+  qed
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Somogyi_Daniel_daniel.somogyi@tum.de_542/user_error_log.txt	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,6 @@
+Using temporary directory '/tmp/tmp.dIdFrZWM0L'
+Files in /tmp/eval-542-QJtghG: hw10.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/10/Stevens_Lukas_lukas.stevens@tum.de_492/Ex10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,122 @@
+(** Score: 10/10
+*)
+(*<*)
+theory Ex10
+imports
+    "../Thys/Leftist_Heap"
+begin
+(*>*)
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+fun merge_pairwise :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+  "merge_pairwise [] = []" |
+  "merge_pairwise [x] = [x]" |
+  "merge_pairwise (x1#x2#xs) = (merge x1 x2)#(merge_pairwise xs)"
+
+lemma length_merge_pairwise: "length (merge_pairwise xs) < Suc (length xs)"
+  by(induction xs rule: merge_pairwise.induct) (auto)
+
+function heap_of_list_helper :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+  "heap_of_list_helper [] = Leaf" |
+  "heap_of_list_helper [x] = x" |
+  "heap_of_list_helper (x1#x2#xs) = heap_of_list_helper (merge_pairwise (x1#x2#xs))"
+  by(pat_completeness) auto
+termination
+  by(relation "measure length") (auto simp add: length_merge_pairwise)
+
+fun to_tree :: "'a::ord \<Rightarrow> 'a lheap" where
+  "to_tree a = \<langle>1,\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>"
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list xs = heap_of_list_helper (map to_tree xs)"
+
+
+lemmas length_induct_rule = measure_induct_rule[where f=length, case_names shorter]
+
+lemma heap_of_list_helper_merge_pairwise:
+  "mset_tree (heap_of_list_helper (merge_pairwise xs)) = mset_tree (heap_of_list_helper xs)"
+  by (induction xs rule: heap_of_list_helper.induct) auto
+
+lemma mset_heap_of_list_helper:
+  "mset_tree (heap_of_list_helper (x1#xs)) = mset_tree x1 + mset_tree (heap_of_list_helper xs)"
+  unfolding heap_of_list_def
+proof (induction xs arbitrary: x1 rule: length_induct_rule)
+  case (shorter xs)
+  show ?case proof (cases xs)
+    case Nil
+    then show ?thesis by auto
+  next
+    case (Cons x2 xss)
+    then have "mset_tree (heap_of_list_helper (x1 # xs)) =
+      mset_tree (heap_of_list_helper (x1 # x2 # xss))" by simp
+    also have "\<dots> = mset_tree (heap_of_list_helper (merge x1 x2 # merge_pairwise xss))" by(simp)
+    also have "\<dots> = mset_tree (merge x1 x2) + mset_tree (heap_of_list_helper (merge_pairwise xss))"
+      using shorter length_merge_pairwise Cons by auto
+    also have "\<dots> = mset_tree x1 + mset_tree x2 + mset_tree (heap_of_list_helper (merge_pairwise xss))"
+      using mset_merge by simp
+    also have "\<dots> = mset_tree x1 + mset_tree x2 + mset_tree (heap_of_list_helper xss)"
+      using heap_of_list_helper_merge_pairwise by simp
+    also have "\<dots> = mset_tree x1 + mset_tree (heap_of_list_helper (x2#xss))"
+      using shorter[symmetric, of "xss" "x2"] using Cons by auto
+    finally show ?thesis using Cons by blast
+  qed
+qed
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+  by(induction xs) (auto simp add: mset_heap_of_list_helper)
+
+
+lemma heap_merge_pairwise: "\<lbrakk>\<forall>x \<in> set xs. heap x\<rbrakk> \<Longrightarrow> \<forall>x \<in> set (merge_pairwise xs). heap x"
+  apply(induction xs rule: merge_pairwise.induct)
+  done
+
+lemma heap_heap_of_list_helper:
+  "\<lbrakk>\<forall>x \<in> set xs. heap x\<rbrakk> \<Longrightarrow> heap (heap_of_list_helper xs)"
+  apply(induction xs rule: heap_of_list_helper.induct)
+  done
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def
+  apply(induction "map to_tree xs" rule: heap_of_list_helper.induct)
+  done
+
+
+lemma ltree_merge_pairwise: "\<lbrakk>\<forall>x \<in> set xs. ltree x\<rbrakk> \<Longrightarrow> \<forall>x \<in> set (merge_pairwise xs). ltree x"
+  apply(induction xs rule: merge_pairwise.induct)
+  done
+
+lemma ltree_heap_of_list_helper:
+  "\<lbrakk>\<forall>x \<in> set xs. ltree x\<rbrakk> \<Longrightarrow> ltree (heap_of_list_helper xs)"
+  apply(induction xs rule: heap_of_list_helper.induct)
+  done
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def
+  apply(induction "map to_tree xs" rule: heap_of_list_helper.induct)
+    apply(auto simp add: ltree_heap_of_list_helper ltree_node)
+  done
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Stevens_Lukas_lukas.stevens@tum.de_492/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+lukas.stevens@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Stevens_Lukas_lukas.stevens@tum.de_492/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Stwe_Daniel_daniel.stuewe@tum.de_516/HW10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,89 @@
+(** Score: 10/10
+*)
+theory HW10
+imports
+    "Thys/Leftist_Heap"
+begin
+
+fun compress :: "('a::ord) lheap list \<Rightarrow> 'a lheap list" where
+  "compress [] = []" |
+  "compress [t] = [t]" |
+  "compress (t#t'#ts) = merge t t' # compress ts"
+
+lemma [simp]: "length (compress ts) \<le> length ts"
+  by (induction ts rule: compress.induct) auto
+
+fun compressI :: "('a::ord) lheap list \<Rightarrow> 'a lheap list" where
+  "compressI [] = [Leaf]" |
+  "compressI [t] = [t]" |
+  "compressI (t#t'#ts) = compressI (compress (t # t' # ts))"
+
+definition singleton where "singleton x = insert x Leaf"
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list = (\<lambda> xs. if xs = [] then Leaf else hd xs) o compressI o map singleton"
+
+lemmas [simp] = mset_merge mset_insert singleton_def heap_of_list_def
+
+lemma compress_mset[simp]: "\<Union># (mset (map mset_tree (compress xs))) = \<Union># (mset (map mset_tree xs))"
+  by (induction xs rule: compress.induct) auto
+
+lemma compressI_mset[simp]: "\<Union># (mset (map mset_tree (compressI xs))) = \<Union># (mset (map mset_tree xs))"
+  by (induction xs rule: compressI.induct) (simp_all del: mset_map)
+
+lemma [simp]: "compressI xs = [] \<longleftrightarrow> False"
+  by (induction xs rule: compressI.induct) auto
+
+lemma compressI_nonE_single: "\<exists> t. compressI xs = [t]"
+  by (induction xs rule: compressI.induct) auto
+
+lemma insert_map_mset: "\<Union># (mset (map mset_tree (map singleton xs))) = mset xs"
+  by (induction xs) simp_all
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+proof clarsimp
+  let ?xs' = "map singleton xs"
+  obtain t where [simp] : "compressI ?xs' = [t]"
+    using compressI_nonE_single by blast
+  have "\<Union># (mset (map mset_tree (compressI ?xs'))) = mset xs"
+    by (metis compressI_mset insert_map_mset mset_map)
+  then show "mset_tree (hd (compressI ?xs')) = mset xs" by auto
+qed
+
+lemma compress_heap: "\<forall> t \<in> set xs. heap t \<Longrightarrow> \<forall> t \<in> set (compress xs) . heap t"
+  by (induction xs rule: compress.induct) (simp_all add: heap_merge)
+
+lemma compressI_heap: "\<forall> t \<in> set xs. heap t \<Longrightarrow> \<forall> t \<in> set (compressI xs) . heap t"
+  by (induction xs rule: compressI.induct) (simp_all add: compress_heap)
+
+lemma map_insert_heap: "\<forall> t \<in> set (map singleton xs) . heap t"
+  by (induction xs) auto
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+proof clarsimp
+  let ?xs' = "map singleton xs"
+  obtain t where [simp] : "compressI ?xs' = [t]"
+    using compressI_nonE_single by blast
+  hence "heap t" using compressI_heap[of ?xs'] map_insert_heap by fastforce
+  thus "heap (hd (compressI ?xs'))" by auto
+qed
+
+lemma compress_ltree: "\<forall> t \<in> set xs. ltree t \<Longrightarrow> \<forall> t \<in> set (compress xs) . ltree t"
+  by (induction xs rule: compress.induct) (auto simp: ltree_merge)
+
+lemma compressI_ltree: "\<forall> t \<in> set xs. ltree t \<Longrightarrow> \<forall> t \<in> set (compressI xs) . ltree t"
+  by (induction xs rule: compressI.induct) (simp_all add: compress_ltree)
+
+lemma map_insert_ltree: "\<forall> t \<in> set (map singleton xs) . ltree t"
+  by (induction xs) (simp_all add: insert_def)
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+proof clarsimp
+  let ?xs' = "map singleton xs"
+  obtain t where [simp] : "compressI ?xs' = [t]"
+    using compressI_nonE_single by blast
+  hence "ltree t" using compressI_ltree[of ?xs'] map_insert_ltree by fastforce
+  thus "ltree (hd (compressI ?xs'))" by auto
+qed
+
+end
\ No newline at end of file```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Stwe_Daniel_daniel.stuewe@tum.de_516/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+daniel.stuewe@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Stwe_Daniel_daniel.stuewe@tum.de_516/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_508/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+sreeharsha.totakura@mytum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_508/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,94 @@
+(** Score: 10/10
+*)
+(*<*)
+theory hw10
+imports
+    "../../fds_ss17/Thys/Leftist_Heap"
+begin
+(*>*)
+
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+fun fold_heaps::"'a::ord lheap list \<Rightarrow> 'a lheap list \<Rightarrow> 'a lheap" where
+  "fold_heaps [] [] = Leaf" |
+  "fold_heaps [] [x] = x" |
+  "fold_heaps acc [] = fold_heaps [] acc" |
+  "fold_heaps (a#acc) [x] = fold_heaps [(merge a x)] (acc)" |
+  "fold_heaps acc (x#y#ys) = fold_heaps ((merge x y) # acc) ys"
+
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap"
+  where "heap_of_list xs = fold_heaps [] (map (\<lambda>x. insert x Leaf) xs)"
+
+definition mset_tree_fold::"('a,'b) tree list \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
+  "mset_tree_fold xs acc= fold (\<lambda>t m. m + mset_tree t) xs acc "
+
+lemma "fold_heaps acc [] = fold_heaps [] acc"
+  apply (cases acc) by auto
+
+lemma mset_tree_fold_mset[simp]: "mset_tree_fold (map (\<lambda>x. insert x Leaf) xs) ms = mset xs + ms"
+  unfolding mset_tree_fold_def
+  apply (induction xs arbitrary:ms)
+   apply (auto simp:mset_insert)
+  done
+
+lemma mset_tree_fold_assoc: "mset_tree_fold xs (ys + zs) =  mset_tree_fold xs ys + zs"
+  apply (induct xs arbitrary: ys zs)
+   apply (auto simp:mset_tree_fold_def)
+  done
+
+lemma mset_fold_heaps_gen:
+ "mset_tree (fold_heaps xs ys) + zs = mset_tree_fold xs (mset_tree_fold ys zs)"
+  apply (induction xs ys arbitrary:zs rule:fold_heaps.induct)
+    using mset_tree_fold_assoc unfolding mset_tree_fold_def
+    apply (auto simp:mset_tree_fold_def mset_merge)
+    using mset_tree_fold_assoc unfolding mset_tree_fold_def
+    by (smt union_assoc)
+
+lemma mset_fold_heaps: "mset_tree (fold_heaps [] xs) = mset_tree_fold xs {#}"
+proof -
+  have "mset_tree (fold_heaps [] xs)
+        = mset_tree_fold ([]::('a,nat) tree list) (mset_tree_fold xs {#})"
+    using mset_fold_heaps_gen[of "[]" xs "{#}"] by auto
+  then show ?thesis unfolding mset_tree_fold_def by auto
+qed
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  unfolding heap_of_list_def
+
+lemma [simp]: "\<forall>x \<in> set xs \<union> set ys. heap x \<Longrightarrow> heap (fold_heaps ys xs)"
+  apply (induction ys xs rule:fold_heaps.induct)
+      apply (auto simp: heap_merge)
+  done
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+  unfolding heap_of_list_def by simp
+
+lemma [simp]: "\<forall>x\<in> set xs \<union> set ys. ltree x \<Longrightarrow> ltree (fold_heaps ys xs)"
+  apply (induction ys xs rule:fold_heaps.induct)
+      apply (auto simp: ltree_merge)
+  done
+
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"
+  unfolding heap_of_list_def by (auto simp:ltree_insert)
+
+(*<*)
+end
+(*>*)
+```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_508/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/Wauligmann_Martin_martin.wauligmann@tum.de_498/SENTMAIL	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,1 @@
+martin.wauligmann@tum.de```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Wauligmann_Martin_martin.wauligmann@tum.de_498/hw10.thy	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,85 @@
+(** Score: 10/10
+*)
+theory hw10
+imports
+    "../../../Public/Thys/Leftist_Heap"
+begin
+
+(* pass: performs a single pass over the list of heaps by merging adjacent heaps *)
+fun pass :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+"pass (x # y # hs) = merge x y # pass hs" |
+"pass hs = hs"
+
+(* lemma needed for termination proof of "construct" *)
+lemma pass_length[simp]: "length (pass hs) \<le> length hs"
+by (induction hs rule: pass.induct) auto
+
+(* construct: creates a single heap by making repeated passes over the list of heaps *)
+fun construct :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+"construct [] = Leaf" |
+"construct [h] = h" |
+"construct hs = construct (pass hs)"
+
+(* singleton: creates a singleton heap from an element *)
+fun singleton :: "'a::ord \<Rightarrow> 'a lheap" where
+"singleton x = Node 1 Leaf x Leaf"
+
+(* heap_of_list: constructs a heap from a list of elements *)
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap" where
+"heap_of_list xs = construct (map singleton xs)"
+
+
+
+(* Proofs *)
+
+(* 1. mset *)
+fun mset_tree_list :: "'a::ord lheap list \<Rightarrow> 'a multiset" where
+"mset_tree_list [] = {#}" |
+"mset_tree_list (h # hs) = mset_tree h + mset_tree_list hs"
+
+lemma mset_tree_pass: "mset_tree_list (pass hs) = mset_tree_list hs"
+by (induction hs rule: pass.induct) (auto simp add: mset_merge)
+
+lemma mset_tree_construct: "mset_tree (construct hs) = mset_tree_list hs"
+by (induction hs rule: construct.induct) (auto simp add: mset_merge mset_tree_pass)
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+by (induction xs) (auto simp add: heap_of_list_def mset_tree_construct)
+
+
+(* 2. heap *)
+fun heap_list :: "'a::linorder lheap list \<Rightarrow> bool" where
+"heap_list [] = True" |
+"heap_list (h # hs) \<longleftrightarrow> heap h \<and> heap_list hs"
+
+lemma heap_pass: "heap_list hs \<Longrightarrow> heap_list (pass hs)"
+by (induction hs rule: pass.induct) (auto simp add: heap_merge)
+
+lemma heap_construct: "heap_list hs \<Longrightarrow> heap (construct hs)"
+by (induction hs rule: construct.induct) (auto simp add: heap_merge heap_pass)
+
+lemma heap_singleton: "heap_list (map singleton xs)"
+by (induction xs) auto
+
+lemma heap_heap_of_list: "heap (heap_of_list xs)"
+by (induction xs) (auto simp add: heap_of_list_def heap_construct heap_singleton)
+
+
+(* 3. ltree *)
+fun ltree_list :: "'a::ord lheap list \<Rightarrow> bool" where
+"ltree_list [] = True" |
+"ltree_list (h # hs) \<longleftrightarrow> ltree h \<and> ltree_list hs"
+
+lemma ltree_pass: "ltree_list hs \<Longrightarrow> ltree_list (pass hs)"
+by (induction hs rule: pass.induct) (auto simp add: ltree_merge)
+
+lemma ltree_construct: "ltree_list hs \<Longrightarrow> ltree (construct hs)"
+by (induction hs rule: construct.induct) (auto simp add: ltree_merge ltree_pass)
+
+lemma ltree_singleton: "ltree_list (map singleton xs)"
+by (induction xs) auto
+
+lemma ltree_heap_of_list: "ltree (heap_of_list xs)"
+by (induction xs) (auto simp add: heap_of_list_def ltree_construct ltree_singleton)
+
+end
\ No newline at end of file```
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/10/Wauligmann_Martin_martin.wauligmann@tum.de_498/testoutput.html	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+<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/10/meta.csv	Thu Jul 13 15:33:16 2017 +0200
@@ -0,0 +1,20 @@
+"482","shuwei.hu@tum.de","Hu","Shuwei","http://vmnipkow3.in.tum.de/web/submissions/482"
+"484","f.hellauer@tum.de","Hellauer","Fabian","http://vmnipkow3.in.tum.de/web/submissions/484"
+"489","ga95luy@mytum.de","Hutzler","Matthias","http://vmnipkow3.in.tum.de/web/submissions/489"
+"492","lukas.stevens@tum.de","Stevens","Lukas","http://vmnipkow3.in.tum.de/web/submissions/492"
+"498","martin.wauligmann@tum.de","Wauligmann","Martin","http://vmnipkow3.in.tum.de/web/submissions/498"
+"508","sreeharsha.totakura@mytum.de","Totakura","Sree Harsha","http://vmnipkow3.in.tum.de/web/submissions/508"
+"510","jonas.keinholz@tum.de","Keinholz","Jonas","http://vmnipkow3.in.tum.de/web/submissions/510"
+"511","max.haslbeck@mytum.de","Haslbeck","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/511"
+"512","julian.biendarra@tum.de","Biendarra","Julian","http://vmnipkow3.in.tum.de/web/submissions/512"
+"513","markus.grosser@tum.de","Großer","Markus","http://vmnipkow3.in.tum.de/web/submissions/513"
+"514","jonas.raedle@tum.de","Rädle","Karl Jonas","http://vmnipkow3.in.tum.de/web/submissions/514"
+"515","simon.rosskopf@tum.de","Roßkopf","Simon","http://vmnipkow3.in.tum.de/web/submissions/515"
+"516","daniel.stuewe@tum.de","Stüwe","Daniel","http://vmnipkow3.in.tum.de/web/submissions/516"
+"517","antoine.saporta@tum.de","Saporta","Antoine Jacques","http://vmnipkow3.in.tum.de/web/submissions/517"
+"523","ga96vup@mytum.de","Ouyang","Lena","http://vmnipkow3.in.tum.de/web/submissions/523"
+"541","maximilian.schaeffeler@tum.de","Schäffeler","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/541"
+"542","daniel.somogyi@tum.de","Somogyi","Daniel","http://vmnipkow3.in.tum.de/web/submissions/542"
+"543","ga48kog@mytum.de","Erhard","Julian","http://vmnipkow3.in.tum.de/web/submissions/543"
+"544","friedrich.kurz@tum.de","Kurz","Friedrich","http://vmnipkow3.in.tum.de/web/submissions/544"```
```--- a/Exercises/hwsubm/email.log	Mon Jul 10 13:49:39 2017 +0200
+++ b/Exercises/hwsubm/email.log	Thu Jul 13 15:33:16 2017 +0200
@@ -757,3 +757,63 @@
Di 4. Jul 21:19:48 CEST 2017
OK
+Mo 10. Jul 15:08:16 CEST 2017
+OK
+Mo 10. Jul 15:08:18 CEST 2017
+OK
+Mo 10. Jul 15:08:18 CEST 2017
+OK
+Mo 10. Jul 15:08:18 CEST 2017
+OK
+Mo 10. Jul 15:08:18 CEST 2017
+OK
+Mo 10. Jul 15:08:18 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017
+OK
+Mo 10. Jul 15:08:19 CEST 2017