author lammich Mon, 09 Jul 2018 11:57:00 +0200 changeset 69947 cd8eb35f3c38 parent 69946 ed7c67f266ac child 69948 7c35ab688cb8
corr 11
 SS18/Exercises/exam.pdf file | annotate | diff | comparison | revisions SS18/Exercises/exam/Q_Balanced_Insert.thy file | annotate | diff | comparison | revisions SS18/Exercises/hwsubm/email.log file | annotate | diff | comparison | revisions
Binary file SS18/Exercises/exam.pdf has changed
--- a/SS18/Exercises/exam/Q_Balanced_Insert.thy	Mon Jul 09 11:56:29 2018 +0200
+++ b/SS18/Exercises/exam/Q_Balanced_Insert.thy	Mon Jul 09 11:57:00 2018 +0200
@@ -1,15 +1,15 @@
-(*<*)
+(*<*)
theory Q_Balanced_Insert
-imports
+imports
Complex_Main
-  "~~/src/HOL/Library/Multiset"
-  "../../../Public/Demos/BST_Demo"
+  "HOL-Library.Multiset"
+  "HOL-Library.Tree"
begin
(*>*)
-
-  section \<open>Converting List for Balanced Insert\<close>
+
+  section \<open>Converting List for Balanced Insert\<close>
(*<*)
-  consts preprocess :: "'a::linorder list \<Rightarrow> 'a list"
+  consts preprocess :: "'a::linorder list \<Rightarrow> 'a list"
(*>*)

text \<open>
@@ -23,112 +23,112 @@
else Node l a r)"
\<close>}

-    We define the function \<open>from_list\<close>, which inserts the elements of a
+    We define the function \<open>from_list\<close>, which inserts the elements of a
list into an initially empty search tree:
\<close>
-  definition from_list :: "'a::linorder list \<Rightarrow> 'a tree" where
+  definition from_list :: "'a::linorder list \<Rightarrow> 'a tree" where
"from_list l = fold ins l Leaf"

-  text \<open>
+  text \<open>
that preprocesses the list such that the resulting tree is balanced.

You may assume that the list
is sorted, distinct, and has exactly \<open>2^k - 1\<close> elements for some \<open>k\<close>.
That is, your \<open>preprocess\<close> function must satisfy:
\<close>
-  lemma
+  lemma
assumes "sorted l" and "distinct l" and  "length l = 2^k-1"
shows "set (preprocess l) = set l" and "balanced (from_list (preprocess l))"
(*<*) oops (*>*)

-  text \<open>
+  text \<open>
Note: {\bf No proofs required}, only a specification of the \<open>preprocess\<close> function!
-  \<close>
+  \<close>

-  subsubsection \<open>Solution\<close>
-
-
+  subsubsection \<open>Solution\<close>
+
+
definition split :: "'a list \<Rightarrow> ('a list \<times> 'a \<times> 'a list)" where
"split l = (let n=length l in (take (n div 2) l, l!(n div 2), drop (n div 2 + 1) l))"
-
-  (*<*)
+
+  (*<*)
lemma split_lemma:
-    assumes "(l,x,r) = split xs"
-    assumes "xs\<noteq>[]"
+    assumes "(l,x,r) = split xs"
+    assumes "xs\<noteq>[]"
shows "xs = l@x#r"
-    using assms unfolding split_def
-    by (cases "even (length xs)"; auto elim!: dvdE simp: id_take_nth_drop)
+    using assms unfolding split_def
+    by (cases "even (length xs)"; auto elim!: dvdE simp: id_take_nth_drop)

