corr12 draft
authorlammich <lammich@in.tum.de>
Fri, 13 Jul 2018 20:34:42 +0200
changeset 69954 849f58791a05
parent 69953 437b4a691a03
child 69955 db5ebc272bcf
corr12
SS18/Exercises/hwsubm/hw12/Das_Sharma_Amartya_ga53qud@mytum.de_578/SENTMAIL
SS18/Exercises/hwsubm/hw12/Das_Sharma_Amartya_ga53qud@mytum.de_578/hw12_tmpl.thy
SS18/Exercises/hwsubm/hw12/Gottfriedsen_Jakob_j.gottfriedsen@tum.de_577/SENTMAIL
SS18/Exercises/hwsubm/hw12/Gottfriedsen_Jakob_j.gottfriedsen@tum.de_577/hw12.thy
SS18/Exercises/hwsubm/hw12/Griebel_Simon_s.griebel@tum.de_583/SENTMAIL
SS18/Exercises/hwsubm/hw12/Griebel_Simon_s.griebel@tum.de_583/hw12.thy
SS18/Exercises/hwsubm/hw12/Jonischkeit_Clemens_clemens.jonischkeit@tum.de_581/SENTMAIL
SS18/Exercises/hwsubm/hw12/Jonischkeit_Clemens_clemens.jonischkeit@tum.de_581/jonischkeit12.thy
SS18/Exercises/hwsubm/hw12/Kirchmeier_Maximilian_max.kirchmeier@tum.de_580/SENTMAIL
SS18/Exercises/hwsubm/hw12/Kirchmeier_Maximilian_max.kirchmeier@tum.de_580/hw12_tmpl.thy
SS18/Exercises/hwsubm/hw12/Koepke_Eric_eric.koepke@tum.de_570/SENTMAIL
SS18/Exercises/hwsubm/hw12/Koepke_Eric_eric.koepke@tum.de_570/hw12.thy
SS18/Exercises/hwsubm/hw12/Krebs_Mitja_mitja.krebs@tum.de_572/SENTMAIL
SS18/Exercises/hwsubm/hw12/Krebs_Mitja_mitja.krebs@tum.de_572/hw12_tmpl.thy
SS18/Exercises/hwsubm/hw12/Kutasi_Daniel_daniel.kutasi@mytum.de_573/SENTMAIL
SS18/Exercises/hwsubm/hw12/Kutasi_Daniel_daniel.kutasi@mytum.de_573/hw12.thy
SS18/Exercises/hwsubm/hw12/Mutius_Joshua_ga96koz@mytum.de_587/SENTMAIL
SS18/Exercises/hwsubm/hw12/Mutius_Joshua_ga96koz@mytum.de_587/hw12_tmpl.thy
SS18/Exercises/hwsubm/hw12/Putwattana_Attakorn_a.putwattana@tum.de_582/Fenwick_Trees_List.thy
SS18/Exercises/hwsubm/hw12/Putwattana_Attakorn_a.putwattana@tum.de_582/SENTMAIL
SS18/Exercises/hwsubm/hw12/Putwattana_Attakorn_a.putwattana@tum.de_582/hw12.thy
SS18/Exercises/hwsubm/hw12/Rau_Martin_martin.rau@tum.de_571/Home12.thy
SS18/Exercises/hwsubm/hw12/Rau_Martin_martin.rau@tum.de_571/SENTMAIL
SS18/Exercises/hwsubm/hw12/Rieder_Sabine_sabine.rieder@tum.de_586/SENTMAIL
SS18/Exercises/hwsubm/hw12/Rieder_Sabine_sabine.rieder@tum.de_586/hw12_tmpl.thy
SS18/Exercises/hwsubm/hw12/Smith_Nicholas_nick.smith@tum.de_584/HW12.thy
SS18/Exercises/hwsubm/hw12/Smith_Nicholas_nick.smith@tum.de_584/SENTMAIL
SS18/Exercises/hwsubm/hw12/Somasundaram_Arun_ge69kel@mytum.de_588/SENTMAIL
SS18/Exercises/hwsubm/hw12/Somasundaram_Arun_ge69kel@mytum.de_588/hw12_tmpl.thy
SS18/Exercises/hwsubm/hw12/Stamer_Florian_florian.stamer@tum.de_575/SENTMAIL
SS18/Exercises/hwsubm/hw12/Stamer_Florian_florian.stamer@tum.de_575/ex12.thy
SS18/Exercises/hwsubm/hw12/Wielander_Felix_felix.wielander@tum.de_574/SENTMAIL
SS18/Exercises/hwsubm/hw12/Wielander_Felix_felix.wielander@tum.de_574/hw12_tmpl.thy
SS18/Exercises/hwsubm/hw12/meta.csv
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Das_Sharma_Amartya_ga53qud@mytum.de_578/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+ga53qud@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Das_Sharma_Amartya_ga53qud@mytum.de_578/hw12_tmpl.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,257 @@
+(** Score: 4/5
+  wrong get_min spec. rest OK.
+*)
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q \<in> set_mset(mset q) \<Longrightarrow> \<forall>p \<in> set_mset(mset q). snd (get_min q) \<le> snd p"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation Priority_Queue "{#}" "op={#}" add_mset
+  "\<lambda>_. (undefined,0::nat)"
+  "\<lambda>m. m-{#(undefined,0)#}"
+  top id
+  apply unfold_locales by auto
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+
+
+
+
+
+fun mset_tree :: "(('d\<times>'a),'b) tree \<Rightarrow> ('d\<times>'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
+
+type_synonym ('d, 'a) lheap = "(('d\<times>'a),nat)tree"
+
+fun rank :: "('d, 'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d, 'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('d\<times>'a),'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (d,m) r) =
+  (heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). m \<le> y))"
+
+fun ltree :: "('d, '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 :: "('d, 'a) lheap \<Rightarrow> ('d\<times>'a) \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, '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 :: "('d, 'a) lheap \<Rightarrow> ('d\<times>'a::linorder)" where
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1,a1) r1 =: t1) (Node n2 l2 (d2,a2) r2 =: t2) =
+   (if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2)
+    else node l2 (d2,a2) (merge r2 t1))"
+
+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 snd a1 \<le> snd 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)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::ord) \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d,a) r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). a \<le> y)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow>  get_min h \<in> set_mset(mset_tree h) \<Longrightarrow> \<forall>(x,y) \<in> set_mset(mset_tree h). snd (get_min h) \<le> y"
+  apply(induction h)
+   apply auto
+   apply blast
+  by blast
+
+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 d1 a1 r1 n2 l2 d2 a2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (d1,a1) (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    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_aux1_aux1[simp]: "heap \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle>"
+  by(induction x)(auto)
+
+lemma heap_insert_aux1[simp]:  "heap t \<Longrightarrow> heap (merge \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle> t)"
+  apply(induction t)
+  by(auto simp add:heap_merge)
+
+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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case
+    by (metis (full_types) case_prodE get_min mset_tree.simps(1) prod.sel(2))
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Gottfriedsen_Jakob_j.gottfriedsen@tum.de_577/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+j.gottfriedsen@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Gottfriedsen_Jakob_j.gottfriedsen@tum.de_577/hw12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,213 @@
+(** Score: 5/5
+*)
+theory hw12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+
+text \<open>Priority queue interface:\<close>
+
+value "min_set"
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d \<times> 'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d \<times> 'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d \<times> 'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert (d, a) q) = mset q + {#(d, a)#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> (\<forall>x \<in># mset q. snd (get_min q) \<le> snd x) \<and> get_min q \<in># mset q"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert (d, a) q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+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 heap :: "('d \<times> 'p::linorder) lheap \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (a, p) r) =
+  (heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). p \<le> snd 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"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d \<times> 'p::linorder) lheap \<Rightarrow> ('d \<times> 'p) lheap \<Rightarrow> ('d \<times> 'p) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1, p1) r1 =: t1) (Node n2 l2 (d2, p2) r2 =: t2) =
+   (if p1 \<le> p2 then node l1 (d1, p1) (merge r1 t2)
+    else node l2 (d2, p2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 (d1, p1) r1, Node n2 l2 (d2, p2) r2) \<Rightarrow>
+    if p1 \<le> p2 then node l1 (d1, p1) (merge r1 t2) else node l2 (d2, p2) (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d \<times> 'p::linorder) \<Rightarrow> ('d \<times> 'p) lheap \<Rightarrow> ('d \<times> 'p) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d \<times> 'p::linorder) lheap \<Rightarrow> ('d \<times> 'p) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d, p) r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). p \<le> snd x)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> (\<forall>x \<in># mset_tree h. snd (get_min h) \<le> snd x) \<and> get_min h \<in># mset_tree h"
+  by (induction h) force+
+
+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 d1 p1 r1 n2 l2 d2 p2 r2)
+  then show ?case
+  proof cases
+    assume "p1 \<le> p2"
+    thus ?thesis using 3 by(simp)(auto simp: ltree_node)
+  next
+    assume "\<not> p1 \<le> p2"
+    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 (d, p) 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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case (5 q) thus ?case by (simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Griebel_Simon_s.griebel@tum.de_583/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+s.griebel@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Griebel_Simon_s.griebel@tum.de_583/hw12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,242 @@
+(** Score: 4/5
+  bad get-min spec
+*)
+theory hw12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'p::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "'d \<Rightarrow> 'p::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'p::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'p::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert d p q) = mset q + {#(d, p)#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    snd (get_min q) = Min_mset (image_mset (snd) (mset q))"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert d p q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation Priority_Queue "{#}" "op={#}" "curry add_mset"
+  "\<lambda>m. (undefined,Min_mset (image_mset (snd) m))"
+  "\<lambda>m. m-{#(undefined,Min_mset (image_mset (snd) m))#}"
+  top id
+  apply unfold_locales by auto
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+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 ('d, 'p) lheap = "(('d \<times> 'p) ,nat)tree"
+
+fun rank :: "('d,'p::linorder) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d,'p::linorder) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('d \<times> 'p::linorder),'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). (snd m) \<le> (snd x)))"
+
+fun ltree :: "('d,'p::linorder) 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 :: "('d,'p::linorder) lheap \<Rightarrow> ('d \<times> 'p::linorder) \<Rightarrow> ('d,'p::linorder) lheap \<Rightarrow> ('d,'p::linorder) 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 :: "('d,'p::linorder) lheap \<Rightarrow> ('d \<times>'p::linorder)" where
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d,'p::linorder) lheap \<Rightarrow> ('d,'p::linorder) lheap \<Rightarrow> ('d,'p::linorder) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
+   (if snd a1 \<le> snd a2 then node l1 a1 (merge r1 t2)
+    else node l2 a2 (merge r2 t1))"
+
+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 snd a1 \<le> snd 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)
+
+hide_const (open) insert
+
+definition insert :: "'d \<Rightarrow> 'p::linorder \<Rightarrow> ('d,'p::linorder) lheap \<Rightarrow> ('d,'p::linorder) lheap" where
+"insert d p t = merge (Node 1 Leaf (d, p) Leaf) t"
+
+fun del_min :: "('d,'p::linorder) lheap \<Rightarrow> ('d,'p::linorder) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+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). snd a \<le> snd x)"
+by(auto simp add: node_def)
+
+
+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 d p t) = mset_tree t + {#(d, p)#}"
+by (auto simp add: insert_def mset_merge)
+
+lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> snd (get_min h) = Min (snd ` (set_mset (mset_tree h)))"
+by (induction h) (auto simp add: eq_Min_iff)
+
+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 "snd a1 \<le> snd 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))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `snd a1 \<le> snd a2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> snd a1 \<le> snd 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 d p t)"
+by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)
+
+lemma heap_insert: "heap t \<Longrightarrow> heap(insert d p 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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case by(simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Jonischkeit_Clemens_clemens.jonischkeit@tum.de_581/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+clemens.jonischkeit@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Jonischkeit_Clemens_clemens.jonischkeit@tum.de_581/jonischkeit12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,240 @@
+(** Score: 5/5
+*)
+theory jonischkeit12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> let (v,p) = get_min q in
+ (v,p) \<in> set_mset (mset q) \<and> (\<forall> (_,x) \<in> set_mset (mset q). p \<le> x)"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+
+
+
+
+
+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,'b) lheap = "('a\<times>'b,nat)tree"
+
+fun rank :: "('a,'b) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('a,'b) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun heap2 :: "(('a \<times> 'b::linorder), 'c) tree \<Rightarrow> bool" where
+"heap2 Leaf = True" |
+"heap2 (Node _ l (_,p) r) =
+  (heap2 l \<and> heap2 r \<and> (\<forall>(_,x) \<in> set_mset(mset_tree l + mset_tree r). p \<le> x))"
+
+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,'b) 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,'b) lheap \<Rightarrow> 'a\<times>'b \<Rightarrow> ('a,'b) lheap \<Rightarrow> ('a,'b) 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,'b) lheap \<Rightarrow> 'a\<times>'b" where
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('a,'b::ord) lheap \<Rightarrow> ('a,'b) lheap \<Rightarrow> ('a,'b) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (v1,p1) r1 =: t1) (Node n2 l2 (v2,p2) r2 =: t2) =
+   (if p1 \<le> p2 then node l1 (v1,p1) (merge r1 t2)
+    else node l2 (v2,p2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 (v1,p1) r1, Node n2 l2 (v2,p2) r2) \<Rightarrow>
+    if p1 \<le> p2 then node l1 (v1,p1) (merge r1 t2) else node l2 (v2,p2) (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('a\<times>'b::ord) \<Rightarrow> ('a,'b) lheap \<Rightarrow> ('a,'b) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('a,'b::ord) lheap \<Rightarrow> ('a,'b) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap2 (node l (v,p) r) \<longleftrightarrow>
+  heap2 l \<and> heap2 r \<and> (\<forall>(_,x) \<in> set_mset(mset_tree l + mset_tree r). p \<le> x)"
+by(auto simp add: node_def)
+
+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 get_min: "\<lbrakk> heap2 h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> let (v,p) = get_min h in
+ (v,p) \<in> set_mset (mset_tree h) \<and> (\<forall> (_,x) \<in> set_mset (mset_tree h). p \<le> x)"
+  apply (induction h)
+ apply (auto split: prod.splits)
+ apply (blast+)
+  done
+
+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 v1 p1 r1 n2 l2 v2 p2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "p1 \<le> p2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (v1, p1) (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `p1 \<le> p2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> p1 \<le> p2"
+    thus ?thesis using 3 by(simp)(auto simp: ltree_node)
+  qed
+qed simp_all
+
+lemma heap_merge: "\<lbrakk> heap2 l; heap2 r \<rbrakk> \<Longrightarrow> heap2 (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: "heap2 t \<Longrightarrow> heap2(insert x t)"
+by (smt empty_iff heap2.elims(3) heap_merge jonischkeit12.insert_def merge.simps(1) mset_merge mset_tree.simps(1) set_mset_eq_empty_iff tree.distinct(1) tree.inject)
+
+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: "heap2 t \<Longrightarrow> heap2(del_min t)"
+by(cases t)(auto simp add: heap_merge simp del: merge.simps)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap2 h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case (5 q) thus ?case using mset_tree_empty "5" get_min by blast
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Kirchmeier_Maximilian_max.kirchmeier@tum.de_580/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+max.kirchmeier@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Kirchmeier_Maximilian_max.kirchmeier@tum.de_580/hw12_tmpl.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,339 @@
+(** Score: 5/5
+
+  Specs might have been simpler with
+    get_min :: q \<Rightarrow> d\<times>'a
+
+*)
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+fun getprio :: "('d\<times>'p::linorder) \<Rightarrow> 'p" where
+  "getprio (d,p) = p"
+
+definition prio_set_mset :: "('d\<times>'p::linorder) multiset \<Rightarrow> 'p set" where
+  "prio_set_mset ms = {p | d p. (d,p) \<in> set_mset ms}"
+
+fun minprio :: "('d\<times>'p::linorder) multiset \<Rightarrow> 'p" where
+  "minprio ms = Min (prio_set_mset ms)"
+
+fun minprio_set :: "('d\<times>'p::linorder) multiset \<Rightarrow> 'd set" where
+  "minprio_set ms = {d | d . (d, minprio ms) \<in> set_mset ms}"
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "'d \<Rightarrow> 'p::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> 'd"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'p::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert d p q) = mset q + {#(d,p)#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# (get_min q, minprio (mset q)) #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q \<in> minprio_set (mset q)"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert d p q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+
+
+
+
+
+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 ('d,'p) lheap = "('d\<times>'p,nat)tree"
+
+fun rank :: "('d,'p) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d,'p) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+fun prio_set :: "('d,'p::linorder) lheap \<Rightarrow> 'p set" where
+  "prio_set Leaf = {}"
+| "prio_set (Node n l (d,p) r) = Set.insert p (prio_set l \<union> prio_set r)"
+
+text{* The invariants: *}
+
+fun heap :: "('d\<times>'p::linorder,nat)tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (d,p) r) =
+  (heap l \<and> heap r \<and> (\<forall>(d2,p2) \<in> set_mset (mset_tree l + mset_tree r). p \<le> p2))"
+
+fun ltree :: "('d,'p) 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 :: "('d,'p) lheap \<Rightarrow> ('d\<times>'p) \<Rightarrow> ('d,'p) lheap \<Rightarrow> ('d,'p) 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 :: "('d,'p) lheap \<Rightarrow> 'd" where
+"get_min (Node n l (d,p) r) = d"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d,'p::linorder) lheap \<Rightarrow> ('d,'p) lheap \<Rightarrow> ('d,'p) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1,p1) r1 =: t1) (Node n2 l2 (d2,p2) r2 =: t2) =
+   (if p1 \<le> p2 then node l1 (d1,p1) (merge r1 t2)
+    else node l2 (d2,p2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 (d1,p1) r1, Node n2 l2 (d2,p2) r2) \<Rightarrow>
+    (if p1 \<le> p2 then node l1 (d1,p1) (merge r1 t2)
+    else node l2 (d2,p2) (merge r2 t1)))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "'d \<Rightarrow> 'p::linorder \<Rightarrow> ('d,'p) lheap \<Rightarrow> ('d,'p) lheap" where
+"insert d p t = merge (Node 1 Leaf (d,p) Leaf) t"
+
+fun del_min :: "('d,'p::linorder) lheap \<Rightarrow> ('d,'p) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma prio_set_mset: "prio_set t = prio_set_mset (mset_tree t)" unfolding prio_set_mset_def
+  by (induction t) auto
+
+lemma prio_set_mset_empty[simp]: "prio_set_mset {#} = {}"
+  unfolding prio_set_mset_def by auto
+lemma prio_set_mset_sin[simp]: "prio_set_mset {#(d,p)#} = {p}"
+  unfolding prio_set_mset_def by auto
+lemma prio_set_mset_ins[simp]: "prio_set_mset (add_mset (d,p) ms) = prio_set_mset ms \<union> {p}"
+  unfolding prio_set_mset_def by auto
+lemma prio_set_finite[simp]: "finite (prio_set_mset ms)"
+  by (induction ms) auto
+
+lemma prio_set_step: "\<forall>p2 \<in> prio_set_mset ms. p \<le> p2 \<Longrightarrow>
+  Min (prio_set_mset (add_mset (d, p) ms)) = p"
+  by (auto simp add: Min_insert2)
+
+lemma prio_set_un: "\<forall>(d,p2)\<in>set_mset ms. p \<le> p2 \<Longrightarrow>
+          p2 \<in> prio_set_mset ms \<Longrightarrow> p \<le> p2"
+  using prio_set_mset_def by fastforce
+
+lemma minprio: "heap (Node n l (d,p) r) \<Longrightarrow> minprio (mset_tree (Node n l (d,p) r)) = p"
+proof -
+  let ?node = "Node n l (d,p) r"
+  let ?rest_mset = "mset_tree l + mset_tree r"
+  let ?rest_set = "set_mset ?rest_mset"
+
+  have fin: "finite ?rest_set"
+    by simp
+
+  assume "heap ?node"
+
+  then have "\<forall>(d,p2) \<in> set_mset (mset_tree l) \<union> set_mset (mset_tree r). p \<le> p2"
+    by auto
+
+  then have "\<forall>(d,p2) \<in> ?rest_set. p \<le> p2"
+    by auto
+
+  then have p: "\<forall>p2\<in>prio_set_mset (mset_tree l + mset_tree r). p \<le> p2" using prio_set_un
+    by blast
+
+  then show "minprio (mset_tree (Node n l (d,p) r)) = p"
+  proof (cases "?rest_mset = {#}")
+    case True
+    then show ?thesis by auto
+  next
+    case False
+    then show ?thesis using prio_set_step[of ?rest_mset p] p
+      by simp
+  qed
+qed
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d,p) r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>(d2,p2) \<in> set_mset (mset_tree l + mset_tree r). p \<le> p2)"
+  by (auto simp add: node_def sup_commute)
+
+
+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 d p t) = mset_tree t + {#(d,p)#}"
+  by (auto simp add: insert_def mset_merge)
+
+lemma mset_del: "mset_tree (Node n l a r) = ms \<Longrightarrow> mset_tree (merge l r) = ms - {#a#}"
+  using mset_merge by fastforce
+
+lemma min_elem: "heap (Node n l (d,p) r) \<Longrightarrow>
+  d \<in> minprio_set (mset_tree (Node n l (d,p) r)) \<and> p = minprio (mset_tree (Node n l (d,p) r))"
+proof -
+  let ?node = "Node n l (d,p) r"
+  assume "heap ?node"
+  then have p: "p = minprio (mset_tree ?node)" using minprio by force
+
+  then have "d \<in> minprio_set (mset_tree ?node)"
+    by auto
+
+  then show "d \<in> minprio_set (mset_tree (Node n l (d,p) r)) \<and> p = minprio (mset_tree (Node n l (d,p) r))"
+    using p by auto
+qed
+
+lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h \<in> minprio_set (mset_tree h)"
+  using min_elem
+  by (smt get_min.elims)
+
+lemma mset_del_min: "\<lbrakk> heap h \<rbrakk> \<Longrightarrow>
+  mset_tree (del_min h) = mset_tree h - {# (get_min h, minprio (mset_tree h)) #}"
+proof (cases h)
+  case Leaf
+  then show ?thesis by auto
+next
+  case (Node n l a r)
+
+  obtain d p where a: "(d,p) = a"
+    by (metis getprio.cases)
+
+  let ?node = "Node n l (d,p) r"
+
+  assume "heap h"
+  then have "p = minprio (mset_tree ?node)" using min_elem[of n l d p r] using Node a by auto
+
+  then show ?thesis using Node a mset_del by fastforce
+qed
+
+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 d1 p1 r1 n2 l2 d2 p2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "p1 \<le> p2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (d1,p1) (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `p1 \<le> p2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> p1 \<le> p2"
+    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 d p t)"
+by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)
+
+lemma heap_insert: "heap t \<Longrightarrow> heap(insert d p 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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 thus ?case by(simp add: mset_del_min)
+next
+  case 5 thus ?case
+    using get_min mset_tree_empty by auto
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Koepke_Eric_eric.koepke@tum.de_570/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+eric.koepke@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Koepke_Eric_eric.koepke@tum.de_570/hw12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,256 @@
+(** Score: 4/5
+  bad spec of get-min
+*)
+theory hw12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> \<forall>x\<in>set_mset (mset q). snd (get_min q) \<le> snd x"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation foo: Priority_Queue "{#}" "op={#}" add_mset
+  "\<lambda>_. (undefined,0::nat)"
+  "\<lambda>m. m-{#(undefined,0)#}"
+  top id
+  apply unfold_locales by auto
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+value "let s = {#3::nat, 3#} in Min_mset s"
+
+lemma "Min_mset (mset (e#l)) = fold min l e"
+  using Min.set_eq_fold by auto
+
+value "min (3::nat) "
+
+
+
+
+
+
+
+
+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 :: "(('d\<times>'a),'c) 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). snd m \<le> snd 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 :: "('d\<times>'a) lheap \<Rightarrow> ('d\<times>'a)" where
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d\<times>'a::ord) lheap \<Rightarrow> ('d\<times>'a) lheap \<Rightarrow> ('d\<times>'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
+   (if snd a1 \<le>  snd a2 then node l1 a1 (merge r1 t2)
+    else node l2 a2 (merge r2 t1))"
+
+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 snd a1 \<le>  snd 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)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::ord) \<Rightarrow> ('d\<times>'a) lheap \<Rightarrow> ('d\<times>'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d\<times>'a::ord) lheap \<Rightarrow> ('d\<times>'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+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). snd a \<le> snd x)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow>  \<forall>x\<in>set_mset (mset_tree h). snd (get_min h) \<le> snd x"
+  apply (induction h)
+  apply (auto simp add: eq_Min_iff)
+  done
+
+
+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 "snd a1 \<le> snd 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))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `snd a1 \<le> snd a2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> snd a1 \<le> snd 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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case by(simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Krebs_Mitja_mitja.krebs@tum.de_572/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+mitja.krebs@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Krebs_Mitja_mitja.krebs@tum.de_572/hw12_tmpl.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,237 @@
+(** Score: 5/5
+
+  get_min q = dp \<longrightarrow> \<dots>
+
+    just writing get_min q twice would be more readable!
+    or \<open>let dp=get_min q in \<dots>\<close>
+
+*)
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+(* and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)" *)
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> (get_min q = dp \<longrightarrow> (dp \<in># mset q \<and> (\<forall>x \<in># mset q. snd dp \<le> snd x)))"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+fun mset_tree :: "('d\<times>'a,'b) tree \<Rightarrow> ('d\<times>'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l dp r) = {#dp#} + mset_tree l + mset_tree r"
+
+type_synonym ('d,'a) lheap = "('d\<times>'a,nat) tree"
+
+fun rank :: "('d,'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d,'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "('d\<times>'a,'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l dp r) =
+  (heap l \<and> heap r \<and> (\<forall>x \<in># (mset_tree l + mset_tree r). snd dp \<le> snd x))"
+
+fun ltree :: "('d,'a) lheap \<Rightarrow> bool" where
+"ltree Leaf = True" |
+"ltree (Node n l dp r) =
+ (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
+
+definition node :: "('d,'a) lheap \<Rightarrow> ('d\<times>'a) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"node l dp r =
+ (let rl = rk l; rr = rk r
+  in if rl \<ge> rr then Node (rr+1) l dp r else Node (rl+1) r dp l)"
+
+fun get_min :: "('d,'a) lheap \<Rightarrow> ('d\<times>'a)" where
+"get_min (Node n l dp r) = dp"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d,'a::linorder) lheap \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 dp1 r1 =: t1) (Node n2 l2 dp2 r2 =: t2) =
+   (if snd dp1 \<le> snd dp2 then node l1 dp1 (merge r1 t2)
+    else node l2 dp2 (merge r2 t1))"
+
+lemma merge_node: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 dp1 r1, Node n2 l2 dp2 r2) \<Rightarrow>
+    if snd dp1 \<le> snd dp2 then node l1 dp1 (merge r1 t2) else node l2 dp2 (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::linorder) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"insert dp t = merge (Node 1 Leaf dp Leaf) t"
+
+fun del_min :: "('d,'a::linorder) lheap \<Rightarrow> ('d,'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l dp r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
+by(cases t) auto
+
+lemma ltree_node: "ltree (node l dp r) \<longleftrightarrow> ltree l \<and> ltree r"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l dp r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). snd dp \<le> snd x)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> (get_min h = dp \<longrightarrow> (dp \<in># mset_tree h \<and> (\<forall>x \<in># mset_tree h. snd dp \<le> snd x)))"
+by (induction h) (auto (* simp add: eq_Min_iff *))
+
+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 dp1 r1 n2 l2 dp2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "snd dp1 \<le> snd dp2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 dp1 (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `snd dp1 \<le> snd dp2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> snd dp1 \<le> snd dp2"
+    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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case
+    apply (simp add: get_min mset_tree_empty)
+    using get_min apply blast
+    done
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Kutasi_Daniel_daniel.kutasi@mytum.de_573/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+daniel.kutasi@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Kutasi_Daniel_daniel.kutasi@mytum.de_573/hw12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,245 @@
+(** Score: 4/5
+  bad spec of get-min
+*)
+theory hw12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#}
+       \<Longrightarrow> get_min q \<in> set_mset (mset q) \<Longrightarrow> \<forall>x \<in> set_mset (mset q). snd (get_min q) \<le> snd x"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation foo: Priority_Queue "{#}" "op={#}" add_mset
+  "\<lambda>_. (undefined,0::nat)"
+  "\<lambda>m. m-{#(undefined,0)#}"
+  top id
+  apply unfold_locales by auto
+
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+fun mset_tree :: "(('d\<times>'a),'b) tree \<Rightarrow> ('d\<times>'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
+
+type_synonym ('d,'a) lheap = "(('d\<times>'a),nat)tree"
+
+fun rank :: "('d,'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d,'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('d\<times>'a),'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (d,a) r) =
+  (heap l \<and> heap r \<and> (\<forall>(d',a') \<in> set_mset(mset_tree l + mset_tree r). a \<le> a'))"
+
+fun ltree :: "('d,'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 :: "('d,'a) lheap \<Rightarrow> ('d\<times>'a) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'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 :: "('d,'a) lheap \<Rightarrow> ('d\<times>'a)" where
+"get_min Leaf = undefined" |
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d,'a::ord) lheap \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1,a1) r1 =: t1) (Node n2 l2 (d2,a2) r2 =: t2) =
+   (if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2)
+    else node l2 (d2,a2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 (d1,a1) r1, Node n2 l2 (d2,a2) r2) \<Rightarrow>
+    if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2) else node l2 (d2,a2) (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::ord) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d,'a::ord) lheap \<Rightarrow> ('d,'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d,a) r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>(d',a') \<in> set_mset(mset_tree l + mset_tree r). a \<le> a')"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h \<in> set_mset (mset_tree h)
+ \<Longrightarrow> \<forall>x \<in> set_mset (mset_tree h). snd (get_min h) \<le> snd x"
+  apply (induction h)
+  apply auto
+  by blast+
+
+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 d1 a1 r1 n2 l2 d2 a2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (d1, a1) (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    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_leaves: "heap \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle>"
+by (induction x) (auto)
+
+lemma heap_insert_leaves: "heap t \<Longrightarrow> heap (merge \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle> t)"
+by (simp add: heap_leaves heap_merge)
+
+lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
+by (simp add: insert_def heap_insert_leaves 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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case by(simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Mutius_Joshua_ga96koz@mytum.de_587/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+ga96koz@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Mutius_Joshua_ga96koz@mytum.de_587/hw12_tmpl.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,259 @@
+(** Score: 4/5
+  bad get-min spec!
+*)
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "'d *'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> 'd * 'a"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d * 'a) multiset"
+and prio :: "('d \<times> 'a::linorder) \<Rightarrow> 'a::linorder"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min_is_min :"invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> (\<forall> m \<in># (mset q). prio (get_min q) \<le> prio m)"
+and mset_get_min_isin: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> (get_min q) \<in># (mset q)"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+(** Not a good idea to fix a prio-function, without any constraints!
+  you probably meant prio \<equiv> snd!
+
+  Anyway, in your locale, I am allowed to insert any prio function I like (e.g. \<lambda>_. 0),
+  which allows quite funny specifications for get_min. Below, I'm using a list for implementation,
+  and always return the first element of the list, without caring about priorities at all!
+*)
+
+interpretation foo: Priority_Queue "[]" "op=[]" Cons
+  "hd"
+  "tl"
+  top mset
+  "\<lambda>_. (0::nat)"
+  apply unfold_locales by (auto simp: neq_Nil_conv)
+
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+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 ('d,'a) lheap = "(('d \<times> 'a),nat) tree"
+
+fun rank :: "('d,'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d,'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+definition  prio ::"('d \<times> 'a) \<Rightarrow> 'a" where
+"prio \<equiv> snd"
+
+fun (in linorder) heap :: "(('d \<times> '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). prio m \<le> prio x))"
+
+fun ltree :: "('d,'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 :: "('d,'a) lheap \<Rightarrow> 'd \<times> 'a \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, '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 :: "('d, 'a) lheap \<Rightarrow> 'd \<times> 'a" where
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
+   (if prio a1 \<le> prio a2 then node l1 a1 (merge r1 t2)
+    else node l2 a2 (merge r2 t1))"
+
+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 prio a1 \<le> prio 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)
+
+hide_const (open) insert
+
+definition insert :: "'d \<times> 'a::ord \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+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). prio a \<le> prio x)"
+by(auto simp add: node_def)
+
+
+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_get_min_is_min :"\<lbrakk> heap h; h \<noteq> Leaf \<rbrakk> \<Longrightarrow> (\<forall> m \<in># (mset_tree h). prio (get_min h) \<le> prio m)"
+  by (cases h) (auto)
+lemma mset_get_min_isin: "\<lbrakk> heap h; h \<noteq> Leaf \<rbrakk> \<Longrightarrow> (get_min h) \<in># (mset_tree h)"
+  by (cases h) (auto)
+
+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 "prio a1 \<le> prio 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))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `prio a1 \<le> prio a2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> prio a1 \<le> prio 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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+and prio = prio
+proof(standard, goal_cases)
+ case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case (5 q)
+  then show ?case
+    by (simp add: mset_get_min_is_min mset_tree_empty)
+next
+  case (6 q)
+  then show ?case
+    by (simp add: mset_get_min_isin mset_tree_empty)
+next
+  case 7
+  then show ?case
+    by simp
+next
+case (8 q x)
+then show ?case
+  by (simp add: heap_insert ltree_insert)
+next
+case (9 q)
+then show ?case
+  by (simp add: heap_del_min ltree_del_min)
+next
+case (10 q1 q2)
+  then show ?case
+    using mset_merge by blast
+next
+case (11 q1 q2)
+then show ?case
+  by (simp add: heap_merge ltree_merge)
+qed
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Putwattana_Attakorn_a.putwattana@tum.de_582/Fenwick_Trees_List.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,254 @@
+(*
+  Author: Attakorn Putwattana
+*)
+
+theory Fenwick_Trees_List
+
+imports
+  Main
+  Orderings
+begin
+
+section {* Fenwick Tree *}
+text {*
+  This theory implemented Fenwick tree (https://en.wikipedia.org/wiki/Fenwick_tree)
+  using list and proves some of its properties.  Fenwick tree is used to implement
+  cumulative frequency tables.  Note that this implementation ignores the frequency 
+  of index 0, e.g., consider only frequency of indexes between 1 and n.
+*}
+subsection {* Implementation *}
+
+type_synonym ftree = "nat list"
+
+text {* 
+  Calculate the value of the least significant bit (except for 0)
+*}
+
+fun lsone :: "nat \<Rightarrow> nat" where
+  "lsone 0 = 1"
+| "lsone n = (
+  if n mod 2 = 1 then 1
+  else 2 * lsone (n div 2)
+  )"
+
+text {* 
+  Build the tree for computing cumulative frequency of range between 1 and n 
+  (ignoring index 0).
+*}
+fun build :: "nat \<Rightarrow> ftree" where
+  "build 0 = []"
+| "build (Suc n) = 0#build n"
+
+text{*
+  This lemma is required for proving termination of increase/decrease function
+*}
+lemma lsone_gt_zero[simp]: "lsone n > 0"
+  by (induction n rule: lsone.induct) auto
+
+text {* Increase the frequency of key n by x*}
+function increase :: "ftree \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ftree" where
+  "increase t n x = (
+    if n < length t then increase (t[n:=t!n + x]) (n + lsone n) x
+    else t
+  )"
+  by auto
+termination 
+  by (relation "measure (\<lambda>(t,n,x). length t - n)"; auto simp: diff_less_mono2)
+
+function decrease :: "ftree \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ftree" where
+  "decrease t n x = (
+    if n < length t then decrease (t[n:=t!n - x]) (n + lsone n) x
+    else t
+  )"
+  by auto
+termination 
+  by (relation "measure (\<lambda>(t,n,x). length t - n)"; auto simp: diff_less_mono2)
+
+text {* Request cumulative frequency of between 0 and n *}
+fun request :: "ftree \<Rightarrow> nat \<Rightarrow> nat" where
+  "request t n = (
+    if n \<ge> length t then 0
+    else if n = 0 then 0
+    else t!n + request t (n - lsone n)
+  )"
+
+text {* Request cumulative frequency of between a and b *}
+definition request_range :: "ftree \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "request_range t a b = request t b - request t (a - 1)"
+
+text {* 
+  Function to check that the given list is a Fenwick tree, e.g.,
+  the frequency list derived from it is monotonic.
+*}
+definition is_ftree :: "nat list \<Rightarrow> bool" where
+  "is_ftree t \<equiv> \<forall>n<length t. \<forall>i<n. request t i \<le> request t n"
+
+subsection {* Functional Correctness *}
+text {*
+  Function build creates a list of zero which is a correct Fenwick tree
+*}
+(* auxiliary lemma  *)
+lemma set_elm_build: "\<forall>x\<in>set (build n). x = 0"
+  by (induction n) auto
+
+lemma elm_build: "t = build n \<Longrightarrow> i < length t \<Longrightarrow> t!i = 0"
+  using set_elm_build nth_mem by auto
+
+lemma rqt_build: "t = build n \<Longrightarrow> request t i = 0"
+  apply (induction t i rule: request.induct)
+  by (simp add: elm_build)
+(* end *)
+lemma build_ftree: "t = build n \<Longrightarrow> is_ftree t"
+  unfolding is_ftree_def
+  by (metis rqt_build eq_refl)
+
+text {*
+  Request frequency of n-th element of tree of length larger than n+1
+*}
+lemma rqt_longer_lst: "i \<ge> n \<Longrightarrow> request (take (n + 1) t) n = request (take (i + 1) t) n"
+proof (induction t n arbitrary: i rule: request.induct)
+  case (1 t n)
+  then show ?case
+  proof (cases)
+    assume "n \<ge> length t"
+    then show ?thesis
+      by auto
+  next
+    assume "\<not> n \<ge> length t"
+    then show ?thesis
+    proof (cases)
+      assume "n = 0"
+      then show ?thesis
+        by (smt "1.prems" Suc_eq_plus1 add_le_same_cancel2 le_SucE le_add2 le_antisym le_imp_less_Suc le_numeral_extra(1) length_take min_le_iff_disj not_one_le_zero nth_take request.elims)
+    next
+      assume "\<not> n = 0"
+      then show ?thesis
+        (* take about 10 seconds *)
+        by (smt "1.IH" "1.prems" Suc_eq_plus1 diff_le_self le_add_diff_inverse le_imp_less_Suc length_take min_le_iff_disj not_less nth_take request.elims trans_le_add1)
+    qed
+  qed
+qed
+
+text {*
+  Request frequency of n-th element uses only first n+1 element of tree
+*}
+lemma rqt_nth_first_n_plus_one: "request t n = request (take (n + 1) t) n"
+  apply (induction t n rule: request.induct)
+  using diff_le_self min_le_iff_disj rqt_longer_lst by auto
+
+text {*
+  Increase/decrease does not change first n element in the tree 
+  (the n-th element is at (n+1)th element of the list)
+*}
+lemma inc_elm_bf_n: "i < n \<Longrightarrow> (increase t n x)!i = t!i"
+  by (induction t n x rule: increase.induct) auto
+
+lemma dec_elm_bf_n: "i < n \<Longrightarrow> (decrease t n x)!i = t!i"
+  by (induction t n x rule: decrease.induct) auto
+
+lemma inc_prefix: "i \<le> n \<Longrightarrow> take i (increase t n x) = take i t"
+  apply (induction t n x rule: increase.induct)
+  by (metis increase.elims take_update_cancel trans_le_add1)
+
+lemma dec_prefix: "i \<le> n \<Longrightarrow> take i (decrease t n x) = take i t"
+  apply (induction t n x rule: decrease.induct)
+  by (metis decrease.elims take_update_cancel trans_le_add1)
+
+(* minor fact *)
+lemma plus_lsone: "n > 0 \<Longrightarrow> even (n + lsone n)"
+  by (metis Suc_pred dvdI lsone.simps(2) odd_add odd_iff_mod_2_eq_one one_mod_two_eq_one)
+  
+lemma rqt_freq_mono: "is_ftree t \<Longrightarrow> n < length t \<Longrightarrow> request t n \<ge> request t (n - lsone n)"
+  by (cases t)  auto
+
+lemma rqt_adj: "is_ftree t \<Longrightarrow> \<forall>n<length t. request t (n - 1) \<le> request t n"
+  by (metis (no_types) diff_le_self dual_order.order_iff_strict is_ftree_def)
+(* end *)
+
+text{*
+  Increase preserves Fenwick tree's properties:
+    - Length
+    - Fenwick tree invariance
+*}
+lemma inc_length: "length t = length (increase t n x)"
+  by (induction t n x rule: increase.induct) auto
+
+lemma rqt_update_elm_lt_n: "n < length t \<Longrightarrow> i < n \<Longrightarrow> t' = (increase t n x) \<Longrightarrow>
+  request t' i = request t i"
+  apply (induction t n x arbitrary: i rule: increase.induct)
+  by (metis Suc_eq_plus1 Suc_leI inc_prefix rqt_nth_first_n_plus_one)
+
+text {* 
+  This lemma shows that for i such that n < i < n + lsone n, i - lsone i = n.
+  It will be used to show that request the frequency of i require to access n-th element 
+  of the tree.
+*}
+lemma btw_lsone: "i > n \<Longrightarrow> i < n + lsone n \<Longrightarrow> i - lsone i = n"
+  sorry
+
+lemma rqt_update_elm_gt_n: "n < length t \<Longrightarrow> n > 0 \<Longrightarrow> i \<ge> n \<Longrightarrow> i < length (increase t n x) \<Longrightarrow>
+  request (increase t n x) i = request t i + x"
+proof (induction t n x arbitrary: i rule: increase.induct)
+  case (1 t n x)
+  then show ?case
+  proof (cases)
+    assume "i \<ge> n + lsone n"
+    then have "request (increase t n x) i = request (t[n := t ! n + x]) i + x"
+      by (smt "1.IH" "1.prems" increase.simps le_add1 le_less_trans less_le_trans)
+    also have "... = request t i + x" (* request for frequency of i will skip n-th element on the tree *)
+      sorry
+    then show ?thesis
+      using calculation by linarith
+  next
+    assume "\<not> i \<ge> n + lsone n"
+    then have "request (increase t n x) i = (increase t n x)!i + request (increase t n x) (i - lsone i)"
+      using "1.prems" by auto
+    also have b0:"... = (t[n := t ! n + x])!i + request (increase t n x) (i - lsone i)"
+      by (metis "1.prems"(1) \<open>\<not> n + lsone n \<le> i\<close> inc_elm_bf_n increase.simps not_le_imp_less)
+    then show ?thesis
+    proof (cases)
+      assume "i = n"
+      then have "(t[n := t ! n + x])!i = t!i + x"
+        by (simp add: "1.prems"(1))
+      then have "request (increase t n x) (i - lsone i) = request t (n - lsone n)"
+        using "1.prems"(1) \<open>i = n\<close> rqt_update_elm_lt_n by auto
+      then show ?thesis
+        using "1.prems"(1) "1.prems"(2) \<open>i = n\<close> b0 calculation le_zero_eq by auto
+    next
+      assume "\<not> i = n"
+      then have "(t[n := t ! n + x])!i = t!i"
+        using b0 by auto
+      then have "request (increase t n x) (i - lsone i) = request (increase t n x) n"
+        by (metis "1.prems"(3) \<open>\<not> n + lsone n \<le> i\<close> \<open>i \<noteq> n\<close> btw_lsone eq_imp_le le_neq_implies_less less_imp_le_nat linorder_neqE_nat)
+      also have "... = request t n + x"
+        by (smt "1.prems"(1) "1.prems"(2) add.assoc add.commute diff_less inc_elm_bf_n inc_length increase.simps leD less_add_same_cancel1 lsone_gt_zero nth_list_update_eq order.strict_iff_order request.simps rqt_update_elm_lt_n)
+      then show ?thesis
+        by (smt "1.prems" \<open>\<not> n + lsone n \<le> i\<close> \<open>t[n := t ! n + x] ! i = t ! i\<close> ab_semigroup_add_class.add_ac(1) b0 btw_lsone dual_order.order_iff_strict inc_length leD not_le_imp_less ord_eq_le_trans request.simps)
+    qed
+  qed
+qed
+
+lemma inc_inv: "n < length t \<Longrightarrow> n > 0  \<Longrightarrow> is_ftree t \<Longrightarrow> is_ftree (increase t n x)"
+  by (smt add_le_mono1 inc_length is_ftree_def less_trans not_le rqt_update_elm_gt_n rqt_update_elm_lt_n trans_le_add1)
+text{*
+  Dncrease preserves Fenwick tree's properties:
+    - Length
+    - Fenwick tree invariance
+*}
+lemma dec_length: "length t = length (decrease t n x)"
+  by (induction t n x rule: decrease.induct) auto
+
+lemma decrease_inv: "is_ftree t \<Longrightarrow> request_range t n n \<ge> x \<Longrightarrow> is_ftree (decrease t n x)"
+  oops
+
+(* testcases *)
+definition tt :: "nat list" where
+  "tt = [0, 0, 6, 0, 7, 2, 5, 2, 15, 0]"
+
+value "is_ftree [0, 0, 1, 0, 2, 2, 5, 2, 10, 0]"
+value "is_ftree (increase [0, 0, 1, 0, 2, 2, 5, 2, 10, 0] 2 5)"
+value "request [0, 0, 1, 0, 2, 2, 5, 2, 10, 0] 7"
+value "request_range [0, 0, 1, 0, 2, 2, 5, 2, 10, 0] 3 6"
+(* end *)
+
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Putwattana_Attakorn_a.putwattana@tum.de_582/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+a.putwattana@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Putwattana_Attakorn_a.putwattana@tum.de_582/hw12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,238 @@
+(** Score: 3/5
+  severe errors in spec! tree structure seems to be OK.
+*)
+theory hw12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "'d\<times>'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d \<times> 'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d \<times> 'a::linorder) multiset" (* *** *)
+and Min_mset :: "('d \<times> 'a::linorder) multiset \<Rightarrow> ('d \<times> 'a)"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+(**
+  It makes no sense to fix Min_mset in the locale without any constraints!
+
+  I could simply implement Min_mset=get_min, and thus trivially get rid of
+  the mset_get_min condition, allowing me to return arbitrary elements!
+
+  Note that Min_mset on pairs is not even a well-defined function: There may
+  be multiple unequal minimal elements, e.g. (x,0) and (y,0)!
+*)
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+fun less :: "'d\<times>'a::linorder \<Rightarrow> 'd\<times>'a \<Rightarrow> bool" where
+  "less (d1,a1) (d2,a2) = (a1 < a2)"
+
+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 ('d,'a) lheap = "('d\<times>'a,nat)tree"
+
+fun rank :: "('d,'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d,'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "('d\<times>'a,'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (d,a) r) =
+  (heap l \<and> heap r \<and> (\<forall>(d',a') \<in> set_mset(mset_tree l + mset_tree r). a \<le> a'))"
+
+fun ltree :: "('d,'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 :: "('d,'a) lheap \<Rightarrow> 'd \<Rightarrow> 'a  \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"node l a b r =
+ (let rl = rk l; rr = rk r
+  in if rl \<ge> rr then Node (rr+1) l (a,b) r else Node (rl+1) r (a,b) l)"
+
+fun get_min :: "('d,'a) lheap \<Rightarrow> 'd\<times>'a" where
+"get_min(Node n l (a,b) r) = (a,b)"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d,'a::linorder) lheap \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1,a1) r1 =: t1) (Node n2 l2 (d2,a2) r2 =: t2) =
+   (if a1 \<le> a2 then node l1 d1 a1 (merge r1 t2)
+    else node l2 d2 a2 (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 (d1,a1) r1, Node n2 l2 (d2,a2) r2) \<Rightarrow>
+    if a1 \<le> a2 then node l1 d1 a1 (merge r1 t2) else node l2 d2 a2 (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::linorder) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d,'a::linorder) lheap \<Rightarrow> ('d,'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
+by(cases t) auto
+
+lemma ltree_node: "ltree (node l a b r) \<longleftrightarrow> ltree l \<and> ltree r"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l a b r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>(a',b') \<in> set_mset(mset_tree l + mset_tree r). b \<le> b')"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
+by (induction h) (auto simp add: eq_Min_iff)
+*)
+
+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 d1 a1 r1 n2 l2 d2 a2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 d1 a1 (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    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)"
+apply(simp add: insert_def)
+(* apply(simp add: heap_merge) not work *)
+oops
+
+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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case sorry (* by(simp add: get_min mset_tree_empty) *)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case sorry (* by(simp add: heap_insert ltree_insert) *)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Rau_Martin_martin.rau@tum.de_571/Home12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,200 @@
+(** Score: 5/5
+*)
+theory Home12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+(* Homework 12 Explicit Priorities *)
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "'d * 'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> 'd * 'a"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d * 'a) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> \<forall>da \<in># mset q. snd (get_min q) \<le> snd da \<and> get_min q \<in># mset q"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+fun mset_tree :: "('d * 'a,'b) tree \<Rightarrow> ('d * 'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l da r) = {#da#} + mset_tree l + mset_tree r"
+
+type_synonym ('d, 'a) lheap = "('d * 'a, nat)tree"
+
+fun rank :: "('d, 'a) lheap \<Rightarrow> nat" where
+  "rank Leaf = 0"
+| "rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d, 'a) lheap \<Rightarrow> nat" where
+  "rk Leaf = 0"
+| "rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun heap :: "('d * 'a::linorder,'b) tree \<Rightarrow> bool" where
+  "heap Leaf = True"
+| "heap (Node _ l (d, a) r) =
+  (heap l \<and> heap r \<and> (\<forall>(d', a') \<in> set_mset(mset_tree l + mset_tree r). a \<le> a'))"
+
+fun ltree :: "('d, 'a) lheap \<Rightarrow> bool" where
+  "ltree Leaf = True"
+| "ltree (Node n l da r) =
+    (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
+
+definition node :: "('d, 'a) lheap \<Rightarrow> 'd * 'a \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"node l da r = (
+  let rl = rk l; rr = rk r in
+  if rl \<ge> rr then Node (rr+1) l da r else Node (rl+1) r da l
+  )"
+
+fun get_min :: "('d, 'a) lheap \<Rightarrow> 'd * 'a" where
+  "get_min(Node n l da r) = da"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+  "merge Leaf t2 = t2"
+| "merge t1 Leaf = t1"
+| "merge (Node n1 l1 (d1, a1) r1 =: t1) (Node n2 l2 (d2, a2) r2 =: t2) =
+   (if a1 \<le> a2 then node l1 (d1, a1) (merge r1 t2)
+    else node l2 (d2, a2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 (d1, a1) r1, Node n2 l2 (d2, a2) r2) \<Rightarrow>
+    if a1 \<le> a2 then node l1 (d1, a1) (merge r1 t2) else node l2 (d2, a2) (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d * 'a::ord) \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+  "insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap" where
+  "del_min Leaf = Leaf"
+| "del_min (Node n l _ r) = merge l r"
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+  by(cases t) auto
+
+lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
+  by(cases t) auto
+
+lemma ltree_node: "ltree (node l da r) \<longleftrightarrow> ltree l \<and> ltree r"
+  by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d, a) r) \<longleftrightarrow> heap l \<and> heap r \<and> (\<forall>(d', a') \<in> set_mset(mset_tree l + mset_tree r). a \<le> a')"
+  by(auto simp add: node_def)
+
+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)
+
+lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
+  by (auto simp add: insert_def mset_merge)
+
+lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> \<forall>da \<in># mset_tree h. snd (get_min h) \<le> snd da \<and> get_min h \<in># mset_tree h"
+  apply (induction h)
+  apply (auto)
+  by blast+
+
+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 d1 a1 r1 n2 l2 d2 a2 r2)
+  then show ?case (is "ltree (merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (d1, a1) (merge r1 ?t2))" by simp
+    also have "... = (ltree l1 \<and> ltree (merge r1 ?t2))"
+      by (simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by simp
+    finally show ?thesis .
+  next
+    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_node_1: "heap (Node 1 Leaf x Leaf)"
+  by (induction x) auto
+
+lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
+  using heap_merge heap_node_1 by (fastforce simp add: insert_def)
+
+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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case by(simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Rau_Martin_martin.rau@tum.de_571/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+martin.rau@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Rieder_Sabine_sabine.rieder@tum.de_586/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+sabine.rieder@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Rieder_Sabine_sabine.rieder@tum.de_586/hw12_tmpl.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,246 @@
+(** Score: 4/5
+  bad get-min spec!
+*)
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times> 'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> (*mset q \<noteq> {#} \<Longrightarrow>*) \<forall>x\<in>#(mset q). snd (get_min q) \<le> (snd x)" (*the part is not needed*)
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation foo: Priority_Queue "{#}" "op={#}" add_mset
+  "\<lambda>_. (undefined,0::nat)"
+  "\<lambda>m. m-{#(undefined,0)#}"
+  top id
+  apply unfold_locales by auto
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+
+
+
+
+fun mset_tree :: "(('a\<times>'b),'c) tree \<Rightarrow> ('a\<times>'b) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node b l a r) = {#a#} + mset_tree l + mset_tree r"
+
+type_synonym ('a,'b) lheap = "(('a\<times>'b),nat)tree"
+
+fun rank :: "('a,'b) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('a,'b) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('a\<times>'b::linorder),'c) 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). snd m \<le> (snd x)))"
+
+fun ltree :: "('a,'b) 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, 'b) lheap \<Rightarrow> ('a\<times> 'b) \<Rightarrow> ('a,'b) lheap \<Rightarrow> ('a,'b) 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,'b) lheap \<Rightarrow> ('a\<times>'b)" where
+"get_min(Node n l a r) = a" |
+"get_min Leaf = undefined"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('a,'b::ord) lheap \<Rightarrow> ('a,'b) lheap \<Rightarrow> ('a,'b) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
+   (if snd a1 \<le> snd a2 then node l1 a1 (merge r1 t2)
+    else node l2 a2 (merge r2 t1))"
+
+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 snd a1 \<le> snd 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)
+
+hide_const (open) insert
+
+definition insert :: "('a\<times> 'b::ord) \<Rightarrow> ('a , 'b) lheap \<Rightarrow>  ('a , 'b) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('a, 'b::ord) lheap \<Rightarrow> ('a , 'b) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+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). snd a \<le> snd x)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h(*;  h \<noteq> Leaf *)\<rbrakk> \<Longrightarrow>  \<forall>x\<in>#(mset_tree h). snd (get_min h) \<le> (snd x)" (*not needed as well*)
+by (induction h) (auto simp add: eq_Min_iff)
+
+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 "snd a1 \<le> snd 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))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `snd a1 \<le> snd a2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> snd a1 \<le> snd 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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case by(simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Smith_Nicholas_nick.smith@tum.de_584/HW12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,246 @@
+(** Score: 4/5
+  bad get-min spec
+*)
+theory HW12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d \<times> 'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d \<times> 'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d \<times> 'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q \<in> set_mset(mset q)
+\<Longrightarrow>\<forall>(d,a)\<in>set_mset(mset q). a \<ge> snd(get_min q)"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation foo: Priority_Queue "{#}" "op={#}" add_mset
+  "\<lambda>_. (undefined,0::nat)"
+  "\<lambda>m. m-{#(undefined,0)#}"
+  top id
+  apply unfold_locales by auto
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+fun mset_tree :: "(('d\<times>'a),'b) tree \<Rightarrow> ('d\<times>'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
+
+type_synonym ('d,'a) lheap = "(('d\<times>'a),nat)tree"
+
+fun rank :: "('d,'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d,'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('d\<times>'a),'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (d,a) r) =
+  (heap l \<and> heap r \<and> (\<forall>(x,p) \<in> set_mset(mset_tree l + mset_tree r). a \<le> p))"
+
+fun ltree :: "('d,'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 :: "('d,'a) lheap \<Rightarrow> ('d \<times>'a)\<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'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 :: "('d,'a) lheap \<Rightarrow> ('d \<times>'a)" where
+"get_min(Node n l x r) = x" |
+"get_min Leaf = undefined"
+
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d,'a::ord) lheap \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1,a1) r1 =: t1) (Node n2 l2 (d2,a2) r2 =: t2) =
+   (if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2)
+    else node l2 (d2,a2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1(d1,a1) r1, Node n2 l2 (d2,a2) r2) \<Rightarrow>
+    if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2) else node l2 (d2,a2) (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::ord) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d,'a::ord) lheap \<Rightarrow> ('d,'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d,a) r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). a \<le> y)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap q;  q \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min q \<in> set_mset(mset_tree q)\<Longrightarrow>
+\<forall>(x,p)\<in>set_mset(mset_tree q). p \<ge> snd(get_min q)"
+  apply (induction q)
+  apply auto
+  by blast+
+
+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 d1 a1 r1 n2 l2 d2 a2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (d1, a1) (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    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 base_heap[simp]: " heap \<langle>n, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle>"
+  apply (induction x)
+  by (auto)
+
+lemma aux: "heap t \<Longrightarrow>  heap (merge \<langle>n, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle> t)"
+  apply (induction t)
+  by (auto simp add: heap_merge)
+
+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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case by(simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Smith_Nicholas_nick.smith@tum.de_584/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+nick.smith@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Somasundaram_Arun_ge69kel@mytum.de_588/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+ge69kel@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Somasundaram_Arun_ge69kel@mytum.de_588/hw12_tmpl.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,256 @@
+(** Score: 4/5
+  bad get-min spec
+*)
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q \<in> set_mset(mset q) \<Longrightarrow> \<forall>p \<in> set_mset(mset q). snd (get_min q) \<le> snd p"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation foo: Priority_Queue "{#}" "op={#}" add_mset
+  "\<lambda>_. (undefined,0::nat)"
+  "\<lambda>m. m-{#(undefined,0)#}"
+  top id
+  apply unfold_locales by auto
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+
+
+
+
+
+fun mset_tree :: "(('d\<times>'a),'b) tree \<Rightarrow> ('d\<times>'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
+
+type_synonym ('d, 'a) lheap = "(('d\<times>'a),nat)tree"
+
+fun rank :: "('d, 'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d, 'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('d\<times>'a),'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (d,m) r) =
+  (heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). m \<le> y))"
+
+fun ltree :: "('d, '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 :: "('d, 'a) lheap \<Rightarrow> ('d\<times>'a) \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, '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 :: "('d, 'a) lheap \<Rightarrow> ('d\<times>'a)" where
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1, a1) r1 =: t1) (Node n2 l2 (d2,a2) r2 =: t2) =
+   (if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2)
+    else node l2 (d2,a2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 (d1,a1) r1, Node n2 l2 (d2,a2) r2) \<Rightarrow>
+    if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2) else node l2 (d2,a2) (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: " ('d\<times>'a::ord) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d,a) r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). a \<le> y)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow>  get_min h \<in> set_mset(mset_tree h) \<Longrightarrow> \<forall>(x,y) \<in> set_mset(mset_tree h). snd (get_min h) \<le> y"
+  apply(induction h)
+   apply auto
+   apply blast
+  by blast
+
+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 d1 a1 r1 n2 l2 d2 a2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (d1,a1) (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    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_aux1[simp]: "heap \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle>"
+  by(induction x)(auto)
+
+lemma heap_insert_aux2[simp]:  "heap t \<Longrightarrow> heap (merge \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle> t)"
+  apply(induction t)
+  by(auto simp add:heap_merge)
+
+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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case
+    by (metis (full_types) case_prodE get_min mset_tree.simps(1) prod.sel(2))
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Stamer_Florian_florian.stamer@tum.de_575/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+florian.stamer@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Stamer_Florian_florian.stamer@tum.de_575/ex12.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,246 @@
+(** Score: 4/5
+  bad get-min spec
+*)
+theory ex12
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert (d,p) q) = mset q + {#(d,p)#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> snd (get_min q) = Min (snd ` (set_mset (mset q)))"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert (d,p) q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation foo: Priority_Queue "{#}" "op={#}" "add_mset"
+  "\<lambda>m. (undefined,Min_mset (image_mset (snd) m))"
+  "\<lambda>m. m-{#(undefined,Min_mset (image_mset (snd) m))#}"
+  top id
+  apply unfold_locales by auto
+
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+
+
+
+
+
+fun mset_tree :: "(('d\<times>'a),'b) tree \<Rightarrow> ('d\<times>'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l x r) = {#x#} + mset_tree l + mset_tree r"
+
+type_synonym ('d,'a) lheap = "(('d\<times>'a),nat)tree"
+
+fun rank :: "('d,'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d,'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('d\<times>'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). snd m \<le> snd x))"
+
+fun ltree :: "('d,'a) lheap \<Rightarrow> bool" where
+"ltree Leaf = True" |
+"ltree (Node n l x r) =
+ (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
+
+definition node :: "('d,'a) lheap \<Rightarrow> ('d\<times>'a) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"node l x r =
+ (let rl = rk l; rr = rk r
+  in if rl \<ge> rr then Node (rr+1) l x r else Node (rl+1) r x l)"
+
+fun get_min :: "('d,'a) lheap \<Rightarrow> ('d\<times>'a)" where
+"get_min(Node n l x r) = x"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d,'a::ord) lheap \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 x1 r1 =: t1) (Node n2 l2 x2 r2 =: t2) =
+   (if snd x1 \<le> snd x2 then node l1 x1 (merge r1 t2)
+    else node l2 x2 (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 x1 r1, Node n2 l2 x2 r2) \<Rightarrow>
+    if snd x1 \<le> snd x2 then node l1 x1 (merge r1 t2) else node l2 x2 (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::ord) \<Rightarrow> ('d,'a) lheap \<Rightarrow> ('d,'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d,'a::ord) lheap \<Rightarrow> ('d,'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+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). snd a \<le> snd x)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> snd (get_min h) = Min (snd ` (set_mset (mset_tree h)))"
+by (induction h) (auto simp add: eq_Min_iff)
+
+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 x1 r1 n2 l2 x2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "snd x1 \<le> snd x2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 x1 (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `snd x1 \<le> snd x2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> snd x1 \<le> snd x2"
+    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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case by(simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Wielander_Felix_felix.wielander@tum.de_574/SENTMAIL	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,1 @@
+felix.wielander@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/Wielander_Felix_felix.wielander@tum.de_574/hw12_tmpl.thy	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,241 @@
+(** Score: 2/5
+
+  errors in the theory!
+  bad spec of get-min
+*)
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d * 'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d * 'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d * 'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> snd (get_min q) = Min_mset (image_mset (\<lambda>x . snd x) (mset q))"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+(** Bad specification of get_min! It's return value needs not to be in the queue.
+
+  For example, the following "implementation" of get_min returning
+  an arbitrary value with smallest priority satisfies your spec!
+*)
+
+interpretation foo: Priority_Queue "{#}" "op={#}" "add_mset"
+  "\<lambda>m. (undefined,Min_mset (image_mset (snd) m))"
+  "\<lambda>m. m-{#(undefined,Min_mset (image_mset (snd) m))#}"
+  top id
+  apply unfold_locales by auto
+
+
+
+
+
+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> ('d * 'a::linorder)" where
+  "get_min(Node n l a r) = (0::nat,a)"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+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 =: t1) (Node n2 l2 a2 r2 =: t2) =
+   (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
+    else node l2 a2 (merge r2 t1))"
+
+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)
+
+hide_const (open) insert
+
+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"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+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"
+by(auto simp add: node_def)
+
+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)"
+by(auto simp add: node_def)
+
+
+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 get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
+by (induction h) (auto simp add: eq_Min_iff)
+
+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))"
+      by(simp add: ltree_node)
+    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)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case by(simp add: get_min mset_tree_empty)
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw12/meta.csv	Fri Jul 13 20:34:42 2018 +0200
@@ -0,0 +1,16 @@
+"570","eric.koepke@tum.de","Koepke","Eric","http://vmnipkow3.in.tum.de/web/submissions/570"
+"571","martin.rau@tum.de","Rau","Martin","http://vmnipkow3.in.tum.de/web/submissions/571"
+"572","mitja.krebs@tum.de","Krebs","Mitja","http://vmnipkow3.in.tum.de/web/submissions/572"
+"573","daniel.kutasi@mytum.de","Kutasi","Daniel","http://vmnipkow3.in.tum.de/web/submissions/573"
+"574","felix.wielander@tum.de","Wielander","Felix","http://vmnipkow3.in.tum.de/web/submissions/574"
+"575","florian.stamer@tum.de","Stamer","Florian","http://vmnipkow3.in.tum.de/web/submissions/575"
+"577","j.gottfriedsen@tum.de","Gottfriedsen","Jakob","http://vmnipkow3.in.tum.de/web/submissions/577"
+"578","ga53qud@mytum.de","Das Sharma","Amartya","http://vmnipkow3.in.tum.de/web/submissions/578"
+"580","max.kirchmeier@tum.de","Kirchmeier","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/580"
+"581","clemens.jonischkeit@tum.de","Jonischkeit","Clemens","http://vmnipkow3.in.tum.de/web/submissions/581"
+"582","a.putwattana@tum.de","Putwattana","Attakorn","http://vmnipkow3.in.tum.de/web/submissions/582"
+"583","s.griebel@tum.de","Griebel","Simon","http://vmnipkow3.in.tum.de/web/submissions/583"
+"584","nick.smith@tum.de","Smith","Nicholas","http://vmnipkow3.in.tum.de/web/submissions/584"
+"586","sabine.rieder@tum.de","Rieder","Sabine","http://vmnipkow3.in.tum.de/web/submissions/586"
+"587","ga96koz@mytum.de","Mutius","Joshua","http://vmnipkow3.in.tum.de/web/submissions/587"
+"588","ge69kel@mytum.de","Somasundaram","Arun","http://vmnipkow3.in.tum.de/web/submissions/588"