ex1+2

Binary file SS18/Exercises/ex01.pdf has changed

--- a/SS18/Exercises/ex01/ex01.thy	Thu Apr 12 17:04:19 2018 +0200
+++ b/SS18/Exercises/ex01/ex01.thy	Fri Apr 20 10:47:36 2018 +0200
@@ -6,7 +6,7 @@
 
 
 
-text {* \ExerciseSheet{1}{13.~4.~2017} *}
+text {* \ExerciseSheet{1}{13.~4.~2018} *}
 
 text {*
 Before beginning to solve the exercises, open a new theory file

Binary file SS18/Exercises/ex02.pdf has changed

--- a/SS18/Exercises/ex02/ex02.thy	Thu Apr 12 17:04:19 2018 +0200
+++ b/SS18/Exercises/ex02/ex02.thy	Fri Apr 20 10:47:36 2018 +0200
@@ -6,7 +6,7 @@
 
 
 
-text {* \ExerciseSheet{2}{5.~5.~2017} *}
+text {* \ExerciseSheet{2}{20.~4.~2018} *}
 
 text {* \Exercise{Folding over Trees}
 
@@ -153,15 +153,21 @@
 
 
 text \<open>An experienced functional programmer might also write this function as 
-  @{term [display] \<open>map snd (filter (op= x o fst) ys)\<close>}
+  @{term [display] \<open>map snd (filter (\<lambda>kv. fst kv = x) ys)\<close>}
   
   Show that this specifies the same function:\<close>
 
-lemma "collect x ys = map snd (filter (op= x o fst) ys)"
+lemma "collect x ys = map snd (filter (\<lambda>kv. fst kv = x) ys)"
 (*<*)
   by (induction ys) auto
 (*>*)
 
+text \<open>
+  Note that Isabelle pretty-prints the filter function to \<open>[kv\<leftarrow>ys . fst kv = x]\<close>, 
+  which is just a pretty-printing conversion, but does not change the term in the 
+  underlying logic.
+\<close>
+
 text \<open>When the lists get bigger, efficiency might be a concern. 
   To avoid stack overflows, you might want to specify a tail-recursive version 
   of @{term collect}. The first parameter is the accumulator, that accumulates 
@@ -173,9 +179,22 @@
   Complete the second equation!
 \<close>
 
+(*<*)
+locale foo begin
+(*>*)
 fun collect_tr :: "'a list \<Rightarrow> 'b \<Rightarrow> ('b \<times> 'a) list \<Rightarrow> 'a list"  where
   "collect_tr acc x [] = rev acc"
-| "collect_tr acc x ((k,v)#ys) = (*<*)(if k=x then collect_tr (v#acc) x ys else collect_tr acc x ys)(*>*)"
+| "collect_tr acc x ((k,v)#ys) = undefined"
+(*<*)
+end
+(*>*)
+
+(*<*)
+fun collect_tr :: "'a list \<Rightarrow> 'b \<Rightarrow> ('b \<times> 'a) list \<Rightarrow> 'a list"  where
+  "collect_tr acc x [] = rev acc"
+| "collect_tr acc x ((k,v)#ys) = (if k=x then collect_tr (v#acc) x ys else collect_tr acc x ys)"
+(*>*)
+
 
 text \<open>Show correctness of your tail-recursive version. Hint: Generalization!\<close>