lemma split_lemma':
-    assumes "(l,x,r) = split xs"
-    assumes "length xs = 2^(Suc k) - 1"
+    assumes "(l,x,r) = split xs"
+    assumes "length xs = 2^(Suc k) - 1"
shows "length r = length l" "length l = 2^k - 1" "xs = l@x#r"
-    using assms unfolding split_def
-    apply -
+    using assms unfolding split_def
+    apply -
apply (auto simp: min_def)
apply (smt One_nat_def Suc_double_not_eq_double Suc_eq_plus1 Suc_mult_two_diff_one add_diff_cancel_left diff_Suc_1 dvd_mult_div_cancel mult_2 nonzero_mult_div_cancel_left odd_Suc_div_two power_not_zero zero_not_eq_two)
by (metis One_nat_def Suc_mult_two_diff_one assms(1) list.size(3) nonzero_mult_div_cancel_left one_div_two_eq_zero power_not_zero split_lemma zero_not_eq_two)
-
+
lemma [simp]: "(l,a,r) = split (x#xs) \<Longrightarrow> length l < Suc (length xs) \<and> length r < Suc (length xs)"
-    using split_lemma[of l a r "x#xs"]
+    using split_lemma[of l a r "x#xs"]
apply auto
apply (metis append_eq_conv_conj diff_self_eq_0 length_Cons length_drop length_take linorder_neqE_nat min.strict_order_iff nat.distinct(1))
-    by (metis Suc_le_lessD le_add2 length_Cons length_append)
+    by (metis Suc_le_lessD le_add2 length_Cons length_append)

(*>*)
-
+
fun preproc :: "'a list \<Rightarrow> 'a list" where
"preproc [] = []"
| "preproc xs = (let (l,x,r) = split xs in x#preproc l@preproc r)"
-
+

-  (*<*)
-  lemma split_mset:
-    "\<lbrakk> split (x#xs) = (l,a,r) \<rbrakk> \<Longrightarrow> add_mset x (mset xs) = add_mset a (mset l + mset r)"
-    apply (drule split_lemma[OF sym])
-    apply simp
+  (*<*)
+  lemma split_mset:
+    "\<lbrakk> split (x#xs) = (l,a,r) \<rbrakk> \<Longrightarrow> add_mset x (mset xs) = add_mset a (mset l + mset r)"
+    apply (drule split_lemma[OF sym])
+    apply simp
apply (drule arg_cong[where f=mset])
-    by auto
-
-  lemma L_mset_preserve[simp]: "mset (preproc l) = mset l"
+    by auto
+
+  lemma L_mset_preserve[simp]: "mset (preproc l) = mset l"
apply (induction l rule: preproc.induct)
apply simp
apply (auto dest: split_mset split:prod.split)
-    done
+    done

-  theorem L_set_preserve[simp]: "set (preproc l) = set l"
+  theorem L_set_preserve[simp]: "set (preproc l) = set l"
by (metis L_mset_preserve set_mset_mset)
-
-  lemma L_len_preserve[simp]: "length (preproc l) = length l"
+
+  lemma L_len_preserve[simp]: "length (preproc l) = length l"
by (metis L_mset_preserve size_mset)
-
+
lemma ins_left:
assumes "\<forall>x\<in>set xs. x<a"
-    shows "fold ins xs \<langle>l, a, r\<rangle> = \<langle>fold ins xs l,a,r\<rangle>"
+    shows "fold ins xs \<langle>l, a, r\<rangle> = \<langle>fold ins xs l,a,r\<rangle>"
using assms
-    by (induction xs arbitrary: l) auto
-
+    by (induction xs arbitrary: l) auto
+
lemma ins_right:
assumes "\<forall>x\<in>set xs. x>a"
-    shows "fold ins xs \<langle>l, a, r\<rangle> = \<langle>l,a,fold ins xs r\<rangle>"
+    shows "fold ins xs \<langle>l, a, r\<rangle> = \<langle>l,a,fold ins xs r\<rangle>"
using assms
by (induction xs arbitrary: r) auto
-
-  (* TODO: Move *)
+
+  (* TODO: Move *)
lemma empty_balanced[simp]: "balanced \<langle>\<rangle>" unfolding balanced_def by auto
-
+
lemma bst_size_card_set: "bst t \<Longrightarrow> size t = card (set_tree t)"
apply (induction t) apply (auto)
-    using not_less_iff_gr_or_eq
+    using not_less_iff_gr_or_eq
by (subst card_Un_disjoint card_insert_disjoint; auto)+
-
+
lemma bst_fold_ins: "bst t \<Longrightarrow> bst (fold ins xs t)"
by (induction xs arbitrary: t) (auto simp: bst_ins)

