corr 11 draft
authorlammich <lammich@in.tum.de>
Mon, 09 Jul 2018 11:57:00 +0200
changeset 69947 cd8eb35f3c38
parent 69946 ed7c67f266ac
child 69948 7c35ab688cb8
corr 11
SS18/Exercises/exam.pdf
SS18/Exercises/exam/Q_Balanced_Insert.thy
SS18/Exercises/hwsubm/email.log
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>  
-    Your task is to specify a function @{term_type preprocess}, 
+  text \<open>
+    Your task is to specify a function @{term_type preprocess},
     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 (simp add: from_list_def)
-      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)]
       by (simp add: ss[OF bst_from_list])
-  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
       by (simp_all add: ss[OF bst_from_list])
-      
-        
-        
-        
+
+
+
+
     show ?case
       apply (simp add: from_list_def)
-      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
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 sabine.rieder@tum.de ex11_tmpl.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 a.putwattana@tum.de hw11.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 mitja.krebs@tum.de ex11_tmpl.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 eric.koepke@tum.de hw11.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 ge72lic@mytum.de ex11.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 felix.wielander@tum.de ex11_tmpl.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 j.gottfriedsen@tum.de hw11.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 max.kirchmeier@tum.de ex11_tmpl.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 martin.rau@tum.de Home11.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 ga96koz@mytum.de ex11_tmpl.thy
+OK
+Fr 6. Jul 11:38:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 daniel.kutasi@mytum.de hw11.thy
+OK
+Fr 6. Jul 11:38:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 s.griebel@tum.de hw11.thy
+OK
+Fr 6. Jul 11:38:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 ga59zew@mytum.de hw11.thy
+OK
+Fr 6. Jul 11:38:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 florian.stamer@tum.de ex11.thy
+OK
+Fr 6. Jul 11:38:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 nick.smith@tum.de HW11.thy
+OK
+Fr 6. Jul 11:39:38 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw11 clemens.jonischkeit@tum.de jonischkeit11.thy
+OK