--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Biendarra_Julian_julian.biendarra@tum.de_613/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+julian.biendarra@tum.de
--- a/Exercises/hwsubm/13/Biendarra_Julian_julian.biendarra@tum.de_613/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Biendarra_Julian_julian.biendarra@tum.de_613/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
(*<*)
theory hw13
imports "~~/src/HOL/Library/Multiset"
@@ -70,4 +72,4 @@
(*<*)
end
(*>*)
-
\ No newline at end of file
+
--- a/Exercises/hwsubm/13/Erhard_Julian_ga48kog@mytum.de_623/Ex13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Erhard_Julian_ga48kog@mytum.de_623/Ex13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
theory Ex13
imports "~~/src/HOL/Library/Multiset"
begin
@@ -117,4 +119,4 @@
finally show ?thesis using c Hp by simp
qed
end
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Erhard_Julian_ga48kog@mytum.de_623/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+ga48kog@mytum.de
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Gnther_Jochen_jochen.guenther@mytum.de_624/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+jochen.guenther@mytum.de
--- a/Exercises/hwsubm/13/Gnther_Jochen_jochen.guenther@mytum.de_624/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Gnther_Jochen_jochen.guenther@mytum.de_624/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
(*<*)
theory hw13
imports "~~/src/HOL/Library/Multiset"
@@ -81,4 +83,4 @@
(*<*)
end
(*>*)
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Groer_Markus_markus.grosser@tum.de_635/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+markus.grosser@tum.de
--- a/Exercises/hwsubm/13/Groer_Markus_markus.grosser@tum.de_635/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Groer_Markus_markus.grosser@tum.de_635/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
(* Original Author: Tobias Nipkow *)
theory hw13
@@ -64,4 +66,4 @@
done \<comment> \<open>I am not very happy with this proof\<close>
end
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Haslbeck_Maximilian_max.haslbeck@mytum.de_622/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+max.haslbeck@mytum.de
--- a/Exercises/hwsubm/13/Haslbeck_Maximilian_max.haslbeck@mytum.de_622/ex13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Haslbeck_Maximilian_max.haslbeck@mytum.de_622/ex13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,6 +1,8 @@
+(** Score: 5/5
+*)
(*<*)
theory ex13
-imports "../Thys/Skew_Heap"
+ imports "~~/src/HOL/Library/Multiset"
begin
(*>*)
@@ -133,4 +135,4 @@
(*<*)
end
(*>*)
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hellauer_Fabian_f.hellauer@tum.de_616/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+f.hellauer@tum.de
--- a/Exercises/hwsubm/13/Hellauer_Fabian_f.hellauer@tum.de_616/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Hellauer_Fabian_f.hellauer@tum.de_616/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,5 +1,7 @@
+(** Score: 5/5
+*)
theory hw13
- imports "../../../Public/Thys/Skew_Heap"
+ imports "../../../../../Public/Thys/Skew_Heap"
begin
text \<open>
@@ -70,4 +72,4 @@
done
end
-
\ No newline at end of file
+
--- a/Exercises/hwsubm/13/Hu_Shuwei_shuwei.hu@tum.de_614/Homework13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Hu_Shuwei_shuwei.hu@tum.de_614/Homework13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,5 +1,7 @@
+(** Score: 5/5
+*)
theory Homework13
-imports "material/Thys/Skew_Heap"
+imports "../../../../../Public/Thys/Skew_Heap"
begin
datatype 'a hp = Hp 'a "'a hp list"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hu_Shuwei_shuwei.hu@tum.de_614/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+shuwei.hu@tum.de
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Hutzler_Matthias_ga95luy@mytum.de_650/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+ga95luy@mytum.de
--- a/Exercises/hwsubm/13/Hutzler_Matthias_ga95luy@mytum.de_650/ex13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Hutzler_Matthias_ga95luy@mytum.de_650/ex13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,7 @@
+(** Score: 0/5
+
+ No proofs? no points!
+*)
theory ex13
imports Complex_Main
"~~/src/HOL/Library/Multiset"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Keinholz_Jonas_jonas.keinholz@tum.de_612/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+jonas.keinholz@tum.de
--- a/Exercises/hwsubm/13/Keinholz_Jonas_jonas.keinholz@tum.de_612/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Keinholz_Jonas_jonas.keinholz@tum.de_612/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
theory hw13
imports "~~/src/HOL/Library/Multiset"
begin
@@ -57,4 +59,4 @@
by (cases h) (auto simp: mset_merge_pairs)
end
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Kurz_Friedrich_friedrich.kurz@tum.de_645/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+friedrich.kurz@tum.de
--- a/Exercises/hwsubm/13/Kurz_Friedrich_friedrich.kurz@tum.de_645/hw_13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Kurz_Friedrich_friedrich.kurz@tum.de_645/hw_13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,6 +1,9 @@
+(** Score: 3/5
+ sorried lemma about merge, required for del_min.
+*)
(*<*)
theory hw_13
-imports "../../../Public/Thys/Skew_Heap"
+imports "../../../../../Public/Thys/Skew_Heap"
begin
(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Madge_Pimentel_Fabio_fabio.madge@tum.de_626/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+fabio.madge@tum.de
--- a/Exercises/hwsubm/13/Madge_Pimentel_Fabio_fabio.madge@tum.de_626/tmpl13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Madge_Pimentel_Fabio_fabio.madge@tum.de_626/tmpl13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,6 +1,8 @@
+(** Score: 5/5
+*)
(*<*)
theory tmpl13
-imports "Skew_Heap"
+imports "../../../../../Public/Thys/Skew_Heap"
begin
(*>*)
@@ -77,4 +79,4 @@
(*<*)
end
(*>*)
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Ouyang_Lena_ga96vup@mytum.de_627/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+ga96vup@mytum.de
--- a/Exercises/hwsubm/13/Ouyang_Lena_ga96vup@mytum.de_627/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Ouyang_Lena_ga96vup@mytum.de_627/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,8 +1,10 @@
+(** Score: 5/5
+*)
theory hw13
imports Complex_Main
"~~/src/HOL/Library/Multiset"
- "../../../../Desktop/fds/Thys/Priority_Queue"
- "../../../../Desktop/fds/Thys/Heap_Prelim"
+ "../../../../../Public/Thys/Priority_Queue"
+ "../../../../../Public/Thys/Heap_Prelim"
begin
subsection \<open>Pairing_Heap\<close>
datatype 'a hp = Hp 'a "'a hp list"
@@ -49,6 +51,8 @@
lemma mset_del_min: "mset_heap2 (del_min2 (Some h)) = mset_hp h - {#get_min2 (Some h)#}"
by(cases h) (auto simp: mset_merge_pairs)
+(** Using separate submission \<dots> *)
+
text \<open>Project\<close>
section \<open>Fibonacci Heaps\<close>
datatype 'a Node = Node (rank: nat) (root: 'a) (children: "'a Node list")
@@ -314,4 +318,4 @@
then show ?case by auto
qed
end
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Rdle_Karl_Jonas_jonas.raedle@tum.de_621/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+jonas.raedle@tum.de
--- a/Exercises/hwsubm/13/Rdle_Karl_Jonas_jonas.raedle@tum.de_621/hw13_sub.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Rdle_Karl_Jonas_jonas.raedle@tum.de_621/hw13_sub.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,6 +1,8 @@
+(** Score: 5/5
+*)
(*<*)
theory hw13_sub
- imports "../../../Public/Thys/Skew_Heap"
+ imports "../../../../../Public/Thys/Skew_Heap"
begin
(*>*)
@@ -68,4 +70,4 @@
(*<*)
end
(*>*)
-
\ No newline at end of file
+
--- a/Exercises/hwsubm/13/Rokopf_Simon_simon.rosskopf@tum.de_630/Pairing_Heap.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Rokopf_Simon_simon.rosskopf@tum.de_630/Pairing_Heap.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
theory Pairing_Heap
imports "~~/src/HOL/Library/Multiset"
@@ -72,4 +74,4 @@
by (smt image_mset.compositionality image_mset_cong mset_heap.elims mset_hp.simps o_def option.sel option.simps(3))
end
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Rokopf_Simon_simon.rosskopf@tum.de_630/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+simon.rosskopf@tum.de
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Saporta_Antoine_Jacques_antoine.saporta@tum.de_620/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+antoine.saporta@tum.de
--- a/Exercises/hwsubm/13/Saporta_Antoine_Jacques_antoine.saporta@tum.de_620/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Saporta_Antoine_Jacques_antoine.saporta@tum.de_620/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
(*<*)
theory hw13
imports "~~/src/HOL/Library/Multiset"
@@ -81,4 +83,4 @@
(*<*)
end
(*>*)
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_643/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+maximilian.schaeffeler@tum.de
--- a/Exercises/hwsubm/13/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_643/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_643/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
theory hw13
imports "~~/src/HOL/Library/Multiset"
begin
@@ -55,4 +57,4 @@
by (simp add: mset_merge_pairs)
end
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+daniel.somogyi@tum.de
--- a/Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Somogyi_Daniel_daniel.somogyi@tum.de_625/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
(* Author: Tobias Nipkow *)
theory hw13
@@ -139,4 +141,4 @@
(* maybe doing mset_heap first would've simplify the proofs
whatever... *)
end
-
\ No newline at end of file
+
--- a/Exercises/hwsubm/13/Stevens_Lukas_lukas.stevens@tum.de_617/Ex13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Stevens_Lukas_lukas.stevens@tum.de_617/Ex13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,6 +1,8 @@
+(** Score: 5/5
+*)
(*<*)
theory Ex13
- imports "../Thys/Skew_Heap"
+ imports "../../../../../Public/Thys/Skew_Heap"
begin
(*>*)
@@ -69,4 +71,4 @@
(*<*)
end
(*>*)
-
\ No newline at end of file
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Stevens_Lukas_lukas.stevens@tum.de_617/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+lukas.stevens@tum.de
--- a/Exercises/hwsubm/13/Stwe_Daniel_daniel.stuewe@tum.de_649/HW13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Stwe_Daniel_daniel.stuewe@tum.de_649/HW13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,5 +1,7 @@
+(** Score: 5/5
+*)
theory HW13
- imports "Thys/Pairing_Heap"
+ imports "../../../../../Public/Thys/Pairing_Heap"
begin
datatype 'a hp = Hp 'a "'a hp list"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Stwe_Daniel_daniel.stuewe@tum.de_649/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+daniel.stuewe@tum.de
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/13/Wauligmann_Martin_martin.wauligmann@tum.de_641/SENTMAIL Mon Jul 31 14:21:11 2017 +0200
@@ -0,0 +1,1 @@
+martin.wauligmann@tum.de
--- a/Exercises/hwsubm/13/Wauligmann_Martin_martin.wauligmann@tum.de_641/hw13.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/13/Wauligmann_Martin_martin.wauligmann@tum.de_641/hw13.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 5/5
+*)
theory hw13
imports "~~/src/HOL/Library/Tree_Multiset"
begin
--- a/Exercises/hwsubm/OR/Groer_Markus_markus.grosser@tum.de_636/Arbitrary_Precision.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Groer_Markus_markus.grosser@tum.de_636/Arbitrary_Precision.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,5 @@
+(** Score: 20/15
+*)
theory Arbitrary_Precision
imports Main
begin
@@ -7,6 +9,14 @@
implemented and proven.
\<close>
+(** The theory also contains shl, shr, cmp. All seem implemented and proved!
+ You overlooked one Isabelle error, probably due to a late change.
+ I could easily fix it by removing the "(2)"!
+
+ Nice project, fully functional
+*)
+
+
section \<open>Type Definition and Conversions\<close>
type_synonym bitlist = "bool list"
@@ -19,6 +29,8 @@
"nat_of_bitlist [] = 0"
| "nat_of_bitlist (b#bs) = (if b then 1 else 0) + 2 * nat_of_bitlist bs"
+value \<open>nat_of_bitlist [False,True]\<close> (** Leading zeroes treated as significant places *)
+
section \<open>Optimality\<close>
text \<open>
@@ -99,7 +111,9 @@
case False
then show ?thesis
using 1 optimal_def apply (auto split: prod.splits)
- using add_with_carry_empty(2)[of as bs False] by fastforce+
+ (** ISABELLE ERROR! *)
+ (**using add_with_carry_empty(2)[of as bs False] by fastforce+*)
+ using add_with_carry_empty[of as bs False] by fastforce+
qed
next
case (2 a as c)
@@ -233,4 +247,4 @@
qed (fastforce dest: optimal_nat_of_bitlist_ne_zero)+
end
-
\ No newline at end of file
+
--- a/Exercises/hwsubm/OR/Haslbeck_Maximilian_max.haslbeck@mytum.de_640/Pell.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Haslbeck_Maximilian_max.haslbeck@mytum.de_640/Pell.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,4 +1,6 @@
(*\<Rightarrow>Manuel*)
+(** Score: 20/15
+*)
theory Pell
imports Analysis
begin
--- a/Exercises/hwsubm/OR/Hu_Shuwei_shuwei.hu@tum.de_651/Homework_Fibonacci.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Hu_Shuwei_shuwei.hu@tum.de_651/Homework_Fibonacci.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,5 +1,19 @@
(* Author: Shuwei Hu *)
+(** Score: 15/15
+ The formalization contains Fibonacci heaps, with an invariant and
+ an empty, insert, and merge function, proved correct.
+
+ It also defines a consolidate function and a meld function on trees, but
+ the proof attempt stops at this point.
+
+ Also contains a small formalization of lists with O(1) merge, represented
+ as trees.
+
+
+*)
+
+
theory Homework_Fibonacci
imports "~~/src/HOL/Library/Multiset"
begin
@@ -14,6 +28,11 @@
we need a "mark" in a Fibonacci Heap. Here I abandoned the mark, which makes
the "fake Fibonacci Heap" effectively a collection of binomial heaps.
+ Peter: You're fully right, for functional Fibonacci heaps, decrease-key
+ does not really make sense. There are data structures that can overlay
+ an efficient indexing with a priority queue (e.g. Finger Trees), there
+ decreaseKey makes sense. For FibHeaps, it probably does not.
+
2. The constant time of insertion and merging requires doubly linked list, which
is not even easy to just implement (possible in Haskell, but still not easy)
let alone verifying it. It is possible to just use list here and claiming that
@@ -25,8 +44,14 @@
merging by creating a new tree. However, it doesn't support deletion. This is why
I didn't implement del_min for the heap.
+ Peter: That mergable lists sound like a mini-project on its own :)
+
+
3. The @{term consolidate} operation requires randomly accessible array. I used
@{type map} here as an alternative.
+ Peter: That sounds reasonable! Another alternative is to use a
+ list with operations nth and list_update, which, with some tricks,
+ can be mapped to an array.
\<close>
section \<open>Mergeable Sequence\<close>
@@ -297,4 +322,4 @@
oops
end
-
\ No newline at end of file
+
--- a/Exercises/hwsubm/OR/Ouyang_Lena_ga96vup@mytum.de_654/hw13Original.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Ouyang_Lena_ga96vup@mytum.de_654/hw13Original.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,13 @@
+(** Score: 10/15
+
+
+ FibHeap with empty, insert.
+ Correctness of get-min with sorry
+ Started some definitions for delMin, but no proofs
+ Tried some complexity analysis, but only trivial things proved, rest sorried
+
+*)
+
theory hw13Original
imports Complex_Main
"~~/src/HOL/Library/Multiset"
--- a/Exercises/hwsubm/OR/Rokopf_Simon_simon.rosskopf@tum.de_637/SkewBinHeap.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Rokopf_Simon_simon.rosskopf@tum.de_637/SkewBinHeap.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,17 @@
+(** Score: 28/15
+ Really nice one!
+ There is also a
+ skew binomial heap formalization in the AFP, which also supports
+ bootstrapping (probably similar to what you tried as Brodal heaps)
+
+ https://www.isa-afp.org/entries/Binomial-Heaps.shtml
+ This one was also a student project (Half a semester long), and
+ the bootstrapping was only added afterwards by myself.
+
+
+*)
+
+
(*
Contains a formalisation of Skew Binomial heaps, based on the Binomial heaps theory from repository.
--- a/Exercises/hwsubm/OR/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_644/skewBin.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_644/skewBin.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,11 @@
+(** Score: 15/15
+
+ Skew bin numbers with inc, dec, from_nat
+
+ Unicity proof attempted, but not finished.
+
+*)
+
theory skewBin
imports Main
begin
--- a/Exercises/hwsubm/OR/Somogyi_Daniel_daniel.somogyi@tum.de_633/FiboHeap.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Somogyi_Daniel_daniel.somogyi@tum.de_633/FiboHeap.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,9 @@
+(** Score: 15/15
+ Fibonacci heaps with empty, meld.
+ Delete-Min (consolidate) attempted, but proofs not completed.
+ Timing of trivial operations done, no timing of consolidate.
+
+*)
section \<open>Fibonacci Heap\<close>
text\<open>for the whole file: theorems are important things to show, lemmas are
--- a/Exercises/hwsubm/OR/Stevens_Lukas_lukas.stevens@tum.de_657/LazyBinHeap.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Stevens_Lukas_lukas.stevens@tum.de_657/LazyBinHeap.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,19 @@
+(** Score: 24/15
+ Fibonacci heaps with empty, merge, and del_min
+
+ ** One uncommented Isabelle error in proof. Analyzing it hints at some missing invariant proofs.
+ UPDATE: Included patch sent by email on request, errors gone.
+
+ ** Two sorries in auxiliary lemmas. Not clear to me whether these are really provable,
+ or require some preconditions.
+
+ ** empty: The correct correctness lemma would be:
+ mset_lazybheap Empty = {#}
+ the is_empty predicate seems to make little sense
+
+*)
+
+
theory LazyBinHeap
imports Complex_Main "../../../../../Public/Thys/Heap_Prelim" "../../../../../Public/Thys/BinHeap"
begin
@@ -364,6 +380,7 @@
qed
+(** Maybe. Looks like you could need a precondition rank x < length rs ... *)
lemma list_length_three: "\<lbrakk>rs ! rank x = None\<rbrakk>
\<Longrightarrow> consolidate_list_length_aux (x#xs) rs = consolidate_list_length_aux xs (rs[rank x := Some x])"
(* this lemma can certainly be proven *)
@@ -646,7 +663,9 @@
"set (filter_map_None (replicate i None)) = {}"
by (induction i) auto
-lemma mset_consolidate: "mset_heap (consolidate xs) = mset_heap xs"
+lemma mset_consolidate:
+ assumes "\<forall>t \<in> set xs. otree_invar t \<and> btree_invar t"
+ shows "mset_heap (consolidate xs) = mset_heap xs"
unfolding consolidate_list_length_def
proof -
let ?in = "replicate (consolidate_list_length_aux xs []) None"
@@ -654,12 +673,22 @@
have simp_def: "mset_heap (consolidate xs) =
mset_heap (filter_map_None (consolidate_helper xs ?in))"
by(simp add: consolidate_list_length_def)
-
- have length_rep: "length ?in = consolidate_list_length_aux xs []"
- using length_replicate by simp
-
- show ?thesis using simp_def length_rep mset_consolidate_helper[of xs ?in]
- by (simp add: consolidate_list_length_aux_None mset_replicate_None)
+ have length_rep: "consolidate_list_length_aux xs ?in
+ \<le> length (replicate (consolidate_list_length_aux xs []) None)"
+ using length_replicate
+ by (simp add: consolidate_list_length_aux_None)
+
+ have "\<forall>t\<in> set (filter_map_None ?in). otree_invar t \<and> btree_invar t"
+ by (simp add: set_replicate_None)
+ then have invar_rep: "\<forall>t\<in>set xs \<union> set (filter_map_None ?in). otree_invar t \<and> btree_invar t"
+ using assms by blast
+
+ have invar2_rep: "\<forall>i<length ?in. \<forall>t.
+ ?in ! i = Some t \<longrightarrow> rank t = i"
+ by(simp add: set_replicate_None)
+ show ?thesis using simp_def length_rep mset_consolidate_helper[of xs ?in] invar_rep invar2_rep
+ by (simp add: mset_replicate_None)
+
qed
@@ -687,7 +716,9 @@
show ?thesis
using simp_def length_rep invars_consolidate_helper[of xs ?in] invar_rep invar2_rep
- by (metis consolidate.simps consolidate_list_length_def)
+ by (simp add: consolidate_list_length_def)
+ (** Isabelle error! I re-sledgehammered to find the above proof. *)
+ (**by (metis consolidate.simps consolidate_list_length_def) *)
qed
@@ -760,6 +791,7 @@
lemma mset_delete_min:
assumes "hp \<noteq> Empty"
+ assumes "invar hp"
shows "mset_lazybheap hp = mset_lazybheap (delete_min hp) + {#get_min hp#}"
proof(cases hp)
case (Heap x xs)
@@ -775,7 +807,10 @@
using \<open>x = Node r a ns\<close> mset_btree_Node by simp
finally have mset_transform: "mset_lazybheap (Heap x xs) =
add_mset (root x) (mset_heap (ns@xs))" .
-
+ have weaker_invar_xs: "weaker_invar xs" using assms unfolding invar_def by (simp add: Heap)
+ have weaker_invar_ns: "weaker_invar ns" using assms unfolding invar_def Heap
+ by(auto split: lazybheap.split simp: \<open>x = Node r a ns\<close>)
+
have "mset_lazybheap (delete_min hp) = mset_lazybheap (delete_min (Heap x xs))"
using Heap by simp
also have "\<dots> = mset_lazybheap (lazybheap_from_treelist (consolidate (ns@xs)))"
@@ -783,7 +818,7 @@
also have "\<dots> = mset_heap (consolidate (ns@xs))"
using mset_lazybheap_from_treelist by simp
also have "\<dots> = mset_heap (ns@xs)"
- using mset_consolidate[of "ns@xs"] by simp
+ using mset_consolidate[of "ns@xs"] weaker_invar_xs weaker_invar_ns by auto
finally have "mset_lazybheap (delete_min hp) = mset_heap (ns@xs)" .
then show ?thesis using Heap get_min_a mset_transform by auto
--- a/Exercises/hwsubm/OR/Stwe_Daniel_daniel.stuewe@tum.de_660/SkewBinHeap.thy Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/OR/Stwe_Daniel_daniel.stuewe@tum.de_660/SkewBinHeap.thy Mon Jul 31 14:21:11 2017 +0200
@@ -1,3 +1,9 @@
+(** 20/15
+ Skew binomial heaps and size-height relation.
+
+ Missing: get_min, delete_min mset_heap lemma
+
+*)
theory SkewBinHeap
imports
"../../../../../Public/Thys/BinHeap"
--- a/Exercises/hwsubm/email.log Mon Jul 31 14:20:55 2017 +0200
+++ b/Exercises/hwsubm/email.log Mon Jul 31 14:21:11 2017 +0200
@@ -934,3 +934,63 @@
Do 27. Jul 11:20:08 CEST 2017
/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 12 maximilian.schaeffeler@tum.de hw12.thy
OK
+Mo 31. Jul 12:02:03 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 jonas.keinholz@tum.de hw13.thy
+OK
+Mo 31. Jul 12:02:03 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 julian.biendarra@tum.de hw13.thy
+OK
+Mo 31. Jul 12:02:03 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 shuwei.hu@tum.de Homework13.thy
+OK
+Mo 31. Jul 12:02:03 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 f.hellauer@tum.de hw13.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 lukas.stevens@tum.de Ex13.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 antoine.saporta@tum.de hw13.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 jonas.raedle@tum.de hw13_sub.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 max.haslbeck@mytum.de ex13.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 ga48kog@mytum.de Ex13.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 jochen.guenther@mytum.de hw13.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 daniel.somogyi@tum.de FiboHeap.thy hw13.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 fabio.madge@tum.de tmpl13.thy
+OK
+Mo 31. Jul 12:02:04 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 ga96vup@mytum.de hw13.thy
+OK
+Mo 31. Jul 12:02:05 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 simon.rosskopf@tum.de Pairing_Heap.thy
+OK
+Mo 31. Jul 12:02:05 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 markus.grosser@tum.de hw13.thy
+OK
+Mo 31. Jul 12:02:05 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 martin.wauligmann@tum.de hw13.thy
+OK
+Mo 31. Jul 12:02:05 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 maximilian.schaeffeler@tum.de hw13.thy
+OK
+Mo 31. Jul 12:02:05 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 friedrich.kurz@tum.de hw_13.thy
+OK
+Mo 31. Jul 12:02:05 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 daniel.stuewe@tum.de HW13.thy
+OK
+Mo 31. Jul 12:02:05 CEST 2017
+/home/lammich/lehre/FDS/Private/Exercises/hwsubm/_sendmail.py PASSWORD 13 ga95luy@mytum.de ex13.thy
+OK