lemma bst_from_list: "bst (from_list xs)"
unfolding from_list_def by (simp add: bst_fold_ins)
-
+
lemma ss_aux: "bst t \<Longrightarrow> distinct xs \<Longrightarrow> set xs \<inter> set_tree t = {} \<Longrightarrow> card (set_tree (fold ins xs t)) = length xs + card (set_tree t)"
proof (induction xs arbitrary: t)
case Nil
@@ -141,99 +141,99 @@
then show ?case
by simp
qed
-
-  lemma ss: "bst t \<Longrightarrow> distinct xs \<Longrightarrow> size (from_list xs) = length xs"
+
+  lemma ss: "bst t \<Longrightarrow> distinct xs \<Longrightarrow> size (from_list xs) = length xs"
by (simp add: bst_fold_ins ss_aux bst_size_card_set from_list_def)
-
-
-  lemma height_if_complete: "complete t \<Longrightarrow> height t = log 2 (size t + 1)"
+
+
+  lemma height_if_complete: "complete t \<Longrightarrow> height t = log 2 (size t + 1)"
apply (drule size_if_complete)
by (auto simp: ln_realpow log_def)
-
-
+
+
theorem "\<lbrakk>sorted xs; distinct xs; length xs = 2^k - 1\<rbrakk> \<Longrightarrow> complete (from_list (preproc xs))"
proof (induction xs arbitrary: k rule: preproc.induct)
case 1
then show ?case by (auto simp: from_list_def split:prod.split)
next
case (2 v va)
-
-    obtain l x r where
+
+    obtain l x r where
X1[simp]: "split (v # va) = (l,x,r)"
by (cases "split (v # va)")

from split_lemma[OF X1[symmetric]] have
U: "v # va = l @ x # r"
by simp_all
-
+
note PREMS = "2.prems"[unfolded U]
-
-    from PREMS(3) obtain kk where KK[simp]: "k=Suc kk"
+
+    from PREMS(3) obtain kk where KK[simp]: "k=Suc kk"
by (cases k) auto
from split_lemma'[of l x r "v#va" kk, OF sym, OF X1]
-    have [simp]: "length r = length l" "length l = 2 ^ kk - 1"
+    have [simp]: "length r = length l" "length l = 2 ^ kk - 1"
unfolding U using PREMS(3) by auto
-
+
from PREMS have X2: "\<forall>y\<in>set (preproc l). y<x" "\<forall>y\<in>set (preproc r). x<y"
by (force simp: sorted_append sorted_Cons)+
-
+
from PREMS(2) have [simp]: "distinct (preproc l)" "distinct (preproc r)"
by (clarsimp; auto simp: distinct_count_atmost_1)+
-
-    from "2.IH"[unfolded X1, OF refl refl refl] PREMS have
+
+    from "2.IH"[unfolded X1, OF refl refl refl] PREMS have
C[simp]: "complete (from_list (preproc l))" "complete (from_list (preproc r))"
by (auto simp:sorted_Cons sorted_append)
-
+
show ?case
-      apply (auto simp: ins_left ins_right X2)
-      apply (fold from_list_def)
-      apply simp_all
-      using height_if_complete[OF C(1)] height_if_complete[OF C(2)]
+      apply (auto simp: ins_left ins_right X2)
+      apply (fold from_list_def)
+      apply simp_all
+      using height_if_complete[OF C(1)] height_if_complete[OF C(2)]
-  qed
+  qed

