More ex draft
authorlammich <lammich@in.tum.de>
Thu, 06 Jul 2017 14:57:19 +0200
changeset 69828 e59d2c2ee8b2
parent 69827 6280da38ced7
child 69829 6c684a17800e
More ex
Exercises/ex10/sol10.thy
Exercises/hwsubm/09/Biendarra_Julian_julian.biendarra@tum.de_469/SENTMAIL
Exercises/hwsubm/09/Biendarra_Julian_julian.biendarra@tum.de_469/hw09.thy
Exercises/hwsubm/09/Biendarra_Julian_julian.biendarra@tum.de_469/testoutput.html
Exercises/hwsubm/09/Erhard_Julian_ga48kog@mytum.de_477/SENTMAIL
Exercises/hwsubm/09/Erhard_Julian_ga48kog@mytum.de_477/hw09.thy
Exercises/hwsubm/09/Erhard_Julian_ga48kog@mytum.de_477/testoutput.html
Exercises/hwsubm/09/Groer_Markus_markus.grosser@tum.de_463/SENTMAIL
Exercises/hwsubm/09/Groer_Markus_markus.grosser@tum.de_463/hw09.thy
Exercises/hwsubm/09/Groer_Markus_markus.grosser@tum.de_463/testoutput.html
Exercises/hwsubm/09/Haslbeck_Maximilian_max.haslbeck@mytum.de_458/SENTMAIL
Exercises/hwsubm/09/Haslbeck_Maximilian_max.haslbeck@mytum.de_458/ex09.thy
Exercises/hwsubm/09/Haslbeck_Maximilian_max.haslbeck@mytum.de_458/testoutput.html
Exercises/hwsubm/09/Hellauer_Fabian_f.hellauer@tum.de_456/SENTMAIL
Exercises/hwsubm/09/Hellauer_Fabian_f.hellauer@tum.de_456/hw09_new.thy
Exercises/hwsubm/09/Hellauer_Fabian_f.hellauer@tum.de_456/testoutput.html
Exercises/hwsubm/09/Hu_Shuwei_shuwei.hu@tum.de_455/Homework09.thy
Exercises/hwsubm/09/Hu_Shuwei_shuwei.hu@tum.de_455/SENTMAIL
Exercises/hwsubm/09/Hu_Shuwei_shuwei.hu@tum.de_455/testoutput.html
Exercises/hwsubm/09/Hutzler_Matthias_ga95luy@mytum.de_465/SENTMAIL
Exercises/hwsubm/09/Hutzler_Matthias_ga95luy@mytum.de_465/ex09.thy
Exercises/hwsubm/09/Hutzler_Matthias_ga95luy@mytum.de_465/user_error_log.txt
Exercises/hwsubm/09/Kurz_Friedrich_friedrich.kurz@tum.de_468/SENTMAIL
Exercises/hwsubm/09/Kurz_Friedrich_friedrich.kurz@tum.de_468/hw_09.thy
Exercises/hwsubm/09/Kurz_Friedrich_friedrich.kurz@tum.de_468/user_error_log.txt
Exercises/hwsubm/09/Madge_Pimentel_Fabio_fabio.madge@tum.de_445/SENTMAIL
Exercises/hwsubm/09/Madge_Pimentel_Fabio_fabio.madge@tum.de_445/tmpl09.thy
Exercises/hwsubm/09/Oganyan_Levon_levon.oganyan@tum.de_471/SENTMAIL
Exercises/hwsubm/09/Oganyan_Levon_levon.oganyan@tum.de_471/hmw09.thy
Exercises/hwsubm/09/Oganyan_Levon_levon.oganyan@tum.de_471/testoutput.html
Exercises/hwsubm/09/Ouyang_Lena_ga96vup@mytum.de_472/SENTMAIL
Exercises/hwsubm/09/Ouyang_Lena_ga96vup@mytum.de_472/hw09new.thy
Exercises/hwsubm/09/Ouyang_Lena_ga96vup@mytum.de_472/testoutput.html
Exercises/hwsubm/09/Rokopf_Simon_simon.rosskopf@tum.de_467/SENTMAIL
Exercises/hwsubm/09/Rokopf_Simon_simon.rosskopf@tum.de_467/testoutput.html
Exercises/hwsubm/09/Rokopf_Simon_simon.rosskopf@tum.de_467/tmpl09.thy
Exercises/hwsubm/09/Saporta_Antoine_Jacques_antoine.saporta@tum.de_453/SENTMAIL
Exercises/hwsubm/09/Saporta_Antoine_Jacques_antoine.saporta@tum.de_453/hw09.thy
Exercises/hwsubm/09/Saporta_Antoine_Jacques_antoine.saporta@tum.de_453/testoutput.html
Exercises/hwsubm/09/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_466/SENTMAIL
Exercises/hwsubm/09/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_466/testoutput.html
Exercises/hwsubm/09/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_466/tmpl09.thy
Exercises/hwsubm/09/Somogyi_Daniel_daniel.somogyi@tum.de_459/SENTMAIL
Exercises/hwsubm/09/Somogyi_Daniel_daniel.somogyi@tum.de_459/hw09.thy
Exercises/hwsubm/09/Somogyi_Daniel_daniel.somogyi@tum.de_459/testoutput.html
Exercises/hwsubm/09/Stevens_Lukas_lukas.stevens@tum.de_460/Ex09.thy
Exercises/hwsubm/09/Stevens_Lukas_lukas.stevens@tum.de_460/SENTMAIL
Exercises/hwsubm/09/Stevens_Lukas_lukas.stevens@tum.de_460/testoutput.html
Exercises/hwsubm/09/Stwe_Daniel_daniel.stuewe@tum.de_462/HW09b.thy
Exercises/hwsubm/09/Stwe_Daniel_daniel.stuewe@tum.de_462/SENTMAIL
Exercises/hwsubm/09/Stwe_Daniel_daniel.stuewe@tum.de_462/user_error_log.txt
Exercises/hwsubm/09/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_479/SENTMAIL
Exercises/hwsubm/09/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_479/hw09.thy
Exercises/hwsubm/09/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_479/user_error_log.txt
Exercises/hwsubm/09/Wauligmann_Martin_martin.wauligmann@tum.de_475/SENTMAIL
Exercises/hwsubm/09/Wauligmann_Martin_martin.wauligmann@tum.de_475/hw09.thy
Exercises/hwsubm/09/Wauligmann_Martin_martin.wauligmann@tum.de_475/testoutput.html
Exercises/hwsubm/09/meta.csv
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/ex10/sol10.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,181 @@
+(*<*)
+theory sol10
+imports 
+    "../../../Public/Thys/Leftist_Heap"    
+begin
+(*>*)  
+text {* \ExerciseSheet{10}{30.~6.~2017} *}
+
+text \<open>
+  \Exercise{Insert for Leftist Heap}
+
+  \<^item> Define a function to directly insert an element into a leftist heap.
+    Do not construct an intermediate heap like insert via meld does!
+    
+  \<^item> Show that your function is correct
+
+  \<^item> Define a timing function for your insert function, and show that it is 
+    linearly bounded by the rank of the tree.
+\<close>  
+  
+fun lh_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" 
+(*<*)  
+  where
+  "lh_insert x \<langle>\<rangle> = \<langle>1,\<langle>\<rangle>,x,\<langle>\<rangle>\<rangle>"
+| "lh_insert x \<langle>s,l,y,r\<rangle> = (
+    if x\<le>y then node l x (lh_insert y r)
+    else node l y (lh_insert x r)
+)"  
+(*>*)  
+  
+lemma mset_lh_insert: "mset_tree (lh_insert x t) = mset_tree t + {# x #}"
+(*<*)  
+  apply (induction t arbitrary: x)
+  apply (auto simp: node_def)
+  done  
+(*>*)
+  
+lemma "heap t \<Longrightarrow> heap (lh_insert x t)"
+(*<*)  
+  by (induction t arbitrary: x) (auto simp: node_def ball_Un mset_lh_insert)  
+(*>*)
+    
+lemma "ltree t \<Longrightarrow> ltree (lh_insert x t)"    
+(*<*)  
+  apply (induction t arbitrary: x)
+  apply (auto simp: node_def)  
+  done
+(*>*)
+
+    
+fun t_lh_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" 
+(*<*)  
+  where
+  "t_lh_insert x \<langle>\<rangle> = 1"
+| "t_lh_insert x \<langle>s,l,y,r\<rangle> = 1 + (
+    if x\<le>y then t_lh_insert y r
+    else (t_lh_insert x r)
+)"  
+(*>*)
+    
+lemma "t_lh_insert x t \<le> rank t + 1"
+(*<*)  
+  by (induction t arbitrary: x) auto  
+(*>*)
+  
+text \<open>
+  \Exercise{Bootstrapping a Priority Queue}
+
+  Given a generic priority queue implementation with
+  \<open>O(1)\<close> \<open>empty\<close>, \<open>is_empty\<close> operations, \<open>O(f\<^sub>1 n)\<close> insert, 
+  and \<open>O(f\<^sub>2 n)\<close> \<open>get_min\<close> and \<open>del_min\<close> operations.
+
+  Derive an implementation with \<open>O(1)\<close> \<open>get_min\<close>, and the
+  asymptotic complexities of the other operations unchanged!
+
+  Hint: Store the current minimal element! As you know nothing 
+    about \<open>f\<^sub>1\<close> and \<open>f\<^sub>2\<close>, you must not use \<open>get_min/del_min\<close> 
+    in your new \<open>insert\<close> operation, and vice versa!
+\<close>
+
+text \<open>For technical reasons, you have to define the new implementations type 
+      outside the locale!\<close>
+datatype ('a,'s) bs_pq = (*<*)Empty | Heap 'a 's(*>*)
+
+locale Bs_Priority_Queue = 
+  orig: Priority_Queue orig_empty orig_is_empty orig_insert orig_get_min orig_del_min orig_invar orig_mset
+  for orig_empty orig_is_empty orig_insert orig_get_min orig_del_min orig_invar 
+  and orig_mset :: "'s \<Rightarrow> 'a::linorder multiset"
+begin
+  text \<open>In here, the original implementation is available with the prefix \<open>orig\<close>, e.g. \<close>
+  term orig_empty term orig_invar  
+  thm orig.invar_empty  
+  
+  definition empty :: "('a,'s) bs_pq" 
+  (*<*)  
+    where "empty = Empty"
+  (*>*)    
+      
+  fun is_empty :: "('a,'s) bs_pq \<Rightarrow> bool" 
+  (*<*)  
+    where 
+    "is_empty Empty \<longleftrightarrow> True"
+  | "is_empty (Heap _ _) \<longleftrightarrow> False"
+  (*>*)    
+    
+  fun insert :: "'a \<Rightarrow> ('a,'s) bs_pq \<Rightarrow> ('a,'s) bs_pq" 
+  (*<*)  
+    where
+    "insert x Empty = Heap x orig_empty"
+  | "insert x (Heap m h) = (if x<m then Heap x (orig_insert m h) else Heap m (orig_insert x h))"
+  (*>*)    
+    
+  fun get_min :: "('a,'s) bs_pq \<Rightarrow> 'a" 
+  (*<*)  
+    where
+    "get_min (Heap m _) = m"
+  (*>*)    
+
+  fun del_min :: "('a,'s) bs_pq \<Rightarrow> ('a,'s) bs_pq" 
+  (*<*)  
+    where
+    "del_min (Heap m h) = (
+      if orig_is_empty h then Empty
+      else Heap (orig_get_min h) (orig_del_min h)
+      )"
+  (*>*)    
+    
+  fun invar :: "('a,'s) bs_pq \<Rightarrow> bool" 
+  (*<*)  
+    where
+    "invar Empty = True"
+  | "invar (Heap m h) = (orig_invar h \<and> (\<forall>x\<in>#orig_mset h. m\<le>x))"
+  (*>*)    
+    
+  fun mset :: "('a,'s) bs_pq \<Rightarrow> 'a multiset" 
+  (*<*)  
+    where
+    "mset Empty = {#}"
+  | "mset (Heap m h) = add_mset m (orig_mset h)"
+  (*>*)    
+    
+  text \<open>Show that your new implementation satisfies the priority queue interface!\<close>  
+  sublocale Priority_Queue empty is_empty insert get_min del_min invar mset  
+    apply unfold_locales
+  proof goal_cases
+    case 1
+    then show ?case 
+  (*<*)  
+      by (simp add: empty_def)
+  (*>*)    
+  next
+    case (2 q) -- \<open>and so on\<close>
+  (*<*)  
+    then show ?case by (cases q) auto
+  next
+    case (3 q x)
+    then show ?case by (cases q) (auto)
+  next
+    case (4 q)
+    then show ?case by (cases q; auto simp: min_def)
+  next
+    case (5 q)
+    then show ?case 
+      by (cases q; simp add: Min_mset_alt)
+  next
+    case 6
+    then show ?case by (simp add: empty_def)
+  next
+    case (7 q x)
+    then show ?case by (cases q; auto)
+  next
+    case (8 q)
+    then show ?case by (cases q) (auto dest: in_diffD)
+  (*>*)    
+  qed
+end
+  
+    
+(*<*)
+end
+(*>*)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Biendarra_Julian_julian.biendarra@tum.de_469/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+julian.biendarra@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Biendarra_Julian_julian.biendarra@tum.de_469/hw09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,111 @@
+(** Score: 10/10
+*)
+(*<*)
+theory hw09
+  imports "../../Material/Thys/Trie1"
+begin
+(*>*)
+
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>
+
+fun shrunk :: "trie \<Rightarrow> bool" where
+  "shrunk Leaf \<longleftrightarrow> True" |
+  "shrunk (Node b (l,r)) \<longleftrightarrow> (b \<or> l \<noteq> Leaf \<or> r \<noteq> Leaf) \<and> shrunk l \<and> shrunk r"
+
+lemma insert_not_Leaf: "insert ks t \<noteq> Leaf"
+  by (induction t rule: insert.induct) auto
+
+lemma "shrunk Leaf" by simp
+
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+proof (induction t rule: insert.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 b lr)
+  then show ?case by (cases lr) auto
+next
+  case (3 k ks)
+  then show ?case by (auto simp: insert_not_Leaf)
+next
+  case (4 k ks b l r) 
+  then show ?case by (auto simp: insert_not_Leaf)
+qed
+
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+proof (induction t rule: delete2.induct)
+  case (1 ks)
+  then show ?case by simp
+next
+  case (2 ks b l r)
+  then show ?case
+    by (cases ks) auto
+qed
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+    
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI ks LeafI = LeafI" |
+  "deleteI ks (UnaryI b t) = 
+    (case ks of
+      [] \<Rightarrow> UnaryI b t |
+      k#ks' \<Rightarrow> UnaryI b (if k = b then deleteI ks' t else t))" |
+  "deleteI ks (BinaryI b (l,r)) =
+    (case ks of
+      [] \<Rightarrow> BinaryI False (l,r) |
+      k#ks' \<Rightarrow> BinaryI b (if k then (l, deleteI ks' r) else (deleteI ks' l, r)))"
+
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+by (induction t arbitrary: ks rule: abs_itrie.induct) (auto split: list.split)
+
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"  where  
+  "pdelete ks LeafP = LeafP" |
+  "pdelete ks (NodeP ps b (l,r)) =
+    (let n = length ps in
+     if ps = take n ks
+      then case drop n ks of
+        [] \<Rightarrow> NodeP ps False (l, r) |
+        k#ks' \<Rightarrow> if k then NodeP ps b (l, pdelete ks' r) else NodeP ps b (pdelete ks' l, r)
+      else NodeP ps b (l, r))"
+
+lemma "deleteI ks (absI_ptrie t) = absI_ptrie (pdelete ks t)"
+by (induction t arbitrary: ks rule: absI_ptrie.induct) (auto split: list.split)
+    
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Biendarra_Julian_julian.biendarra@tum.de_469/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Erhard_Julian_ga48kog@mytum.de_477/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+ga48kog@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Erhard_Julian_ga48kog@mytum.de_477/hw09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,318 @@
+(** Score: 8/10
+
+  delete on patricia tries missing
+*)
+(*<*)
+theory hw09
+  imports "../fds_ss17/Thys/Trie1"
+begin
+(*>*)  
+text {* \ExerciseSheet{9}{23.~6.~2017} *}
+(*
+text \<open>\Exercise{Union Function on Tries}
+  Define a function to merge two tries and show its correctness
+\<close>  
+fun union :: "trie \<Rightarrow> trie \<Rightarrow> trie" 
+  where "union Leaf t = t" |
+        "union t Leaf = t" |
+        "union (Node b (l1, r1)) (Node c (l2, r2)) = (let l = union l1 l2 in 
+                                                      let r = union r1 r2 in
+                                                         Node (b \<or> c) (l,r))"
+  
+lemma "isin (union a b) x = isin a x \<or> isin b x"
+  apply (induction a b rule: union.induct)
+    apply force
+   apply force
+    apply (auto split:  if_splits)
+  sorry  (** Why did you leave this in? *)
+*)    
+text \<open>
+  \Exercise{Intermediate Abstraction Level for Patricia Tries}
+
+  We introduce an abstraction level in between tries and Patricia tries:
+  A node with only a single non-leaf successor is represented as an unary node.
+
+  Via unary nodes, this implementation already introduces a notion of common prefix,
+  but does not yet summarize runs of multiple prefixes into a list.
+\<close>
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+text \<open>Refine the union function to intermediate tries\<close>
+fun unionI :: "itrie \<Rightarrow> itrie \<Rightarrow> itrie" 
+  where "unionI LeafI t = t" |
+        "unionI t LeafI = t" |
+        "unionI (UnaryI True t1) (UnaryI True t2) = UnaryI True (unionI t1 t2)"|
+        "unionI (UnaryI False t1) (UnaryI False t2) = UnaryI False (unionI t1 t2)" |
+        "unionI (UnaryI False t1) (UnaryI True t2) = BinaryI False (t1, t2)" |
+        "unionI (UnaryI True t1) (UnaryI False t2) = BinaryI False (t2, t1)" |
+        "unionI (UnaryI True t1) (BinaryI b (t2, t3)) = BinaryI b (t2, unionI t1 t3)" |
+        "unionI (UnaryI False t1) (BinaryI b (t2, t3)) = BinaryI b (unionI t1 t2, t3)" |
+        "unionI (BinaryI b (t1, t2)) (UnaryI True t3) = BinaryI b (t1, unionI t2 t3)" |
+        "unionI (BinaryI b (t1, t2)) (UnaryI False t3) = BinaryI b (unionI t1 t3, t2)" |
+        "unionI (BinaryI v1 (l1,r1)) (BinaryI v2 (l2, r2)) = BinaryI (v1 \<or> v2) (unionI l1 l2, unionI r1 r2)"
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+  
+(*
+text \<open>Warmup: Show that abstracting Patricia tries over intermediate 
+  tries to tries is the same as abstracting directly to tries.\<close>  
+lemma "abs_itrie o absI_ptrie = abs_ptrie"
+sorry
+*)  
+text \<open>Refine the union function to Patricia tries.
+
+  Hint: First figure out how a Patricia trie that 
+    correspond to a leaf/unary/binary node looks like. 
+    Then translate @{const \<open>unionI\<close>} equation by equation!
+
+  More precisely, try to find terms \<open>unaryP\<close> and \<open>binaryP\<close> such that
+    @{term [display] "absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"}
+    @{term [display] "absI_ptrie (binaryP v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"}
+
+  You will encounter a small problem with \<open>unaryP\<close>. Which one?
+\<close>
+  
+    
+fun unionP :: "ptrie \<Rightarrow> ptrie \<Rightarrow> ptrie" 
+  where "unionP _ _ = undefined"
+(*  
+lemma "absI_ptrie (unionP t\<^sub>1 t\<^sub>2) = unionI (absI_ptrie t\<^sub>1) (absI_ptrie t\<^sub>2)"
+  sorry
+*)    
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" where 
+  "shrunk Leaf = True" |
+  "shrunk (Node False (Leaf, Leaf)) = False" |
+  "shrunk (Node _ (t1, t2)) = (shrunk t1 \<and> shrunk t2)"
+
+lemma "shrunk Leaf"
+  apply simp
+  done
+
+lemma shrunk_rec: "shrunk (Node b (t1, t2)) \<Longrightarrow> shrunk t1 \<and> shrunk t2"
+  using shrunk.elims(2) by blast
+    
+lemma shr_Node: "shrunk (Node False (t1, t2)) \<Longrightarrow> shrunk (Node True (t1,t2))"
+  using shrunk.simps(3) shrunk_rec by blast
+    (* longer proof no longer needed:
+proof -
+  assume a: "shrunk (Node False (t1, t2))"
+  have "(t1, t2) = (Leaf, Leaf) \<or> t1 \<noteq> Leaf \<or> t2 \<noteq> Leaf" by simp
+  then show ?thesis
+  proof 
+    assume "(t1, t2) = (Leaf, Leaf)"
+    then show ?thesis by simp
+  next
+    assume "t1 \<noteq> Leaf \<or> t2 \<noteq> Leaf" 
+    then show ?thesis 
+    proof 
+      assume nl: "t1 \<noteq> Leaf"
+      have "shrunk t1 \<and> shrunk t2" using shrunk.elims(2) a nl by blast
+      from this have "shrunk (Node True (t1, t2))" by simp
+      from this show ?thesis by simp
+    next
+      assume nl: "t2 \<noteq> Leaf"
+      have "shrunk t1 \<and> shrunk t2" using shrunk.elims(2) a nl by blast
+      from this have "shrunk (Node True (t1, t2))" by simp
+      from this show ?thesis by simp
+    qed
+  qed
+qed
+*)
+  
+lemma insert_eq_Node: "\<exists> a b .insert ks t = Node a b"
+  by (metis isin.simps(1) isin_insert shrunk.elims(2) shrunk.elims(3))
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+proof (induction t  rule: insert.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 b lr)
+  then show ?case  by (metis insert.simps(2) prod.collapse shr_Node)
+next
+  case (3 k ks)
+  have "k \<or> \<not> k" by simp
+  then show ?case proof 
+    assume "k"
+    have rp: "shrunk (insert ks Leaf)" using `k` 3 by simp
+    have "shrunk (insert (k # ks) Leaf) = shrunk (Node False (if k then (Leaf, insert ks Leaf)
+                   else (insert ks Leaf, Leaf)))" by simp
+    also have "... = shrunk (Node False (Leaf, insert ks Leaf))" using `k` by simp
+    also have "... = shrunk Leaf \<and> shrunk (insert ks Leaf)" using insert_eq_Node[of ks Leaf] rp by auto
+    also have "... = True" using rp by auto
+    finally show ?case by simp
+  next
+    assume "\<not> k"
+    have rp: "shrunk (insert ks Leaf)" using `\<not> k` 3 by simp
+    have "shrunk (insert (k # ks) Leaf) = shrunk (Node False (if k then (Leaf, insert ks Leaf)
+                   else (insert ks Leaf, Leaf)))" by simp
+    also have "... = shrunk (Node False (insert ks Leaf, Leaf))" using `\<not> k` by simp
+    also have "... = shrunk Leaf \<and> shrunk (insert ks Leaf)" using insert_eq_Node[of ks Leaf] rp by auto
+    also have "... = True" using rp by auto
+    finally show ?case by simp
+  qed
+ next
+  case (4 k ks b l r)
+  have "k \<or> \<not> k" by simp
+  then show ?case proof
+    assume "k"
+    have l: "shrunk l " using 4 shrunk_rec[of b l r] by simp
+    have r: "shrunk r" using 4 shrunk_rec[of b l r] by simp
+    from this have rp: "shrunk (insert ks r)" using `k` 4 by simp
+    
+    have "shrunk (insert (k # ks) (Node b (l, r))) = shrunk(  Node b (if k then (l, insert ks r)
+               else (insert ks l, r)))" by simp
+    also have "... = shrunk (Node b (l, insert ks r))" using `k` by simp
+    also have "... = (shrunk l \<and> shrunk (insert ks r))" using insert_eq_Node[of ks r] rp by auto
+    also have "... = True " using shrunk_rec[of b l "insert ks r"] l rp by auto
+    finally show ?case by simp
+   next
+    assume "\<not>k"
+    have r: "shrunk r" using 4 shrunk_rec[of b l r] by simp
+    have l: "shrunk l" using 4 shrunk_rec[of b l r] by simp
+    from this have rp: "shrunk (insert ks l)" using `\<not>k` 4 by simp
+    
+    have "shrunk (insert (k # ks) (Node b (l, r))) = shrunk(  Node b (if k then (l, insert ks r)
+               else (insert ks l, r)))" by simp
+    also have "... = shrunk (Node b (insert ks l,  r))" using `\<not>k` by simp
+    also have "... = (shrunk r \<and> shrunk (insert ks l))" using insert_eq_Node[of ks l] rp by auto
+    also have "... = True " using shrunk_rec[of b "insert ks l" r] r rp by auto
+    finally show ?case by auto     
+  qed
+qed
+  
+lemma shrunk_node: "shrunk t1 \<Longrightarrow> shrunk t2 \<Longrightarrow> shrunk (node b (t1, t2))"
+  apply auto
+  using shrunk.elims(3) apply fastforce
+  using shrunk.elims(3) apply fastforce
+  done
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+proof (induction t rule: delete2.induct)
+  case (1 ks)
+  then show ?case by simp
+next
+  case (2 ks b l r)
+  then show ?case proof (cases ks)
+    case Nil
+    have lr: "shrunk l \<and> shrunk r" using shrunk_rec[of b l r] 2 by simp
+        
+    have "shrunk (delete2 ks (Node b (l, r))) = shrunk (node False (l,r)) " using 2 Nil by simp
+    also have "... =  True" using lr shrunk_node[of l r False] by simp
+    finally show ?thesis by simp
+  next
+    case (Cons k ks')
+    have lr: "shrunk l \<and> shrunk r" using shrunk_rec[of b l r] 2 by simp
+    have "k \<or> \<not> k" by simp
+    then show ?thesis proof
+      assume "k"
+      have sr: "shrunk (delete2 ks' r)" using 2 Cons lr `k` by simp
+      have "shrunk (delete2 ks (Node b (l, r))) =  shrunk (node b (if k then (l, delete2 ks' r) else (delete2 ks' l, r)))" using 2 Cons by simp
+      also have "... = shrunk (node b (l, delete2 ks' r))" using `k` by simp
+      also have "... = True " using sr shrunk_node[of l "delete2 ks' r " b] lr by simp
+      finally show ?thesis by simp
+     next
+      assume "\<not> k"
+      have sl: "shrunk (delete2 ks' l)" using 2 Cons lr `\<not>k` by simp
+      have "shrunk (delete2 ks (Node b (l, r))) =  shrunk (node b (if k then (l, delete2 ks' r) else (delete2 ks' l, r)))" using 2 Cons by simp
+      also have "... = shrunk (node b (delete2 ks' l,  r))" using `\<not>k` by simp
+      also have "... = True " using sl shrunk_node[of "delete2 ks' l " r b] lr by simp
+      finally show ?thesis by simp
+    qed 
+  qed
+qed
+  
+  
+    
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+    
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI ks LeafI = LeafI" |
+  "deleteI [] (UnaryI b t) = UnaryI b t " |
+  "deleteI (k#ks) (UnaryI b t) = (if k=b then UnaryI b (deleteI ks t) else UnaryI b t)" |
+  "deleteI ks (BinaryI b (l,r)) =
+   (case ks of
+      [] \<Rightarrow> BinaryI False (l,r) |
+      k#ks' \<Rightarrow> BinaryI b (if k then (l, deleteI ks' r) else (deleteI ks' l, r)))"
+
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)" 
+proof (induction ks t rule: deleteI.induct)
+  case (1 ks)
+  then show ?case by simp
+next
+  case (2 b t)
+  have "b \<or> \<not> b" by simp
+  then show ?case proof (*alternative : by fastforce*) 
+    assume "b"
+    have a: "abs_itrie (deleteI [] (UnaryI b t)) = abs_itrie (UnaryI b t)" by simp
+    also have b:"... = Node False (Leaf, abs_itrie t)" using `b` by simp
+    have c: "delete [] (abs_itrie (UnaryI b t)) = delete [] (Node False (Leaf, abs_itrie t))" using `b` by simp
+    also have d: "... = Node False (Leaf, abs_itrie t)" by simp
+    from a b c d show ?thesis by simp
+  next 
+     assume "\<not>b"
+    have a: "abs_itrie (deleteI [] (UnaryI b t)) = abs_itrie (UnaryI b t)" by simp
+    also have b:"... = Node False (abs_itrie t, Leaf)" using `\<not>b` by simp
+    have c: "delete [] (abs_itrie (UnaryI b t)) = delete [] (Node False(abs_itrie t, Leaf))" using `\<not>b` by simp
+    also have d: "... = Node False (abs_itrie t, Leaf)" by simp
+    from a b c d show ?thesis by simp
+   qed
+next
+  case (3 k ks b t)
+  then show ?case by auto
+next
+  case (4 ks b l r)
+  then show ?case proof (cases ks)
+    case Nil
+    then show ?thesis by simp
+  next
+    case (Cons k ks')
+    then show ?thesis by (simp add: "4.IH"(1) "4.IH"(2))
+  qed 
+qed
+  
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete _ _ = undefined"
+  
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"  sorry
+    
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Erhard_Julian_ga48kog@mytum.de_477/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Groer_Markus_markus.grosser@tum.de_463/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+markus.grosser@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Groer_Markus_markus.grosser@tum.de_463/hw09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,187 @@
+(** Score: 10/10
+*)
+(*<*)
+theory hw09
+  imports "../../repo/Thys/Trie1"
+begin
+(*>*)
+text {* \ExerciseSheet{9}{23.~6.~2017} *}
+
+text \<open>\Exercise{Union Function on Tries}
+  Define a function to merge two tries and show its correctness
+\<close>
+fun union :: "trie \<Rightarrow> trie \<Rightarrow> trie" where
+  "union (Node b\<^sub>1 (l\<^sub>1, r\<^sub>1)) (Node b\<^sub>2 (l\<^sub>2, r\<^sub>2)) =
+    Node (b\<^sub>1 \<or> b\<^sub>2) (union l\<^sub>1 l\<^sub>2, union r\<^sub>1 r\<^sub>2)"
+| "union Leaf t = t"
+| "union t Leaf = t"
+
+lemma [simp]: "union t Leaf = t" by (cases t) auto
+
+lemma "isin (union a b) x = isin a x \<or> isin b x"
+  by (induction arbitrary: x rule: union.induct) (auto split: list.splits)
+
+fun inter :: "trie \<Rightarrow> trie \<Rightarrow> trie" where
+  "inter (Node b\<^sub>1 (l\<^sub>1, r\<^sub>1)) (Node b\<^sub>2 (l\<^sub>2, r\<^sub>2)) =
+    Node (b\<^sub>1 \<and> b\<^sub>2) (inter l\<^sub>1 l\<^sub>2, inter r\<^sub>1 r\<^sub>2)"
+| "inter Leaf t = Leaf"
+| "inter t Leaf = Leaf"
+
+lemma "inter t Leaf = Leaf" by (cases t) auto
+
+lemma "isin (inter a b) x = (isin a x \<and> isin b x)"
+  by (induction arbitrary: x rule: inter.induct) (auto split: list.splits)
+
+text \<open>
+  \Exercise{Intermediate Abstraction Level for Patricia Tries}
+
+  We introduce an abstraction level in between tries and Patricia tries:
+  A node with only a single non-leaf successor is represented as an unary node.
+
+  Via unary nodes, this implementation already introduces a notion of common prefix,
+  but does not yet summarize runs of multiple prefixes into a list.
+\<close>
+
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial)
+
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+fun unaryP :: "bool \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+  "unaryP k (NodeP ks v lr) = NodeP (k#ks) v lr"
+| "unaryP _ LeafP = undefined"
+
+lemma absI_ptrie_unaryP: "t \<noteq> LeafP \<Longrightarrow> absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"
+  by (cases t) auto
+
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a
+  ``shrunk'' - property on tries. Identify this property, define a predicate
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>
+
+fun shrunk :: "trie \<Rightarrow> bool" where
+  "shrunk (Node False (Leaf, Leaf)) = False"
+| "shrunk (Node _ (l, r)) = (shrunk l \<and> shrunk r)"
+| "shrunk Leaf = True"
+
+lemma "shrunk Leaf" by simp
+
+lemma shrunk_lr: "shrunk (Node b (l, r)) \<Longrightarrow> shrunk l \<and> shrunk r"
+  by (cases b, auto, cases l, auto, cases r, auto)
+
+lemma insert_ne_Leaf: "insert ks t \<noteq> Leaf"
+  by (induction ks t rule: insert.induct) auto
+
+lemma shrunk_nonleaf: "\<lbrakk>shrunk l; shrunk r; l \<noteq> Leaf \<or> r \<noteq> Leaf\<rbrakk> \<Longrightarrow> shrunk (Node b (l, r))"
+  by (auto elim: shrunk.elims)
+
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+proof (induction t rule: insert.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 b lr)
+  then show ?case by (auto elim: shrunk.elims)
+next
+  case (3 k ks)
+  then have "shrunk (insert ks Leaf)" by blast
+  moreover have "insert (k#ks) Leaf \<noteq> Node False (Leaf, Leaf)"
+    using insert_ne_Leaf[of ks Leaf] by simp
+  ultimately show ?case by (auto elim: shrunk.elims)
+next
+  case (4 k ks b l r)
+  then obtain l' r' where result: "Node b (l', r') = insert (k#ks) (Node b (l, r))" by force
+  then have "shrunk l" "shrunk r" by (auto simp: shrunk_lr[OF "4.prems"])
+  then show ?case proof (cases k)
+    case True
+    then have "shrunk l'" using result by (auto simp: \<open>shrunk l\<close>)
+    moreover have "r' \<noteq> Leaf" using result by (auto simp: insert_ne_Leaf[of ks r] True)
+    ultimately show ?thesis using result 4 by (auto simp: True \<open>shrunk r\<close> elim: shrunk.elims)
+  next
+    case False
+    then have "shrunk r'" using result by (auto simp: \<open>shrunk r\<close>)
+    moreover have "l' \<noteq> Leaf" using result by (auto simp: insert_ne_Leaf[of ks l] False)
+    ultimately show ?thesis using result 4 by (auto simp: False \<open>shrunk l\<close> elim: shrunk.elims)
+  qed
+qed
+
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+proof (induction t rule: delete2.induct)
+  case (1 ks)
+  then show ?case by simp
+next
+  case (2 ks b l r)
+  have "shrunk l" "shrunk r" by (auto simp: shrunk_lr[OF "2.prems"])
+  show ?case proof (cases ks)
+    case Nil
+    then show ?thesis by (auto simp: shrunk_nonleaf[OF \<open>shrunk l\<close> \<open>shrunk r\<close>])
+  next
+    case (Cons x xs)
+    then show ?thesis using 2 by (auto simp: \<open>shrunk l\<close> \<open>shrunk r\<close> shrunk_nonleaf)
+  qed
+qed
+
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down
+  to Patricia tries.
+\<close>
+
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI"
+| "deleteI (True#ks) (UnaryI True r) = UnaryI True (deleteI ks r)"
+| "deleteI (False#ks) (UnaryI False l) = UnaryI False (deleteI ks l)"
+| "deleteI _ (UnaryI b t) = UnaryI b t"
+| "deleteI [] (BinaryI _ t) = BinaryI False t"
+| "deleteI (True#ks) (BinaryI b (l, r)) = BinaryI b (l, deleteI ks r)"
+| "deleteI (False#ks) (BinaryI b (l, r)) = BinaryI b (deleteI ks l, r)"
+
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+proof (induction rule: deleteI.induct)
+  case ("4_1" b t)
+  then show ?case by (cases b) auto
+qed auto
+
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+  "pdelete _ LeafP = LeafP"
+| "pdelete (True#ks) (NodeP (True#ns) b lr) = unaryP True (pdelete ks (NodeP ns b lr))"
+| "pdelete (False#ks) (NodeP (False#ns) b lr) = unaryP False (pdelete ks (NodeP ns b lr))"
+| "pdelete _ (NodeP (n#ns) b lr) = NodeP (n#ns) b lr"
+| "pdelete [] (NodeP [] _ lr) = NodeP [] False lr"
+| "pdelete (True#ks) (NodeP [] b (l, r)) = NodeP [] b (l, pdelete ks r)"
+| "pdelete (False#ks) (NodeP [] b (l, r)) = NodeP [] b (pdelete ks l, r)"
+
+lemma unaryP_nonleaf: "t \<noteq> LeafP \<Longrightarrow> unaryP k t \<noteq> LeafP" using unaryP.elims by blast
+
+lemma pdelete_nonleaf: "t \<noteq> LeafP \<Longrightarrow> pdelete ks t \<noteq> LeafP"
+  by (induction ks t rule: pdelete.induct) (auto simp: unaryP_nonleaf)
+
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  by (induction rule: pdelete.induct) (auto simp: pdelete_nonleaf absI_ptrie_unaryP)
+
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Groer_Markus_markus.grosser@tum.de_463/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Haslbeck_Maximilian_max.haslbeck@mytum.de_458/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+max.haslbeck@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Haslbeck_Maximilian_max.haslbeck@mytum.de_458/ex09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,163 @@
+(** Score: 10/10
+*)
+(*<*)
+theory ex09
+  imports "../Thys/Trie1"
+begin
+(*>*)  
+text {* \ExerciseSheet{9}{23.~6.~2017} *}
+
+text \<open>\Exercise{Union Function on Tries}
+  Define a function to merge two tries and show its correctness
+\<close>  
+fun union :: "trie \<Rightarrow> trie \<Rightarrow> trie" 
+  where "union _ _ = undefined"
+  
+    
+text \<open>
+  \Exercise{Intermediate Abstraction Level for Patricia Tries}
+
+  We introduce an abstraction level in between tries and Patricia tries:
+  A node with only a single non-leaf successor is represented as an unary node.
+
+  Via unary nodes, this implementation already introduces a notion of common prefix,
+  but does not yet summarize runs of multiple prefixes into a list.
+\<close>
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+text \<open>Refine the union function to intermediate tries\<close>
+fun unionI :: "itrie \<Rightarrow> itrie \<Rightarrow> itrie" 
+  where "unionI _ _ = undefined"
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+  
+
+text \<open>Warmup: Show that abstracting Patricia tries over intermediate 
+  tries to tries is the same as abstracting directly to tries.\<close>  
+  
+  
+text \<open>Refine the union function to Patricia tries.
+
+  Hint: First figure out how a Patricia trie that 
+    correspond to a leaf/unary/binary node looks like. 
+    Then translate @{const \<open>unionI\<close>} equation by equation!
+
+  More precisely, try to find terms \<open>unaryP\<close> and \<open>binaryP\<close> such that
+    @{term [display] "absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"}
+    @{term [display] "absI_ptrie (binaryP v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"}
+
+  You will encounter a small problem with \<open>unaryP\<close>. Which one?
+\<close>
+  
+    
+fun unionP :: "ptrie \<Rightarrow> ptrie \<Rightarrow> ptrie" 
+  where "unionP _ _ = undefined"
+    
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" where
+  "shrunk Leaf \<longleftrightarrow> True" |
+  "shrunk (Node b lr) \<longleftrightarrow> (if \<not> b \<and> lr = (Leaf, Leaf) then False else shrunk (fst lr) \<and> shrunk (snd lr))"
+  (** Umständlich ... 
+  | "shrunk (Node v (l,r)) \<longleftrightarrow> shrunk l \<and> shrunk r \<and> (\<not>v \<longrightarrow> (l,r)\<noteq>(Leaf,Leaf))"
+  *)
+
+lemma "shrunk Leaf"
+  by simp
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  apply(induction ks t rule: insert.induct)
+     apply(simp)
+    apply(simp split: if_splits)
+   apply(auto)[1]
+   apply (metis isin.simps(1) isin_insert)
+  apply(auto split: if_splits simp add: isin_insert)[1]
+       apply (metis isin.simps(1) isin_insert)
+       apply (metis isin.simps(1) isin_insert)
+  done
+    
+    
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  apply(induction ks t rule: delete2.induct)
+  by (auto  split: if_splits list.splits)
+
+
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+    term delete
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI ks LeafI = LeafI" |
+  "deleteI ks (UnaryI b i) =
+   (case ks of
+      [] \<Rightarrow> UnaryI b i |
+      k#ks' \<Rightarrow> UnaryI b (if b = k then deleteI ks' i else i))" |
+  "deleteI ks (BinaryI b (l,r)) =
+     (case ks of
+       [] \<Rightarrow> BinaryI False (l,r) |
+       k#ks' \<Rightarrow> BinaryI b (if k then (l, deleteI ks' r) else (deleteI ks' l, r)))"
+
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  apply(induction ks t rule: deleteI.induct)
+    apply(simp)
+        apply(case_tac b)
+    apply(force split: if_splits list.splits)+
+    done
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where
+  "pdelete ks LeafP = LeafP" |
+  "pdelete ks (NodeP ps b (l,r)) =
+  (let n = length ps in
+   if ps = take n ks
+   then case drop n ks 
+     of [] \<Rightarrow> (NodeP ps False (l,r)) |
+        k#ks' \<Rightarrow> (NodeP ps b (if k then (l, pdelete ks' r) else (pdelete ks' l, r)))
+   else (NodeP ps b (l,r)))"
+  
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  proof(induction t arbitrary: ks rule: absI_ptrie.induct)
+    case 1
+    then show ?case by simp
+  next
+    case (2 v l r)
+    then show ?case by (auto split: if_splits list.splits)
+  next
+    case (3 x xs v l r)
+    from 3[symmetric] show ?case by (simp split: if_splits list.splits)
+  qed
+    
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Haslbeck_Maximilian_max.haslbeck@mytum.de_458/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hellauer_Fabian_f.hellauer@tum.de_456/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+f.hellauer@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hellauer_Fabian_f.hellauer@tum.de_456/hw09_new.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,126 @@
+(** Score: 10/10
+*)
+theory hw09_new
+  imports "../../Material/Thys/Trie1"
+begin
+
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+ 
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" where
+  "shrunk Leaf \<longleftrightarrow> True" |
+  "shrunk (Node True (l,r)) \<longleftrightarrow> shrunk l \<and> shrunk r" |
+  "shrunk (Node False (l,r)) \<longleftrightarrow> (l\<noteq>Leaf \<or> r\<noteq>Leaf) \<and> shrunk l \<and> shrunk r"
+
+lemma "shrunk Leaf" by simp
+
+lemma ins_no_Leaf: "insert ks t \<noteq> Leaf"
+  by (cases ks; cases t) auto
+
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  apply (induction ks t rule: insert.induct)
+     apply (auto elim: shrunk.elims simp: ins_no_Leaf)
+  done
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  apply (induction ks t rule: delete2.induct)
+   apply (auto elim: shrunk.elims split: list.split)
+    done
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+    
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI" |
+  "deleteI [] (UnaryI b lr) = UnaryI b lr" |
+  "deleteI (False#ks) (UnaryI False t) = UnaryI False (deleteI ks t)" |
+  "deleteI (False#ks) (UnaryI True t) = UnaryI True t" |
+  "deleteI (True#ks) (UnaryI False t) = UnaryI False t" |
+  "deleteI (True#ks) (UnaryI True t) = UnaryI True (deleteI ks t)" |
+  "deleteI ks (BinaryI b (l,r)) = (case ks of
+    [] \<Rightarrow> BinaryI False (l,r) |
+    k#ks \<Rightarrow> BinaryI b (if k then (l,deleteI ks r) else (deleteI ks l, r)))"
+
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  apply (induction ks t rule: deleteI.induct)
+        apply (auto split: list.split)
+  apply (case_tac b)
+   apply auto
+    done
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete ks LeafP = LeafP" |
+  "pdelete ks (NodeP ps b (l,r)) = (
+    if take (length ps) ks = ps
+    then case drop (length ps) ks of
+      [] \<Rightarrow> NodeP ps False (l,r) |
+      k#ks' \<Rightarrow> NodeP ps b (if k then (l, pdelete ks' r) else (pdelete ks' l, r))
+    else NodeP ps b (l,r))"
+  
+lemma [simp]: "deleteI ps (absI_ptrie (NodeP ps b (l, r))) = absI_ptrie (NodeP ps False (l,r))"
+  apply (induction ps)
+   apply simp_all
+    by (metis deleteI.simps(3) deleteI.simps(6))
+  
+lemma [simp]: "take (length ps) ks \<noteq> ps
+       \<Longrightarrow> deleteI ks (absI_ptrie (NodeP ps b (l, r))) = absI_ptrie (NodeP ps b (l, r))"
+  apply (induction "NodeP ps b (l, r)" arbitrary: ps ks rule: absI_ptrie.induct)
+   apply (auto split: list.splits)
+  by (smt append_Cons append_take_drop_id deleteI.simps(2) deleteI.simps(3) deleteI.simps(4) deleteI.simps(5) deleteI.simps(6) drop_Suc take_Suc)
+
+lemma step_True: "absI_ptrie (pdelete ks' r) = deleteI ks' (absI_ptrie r)
+    \<Longrightarrow> deleteI (ps @ True # ks') (absI_ptrie (NodeP ps b (l, r))) = absI_ptrie (NodeP ps b (l, pdelete ks' r))"
+  apply (induction ps)
+   apply simp_all
+    by (metis deleteI.simps(3) deleteI.simps(6))
+
+lemma step_False: "absI_ptrie (pdelete ks' l) = deleteI ks' (absI_ptrie l)
+    \<Longrightarrow> deleteI (ps @ False # ks') (absI_ptrie (NodeP ps b (l, r))) = absI_ptrie (NodeP ps b (pdelete ks' l, r))"
+  apply (induction ps)
+   apply simp_all
+    by (metis deleteI.simps(3) deleteI.simps(6))
+
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  apply (induction ks t rule: pdelete.induct)
+   apply (auto split: list.splits)
+   apply (metis append_take_drop_id step_True)
+  apply (metis append_take_drop_id step_False)
+    done
+    
+end
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hellauer_Fabian_f.hellauer@tum.de_456/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hu_Shuwei_shuwei.hu@tum.de_455/Homework09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,250 @@
+(** Score: 10/10
+*)
+theory Homework09
+  imports Main
+begin
+  
+  (* >>>>>>> Trie1.thy >>>>>>> *)
+  
+lemma [simp]: "(\<forall>x. x \<noteq> y) = False"
+  by blast
+    
+hide_const (open) insert
+  
+declare Let_def[simp]
+  
+  
+subsection "Trie"
+  
+datatype trie = Leaf | Node bool "trie * trie"
+  
+fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
+  "isin Leaf ks = False" |
+  "isin (Node b (l,r)) ks =
+   (case ks of
+      [] \<Rightarrow> b |
+      k#ks \<Rightarrow> isin (if k then r else l) ks)"
+  
+fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+  "insert [] Leaf = Node True (Leaf,Leaf)" |
+  "insert [] (Node b lr) = Node True lr" |
+  "insert (k#ks) Leaf =
+  Node False (if k then (Leaf, insert ks Leaf)
+                   else (insert ks Leaf, Leaf))" |
+  "insert (k#ks) (Node b (l,r)) =
+  Node b (if k then (l, insert ks r)
+               else (insert ks l, r))"
+  
+lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
+  apply(induction as t arbitrary: bs rule: insert.induct)
+  apply (auto split: list.splits)
+  done
+    
+text \<open>A simple implementation of delete; does not shrink the trie!\<close>
+  
+fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+  "delete ks Leaf = Leaf" |
+  "delete ks (Node b (l,r)) =
+   (case ks of
+      [] \<Rightarrow> Node False (l,r) |
+      k#ks' \<Rightarrow> Node b (if k then (l, delete ks' r) else (delete ks' l, r)))"
+  
+lemma "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
+  apply(induction as t arbitrary: bs rule: delete.induct)
+  apply (auto split: list.splits)
+  done
+    
+fun node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
+  "node b lr = (if \<not> b \<and> lr = (Leaf,Leaf) then Leaf else Node b lr)"
+  
+fun delete2 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+  "delete2 ks Leaf = Leaf" |
+  "delete2 ks (Node b (l,r)) =
+   (case ks of
+      [] \<Rightarrow> node False (l,r) |
+      k#ks' \<Rightarrow> node b (if k then (l, delete2 ks' r) else (delete2 ks' l, r)))"
+  
+lemma "isin (delete2 as t) bs = isin (delete as t) bs"
+  apply(induction as t arbitrary: bs rule: delete2.induct)
+  apply simp
+  apply (force split: list.splits)
+  done
+    
+    
+subsection "Patricia Trie"
+  
+datatype ptrie = LeafP | NodeP "bool list" bool "ptrie * ptrie"
+  
+fun isinP :: "ptrie \<Rightarrow> bool list \<Rightarrow> bool" where
+  "isinP LeafP ks = False" |
+  "isinP (NodeP ps b (l,r)) ks =
+  (let n = length ps in
+   if ps = take n ks
+   then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (if k then r else l) ks'
+   else False)"
+  
+fun split where
+  "split [] ys = ([],[],ys)" |
+  "split xs [] = ([],xs,[])" |
+  "split (x#xs) (y#ys) =
+  (if x\<noteq>y then ([],x#xs,y#ys)
+   else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
+  
+fun insertP :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+  "insertP ks LeafP  = NodeP ks True (LeafP,LeafP)" |
+  "insertP ks (NodeP ps b (l,r)) =
+  (case split ks ps of
+     (qs,k#ks',p#ps') \<Rightarrow>
+       let tp = NodeP ps' b (l,r); tk = NodeP ks' True (LeafP,LeafP) in
+       NodeP qs False (if k then (tp,tk) else (tk,tp)) |
+     (qs,k#ks',[]) \<Rightarrow>
+       NodeP ps b (if k then (l, insertP ks' r) else (insertP ks' l, r)) |
+     (qs,[],p#ps') \<Rightarrow>
+       let t = NodeP ps' b (l,r) in
+       NodeP qs True (if p then (LeafP,t) else (t,LeafP)) |
+     (qs,[],[]) \<Rightarrow> NodeP ps True (l,r))"
+  
+fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+  "prefix_trie [] t = t" |
+  "prefix_trie (k#ks) t =
+  (let t' = prefix_trie ks t in Node False (if k then (Leaf,t') else (t',Leaf)))"
+  
+fun abs_ptrie :: "ptrie \<Rightarrow> trie" where
+  "abs_ptrie LeafP = Leaf" |
+  "abs_ptrie (NodeP ps b (l,r)) = prefix_trie ps (Node b (abs_ptrie l, abs_ptrie r))"
+  
+lemma isin_prefix_trie: "isin (prefix_trie ps t) ks =
+ (length ks \<ge> length ps \<and>
+  (let n = length ps in ps = take n ks \<and> isin t (drop n ks)))"
+  apply(induction ps arbitrary: ks)
+  apply(auto split: list.split)
+  done
+    
+lemma isinP: "isinP t ks = isin (abs_ptrie t) ks"
+  apply(induction t arbitrary: ks rule: abs_ptrie.induct)
+  apply(auto simp: isin_prefix_trie split: list.split)
+  using nat_le_linear apply force
+  using nat_le_linear apply force
+  done
+    
+lemma prefix_trie_Leafs: "prefix_trie ks (Node True (Leaf,Leaf)) = insert ks Leaf"
+  apply(induction ks)
+  apply auto
+  done
+    
+lemma insert_prefix_trie_same:
+  "insert ps (prefix_trie ps (Node b lr)) = prefix_trie ps (Node True lr)"
+  apply(induction ps)
+  apply auto
+  done
+    
+lemma insert_append: "insert (ks @ k # ks') (prefix_trie ks (Node b (t1,t2))) =
+  prefix_trie ks (Node b (if k then (t1, insert ks' t2) else (insert ks' t1, t2)))"
+  apply(induction ks)
+  apply auto
+  done
+    
+lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
+  apply(induction ps)
+  apply auto
+  done
+    
+lemma split_if: "split ks ps = (qs, ks', ps') \<Longrightarrow>
+  ks = qs @ ks' \<and> ps = qs @ ps' \<and> (ks' \<noteq> [] \<and> ps' \<noteq> [] \<longrightarrow> hd ks' \<noteq> hd ps')"
+  apply(induction ks ps arbitrary: qs ks' ps' rule: split.induct)
+  apply(auto split: prod.splits if_splits)
+  done
+    
+lemma abs_ptrie_insertP:
+  "abs_ptrie (insertP ks t) = insert ks (abs_ptrie t)"
+  apply(induction t arbitrary: ks)
+  apply(auto simp: prefix_trie_Leafs insert_prefix_trie_same insert_append prefix_trie_append
+      dest!: split_if split: list.split prod.split)
+  done
+    
+corollary isinP_insertP: "isinP (insertP ks t) ks' = (ks=ks' \<or> isinP t ks')"
+  by (simp add: isin_insert isinP abs_ptrie_insertP)
+    
+    (* <<<<<<< Trie1.thy <<<<<<< *)
+    
+    (** >>>>>>> Homework 09 >>>>>>> **)
+    
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+  
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+    "abs_itrie LeafI = Leaf"
+  | "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+  | "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+  | "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+    
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+  
+  
+section \<open>Homework 9.1\<close>
+  
+fun shrunk :: "trie \<Rightarrow> bool" where
+  "shrunk Leaf \<longleftrightarrow> True"
+| "shrunk (Node b (l, r)) \<longleftrightarrow> (l=Leaf\<and>r=Leaf \<longrightarrow> b) \<and> shrunk l \<and> shrunk r"
+  
+lemma "shrunk Leaf"
+  by simp
+    
+lemma [dest]: "insert ks t = Leaf \<Longrightarrow> False"
+  by (induction ks t rule: insert.induct) auto
+    
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  by (induction ks t rule: insert.induct) auto
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  by (induction ks t rule: delete2.induct) (auto split: list.split)
+    
+section \<open>Homework 9.2\<close>
+  
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI"
+| "deleteI ks (UnaryI d t) = UnaryI d (if ks=[] \<or> hd ks\<noteq>d then t else deleteI (tl ks) t)"
+| "deleteI [] (BinaryI b lr) = BinaryI False lr"
+| "deleteI (k#ks) (BinaryI b (l, r)) = BinaryI b (if k then (l, deleteI ks r) else (deleteI ks l, r))"
+  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  by (induction t arbitrary: ks rule: abs_itrie.induct) (auto split: list.split)
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+    "pdelete _ LeafP = LeafP"
+  | "pdelete ks (NodeP ps b (l, r)) = (case split ks ps of
+    (_, [], []) \<Rightarrow> NodeP ps False (l, r)
+  | (_, k#ks', []) \<Rightarrow> NodeP ps b (if k then (l, pdelete ks' r) else (pdelete ks' l, r))
+  | _ \<Rightarrow> NodeP ps b (l, r))"
+    
+fun prefix_trieI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "prefix_trieI [] = id"
+| "prefix_trieI (k#ks) = UnaryI k \<circ> prefix_trieI ks"
+  
+lemma [simp]: "prefix_trieI (ks@ks') = prefix_trieI ks \<circ> prefix_trieI ks'"
+  by (induction ks) auto
+    
+lemma [simp]: "deleteI (ks@ks') (prefix_trieI ks t) = prefix_trieI ks (deleteI ks' t)"
+  by (induction ks) auto
+    
+lemma [simp]: "deleteI ks (prefix_trieI ks t) = prefix_trieI ks (deleteI [] t)"
+  by (induction ks) auto
+    
+lemma [simp]: "absI_ptrie (NodeP ps b (l, r)) = prefix_trieI ps (BinaryI b (absI_ptrie l, absI_ptrie r))"
+  by (induction ps)  auto
+    
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  by (induction t arbitrary: ks) (auto split: prod.split list.split if_splits dest!: split_if)
+    
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hu_Shuwei_shuwei.hu@tum.de_455/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+shuwei.hu@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hu_Shuwei_shuwei.hu@tum.de_455/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hutzler_Matthias_ga95luy@mytum.de_465/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+ga95luy@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hutzler_Matthias_ga95luy@mytum.de_465/ex09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,111 @@
+(** Score: 10/10
+*)
+theory ex09
+  imports "../fds_ss17/Thys/Trie1"
+begin
+
+
+  (* needed for Homework *)
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+
+
+    (* Homework 9.1 *)
+
+fun shrunk :: "trie \<Rightarrow> bool" where
+  "shrunk Leaf = True" |
+  "shrunk (Node b (l, r)) \<longleftrightarrow> shrunk l \<and> shrunk r \<and> (b \<or> l\<noteq>Leaf \<or> r\<noteq>Leaf)"
+
+lemma "shrunk Leaf"
+  by auto
+    
+lemma [simp]: "insert ks t \<noteq> Leaf"
+  apply (cases ks)
+   apply (cases t)
+    apply auto
+  apply (cases t)
+   apply auto
+  done
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  by (induction t rule: insert.induct) auto
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  by (induction t rule: delete2.induct) (auto split: list.split)
+    
+    
+  (* Homework 9.2 *)
+  
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI ks LeafI = LeafI" |
+  "deleteI ks (UnaryI k t) = (case ks of
+     [] \<Rightarrow> UnaryI k t |
+     (k'#ks') \<Rightarrow> if k'=k then UnaryI k (deleteI ks' t) else UnaryI k t)" |
+  "deleteI ks (BinaryI b (l, r)) = (case ks of
+     [] \<Rightarrow> BinaryI False (l, r) |
+     (k'#ks') \<Rightarrow> if k' then BinaryI b (l, deleteI ks' r) else BinaryI b (deleteI ks' l, r))"
+  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  by (induction t arbitrary: ks rule: abs_itrie.induct) (auto split: list.split)
+    
+fun dropPrefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> ('a list) option" where
+  "dropPrefix [] l = Some l" |
+  "dropPrefix (p#ps) (x#xs) = (if p=x then dropPrefix ps xs else None)" |
+  "dropPrefix (p#ps) [] = None"
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where  
+  "pdelete ks LeafP = LeafP" |
+  "pdelete ks (NodeP ps b (l, r)) = (case dropPrefix ps ks of
+     None \<Rightarrow> NodeP ps b (l, r) |
+     Some [] \<Rightarrow> NodeP ps False (l, r) |
+     Some (True#ks') \<Rightarrow> NodeP ps b (l, pdelete ks' r) |
+     Some (False#ks') \<Rightarrow> NodeP ps b (pdelete ks' l, r))"
+
+lemma aux_non_deleteI: "dropPrefix ps ks = None \<Longrightarrow>
+  deleteI ks (absI_ptrie (NodeP ps b (l, r))) = absI_ptrie (NodeP ps b (l, r))"
+  by (induction ps arbitrary: ks) (auto split: list.split)
+lemma aux_deleteI: "dropPrefix ps ks = Some [] \<Longrightarrow>
+  deleteI ks (absI_ptrie (NodeP ps b (l, r))) = absI_ptrie (NodeP ps False (l, r))"
+  by (induction ps arbitrary: ks) (auto split: list.split)
+    
+lemma aux_deleteI_right:
+  "absI_ptrie (pdelete ks' r) = deleteI ks' (absI_ptrie r) \<Longrightarrow>
+   dropPrefix ps ks = Some (True # ks') \<Longrightarrow>
+   absI_ptrie (NodeP ps b (l, pdelete ks' r)) = deleteI ks (absI_ptrie (NodeP ps b (l, r)))"
+  apply (induction ps arbitrary: ks ks')
+  by (auto split: list.split)
+    
+lemma aux_deleteI_left:
+  "absI_ptrie (pdelete ks' l) = deleteI ks' (absI_ptrie l) \<Longrightarrow>
+   dropPrefix ps ks = Some (False # ks') \<Longrightarrow>
+   absI_ptrie (NodeP ps b (pdelete ks' l, r)) = deleteI ks (absI_ptrie (NodeP ps b (l, r)))"
+  apply (induction ps arbitrary: ks ks')
+  by (auto split: list.split)
+    
+  
+    
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  apply (induction t rule: pdelete.induct)
+  using aux_deleteI aux_non_deleteI
+  by (auto split: option.split list.split bool.split intro: aux_deleteI_right aux_deleteI_left)
+
+end    
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Hutzler_Matthias_ga95luy@mytum.de_465/user_error_log.txt	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,4 @@
+Using temporary directory '/tmp/tmp.A3faEwVYB9'
+Files in /tmp/eval-465-ZWm9R8: ex09.thy
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Kurz_Friedrich_friedrich.kurz@tum.de_468/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+friedrich.kurz@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Kurz_Friedrich_friedrich.kurz@tum.de_468/hw_09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,270 @@
+(** Score: 7/10
+
+  Introduced inconsistent lemma by sorry, and unconsciously used resulting
+  inconsistency to 'prove' further lemmas \<dots> ignoring warning from metis \<dots>
+
+  See detailed comments below \<dots>
+*)
+(*<*)
+theory hw_09
+  imports "../../Material/Thys/Trie1"
+begin
+(*>*)  
+text {* \ExerciseSheet{9}{23.~6.~2017} *}
+
+text \<open>\Exercise{Union Function on Tries}
+  Define a function to merge two tries and show its correctness
+\<close>  
+fun union :: "trie \<Rightarrow> trie \<Rightarrow> trie" 
+  where "union _ _ = undefined"
+    
+text \<open>
+  \Exercise{Intermediate Abstraction Level for Patricia Tries}
+
+  We introduce an abstraction level in between tries and Patricia tries:
+  A node with only a single non-leaf successor is represented as an unary node.
+
+  Via unary nodes, this implementation already introduces a notion of common prefix,
+  but does not yet summarize runs of multiple prefixes into a list.
+\<close>
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+text \<open>Refine the union function to intermediate tries\<close>
+fun unionI :: "itrie \<Rightarrow> itrie \<Rightarrow> itrie" 
+  where "unionI _ _ = undefined"
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+  
+
+text \<open>Warmup: Show that abstracting Patricia tries over intermediate 
+  tries to tries is the same as abstracting directly to tries.\<close>  
+  
+  
+text \<open>Refine the union function to Patricia tries.
+
+  Hint: First figure out how a Patricia trie that 
+    correspond to a leaf/unary/binary node looks like. 
+    Then translate @{const \<open>unionI\<close>} equation by equation!
+
+  More precisely, try to find terms \<open>unaryP\<close> and \<open>binaryP\<close> such that
+    @{term [display] "absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"}
+    @{term [display] "absI_ptrie (binaryP v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"}
+
+  You will encounter a small problem with \<open>unaryP\<close>. Which one?
+\<close>
+  
+    
+fun unionP :: "ptrie \<Rightarrow> ptrie \<Rightarrow> ptrie" 
+  where "unionP _ _ = undefined"
+    
+(**
+ * HW 9.1
+ *)
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>
+  
+thm delete2.simps
+thm node.simps
+thm Trie1.insert.simps
+  
+value "insert [True, True, True] Leaf"
+value "insert [False, False, False] Leaf"
+value "insert [True, False, True, False, True] Leaf"
+  
+fun shrunk :: "trie \<Rightarrow> bool" where 
+  "shrunk Leaf = True"
+  | "shrunk (Node False (Leaf, Leaf)) = False"
+  | "shrunk (Node _ _) = True"
+
+value "shrunk (insert [True, True, True] Leaf)"
+value "shrunk (insert [False, False, False] Leaf)"
+value "shrunk (insert [True, False, True, False, True] Leaf)"
+
+lemma hw_9_1_a: "shrunk (insert [] t)" 
+  apply(induction t)
+  apply(auto)
+  done
+
+lemma "shrunk Leaf" by simp
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  proof (induction ks)
+    case Nil
+    then show ?case 
+      by (simp add: hw_9_1_a)
+  next
+    case (Cons a ks)
+    then show ?case proof (induction t)
+      case Leaf
+      then show ?case
+        by (smt insert.simps(3) isin.simps(1) isin_insert old.prod.inject shrunk.elims(3) trie.inject)
+    next
+      case (Node b lr)
+      term "?case"
+      then show ?case by (smt insert.simps(4) isin.simps(1) isin_insert old.prod.exhaust old.prod.inject shrunk.elims(3) trie.inject)
+    qed
+  qed
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)" 
+  proof (induction ks)
+    case Nil
+    then show ?case by (smt delete2.elims list.simps(4) node.simps shrunk.elims(3) trie.distinct(1) trie.inject)
+  next 
+    case (Cons a ks)
+    then show ?case 
+      apply(induction t rule: delete2.induct) 
+      apply(auto) 
+      by (smt list.case_eq_if node.simps shrunk.elims(3) trie.distinct(1) trie.inject)
+  qed    
+  
+(**
+ * HW 9.2
+ *)
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>
+
+value "abs_itrie (UnaryI True (UnaryI True (UnaryI True (BinaryI True (LeafI, LeafI)))))"
+value "insert [True, True, True] Leaf"
+value "abs_itrie (UnaryI True (UnaryI True (UnaryI True (BinaryI True (LeafI, LeafI))))) = insert [True, True, True] Leaf"
+  
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI"
+  | "deleteI (k # ks) (UnaryI b t) = (if k = b 
+      then (UnaryI b (deleteI ks t))
+      else (UnaryI b t)
+    )"
+  | "deleteI (k # ks) (BinaryI b (l, r)) = (if k 
+      then BinaryI b (l, deleteI ks r)
+      else BinaryI b (deleteI ks l, r)
+  )"
+  | "deleteI [] (BinaryI True t) = BinaryI False t"
+  | "deleteI [] t = t"
+  
+value "delete [True, True, True] (insert [True, True, True] Leaf)"
+value "abs_itrie (deleteI [True, True, True] (UnaryI True (UnaryI True (UnaryI True (BinaryI True (LeafI, LeafI))))))"
+value "abs_itrie (deleteI [True, True, True] (UnaryI True (UnaryI True (UnaryI True (BinaryI True (LeafI, LeafI)))))) = delete [True, True, True] (insert [True, True, True] Leaf)"
+
+value "delete [False, False, False] (insert [False, False, False] Leaf)"
+value "abs_itrie (deleteI [False, False, False] (UnaryI False (UnaryI False (UnaryI False (BinaryI False (LeafI, LeafI))))))"
+value "abs_itrie (deleteI [False, False, False] (UnaryI False (UnaryI False (UnaryI False (BinaryI False (LeafI, LeafI)))))) = delete [False, False, False] (insert [False, False, False] Leaf)"
+
+lemma hw_9_2_a: "abs_itrie (deleteI ks t) = delete ks (abs_itrie t) \<Longrightarrow> abs_itrie (UnaryI b (deleteI ks t)) = delete (b # ks) (abs_itrie (UnaryI b t))"
+  apply(induction t arbitrary: ks rule: deleteI.induct)
+  apply(simp)+
+  apply(auto split: if_splits)
+  apply (smt abs_itrie.simps(1) abs_itrie.simps(2) abs_itrie.simps(3) delete.simps(1) delete.simps(2) list.case_eq_if)
+  subgoal by (smt abs_itrie.simps(2) abs_itrie.simps(3) delete.simps(2) list.case_eq_if list.sel(1) list.sel(3) list.simps(3))
+  subgoal by (smt abs_itrie.simps(2) abs_itrie.simps(3) abs_itrie.simps(4) delete.simps(2) list.case(2) list.case_eq_if) 
+  subgoal by (smt abs_itrie.simps(2) abs_itrie.simps(3) abs_itrie.simps(4) delete.simps(2) list.case(2) list.case_eq_if)
+  subgoal by (meson \<open>\<And>ta ksa k ba. \<lbrakk>\<And>ks. \<lbrakk>k = ba; abs_itrie (deleteI ks ta) = delete ks (abs_itrie ta)\<rbrakk> \<Longrightarrow> abs_itrie (UnaryI b (deleteI ks ta)) = delete (b # ks) (abs_itrie (UnaryI b ta)); abs_itrie (deleteI ksa (UnaryI ba ta)) = delete ksa (abs_itrie (UnaryI ba ta))\<rbrakk> \<Longrightarrow> abs_itrie (UnaryI b (deleteI ksa (UnaryI ba ta))) = delete (b # ksa) (abs_itrie (UnaryI b (UnaryI ba ta)))\<close>)
+  subgoal by (smt abs_itrie.simps(2) abs_itrie.simps(3) abs_itrie.simps(4) delete.simps(2) list.case(2) list.case_eq_if) 
+  done
+  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)" 
+  apply(induction ks t rule: deleteI.induct)
+  apply(auto)
+  subgoal 
+    apply(simp add: hw_9_2_a) 
+    done
+  subgoal by (smt abs_itrie.simps(2) abs_itrie.simps(3) delete.simps(1) delete.simps(2) list.case_eq_if list.sel(1))
+  subgoal by (smt abs_itrie.simps(2) abs_itrie.simps(3) delete.simps(2) list.case_eq_if)
+  done
+
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where  
+  "pdelete _ LeafP = LeafP"
+  | "pdelete [] (NodeP list b t) = (NodeP list False t)"
+  | "pdelete ks (NodeP list b (l, r)) = (let n = length list in
+    if list = take n ks
+    then case drop n ks of
+      [] \<Rightarrow> (NodeP list False (l, r))
+      | (k # ks') \<Rightarrow> if k then (NodeP list b (l, pdelete ks' r)) else (NodeP list b (pdelete ks' l, r))
+    else (NodeP list b (l, r))
+  )"
+
+thm absI_ptrie.simps
+
+value "insertP [True, True, True] LeafP"
+value "pdelete [True, True, True] (insertP [True, True, True] LeafP)"
+value "absI_ptrie (pdelete [True, True, True] (insertP [True, True, True] LeafP))"
+value "deleteI [True, True, True] (absI_ptrie (insertP [True, True, True] LeafP))"
+value "absI_ptrie (pdelete [True, True, True] (insertP [True, True, True] LeafP)) = deleteI [True, True, True] (absI_ptrie (insertP [True, True, True] LeafP))"
+
+value "insertP [False, False, False] LeafP"
+value "pdelete [False, False, False] (insertP [False, False, False] LeafP)"
+value "absI_ptrie (pdelete [True, True, True] (insertP [False, False, False] LeafP))"
+value "deleteI [False, False, False] (absI_ptrie (insertP [False, False, False] LeafP))"
+value "absI_ptrie (pdelete [False, False, False] (insertP [False, False, False] LeafP)) = deleteI [False, False, False] (absI_ptrie (insertP [False, False, False] LeafP))"   
+
+  
+lemma hw_9_2_b: "absI_ptrie (pdelete [] (NodeP list b t)) = deleteI [] (absI_ptrie (NodeP list b t))"
+  apply(induction list arbitrary: t)
+  apply(auto)
+  subgoal by (metis deleteI.simps(4) deleteI.simps(6))
+  subgoal sorry
+  done
+
+lemma "absI_ptrie (pdelete [] (NodeP list b t)) = deleteI [] (absI_ptrie (NodeP list b t))"
+  nitpick  (** Und da gibt es auch schon ein Gegenbeispiel *)
+  oops
+
+(** Sorry ist gefährlich, wenn das angenommene Lemma gar nicht gilt \<dots>*)    
+lemmas FalseI = hw_9_2_b[of "[False]" True "(LeafP, LeafP)", simplified]
+  
+(** Ab jetzt sind Beweise sehr einfach \<dots> *)  
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)" 
+  using FalseI by simp
+
+(** Der metis-Aufruf in ihrem lemma hat diesen Widerspruch auch gefunden, und einen mit
+  Metis: The assumptions are inconsistent
+  gewarnt \<dots>
+*)    
+    
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)" 
+  apply(induction ks t rule: pdelete.induct)
+  (*Den Fehler "wrong format for split rule" kann ich leider nicht beheben. Tut mir leid! :( *)
+    (** case_split ist halt keine split-rule, trotz des etwas ungünstigen Namens ...
+      Sie meinten wahrscheinlich list.split? Dadurch wird ihr goal aber auch nicht lösbarer \<dots>   
+ 
+      Spätestens die Warnung von metis, "The assumptions are inconsistent", sollte einen
+      hier stutzig machen, vor allem wenn man ein lemma was man mit sorry eingeführt hat, benutzt \<dots>
+      Deutet alles darauf hin, das hw_9_2_b gar nicht gilt \<dots> Siehe oben
+    *)
+  (*apply(auto split: if_splits list.split)
+  apply(auto split: if_splits case_split)*)
+  subgoal by simp
+  subgoal using hw_9_2_b by auto
+  subgoal by (metis \<open>\<And>ta list b. absI_ptrie (pdelete [] (NodeP list b ta)) = deleteI [] (absI_ptrie (NodeP list b ta))\<close> absI_ptrie.elims absI_ptrie.simps(2) absI_ptrie.simps(3) deleteI.simps(5) itrie.distinct(5) itrie.inject(1) itrie.inject(2) pdelete.simps(2) ptrie.distinct(1))
+  done
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Kurz_Friedrich_friedrich.kurz@tum.de_468/user_error_log.txt	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,6 @@
+Using temporary directory '/tmp/tmp.IollmkWelA'
+Files in /tmp/eval-468-D7fakY: hw_09.thy
+Submission did not check in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Madge_Pimentel_Fabio_fabio.madge@tum.de_445/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+fabio.madge@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Madge_Pimentel_Fabio_fabio.madge@tum.de_445/tmpl09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,106 @@
+(** Score: 10/10
+*)
+(*<*)
+theory tmpl09
+  imports "Trie1"
+begin
+(*>*)  
+text {* \ExerciseSheet{9}{23.~6.~2017} *}
+
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" where 
+    "shrunk Leaf = True"
+  | "shrunk (Node False (Leaf,Leaf)) \<longleftrightarrow> False"
+  | "shrunk (Node b (l,r)) \<longleftrightarrow> shrunk l \<and> shrunk r"
+
+lemma "shrunk Leaf" by simp
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  apply (induct ks t rule: insert.induct, simp)
+  using shrunk.elims(2) apply fastforce
+   apply simp_all
+   apply (metis insert.simps(1) insert.simps(3) list.exhaust shrunk.simps(1) shrunk.simps(4) shrunk.simps(5))
+  by (metis insert.simps(2) insert.simps(4) list.exhaust shrunk.simps(1) shrunk.simps(4) shrunk.simps(5) surj_pair trie.distinct(1) trie.exhaust)
+
+  
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  apply (induct ks t rule: delete2.induct, simp)
+  apply (auto split: list.split)
+  by (metis (full_types) shrunk.simps(4) shrunk.simps(5) trie.exhaust)+
+
+
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI" |
+  "deleteI ks (UnaryI b t) = (case ks of 
+    [] \<Rightarrow> UnaryI b t | 
+    k#ks \<Rightarrow> UnaryI b ((if k = b then deleteI ks else id) t))" | 
+  "deleteI ks (BinaryI b (l,r)) =
+   (case ks of
+      [] \<Rightarrow> BinaryI False (l,r) |
+      k#ks' \<Rightarrow> BinaryI b (if k then (l, deleteI ks' r) else (deleteI ks' l, r)))"
+  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  apply (induct t arbitrary: ks rule: abs_itrie.induct, simp)
+  by (auto split: list.split)
+
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete _ LeafP = LeafP" |
+  "pdelete ks (NodeP ps b (l,r)) = (let n = length ps in
+    if ps = take n ks                                                                        
+    then case drop n ks of 
+      [] \<Rightarrow> NodeP ps False (l,r) | 
+      k#ks \<Rightarrow> NodeP ps b (if k then (l, pdelete ks r) else (pdelete ks l, r))
+    else NodeP ps b (l,r))
+"
+
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)" 
+  apply (induct t arbitrary: ks rule: absI_ptrie.induct, simp)
+   apply (simp add: list.case_eq_if)
+  apply (simp add: list.case_eq_if take_Suc drop_Suc)
+  by (smt One_nat_def drop_eq_Nil length_tl list.case_eq_if take_all)
+
+    
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Oganyan_Levon_levon.oganyan@tum.de_471/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+levon.oganyan@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Oganyan_Levon_levon.oganyan@tum.de_471/hmw09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,159 @@
+(** Score: 5/10
+  hw 2 no proofs
+*)
+(*<*)
+theory hmw09
+  imports "Thys/Trie1"
+begin
+(*>*)  
+text {* \ExerciseSheet{9}{23.~6.~2017} *}
+
+text \<open>\Exercise{Union Function on Tries}
+  Define a function to merge two tries and show its correctness
+\<close>  
+fun union :: "trie \<Rightarrow> trie \<Rightarrow> trie" 
+  where "union _ _ = undefined"
+  
+    
+text \<open>
+  \Exercise{Intermediate Abstraction Level for Patricia Tries}
+
+  We introduce an abstraction level in between tries and Patricia tries:
+  A node with only a single non-leaf successor is represented as an unary node.
+
+  Via unary nodes, this implementation already introduces a notion of common prefix,
+  but does not yet summarize runs of multiple prefixes into a list.
+\<close>
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+text \<open>Refine the union function to intermediate tries\<close>
+fun unionI :: "itrie \<Rightarrow> itrie \<Rightarrow> itrie" 
+  where "unionI _ _ = undefined"
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+  
+
+text \<open>Warmup: Show that abstracting Patricia tries over intermediate 
+  tries to tries is the same as abstracting directly to tries.\<close>  
+  
+  
+text \<open>Refine the union function to Patricia tries.
+
+  Hint: First figure out how a Patricia trie that 
+    correspond to a leaf/unary/binary node looks like. 
+    Then translate @{const \<open>unionI\<close>} equation by equation!
+
+  More precisely, try to find terms \<open>unaryP\<close> and \<open>binaryP\<close> such that
+    @{term [display] "absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"}
+    @{term [display] "absI_ptrie (binaryP v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"}
+
+  You will encounter a small problem with \<open>unaryP\<close>. Which one?
+\<close>
+  
+    
+fun unionP :: "ptrie \<Rightarrow> ptrie \<Rightarrow> ptrie" 
+  where "unionP _ _ = undefined"
+  
+    
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" where 
+
+"shrunk Leaf  = True"|
+"shrunk (Node b (l,r)) = (
+  if b 
+  then shrunk l \<and> shrunk r
+  else if (l,r) \<noteq> (Leaf,Leaf)
+       then shrunk l \<and> shrunk r
+       else False
+)"
+
+lemma "shrunk Leaf" by simp
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  apply (induction t rule: insert.induct)
+  apply auto
+  apply metis
+  apply metis
+  apply (metis isin.simps(1) isin_insert)
+  apply (metis isin.simps(1) isin_insert)
+  apply (metis isin.simps(1) isin_insert)
+  apply meson
+  apply meson
+  apply (metis isin.simps(1) isin_insert)
+  apply meson
+  apply (metis isin.simps(1) isin_insert)
+  by meson    
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  apply (induction t rule: insert.induct)
+  apply auto
+  apply metis
+  apply metis
+  apply metis
+  apply metis
+  apply metis
+  by metis
+    
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+    
+fun deleteI :: "bool list \<Rightarrow>  itrie \<Rightarrow> itrie" where
+  "deleteI ks LeafI = LeafI"|
+  "deleteI ks (UnaryI b t) =
+    (case ks of
+        [] \<Rightarrow> UnaryI b t |
+        k#ks' \<Rightarrow> UnaryI b (if k = b then (deleteI ks' t) else t)
+    )"|
+  "deleteI ks (BinaryI b (l,r)) = 
+    (case ks of
+      [] \<Rightarrow> BinaryI False (l,r)|
+      k#ks' \<Rightarrow> BinaryI b (if k then (l, deleteI ks' r) else (deleteI ks' l, r))
+    )"
+  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  apply (induction t rule: deleteI.induct)
+  sorry
+   
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete _ _ = undefined"
+  
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"  sorry
+    
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Oganyan_Levon_levon.oganyan@tum.de_471/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Ouyang_Lena_ga96vup@mytum.de_472/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+ga96vup@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Ouyang_Lena_ga96vup@mytum.de_472/hw09new.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,192 @@
+(** Score: 4/10
+  hw1 ... too many sorries
+  hw2. ptrie missing
+
+*)
+(*<*)
+theory hw09new
+  
+  imports "../../Material/Thys/Trie1"
+  (*
+  imports "../../../../Desktop/fds/Thys/Trie1"
+*)
+    
+begin
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+(*>*)  
+fun shrunk :: "trie \<Rightarrow> bool" where
+  "shrunk (Node False (Leaf,Leaf)) = False"|
+  "shrunk Leaf = True"|
+  "shrunk (Node _ (l,r)) = ((shrunk l) \<and> (shrunk r))"
+  
+  
+lemma "shrunk Leaf" by auto
+
+lemma a:"insert ks Leaf \<noteq> Leaf" apply (induction ks) by auto
+lemma b:"shrunk (Node b (Leaf, insert ks Leaf)) = shrunk (insert ks Leaf)" by (cases ks)(auto simp: a)
+lemma c:"shrunk (Node b (insert ks Leaf, Leaf)) = shrunk (insert ks Leaf)" by (cases ks)(auto simp: a)
+lemma d:"shrunk (insert ks Leaf)"
+  apply (induction ks) by (auto simp: b c)
+lemma e: "(a\<noteq> Leaf \<or> b \<noteq> Leaf \<or> x1) \<and> shrunk (Node x1 (a, b)) \<Longrightarrow> shrunk a \<and> shrunk b"
+  using insert.simps(2) shrunk.elims(2) by blast
+lemma f: "a= Leaf \<and> b = Leaf \<and> \<not>x1 \<Longrightarrow> \<not>shrunk (Node x1 (a, b))" by auto
+lemma g: "(\<not>a \<Longrightarrow> \<not>b) \<Longrightarrow> (a \<and> b \<Longrightarrow> c) \<Longrightarrow> b \<Longrightarrow> c" by auto
+lemma h: "shrunk (Node x1 (a, b)) \<Longrightarrow> shrunk a \<and> shrunk b"
+  using e f g[of "(a\<noteq> Leaf \<or> b \<noteq> Leaf \<or> x1)" "shrunk (Node x1 (a, b))" "shrunk a \<and> shrunk b"] by blast
+  
+lemma i:"(a \<Longrightarrow> b) \<Longrightarrow> a \<Longrightarrow> b" by auto
+  
+lemma aux:
+assumes "(shrunk a \<Longrightarrow> shrunk (insert ks a)) \<Longrightarrow>
+       (shrunk b \<Longrightarrow> shrunk (insert ks b)) \<Longrightarrow> shrunk (Node x1 (a, b))"
+shows "shrunk (insert ks (Node x1 (a, b)))"
+  proof (cases ks)
+    case Nil
+    then have "shrunk (insert ks (Node x1 (a, b))) = shrunk(Node True (a,b))"by auto
+        then have "... = True" using h[of "x1" "a" "b"] assms 
+          (*sledgehammer found this but it times out for me
+            by (smt d insert.simps(2) local.Nil shrunk.elims(2) shrunk.simps(3))*)
+            sorry
+    then show ?thesis using assms
+      by (simp add: \<open>shrunk (insert ks (Node x1 (a, b))) = shrunk (Node True (a, b))\<close>)
+  next
+    case (Cons x xs)
+    then show ?thesis
+      proof (cases x)
+        case True
+        then show ?thesis sorry
+      next
+        case False
+        then show ?thesis sorry
+      qed
+  qed
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  apply (induction t arbitrary: ks)
+   apply (cases t)
+    apply (auto simp: d)
+    using aux by auto
+  
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)" 
+  apply (induction t arbitrary: ks)
+   apply (cases t)
+    apply (auto split:list.splits)
+    apply (metis h shrunk.elims(2) shrunk.simps(4))
+    apply (metis h shrunk.elims(2) shrunk.simps(4))
+    apply (metis h shrunk.elims(2) shrunk.simps(4))
+    apply (metis h shrunk.elims(2) shrunk.simps(4))
+    (*found by sledgehammer but times out
+      apply (smt h shrunk.elims(2) shrunk.simps(5))*)
+  sorry
+    
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+"deleteI ks LeafI = LeafI" |
+"deleteI [] (UnaryI b n) = UnaryI b n"|
+"deleteI [] (BinaryI b n) = BinaryI False n"|
+"deleteI (k#ks) (UnaryI b n) = (if k=b then UnaryI b (deleteI ks n) else UnaryI b n)"|
+"deleteI (k#ks) (BinaryI b (l,r)) = BinaryI b (if k then (l, deleteI ks r) else (deleteI ks l , r))"
+
+lemma a1: "abs_itrie (UnaryI b n) = delete [] (abs_itrie (UnaryI b n))"
+proof (cases b)
+  case True
+  then have a:"abs_itrie (UnaryI b n) = Node False (Leaf, abs_itrie n)" by auto
+  also have "... = delete [] (Node False (Leaf, abs_itrie n))" by auto
+  also have "... = delete [] (abs_itrie (UnaryI b n))" using a by auto
+  then show ?thesis using local.a by auto
+next
+  case False
+  then have a:"abs_itrie (UnaryI b n) = Node False (abs_itrie n, Leaf)" by auto
+  also have "... = delete [] (Node False (abs_itrie n, Leaf))" by auto
+  also have "... = delete [] (abs_itrie (UnaryI b n))" using a by auto
+  then show ?thesis using local.a by auto
+qed
+  
+lemma a2:
+  assumes "abs_itrie (deleteI ks n) = delete ks (abs_itrie n)"
+  shows "abs_itrie (UnaryI b (deleteI ks n)) = delete (b # ks) (abs_itrie (UnaryI b n))"
+proof (cases b)
+  case True
+  then have "abs_itrie (UnaryI b (deleteI ks n)) = Node False (Leaf, abs_itrie (deleteI ks n))" by auto
+  also have "... = Node False (Leaf, delete ks (abs_itrie n))" using assms by auto
+  also have "... = delete (b # ks) (Node False (Leaf, abs_itrie n))" by (simp add: True) 
+  also have "... = delete (b # ks) (abs_itrie (UnaryI b n))" by (simp add: True)
+  then show ?thesis by (simp add: calculation)
+next
+  case False
+  then have "abs_itrie (UnaryI b (deleteI ks n)) = Node False (abs_itrie (deleteI ks n), Leaf)" by auto
+  also have "... = Node False (delete ks (abs_itrie n), Leaf)" using assms by auto
+  also have "... = delete (b # ks) (Node False (abs_itrie n, Leaf))" by (simp add: False) 
+  also have "... = delete (b # ks) (abs_itrie (UnaryI b n))" by (simp add: False)
+  then show ?thesis by (simp add: calculation)
+qed
+lemma a3: "abs_itrie (UnaryI b n) = delete ((\<not> b) # ks) (abs_itrie (UnaryI b n))"
+  proof (cases b)
+    case True
+    then have "abs_itrie (UnaryI b n) = Node False (Leaf, abs_itrie n)" by auto
+        also have "... = delete ((\<not> b) # ks) (Node False (Leaf, abs_itrie n))" by (simp add: True)
+        also have "... = delete ((\<not> b) # ks) (abs_itrie (UnaryI b n))" by (simp add: True)
+    then show ?thesis by (simp add: calculation)
+  next
+    case False
+    then have "abs_itrie (UnaryI b n) = Node False (abs_itrie n, Leaf)" by auto
+        also have "... = delete ((\<not> b) # ks) (Node False (abs_itrie n, Leaf))" by (simp add: False)
+        also have "... = delete ((\<not> b) # ks) (abs_itrie (UnaryI b n))" by (simp add: False)
+    then show ?thesis by (simp add: calculation)
+  qed
+
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  apply (induction ks t rule: deleteI.induct)
+      apply auto
+  using a1 apply simp
+  using a2 apply simp
+  using a3 apply simp
+  done
+    
+(*is that function correct? or how could I define this better*)
+(** Not using split, but recursion removing only the first element of the prefix,
+  as we did for unionP in the tutorial \<dots> *)    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete ks LeafP = LeafP"|
+  "pdelete [] (NodeP [] b (l,r)) = NodeP [] False (l,r)"|
+  "pdelete [] (NodeP (x#xs) b (l,r)) = NodeP (x#xs) b (l,r)"|
+  "pdelete (k#ks) (NodeP [] b (l,r)) = NodeP [] b (if k then (l, pdelete ks r) else (pdelete ks l , r))"|
+  "pdelete (k#ks) (NodeP (x#xs) b (l,r)) = (case split (k#ks) (x#xs) of
+        ((k#ks), [], []) \<Rightarrow> NodeP (x#xs) False (l,r)
+        | (z, (y#ys), []) \<Rightarrow> NodeP (x#xs) b (if y then (l, pdelete ys r) else (pdelete ys l, r))
+        | (_,_,_) \<Rightarrow> NodeP (x#xs) b (l,r))"
+  
+(*no idea how to solve that one list.splits doesn't work either, and I don't understand the "case case"*)    
+  
+(**
+  case (case \<dots> of \<dots>) of \<dots>
+  you're simply doing case distinction over the result of a case distinction.
+*)  
+  
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  apply (induction ks t rule:pdelete.induct)
+      apply auto
+  sorry
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Ouyang_Lena_ga96vup@mytum.de_472/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Rokopf_Simon_simon.rosskopf@tum.de_467/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+simon.rosskopf@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Rokopf_Simon_simon.rosskopf@tum.de_467/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Rokopf_Simon_simon.rosskopf@tum.de_467/tmpl09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,394 @@
+(** Score: 10/10 *)
+(*<*)
+theory tmpl09
+  imports Main
+begin
+(*>*)
+
+(* Bla bla proofs are ugly as always. *)
+  
+(* Inlined entire Trie1 theory*)
+  
+lemma [simp]: "(\<forall>x. x \<noteq> y) = False"
+by blast
+
+hide_const (open) insert
+
+declare Let_def[simp]
+
+
+subsection "Trie"
+
+datatype trie = Leaf | Node bool "trie * trie"
+
+fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
+"isin Leaf ks = False" |
+"isin (Node b (l,r)) ks =
+   (case ks of
+      [] \<Rightarrow> b |
+      k#ks \<Rightarrow> isin (if k then r else l) ks)"
+
+fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"insert [] Leaf = Node True (Leaf,Leaf)" |
+"insert [] (Node b lr) = Node True lr" |
+"insert (k#ks) Leaf =
+  Node False (if k then (Leaf, insert ks Leaf)
+                   else (insert ks Leaf, Leaf))" |
+"insert (k#ks) (Node b (l,r)) =
+  Node b (if k then (l, insert ks r)
+               else (insert ks l, r))"
+
+lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
+apply(induction as t arbitrary: bs rule: insert.induct)
+apply (auto split: list.splits)
+done
+
+text \<open>A simple implementation of delete; does not shrink the trie!\<close>
+
+fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"delete ks Leaf = Leaf" |
+"delete ks (Node b (l,r)) =
+   (case ks of
+      [] \<Rightarrow> Node False (l,r) |
+      k#ks' \<Rightarrow> Node b (if k then (l, delete ks' r) else (delete ks' l, r)))"
+
+lemma "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
+apply(induction as t arbitrary: bs rule: delete.induct)
+apply (auto split: list.splits)
+done
+
+fun node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
+"node b lr = (if \<not> b \<and> lr = (Leaf,Leaf) then Leaf else Node b lr)"
+
+fun delete2 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"delete2 ks Leaf = Leaf" |
+"delete2 ks (Node b (l,r)) =
+   (case ks of
+      [] \<Rightarrow> node False (l,r) |
+      k#ks' \<Rightarrow> node b (if k then (l, delete2 ks' r) else (delete2 ks' l, r)))"
+
+lemma "isin (delete2 as t) bs = isin (delete as t) bs"
+apply(induction as t arbitrary: bs rule: delete2.induct)
+ apply simp
+apply (force split: list.splits)
+done
+
+
+subsection "Patricia Trie"
+
+datatype ptrie = LeafP | NodeP "bool list" bool "ptrie * ptrie"
+
+fun isinP :: "ptrie \<Rightarrow> bool list \<Rightarrow> bool" where
+"isinP LeafP ks = False" |
+"isinP (NodeP ps b (l,r)) ks =
+  (let n = length ps in
+   if ps = take n ks
+   then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (if k then r else l) ks'
+   else False)"
+
+fun split where
+"split [] ys = ([],[],ys)" |
+"split xs [] = ([],xs,[])" |
+"split (x#xs) (y#ys) =
+  (if x\<noteq>y then ([],x#xs,y#ys)
+   else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
+
+fun insertP :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+"insertP ks LeafP  = NodeP ks True (LeafP,LeafP)" |
+"insertP ks (NodeP ps b (l,r)) =
+  (case split ks ps of
+     (qs,k#ks',p#ps') \<Rightarrow>
+       let tp = NodeP ps' b (l,r); tk = NodeP ks' True (LeafP,LeafP) in
+       NodeP qs False (if k then (tp,tk) else (tk,tp)) |
+     (qs,k#ks',[]) \<Rightarrow>
+       NodeP ps b (if k then (l, insertP ks' r) else (insertP ks' l, r)) |
+     (qs,[],p#ps') \<Rightarrow>
+       let t = NodeP ps' b (l,r) in
+       NodeP qs True (if p then (LeafP,t) else (t,LeafP)) |
+     (qs,[],[]) \<Rightarrow> NodeP ps True (l,r))"
+
+fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"prefix_trie [] t = t" |
+"prefix_trie (k#ks) t =
+  (let t' = prefix_trie ks t in Node False (if k then (Leaf,t') else (t',Leaf)))"
+
+fun abs_ptrie :: "ptrie \<Rightarrow> trie" where
+"abs_ptrie LeafP = Leaf" |
+"abs_ptrie (NodeP ps b (l,r)) = prefix_trie ps (Node b (abs_ptrie l, abs_ptrie r))"
+
+lemma isin_prefix_trie: "isin (prefix_trie ps t) ks =
+ (length ks \<ge> length ps \<and>
+  (let n = length ps in ps = take n ks \<and> isin t (drop n ks)))"
+apply(induction ps arbitrary: ks)
+apply(auto split: list.split)
+done
+
+lemma isinP: "isinP t ks = isin (abs_ptrie t) ks"
+apply(induction t arbitrary: ks rule: abs_ptrie.induct)
+ apply(auto simp: isin_prefix_trie split: list.split)
+ using nat_le_linear apply force
+using nat_le_linear apply force
+done
+
+lemma prefix_trie_Leafs: "prefix_trie ks (Node True (Leaf,Leaf)) = insert ks Leaf"
+apply(induction ks)
+apply auto
+done
+
+lemma insert_prefix_trie_same:
+  "insert ps (prefix_trie ps (Node b lr)) = prefix_trie ps (Node True lr)"
+apply(induction ps)
+apply auto
+done
+
+lemma insert_append: "insert (ks @ k # ks') (prefix_trie ks (Node b (t1,t2))) =
+  prefix_trie ks (Node b (if k then (t1, insert ks' t2) else (insert ks' t1, t2)))"
+apply(induction ks)
+apply auto
+done
+
+lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
+apply(induction ps)
+apply auto
+done
+
+lemma split_if: "split ks ps = (qs, ks', ps') \<Longrightarrow>
+  ks = qs @ ks' \<and> ps = qs @ ps' \<and> (ks' \<noteq> [] \<and> ps' \<noteq> [] \<longrightarrow> hd ks' \<noteq> hd ps')"
+apply(induction ks ps arbitrary: qs ks' ps' rule: split.induct)
+apply(auto split: prod.splits if_splits)
+done
+
+lemma abs_ptrie_insertP:
+  "abs_ptrie (insertP ks t) = insert ks (abs_ptrie t)"
+apply(induction t arbitrary: ks)
+apply(auto simp: prefix_trie_Leafs insert_prefix_trie_same insert_append prefix_trie_append
+           dest!: split_if split: list.split prod.split)
+done
+
+corollary isinP_insertP: "isinP (insertP ks t) ks' = (ks=ks' \<or> isinP t ks')"
+by (simp add: isin_insert isinP abs_ptrie_insertP)
+
+(* End inlining *)
+
+(* Begin homework *)
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+      
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+text \<open>Warmup: Show that abstracting Patricia tries over intermediate 
+  tries to tries is the same as abstracting directly to tries.\<close>  
+lemma "abs_itrie o absI_ptrie = abs_ptrie"
+  apply (rule ext)
+    subgoal for t by (induction rule: absI_ptrie.induct) simp_all
+    done 
+  
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" where 
+  "shrunk Leaf = True"
+| "shrunk (Node b (l, r)) = ((b \<or> l\<noteq>Leaf \<or> r\<noteq>Leaf) \<and> shrunk l \<and> shrunk r)"
+
+lemma "shrunk Leaf" by simp
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)" 
+  apply (induction ks t rule: insert.induct)
+    apply auto[3]
+   apply (metis isin.simps(1) isin_insert)
+  subgoal for k ks b l r apply (cases k) apply simp_all 
+     apply (metis isin.simps(1) isin_insert)+
+    done
+  done
+    
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  apply (induction ks t rule: delete2.induct)
+   apply simp
+  apply simp
+  subgoal for ks b l r
+    apply (cases ks)
+     apply simp_all
+    done
+  done  
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+    
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI"
+| "deleteI [] (UnaryI b t) = (UnaryI b t)"
+| "deleteI (k#ks) (UnaryI b t) = (if k=b then (UnaryI b (deleteI ks t)) else UnaryI b t)"
+| "deleteI [] (BinaryI v (l,r)) = (BinaryI False (l, r))"
+| "deleteI (k#ks) (BinaryI v (l,r)) 
+    = (BinaryI v (if k then (l, deleteI ks r) else (deleteI ks l,r)))"
+  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+proof (induction ks t rule: deleteI.induct)
+  case (1 uu)
+  then show ?case by simp
+next
+  case (2 b t)
+  then show ?case by (cases b) simp_all
+next
+  case (3 k ks b t)
+  then show ?case by auto
+next
+  case (4 v l r)
+  then show ?case by simp
+next
+  case (5 k ks v l r)
+  then show ?case by simp
+qed
+
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+"pdelete _ LeafP  = LeafP" |
+"pdelete ks (NodeP ps b (l,r)) =
+  (case split ks ps of
+     (qs,k#ks',p#ps') \<Rightarrow> NodeP ps b (l,r) |
+     (qs,k#ks',[]) \<Rightarrow>
+       NodeP ps b (if k then (l, pdelete ks' r) else (pdelete ks' l, r)) |
+     (qs,[],p#ps') \<Rightarrow> NodeP ps b (l,r) |
+     (qs,[],[]) \<Rightarrow> NodeP ps False (l,r))"
+
+(* Idea from Trie1 *)
+fun prefix_trieI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+"prefix_trieI [] t = t" |
+"prefix_trieI (k#ks) t = UnaryI k (prefix_trieI ks t)"
+
+lemma prefix_trieI_absI_ptrie: 
+  "absI_ptrie (NodeP ps v (l,r)) = prefix_trieI ps (BinaryI v (absI_ptrie l, absI_ptrie r))"
+  by (induction ps) simp_all
+    
+lemma deleteI_append_s: "deleteI ks (absI_ptrie (NodeP (ks@p#ps) v lr)) 
+  = prefix_trieI ks (absI_ptrie (NodeP (p#ps) v lr))"
+  apply (induction ks)
+    apply simp_all 
+   apply (metis absI_ptrie.simps(3) deleteI.simps(2) old.prod.exhaust)
+  by (metis absI_ptrie.simps(3) deleteI.simps(3) prod.collapse)
+
+lemma prefix_trieI_append: "prefix_trieI (ps @ qs) t = prefix_trieI ps (prefix_trieI qs t)"
+  by(induction ps) auto  
+  
+lemma deleteI_append: "deleteI (ks @ k # ks') (prefix_trieI ks (BinaryI b (t1,t2)))
+    = prefix_trieI ks (BinaryI b (if k then (t1, deleteI ks' t2) else (deleteI ks' t1, t2)))"
+  by (induction ks) simp_all
+
+lemma split_same: "split ks ks = (ks, [], [])"
+  by (induction ks) simp_all
+    
+lemma delete_pdelete_same: "absI_ptrie (pdelete ks (NodeP ks v (l, r))) =
+    deleteI ks (absI_ptrie (NodeP ks v (l, r)))"
+  by (induction ks) (simp_all add: split_same)
+           
+lemma deleteI_neq:"k\<noteq>p \<Longrightarrow> deleteI (qs @ k#ks) (absI_ptrie (NodeP (qs @ p#ps) v (l, r)))
+     = (absI_ptrie (NodeP (qs @ p#ps) v (l, r)))"
+  by (induction qs) simp_all
+
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)" 
+proof(induction t arbitrary: ks)
+  case LeafP
+  then show ?case by simp
+next
+  case (NodeP ps v lr)
+  obtain l r where "l=fst lr" "r=snd lr" by simp
+  hence "lr = (l, r)" by simp
+  have nicerIH1: "\<And>ks. absI_ptrie (pdelete ks l) = deleteI ks (absI_ptrie l)" 
+    using NodeP \<open>l = fst lr\<close> by (simp add: fsts.intros)
+  have nicerIH2: "\<And>ks. absI_ptrie (pdelete ks r) = deleteI ks (absI_ptrie r)" 
+    using NodeP \<open>r = snd lr\<close> by (simp add: snds.intros)
+
+  obtain qs kss pss where split: "split ks ps = (qs, kss, pss)" using prod_cases3 .
+  hence "ks = qs@kss" "ps = qs @ pss" "(kss \<noteq> [] \<and> pss \<noteq> [] \<longrightarrow> hd kss \<noteq> hd pss)" 
+    using split_if[of ks ps qs kss pss] by simp_all    
+  
+  show ?case
+  proof(cases kss)
+    case Nil
+    then show ?thesis
+    proof(cases pss)
+      case Nil
+      have "ks=qs" using \<open>kss=[]\<close> \<open>ks = qs @ kss\<close> by simp
+      have "ps=qs" using \<open>pss=[]\<close> \<open>ps = qs @ pss\<close> by simp
+      then show ?thesis
+        using \<open>ks = qs\<close> \<open>lr = (l, r)\<close> delete_pdelete_same by auto
+    next
+      case (Cons p' pss')
+      have "split ks ps = (qs, [], p'#pss')"
+        by (simp add: \<open>split ks ps = (qs, kss, pss)\<close> \<open>kss = []\<close> Cons)
+      hence "absI_ptrie (pdelete ks (NodeP ps v lr)) = absI_ptrie (NodeP ps v lr)"
+        using \<open>lr = (l,r)\<close> by (cases kss) simp_all 
+      have "ps \<noteq> []"
+        by (simp add: \<open>ps = qs @ pss\<close> local.Cons)
+      have "ks = qs"
+        by (simp add: \<open>ks = qs @ kss\<close> local.Nil)
+      then show ?thesis
+      proof(cases kss)
+        case Nil
+        then show ?thesis 
+          using \<open>absI_ptrie (pdelete ks (NodeP ps v lr)) = absI_ptrie (NodeP ps v lr)\<close> 
+            \<open>ks = qs\<close> \<open>lr = (l, r)\<close> \<open>ps = qs @ pss\<close> deleteI_append_s local.Cons 
+            prefix_trieI_absI_ptrie prefix_trieI_append by auto
+      next
+        case (Cons k' kss')
+        hence False using \<open>kss = []\<close> by simp
+        then show ?thesis ..
+      qed
+    qed
+  next
+    case (Cons k' kss')
+    then show ?thesis
+    proof(cases pss)
+      case Nil
+      then show ?thesis using Cons  \<open>lr = (l,r)\<close>
+        using \<open>ks = qs @ kss\<close> \<open>ps = qs @ pss\<close> \<open>split ks ps = (qs, kss, pss)\<close> 
+          deleteI_append nicerIH1 nicerIH2 prefix_trieI_absI_ptrie by auto
+    next
+      case (Cons p' pss')
+      have "k'\<noteq>p'" using \<open>(kss \<noteq> [] \<and> pss \<noteq> [] \<longrightarrow> hd kss \<noteq> hd pss)\<close> 
+          \<open>kss = k'#kss'\<close> \<open>pss = p'#pss'\<close> by simp
+            
+        have "split (qs@k'#kss') (qs@p'#pss') = (qs, k'#kss', p'#pss')" using 
+            \<open>split ks ps = (qs, kss, pss)\<close> \<open>ks = qs@kss\<close> \<open>ps = qs @ pss\<close>
+            \<open>kss = k'#kss'\<close> \<open>pss = p'#pss'\<close> by simp 
+        hence "absI_ptrie (pdelete (qs@k'#kss') (NodeP (qs@p'#pss') v (l,r)))
+             = absI_ptrie (NodeP (qs@p'#pss') v (l,r))"
+          by simp
+        then show ?thesis using \<open>kss = k'#kss'\<close>  \<open>lr = (l,r)\<close> \<open>ks = qs@kss\<close> \<open>ps = qs @ pss\<close>
+          by (simp add: \<open>k' \<noteq> p'\<close> local.Cons deleteI_neq)
+    qed
+  qed
+qed
+
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Saporta_Antoine_Jacques_antoine.saporta@tum.de_453/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+antoine.saporta@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Saporta_Antoine_Jacques_antoine.saporta@tum.de_453/hw09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,101 @@
+(** Score: 5/10
+  lemmas in hw2 do not hold, nitpick easily finds counterexamples \<longrightarrow> definitions wrong!
+  see comments below for details
+*)
+(*<*)
+theory hw09
+  imports "../../Material/Thys/Trie1"
+begin
+(*>*)  
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" where 
+"shrunk Leaf \<longleftrightarrow> True" |
+"shrunk (Node b (l,r)) \<longleftrightarrow> (b \<or> l\<noteq>Leaf \<or> r\<noteq>Leaf)  \<and> shrunk l \<and> shrunk r"
+
+lemma "shrunk Leaf" by simp
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+apply (induction ks t rule: insert.induct)
+apply auto
+apply (metis isin.simps(1) isin_insert)
+apply (metis isin.simps(1) isin_insert)
+apply (metis isin.simps(1) isin_insert)
+done
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+apply (induction t arbitrary: ks)
+apply (auto simp add: list.case_eq_if)
+done    
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"    
+    
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI ks LeafI = LeafI" |
+  "deleteI ks (UnaryI b t) =
+    (case ks of
+      [] \<Rightarrow> UnaryI False t |
+      k#ks' \<Rightarrow> (if k\<longleftrightarrow>b then (UnaryI b (deleteI ks' t)) else (UnaryI b t)))" |
+  "deleteI ks (BinaryI v (l,r)) =
+    (case ks of
+      [] \<Rightarrow> BinaryI False (l,r) |
+      k#ks' \<Rightarrow> BinaryI v (if k then (l, deleteI ks' r) else (deleteI ks' l, r)))"
+
+(* Could not prove lemma *)  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  nitpick (** b/c it does not hold \<dots>*)
+sorry
+
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete ks LeafP = LeafP" |
+  "pdelete ks (NodeP ps b (l,r)) = 
+    (case split ks ps of
+       (qs,k#ks',p#ps') \<Rightarrow>
+         NodeP ps b (l,r) |
+       (qs,k#ks',[]) \<Rightarrow>
+         NodeP ps b (if k then (l, pdelete ks' r) else (pdelete ks' l, r)) |
+       (qs,[],p#ps') \<Rightarrow>
+         let t = NodeP ps' b (l,r) in
+         NodeP qs False (if p then (LeafP,t) else (t,LeafP)) |
+       (qs,[],[]) \<Rightarrow> NodeP ps False (l,r))"
+
+(* Could not prove lemma *)  
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  nitpick (** b/c it does not hold \<dots>*)
+sorry
+    
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Saporta_Antoine_Jacques_antoine.saporta@tum.de_453/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_466/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+maximilian.schaeffeler@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_466/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Schffeler_Maximilian_maximilian.schaeffeler@tum.de_466/tmpl09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,224 @@
+(** Score: 8/10
+  hw2 ptrie no proofs
+*)
+(*<*)
+theory tmpl09
+  imports "../../Material/Thys/Trie1"
+begin
+(*>*)  
+text {* \ExerciseSheet{9}{23.~6.~2017} *}
+
+text \<open>\Exercise{Union Function on Tries}
+  Define a function to merge two tries and show its correctness
+\<close>  
+fun union :: "trie \<Rightarrow> trie \<Rightarrow> trie" 
+  where "union _ _ = undefined"
+  
+    
+text \<open>
+  \Exercise{Intermediate Abstraction Level for Patricia Tries}
+
+  We introduce an abstraction level in between tries and Patricia tries:
+  A node with only a single non-leaf successor is represented as an unary node.
+
+  Via unary nodes, this implementation already introduces a notion of common prefix,
+  but does not yet summarize runs of multiple prefixes into a list.
+\<close>
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+text \<open>Refine the union function to intermediate tries\<close>
+fun unionI :: "itrie \<Rightarrow> itrie \<Rightarrow> itrie" 
+  where "unionI _ _ = undefined"
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+  
+
+text \<open>Warmup: Show that abstracting Patricia tries over intermediate 
+  tries to tries is the same as abstracting directly to tries.\<close>  
+  
+  
+text \<open>Refine the union function to Patricia tries.
+
+  Hint: First figure out how a Patricia trie that 
+    correspond to a leaf/unary/binary node looks like. 
+    Then translate @{const \<open>unionI\<close>} equation by equation!
+
+  More precisely, try to find terms \<open>unaryP\<close> and \<open>binaryP\<close> such that
+    @{term [display] "absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"}
+    @{term [display] "absI_ptrie (binaryP v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"}
+
+  You will encounter a small problem with \<open>unaryP\<close>. Which one?
+\<close>
+  
+    
+fun unionP :: "ptrie \<Rightarrow> ptrie \<Rightarrow> ptrie" 
+  where "unionP _ _ = undefined"
+    
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+fun containsword :: "trie \<Rightarrow> bool" where
+  "containsword Leaf = False" |
+  "containsword (Node True (l, r)) = True" |
+  "containsword (Node False (l, r)) = ((containsword l) \<or> (containsword r))
+"
+fun shrunk :: "trie \<Rightarrow> bool" where 
+  "shrunk Leaf = True" |
+  "shrunk (Node False (Leaf, Leaf)) = False" | 
+  "shrunk (Node v (l,r)) = ((shrunk l) \<and> (shrunk r))"
+
+lemma shrunkl: "shrunk (Node v (l,r)) \<Longrightarrow> shrunk l"
+  apply (induction l) by auto
+  
+lemma shrunkr: "shrunk (Node v (l,r)) \<Longrightarrow> shrunk r"
+  apply (induction r) by auto
+
+lemma shrunkinsertr [simp]:"shrunk (insert ks r) \<Longrightarrow> shrunk (Node b (l, r)) \<Longrightarrow> shrunk l \<Longrightarrow> shrunk (Node b (l, insert ks r))"
+  apply (induction ks r rule: insert.induct)
+  by auto
+
+lemma shrunkinsertl [simp]:"shrunk (insert ks l) \<Longrightarrow> shrunk (Node b (l, r)) \<Longrightarrow> shrunk r \<Longrightarrow> shrunk (Node b (insert ks l, r))"
+  apply (induction ks l rule: insert.induct)
+     by auto
+(*lemma [simp]: "t=(Node True tp) \<Longrightarrow> (insert ks t) = Node True tp"
+  sorry*)
+  
+lemma "shrunk Leaf"
+  by simp
+
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  apply (induction ks t rule: insert.induct)
+     apply auto
+    apply (simp only: shrunkl)
+      apply (simp only: shrunkr)
+    apply (metis insert.simps(1) insert.simps(3) list.exhaust shrunk.simps(1) shrunk.simps(3) shrunk.simps(5))
+    apply (metis insert.simps(1) insert.simps(3) list.exhaust shrunk.simps(1) shrunk.simps(4))
+    apply (simp only: shrunkl)
+   apply (simp only: shrunkr)
+   apply (auto)
+   apply (simp only: shrunkl shrunkinsertr)
+    apply (simp only: shrunkl)
+   apply (simp only: shrunkr)
+   apply (auto)
+    apply (simp only: shrunkr shrunkinsertl)
+    done
+      
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  apply (induction ks t rule: delete2.induct)
+  apply (auto split: list.split)
+  apply (simp_all only: shrunkl)
+  apply (simp_all only: shrunkr)
+  apply simp_all
+  apply (metis shrunk.elims(2) shrunk.simps(4) shrunkl)
+  apply (metis shrunk.elims(2) shrunk.simps(4) shrunkl)
+  apply (metis shrunk.elims(2) shrunk.simps(4) shrunkl)
+  apply (metis shrunk.elims(2) shrunk.simps(4) shrunkl)
+  apply (smt prod.inject shrunk.elims(3) shrunkr trie.inject)
+  apply (metis shrunk.elims(2) shrunk.simps(5) shrunkr)
+  apply (smt prod.inject shrunk.elims(3) shrunk.simps(4) trie.inject)
+  apply (metis (no_types, lifting) shrunk.elims(2) shrunk.simps(5) shrunkl)
+  apply (metis (no_types, lifting) shrunk.elims(2) shrunk.simps(4) shrunkr)
+  by (smt prod.inject shrunk.elims(3) shrunkr trie.inject)
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+    
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI" |
+  
+  "deleteI [] (UnaryI v t) = (UnaryI v t)" |
+  
+  "deleteI (True#xs) (UnaryI True t) = (UnaryI True (deleteI xs t))" |
+  "deleteI (False#xs) (UnaryI True t) = (UnaryI True t)" |
+  
+  "deleteI (False#xs) (UnaryI False t) = (UnaryI False (deleteI xs t))" |
+  "deleteI (True#xs) (UnaryI False t) = (UnaryI False t)" |
+  
+  "deleteI [] (BinaryI v (l,r)) = (BinaryI False (l,r))"|
+  
+  "deleteI (True#xs) (BinaryI v (l,r)) = (BinaryI v (l,deleteI xs r))" |
+  "deleteI (False#xs) (BinaryI v (l,r)) = (BinaryI v (deleteI xs l, r))"
+  
+lemma aux1:"abs_itrie (UnaryI v t) = delete [] (abs_itrie (UnaryI v t))"
+  apply (induction t arbitrary: v rule: itrie.induct)
+  apply auto
+  apply (smt abs_itrie.simps(2) abs_itrie.simps(3) delete.simps(2) list.simps(4))
+  apply (smt abs_itrie.simps(2) abs_itrie.simps(3) delete.simps(2) list.simps(4))
+  by (smt abs_itrie.simps(2) abs_itrie.simps(3) delete.simps(2) list.simps(4))
+  
+    
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  apply (induction ks t rule: deleteI.induct)
+  using aux1 by auto
+(*fun split where
+"split [] ys = ([],[],ys)" |
+"split xs [] = ([],xs,[])" |
+"split (x#xs) (y#ys) =
+  (if x\<noteq>y then ([],x#xs,y#ys)
+   else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
+*)    
+(*datatype ptrie = LeafP | NodeP "bool list" bool "ptrie * ptrie"*)
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete _ LeafP  = LeafP" |
+  
+  "pdelete [] (NodeP [] v (l,r)) = NodeP [] False (l,r)" |
+  "pdelete [] (NodeP (x#xs) v (l,r)) = NodeP (x#xs) v (l,r)" |
+
+  (*
+  "pdelete (False#ks) (NodeP [] v (l,r)) = NodeP [] v (pdelete ks l, r)" |
+  "pdelete (False#ks) (NodeP (False#xs) v (l,r)) = NodeP [] False (pdelete ks (NodeP xs v (l,r)), LeafP)" |
+  "pdelete (False#ks) (NodeP (True#xs) v (l,r)) = (NodeP (True#xs) v (l,r))" |
+  
+  "pdelete (True#ks) (NodeP [] v (l,r)) = NodeP [] v (l, pdelete ks r)" |
+  "pdelete (True#ks) (NodeP (True#xs) v (l,r)) = NodeP [] False (LeafP, pdelete ks (NodeP xs v (l,r)))" |
+  "pdelete (True#ks) (NodeP (False#xs) v (l,r)) = (NodeP (False#xs) v (l,r))"
+  *)
+  
+  "pdelete ks (NodeP xs v (l,r)) = (case (split ks xs) of
+   (ks, [], []) \<Rightarrow> (NodeP xs False (l,r))
+  |(ks, (True#ks'), []) \<Rightarrow> (NodeP xs v (l, pdelete ks' r))
+  |(ks, (False#ks'), []) \<Rightarrow> (NodeP xs v (pdelete ks' l, r))
+  |(_,_,_) \<Rightarrow> NodeP xs v (l,r))" 
+
+lemma aux: "absI_ptrie (pdelete ks LeafP) = deleteI ks (absI_ptrie LeafP)"
+  apply (induction ks) by auto
+    
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  apply (induction ks t rule: pdelete.induct)
+  apply auto
+  apply (auto split: list.split prod.split bool.split)
+  sorry
+    
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Somogyi_Daniel_daniel.somogyi@tum.de_459/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+daniel.somogyi@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Somogyi_Daniel_daniel.somogyi@tum.de_459/hw09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,73 @@
+(** Score: 0/10
+
+  NOTE: 
+    Thanks for this easy to correct submission, allowing me to clock off a few minutes earlier. 
+    Do not try to find more points for this submission, there are none ;)
+
+
+*)
+(*<*)
+theory hw09
+  imports "Main"
+    
+begin
+(*>*)
+
+(* NOTE: 
+  I have holidays. So I only did homeworks i could solve in 5 minutes. Don't try
+  to find more, there is nothing ;)
+*)  
+
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the delete2 function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+(* "imports" from Trie1.thy *)
+  
+datatype trie = Leaf | Node bool "trie * trie"
+
+fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"insert [] Leaf = Node True (Leaf,Leaf)" |
+"insert [] (Node b lr) = Node True lr" |
+"insert (k#ks) Leaf =
+  Node False (if k then (Leaf, insert ks Leaf)
+                   else (insert ks Leaf, Leaf))" |
+"insert (k#ks) (Node b (l,r)) =
+  Node b (if k then (l, insert ks r)
+               else (insert ks l, r))"
+fun node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
+"node b lr = (if \<not> b \<and> lr = (Leaf,Leaf) then Leaf else Node b lr)"
+
+fun delete2 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+"delete2 ks Leaf = Leaf" |
+"delete2 ks (Node b (l,r)) =
+   (case ks of
+      [] \<Rightarrow> node False (l,r) |
+      k#ks' \<Rightarrow> node b (if k then (l, delete2 ks' r) else (delete2 ks' l, r)))"
+
+(* IMPORT END ------------------------------*)
+
+(* delete 2 technically just does not leave empty nodes (with (Leaf,Leaf) as children) in the tree
+ This means, 'shrunk' can be defined as option that no node with structure (Node False (Leaf,Leaf)) exists *)
+fun shrunk :: "trie \<Rightarrow> bool" where 
+ "shrunk (Node False (Leaf,Leaf)) = False"
+|"shrunk Leaf = True"
+|"shrunk (Node _ (l,r)) = (shrunk l \<and> shrunk r)"
+  
+
+lemma "shrunk Leaf" by simp
+                
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)" 
+  sorry
+    
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)" 
+    sorry
+  
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Somogyi_Daniel_daniel.somogyi@tum.de_459/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Stevens_Lukas_lukas.stevens@tum.de_460/Ex09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,319 @@
+(** Score: 10/10
+*)
+(*<*)
+theory Ex09
+  imports "../Thys/Trie1"
+begin
+(*>*)  
+   
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+  
+fun shrunk :: "trie \<Rightarrow> bool" where 
+  "shrunk Leaf \<longleftrightarrow> True" |
+  "shrunk (Node b (Leaf,Leaf)) \<longleftrightarrow> b" |
+  "shrunk (Node _ (Leaf,r)) \<longleftrightarrow> shrunk r" |
+  "shrunk (Node _ (l,Leaf)) \<longleftrightarrow> shrunk l" |
+  "shrunk (Node _ (l,r)) \<longleftrightarrow> shrunk l \<and> shrunk r"
+
+lemma "shrunk Leaf" by simp
+
+lemma insert_not_empty: "\<exists>b st. insert ks t = Node b st"
+    by (induction ks t rule: insert.induct) auto
+    
+lemma shrunk_insert_Leaf: "shrunk (insert ks Leaf)"
+proof(induction ks)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons k ks)
+  from insert_not_empty obtain b t where "insert ks Leaf = Node b t" by blast
+  then show ?case using Cons by auto
+qed
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+proof(induction t arbitrary: ks rule: shrunk.induct)
+  case 1
+  then show ?case using shrunk_insert_Leaf by simp
+next
+  case (2 b)
+  then show ?case
+  proof(cases ks)
+    case Nil
+    then show ?thesis by simp
+  next
+    case (Cons k ks)
+    from insert_not_empty obtain b t where "insert ks Leaf = Node b t" by blast
+    then show ?thesis using Cons shrunk_insert_Leaf by auto metis
+  qed    
+next
+  case (3 b cb ct)
+  then show ?case
+  proof(cases ks)
+    case Nil
+    then show ?thesis using 3 shrunk_insert_Leaf by auto
+  next
+    case (Cons k ks)
+    then show ?thesis
+    proof(cases k)
+      case True
+      from insert_not_empty obtain ib it where ib_it_constr: "insert ks (Node cb ct) = Node ib it" by blast
+      have "shrunk (insert (k#ks) (Node b (Leaf, Node cb ct))) = 
+        shrunk (Node b (Leaf, insert ks (Node cb ct)))" using \<open>k\<close> by simp
+      also have "\<dots> = shrunk (insert ks (Node cb ct))" by(auto simp add: ib_it_constr)
+      finally have "shrunk (insert (k#ks) (Node b (Leaf, Node cb ct))) = 
+        shrunk (insert ks (Node cb ct))" .
+      then show ?thesis using Cons 3 by(auto split: if_splits)
+    next
+      case False    
+      from insert_not_empty obtain ib' it' where "insert ks Leaf = Node ib' it'" by blast
+      then show ?thesis using Cons 3 \<open>\<not>k\<close> shrunk_insert_Leaf by (auto) metis
+    qed
+  qed 
+next
+  case (4 b cb ct)
+  then show ?case
+  proof(cases ks)
+    case Nil
+    then show ?thesis using 4 shrunk_insert_Leaf by auto
+  next
+    case (Cons k ks)
+    then show ?thesis
+    proof(cases k)
+      case True
+      from insert_not_empty obtain ib' it' where "insert ks Leaf = Node ib' it'" by blast
+      then show ?thesis using Cons 4 \<open>k\<close> shrunk_insert_Leaf by (auto) metis
+    next
+      case False
+      from insert_not_empty obtain ib it where ib_it_constr: "insert ks (Node cb ct) = Node ib it" by blast
+      have "shrunk (insert (k#ks) (Node b (Node cb ct, Leaf))) = 
+        shrunk (Node b (insert ks (Node cb ct), Leaf))" using \<open>\<not>k\<close> by simp
+      also have "\<dots> = shrunk (insert ks (Node cb ct))" by(auto simp add: ib_it_constr)
+      finally have "shrunk (insert (k#ks) (Node b (Node cb ct, Leaf))) = 
+        shrunk (insert ks (Node cb ct))" .
+      then show ?thesis using Cons 4 by(auto split: if_splits)
+    qed
+  qed 
+next
+  case ("5_1" pb lb lt rb rt)
+  then show ?case
+  proof(cases ks)
+    case Nil
+    then show ?thesis using "5_1.prems" by auto
+  next
+    case (Cons k ks)
+    from insert_not_empty obtain ilb ilt where l_constr: "insert ks (Node lb lt) = Node ilb ilt" 
+      by blast
+    from insert_not_empty obtain irb irt where r_constr: "insert ks (Node rb rt) = Node irb irt" 
+      by blast
+    then show ?thesis using l_constr r_constr "5_1.prems" "5_1.IH" Cons
+      by(auto) (metis)+
+  qed 
+next
+  case ("5_2" pb lb lt rb rt)
+  then show ?case
+  proof(cases ks)
+    case Nil
+    then show ?thesis using "5_2.prems" by auto
+  next
+    case (Cons k ks)
+    from insert_not_empty obtain ilb ilt where l_constr: "insert ks (Node lb lt) = Node ilb ilt" 
+      by blast
+    from insert_not_empty obtain irb irt where r_constr: "insert ks (Node rb rt) = Node irb irt" 
+      by blast
+    then show ?thesis using l_constr r_constr "5_2.prems" "5_2.IH" Cons
+      by(auto) (metis)+
+  qed 
+qed
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+proof(induction t arbitrary: ks rule: shrunk.induct)
+  case 1
+  then show ?case by simp
+next
+  case (2 b)
+  then show ?case by(simp split: list.splits)
+next
+  case (3 pb cb ct)
+  then show ?case
+  proof(cases ks)
+    case Nil
+    then show ?thesis using 3 by simp
+  next
+    case (Cons k ks)
+    then show ?thesis using 3 Cons 
+      apply(cases "delete2 ks (Node cb ct)") by auto metis+
+  qed
+next
+  case (4 pb cb ct)
+  then show ?case 
+  proof(cases ks)
+    case Nil
+    then show ?thesis using 4 by simp
+  next
+    case (Cons k ks)
+    then show ?thesis using 4 Cons
+      apply (cases "delete2 ks (Node cb ct)") by auto metis+
+   qed
+next
+  case ("5_1" pb lb lt rb rt)
+  then show ?case
+  proof(cases ks)
+    case Nil
+    then show ?thesis using "5_1" by simp
+  next
+    case (Cons k ks)
+    then show ?thesis
+    proof(cases k)
+      case True
+      then show ?thesis using "5_1" Cons 
+         apply (cases "delete2 ks (Node rb rt)") by (auto split: list.splits) metis
+    next
+      case False
+      then show ?thesis using "5_1" Cons
+          apply(cases "delete2 ks (Node lb lt)") by (auto split: list.splits) metis
+    qed     
+  qed   
+next
+  case ("5_2" pb lb lt rb rt)
+  then show ?case
+  proof(cases ks)
+    case Nil
+    then show ?thesis using "5_2" by simp
+  next
+    case (Cons k ks)
+    then show ?thesis
+    proof(cases k)
+      case True
+      then show ?thesis using "5_2" Cons 
+         apply (cases "delete2 ks (Node rb rt)") by (auto split: list.splits) metis
+    next
+      case False
+      then show ?thesis using "5_2" Cons
+          apply(cases "delete2 ks (Node lb lt)") by (auto split: list.splits) metis
+    qed     
+  qed  
+qed
+     
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>
+
+(* Stuff from the tutorial *)
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+(* end stuff from the tutorial *)
+
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI" |
+  "deleteI [] (UnaryI b t) = UnaryI b t" |
+  "deleteI (x#xs) (UnaryI b t) = (if x = b then UnaryI b (deleteI xs t) else UnaryI b t)" |
+  "deleteI [] (BinaryI b (l,r)) = (if b then BinaryI False (l,r) else BinaryI b (l,r))" |
+  "deleteI (x#xs) (BinaryI b (l,r)) = 
+    (if x then BinaryI b (l, deleteI xs r) else BinaryI b (deleteI xs l, r))"
+  
+lemma [simp]: "delete [] (abs_itrie (UnaryI b t)) = abs_itrie (UnaryI b t)"
+proof(cases "abs_itrie (UnaryI b t)")
+  case Leaf
+  then show ?thesis by simp
+next
+  case (Node x21 x22)
+  then show ?thesis using abs_itrie.elims by force
+qed
+    
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+proof(induction ks t rule: deleteI.induct)
+  case (1 ks)
+  then show ?case by auto
+next
+  case (2 b t)
+  then show ?case by auto
+next
+  case (3 x xs b t)
+  then show ?case by auto
+next
+  case (4 b l r)
+  then show ?case by auto
+next
+  case (5 x xs b l r)
+  then show ?case by auto
+qed
+
+fun cons_prefix :: "bool \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+  "cons_prefix _ LeafP = undefined" |
+  "cons_prefix x (NodeP xs b t) = NodeP (x#xs) b t"
+   
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete _ LeafP = LeafP" |
+  "pdelete [] (NodeP [] b t) = NodeP [] False t" |
+  "pdelete [] (NodeP (y#ys) b t) = NodeP (y#ys) b t" |
+  "pdelete (x#xs) (NodeP [] b (l,r)) = 
+    (if x then NodeP [] b (l, pdelete xs r) else NodeP [] b (pdelete xs l, r))" |
+  "pdelete (x#xs) (NodeP (y#ys) b (l,r)) = 
+    (if x \<noteq> y then NodeP (y#ys) b (l,r)
+    else cons_prefix x (pdelete xs (NodeP ys b (l,r))))"
+    
+lemma absI_cons_prefix: "t \<noteq> LeafP \<Longrightarrow> absI_ptrie (cons_prefix y t) = UnaryI y (absI_ptrie t)"
+  by (induction t) auto
+
+lemma pdelete_Node: "t \<noteq> LeafP \<Longrightarrow> pdelete xs t \<noteq> LeafP"
+  apply (induction xs t rule: pdelete.induct) 
+      apply(auto) 
+  using cons_prefix.elims by blast
+    
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+proof(induction ks t rule: pdelete.induct)
+  case (1 xs)
+  then show ?case by simp
+next
+  case (2 b t)
+  then show ?case by (cases t) auto
+next
+  case (3 y ys b t)
+  then show ?case by (cases t) auto
+next
+  case (4 x xs b l r)
+  then show ?case by auto
+next
+  case (5 x xs y ys b l r)
+  then show ?case
+  proof(cases xs)
+    case Nil
+    then show ?thesis by (cases ys) auto
+  next
+    case (Cons x' xs')
+    then show ?thesis using 5 by(auto simp add: absI_cons_prefix pdelete_Node)
+  qed
+qed
+      
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Stevens_Lukas_lukas.stevens@tum.de_460/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+lukas.stevens@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Stevens_Lukas_lukas.stevens@tum.de_460/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Stwe_Daniel_daniel.stuewe@tum.de_462/HW09b.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,87 @@
+(** Score: 10/10
+*)
+theory HW09b
+  imports "Material/Thys/Trie1"
+          "~~/src/HOL/Data_Structures/Cmp"
+begin
+
+declare [[names_short]]  
+
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+ 
+fun shrunk :: "trie \<Rightarrow> bool" where
+ "shrunk Leaf = True" | 
+ "shrunk (Node False (Leaf, Leaf)) = False" |
+ "shrunk (Node b (l, r)) = (shrunk l \<and> shrunk r)"
+ 
+lemma [simp]: "shrunk (Node b (l, r)) = ((shrunk l \<and> shrunk r \<and> (l \<noteq> Leaf \<or> r \<noteq> Leaf)
+                               \<or> (l = Leaf \<and> r = Leaf \<and> b = True)))"
+  by (cases b; cases l; cases r; simp)
+   
+lemma "shrunk Leaf" by simp
+  
+lemma "shrunk t \<Longrightarrow> shrunk (Trie1.insert ks t)"
+  apply (induction ks t  rule: Trie1.insert.induct)
+  apply (simp_all, safe)+ 
+  using Trie1.isin.simps(1) isin_insert apply metis+
+done 
+    
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)" 
+  by (induction ks t rule: Trie1.delete2.induct) (auto split: list.splits)  
+      
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI _ LeafI = LeafI" |
+  "deleteI [] (UnaryI b t) = UnaryI b t" |
+  "deleteI [] (BinaryI _ tpl) = BinaryI False tpl" |
+  "deleteI (k#ks) (UnaryI b t) = UnaryI b (if k = b then deleteI ks t else t)" |
+  "deleteI (k#ks) (BinaryI b (l,r)) = BinaryI b (if k then (l, deleteI ks r) else (deleteI ks l, r))"  
+
+lemma [simp]: "abs_itrie (UnaryI b t) = Node False (if b then (Leaf, abs_itrie t) else (abs_itrie t, Leaf))"
+  by auto
+    
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)" 
+  by (induction ks t rule: deleteI.induct) auto
+   
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  where  
+  "pdelete _ LeafP = LeafP" |
+  "pdelete ks (NodeP ps b (l,r)) = 
+    (case split ks ps of
+      (_, k#ks', []) \<Rightarrow> NodeP ps b (if k then (l, pdelete ks' r) else (pdelete ks' l, r)) |
+      (_, _ , p#ps') \<Rightarrow> NodeP ps b (l,r) |
+      (_, [], []) \<Rightarrow> NodeP ps False (l,r))"
+
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+proof (induction ks arbitrary: t)
+  case (Nil)
+  then show ?case  by (cases t)  (auto  split: prod.splits list.splits )
+next
+  case (Cons k' ks' t)         
+  show ?case proof (cases t)
+    case (NodeP ps l r)
+    then show ?thesis
+      by (cases ps; cases r)
+         (auto simp: Cons.IH[symmetric] split: prod.splits list.splits)   
+  qed (auto split: prod.splits list.splits )
+qed
+
+    
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Stwe_Daniel_daniel.stuewe@tum.de_462/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+daniel.stuewe@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Stwe_Daniel_daniel.stuewe@tum.de_462/user_error_log.txt	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,6 @@
+Using temporary directory '/tmp/tmp.vOPNlDtdkp'
+Files in /tmp/eval-462-IgiyUN: HW09b.thy
+Submission did not check in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_479/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+sreeharsha.totakura@mytum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_479/hw09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,197 @@
+(** Score: 8/10
+  hw2 ptrie proofs missing
+*)
+(*<*)
+theory hw09
+  imports "../../fds_ss17/Thys/Trie1"
+begin
+(*>*)  
+text {* \ExerciseSheet{9}{23.~6.~2017} *}
+
+text \<open>\Exercise{Union Function on Tries}
+  Define a function to merge two tries and show its correctness
+\<close>  
+fun union :: "trie \<Rightarrow> trie \<Rightarrow> trie" 
+  where "union _ _ = undefined"
+  
+    
+text \<open>
+  \Exercise{Intermediate Abstraction Level for Patricia Tries}
+
+  We introduce an abstraction level in between tries and Patricia tries:
+  A node with only a single non-leaf successor is represented as an unary node.
+
+  Via unary nodes, this implementation already introduces a notion of common prefix,
+  but does not yet summarize runs of multiple prefixes into a list.
+\<close>
+  
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+text \<open>Refine the union function to intermediate tries\<close>
+fun unionI :: "itrie \<Rightarrow> itrie \<Rightarrow> itrie" 
+  where "unionI _ _ = undefined"
+
+text \<open>Next, we define an abstraction function from Patricia tries to intermediate tries.
+  Note that we need to install a custom measure function to get the termination proof through!
+\<close>
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+  
+
+text \<open>Warmup: Show that abstracting Patricia tries over intermediate 
+  tries to tries is the same as abstracting directly to tries.\<close>  
+  
+  
+text \<open>Refine the union function to Patricia tries.
+
+  Hint: First figure out how a Patricia trie that 
+    correspond to a leaf/unary/binary node looks like. 
+    Then translate @{const \<open>unionI\<close>} equation by equation!
+
+  More precisely, try to find terms \<open>unaryP\<close> and \<open>binaryP\<close> such that
+    @{term [display] "absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"}
+    @{term [display] "absI_ptrie (binaryP v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"}
+
+  You will encounter a small problem with \<open>unaryP\<close>. Which one?
+\<close>
+  
+    
+fun unionP :: "ptrie \<Rightarrow> ptrie \<Rightarrow> ptrie" 
+  where "unionP _ _ = undefined"
+  
+    
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" where
+ "shrunk Leaf = True" |
+ "shrunk (Node b (l,r)) =
+ (if \<not>b \<and> l = Leaf \<and> r = Leaf then False else shrunk l \<and> shrunk r)"
+
+lemma "shrunk Leaf" by simp
+
+lemma insert_leaf_neq_leaf: "insert xs t \<noteq> Leaf"
+  apply (induct xs t rule: insert.induct)
+   apply auto
+  done
+    
+lemma shrunk_insert: "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  apply (induction ks t rule:insert.induct)
+   apply (auto simp add:insert_leaf_neq_leaf)+
+     apply presburger+
+  done
+    
+lemma shrunk_delete2: "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+  apply (induction ks t rule:delete2.induct)
+  apply (auto split:list.splits)
+  done
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  "deleteI ks LeafI = LeafI" |
+  "deleteI [] (UnaryI True t) = UnaryI True t"|
+  "deleteI [] (UnaryI False t) = UnaryI False t"|
+  "deleteI (True # xs) (UnaryI True t) =
+     UnaryI True (deleteI xs t)" |
+  "deleteI (True # xs) (UnaryI False t) =
+     UnaryI False t" |
+
+  "deleteI (False # xs) (UnaryI True t) =
+     UnaryI True t" |
+  "deleteI (False # xs) (UnaryI False t) =
+     UnaryI False (deleteI xs t)" |
+  "deleteI [] (BinaryI b (l,r)) = BinaryI False (l,r)" |
+  "deleteI (x # xs) (BinaryI b (l,r)) =
+     BinaryI b (if x then (l, deleteI xs r) else (deleteI xs l, r))"
+thm deleteI.simps
+lemma [simp]:
+ "t = BinaryI b (LeafI, LeafI) \<Longrightarrow> deleteI [] t = BinaryI False (LeafI,LeafI)"
+  apply (cases t)
+  by auto
+
+lemma deleteI_correctness:
+ "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  apply (induction ks t rule:deleteI.induct) by auto
+
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where  
+  "pdelete ks LeafP = LeafP" |
+  "pdelete [] (NodeP [] b (l,r)) = NodeP [] False (l,r)" |
+  "pdelete [] (NodeP ps b (l,r)) = NodeP ps b (l,r)" |
+  "pdelete (k#ks) (NodeP [] b (l,r)) =
+     NodeP [] b (if k then (l, pdelete ks r) else (pdelete ks l, r))" |
+  "pdelete ks (NodeP ps b (l,r)) =
+    (case split ks ps of
+     (qs, [], []) \<Rightarrow> NodeP ps False (l,r) |
+     (qs, k#ks', []) \<Rightarrow> NodeP ps b (if k then (l, pdelete ks' r) else (pdelete ks' l, r)) |
+     (qs, _, p#ps') \<Rightarrow> NodeP ps b (l,r)
+    )"
+print_statement pdelete.induct
+lemma d1: "deleteI [] (UnaryI b t) = UnaryI b t"
+  apply (cases b) by auto
+
+lemma d2[simp]:
+ "deleteI (p#ps) (UnaryI p t) = UnaryI p (deleteI ps t)"
+  apply (cases p) by auto
+    
+lemma d3:
+  "deleteI (p#ps) (UnaryI (\<not>p) t) = UnaryI (\<not>p) t"
+  apply (cases p) by auto
+    
+lemma d4:
+  "deleteI ((\<not>p) # ps) (UnaryI p t) = UnaryI p t"
+  using d3[of "\<not>p"] by simp
+
+lemma split_aux: "split xs ys = (zs, [], []) \<Longrightarrow> xs = ys \<and> zs = xs"
+  apply (induction xs ys arbitrary:zs rule:split.induct)
+    apply (auto split:prod.splits if_splits)
+  done
+  
+lemma d5[simp]:
+  "absI_ptrie (NodeP v False (l, r)) = deleteI v (absI_ptrie (NodeP v b (l, r)))"
+  apply (induct v)
+   apply simp
+  apply simp
+  done
+
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+  apply (induction ks t rule:pdelete.induct)
+      apply simp
+     apply simp
+    apply (simp add:d1)
+    apply simp
+   apply auto
+  using d4 apply auto
+   apply (auto split:prod.splits list.splits simp:d1 d3 d4)
+  using split_aux apply fastforce
+    (**sledgehammer*) oops
+    
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Totakura_Sree_Harsha_sreeharsha.totakura@mytum.de_479/user_error_log.txt	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,6 @@
+Using temporary directory '/tmp/tmp.SipgD24itk'
+Files in /tmp/eval-479-WlFC0L: hw09.thy
+Submission did not check in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Wauligmann_Martin_martin.wauligmann@tum.de_475/SENTMAIL	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,1 @@
+martin.wauligmann@tum.de
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Wauligmann_Martin_martin.wauligmann@tum.de_475/hw09.thy	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,85 @@
+(** Score: 0/10
+  no proofs
+*)
+theory hw09
+  imports "../../Material/Thys/Trie1"
+begin
+
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+    
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+
+(* Homework 9.1 Shrunk Trees *)
+ 
+fun shrunk :: "trie \<Rightarrow> bool" where
+"shrunk Leaf = True" |
+"shrunk (Node b (Leaf,Leaf)) = b" |
+"shrunk (Node b (l,r)) = (shrunk l \<and> shrunk r)"
+
+lemma "shrunk Leaf" by simp
+
+lemma shrunk_node: "shrunk(Node b lr) \<Longrightarrow> shrunk(Node True lr)"
+by (smt shrunk.elims(3) shrunk.simps(3) shrunk.simps(4) trie.inject)
+  
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+apply(induction ks t rule: insert.induct)
+apply (simp add: isin_insert)
+apply (simp add: shrunk_node)
+apply (smt insert.simps(1) insert.simps(3) neq_Nil_conv shrunk.simps(3) shrunk.simps(4))
+apply (auto split: if_splits)
+sorry
+
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"
+apply (induction arbitrary: ks rule: shrunk.induct)
+apply (force split: list.splits)
+apply (simp add: list.case_eq_if)
+sorry
+
+
+(* Homework 9.2 Refining Delete *)
+
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+"deleteI ks LeafI = LeafI" |
+"deleteI ks (UnaryI v t) =
+   (case ks of
+      [] \<Rightarrow> UnaryI v t |
+      k#ks' \<Rightarrow> UnaryI v (deleteI ks' t))" |
+"deleteI ks (BinaryI v (l,r)) =
+   (case ks of
+      [] \<Rightarrow> BinaryI False (l,r) |
+      k#ks' \<Rightarrow> BinaryI v (if k then (l, deleteI ks' r) else (deleteI ks' l, r)))"
+  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+apply (induction ks t rule: deleteI.induct)
+sorry
+
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where  
+"pdelete ks LeafP = LeafP" |
+"pdelete ks (NodeP ps b (l,r)) = 
+   (case ks of
+      [] \<Rightarrow> NodeP ps False (l,r) |
+      k#ks' \<Rightarrow> NodeP ps b (if k then (l, pdelete ks' r) else (pdelete ks' l, r)))"
+  
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"
+apply (induction ks t rule: pdelete.induct)
+sorry
+    
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/Wauligmann_Martin_martin.wauligmann@tum.de_475/testoutput.html	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,24 @@
+
+<html>
+<head>
+<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.7/css/bootstrap.min.css">
+</head>
+<body>
+<h3>1/1 test cases passed!</h3>
+
+<table class="table">
+<thead>
+<tr>
+<th>Test Case</th><th>Passed</th>
+</tr>
+</thead>
+<tbody>
+
+<tr><td>check_build</td><td>Passed</td></tr>
+
+</tbody>
+</table>
+
+</body>
+</html>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsubm/09/meta.csv	Thu Jul 06 14:57:19 2017 +0200
@@ -0,0 +1,19 @@
+"445","fabio.madge@tum.de","Madge Pimentel","Fabio","INVALID"
+"453","antoine.saporta@tum.de","Saporta","Antoine Jacques","http://vmnipkow3.in.tum.de/web/submissions/453"
+"455","shuwei.hu@tum.de","Hu","Shuwei","http://vmnipkow3.in.tum.de/web/submissions/455"
+"456","f.hellauer@tum.de","Hellauer","Fabian","http://vmnipkow3.in.tum.de/web/submissions/456"
+"458","max.haslbeck@mytum.de","Haslbeck","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/458"
+"459","daniel.somogyi@tum.de","Somogyi","Daniel","http://vmnipkow3.in.tum.de/web/submissions/459"
+"460","lukas.stevens@tum.de","Stevens","Lukas","http://vmnipkow3.in.tum.de/web/submissions/460"
+"462","daniel.stuewe@tum.de","Stwe","Daniel","http://vmnipkow3.in.tum.de/web/submissions/462"
+"463","markus.grosser@tum.de","Groer","Markus","http://vmnipkow3.in.tum.de/web/submissions/463"
+"465","ga95luy@mytum.de","Hutzler","Matthias","http://vmnipkow3.in.tum.de/web/submissions/465"
+"466","maximilian.schaeffeler@tum.de","Schffeler","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/466"
+"467","simon.rosskopf@tum.de","Rokopf","Simon","http://vmnipkow3.in.tum.de/web/submissions/467"
+"468","friedrich.kurz@tum.de","Kurz","Friedrich","http://vmnipkow3.in.tum.de/web/submissions/468"
+"469","julian.biendarra@tum.de","Biendarra","Julian","http://vmnipkow3.in.tum.de/web/submissions/469"
+"471","levon.oganyan@tum.de","Oganyan","Levon","http://vmnipkow3.in.tum.de/web/submissions/471"
+"472","ga96vup@mytum.de","Ouyang","Lena","http://vmnipkow3.in.tum.de/web/submissions/472"
+"475","martin.wauligmann@tum.de","Wauligmann","Martin","http://vmnipkow3.in.tum.de/web/submissions/475"
+"477","ga48kog@mytum.de","Erhard","Julian","http://vmnipkow3.in.tum.de/web/submissions/477"
+"479","sreeharsha.totakura@mytum.de","Totakura","Sree Harsha","http://vmnipkow3.in.tum.de/web/submissions/479"