--- /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","Stüwe","Daniel","http://vmnipkow3.in.tum.de/web/submissions/462"
+"463","markus.grosser@tum.de","Großer","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","Schäffeler","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/466"
+"467","simon.rosskopf@tum.de","Roßkopf","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"