-
+
(*  attempt to prove for arbitrary sizes. Stopped at the following lemma for balanced!
lemma
assumes "balanced l"
-    assumes "balanced r"
-    assumes "size r \<le> size l"
-    assumes "size l \<le> size r + 1"
-    shows "balanced \<langle>l,a,r\<rangle>"
+    assumes "balanced r"
+    assumes "size r \<le> size l"
+    assumes "size l \<le> size r + 1"
+    shows "balanced \<langle>l,a,r\<rangle>"
proof -
from assms(3,4) consider "size l = size r" | "size l = size r + 1"
by force
then show ?thesis proof (cases)
case 1
-
+
with balanced_optimal[of l r] balanced_optimal[of r l] assms (1,2)
have "height l = height r" by auto
-
-      then show ?thesis
+
+      then show ?thesis
unfolding balanced_def
apply auto
-        by (metis One_nat_def assms(1) assms(2) balanced_def min_def)
+        by (metis One_nat_def assms(1) assms(2) balanced_def min_def)
next
case 2
-
+
with balanced_optimal[of r l] assms (1,2)
-      have "height r \<le> height l" by auto
+      have "height r \<le> height l" by auto
then show ?thesis
unfolding balanced_def
-        using assms(1,2) unfolding balanced_def
+        using assms(1,2) unfolding balanced_def
apply (auto simp: max_def min_def not_le)
-
-    qed
-
+
+    qed
+
lemma "sorted xs \<Longrightarrow> distinct xs \<Longrightarrow> balanced (from_list (L xs))"
proof (induction xs rule: L.induct)
case 1
then show ?case by (auto simp: from_list_def split:prod.split)
next
case (2 v va)
-
-    obtain l x r where
+
+    obtain l x r where
X1[simp]: "split (v # va) = (l,x,r)"
by (cases "split (v # va)")

@@ -241,45 +241,45 @@
LEN: "length r \<le> length l" "length l \<le> length r + 1"
and U: "v # va = l @ x # r"
by simp_all
-
+
note PREMS = "2.prems"[unfolded U]
-
+
from PREMS have X2: "\<forall>y\<in>set (L l). y<x" "\<forall>y\<in>set (L r). x<y"
by (force simp: sorted_append sorted_Cons)+
-
+
from PREMS(2) have [simp]: "distinct (L l)" "distinct (L r)"
by (clarsimp; auto simp: distinct_count_atmost_1)+
-
-    from "2.IH"[unfolded X1, OF refl refl refl] PREMS have
+
+    from "2.IH"[unfolded X1, OF refl refl refl] PREMS have
"balanced (from_list (L l))" "balanced (from_list (L r))"
by (auto simp:sorted_Cons sorted_append)
-
+
have "size (from_list (L r)) \<le> size (from_list (L l))" "size (from_list (L l)) \<le> size (from_list (L r)) + 1"
using LEN
-
-
-
-
+
+
+
+
show ?case
-      apply (auto simp: ins_left ins_right X2)
-      apply (fold from_list_def)
-
-
+      apply (auto simp: ins_left ins_right X2)
+      apply (fold from_list_def)
+
+
qed
-    apply (auto split: prod.split)
-    apply (auto simp: from_list_def)
-    apply (frule split_lemma(3)[OF sym]; simp)
-    apply (clarsimp simp: sorted_append sorted_Cons ins_left)
-
-
-
-  *)
+    apply (auto split: prod.split)
+    apply (auto simp: from_list_def)
+    apply (frule split_lemma(3)[OF sym]; simp)
+    apply (clarsimp simp: sorted_append sorted_Cons ins_left)
+
+

-(*>*)
-
-(*<*)
+  *)
+
+(*>*)
+
+(*<*)
end
-(*>*)
+(*>*)
text_raw \<open>\blankpage\<close>
--- a/SS18/Exercises/hwsubm/email.log	Mon Jul 09 11:56:29 2018 +0200
+++ b/SS18/Exercises/hwsubm/email.log	Mon Jul 09 11:57:00 2018 +0200
@@ -469,3 +469,51 @@
Do 28. Jun 12:23:50 CEST 2018
/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw10 felix.wielander@tum.de hw10_1_tmpl.thy hw10_2_tmpl.thy
OK
+Fr 6. Jul 11:38:08 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+OK
+Fr 6. Jul 11:38:10 CEST 2018
+OK