diff --git a/01/ex01.pdf b/01/ex01.pdf
new file mode 100644
index 0000000..8c14ff6
Binary files /dev/null and b/01/ex01.pdf differ
diff --git a/01/ex01.thy b/01/ex01.thy
new file mode 100644
index 0000000..632cb26
--- /dev/null
+++ b/01/ex01.thy
@@ -0,0 +1,63 @@
+theory ex01
+  imports Main
+begin
+
+term "op+"
+
+lemma "a + b = b + (a :: nat)"
+  by auto
+
+lemma "a + (b + c) = (a + b) + (c::nat)"
+  by auto
+
+term "Nil"
+term "Cons a b"
+
+fun count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
+  "count [] _ = 0"
+| "count (x#xs) y = (if x=y then count xs y + 1 else count xs y)"
+
+fun count' :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
+  "count' [] _ = 0"
+| "count' (x # xs) y = (if x = y then 1 else 0) + count' xs y"
+
+value "count [1,2,3,4,2,2,2::int] 2"
+
+find_theorems "length [] = _"
+find_theorems "length (_ # _) =  _"
+
+lemma "count xs a \<le> length xs"
+  apply(induction xs)
+   apply(simp)
+  apply(simp)
+  done
+
+fun snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
+  "snoc [] y = [y]"
+| "snoc (x # xs) y = x # snoc xs y"
+
+lemma "snoc xs x = xs@[x]"
+  apply(induction xs) by auto
+
+fun reverse :: "'a list \<Rightarrow> 'a list" where
+  "reverse [] = []"
+| "reverse (x # xs) = snoc (reverse xs) x"
+
+lemma aux: "reverse (snoc xs x) = x # reverse xs"
+  apply(induction xs) by auto
+
+lemma rev_rev[simp]: "reverse (reverse xs) = xs"
+  apply (induction xs)
+   apply (auto simp:aux)
+  done
+
+lemma "reverse (reverse xs) = xs"
+  apply(induction xs)
+   apply(auto simp:)
+  apply(subst aux)
+  apply auto
+  done
+
+
+  
+end
\ No newline at end of file
diff --git a/01/ex01.thy~ b/01/ex01.thy~
new file mode 100644
index 0000000..39b2149
--- /dev/null
+++ b/01/ex01.thy~
@@ -0,0 +1,34 @@
+theory ex01
+  imports Main
+begin
+
+term "op+"
+
+lemma "a + b = b + (a :: nat)"
+  by auto
+
+lemma "a + (b + c) = (a + b) + (c::nat)"
+  by auto
+
+term "Nil"
+term "Cons a b"
+
+fun count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
+  "count [] _ = 0"
+| "count (x#xs) y = (if x=y then count xs y + 1 else count xs y)"
+
+fun count' :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
+  "count' [] _ = 0"
+| "count' (x # xs) y = (if x = y then 1 else 0) + count' xs y"
+
+value "count [1,2,3,4,2,2,2::int] 2"
+
+find_theorems "length [] = _"
+find_theorems "length (_ # _) =  _"
+
+lemma "count xs a \<le> length xs"
+  apply(induction xs)
+   apply(simp)
+  apply(simp)
+  done
+end
\ No newline at end of file
diff --git a/01/ex0104.thy b/01/ex0104.thy
new file mode 100644
index 0000000..a61880d
--- /dev/null
+++ b/01/ex0104.thy
@@ -0,0 +1,11 @@
+theorem ex0104
+  imports Main
+begin
+
+term "op#"
+
+fun snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
+  "snoc [] y = [y]"
+| "snoc (x # xs) y = x # snoc xs y"
+
+end
\ No newline at end of file
diff --git a/01/hw01.thy b/01/hw01.thy
new file mode 100644
index 0000000..24ae11e
--- /dev/null
+++ b/01/hw01.thy
@@ -0,0 +1,45 @@
+theory hw01
+  imports Main
+begin
+
+fun listsum:: "int list \<Rightarrow> int" where
+  "listsum [] = 0"
+| "listsum (x # xs) =  listsum xs + x"
+
+value "listsum [1,2,3] = 6"
+value "listsum [] = 0"
+value "listsum [1,-2,3] = 2"
+
+lemma listsum_filter_x: "listsum (filter (\<lambda>x. x\<noteq>0) l) = listsum l"
+  apply(induction l)
+  apply(auto)
+  done
+
+lemma listsum_append: "listsum (xs @ ys) = listsum xs + listsum ys"
+  apply(induction xs)
+   apply(auto)
+  done
+
+lemma listsum_rev: "listsum (rev xs) = listsum xs"
+  apply(induction xs)
+   apply(auto simp:listsum_append)
+  done
+
+lemma listsum_noneg: "listsum (filter (\<lambda>x. x>0) l) \<ge> listsum l"
+  apply(induction l)
+   apply(auto)
+  done
+
+fun flatten :: "'a list list \<Rightarrow> 'a list" where
+  "flatten [] = []"
+| "flatten (l#ls) = l @ flatten ls"
+
+value "flatten [[1,2,3],[2]] = [1,2,3,2::int]"
+value "flatten [[1,2,3],[],[2]] = [1,2,3,2::int]"
+
+lemma "listsum (flatten xs) = listsum(map listsum xs)"
+  apply(induction xs)
+  apply(auto simp:listsum_append)
+  done
+
+end
\ No newline at end of file
diff --git a/01/hw01.thy~ b/01/hw01.thy~
new file mode 100644
index 0000000..24ae11e
--- /dev/null
+++ b/01/hw01.thy~
@@ -0,0 +1,45 @@
+theory hw01
+  imports Main
+begin
+
+fun listsum:: "int list \<Rightarrow> int" where
+  "listsum [] = 0"
+| "listsum (x # xs) =  listsum xs + x"
+
+value "listsum [1,2,3] = 6"
+value "listsum [] = 0"
+value "listsum [1,-2,3] = 2"
+
+lemma listsum_filter_x: "listsum (filter (\<lambda>x. x\<noteq>0) l) = listsum l"
+  apply(induction l)
+  apply(auto)
+  done
+
+lemma listsum_append: "listsum (xs @ ys) = listsum xs + listsum ys"
+  apply(induction xs)
+   apply(auto)
+  done
+
+lemma listsum_rev: "listsum (rev xs) = listsum xs"
+  apply(induction xs)
+   apply(auto simp:listsum_append)
+  done
+
+lemma listsum_noneg: "listsum (filter (\<lambda>x. x>0) l) \<ge> listsum l"
+  apply(induction l)
+   apply(auto)
+  done
+
+fun flatten :: "'a list list \<Rightarrow> 'a list" where
+  "flatten [] = []"
+| "flatten (l#ls) = l @ flatten ls"
+
+value "flatten [[1,2,3],[2]] = [1,2,3,2::int]"
+value "flatten [[1,2,3],[],[2]] = [1,2,3,2::int]"
+
+lemma "listsum (flatten xs) = listsum(map listsum xs)"
+  apply(induction xs)
+  apply(auto simp:listsum_append)
+  done
+
+end
\ No newline at end of file
diff --git a/02/ex02.pdf b/02/ex02.pdf
new file mode 100644
index 0000000..5256b59
Binary files /dev/null and b/02/ex02.pdf differ
diff --git a/02/ex02.thy b/02/ex02.thy
new file mode 100644
index 0000000..2d43888
--- /dev/null
+++ b/02/ex02.thy
@@ -0,0 +1,67 @@
+theory ex02
+  imports Main
+begin
+
+datatype 'a ltree = Leaf 'a | Node "'a ltree" "'a ltree" 
+
+fun inorder:: "'a ltree \<Rightarrow> 'a list" where
+  "inorder (Leaf x) = [x]"
+| "inorder (Node l r) = inorder l @ inorder r"
+
+lemma
+  "fold f [] s = s"
+  "fold f (x # xs) s = fold f xs (f x s)"
+  by auto
+
+fun fold_tree:: "('b \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b ltree \<Rightarrow> 'a \<Rightarrow> 'a" where
+  "fold_tree f (Leaf b) a = f b a"
+| "fold_tree f (Node l r) a = fold_tree f r (fold_tree f l a)"
+
+value "fold_tree
+(\<lambda>x y. x + y)
+(Node (Leaf (1::nat)) (Node (Leaf 2) (Leaf 4)))
+0
+"
+
+lemma "fold_tree f t s = fold f (inorder t) s"
+  apply(induction t arbitrary: s)
+   apply(auto)
+  done
+
+fun mirror:: "'a ltree \<Rightarrow> 'a ltree" where
+  "mirror (Leaf a) = Leaf a"
+| "mirror (Node l r) = Node (mirror r) (mirror l)"
+
+lemma "inorder (mirror t) = rev (inorder t)"
+  by (induction t) auto
+
+fun shuffles:: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
+  "shuffles [] ys = [ys]"
+| "shuffles xs [] = [xs]"
+| "shuffles (x#xs) (y#ys) = 
+    map(op # x) (shuffles xs (y#ys)) 
+    @ map(op # y) (shuffles (x#xs) ys)"
+
+lemma "l\<in>set (shuffles xs ys) \<Longrightarrow> length l = length xs + length ys"
+  apply(induction xs ys arbitrary: l rule: shuffles.induct)
+    apply(auto)
+  done
+
+fun list_sum :: "nat list \<Rightarrow> nat" where
+  "list_sum [] = 0"
+| "list_sum (x#xs) = x + list_sum xs"
+
+definition "list_sum' xs = fold (op +) xs 0"
+
+lemma auxi: "fold (op +) xs a = list_sum xs + a"
+  apply(induction xs arbitrary: a)
+   apply(auto)
+  done
+
+lemma "list_sum xs = list_sum' xs"
+  unfolding list_sum'_def
+  using auxi[where a=0]
+  apply auto
+  done
+
+end
\ No newline at end of file
diff --git a/02/ex0202.thy b/02/ex0202.thy
new file mode 100644
index 0000000..f2c6c76
--- /dev/null
+++ b/02/ex0202.thy
@@ -0,0 +1,7 @@
+theory ex0202
+  imports Main
+begin
+
+
+
+end
\ No newline at end of file
diff --git a/02/hw02.thy b/02/hw02.thy
new file mode 100644
index 0000000..20b6038
--- /dev/null
+++ b/02/hw02.thy
@@ -0,0 +1,105 @@
+theory hw02
+  imports Main
+begin
+
+fun collect:: "'a \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b list" where
+  "collect x [] = []"
+| "collect x ((k,y)#xs) = (if x = k then y # collect x xs else collect x xs)"
+
+definition ctest :: " (int * int) list" where "ctest = [
+(2 ,3 ),(2 ,5 ),(2 ,7 ),(2 ,9 ),
+(3 ,2 ),(3 ,4 ),(3 ,5 ),(3 ,7 ),(3 ,8 ),
+(4 ,3 ),(4 ,5 ),(4 ,7 ),(4 ,9 ),
+(5 ,2 ),(5 ,3 ),(5 ,4 ),(5 ,6 ),(5 ,7 ),(5 ,8 ),(5 ,9 ),
+(6 ,5 ),(6 ,7 ),
+(7 ,2 ),(7 ,3 ),(7 ,4 ),(7 ,5 ),(7 ,6 ),(7 ,8 ),(7 ,9 ),
+(8 ,3 ),(8 ,5 ),(8 ,7 ),(8 ,9 ),
+(9 ,2 ),(9 ,4 ),(9 ,5 ),(9 ,7 ),(9 ,8 )
+]"
+value "collect 3 ctest = [2 ,4 ,5 ,7, 8 ]"
+value "collect 1 ctest = []"
+
+lemma "collect x ys = map snd (filter (\<lambda>kv. fst kv = x) ys)"
+  apply(induction ys)
+   apply(auto)
+  done
+
+fun collect_tr:: "'b list \<Rightarrow> 'a \<Rightarrow> ('a * 'b) list \<Rightarrow> 'b list" where
+  "collect_tr acc x [] = rev acc"
+| "collect_tr acc x ((k,v)#ys) = (if (x = k) then collect_tr (v # acc) x ys else collect_tr acc x ys)"
+
+lemma collect_gen:"collect_tr acc x ys = rev acc @ (collect x ys)"
+  apply(induction ys arbitrary:acc)
+   apply(auto)
+  done
+
+lemma "collect_tr [] x ys = collect x ys"
+  apply(induction ys)
+   apply(auto simp:collect_gen)
+  done
+
+
+
+
+
+
+datatype 'a ltree = Leaf 'a | Node "'a ltree" "'a ltree" 
+
+fun lheight:: "'a ltree \<Rightarrow> nat" where
+  "lheight (Leaf x) = 0"
+| "lheight (Node x y) = max (lheight x) (lheight y) + 1"
+
+value "lheight (Node (Leaf (1::nat)) (Node (Leaf 2) (Leaf 4)))"
+
+fun num_leafs:: "'a ltree \<Rightarrow> nat" where
+  "num_leafs (Leaf x) = 1"
+| "num_leafs (Node x y) = num_leafs x + num_leafs y"
+
+value "num_leafs (Node (Leaf (1::nat)) (Node (Leaf 2) (Leaf 4)))"
+
+fun balanced:: "'a ltree \<Rightarrow> bool" where
+  "balanced (Leaf a) = True"
+| "balanced (Node x y) = (op &)((op &)(lheight x = lheight y)(balanced x))(balanced y)"
+
+value "balanced (Node (Node (Leaf a\<^sub>1) (Node (Leaf a\<^sub>1) (Leaf a\<^sub>1))) (Node (Leaf a\<^sub>1) (Node (Leaf a\<^sub>1) (Leaf a\<^sub>1))))"
+
+
+lemma "balanced t \<Longrightarrow> num_leafs t = 2 ^ lheight t"
+  apply(induction t)
+  apply(auto)
+  done
+
+
+
+
+
+
+fun denc :: "int \<Rightarrow> int list \<Rightarrow> int list" where
+  "denc a [] = []"
+| "denc a (x#xs) = (x-a) # denc x xs"
+
+value "denc 0 [1,2,4,8]"
+value "denc 0 [3,4,5]"
+value "denc 0 [5]"
+value "denc 0 []"
+
+fun ddec :: "int \<Rightarrow> int list \<Rightarrow> int list" where
+  "ddec a [] = []"
+| "ddec (a::int) (x#xs) = (x + a) # (ddec (x + a) xs)"
+
+value "ddec 0 [1,1,2,4]"
+value "ddec 0 [3,1,1]"
+value "ddec 0 [5]"
+value "ddec 0 []"
+
+value "ddec 5 (denc 4 [1,2,3])"
+
+lemma encdecgen: "ddec n (denc n l) = l"
+  apply(induction l arbitrary:n)
+  by auto
+
+lemma "ddec 0 (denc 0 l) = l"
+  apply(auto simp:encdecgen)
+  done
+
+end
\ No newline at end of file
diff --git a/02/hw02.thy~ b/02/hw02.thy~
new file mode 100644
index 0000000..37a51fa
--- /dev/null
+++ b/02/hw02.thy~
@@ -0,0 +1,105 @@
+theory hw02
+  imports Main
+begin
+
+fun collect:: "'a \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b list" where
+  "collect x [] = []"
+| "collect x ((k,y)#xs) = (if x = k then y # collect x xs else collect x xs)"
+
+definition ctest :: " (int * int) list" where "ctest = [
+(2 ,3 ),(2 ,5 ),(2 ,7 ),(2 ,9 ),
+(3 ,2 ),(3 ,4 ),(3 ,5 ),(3 ,7 ),(3 ,8 ),
+(4 ,3 ),(4 ,5 ),(4 ,7 ),(4 ,9 ),
+(5 ,2 ),(5 ,3 ),(5 ,4 ),(5 ,6 ),(5 ,7 ),(5 ,8 ),(5 ,9 ),
+(6 ,5 ),(6 ,7 ),
+(7 ,2 ),(7 ,3 ),(7 ,4 ),(7 ,5 ),(7 ,6 ),(7 ,8 ),(7 ,9 ),
+(8 ,3 ),(8 ,5 ),(8 ,7 ),(8 ,9 ),
+(9 ,2 ),(9 ,4 ),(9 ,5 ),(9 ,7 ),(9 ,8 )
+]"
+value "collect 3 ctest = [2 ,4 ,5 ,7, 8 ]"
+value "collect 1 ctest = []"
+
+lemma "collect x ys = map snd (filter (\<lambda>kv. fst kv = x) ys)"
+  apply(induction ys)
+   apply(auto)
+  done
+
+fun collect_tr:: "'b list \<Rightarrow> 'a \<Rightarrow> ('a * 'b) list \<Rightarrow> 'b list" where
+  "collect_tr acc x [] = rev acc"
+| "collect_tr acc x ((k,v)#ys) = (if (x = k) then collect_tr (v # acc) x ys else collect_tr acc x ys)"
+
+lemma collect_gen:"collect_tr acc x ys = rev acc @ (collect x ys)"
+  apply(induction ys arbitrary:acc)
+   apply(auto)
+  done
+
+lemma "collect_tr [] x ys = collect x ys"
+  apply(induction ys)
+   apply(auto simp:collect_gen)
+  done
+
+
+
+
+
+
+datatype 'a ltree = Leaf 'a | Node "'a ltree" "'a ltree" 
+
+fun lheight:: "'a ltree \<Rightarrow> nat" where
+  "lheight (Leaf x) = 0"
+| "lheight (Node x y) = max (lheight x) (lheight y) + 1"
+
+value "lheight (Node (Leaf (1::nat)) (Node (Leaf 2) (Leaf 4)))"
+
+fun num_leafs:: "'a ltree \<Rightarrow> nat" where
+  "num_leafs (Leaf x) = 1"
+| "num_leafs (Node x y) = num_leafs x + num_leafs y"
+
+value "num_leafs (Node (Leaf (1::nat)) (Node (Leaf 2) (Leaf 4)))"
+
+fun balanced:: "'a ltree \<Rightarrow> bool" where
+  "balanced (Leaf a) = True"
+| "balanced (Node x y) = (if (lheight x = lheight y) then (op &)(balanced x)(balanced y)  else False)"
+
+value "balanced (Node (Node (Leaf a\<^sub>1) (Node (Leaf a\<^sub>1) (Leaf a\<^sub>1))) (Node (Leaf a\<^sub>1) (Node (Leaf a\<^sub>1) (Leaf a\<^sub>1))))"
+
+
+lemma "balanced t \<longrightarrow> num_leafs t = 2 ^ lheight t"
+  apply(induction t)
+  apply(auto)
+  done
+
+
+
+
+
+
+fun denc :: "int \<Rightarrow> int list \<Rightarrow> int list" where
+  "denc a [] = []"
+| "denc a (x#xs) = (x-a) # denc x xs"
+
+value "denc 0 [1,2,4,8]"
+value "denc 0 [3,4,5]"
+value "denc 0 [5]"
+value "denc 0 []"
+
+fun ddec :: "int \<Rightarrow> int list \<Rightarrow> int list" where
+  "ddec a [] = []"
+| "ddec (a::int) (x#xs) = (x + a) # (ddec (x + a) xs)"
+
+value "ddec 0 [1,1,2,4]"
+value "ddec 0 [3,1,1]"
+value "ddec 0 [5]"
+value "ddec 0 []"
+
+value "ddec 5 (denc 4 [1,2,3])"
+
+lemma encdecgen: "ddec n (denc n l) = l"
+  apply(induction l arbitrary:n)
+  by auto
+
+lemma "ddec 0 (denc 0 l) = l"
+  apply(auto simp:encdecgen)
+  done
+
+end
\ No newline at end of file
diff --git a/03/ex03.pdf b/03/ex03.pdf
new file mode 100644
index 0000000..2dc5a71
Binary files /dev/null and b/03/ex03.pdf differ
diff --git a/03/hw03.thy b/03/hw03.thy
new file mode 100644
index 0000000..ab1fa95
--- /dev/null
+++ b/03/hw03.thy
@@ -0,0 +1,114 @@
+theory hw03
+  imports  "~~/src/HOL/Library/Tree" Main
+begin
+
+(* Part 1 - complete*)
+
+declare Let_def [simp]
+
+datatype direction = L|R
+type_synonym path = "direction list"
+
+fun valid:: "'a tree \<Rightarrow> path \<Rightarrow> bool" where
+  "valid _ [] = True"
+| "valid Leaf _ = False"
+| "valid (Node ltr a rtr) (x#xs) = (if x = L then (valid ltr xs) else (valid rtr xs))"
+
+fun get:: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree" where
+  "get x [] = x"
+| "get (Node ltr a rtr) (x# xs) = (if x = L then get ltr xs else get rtr xs)"
+| "get _ _ = undefined "
+
+fun put:: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+  "put x [] y = y"
+| "put Leaf _ _ = Leaf"
+| "put (Node l a r) (x# xs) y = (if x = L then (Node (put l xs y) a r) else (Node l a (put r xs y)))"
+
+value "put (Node (Node (Leaf) b (Leaf)) d Leaf) [R,R] (Node Leaf q Leaf)"
+value "valid (Node Leaf a Leaf) [R]"
+
+lemma put_invalid[simp]: "\<not>valid t p \<Longrightarrow> put t p s = t"
+  apply(induction p rule:valid.induct)
+     apply(auto)
+  done
+
+lemma get_put[simp]: "put t p (get t p) = t"
+  apply(induction p rule:get.induct)
+     apply(auto)
+  done
+
+
+lemma put_put[simp]: "valid t p \<Longrightarrow> put (put t p s) p s' = put t p s'"
+  apply(induction p arbitrary:s' rule: valid.induct)
+  apply(auto)
+  done
+
+lemma put_get[simp]: "valid t p \<Longrightarrow> get (put t p s) p = s"
+  apply(induction t p rule:get.induct)
+    apply(auto)
+  done
+  
+lemma valid_put[simp]: "valid t p \<longleftrightarrow> valid (put t p s) p"
+  apply(induction t p rule:valid.induct)
+    apply(auto)
+  done
+
+lemma valid_append[simp]: "valid t (p@q)\<longleftrightarrow> valid t p \<and> valid (get t p) q"
+  apply(induction t p rule:valid.induct)
+    apply auto
+  done
+
+lemma get_append[simp]: "valid t p \<Longrightarrow> get t (p@q) = get (get t p) q"
+  apply(induction t p rule:get.induct)
+    apply auto
+  done
+
+lemma put_append[simp]: "put t (p@q) s = put t p (put (get t p) q s)"
+  apply(induction t p rule:get.induct)
+  apply auto
+  done
+
+
+(*Part 2 - Incomplete, bst_remdups done, sublist done, first proof done with a generalization which I couldn't prove*)
+
+
+
+fun ins :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"ins x Leaf = Node Leaf x Leaf" |
+"ins x (Node l a r) =
+  (if x < a then Node (ins x l) a r else
+   if x > a then Node l a (ins x r)
+   else Node l a r)"
+
+fun bst_remdups_aux:: "'a::linorder tree \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "bst_remdups_aux t [] = inorder t"
+| "bst_remdups_aux t (x # xs) = bst_remdups_aux (ins x t) xs"
+
+definition "bst_remdups xs \<equiv> bst_remdups_aux Leaf xs"
+
+value "bst_remdups [1::int,2,3,4,1,5,5,6,6,10,7]"
+
+value "bst_remdups_aux (Node Leaf (7::nat) (Node Leaf (1::nat) Leaf)) [2::nat]"
+
+lemma bst_gen[simp]:"set (bst_remdups_aux t s) = set(bst_remdups_aux t []) \<union> set s"
+  sorry
+
+value "filter (\<lambda>x. x \<le> (2::nat)) [2::nat,3,4]"
+
+lemma "set (bst_remdups xs) = set xs"
+  unfolding bst_remdups_def
+  apply(induction xs)
+  apply(auto)
+  done
+
+fun remove:: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "remove a [] = []"
+| "remove a (x #xs) = (if (a = x) then xs else x #(remove a xs))"
+
+fun sublist:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "sublist [] ys = True"
+| "sublist xs [] = False"
+| "sublist (x#xs) ys = (if x\<in> set ys then sublist xs (remove x ys) else False)"
+
+
+end
\ No newline at end of file
diff --git a/03/hw03.thy~ b/03/hw03.thy~
new file mode 100644
index 0000000..6920130
--- /dev/null
+++ b/03/hw03.thy~
@@ -0,0 +1,125 @@
+theory hw03
+  imports  "~~/src/HOL/Library/Tree" Main
+begin
+
+declare Let_def [simp]
+
+datatype direction = L|R
+type_synonym path = "direction list"
+
+fun valid:: "'a tree \<Rightarrow> path \<Rightarrow> bool" where
+  "valid _ [] = True"
+| "valid Leaf _ = False"
+| "valid (Node ltr a rtr) (x#xs) = (if x = L then (valid ltr xs) else (valid rtr xs))"
+
+fun get:: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree" where
+  "get x [] = x"
+| "get (Node ltr a rtr) (x# xs) = (if x = L then get ltr xs else get rtr xs)"
+| "get _ _ = undefined "
+
+fun put:: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+  "put x [] y = y"
+| "put Leaf _ _ = Leaf"
+| "put (Node l a r) (x# xs) y = (if x = L then (Node (put l xs y) a r) else (Node l a (put r xs y)))"
+
+value "put (Node (Node (Leaf) b (Leaf)) d Leaf) [R,R] (Node Leaf q Leaf)"
+value "valid (Node Leaf a Leaf) [R]"
+
+lemma put_invalid[simp]: "\<not>valid t p \<Longrightarrow> put t p s = t"
+  apply(induction p rule:valid.induct)
+     apply(auto)
+  done
+
+lemma get_put[simp]: "put t p (get t p) = t"
+  apply(induction p rule:get.induct)
+     apply(auto)
+  done
+
+
+lemma put_put[simp]: "valid t p \<Longrightarrow> put (put t p s) p s' = put t p s'"
+  apply(induction p arbitrary:s' rule: valid.induct)
+  apply(auto)
+  done
+
+lemma put_get[simp]: "valid t p \<Longrightarrow> get (put t p s) p = s"
+  apply(induction t p rule:get.induct)
+    apply(auto)
+  done
+  
+lemma valid_put[simp]: "valid t p \<longleftrightarrow> valid (put t p s) p"
+  apply(induction t p rule:valid.induct)
+    apply(auto)
+  done
+
+lemma valid_append[simp]: "valid t (p@q)\<longleftrightarrow> valid t p \<and> valid (get t p) q"
+  apply(induction t p rule:valid.induct)
+    apply auto
+  done
+
+lemma get_append[simp]: "valid t p \<Longrightarrow> get t (p@q) = get (get t p) q"
+  apply(induction t p rule:get.induct)
+    apply auto
+  done
+
+lemma put_append[simp]: "put t (p@q) s = put t p (put (get t p) q s)"
+  apply(induction t p rule:get.induct)
+  apply auto
+  done
+
+
+(*Part 2*)
+
+
+
+fun ins :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"ins x Leaf = Node Leaf x Leaf" |
+"ins x (Node l a r) =
+  (if x < a then Node (ins x l) a r else
+   if x > a then Node l a (ins x r)
+   else Node l a r)"
+
+fun bst_remdups_aux:: "'a::linorder tree \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "bst_remdups_aux t [] = inorder t"
+| "bst_remdups_aux t (x # xs) = bst_remdups_aux (ins x t) xs"
+
+definition "bst_remdups xs \<equiv> bst_remdups_aux Leaf xs"
+
+value "bst_remdups [1::int,2,3,4,1,5,5,6,6,10]"
+
+fun unique::"'a list \<Rightarrow> 'a list" where
+  "unique [] = []"
+| "unique (x#xs) = (x # unique(filter(\<lambda>x'. x \<noteq> x') xs))"
+
+value "bst_remdups_aux (Node Leaf (7::nat) (Node Leaf (1::nat) Leaf)) [2::nat]"
+
+lemma bst_gen[simp]:"bst_remdups xs = sort (unique xs)"
+  sorry
+
+value "filter (\<lambda>x. x \<noteq> (2::nat)) [2::nat,3,4]"
+
+lemma "set (bst_remdups xs) = set xs"
+  apply(induction xs rule:bst_remdups_aux.induct)
+  apply(auto)
+  done
+
+lemma "distinct (bst_remdups xs)"
+  unfolding bst_remdups_def
+  apply(induction xs)
+  apply(auto simp:bst_gen)
+
+fun remove:: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "remove a [] = []"
+| "remove a (x #xs) = (if (a = x) then xs else x #(remove a xs))"
+
+fun sublist:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "sublist [] ys = True"
+| "sublist xs [] = False"
+| "sublist (x#xs) ys = (if x\<in> set ys then sublist xs (remove x ys) else False)"
+
+lemma "sublist (bst_remdups xs) xs"
+  unfolding bst_remdups_def
+  apply(induction xs)
+   apply(auto simp:bst_gen)
+  done
+
+end
\ No newline at end of file
diff --git a/04/BST_Demo.thy b/04/BST_Demo.thy
new file mode 100644
index 0000000..e60adf8
--- /dev/null
+++ b/04/BST_Demo.thy
@@ -0,0 +1,73 @@
+theory BST_Demo
+imports "~~/src/HOL/Library/Tree"
+begin
+
+(* useful most of the time: *)
+declare Let_def [simp]
+
+section "BST Search and Insertion"
+
+fun isin :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> bool" where
+"isin Leaf x = False" |
+"isin (Node l a r) x =
+  (if x < a then isin l x else
+   if x > a then isin r x
+   else True)"
+
+fun ins :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"ins x Leaf = Node Leaf x Leaf" |
+"ins x (Node l a r) =
+  (if x < a then Node (ins x l) a r else
+   if x > a then Node l a (ins x r)
+   else Node l a r)"
+
+subsection "Functional Correctness"
+
+lemma set_tree_isin: "bst t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
+apply(induction t)
+apply auto
+done
+
+lemma set_tree_ins: "set_tree (ins x t) = {x} \<union> set_tree t"
+apply(induction t)
+apply auto
+done
+
+subsection "Preservation of Invariant"
+
+lemma bst_ins: "bst t \<Longrightarrow> bst (ins x t)"
+apply(induction t)
+apply (auto simp: set_tree_ins)
+done
+
+
+section "BST Deletion"
+
+fun split_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
+"split_min (Node l a r) =
+  (if l = Leaf then (a,r)
+   else let (x,l') = split_min l
+        in (x, Node l' a r))"
+
+fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"delete x Leaf = Leaf" |
+"delete x (Node l a r) =
+  (if x < a then Node (delete x l) a r else
+   if x > a then Node l a (delete x r)
+   else if r = Leaf then l else let (a',r') = split_min r in Node l a' r')"
+
+(* A proof attempt *)
+
+lemma "split_min t = (x,t') \<Longrightarrow> set_tree t' = set_tree t - {x}"
+oops
+
+(* The final proof (needs more than auto!): *)
+
+lemma "\<lbrakk> split_min t = (x,t'); bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
+  set_tree t' = set_tree t - {x} \<and> x \<in> set_tree t"
+apply(induction t arbitrary: x t')
+ apply simp
+apply (force split: if_split_asm prod.splits)
+done
+
+end
diff --git a/04/Homework04.thy b/04/Homework04.thy
new file mode 100644
index 0000000..ed1f7df
--- /dev/null
+++ b/04/Homework04.thy
@@ -0,0 +1,71 @@
+theory Homework04
+  imports "BST_Demo"
+begin
+
+
+datatype 'a rtree = Leaf|Node "'a rtree" nat 'a "'a rtree"
+
+fun num_nodes :: "'a rtree \<Rightarrow> nat" where
+  "num_nodes Leaf = 0"|
+  "num_nodes (Node l a b r) = num_nodes l + num_nodes r + 1"
+
+
+fun rbst :: "'a::linorder rtree \<Rightarrow> bool" where
+  "rbst Leaf = True"|
+  "rbst (Node l a b r) = 
+    ((rbst l)\<and>
+    (\<forall>x\<in>set_rtree l. x<b)\<and>
+    (a = num_nodes l)\<and>
+    (\<forall>x\<in>set_rtree r. b<x)\<and>
+    (rbst r))"
+  
+
+value "rbst (Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+value "set_rtree(Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+
+fun rins :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> 'a rtree" where
+  "rins x Leaf = (Node Leaf 0 x Leaf)"|
+  "rins x (Node l a b r) = (if x<b then (Node (rins x l) (Suc a) b r) else (Node l a b (rins x r)))"
+
+value "rins 5 (Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+
+lemma rins_set[simp]: "set_rtree (rins x t) = insert x (set_rtree t)"
+  apply(induction t)
+   apply auto
+  done
+
+lemma aux1[simp]:  "(x\<notin>set_rtree t) \<Longrightarrow>num_nodes (rins x t) = Suc(num_nodes t)"
+  apply(induction t arbitrary:x)
+   apply auto
+  done
+
+lemma aux[simp]: "rbst(Node l a b r) \<Longrightarrow> (num_nodes l = a) "
+  apply auto
+  done
+
+
+lemma "x\<notin>set_rtree t \<Longrightarrow> rbst t \<Longrightarrow> rbst (rins x t)"
+  apply(induction t arbitrary: x rule:rbst.induct)
+   apply auto
+  done
+
+fun risin:: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> bool" where
+  "risin _ Leaf = False"|
+  "risin x (Node l a b r) = ((x=b)\<or>(risin x l)\<or>(risin x r))"
+
+lemma "rbst t \<Longrightarrow> risin x t \<longleftrightarrow> x\<in>set_rtree t"
+  apply(induction t)
+   apply auto
+  done
+
+fun inorder :: "'a rtree \<Rightarrow> 'a list" where
+  "inorder Leaf = []"|
+  "inorder (Node l a b r) = inorder l @ b # inorder r"
+
+fun rank:: "'a::linorder \<Rightarrow> _" where
+
+
+
+
+
+end
diff --git a/04/ex04.pdf b/04/ex04.pdf
new file mode 100644
index 0000000..969ac94
Binary files /dev/null and b/04/ex04.pdf differ
diff --git a/04/ex04self.thy b/04/ex04self.thy
new file mode 100644
index 0000000..efd0691
--- /dev/null
+++ b/04/ex04self.thy
@@ -0,0 +1,27 @@
+theory ex04self
+  imports Main  "~~/src/HOL/Library/Tree"
+begin
+
+
+fun in_range :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where
+  "in_range Leaf x y = []"
+| "in_range (Node l x r) u v = 
+  (if x > u then in_range l u v else [])
+@ (if u \<le> x \<and> x \<le> v then [x] else [])
+@ (if v > x then in_range r u v else [])"
+
+lemma "bst t \<Longrightarrow> set (in_range t u v) = {x\<in>set_tree t. u\<le>x \<and> x\<le>v}"
+  apply (induction t)
+  apply auto
+  done
+
+
+text \<open>Show that your list is actually in-order\<close>
+lemma "bst t \<Longrightarrow> in_range t u v = filter (\<lambda>x. u\<le>x \<and> x\<le>v) (inorder t)"
+  apply (induction t)
+  apply simp
+  apply (clarsimp)
+  apply safe
+
+
+end
diff --git a/04/hw04.thy b/04/hw04.thy
new file mode 100644
index 0000000..ebe9a68
--- /dev/null
+++ b/04/hw04.thy
@@ -0,0 +1,101 @@
+theory hw04
+  imports Main  "~~/src/HOL/Library/Tree"
+begin
+
+declare Let_def [simp]
+
+datatype 'a rtree = Leaf | Node "'a rtree" nat 'a "'a rtree"
+
+fun num_nodes:: "'a rtree \<Rightarrow> nat" where
+  "num_nodes Leaf = 0"
+| "num_nodes (Node l n b r) = 1 + num_nodes l + num_nodes r"
+
+fun rbst:: "'a::linorder rtree \<Rightarrow> bool" where
+  "rbst Leaf = True"
+| "rbst (Node l a b r) = (rbst l \<and> (\<forall>x\<in>set_rtree l. (b > x)) \<and> (\<forall>x\<in>set_rtree r. (b < x)) \<and> (a = num_nodes l) \<and> rbst r)"
+
+
+value "rbst (Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+
+fun rins:: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> 'a rtree" where
+  "rins x Leaf = (Node Leaf 0 x Leaf)"
+| "rins x (Node l n b r) =
+  (if (x < b) then (Node (rins x l) (Suc n) b r) else (Node l n b (rins x r)))"
+
+value "rins (4::nat) (Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+
+lemma rins_set[simp]: "set_rtree (rins x t) = insert x (set_rtree t)"
+  apply(induction t arbitrary:x)
+   apply(auto)
+  done
+
+
+lemma aux1[simp]: "(x\<notin>set_rtree t) \<Longrightarrow> num_nodes (rins x t) = Suc(num_nodes t)"
+  apply(induction t arbitrary: x)
+   apply(auto)
+  done
+
+lemma aux2[simp]: "rbst(Node l a b r) \<Longrightarrow> (num_nodes l = a) "
+   apply(auto)
+  done
+
+value "rbst  (rtree.Node rtree.Leaf 0 (1::nat) (rtree.Node rtree.Leaf 0 (1::nat) rtree.Leaf))"
+
+
+
+lemma "x\<notin>set_rtree t \<Longrightarrow> rbst t \<Longrightarrow> rbst (rins x t)"
+  apply(induction t arbitrary: x rule:rbst.induct)
+   apply(auto)
+  done
+
+fun risin :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> bool" where
+  "risin x Leaf = False"
+| "risin x (Node l a b r) = 
+  (
+    if (b < x) then
+      (risin x r)
+    else if (b > x) then
+      (risin x l)
+    else
+      True
+  )"
+
+value "risin (3::nat) (Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+
+lemma "rbst t \<Longrightarrow> risin x t \<longleftrightarrow> x\<in>set_rtree t"
+  apply(induction t)
+   apply(auto)
+  done
+
+fun inorder:: "'a rtree \<Rightarrow> 'a list" where
+  "inorder Leaf = []"
+| "inorder (Node l a b r) = inorder l @ [b] @ inorder r"
+
+fun rank::"'a::linorder \<Rightarrow> _" where
+  "rank x Leaf = undefined"
+| "rank x (Node l a b r) = (if (x = b) then a else if (x < b) then (rank x l) else (a + 1 + rank x r))"
+
+definition "at_index i l x \<equiv> i<length l \<and> l!i=x"
+
+lemma aux3[simp]:"rbst t \<Longrightarrow> num_nodes t = length (inorder t)"
+  apply(induction t)
+   apply(auto)
+  done
+
+
+lemma "rbst t \<Longrightarrow> x\<in>set_rtree t \<Longrightarrow> at_index (rank x t) (inorder t) x"
+  unfolding at_index_def
+  apply(induction t rule:inorder.induct)
+   apply(auto)
+  sorry
+
+fun select :: "nat \<Rightarrow> 'a::linorder rtree \<Rightarrow> 'a" where
+  "select n Leaf = undefined"
+| "select n (Node l a b r) = (if (n = a) then b else if n < a then select n l else select (n-a-1) r)"
+
+lemma select_correct: "rbst t \<Longrightarrow> i<length (inorder t) \<Longrightarrow> select i t = inorder t ! i"
+  apply(induction i t rule:select.induct)
+   apply(auto)
+  sorry
+
+end
\ No newline at end of file
diff --git a/04/hw04.thy~ b/04/hw04.thy~
new file mode 100644
index 0000000..714958e
--- /dev/null
+++ b/04/hw04.thy~
@@ -0,0 +1,101 @@
+theory hw04
+  imports Main  "~~/src/HOL/Library/Tree"
+begin
+
+declare Let_def [simp]
+
+datatype 'a rtree = Leaf | Node "'a rtree" nat 'a "'a rtree"
+
+fun num_nodes:: "'a rtree \<Rightarrow> nat" where
+  "num_nodes Leaf = 0"
+| "num_nodes (Node l n b r) = 1 + num_nodes l + num_nodes r"
+
+fun rbst:: "'a::linorder rtree \<Rightarrow> bool" where
+  "rbst Leaf = True"
+| "rbst (Node l a b r) = (rbst l \<and> (\<forall>x\<in>set_rtree l. (b > x)) \<and> (\<forall>x\<in>set_rtree r. (b < x)) \<and> (a = num_nodes l) \<and> rbst r)"
+
+
+value "rbst (Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+
+fun rins:: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> 'a rtree" where
+  "rins x Leaf = (Node Leaf 0 x Leaf)"
+| "rins x (Node l n b r) =
+  (if (x < b) then (Node (rins x l) (Suc n) b r) else (Node l n b (rins x r)))"
+
+value "rins (4::nat) (Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+
+lemma rins_set[simp]: "set_rtree (rins x t) = insert x (set_rtree t)"
+  apply(induction t arbitrary:x)
+   apply(auto)
+  done
+
+
+lemma aux1[simp]: "(x\<notin>set_rtree t) \<Longrightarrow> num_nodes (rins x t) = Suc(num_nodes t)"
+  apply(induction t arbitrary: x)
+   apply(auto)
+  done
+
+lemma aux2[simp]: "rbst(Node l a b r) \<Longrightarrow> (num_nodes l = a) "
+   apply(auto)
+  done
+
+value "rbst  (rtree.Node rtree.Leaf 0 (1::nat) (rtree.Node rtree.Leaf 0 (1::nat) rtree.Leaf))"
+
+
+
+lemma "x\<notin>set_rtree t \<Longrightarrow> rbst t \<Longrightarrow> rbst (rins x t)"
+  apply(induction t arbitrary: x rule:rbst.induct)
+   apply(auto)
+  done
+
+fun risin :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> bool" where
+  "risin x Leaf = False"
+| "risin x (Node l a b r) = 
+  (
+    if (b < x) then
+      (risin x r)
+    else if (b > x) then
+      (risin x l)
+    else
+      True
+  )"
+
+value "risin (3::nat) (Node (Node Leaf (0::nat) (1::nat) Leaf) (1::nat) 2 (Node Leaf (0::nat) 3 Leaf))"
+
+lemma "rbst t \<Longrightarrow> risin x t \<longleftrightarrow> x\<in>set_rtree t"
+  apply(induction t)
+   apply(auto)
+  done
+
+fun inorder:: "'a rtree \<Rightarrow> 'a list" where
+  "inorder Leaf = []"
+| "inorder (Node l a b r) = inorder l @ [b] @ inorder r"
+
+fun rank::"'a::linorder \<Rightarrow> _" where
+  "rank x Leaf = undefined"
+| "rank x (Node l a b r) = (if (x = b) then a else if (x < b) then (rank x l) else (a + 1 + rank x r))"
+
+definition "at_index i l x \<equiv> i<length l \<and> l!i=x"
+
+lemma aux3[simp]:"rbst t \<Longrightarrow> num_nodes t = length (inorder t)"
+  apply(induction t)
+   apply(auto)
+  done
+
+
+lemma "rbst t \<Longrightarrow> x\<in>set_rtree t \<Longrightarrow> at_index (rank x t) (inorder t) x"
+  unfolding at_index_def
+  apply(induction t rule:inorder.induct)
+   apply(auto)
+  sorry
+
+fun select :: "nat \<Rightarrow> 'a::linorder rtree \<Rightarrow> 'a" where
+  "select n Leaf = undefined"
+| "select n (Node l a b r) = (if (n = a) then b else if n < a then select n l else select (n-a-1) r)"
+
+lemma select_correct: "rbst t \<Longrightarrow> i<length (inorder t) \<Longrightarrow> select i t = inorder t ! i"
+  apply(induction t rule:inorder.induct)
+   apply(auto)
+  
+
+end
\ No newline at end of file
diff --git a/05/ex05.pdf b/05/ex05.pdf
new file mode 100644
index 0000000..7b9ba44
Binary files /dev/null and b/05/ex05.pdf differ
diff --git a/05/hw05.thy b/05/hw05.thy
new file mode 100644
index 0000000..f1d08e1
--- /dev/null
+++ b/05/hw05.thy
@@ -0,0 +1,49 @@
+theory hw05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+
+value "(0::nat) div 0"
+
+lemma
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+  let ?n = "length xs div n"
+  let ?ys = "take ?n xs"
+  let ?zs = "drop ?n xs"
+  show "length ?ys = length xs div n \<and> xs = ?ys @ ?zs"  by(simp add:min.absorb2)
+qed
+
+
+fun a :: "nat \<Rightarrow> int" where
+  "a 0 = 0"
+| "a (Suc n) = a n ^ 2 + 1"
+
+thm power_mono[where n = 2]
+
+find_theorems "(_-_)^2"
+find_theorems "(_ + _) > _"
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    from IH have azer:"0 \<le> a n" by (smt a.elims power2_less_eq_zero_iff zero_eq_power2)
+   
+    from IH  have "a (Suc n) = (a n)^2 +1" by simp
+    also have "(a n)^2 \<le> (2 ^ 2 ^ n - 1) ^ 2" using power_mono[where n = 2] IH azer by blast
+    also have "... \<le> (2 ^ 2 ^ (n + 1)) + 1 - 2*2^(2^(n))" by (simp add: power2_diff power_even_eq)
+    also have "... \<le> 2 ^ 2 ^ Suc n - 2 " by (smt Suc.IH Suc_eq_plus1 a.elims power.simps(1) power2_less_eq_zero_iff power_one_right zero_eq_power2)
+    finally show ?thesis by auto
+    
+  qed
+qed
+
+end
\ No newline at end of file
diff --git a/05/hw05.thy~ b/05/hw05.thy~
new file mode 100644
index 0000000..f85a649
--- /dev/null
+++ b/05/hw05.thy~
@@ -0,0 +1,44 @@
+theory hw05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+
+lemma
+  assumes "n\<ge>0" 
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+  apply(simp)
+  apply(induction xs)
+  apply(auto)
+  oops
+
+fun a :: "nat \<Rightarrow> int" where
+  "a 0 = 0"
+| "a (Suc n) = a n ^ 2 + 1"
+
+thm power_mono[where n = 2]
+
+find_theorems "(_-_)^2"
+find_theorems "(_ + _) > _"
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    from IH have azer:"0 \<le> a n" by (smt a.elims power2_less_eq_zero_iff zero_eq_power2)
+   
+    from IH  have "a (Suc n) = (a n)^2 +1" by simp
+    also have "(a n)^2 \<le> (2 ^ 2 ^ n - 1) ^ 2" using power_mono[where n = 2] IH azer by blast
+    also have "... \<le> (2 ^ 2 ^ (n + 1)) + 1 - 2*2^(2^(n))" by (simp add: power2_diff power_even_eq)
+    also have "... \<le> 2 ^ 2 ^ Suc n - 2 " by (smt Suc.IH Suc_eq_plus1 a.elims power.simps(1) power2_less_eq_zero_iff power_one_right zero_eq_power2)
+    finally show ?thesis by auto
+    
+  qed
+qed
+
+end
\ No newline at end of file
diff --git a/05/tmpl05.thy b/05/tmpl05.thy
new file mode 100644
index 0000000..4393d77
--- /dev/null
+++ b/05/tmpl05.thy
@@ -0,0 +1,183 @@
+(*<*)
+theory tmpl05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+    text \<open>Fill in a proof here. Hint: Start with a case distinction
+      whether \<open>n>3\<close> or \<open>n=3\<close>. \<close>
+    sorry
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+where
+"sumto f 0 = 0"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  (*by (induction n) auto*) oops
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+  show "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = sumto (\<lambda>x. x ^ 3) (Suc n)"
+  text \<open>Insert a proof here\<close>
+    sorry
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  where
+  "path _ _ _ _ \<longleftrightarrow> False"
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  oops
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+  oops
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+  oops
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    text \<open>Insert your proof here\<close>
+    show ?thesis sorry
+  qed
+qed
+
+
+(*<*)
+end
+(*>*)
diff --git a/06/ex06.pdf b/06/ex06.pdf
new file mode 100644
index 0000000..7ea780e
Binary files /dev/null and b/06/ex06.pdf differ
diff --git a/06/hw06.thy b/06/hw06.thy
new file mode 100644
index 0000000..9c54599
--- /dev/null
+++ b/06/hw06.thy
@@ -0,0 +1,66 @@
+theory hw06
+  imports Main 
+begin
+
+fun funky::"int \<Rightarrow> int" where
+ "funky k = (k - 3)^2"
+
+value "sort_key funky [(2::int), 1, 3, 4]"
+
+find_theorems "insort_key"
+
+lemma "[x\<leftarrow>sort_key k xs. k x = a] = [x\<leftarrow>xs. k x = a]"
+  apply(induction xs)
+   apply(auto simp: filter_insort_triv filter_insort insort_is_Cons)
+  done
+
+fun quickselect :: "'a::linorder list \<Rightarrow> nat \<Rightarrow> 'a" where
+  "quickselect (x#xs) k = (let
+    xs1 = [y\<leftarrow>xs. y<x];
+    xs2 = [y\<leftarrow>xs. \<not>(y<x)]
+  in
+    if k<length xs1 then quickselect xs1 k
+    else if k=length xs1 then x
+    else quickselect xs2 (k-length xs1-1)
+  )"
+| "quickselect [] _ = undefined"
+
+lemma aux1[simp]: "(\<forall>x\<in>set xs. x < p) \<Longrightarrow> (\<forall>y\<in>set ys. \<not> y < p) \<Longrightarrow> (a < p) \<Longrightarrow> insort a (xs@ys) = (insort a xs) @ ys"
+  apply(induction xs)
+  apply(induction ys)
+  by auto
+
+lemma aux2[simp]: "(\<forall>x\<in>set xs. x < p) \<Longrightarrow> (\<forall>y\<in>set ys. \<not> y < p) \<Longrightarrow> \<not>(a < p) \<Longrightarrow> insort a (xs@ys) = (xs) @ insort a ys"
+  apply(induction xs)
+  apply(induction ys)
+  by auto
+
+
+lemma partition_correct[simp]: "sort xs = sort [x\<leftarrow>xs. x<p] @ sort [x\<leftarrow>xs. \<not>(x<p)]"
+  apply(induction xs)
+  apply(simp)
+   apply(clarsimp)
+  apply(smt aux1 aux2 filter_set member_filter set_sort)
+  done
+
+lemma "k<length xs \<Longrightarrow> quickselect xs k = sort xs ! k"
+proof (induction xs k rule: quickselect.induct)
+  print_cases
+  case (1 x xs k)
+  note IH = "1.IH"[OF refl refl]
+
+  let ?xs1 = "[y\<leftarrow>xs. y<x]"
+  
+
+  show ?case proof cases
+    assume "k<length ?xs1" then show ?thesis apply (simp add: IH) sorry
+  next
+    assume "\<not>(k<length ?xs1)" then show ?thesis sorry
+        
+  qed
+next
+  case 2 then show ?case by simp
+qed
+
+
+end
\ No newline at end of file
diff --git a/06/hw06.thy~ b/06/hw06.thy~
new file mode 100644
index 0000000..281d678
--- /dev/null
+++ b/06/hw06.thy~
@@ -0,0 +1,31 @@
+theory hw06
+  imports Main 
+begin
+
+fun funky::"int \<Rightarrow> int" where
+ "funky k = (k - 3)^2"
+
+value "sort_key funky [(2::int), 1, 3, 4]"
+
+find_theorems "insort"
+
+lemma "[x\<leftarrow>sort_key k xs. k x = a] = [x\<leftarrow>xs. k x = a]"
+  apply(induction xs)
+   apply(auto simp: sort_key_def filter_sort filter_insort_triv)
+  sorry
+
+fun quickselect :: "'a::linorder list \<Rightarrow> nat \<Rightarrow> 'a" where
+  "quickselect (x#xs) k = (let
+    xs1 = [y\<leftarrow>xs. y<x];
+    xs2 = [y\<leftarrow>xs. \<not>(y<x)]
+  in
+    if k<length xs1 then quickselect xs1 k
+    else if k=length xs1 then x
+    else quickselect xs2 (k-length xs1-1)
+  )"
+| "quickselect [] _ = undefined"
+
+find_theorems "sort"
+
+
+end
\ No newline at end of file
diff --git a/06/tmpl06.thy b/06/tmpl06.thy
new file mode 100644
index 0000000..fa4c165
--- /dev/null
+++ b/06/tmpl06.thy
@@ -0,0 +1,149 @@
+(*<*)
+theory tmpl06
+  imports Main
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{6}{18.~5.~2018} *}
+
+text \<open>\Exercise{Complexity of Naive Reverse}
+  Show that the naive reverse function needs quadratically many
+  \<open>Cons\<close> operations in the length of the input list.
+  (Note that \<open>[x]\<close> is syntax sugar for \<open>Cons x []\<close>!)
+\<close>
+
+thm append.simps
+
+fun reverse where
+  "reverse [] = []"
+| "reverse (x#xs) = reverse xs @ [x]"
+
+(** Define cost functions and prove that they are equal to quadratic function *)
+
+text \<open>
+  \Exercise{Simple Paths}
+  Recall the definition of paths from last exercise sheet:
+\<close>
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  where
+  "path G u [] v \<longleftrightarrow> u=v"
+| "path G u (x#xs) v \<longleftrightarrow> G u x \<and> path G x xs v"
+
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  by (induction p1 arbitrary: u) auto
+
+
+text \<open>
+  A simple path is a path without loops, or, in other words, a path
+  where no node occurs twice. (Note that the first node of the path is
+  not included, such that there may be a simple path from \<open>u\<close> to \<open>u\<close>.)
+
+  Show that for every path, there is a corresponding simple path.
+
+  Hint: Induction on the length of the path
+\<close>
+thm measure_induct_rule[where f=length, case_names shorter]
+
+thm not_distinct_decomp
+
+lemma exists_simple_path:
+  assumes "path G u p v"
+  shows "\<exists>p'. path G u p' v \<and> distinct p'"
+  oops
+
+
+text \<open>\NumHomework{Stability of Insertion Sort}{May 25}
+  Have a look at Isabelle's standard implementation of sorting: @{const sort_key}.
+  (Use Ctrl-Click to jump to the definition in @{file "~~/src/HOL/List.thy"})
+  Show that this function is a stable sorting algorithm, i.e., the order of elements
+  with the same key is not changed during sorting!
+\<close>
+
+lemma "[x\<leftarrow>sort_key k xs. k x = a] = [x\<leftarrow>xs. k x = a]"
+  oops
+
+term "[x\<leftarrow>xs. P x]"
+text \<open>
+  Note: @{term [source] \<open>[x\<leftarrow>xs. P x] \<close>} is syntax sugar for @{term [source] \<open>filter P xs\<close>},
+  where the filter function returns only the elements of list \<open>xs\<close> for which \<open>P xs = True\<close>.
+
+  Hint: You do not necessarily need Isar, and the auxiliary lemmas
+    you need are already in Isabelle's library. @{command find_theorems} is your friend!
+\<close>
+
+
+text \<open>\NumHomework{Quickselect}{May 25}
+
+From \<^url>\<open>https://en.wikipedia.org/wiki/Quickselect\<close>:
+
+Quickselect is a selection algorithm to find the kth smallest element in an unordered list.
+It is related to the quicksort sorting algorithm.
+Like quicksort, it was developed by Tony Hoare, and thus is also known as Hoare's selection
+algorithm. Like quicksort, it is efficient in practice and has good average-case performance,
+but has poor worst-case performance. Quickselect and its variants are the selection algorithms
+most often used in efficient real-world implementations.
+
+Quickselect uses the same overall approach as quicksort, choosing one element as a pivot and
+partitioning the data in two based on the pivot, accordingly as less than or greater than the
+pivot. However, instead of recursing into both sides, as in quicksort, quickselect only
+recurses into one side --- the side with the element it is searching for.
+
+
+Your task is to prove correct the quickselect algorithm, which can be
+  implemented in Isabelle as follows:
+\<close>
+
+fun quickselect :: "'a::linorder list \<Rightarrow> nat \<Rightarrow> 'a" where
+  "quickselect (x#xs) k = (let
+    xs1 = [y\<leftarrow>xs. y<x];
+    xs2 = [y\<leftarrow>xs. \<not>(y<x)]
+  in
+    if k<length xs1 then quickselect xs1 k
+    else if k=length xs1 then x
+    else quickselect xs2 (k-length xs1-1)
+  )"
+| "quickselect [] _ = undefined"
+
+
+text \<open>Your first task is to prove the crucial idea of quicksort, i.e., that
+  partitioning wrt.\ a pivot element $p$ is correct.
+\<close>
+
+lemma partition_correct: "sort xs = sort [x\<leftarrow>xs. x<p] @ sort [x\<leftarrow>xs. \<not>(x<p)]"
+  oops
+
+text \<open>
+  Hint: Induction, and auxiliary lemmas to transform a term of the
+    form @{term \<open>insort x (xs@ys)\<close>} when you know that \<open>x\<close> is greater than
+    all elements in \<open>xs\<close> / less than or equal all elements in \<open>ys\<close>.
+\<close>
+
+
+
+text \<open>Next, show that quickselect is correct\<close>
+lemma "k<length xs \<Longrightarrow> quickselect xs k = sort xs ! k"
+  text \<open>Proceed by computation induction, and a case distinction according to the
+    cases in the body of the quickselect function\<close>
+proof (induction xs k rule: quickselect.induct)
+  case (1 x xs k)
+
+  text \<open>Note: To make the induction hypothesis more readable,
+    you can collapse the first two premises of the form \<open>?x=\<dots>\<close>
+    by reflexivity:\<close>
+  note IH = "1.IH"[OF refl refl]
+
+  text \<open>Insert your proof here!\<close>
+
+  show ?case sorry
+next
+  case 2 then show ?case by simp
+qed
+
+
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/07/ex07.pdf b/07/ex07.pdf
new file mode 100644
index 0000000..ce05bf0
Binary files /dev/null and b/07/ex07.pdf differ
diff --git a/07/hw07.thy b/07/hw07.thy
new file mode 100644
index 0000000..de35d5b
--- /dev/null
+++ b/07/hw07.thy
@@ -0,0 +1,143 @@
+theory hw07
+  imports Main
+begin
+
+hide_const (open) inv
+
+type_synonym intervals = "(nat*nat) list"
+
+fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
+  "inv' n [] \<longleftrightarrow> True"|
+  "inv' n ((a,b)#ivs) \<longleftrightarrow> n\<le>a \<and> a\<le>b \<and> inv' (b+2) ivs"
+
+definition inv where "inv = inv' 0"
+
+
+fun set_of :: "intervals \<Rightarrow> nat set"
+where
+  "set_of [] = {}"|
+  "set_of ((a,b)#ivs) = {a..b} \<union> set_of ivs"
+
+
+fun del :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+  where
+   "del x [] = []"
+|  "del x ((a,b)#lis) = (
+    if (x < a) then (a,b)#lis
+    else if (x = a \<and> x = b) then lis
+    else if (x = a) then ((a+1), b)#lis
+    else if (x < b) then (a,x-1)#(x+1,b)#lis
+    else if (x = b) then (a,b-1)#lis
+    else (a,b)#(del x lis))"
+
+value "del (12::nat) [(2,5),(7,7),(9,11)]"
+value "set_of [] - {1::nat}"
+
+lemma del_pres_inv: "n\<le>x \<Longrightarrow> inv' n itl \<Longrightarrow> inv' n (del x itl)"
+proof (induction itl arbitrary:n)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case
+    apply (cases a)
+    apply (cases itl)
+    apply auto
+    done
+qed
+
+lemma set_of_del:
+  assumes "n\<le>x"
+  assumes "inv' n itl"
+  shows "set_of (del x itl) =  set_of itl - {x}"
+  using assms
+proof (induction itl arbitrary:n)
+case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case 
+    apply (cases a)
+    apply (cases itl)
+     apply (auto split: if_splits)
+    apply (auto)
+    done
+qed
+
+
+lemma del_correct:
+  assumes "inv itl"
+  shows "inv (del x itl)" "set_of (del x itl) =  (set_of itl) - {x}"
+  using assms del_pres_inv hw07.inv_def apply fastforce
+  using assms hw07.inv_def set_of_del by fastforce
+
+
+
+
+
+
+
+
+
+fun addi :: "nat \<Rightarrow> nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "addi i j [] = [(i,j)]"|
+  "addi i j ((a,b)#lis) = (
+    if j + 1 < a then ((i,j)#(a,b)#lis)
+    else if j+1 = a then ((i,b)#lis)
+    else if j \<le> b then(
+      if i < a then ((i,b)#lis)
+      else ((a,b)#lis))
+    else (
+      if i < a then addi i j lis
+      else if i \<le> b+1 then addi a j lis
+      else ((a,b)#(addi i j lis)))
+    )"
+
+value "addi 5 99 [(2,5),(7,7),(9,11)]"
+
+lemma addi_pres_inv: "n\<le>i \<Longrightarrow> i\<le>j \<Longrightarrow> inv' n itl \<Longrightarrow> inv' n (addi i j itl)"
+proof (induction i j itl arbitrary:n rule:addi.induct)
+  case (1 i j)
+  then show ?case by auto
+next
+  case (2 i j a b itl)
+  then show ?case
+    apply(cases itl)
+     apply(auto)
+    done
+qed
+
+lemma set_of_addi:
+  assumes "n\<le>i" "i\<le>j"
+  assumes "inv' n itl"
+  shows "set_of (addi i j itl) = {i..j} \<union> set_of itl"
+  using assms
+proof (induction i j itl arbitrary:n rule:addi.induct)
+  case (1 i j)
+  then show ?case by auto
+next
+  case (2 i j a b lis)
+  then show ?case
+    apply(cases lis)
+     apply(cases a)
+      apply(cases b)
+       apply (auto split:if_splits)
+          apply fastforce
+         apply fastforce
+        apply fastforce
+       apply fastforce
+      apply fastforce
+     apply fastforce
+    apply fastforce
+    done
+qed
+
+lemma addi_correct:
+  assumes "inv is" "i\<le>j"
+  shows "inv (addi i j is)" "set_of (addi i j is) = {i..j} \<union> (set_of is)"
+  using addi_pres_inv assms hw07.inv_def zero_order(3) apply force
+  by (metis assms hw07.inv_def le0 set_of_addi)
+
+
+end
diff --git a/07/hw07.thy~ b/07/hw07.thy~
new file mode 100644
index 0000000..455d335
--- /dev/null
+++ b/07/hw07.thy~
@@ -0,0 +1,129 @@
+(*<*)
+theory hw07
+  imports Main
+begin
+(*>*)
+
+hide_const (open) inv (*inv is used as a constant in isabelle, renaming it pretty prints the const 
+with the long name if the const is not hidden*)
+
+type_synonym intervals = "(nat*nat) list"
+
+fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
+  "inv' n [] \<longleftrightarrow> True"|
+  "inv' n ((a,b)#ivs) \<longleftrightarrow> n\<le>a \<and> a\<le>b \<and> inv' (b+2) ivs"
+
+definition inv where "inv = inv' 0"
+
+
+fun set_of :: "intervals => nat set"
+where
+  "set_of [] = {}"|
+  "set_of ((a,b)#ivs) = {a..b} \<union> set_of ivs"
+
+
+fun del :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+  where
+   "del x [] = []"
+|  "del x ((a,b)#lis) = (
+    if (x < a) then (a,b)#lis
+    else if (x = a \<and> x = b) then lis
+    else if (x = a) then ((a+1), b)#lis
+    else if (x < b) then (a,x-1)#(x+1,b)#lis
+    else if (x = b) then (a,b-1)#lis
+    else (a,b)#(del x lis))"
+
+value "del (12::nat) [(2,5),(7,7),(9,11)]"
+value "set_of [] - {1::nat}"
+
+lemma del_pres_inv: "n\<le>x \<Longrightarrow> inv' n itl \<Longrightarrow> inv' n (del x itl)"
+proof (induction itl arbitrary:n)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case
+    apply (cases a)
+    apply (cases itl)
+    apply auto
+    done
+qed
+
+lemma set_of_del:
+  assumes "n\<le>x"
+  assumes "inv' n itl"
+  shows "set_of (del x itl) =  set_of itl - {x}"
+  using assms
+proof (induction itl arbitrary:n)
+case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case 
+    apply (cases a)
+    apply (cases itl)
+     apply (auto split: if_splits)
+    apply (auto)
+    done
+qed
+
+
+lemma del_correct:
+  assumes "inv itl"
+  shows "inv (del x itl)" "set_of (del x itl) =  (set_of itl) - {x}"
+  using assms del_pres_inv hw07.inv_def apply fastforce
+  using assms hw07.inv_def set_of_del by fastforce
+
+
+
+text \<open> \NumHomework{Addition of Interval to Interval List}{June 1}
+  For 3 \<^bold>\<open>bonus points\<close>, implement and prove correct a function
+  to add a whole interval to an interval list. The runtime must
+  not depend on the size of the interval, e.g., iterating over the
+  interval and adding the elements separately is not allowed!
+\<close>
+fun merge_aux where
+  "merge_aux a j [] = [(a,j)]"|
+  "merge_aux a j ((c,d)#ivs) = (
+    if (j+1 \<ge> c \<and> j+1 \<le> d) then (a,d)#ivs
+    else if (j+1 < c) then ((a,j)#(c,d)#ivs)
+    else merge_aux a j ivs)"
+
+fun addi :: "nat \<Rightarrow> nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "addi i j [] = [(i,j)]"
+| "addi i j ((a,b)#lis) = (
+  if (j+1 < a) then (i,j)#(a,b)#lis
+  else if (i < a \<and> j+1 \<ge> a \<and> j+1 < b) then (i,b)#lis
+  else if (i \<ge> a \<and> j \<le> b) then (a,b)#lis
+  else if (j+1 \<ge> b \<and> i \<le> b+1) then merge_aux (min a i) j lis
+  else (a,b)#(addi i j lis))"
+
+value "addi 5 99 [(2,5),(7,7),(9,11)]"
+
+lemma addi_pres_inv: "n\<le>i \<Longrightarrow> i\<le>j \<Longrightarrow> inv' n itl \<Longrightarrow> inv' n (addi i j itl)"
+proof (induction itl arbitrary:n)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case
+    apply (cases a)
+    apply (cases itl)
+     apply auto
+         apply linarith
+        apply linarith
+       apply (smt Suc_leD min.left_commute min_def)
+    using Cons.prems(2) min_le_iff_disj apply blast
+     apply linarith
+qed
+
+lemma addi_correct:
+  assumes "inv is" "i\<le>j"
+  shows "inv (addi i j is)" "set_of (addi i j is) = {i..j} \<union> (set_of is)"
+  sorry
+
+
+(*<*)
+end
+(*>*)
diff --git a/07/tmpl07.thy b/07/tmpl07.thy
new file mode 100644
index 0000000..e373aa1
--- /dev/null
+++ b/07/tmpl07.thy
@@ -0,0 +1,135 @@
+(*<*)
+theory tmpl07
+  imports Main "HOL-Data_Structures.Sorting"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{7}{25.~5.~2018} *}
+
+
+text {* \Exercise{Interval Lists}
+
+ Sets of natural numbers can be implemented as lists of intervals, where
+an interval is simply a pair of numbers.  For example the set @{term "{2, 3, 5,
+7, 8, 9::nat}"} can be represented by the list @{term "[(2, 3), (5, 5),
+(7::nat, 9::nat)]"}.  A typical application is the list of free blocks of
+dynamically allocated memory. *}
+
+text {* We introduce the type *}
+
+type_synonym intervals = "(nat*nat) list"
+
+text {* Next, define an \emph{invariant}
+that characterizes valid interval lists:
+For efficiency reasons intervals should be sorted in ascending order, the lower
+bound of each interval should be less than or equal to the upper bound, and the
+intervals should be chosen as large as possible, i.e.\ no two adjacent
+intervals should overlap or even touch each other.  It turns out to be
+convenient to define @{term inv} in terms of a more general function
+such that the additional argument is a lower bound for the intervals in
+the list:*}
+
+fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
+  "inv' _ _ \<longleftrightarrow> undefined"
+
+definition inv where "inv = inv' 0"
+
+
+
+text {* To relate intervals back to sets define an \emph{abstraction function}*}
+
+fun set_of :: "intervals => nat set"
+where
+  "set_of _ = undefined"
+
+text \<open>Define a function to add a single element to the interval list,
+  and show its correctness\<close>
+
+
+fun add :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+  where
+  "add _ _ = undefined"
+
+lemma add_correct:
+  assumes "inv is"
+  shows "inv (add x is)" "set_of (add x is) = insert x (set_of is)"
+  oops
+
+text \<open>Hints:
+  \<^item> Sketch the different cases (position of element relative to the first interval of the list)
+    on paper first
+  \<^item> In one case, you will also need information about the second interval of the list.
+    Do this case split via an auxiliary function! Otherwise, you may end up with a recursion equation of the form
+      \<open>f (x#xs) = \<dots> case xs of x'#xs' \<Rightarrow> \<dots> f (x'#xs') \<dots>\<close>
+    combined with \<open>split: list.splits\<close> this will make the simplifier loop!
+
+\<close>
+
+
+text \<open>\Exercise{Optimized Mergesort}
+
+  Import @{theory "Sorting"} for this exercise.
+  The @{const msort} function recomputes the length of the list in each iteration.
+  Implement an optimized version that has an additional parameter keeping track
+  of the length, and show that it is equal to the original @{const msort}.
+\<close>
+
+(* Optimized mergesort *)
+
+fun msort2 :: "nat \<Rightarrow> 'a::linorder list \<Rightarrow> 'a list"
+  where "msort2 _ _ = undefined"
+
+lemma "n = length xs \<Longrightarrow> msort2 n xs = msort xs"
+  oops
+
+text \<open>Hint:
+  Use @{thm [source] msort.simps} only when instantiated to a particular \<open>xs\<close>
+  (@{thm [source] msort.simps[of xs]}),
+  otherwise the simplifier will loop!
+\<close>
+
+
+
+text \<open> \NumHomework{Deletion from Interval Lists}{June 1}
+
+  Implement and prove correct a delete function.
+
+  Hints:
+    \<^item> The correctness lemma is analogous to the one for add.
+    \<^item> A monotonicity property on \<open>inv'\<close> may be useful, i.e.,
+      @{prop \<open>inv' m is \<Longrightarrow> inv' m' is\<close>} if @{prop \<open>m'\<le>m\<close>}
+    \<^item> A bounding lemma, relating \<open>m\<close> and the elements of @{term \<open>set_of is\<close>}
+      if @{prop \<open>inv' m is\<close>}, may be useful.
+\<close>
+
+
+
+fun del :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "del _ _ = undefined"
+
+lemma del_correct: "Come up with a meaningful spec yourself" oops
+
+
+
+text \<open> \NumHomework{Addition of Interval to Interval List}{June 1}
+  For 3 \<^bold>\<open>bonus points\<close>, implement and prove correct a function
+  to add a whole interval to an interval list. The runtime must
+  not depend on the size of the interval, e.g., iterating over the
+  interval and adding the elements separately is not allowed!
+\<close>
+
+fun addi :: "nat \<Rightarrow> nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "addi i j is = undefined"
+
+lemma addi_correct:
+  assumes "inv is" "i\<le>j"
+  shows "inv (addi i j is)" "set_of (addi i j is) = {i..j} \<union> (set_of is)"
+  sorry
+
+
+(*<*)
+end
+(*>*)
diff --git a/07/tmpl0arun7.thy b/07/tmpl0arun7.thy
new file mode 100644
index 0000000..a4e25f8
--- /dev/null
+++ b/07/tmpl0arun7.thy
@@ -0,0 +1,222 @@
+(*<*)
+theory tmpl0arun7
+  imports Main "HOL-Data_Structures.Sorting"
+begin
+(*>*)
+
+hide_const (open) inv (*inv is used as a constant in isabelle, renaming it pretty prints the const 
+with the long name if the const is not hidden*)
+
+text {* \ExerciseSheet{7}{25.~5.~2018} *}
+
+
+text {* \Exercise{Interval Lists}
+
+ Sets of natural numbers can be implemented as lists of intervals, where
+an interval is simply a pair of numbers.  For example the set @{term "{2, 3, 5,
+7, 8, 9::nat}"} can be represented by the list @{term "[(2, 3), (5, 5),
+(7::nat, 9::nat)]"}.  A typical application is the list of free blocks of
+dynamically allocated memory. *}
+
+text {* We introduce the type *}
+
+type_synonym intervals = "(nat*nat) list"
+
+text {* Next, define an \emph{invariant}
+that characterizes valid interval lists:
+For efficiency reasons intervals should be sorted in ascending order, the lower
+bound of each interval should be less than or equal to the upper bound, and the
+intervals should be chosen as large as possible, i.e.\ no two adjacent
+intervals should overlap or even touch each other.  It turns out to be
+convenient to define @{term inv} in terms of a more general function
+such that the additional argument is a lower bound for the intervals in
+the list:*}
+
+fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
+  "inv' n [] \<longleftrightarrow> True"|
+  "inv' n ((a,b)#ivs) \<longleftrightarrow> n\<le>a \<and> a\<le>b \<and> inv' (b+2) ivs"
+
+definition inv where "inv = inv' 0"
+
+
+
+text {* To relate intervals back to sets define an \emph{abstraction function}*}
+
+fun set_of :: "intervals => nat set"
+where
+  "set_of [] = {}"|
+  "set_of ((a,b)#ivs) = {a..b} \<union> set_of ivs"
+(*{a..<b} for non inclusive bound*)
+
+text \<open>Define a function to add a single element to the interval list,
+  and show its correctness\<close>
+
+fun merge_aux where
+  "merge_aux a b [] = [(a,b)]"|
+  "merge_aux a b ((c,d)#ivs) = (if b+1 = c then (a,d)#ivs else (a,b)#(c,d)#ivs)"
+
+fun add :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+  where
+  "add i [] = [(i,i)]"|
+(*i can be less than a, a-1, between a and b, b+1, greater than b. if b+1 might need to merge with next element too*)
+  "add i ((a,b)#ivs) = (
+    if i+1 < a then (i,i)#(a,b)#ivs
+    else if i+1 = a then (i,b)#ivs
+    else if i\<le>b then (a,b)#ivs
+    else if i = b+1 then merge_aux a i ivs
+    else (a,b)#add i ivs
+)"
+
+(* the (a,b)#add i ivs uses ivs which might cause infinite case splits on ivs when originally 
+the case split on ivs is done in the add function itself, therefore we write a different function for 
+the case splitting
+ else if i = b+1 then case ivs of 
+      [] \<Rightarrow> [(a,i)]|
+      (c,d)#ivs' \<Rightarrow> if i+1 = c then (a,d)#ivs' else (a,i)#ivs*)
+
+lemma add_pres_inv': "n\<le>x \<Longrightarrow> inv' n itl \<Longrightarrow> inv' n (add x itl)"
+  apply(induction itl arbitrary: n) (*arbitrary n as the value of n changes in the inv' function definition*)
+   apply simp (*simp here keeps induction step as (add x (a #itl)) instead of (a,b) *)
+  apply auto (*after this sledgehammer can solve this, auto case splits on products not on anything else,
+              hence we need to case split on merge_aux*)
+  apply (case_tac itl) (*case split by apply (case_tac itl) but it is unstable so don't use except to verify*)
+  apply auto
+  done
+
+lemma add_pres_inv: "n\<le>x \<Longrightarrow> inv' n itl \<Longrightarrow> inv' n (add x itl)"
+proof (induction itl arbitrary:n)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case
+    apply (cases a)
+    apply (cases itl)
+    apply auto
+    done
+qed
+  
+lemma set_of_add:
+  assumes "n\<le>x"
+  assumes "inv' n itl"
+  shows "set_of (add x itl) = {x} \<union> set_of itl"
+  using assms
+proof (induction itl arbitrary:n)
+case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case 
+    apply (cases a)
+    apply (cases itl)
+     apply (auto split: if_splits)  (*the apply auto without splitting on ifs shows 10 subcases where it shows all
+                                      the if cases in each subcase split: if_splits/if_split_asm where asm is 
+                                      assumptions*)
+    done
+qed
+(*not in ex but done in class*)
+consts
+  a :: "nat"
+  b :: "nat set"
+  c :: "nat set"
+
+lemma A: "{a} \<union> b = c" sorry
+
+lemma B: "{a} \<union> b \<union> d = c \<union> d"
+  using A apply simp (*doing apply (simp add: A) will simplify it to insert a (b \<union> d) = c \<union> d *)
+  done
+(*not in ex*)
+lemma add_correct:
+  assumes "inv itl"
+  shows "inv (add x itl)" "set_of (add x itl) = insert x (set_of itl)"
+  using add_pres_inv' assms tmpl0arun7.inv_def apply fastforce
+  using assms set_of_add tmpl0arun7.inv_def by fastforce
+
+text \<open>Hints:
+  \<^item> Sketch the different cases (position of element relative to the first interval of the list)
+    on paper first
+  \<^item> In one case, you will also need information about the second interval of the list.
+    Do this case split via an auxiliary function! Otherwise, you may end up with a recursion equation of the form
+      \<open>f (x#xs) = \<dots> case xs of x'#xs' \<Rightarrow> \<dots> f (x'#xs') \<dots>\<close>
+    combined with \<open>split: list.splits\<close> this will make the simplifier loop!
+
+\<close>
+
+
+text \<open>\Exercise{Optimized Mergesort}
+
+  Import @{theory "Sorting"} for this exercise.
+  The @{const msort} function recomputes the length of the list in each iteration.
+  Implement an optimized version that has an additional parameter keeping track
+  of the length, and show that it is equal to the original @{const msort}.
+\<close>
+
+(* Optimized mergesort *)
+
+fun msort2 :: "nat \<Rightarrow> 'a::linorder list \<Rightarrow> 'a list" where
+  "msort2 n xs = (
+    if n \<le> 1 then xs
+    else merge (msort2 (n div 2) (take (n div 2) xs)) (msort2 (n - n div 2) (drop (n div 2) xs)))"
+
+declare msort2.simps [simp del]
+
+lemma "n = length xs \<Longrightarrow> msort2 n xs = msort xs"
+proof (induction n xs rule:msort2.induct)
+  case (1 n xs)
+  then show ?case 
+    apply (auto simp: msort.simps[of xs] msort2.simps[of _ xs]) (*simplifier works innermost to out and  using
+                                                                  substitutes instead*)
+    done
+qed
+ 
+
+text \<open>Hint:
+  Use @{thm [source] msort.simps} only when instantiated to a particular \<open>xs\<close>
+  (@{thm [source] msort.simps[of xs]}),
+  otherwise the simplifier will loop!
+\<close>
+
+
+
+text \<open> \NumHomework{Deletion from Interval Lists}{June 1}
+
+  Implement and prove correct a delete function.
+
+  Hints:
+    \<^item> The correctness lemma is analogous to the one for add.
+    \<^item> A monotonicity property on \<open>inv'\<close> may be useful, i.e.,
+      @{prop \<open>inv' m is \<Longrightarrow> inv' m' is\<close>} if @{prop \<open>m'\<le>m\<close>}
+    \<^item> A bounding lemma, relating \<open>m\<close> and the elements of @{term \<open>set_of is\<close>}
+      if @{prop \<open>inv' m is\<close>}, may be useful.
+\<close>
+
+
+
+fun del :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "del _ _ = undefined"
+
+lemma del_correct: "Come up with a meaningful spec yourself" oops
+
+
+
+text \<open> \NumHomework{Addition of Interval to Interval List}{June 1}
+  For 3 \<^bold>\<open>bonus points\<close>, implement and prove correct a function
+  to add a whole interval to an interval list. The runtime must
+  not depend on the size of the interval, e.g., iterating over the
+  interval and adding the elements separately is not allowed!
+\<close>
+
+fun addi :: "nat \<Rightarrow> nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "addi i j is = undefined"
+
+lemma addi_correct:
+  assumes "inv is" "i\<le>j"
+  shows "inv (addi i j is)" "set_of (addi i j is) = {i..j} \<union> (set_of is)"
+  sorry
+
+
+(*<*)
+end
+(*>*)
diff --git a/07/tmpl0arun7.thy~ b/07/tmpl0arun7.thy~
new file mode 100644
index 0000000..91dd884
--- /dev/null
+++ b/07/tmpl0arun7.thy~
@@ -0,0 +1,222 @@
+(*<*)
+theory tmpl07
+  imports Main "HOL-Data_Structures.Sorting"
+begin
+(*>*)
+
+hide_const (open) inv (*inv is used as a constant in isabelle, renaming it pretty prints the const 
+with the long name if the const is not hidden*)
+
+text {* \ExerciseSheet{7}{25.~5.~2018} *}
+
+
+text {* \Exercise{Interval Lists}
+
+ Sets of natural numbers can be implemented as lists of intervals, where
+an interval is simply a pair of numbers.  For example the set @{term "{2, 3, 5,
+7, 8, 9::nat}"} can be represented by the list @{term "[(2, 3), (5, 5),
+(7::nat, 9::nat)]"}.  A typical application is the list of free blocks of
+dynamically allocated memory. *}
+
+text {* We introduce the type *}
+
+type_synonym intervals = "(nat*nat) list"
+
+text {* Next, define an \emph{invariant}
+that characterizes valid interval lists:
+For efficiency reasons intervals should be sorted in ascending order, the lower
+bound of each interval should be less than or equal to the upper bound, and the
+intervals should be chosen as large as possible, i.e.\ no two adjacent
+intervals should overlap or even touch each other.  It turns out to be
+convenient to define @{term inv} in terms of a more general function
+such that the additional argument is a lower bound for the intervals in
+the list:*}
+
+fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
+  "inv' n [] \<longleftrightarrow> True"|
+  "inv' n ((a,b)#ivs) \<longleftrightarrow> n\<le>a \<and> a\<le>b \<and> inv' (b+2) ivs"
+
+definition inv where "inv = inv' 0"
+
+
+
+text {* To relate intervals back to sets define an \emph{abstraction function}*}
+
+fun set_of :: "intervals => nat set"
+where
+  "set_of [] = {}"|
+  "set_of ((a,b)#ivs) = {a..b} \<union> set_of ivs"
+(*{a..<b} for non inclusive bound*)
+
+text \<open>Define a function to add a single element to the interval list,
+  and show its correctness\<close>
+
+fun merge_aux where
+  "merge_aux a b [] = [(a,b)]"|
+  "merge_aux a b ((c,d)#ivs) = (if b+1 = c then (a,d)#ivs else (a,b)#(c,d)#ivs)"
+
+fun add :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+  where
+  "add i [] = [(i,i)]"|
+(*i can be less than a, a-1, between a and b, b+1, greater than b. if b+1 might need to merge with next element too*)
+  "add i ((a,b)#ivs) = (
+    if i+1 < a then (i,i)#(a,b)#ivs
+    else if i+1 = a then (i,b)#ivs
+    else if i\<le>b then (a,b)#ivs
+    else if i = b+1 then merge_aux a i ivs
+    else (a,b)#add i ivs
+)"
+
+(* the (a,b)#add i ivs uses ivs which might cause infinite case splits on ivs when originally 
+the case split on ivs is done in the add function itself, therefore we write a different function for 
+the case splitting
+ else if i = b+1 then case ivs of 
+      [] \<Rightarrow> [(a,i)]|
+      (c,d)#ivs' \<Rightarrow> if i+1 = c then (a,d)#ivs' else (a,i)#ivs*)
+
+lemma add_pres_inv': "n\<le>x \<Longrightarrow> inv' n itl \<Longrightarrow> inv' n (add x itl)"
+  apply(induction itl arbitrary: n) (*arbitrary n as the value of n changes in the inv' function definition*)
+   apply simp (*simp here keeps induction step as (add x (a #itl)) instead of (a,b) *)
+  apply auto (*after this sledgehammer can solve this, auto case splits on products not on anything else,
+              hence we need to case split on merge_aux*)
+  apply (case_tac itl) (*case split by apply (case_tac itl) but it is unstable so don't use except to verify*)
+  apply auto
+  done
+
+lemma add_pres_inv: "n\<le>x \<Longrightarrow> inv' n itl \<Longrightarrow> inv' n (add x itl)"
+proof (induction itl arbitrary:n)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case
+    apply (cases a)
+    apply (cases itl)
+    apply auto
+    done
+qed
+  
+lemma set_of_add:
+  assumes "n\<le>x"
+  assumes "inv' n itl"
+  shows "set_of (add x itl) = {x} \<union> set_of itl"
+  using assms
+proof (induction itl arbitrary:n)
+case Nil
+  then show ?case by auto
+next
+  case (Cons a itl)
+  then show ?case 
+    apply (cases a)
+    apply (cases itl)
+     apply (auto split: if_splits)  (*the apply auto without splitting on ifs shows 10 subcases where it shows all
+                                      the if cases in each subcase split: if_splits/if_split_asm where asm is 
+                                      assumptions*)
+    done
+qed
+(*not in ex but done in class*)
+consts
+  a :: "nat"
+  b :: "nat set"
+  c :: "nat set"
+
+lemma A: "{a} \<union> b = c" sorry
+
+lemma B: "{a} \<union> b \<union> d = c \<union> d"
+  using A apply simp (*doing apply (simp add: A) will simplify it to insert a (b \<union> d) = c \<union> d *)
+  done
+(*not in ex*)
+lemma add_correct:
+  assumes "inv itl"
+  shows "inv (add x itl)" "set_of (add x itl) = insert x (set_of itl)"
+  using add_pres_inv' assms tmpl07.inv_def apply fastforce
+  using assms set_of_add tmpl07.inv_def by fastforce
+
+text \<open>Hints:
+  \<^item> Sketch the different cases (position of element relative to the first interval of the list)
+    on paper first
+  \<^item> In one case, you will also need information about the second interval of the list.
+    Do this case split via an auxiliary function! Otherwise, you may end up with a recursion equation of the form
+      \<open>f (x#xs) = \<dots> case xs of x'#xs' \<Rightarrow> \<dots> f (x'#xs') \<dots>\<close>
+    combined with \<open>split: list.splits\<close> this will make the simplifier loop!
+
+\<close>
+
+
+text \<open>\Exercise{Optimized Mergesort}
+
+  Import @{theory "Sorting"} for this exercise.
+  The @{const msort} function recomputes the length of the list in each iteration.
+  Implement an optimized version that has an additional parameter keeping track
+  of the length, and show that it is equal to the original @{const msort}.
+\<close>
+
+(* Optimized mergesort *)
+
+fun msort2 :: "nat \<Rightarrow> 'a::linorder list \<Rightarrow> 'a list" where
+  "msort2 n xs = (
+    if n \<le> 1 then xs
+    else merge (msort2 (n div 2) (take (n div 2) xs)) (msort2 (n - n div 2) (drop (n div 2) xs)))"
+
+declare msort2.simps [simp del]
+
+lemma "n = length xs \<Longrightarrow> msort2 n xs = msort xs"
+proof (induction n xs rule:msort2.induct)
+  case (1 n xs)
+  then show ?case 
+    apply (auto simp: msort.simps[of xs] msort2.simps[of _ xs]) (*simplifier works innermost to out and  using
+                                                                  substitutes instead*)
+    done
+qed
+ 
+
+text \<open>Hint:
+  Use @{thm [source] msort.simps} only when instantiated to a particular \<open>xs\<close>
+  (@{thm [source] msort.simps[of xs]}),
+  otherwise the simplifier will loop!
+\<close>
+
+
+
+text \<open> \NumHomework{Deletion from Interval Lists}{June 1}
+
+  Implement and prove correct a delete function.
+
+  Hints:
+    \<^item> The correctness lemma is analogous to the one for add.
+    \<^item> A monotonicity property on \<open>inv'\<close> may be useful, i.e.,
+      @{prop \<open>inv' m is \<Longrightarrow> inv' m' is\<close>} if @{prop \<open>m'\<le>m\<close>}
+    \<^item> A bounding lemma, relating \<open>m\<close> and the elements of @{term \<open>set_of is\<close>}
+      if @{prop \<open>inv' m is\<close>}, may be useful.
+\<close>
+
+
+
+fun del :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "del _ _ = undefined"
+
+lemma del_correct: "Come up with a meaningful spec yourself" oops
+
+
+
+text \<open> \NumHomework{Addition of Interval to Interval List}{June 1}
+  For 3 \<^bold>\<open>bonus points\<close>, implement and prove correct a function
+  to add a whole interval to an interval list. The runtime must
+  not depend on the size of the interval, e.g., iterating over the
+  interval and adding the elements separately is not allowed!
+\<close>
+
+fun addi :: "nat \<Rightarrow> nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "addi i j is = undefined"
+
+lemma addi_correct:
+  assumes "inv is" "i\<le>j"
+  shows "inv (addi i j is)" "set_of (addi i j is) = {i..j} \<union> (set_of is)"
+  sorry
+
+
+(*<*)
+end
+(*>*)
diff --git a/07/tut07.thy b/07/tut07.thy
new file mode 100644
index 0000000..b334158
--- /dev/null
+++ b/07/tut07.thy
@@ -0,0 +1,197 @@
+(*<*)
+theory tut07
+  imports Main "HOL-Data_Structures.Sorting"
+begin
+(*>*)
+
+hide_const (open) inv
+
+
+text {* \ExerciseSheet{7}{25.~5.~2018} *}
+
+
+text {* \Exercise{Interval Lists}
+
+ Sets of natural numbers can be implemented as lists of intervals, where
+an interval is simply a pair of numbers.  For example the set @{term "{2, 3, 5,
+7, 8, 9::nat}"} can be represented by the list @{term "[(2, 3), (5, 5),
+(7::nat, 9::nat)]"}.  A typical application is the list of free blocks of
+dynamically allocated memory. *}
+
+text {* We introduce the type *}
+
+type_synonym intervals = "(nat*nat) list"
+
+text {* Next, define an \emph{invariant}
+that characterizes valid interval lists:
+For efficiency reasons intervals should be sorted in ascending order, the lower
+bound of each interval should be less than or equal to the upper bound, and the
+intervals should be chosen as large as possible, i.e.\ no two adjacent
+intervals should overlap or even touch each other.  It turns out to be
+convenient to define @{term inv} in terms of a more general function
+such that the additional argument is a lower bound for the intervals in
+the list:*}
+
+fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
+  "inv' n [] \<longleftrightarrow> True"
+| "inv' n ((a,b)#ivs) \<longleftrightarrow> n\<le>a \<and> a\<le>b \<and> inv' (b+2) ivs"
+
+definition inv where "inv = inv' 0"
+
+
+
+text {* To relate intervals back to sets define an \emph{abstraction function}*}
+
+fun set_of :: "intervals => nat set"
+where
+  "set_of [] = {}"
+| "set_of ((a,b)#ivs) = {a..b} \<union> set_of ivs"
+
+text \<open>Define a function to add a single element to the interval list,
+  and show its correctness\<close>
+
+
+fun merge_aux where
+  "merge_aux a b [] = [(a,b)]"
+| "merge_aux a b ((c,d)#ivs) = (if b+1=c then (a,d)#ivs else (a,b)#(c,d)#ivs)"
+
+fun add :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+  where
+  "add i [] = [(i,i)]"
+| "add i ((a,b)#ivs) = (
+    if i+1 < a then (i,i)#(a,b)#ivs
+    else if i+1 = a then (i,b)#ivs
+    else if i\<le>b then (a,b)#ivs
+    else if i=b+1 then merge_aux a i ivs
+    else (a,b)#add i ivs
+  )"
+
+
+lemma add_pres_inv:
+  "n\<le>x \<Longrightarrow> inv' n ivs \<Longrightarrow> inv' n (add x ivs)"
+proof (induction ivs arbitrary: n)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a ivs)
+  then show ?case
+    apply (cases a)
+    apply (cases ivs)
+    apply auto
+    done
+qed
+
+lemma set_of_add:
+  assumes "n\<le>x"
+  assumes "inv' n ivs"
+  shows "set_of (add x ivs) = {x} \<union> set_of ivs"
+  using assms
+proof (induction ivs arbitrary: n)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a ivs)
+  then show ?case
+    apply (cases a)
+    apply (cases ivs)
+    apply (auto split: if_splits)
+    done
+qed
+
+
+lemma add_correct:
+  assumes "inv is"
+  shows "inv (add x is)" "set_of (add x is) = {x} \<union> set_of is"
+  using add_pres_inv assms tut07.inv_def apply fastforce
+  using assms set_of_add tut07.inv_def by fastforce
+
+
+text \<open>Hints:
+  \<^item> Sketch the different cases (position of element relative to the first interval of the list)
+    on paper first
+  \<^item> In one case, you will also need information about the second interval of the list.
+    Do this case split via an auxiliary function! Otherwise, you may end up with a recursion equation of the form
+      \<open>f (x#xs) = \<dots> case xs of x'#xs' \<Rightarrow> \<dots> f (x'#xs') \<dots>\<close>
+    combined with \<open>split: list.splits\<close> this will make the simplifier loop!
+
+\<close>
+
+
+text \<open>\Exercise{Optimized Mergesort}
+
+  Import @{theory "Sorting"} for this exercise.
+  The @{const msort} function recomputes the length of the list in each iteration.
+  Implement an optimized version that has an additional parameter keeping track
+  of the length, and show that it is equal to the original @{const msort}.
+\<close>
+
+(* Optimized mergesort *)
+
+fun msort2 :: "nat \<Rightarrow> 'a::linorder list \<Rightarrow> 'a list" where
+"msort2 n xs = (
+  if n \<le> 1 then xs
+  else merge (msort2 (n div 2) (take (n div 2) xs)) (msort2 (n - n div 2) (drop (n div 2) xs)))"
+
+declare msort2.simps[simp del]
+
+lemma "n = length xs \<Longrightarrow> msort2 n xs = msort xs"
+proof (induction n xs rule: msort2.induct)
+  case (1 n xs)
+  then show ?case
+    using msort.simps[of xs] msort2.simps[of n xs]
+    apply (auto simp: )
+    done
+
+qed
+
+
+text \<open>Hint:
+  Use @{thm [source] msort.simps} only when instantiated to a particular \<open>xs\<close>
+  (@{thm [source] msort.simps[of xs]}),
+  otherwise the simplifier will loop!
+\<close>
+
+
+
+text \<open> \NumHomework{Deletion from Interval Lists}{June 1}
+
+  Implement and prove correct a delete function.
+
+  Hints:
+    \<^item> The correctness lemma is analogous to the one for add.
+    \<^item> A monotonicity property on \<open>inv'\<close> may be useful, i.e.,
+      @{prop \<open>inv' m is \<Longrightarrow> inv' m' is\<close>} if @{prop \<open>m'\<le>m\<close>}
+    \<^item> A bounding lemma, relating \<open>m\<close> and the elements of @{term \<open>set_of is\<close>}
+      if @{prop \<open>inv' m is\<close>}, may be useful.
+\<close>
+
+
+
+fun del :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "del _ _ = undefined"
+
+lemma del_correct: "Come up with a meaningful spec yourself" oops
+
+
+
+text \<open> \NumHomework{Addition of Interval to Interval List}{June 1}
+  For 3 \<^bold>\<open>bonus points\<close>, implement and prove correct a function
+  to add a whole interval to an interval list. The runtime must
+  not depend on the size of the interval, e.g., iterating over the
+  interval and adding the elements separately is not allowed!
+\<close>
+
+fun addi :: "nat \<Rightarrow> nat \<Rightarrow> intervals \<Rightarrow> intervals"
+where
+  "addi i j is = undefined"
+
+lemma addi_correct:
+  assumes "inv is" "i\<le>j"
+  shows "inv (addi i j is)" "set_of (addi i j is) = {i..j} \<union> (set_of is)"
+  sorry
+
+
+(*<*)
+end
+(*>*)
diff --git a/08/.hw08.thy.marks b/08/.hw08.thy.marks
new file mode 100644
index 0000000..eb6908e
Binary files /dev/null and b/08/.hw08.thy.marks differ
diff --git a/08/Untitled-1 b/08/Untitled-1
new file mode 100644
index 0000000..52f9218
--- /dev/null
+++ b/08/Untitled-1
@@ -0,0 +1,26 @@
+lemma min_corr: "avl t \<Longrightarrow> height t = h \<Longrightarrow> avl_minnodes_height h  \<le> size1 t"
+proof(induction t arbitrary:h)
+  case Leaf
+  then show ?case by auto
+next
+  case (Node t1 x2 t2)
+
+  note IH = Node.IH[OF _ refl]
+  then have ?case using IH
+      using Node.prems(1) Suc_eq_plus1 avl_size by force
+  have "height t1 = height t2 \<or> height t1 < height t2 \<or> height t1 > height t2" (is "?C1 \<or> ?C2 \<or> ?C3")
+    by auto
+  moreover {
+    assume ?C1 
+   (* have "h = Suc (height t1)" using Node.prems(2) \<open>height t1 = height t2\<close> by force*)
+    then have ?case using IH
+      using Node.prems(1) Suc_eq_plus1 avl_size by force
+  } moreover {
+    assume ?C2 have ?case sorry
+  } moreover {
+    assume ?C3 have ?case sorry
+  } ultimately show ?case by blast
+
+
+  then show ?case 
+qed
\ No newline at end of file
diff --git a/08/ex08.pdf b/08/ex08.pdf
new file mode 100644
index 0000000..1c164e6
Binary files /dev/null and b/08/ex08.pdf differ
diff --git a/08/hw08 b/08/hw08
new file mode 100644
index 0000000..e69de29
diff --git a/08/hw08.thy b/08/hw08.thy
new file mode 100644
index 0000000..ec77a60
--- /dev/null
+++ b/08/hw08.thy
@@ -0,0 +1,134 @@
+theory hw08
+  imports Complex_Main "HOL-Library.Tree"
+begin
+
+fun fib :: "nat \<Rightarrow> nat"
+  where
+    fib0: "fib 0 = 0"
+  | fib1: "fib (Suc 0) = 1"
+  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+
+lemma f_alt_induct [consumes 1, case_names 1 2 rec]:
+  assumes "n > 0"
+      and "P (Suc 0)" "P 2" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))"
+  shows   "P n"
+  using assms(1)
+proof (induction n rule: fib.induct)
+  case (3 n)
+  thus ?case using assms by (cases n) (auto simp: eval_nat_numeral)
+qed (auto simp: \<open>P (Suc 0)\<close> \<open>P 2\<close>)
+
+lemma fib_lowerbound: "n > 0 \<Longrightarrow> real (fib n) \<ge> 1.5 ^ n / 3"
+proof (induction n rule: f_alt_induct)
+case 1
+then show ?case by auto
+next
+  case 2
+  then show ?case by (auto simp:eval_nat_numeral)
+next
+  case (rec n)
+  then show ?case by auto
+qed
+
+
+
+
+fun avl :: "'a tree \<Rightarrow> bool"
+where
+  "avl (Node l _ r) = ((((height r::int) -(height l::int))\<in> {-1..1})\<and> avl l \<and> avl r)"
+| "avl (Leaf) = True"
+
+value "avl \<langle>\<langle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>\<rangle>"
+
+fun avl_minnodes_height::"nat \<Rightarrow> nat"
+  where
+  "avl_minnodes_height 0 = 1"
+| "avl_minnodes_height (Suc 0) = 2"
+| "avl_minnodes_height (Suc (Suc n)) = avl_minnodes_height n + avl_minnodes_height (Suc n)"
+
+
+value "height \<langle>\<langle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+value "size1 \<langle>\<langle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+
+value "height \<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>"
+value "size1  \<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>"
+
+value "height \<langle>\<rangle>"
+value "size1  \<langle>\<rangle>"
+
+value "height \<langle>\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+value "size1 \<langle>\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+value "avl \<langle>\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+
+lemma avl_size: " size1 (Node t1 x t2) = size1 t1 + size1 t2"
+  by simp
+
+lemma avl_min_mono: "avl_minnodes_height n \<le> avl_minnodes_height (Suc n)"
+  apply(induction n rule: avl_minnodes_height.induct)
+    apply(auto)
+  done
+
+
+lemma min_corr: "avl t \<Longrightarrow> height t = h \<Longrightarrow> avl_minnodes_height h  \<le> size1 t"
+proof(induction t arbitrary:h)
+  case Leaf
+  then show ?case by auto
+next
+  case (Node t1 x2 t2)
+  note IH = Node.IH[OF _ refl]
+    have "height t1 = height t2 \<or> height t1 < height t2 \<or> height t1 > height t2" (is "?C1 \<or> ?C2 \<or> ?C3")
+    by auto
+  moreover {
+    assume ?C1
+    have ?case using IH Node.prems \<open>?C1\<close>
+      apply (cases "height t2")
+       apply (auto)
+      by (meson add_mono_thms_linordered_semiring(1) avl_min_mono le_trans)
+
+  } moreover {
+    assume ?C2 
+    have "h = Suc (height t2)" using IH Node.prems  using \<open>?C2\<close> by force
+    then  have ?case using IH Node.prems \<open>?C2\<close>
+      apply (cases "height t2")
+       apply (auto)
+      by (simp add: le_less_Suc_eq)
+      
+  } moreover {
+    assume ?C3 
+     have "h = Suc (height t1)" using IH Node.prems  using \<open>?C3\<close> by force
+    then  have ?case using IH Node.prems \<open>?C3\<close>
+      apply (cases "height t1")
+       apply (auto)
+      by (simp add: le_less_Suc_eq)
+  } ultimately show ?case by blast
+ 
+qed
+
+  
+
+
+lemma fib_min: "fib (h+2)  = avl_minnodes_height h"
+  apply(induction h rule:avl_minnodes_height.induct)
+    apply(auto)
+  done
+
+lemma avl_fib_bound: "avl t \<Longrightarrow> height t = h \<Longrightarrow> fib (h+2) \<le> size1 t"
+  using fib_min le_trans min_corr by metis
+  
+
+
+lemma avl_lowerbound:
+  assumes "avl t"
+  shows "1.5 ^ (height t + 2) / 3 \<le> real (size1 t)"
+proof -
+  show ?thesis using assms fib_min le_trans min_corr fib_lowerbound
+    by (smt add_gr_0 avl_fib_bound of_nat_le_iff pos2)
+qed
+
+
+
+
+
+
+
+end
\ No newline at end of file
diff --git a/08/hw08.thy~ b/08/hw08.thy~
new file mode 100644
index 0000000..3f3326e
--- /dev/null
+++ b/08/hw08.thy~
@@ -0,0 +1,142 @@
+theory hw08
+  imports Complex_Main "HOL-Library.Tree"
+begin
+
+fun fib :: "nat \<Rightarrow> nat"
+  where
+    fib0: "fib 0 = 0"
+  | fib1: "fib (Suc 0) = 1"
+  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+
+lemma f_alt_induct [consumes 1, case_names 1 2 rec]:
+  assumes "n > 0"
+      and "P (Suc 0)" "P 2" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))"
+  shows   "P n"
+  using assms(1)
+proof (induction n rule: fib.induct)
+  case (3 n)
+  thus ?case using assms by (cases n) (auto simp: eval_nat_numeral)
+qed (auto simp: \<open>P (Suc 0)\<close> \<open>P 2\<close>)
+
+lemma fib_lowerbound: "n > 0 \<Longrightarrow> real (fib n) \<ge> 1.5 ^ n / 3"
+proof (induction n rule: f_alt_induct)
+case 1
+then show ?case by auto
+next
+  case 2
+  then show ?case by (auto simp:eval_nat_numeral)
+next
+  case (rec n)
+  then show ?case by auto
+qed
+
+
+
+
+fun avl :: "'a tree \<Rightarrow> bool"
+where
+  "avl (Node l _ r) = ((((height r::int) -(height l::int))\<in> {-1..1})\<and> avl l \<and> avl r)"
+| "avl (Leaf) = True"
+
+value "avl \<langle>\<langle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>\<rangle>"
+
+fun avl_minnodes_height::"nat \<Rightarrow> nat"
+  where
+  "avl_minnodes_height 0 = 1"
+| "avl_minnodes_height (Suc 0) = 2"
+| "avl_minnodes_height (Suc (Suc n)) = avl_minnodes_height n + avl_minnodes_height (Suc n)"
+
+lemma "avl_minnodes_height h = fib (h+2)"
+  apply(induction h rule:avl_minnodes_height.induct)
+    apply(auto)
+  done  
+
+
+
+value "height \<langle>\<langle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+value "size1 \<langle>\<langle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+
+value "height \<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>"
+value "size1  \<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>"
+
+value "height \<langle>\<rangle>"
+value "size1  \<langle>\<rangle>"
+
+value "height \<langle>\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+value "size1 \<langle>\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+value "avl \<langle>\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>,a,\<langle>\<langle>\<rangle>,a,\<langle>\<rangle>\<rangle>\<rangle>"
+
+lemma avl_size: " size1 (Node t1 x t2) = size1 t1 + size1 t2"
+  by simp
+
+lemma avl_min_mono: "avl_minnodes_height n \<le> avl_minnodes_height (Suc n)"
+  apply(induction n rule: avl_minnodes_height.induct)
+    apply(auto)
+  done
+
+
+lemma min_corr: "avl t \<Longrightarrow> height t = h \<Longrightarrow> avl_minnodes_height h  \<le> size1 t"
+proof(induction t arbitrary:h)
+  case Leaf
+  then show ?case by auto
+next
+  case (Node t1 x2 t2)
+  note IH = Node.IH[OF _ refl]
+    have "height t1 = height t2 \<or> height t1 < height t2 \<or> height t1 > height t2" (is "?C1 \<or> ?C2 \<or> ?C3")
+    by auto
+  moreover {
+    assume ?C1
+    have ?case using IH Node.prems \<open>?C1\<close>
+      apply (cases "height t2")
+       apply (auto)
+      by (meson add_mono_thms_linordered_semiring(1) avl_min_mono le_trans)
+
+  } moreover {
+    assume ?C2 
+    have "h = Suc (height t2)" using IH Node.prems by (simp add: \<open>height t1 < height t2\<close> add.right_neutral less_imp_le_nat max_def)
+    then  have ?case using IH Node.prems \<open>?C2\<close>
+      apply (cases "height t2")
+       apply (auto)
+      by (simp add: le_less_Suc_eq)
+      
+  } moreover {
+    assume ?C3 
+     have "h = Suc (height t1)" using IH Node.prems  using \<open>?C3\<close> by force
+    then  have ?case using IH Node.prems \<open>?C3\<close>
+      apply (cases "height t1")
+       apply (auto)
+      by (simp add: le_less_Suc_eq)
+  } ultimately show ?case by blast
+ 
+qed
+
+  
+
+
+lemma fib_min: "fib (h+2)  \<le> avl_minnodes_height h"
+  apply(induction h rule:avl_minnodes_height.induct)
+    apply(auto)
+  done
+
+lemma avl_fib_bound: "avl t \<Longrightarrow> height t = h \<Longrightarrow> fib (h+2) \<le> size1 t"
+  using fib_min le_trans min_corr by blast
+
+
+  
+
+
+lemma avl_lowerbound:
+  assumes "avl t"
+  shows "1.5 ^ (height t + 2) / 3 \<le> real (size1 t)"
+proof -
+  show ?thesis using assms fib_min le_trans min_corr fib_lowerbound
+    by (smt add_gr_0 avl_fib_bound of_nat_le_iff pos2)
+qed
+
+
+
+
+
+
+
+end
\ No newline at end of file
diff --git a/08/hw08bonustmpl.thy b/08/hw08bonustmpl.thy
new file mode 100644
index 0000000..6504fe4
--- /dev/null
+++ b/08/hw08bonustmpl.thy
@@ -0,0 +1,127 @@
+(*<*)
+theory hw08bonustmpl
+  imports
+    Main
+    "HOL-Data_Structures.Tree23_Set"
+begin
+(*>*)
+
+fun join :: "'a tree23 \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i"
+where
+  "join Leaf Leaf = T\<^sub>i Leaf"
+| "join (Node2 t1 a t2) (Node2 t3 b t4) = (
+    case (join t2 t3) of
+      T\<^sub>i t23 \<Rightarrow> T\<^sub>i (Node3 t1 a t23 b t4)
+    | Up\<^sub>i t2' x t3' \<Rightarrow> Up\<^sub>i (Node2 t1 a t2') x (Node2 t3' b t4)
+  )"
+| "join (Node2 t1 a t2) (Node3 t3 b t4 c t5) = (
+    case (join t2 t3) of
+      T\<^sub>i t23 \<Rightarrow> Up\<^sub>i (Node2 t1 a t23) b (Node2 t4 c t5)
+    | Up\<^sub>i t2' x t3' \<Rightarrow> Up\<^sub>i (Node2 t1 a t2') x (Node3 t3' b t4 c t5)
+)"
+| "join (Node3 t1 a t2 b t3) (Node2 t4 c t5) = (
+    case (join t3 t4) of
+      T\<^sub>i t34 \<Rightarrow> Up\<^sub>i (Node2 t1 a t2) b (Node2 t34 c t5)
+    | Up\<^sub>i t3' x t4' \<Rightarrow> Up\<^sub>i (Node2 t1 a t2) b (Node3 t3' x t4' c t5)
+)"
+| "join (Node3 t1 a t2 b t3) (Node3 t4 c t5 d t6) = (
+    case (join t3 t4) of
+      T\<^sub>i t34 \<Rightarrow> Up\<^sub>i (Node2 t1 a t2) b (Node3 t34 c t5 d t6)
+    | Up\<^sub>i t3' x t4' \<Rightarrow> Up\<^sub>i (Node3 t1 a t2 b t3') x (Node3 t4' c t5 d t6)
+)"
+| "join _ _ = T\<^sub>i Leaf"
+
+
+fun del' :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
+  "del' x Leaf = T\<^sub>d Leaf"
+| "del' x (Node2 Leaf a Leaf) = (if (x = a) then (Up\<^sub>d Leaf) else T\<^sub>d(Node2 Leaf a Leaf))"
+| "del' x (Node3 Leaf a Leaf b Leaf) = T\<^sub>d(if x = a then Node2 Leaf b Leaf else
+     if x = b then Node2 Leaf a Leaf
+     else Node3 Leaf a Leaf b Leaf)"
+| "del' x (Node2 l a r) =  (case cmp x a of
+     LT \<Rightarrow> node21 (del' x l) a r |
+     GT \<Rightarrow> node22 l a (del' x r) |
+     EQ \<Rightarrow>  T\<^sub>d(tree\<^sub>i(join l r)))"
+|"del' x (Node3 l a m b r) =
+  (case cmp x a of
+     LT \<Rightarrow> node31 (del' x l) a m b r |
+     EQ \<Rightarrow>  T\<^sub>d(Node2 tree\<^sub>i((join (l m)::'a tree23) d r)) |
+     GT \<Rightarrow>
+       (case cmp x b of
+          LT \<Rightarrow> node32 l a (del x m) b r |
+          EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
+          GT \<Rightarrow> node33 l a m b (del x r)))"
+
+
+fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
+"del x Leaf = T\<^sub>d Leaf" |
+"del x (Node2 Leaf a Leaf) =
+  (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
+"del x (Node3 Leaf a Leaf b Leaf) =
+  T\<^sub>d(if x = a then Node2 Leaf b Leaf else
+     if x = b then Node2 Leaf a Leaf
+     else Node3 Leaf a Leaf b Leaf)" |
+"del x (Node2 l a r) =
+  (case cmp x a of
+     LT \<Rightarrow> node21 (del x l) a r |
+     GT \<Rightarrow> node22 l a (del x r) |
+     EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
+"del x (Node3 l a m b r) =
+  (case cmp x a of
+     LT \<Rightarrow> node31 (del x l) a m b r |
+     EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
+     GT \<Rightarrow>
+       (case cmp x b of
+          LT \<Rightarrow> node32 l a (del x m) b r |
+          EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
+          GT \<Rightarrow> node33 l a m b (del x r)))"
+
+(* These are the two essential lemmas needed to instantiate the
+  set_by_ordered infrastructure with the new del function:
+
+  (You're not required to repeat the instantiation proof, just these two lemmas are enough. )
+*)
+lemma inorder_del': "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(tree\<^sub>d (del' x t)) = del_list x (inorder t)"
+  sorry
+
+lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del' x t))"
+  sorry
+
+text \<open>A few hints:
+  \<^item> Prove auxiliary lemmas on \<open>join\<close> that are suitable to discharge your proof obligations, and
+    disable simplification of join for your main proof (\<open>declare join.simps[simp del]\<close>).
+    This will make proof obligations more readable.
+  \<^item> Case splitting by \<open>simp\<close> or \<open>auto\<close> may take quite a long time.
+    Use \<open>split!:\<close> instead of \<open>split:\<close> to make it a bit faster.
+
+\<close>
+
+
+(* In case you are interested how to instantiate the infrastructure with
+  the new delete function: *)
+
+definition delete' :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+  "delete' x t = tree\<^sub>d(del' x t)"
+
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete'
+and inorder = inorder and inv = bal
+proof (standard, goal_cases)
+  case 2 thus ?case by(simp add: isin_set)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: delete'_def inorder_del')
+next
+  case 6 thus ?case by(simp add: bal_insert)
+next
+  case 7 thus ?case by(simp add: delete'_def bal_tree\<^sub>d_del)
+qed simp+
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/08/hw08bonustmpl.thy~ b/08/hw08bonustmpl.thy~
new file mode 100644
index 0000000..b5b5fa1
--- /dev/null
+++ b/08/hw08bonustmpl.thy~
@@ -0,0 +1,87 @@
+(*<*)
+theory hw08bonustmpl
+  imports
+    Main
+    "HOL-Data_Structures.Tree23_Set"
+begin
+(*>*)
+
+fun join :: "'a tree23 \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i"
+where
+  "join Leaf Leaf = T\<^sub>i Leaf"
+| "join (Node2 t1 a t2) (Node2 t3 b t4) = (
+    case (join t2 t3) of
+      T\<^sub>i t23 \<Rightarrow> T\<^sub>i (Node3 t1 a t23 b t4)
+    | Up\<^sub>i t2' x t3' \<Rightarrow> Up\<^sub>i (Node2 t1 a t2') x (Node2 t3' b t4)
+  )"
+| "join (Node2 t1 a t2) (Node3 t3 b t4 c t5) = (
+    case (join t2 t3) of
+      T\<^sub>i t23 \<Rightarrow> Up\<^sub>i (Node2 t1 a t23) b (Node2 t4 c t5)
+    | Up\<^sub>i t2' x t3' \<Rightarrow> Up\<^sub>i (Node2 t1 a t2') x (Node3 t3' b t4 c t5)
+)"
+| "join (Node3 t1 a t2 b t3) (Node2 t4 c t5) = (
+    case (join t3 t4) of
+      T\<^sub>i t34 \<Rightarrow> Up\<^sub>i (Node2 t1 a t2) b (Node2 t34 c t5)
+    | Up\<^sub>i t3' x t4' \<Rightarrow> Up\<^sub>i (Node2 t1 a t2) b (Node3 t3' x t4' c t5)
+)"
+| "join (Node3 t1 a t2 b t3) (Node3 t4 c t5 d t6) = (
+    case (join t3 t4) of
+      T\<^sub>i t34 \<Rightarrow> Up\<^sub>i (Node2 t1 a t2) b (Node3 t34 c t5 d t6)
+    | Up\<^sub>i t3' x t4' \<Rightarrow> Up\<^sub>i (Node3 t1 a t2 b t3') x (Node3 t4' c t5 d t6)
+)"
+| "join _ _ = T\<^sub>i Leaf"
+
+
+fun del' :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
+  "del' x Leaf = T\<^sub>d Leaf"
+
+
+(* These are the two essential lemmas needed to instantiate the
+  set_by_ordered infrastructure with the new del function:
+
+  (You're not required to repeat the instantiation proof, just these two lemmas are enough. )
+*)
+lemma inorder_del': "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+  inorder(tree\<^sub>d (del' x t)) = del_list x (inorder t)"
+  sorry
+
+lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del' x t))"
+  sorry
+
+text \<open>A few hints:
+  \<^item> Prove auxiliary lemmas on \<open>join\<close> that are suitable to discharge your proof obligations, and
+    disable simplification of join for your main proof (\<open>declare join.simps[simp del]\<close>).
+    This will make proof obligations more readable.
+  \<^item> Case splitting by \<open>simp\<close> or \<open>auto\<close> may take quite a long time.
+    Use \<open>split!:\<close> instead of \<open>split:\<close> to make it a bit faster.
+
+\<close>
+
+
+(* In case you are interested how to instantiate the infrastructure with
+  the new delete function: *)
+
+definition delete' :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+  "delete' x t = tree\<^sub>d(del' x t)"
+
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete'
+and inorder = inorder and inv = bal
+proof (standard, goal_cases)
+  case 2 thus ?case by(simp add: isin_set)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: delete'_def inorder_del')
+next
+  case 6 thus ?case by(simp add: bal_insert)
+next
+  case 7 thus ?case by(simp add: delete'_def bal_tree\<^sub>d_del)
+qed simp+
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/08/hw08tmpl.thy b/08/hw08tmpl.thy
new file mode 100644
index 0000000..5210424
--- /dev/null
+++ b/08/hw08tmpl.thy
@@ -0,0 +1,70 @@
+(*<*)
+theory hw08tmpl
+  imports Complex_Main "HOL-Library.Tree"
+begin
+(*>*)
+
+text {* \NumHomework{Bounding Fibonacci}{June 8}
+
+  We start by defining the Fibonacci sequence, and an alternative
+  induction scheme for indexes greater 0:
+*}
+
+fun fib :: "nat \<Rightarrow> nat"
+  where
+    fib0: "fib 0 = 0"
+  | fib1: "fib (Suc 0) = 1"
+  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+
+lemma f_alt_induct [consumes 1, case_names 1 2 rec]:
+  assumes "n > 0"
+      and "P (Suc 0)" "P 2" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))"
+  shows   "P n"
+  using assms(1)
+proof (induction n rule: fib.induct)
+  case (3 n)
+  thus ?case using assms by (cases n) (auto simp: eval_nat_numeral)
+qed (auto simp: \<open>P (Suc 0)\<close> \<open>P 2\<close>)
+
+text \<open>Show that the Fibonacci numbers grow exponentially, i.e., that they are
+  bounded from below by \<open>1.5\<^sup>n/3\<close>.
+
+  Use the alternative induction scheme defined above.
+\<close>
+lemma fib_lowerbound: "n > 0 \<Longrightarrow> real (fib n) \<ge> 1.5 ^ n / 3"
+proof (induction n rule: f_alt_induct)
+oops
+
+text \<open>
+  \NumHomework{AVL Trees}{June 8}
+
+  AVL trees are binary search trees where, for each node, the heights of
+  its subtrees differ by at most one. In this homework, you are to bound
+  the minimal number of nodes in an AVL tree of a given height.
+
+  First, define the AVL invariant on binary trees.
+  Note: In practice, one additionally stores the heights or height difference
+  in the nodes, but this is not required for this exercise.
+\<close>
+
+
+fun avl :: "'a tree \<Rightarrow> bool"
+where
+"avl _ = undefined"
+
+
+text \<open>Show that an AVL tree of height \<open>h\<close> has at least \<open>fib (h+2)\<close> nodes:\<close>
+lemma avl_fib_bound: "avl t \<Longrightarrow> height t = h \<Longrightarrow> fib (h+2) \<le> size1 t"
+  oops
+
+text \<open>Combine your results to get an exponential lower bound on the number
+  of nodes in an AVL tree.\<close>
+lemma avl_lowerbound:
+  assumes "avl t"
+  shows "1.5 ^ (height t + 2) / 3 \<le> real (size1 t)"
+  oops
+
+
+(*<*)
+end
+(*>*)
diff --git a/09/ex09.pdf b/09/ex09.pdf
new file mode 100644
index 0000000..55dda14
Binary files /dev/null and b/09/ex09.pdf differ
diff --git a/09/ex09.thy b/09/ex09.thy
new file mode 100644
index 0000000..672fb48
--- /dev/null
+++ b/09/ex09.thy
@@ -0,0 +1,58 @@
+(*<*)
+theory ex09
+  imports Main "HOL-Data_Structures.RBT_Set"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{9}{8.~6.~2018} *}
+
+text \<open>\Exercise{Indicate Unchanged by Option}
+
+  Write an insert function for red-black trees that either inserts the element
+  and returns a new tree, or returns None if the element was already in the tree
+\<close>
+
+fun ins' :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt option"
+(*<*)
+where
+"ins' x Leaf = Some (R Leaf x Leaf)" |
+"ins' x (B l a r) =
+  (case cmp x a of
+     LT \<Rightarrow> (case ins' x l of None \<Rightarrow> None | Some l \<Rightarrow> Some (baliL l a r)) |
+     GT \<Rightarrow> (case ins' x r of None \<Rightarrow> None | Some r \<Rightarrow> Some (baliR l a r)) |
+     EQ \<Rightarrow> None)" |
+"ins' x (R l a r) =
+  (case cmp x a of
+    LT \<Rightarrow> (case ins' x l of None \<Rightarrow> None | Some l \<Rightarrow> Some (R l a r)) |
+    GT \<Rightarrow> (case ins' x r of None \<Rightarrow> None | Some r \<Rightarrow> Some (R l a r)) |
+    EQ \<Rightarrow> None)"
+
+lemma baliR_id: "\<lbrakk>invc l; invc r\<rbrakk> \<Longrightarrow> baliR l a r = B l a r"
+  by (cases "(l,a,r)" rule: baliR.cases; auto)
+
+lemma baliL_id: "\<lbrakk>invc l; invc r\<rbrakk> \<Longrightarrow> baliL l a r = B l a r"
+  by (cases "(l,a,r)" rule: baliL.cases; auto)
+(*>*)
+
+lemma "invc t \<Longrightarrow> case ins' x t of None \<Rightarrow> ins x t = t | Some t' \<Rightarrow> ins x t = t'"
+(*<*)
+proof (induction x t rule: ins.induct)
+  case (1 x)
+  then show ?case by simp
+next
+  case (2 x l a r)
+
+  then show ?case
+    apply (auto split: option.splits simp: baliL_id baliR_id)
+    done
+
+next
+  case (3 x l a r)
+  then show ?case by (auto split: option.splits)
+qed
+(*>*)
+
+(*<*)
+end
+(*>*)
diff --git a/09/ex09_2.thy b/09/ex09_2.thy
new file mode 100644
index 0000000..8a083d9
--- /dev/null
+++ b/09/ex09_2.thy
@@ -0,0 +1,115 @@
+(*<*)
+theory ex09_2
+imports
+  "~~/src/HOL/Data_Structures/Tree23_Set"
+begin
+(*>*)
+
+text \<open>\Exercise{Joining 2-3-Trees}
+
+  Write a join function for 2-3-trees: The function shall take two
+  2-3-trees \<open>l\<close> and \<open>r\<close> and an element \<open>x\<close>, and return a new 2-3-tree with
+  the inorder-traversal \<open>l x r\<close> .
+
+  Write two functions, one for the height of \<open>l\<close> being greater, the
+  other for the height of \<open>r\<close> being greater.
+\<close>
+
+
+
+text \<open>\<open>height r\<close> greater\<close>
+fun joinL :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i"
+(*<*)
+where
+"joinL l x r =
+  (if height l = height r then Up\<^sub>i l x r
+   else case r of
+     Node2 r1 a r2 \<Rightarrow>
+       (case joinL l x r1 of
+         T\<^sub>i t \<Rightarrow> T\<^sub>i (Node2 t a r2) |
+         Up\<^sub>i t1 b t2 \<Rightarrow> T\<^sub>i (Node3 t1 b t2 a r2)) |
+     Node3 r1 a r2 b r3 \<Rightarrow> (case joinL l x r1 of
+         T\<^sub>i t \<Rightarrow> T\<^sub>i (Node3 t a r2 b r3) |
+         Up\<^sub>i t1 y t2 \<Rightarrow> Up\<^sub>i (Node2 t1 y t2) a (Node2 r2 b r3)))"
+(*>*)
+
+lemma bal_joinL: "\<lbrakk> bal l; bal r; height l \<le> height r \<rbrakk> \<Longrightarrow>
+  bal (tree\<^sub>i (joinL l x r)) \<and> height(joinL l x r) = height r"
+(*<*)
+apply(induction r)
+  apply simp
+ apply (fastforce simp: le_less split: up\<^sub>i.split)
+apply (fastforce simp: le_less split: up\<^sub>i.split)
+done
+(*>*)
+
+lemma inorder_joinL: "\<lbrakk> bal l; bal r; height l \<le> height r \<rbrakk> \<Longrightarrow> inorder (tree\<^sub>i (joinL l x r)) = inorder l @x # inorder r"
+(*<*)
+  apply(induction r)
+  apply (auto split: up\<^sub>i.splits)
+  done
+(*>*)
+
+text \<open>\<open>height l\<close> greater\<close>
+fun joinR :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i"
+(*<*)
+where
+"joinR l x r =
+  (if height l = height r then Up\<^sub>i l x r
+   else case l of
+     Node2 l1 a l2 \<Rightarrow>
+       (case joinR l2 x r of
+         T\<^sub>i t \<Rightarrow> T\<^sub>i (Node2 l1 a t) |
+         Up\<^sub>i t1 b t2 \<Rightarrow> T\<^sub>i (Node3 l1 a t1 b t2)) |
+     Node3 l1 a l2 b l3 \<Rightarrow> (case joinR l3 x r of
+         T\<^sub>i t \<Rightarrow> T\<^sub>i (Node3 l1 a l2 b t) |
+         Up\<^sub>i t1 y t2 \<Rightarrow> Up\<^sub>i (Node2 l1 a l2) b (Node2 t1 y t2)))"
+(*>*)
+
+lemma bal_joinR: "\<lbrakk> bal l; bal r; height l \<ge> height r \<rbrakk> \<Longrightarrow>
+  bal (tree\<^sub>i (joinR l x r)) \<and> height(joinR l x r) = height l"
+  text \<open>Note the generalization: We augmented the lemma with a statement about the height of the result.\<close>
+(*<*)
+apply(induction l)
+  apply simp
+ apply (auto simp: le_less split!: up\<^sub>i.splits tree23.split)[]
+apply (fastforce simp: le_less split: up\<^sub>i.split)
+done
+(*>*)
+
+lemma inorder_joinR: "\<lbrakk> bal l; bal r; height l \<ge> height r \<rbrakk> \<Longrightarrow> inorder (tree\<^sub>i (joinR l x r)) = inorder l @x # inorder r"
+(*<*)
+  apply(induction l)
+  apply simp
+  apply (auto split!: up\<^sub>i.splits tree23.split)
+  done
+(*>*)
+
+
+text \<open>Combine both functions\<close>
+fun join :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23"
+(*<*)
+where
+"join l x r =
+  (if height l > height r
+   then tree\<^sub>i(joinR l x r)
+   else if height l < height r
+   then tree\<^sub>i(joinL l x r)
+   else Node2 l x r)"
+(*>*)
+
+lemma "\<lbrakk> bal l; bal r \<rbrakk> \<Longrightarrow> bal (join l x r)"
+(*<*)
+  by(auto simp: bal_joinL bal_joinR simp del: joinL.simps joinR.simps)
+(*>*)
+
+lemma "\<lbrakk> bal l; bal r \<rbrakk> \<Longrightarrow> inorder (join l x r) = inorder l @x # inorder r"
+(*<*)
+  by(auto simp: inorder_joinL inorder_joinR simp del: joinL.simps joinR.simps)
+(*>*)
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/09/ex09_2tmpl.thy b/09/ex09_2tmpl.thy
new file mode 100644
index 0000000..93e6248
--- /dev/null
+++ b/09/ex09_2tmpl.thy
@@ -0,0 +1,78 @@
+(*<*)
+theory ex09_2tmpl
+imports
+  "~~/src/HOL/Data_Structures/Tree23_Set"
+begin
+(*>*)
+
+text \<open>\Exercise{Joining 2-3-Trees}
+
+  Write a join function for 2-3-trees: The function shall take two
+  2-3-trees \<open>l\<close> and \<open>r\<close> and an element \<open>x\<close>, and return a new 2-3-tree with
+  the inorder-traversal \<open>l x r\<close> .
+
+  Write two functions, one for the height of \<open>l\<close> being greater, the
+  other for the height of \<open>r\<close> being greater.
+\<close>
+
+text \<open>\<open>height l\<close> greater\<close>
+fun joinR :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i"
+where
+  "joinR l x r = (
+    if height l = height r then Up\<^sub>i l x r
+    else case l of
+      Node2 l1 a l2 \<Rightarrow> (case joinR l2 x r of
+        T\<^sub>i t \<Rightarrow> T\<^sub>i (Node2 l1 a t)
+      | Up\<^sub>i l2' x' r' \<Rightarrow> T\<^sub>i (Node3 l1 a l2' x' r')
+      )
+    | Node3 l1 a l2 b l3 \<Rightarrow> (case joinR l3 x r of
+        T\<^sub>i t \<Rightarrow> T\<^sub>i (Node3 l1 a l2 b t)
+      | Up\<^sub>i l2' x' r' \<Rightarrow> Up\<^sub>i (Node2 l1 a l2) b (Node2 l2' x' r')
+    )
+    )"
+
+declare joinR.simps[simp del]
+
+
+lemma inorder_joinR: "\<lbrakk> bal l; bal r; height l \<ge> height r \<rbrakk> \<Longrightarrow> inorder (tree\<^sub>i (joinR l x r)) = inorder l @x # inorder r"
+  apply (induction l x r rule: joinR.induct)
+  apply (subst joinR.simps)
+  apply (fastforce split!: tree23.split up\<^sub>i.split)
+  done
+
+lemma bal_joinR: "\<lbrakk> bal l; bal r; height l \<ge> height r \<rbrakk> \<Longrightarrow>
+  bal (tree\<^sub>i (joinR l x r)) \<and> height(joinR l x r) = height l"
+  sorry
+
+
+
+text \<open>\<open>height r\<close> greater\<close>
+fun joinL :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i"
+where
+  "joinL l x r = undefined"
+
+lemma bal_joinL: "\<lbrakk> bal l; bal r; height l \<le> height r \<rbrakk> \<Longrightarrow>
+  bal (tree\<^sub>i (joinL l x r)) \<and> height(joinL l x r) = height r"
+  text \<open>Note the generalization: We augmented the lemma with a statement about the height of the result.\<close>
+  sorry
+
+lemma inorder_joinL: "\<lbrakk> bal l; bal r; height l \<le> height r \<rbrakk> \<Longrightarrow> inorder (tree\<^sub>i (joinL l x r)) = inorder l @x # inorder r"
+  sorry
+
+
+text \<open>Combine both functions\<close>
+fun join :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23"
+where
+"join l x r = undefined"
+
+
+lemma "\<lbrakk> bal l; bal r \<rbrakk> \<Longrightarrow> bal (join l x r)"
+  sorry
+
+lemma "\<lbrakk> bal l; bal r \<rbrakk> \<Longrightarrow> inorder (join l x r) = inorder l @x # inorder r"
+  sorry
+
+
+(*<*)
+end
+(*>*)
diff --git a/09/ex09tmpl.thy b/09/ex09tmpl.thy
new file mode 100644
index 0000000..932ffa7
--- /dev/null
+++ b/09/ex09tmpl.thy
@@ -0,0 +1,59 @@
+(*<*)
+theory ex09tmpl
+  imports Main "HOL-Data_Structures.RBT_Set"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{9}{8.~6.~2018} *}
+
+text \<open>\Exercise{Indicate Unchanged by Option}
+
+  Write an insert function for red-black trees that either inserts the element
+  and returns a new tree, or returns None if the element was already in the tree
+\<close>
+
+term map_option
+
+fun ins' :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt option"
+where
+"ins' x Leaf = Some (R Leaf x Leaf)" |
+"ins' x (B l a r) =
+  (case cmp x a of
+     LT \<Rightarrow> (case ins' x l of None \<Rightarrow> None | Some l' \<Rightarrow> Some (baliL l' a r)) |
+     GT \<Rightarrow> (case ins' x r of None \<Rightarrow> None | Some r' \<Rightarrow> Some (baliR l a r')) |
+     EQ \<Rightarrow> None)" |
+"ins' x (R l a r) =
+  (case cmp x a of
+    LT \<Rightarrow> (case ins' x l of None \<Rightarrow> None | Some l' \<Rightarrow> Some (R l' a r)) |
+    GT \<Rightarrow> (case ins' x r of None \<Rightarrow> None | Some r' \<Rightarrow> Some (R l a r')) |
+    EQ \<Rightarrow> None)"
+
+lemma [simp]: "\<lbrakk>invc r\<rbrakk> \<Longrightarrow> baliR l a r = B l a r"
+  by (cases "(l,a,r)" rule: baliR.cases; simp)
+
+lemma [simp]: "\<lbrakk>invc l\<rbrakk> \<Longrightarrow> baliL l a r = B l a r"
+  by (cases "(l,a,r)" rule: baliL.cases; simp)
+
+lemma X1: "invc t \<Longrightarrow> case ins' x t of None \<Rightarrow> ins x t = t | Some t' \<Rightarrow> ins x t = t'"
+  by (induction x t rule: ins'.induct) (auto split: option.split)
+
+lemma [simp]: "size (baliR l x r) = size l + size r + 1"
+  apply (cases "(l,x,r)" rule: baliR.cases) by auto
+
+lemma [simp]: "size (baliL l x r) = size l + size r + 1"
+  apply (cases "(l,x,r)" rule: baliL.cases) by auto
+
+lemma X2: "invc t \<Longrightarrow> ins' x t = Some t' \<Longrightarrow> size t < size t'"
+  apply (induction x t arbitrary: t' rule: ins'.induct)
+  apply (auto split: option.splits if_splits)
+  done
+
+
+lemma "invc t \<Longrightarrow> case ins' x t of None \<Rightarrow> ins x t = t | Some t' \<Rightarrow> ins x t = t' \<and> t\<noteq>t'"
+  using X1[of t x] X2[of t x] by (auto split: option.split)
+
+
+(*<*)
+end
+(*>*)
diff --git a/09/ex09tmpl.thy~ b/09/ex09tmpl.thy~
new file mode 100644
index 0000000..f7ec48a
--- /dev/null
+++ b/09/ex09tmpl.thy~
@@ -0,0 +1,24 @@
+(*<*)
+theory ex09tmpl
+  imports Main "HOL-Data_Structures.RBT_Set"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{9}{8.~6.~2018} *}
+
+text \<open>\Exercise{Indicate Unchanged by Option}
+
+  Write an insert function for red-black trees that either inserts the element
+  and returns a new tree, or returns None if the element was already in the tree
+\<close>
+
+fun ins' :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt option"
+where
+"ins' _ _ = undefined"
+
+lemma "invc t \<Longrightarrow> case ins' x t of None \<Rightarrow> ins x t = t | Some t' \<Rightarrow> ins x t = t'"
+  sorry
+(*<*)
+end
+(*>*)
diff --git a/09/hw09.thy b/09/hw09.thy
new file mode 100644
index 0000000..2ee9ddd
--- /dev/null
+++ b/09/hw09.thy
@@ -0,0 +1,158 @@
+theory hw09
+  imports Main "HOL-Data_Structures.RBT_Set"
+begin
+
+
+
+fun min_height :: "('a,'b) tree \<Rightarrow> nat" where
+"min_height Leaf = 0" |
+"min_height (Node _ l _ r) = min (min_height l) (min_height r) + 1"
+
+definition "balanced t \<equiv> height t - min_height t \<le> 1"
+
+
+
+fun mk_rbt :: "('a,unit) tree \<Rightarrow> 'a rbt" where
+  "mk_rbt Leaf = Leaf"
+| "mk_rbt (Node _ l a r) = (let
+    l'=mk_rbt l;
+    r'=mk_rbt r
+  in
+    if min_height l > min_height r then
+      B (paint Red l') a r'
+    else if min_height l < min_height r then
+      B l' a (paint Red r')
+    else
+      B l' a r'
+  )"
+
+
+text \<open>
+  \subsection*{Warmup}
+
+\<close>
+
+lemma balanced_subt: "balanced (Node c l a r) \<Longrightarrow> balanced l \<and> balanced r"
+  unfolding balanced_def by auto
+
+
+lemma aux1:"height t \<ge> min_height t"
+  apply(induction t)
+  by auto
+
+lemma balanced_alt:
+  "balanced t \<longleftrightarrow> height t = min_height t \<or> height t = min_height t + 1"
+  unfolding balanced_def
+  by (metis One_nat_def add_diff_cancel_left' aux1 cancel_comm_monoid_add_class.diff_cancel le_Suc_eq le_add_diff_inverse le_zero_eq order_refl)
+
+text \<open>
+  \subsection*{The Easy Parts}
+\<close>
+
+
+lemma mk_rbt_inorder: "inorder (mk_rbt t) = inorder t"
+  apply(induction t)
+   apply(auto)
+  by (smt inorder.simps(2) inorder_paint)
+
+
+lemma mk_rbt_color: "color (mk_rbt t) = Black"
+  apply(induction t)
+   apply(auto)
+  by (smt RBT_Set.color.simps(2))
+
+text \<open>
+  \subsection*{Medium Complex Parts}
+
+\<close>
+
+
+
+lemma mk_rbt_bheight: "balanced t \<Longrightarrow> bheight (mk_rbt t) = min_height t"
+proof(induction t)
+  case Leaf
+  then show ?case by auto
+next
+  case (Node x1 t1 x3 t2)
+  note IH = Node.IH
+  have "min_height t1 = min_height t2 \<or> min_height t1 < min_height t2 \<or> min_height t1 > min_height t2" (is "?C1 \<or> ?C2 \<or> ?C3")
+    by auto
+  moreover
+  {
+    assume ?C1
+    have ?case using IH Node.prems \<open>?C1\<close>
+      apply(cases "min_height t1")
+       apply(auto)
+       apply (meson balanced_subt)
+      by (meson balanced_subt)
+    }
+    moreover
+    {
+      assume ?C2
+      have ?case using IH Node.prems \<open>?C2\<close>
+        apply(cases "min_height t1")
+         apply(auto)
+         apply (meson balanced_subt)
+        by (metis balanced_subt min.strict_order_iff)
+    }
+    moreover
+    {
+      assume ?C3
+      then have h0:"min_height (Node x1 t1 x3 t2) = min_height t2 + 1" using IH Node.prems by force
+      then have h1:"min_height t2 = 0 \<Longrightarrow> bheight (paint Red (mk_rbt t1)) = 0" using IH Node.prems
+        by (metis (no_types, lifting) One_nat_def Suc_eq_plus1 Suc_leI \<open>min_height t2 < min_height t1\<close> add_diff_cancel_right' aux1 balanced_def bheight_paint_Red height.simps(2) le_trans max.commute max_def mk_rbt_color)
+      then have h2: "min_height t1 > min_height t2 \<Longrightarrow> min_height t1 = Suc (min_height t2)" using IH Node.prems
+        by (smt Suc_eq_plus1 Suc_leI Suc_mono balanced_alt balanced_subt h0 height.simps(2) less_Suc_eq max.commute max_def not_le)
+      then have h3: " min_height t1 > min_height t2 \<Longrightarrow> bheight (paint Red (mk_rbt t1)) = min_height t2" using IH Node.prems
+        apply(cases "min_height t1")
+         apply(auto)
+        by (metis Suc_eq_plus1 add_diff_cancel_right' balanced_subt bheight_paint_Red mk_rbt_color)
+        
+      then have ?case using IH Node.prems \<open>?C3\<close> 
+        apply(cases "min_height t2")
+        by (auto)
+        
+      }
+      ultimately show ?case by blast
+qed
+
+
+lemma mk_rbt_invh: "balanced t \<Longrightarrow> invh (mk_rbt t)"
+  apply(induction t rule:mk_rbt.induct)
+   apply(simp add: balanced_alt mk_rbt_color mk_rbt_inorder mk_rbt_bheight)
+  apply(simp split:if_splits)
+  by (smt Suc_eq_plus1 Suc_le_mono add_diff_cancel_right' antisym_conv balanced_alt balanced_subt bheight_paint_Red height.simps(2) invh.simps(2) le_Suc_eq le_simps(3) max_def min_def invh_paint min_height.simps(2) mk_rbt_bheight mk_rbt_color)
+
+
+
+
+
+
+fun mk_rbt' :: "('a,unit) tree \<Rightarrow> 'a rbt \<times> nat"
+where
+  "mk_rbt' Leaf = (Leaf, 0)"
+| "mk_rbt' (Node _ l a r) = (let
+    (l',lx)=mk_rbt' l;
+    (r',rx)=mk_rbt' r
+  in
+    if lx > rx then
+      (B (paint Red l') a r', Suc(rx))
+    else if lx < rx then
+      (B l' a (paint Red r'), Suc(lx))
+    else
+      (B l' a r', Suc(lx))
+  )" 
+
+lemma mk_rbt'_refine_aux: "mk_rbt' t = (mk_rbt t, min_height t)"
+  apply(induction t)
+  apply(auto)
+  done
+
+
+lemma mk_rbt'_refine: "fst (mk_rbt' t) = mk_rbt t"
+  apply(induction t)
+  by(auto simp:mk_rbt'_refine_aux)
+
+
+
+end
diff --git a/09/hw09tmpl.thy b/09/hw09tmpl.thy
new file mode 100644
index 0000000..c339d28
--- /dev/null
+++ b/09/hw09tmpl.thy
@@ -0,0 +1,239 @@
+(*<*)
+theory hw09tmpl
+  imports Main "HOL-Data_Structures.RBT_Set"
+begin
+(*>*)
+
+text \<open>\NumHomework{Balanced Tree to RBT}{15.~6.~2018}
+
+  A tree is balanced, if its minimum height and its height differ by at most 1.
+\<close>
+
+fun min_height :: "('a,'b) tree \<Rightarrow> nat" where
+"min_height Leaf = 0" |
+"min_height (Node _ l _ r) = min (min_height l) (min_height r) + 1"
+
+definition "balanced t \<equiv> height t - min_height t \<le> 1"
+
+text \<open>The following function paints a balanced tree to form a valid red-black tree
+  with the same structure. The task of this homework is to prove this!
+\<close>
+
+fun mk_rbt :: "('a,unit) tree \<Rightarrow> 'a rbt" where
+  "mk_rbt Leaf = Leaf"
+| "mk_rbt (Node _ l a r) = (let
+    l'=mk_rbt l;
+    r'=mk_rbt r
+  in
+    if min_height l > min_height r then
+      B (paint Red l') a r'
+    else if min_height l < min_height r then
+      B l' a (paint Red r')
+    else
+      B l' a r'
+  )"
+
+
+text \<open>
+  \subsection*{Warmup}
+
+  Show that the left and right subtree of a balanced tree are, again, balanced
+\<close>
+
+lemma balanced_subt: "balanced (Node c l a r) \<Longrightarrow> balanced l \<and> balanced r"
+  unfolding balanced_def by auto
+
+
+text \<open>Show the following alternative characterization of balanced:\<close>
+
+lemma aux1:"height t \<ge> min_height t"
+  apply(induction t)
+  by auto
+
+lemma balanced_alt:
+  "balanced t \<longleftrightarrow> height t = min_height t \<or> height t = min_height t + 1"
+  text \<open>Hint: Auxiliary lemma relating @{term \<open>height t\<close>} and @{term \<open>min_height t\<close>}\<close>
+  unfolding balanced_def
+  by (metis One_nat_def add_diff_cancel_left' aux1 cancel_comm_monoid_add_class.diff_cancel le_Suc_eq le_add_diff_inverse le_zero_eq order_refl)
+
+text \<open>
+  \subsection*{The Easy Parts}
+
+  Show that \<open>mk_rbt\<close> does not change the inorder-traversal
+\<close>
+lemma mk_rbt_inorder: "inorder (mk_rbt t) = inorder t"
+  apply(induction t)
+   apply(auto)
+  by (smt inorder.simps(2) inorder_paint)
+
+text \<open>Show that the color of the root node is always black\<close>
+lemma mk_rbt_color: "color (mk_rbt t) = Black"
+  apply(induction t)
+   apply(auto)
+  by (smt RBT_Set.color.simps(2))
+
+text \<open>
+  \subsection*{Medium Complex Parts}
+
+  Show that the black-height of the returned tree is the minimum height of the argument tree
+\<close>
+
+
+
+lemma mk_rbt_bheight: "balanced t \<Longrightarrow> bheight (mk_rbt t) = min_height t"
+text \<open>Hint: Use Isar to have better control when to unfold with @{thm [source] balanced_alt},
+  and when to use @{thm [source] balanced_subt} (e.g. to discharge the premises of the IH)
+\<close>
+proof(induction t)
+  case Leaf
+  then show ?case by auto
+next
+  case (Node x1 t1 x3 t2)
+  note IH = Node.IH
+  have "min_height t1 = min_height t2 \<or> min_height t1 < min_height t2 \<or> min_height t1 > min_height t2" (is "?C1 \<or> ?C2 \<or> ?C3")
+    by auto
+  moreover
+  {
+    assume ?C1
+    have ?case using IH Node.prems \<open>?C1\<close>
+      apply(cases "min_height t1")
+       apply(auto)
+       apply (meson balanced_subt)
+      by (meson balanced_subt)
+    }
+    moreover
+    {
+      assume ?C2
+      have ?case using IH Node.prems \<open>?C2\<close>
+        apply(cases "min_height t1")
+         apply(auto)
+         apply (meson balanced_subt)
+        by (metis balanced_subt min.strict_order_iff)
+    }
+    moreover
+    {
+      assume ?C3
+      then have h0:"min_height (Node x1 t1 x3 t2) = min_height t2 + 1" using IH Node.prems by force
+      then have h1:"min_height t2 = 0 \<Longrightarrow> bheight (paint Red (mk_rbt t1)) = 0" using IH Node.prems
+        by (metis (no_types, lifting) One_nat_def Suc_eq_plus1 Suc_leI \<open>min_height t2 < min_height t1\<close> add_diff_cancel_right' aux1 balanced_def bheight_paint_Red height.simps(2) le_trans max.commute max_def mk_rbt_color)
+      then have h2: "min_height t1 > min_height t2 \<Longrightarrow> min_height t1 = Suc (min_height t2)" using IH Node.prems
+        by (smt Suc_eq_plus1 Suc_leI Suc_mono balanced_alt balanced_subt h0 height.simps(2) less_Suc_eq max.commute max_def not_le)
+      then have h3: " min_height t1 > min_height t2 \<Longrightarrow> bheight (paint Red (mk_rbt t1)) = min_height t2" using IH Node.prems
+        apply(cases "min_height t1")
+         apply(auto)
+        by (metis Suc_eq_plus1 add_diff_cancel_right' balanced_subt bheight_paint_Red mk_rbt_color)
+        
+      then have ?case using IH Node.prems \<open>?C3\<close> 
+        apply(cases "min_height t2")
+        by (auto)
+        
+      }
+      ultimately show ?case by blast
+qed
+
+text \<open>
+  Show that the returned tree satisfies the height invariant.
+\<close>
+
+lemma mk_rbt_invh: "balanced t \<Longrightarrow> invh (mk_rbt t)"
+  apply(induction t rule:mk_rbt.induct)
+   apply(simp add: balanced_alt mk_rbt_color mk_rbt_inorder mk_rbt_bheight)
+  apply(simp split:if_splits)
+  by (smt Suc_eq_plus1 Suc_le_mono add_diff_cancel_right' antisym_conv balanced_alt balanced_subt bheight_paint_Red height.simps(2) invh.simps(2) le_Suc_eq le_simps(3) max_def min_def invh_paint min_height.simps(2) mk_rbt_bheight mk_rbt_color)
+
+
+text \<open>
+  \subsection*{The Hard Part (3 Bonus Points)}
+
+  For {\bf three bonus points}, show that the returned tree satisfies the color invariant.
+
+  Warning: This requires careful case splitting, via a clever combination of
+    automation and manual proof (Isar, aux-lemmas), in order to deal with the
+    multiple cases without a combinatorial explosion of the proofs.
+\<close>
+
+lemma mk_rbt_invc: "balanced t \<Longrightarrow> invc (mk_rbt t)"
+proof(induction t)
+case Leaf
+then show ?case by auto
+next
+  case (Node x1 t1 x3 t2)
+  note IH = Node.IH
+  have "min_height t1 = min_height t2 \<or> min_height t1 < min_height t2 \<or> min_height t1 > min_height t2" (is "?C1 \<or> ?C2 \<or> ?C3")
+    by auto
+  moreover
+  {
+    assume ?C1
+    have ?case using IH Node.prems \<open>?C1\<close>
+      apply(cases "min_height t1")
+       apply(auto)
+         apply (meson balanced_subt)
+        apply (meson balanced_subt)
+       apply (meson balanced_subt)
+      by (meson balanced_subt)
+  }
+  moreover
+  {
+    assume ?C2
+    then have h0:"min_height (Node x1 t1 x3 t2) = min_height t1 + 1" using IH Node.prems by force
+    then have h1: "min_height t1 < min_height t2 \<Longrightarrow> min_height t2 = Suc (min_height t1)" using IH Node.prems
+      by (smt Suc_eq_plus1 Suc_leI Suc_mono balanced_alt balanced_subt h0 height.simps(2) less_Suc_eq max.commute max_def not_le)
+    then have h2:"invc (paint Red (mk_rbt t2))" using IH Node.prems sorry
+      then have ?case using IH Node.prems \<open>?C2\<close> 
+      apply(cases "min_height t1")
+        apply(auto)
+           apply (smt balanced_subt)
+          apply (simp add: h2)
+        by (meson balanced_subt)
+    }
+
+qed
+
+
+(* Now you can combine everything, to show that you are, indeed, generating an RBT *)
+theorem mk_rbt_is_rbt: "balanced t \<Longrightarrow> rbt (mk_rbt t)"
+  using mk_rbt_invh mk_rbt_invc mk_rbt_color unfolding rbt_def by auto
+
+
+
+text \<open>\NumHomework{Linear-Time Repainting}{15.~6.~2018}
+
+  Write a linear-time version of \<open>mk_rbt\<close>, and show that it behaves like
+  \<open>mk_rbt\<close>.
+
+  Idea: Compute the min-height during the same recursion as you build
+    the tree.
+
+  Note: No formal complexity proof required.
+\<close>
+
+fun mk_rbt' :: "('a,unit) tree \<Rightarrow> 'a rbt \<times> nat" -- \<open>Returns the RBT and the min-height of the argument\<close>
+where
+  "mk_rbt' Leaf = (Leaf, 0)"
+| "mk_rbt' (Node _ l a r) = (let
+    (l',lx)=mk_rbt' l;
+    (r',rx)=mk_rbt' r
+  in
+    if lx > rx then
+      (B (paint Red l') a r', Suc(rx))
+    else if lx < rx then
+      (B l' a (paint Red r'), Suc(lx))
+    else
+      (B l' a r', Suc(lx))
+  )" 
+
+lemma mk_rbt'_refine_aux: "mk_rbt' t = (mk_rbt t, min_height t)"
+  apply(induction t)
+  apply(auto)
+  done
+
+
+lemma mk_rbt'_refine: "fst (mk_rbt' t) = mk_rbt t"
+  apply(induction t)
+  by(auto simp:mk_rbt'_refine_aux)
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/09/hw09tmpl.thy~ b/09/hw09tmpl.thy~
new file mode 100644
index 0000000..de121b0
--- /dev/null
+++ b/09/hw09tmpl.thy~
@@ -0,0 +1,192 @@
+(*<*)
+theory hw09tmpl
+  imports Main "HOL-Data_Structures.RBT_Set"
+begin
+(*>*)
+
+text \<open>\NumHomework{Balanced Tree to RBT}{15.~6.~2018}
+
+  A tree is balanced, if its minimum height and its height differ by at most 1.
+\<close>
+
+fun min_height :: "('a,'b) tree \<Rightarrow> nat" where
+"min_height Leaf = 0" |
+"min_height (Node _ l _ r) = min (min_height l) (min_height r) + 1"
+
+definition "balanced t \<equiv> height t - min_height t \<le> 1"
+
+text \<open>The following function paints a balanced tree to form a valid red-black tree
+  with the same structure. The task of this homework is to prove this!
+\<close>
+
+fun mk_rbt :: "('a,unit) tree \<Rightarrow> 'a rbt" where
+  "mk_rbt Leaf = Leaf"
+| "mk_rbt (Node _ l a r) = (let
+    l'=mk_rbt l;
+    r'=mk_rbt r
+  in
+    if min_height l > min_height r then
+      B (paint Red l') a r'
+    else if min_height l < min_height r then
+      B l' a (paint Red r')
+    else
+      B l' a r'
+  )"
+
+
+text \<open>
+  \subsection*{Warmup}
+
+  Show that the left and right subtree of a balanced tree are, again, balanced
+\<close>
+
+lemma balanced_subt: "balanced (Node c l a r) \<Longrightarrow> balanced l \<and> balanced r"
+  unfolding balanced_def by auto
+
+
+text \<open>Show the following alternative characterization of balanced:\<close>
+
+lemma aux1:"height t \<ge> min_height t"
+  apply(induction t)
+  by auto
+
+lemma balanced_alt:
+  "balanced t \<longleftrightarrow> height t = min_height t \<or> height t = min_height t + 1"
+  text \<open>Hint: Auxiliary lemma relating @{term \<open>height t\<close>} and @{term \<open>min_height t\<close>}\<close>
+  unfolding balanced_def
+  by (metis One_nat_def add_diff_cancel_left' aux1 cancel_comm_monoid_add_class.diff_cancel le_Suc_eq le_add_diff_inverse le_zero_eq order_refl)
+
+text \<open>
+  \subsection*{The Easy Parts}
+
+  Show that \<open>mk_rbt\<close> does not change the inorder-traversal
+\<close>
+lemma mk_rbt_inorder: "inorder (mk_rbt t) = inorder t"
+  apply(induction t)
+   apply(auto)
+  by (smt inorder.simps(2) inorder_paint)
+
+text \<open>Show that the color of the root node is always black\<close>
+lemma mk_rbt_color: "color (mk_rbt t) = Black"
+  apply(induction t)
+   apply(auto)
+  by (smt RBT_Set.color.simps(2))
+
+text \<open>
+  \subsection*{Medium Complex Parts}
+
+  Show that the black-height of the returned tree is the minimum height of the argument tree
+\<close>
+
+
+
+lemma mk_rbt_bheight: "balanced t \<Longrightarrow> bheight (mk_rbt t) = min_height t"
+text \<open>Hint: Use Isar to have better control when to unfold with @{thm [source] balanced_alt},
+  and when to use @{thm [source] balanced_subt} (e.g. to discharge the premises of the IH)
+\<close>
+proof(induction t)
+  case Leaf
+  then show ?case by auto
+next
+  case (Node x1 t1 x3 t2)
+  note IH = Node.IH
+  have "min_height t1 = min_height t2 \<or> min_height t1 < min_height t2 \<or> min_height t1 > min_height t2" (is "?C1 \<or> ?C2 \<or> ?C3")
+    by auto
+  moreover
+  {
+    assume ?C1
+    have ?case using IH Node.prems \<open>?C1\<close>
+      apply(cases "min_height t1")
+       apply(auto)
+       apply (meson balanced_subt)
+      by (meson balanced_subt)
+    }
+    moreover
+    {
+      assume ?C2
+      have ?case using IH Node.prems \<open>?C2\<close>
+        apply(cases "min_height t1")
+         apply(auto)
+         apply (meson balanced_subt)
+        by (metis balanced_subt min.strict_order_iff)
+    }
+    moreover
+    {
+      assume ?C3
+      have ?case using IH Node.prems \<open>?C3\<close>
+        apply(cases "min_height t2")
+         apply(auto)
+        
+  then show ?case 
+qed
+
+text \<open>
+  Show that the returned tree satisfies the height invariant.
+\<close>
+
+lemma mk_rbt_invh: "balanced t \<Longrightarrow> invh (mk_rbt t)"
+  unfolding balanced_def
+  apply(induction t) sorry
+
+
+text \<open>
+  \subsection*{The Hard Part (3 Bonus Points)}
+
+  For {\bf three bonus points}, show that the returned tree satisfies the color invariant.
+
+  Warning: This requires careful case splitting, via a clever combination of
+    automation and manual proof (Isar, aux-lemmas), in order to deal with the
+    multiple cases without a combinatorial explosion of the proofs.
+\<close>
+
+lemma mk_rbt_invc: "balanced t \<Longrightarrow> invc (mk_rbt t)"
+  sorry
+
+
+(* Now you can combine everything, to show that you are, indeed, generating an RBT *)
+theorem mk_rbt_is_rbt: "balanced t \<Longrightarrow> rbt (mk_rbt t)"
+  using mk_rbt_invh mk_rbt_invc mk_rbt_color unfolding rbt_def by auto
+
+
+
+text \<open>\NumHomework{Linear-Time Repainting}{15.~6.~2018}
+
+  Write a linear-time version of \<open>mk_rbt\<close>, and show that it behaves like
+  \<open>mk_rbt\<close>.
+
+  Idea: Compute the min-height during the same recursion as you build
+    the tree.
+
+  Note: No formal complexity proof required.
+\<close>
+
+fun mk_rbt' :: "('a,unit) tree \<Rightarrow> 'a rbt \<times> nat" -- \<open>Returns the RBT and the min-height of the argument\<close>
+where
+  "mk_rbt' Leaf = (Leaf, 0)"
+| "mk_rbt' (Node _ l a r) = (let
+    (l',lx)=mk_rbt' l;
+    (r',rx)=mk_rbt' r
+  in
+    if lx > rx then
+      (B (paint Red l') a r', Suc(rx))
+    else if lx < rx then
+      (B l' a (paint Red r'), Suc(lx))
+    else
+      (B l' a r', Suc(lx))
+  )" 
+
+lemma mk_rbt'_refine_aux: "mk_rbt' t = (mk_rbt t, min_height t)"
+  apply(induction t)
+  apply(auto)
+  done
+
+
+lemma mk_rbt'_refine: "fst (mk_rbt' t) = mk_rbt t"
+  apply(induction t)
+  by(auto simp:mk_rbt'_refine_aux)
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/10/Trie1.thy b/10/Trie1.thy
new file mode 100644
index 0000000..c179f23
--- /dev/null
+++ b/10/Trie1.thy
@@ -0,0 +1,168 @@
+(* Author: Tobias Nipkow *)
+
+section "Trie1"
+
+theory Trie1
+imports Main
+begin
+
+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
diff --git a/10/ex10.pdf b/10/ex10.pdf
new file mode 100644
index 0000000..aa869af
Binary files /dev/null and b/10/ex10.pdf differ
diff --git a/10/hw10.thy b/10/hw10.thy
new file mode 100644
index 0000000..0c09385
--- /dev/null
+++ b/10/hw10.thy
@@ -0,0 +1,165 @@
+
+theory hw10
+imports Main
+begin
+
+datatype trie = LeafF | LeafT | Node "trie * trie"
+
+fun is_trie :: "nat \<Rightarrow> trie \<Rightarrow> bool"
+  where
+  "is_trie 0 (Node(x,y)) \<longleftrightarrow> False"
+| "is_trie 0 _ \<longleftrightarrow> True"
+| "is_trie (Suc n) LeafF \<longleftrightarrow> True"
+| "is_trie (Suc n) LeafT \<longleftrightarrow> False"
+| "is_trie (Suc n) (Node (x,y)) \<longleftrightarrow> is_trie n x \<and> is_trie n y"
+
+text \<open>Hint: The following should evaluate to true!\<close>
+value "is_trie 42 LeafF"
+value "is_trie 2 (Node (LeafF,Node (LeafT,LeafF)))"
+text \<open>Whereas these should be false\<close>
+value "is_trie 42 LeafT" -- \<open>Wrong key length\<close>
+value "is_trie 2 (Node (LeafT,Node (LeafT,LeafF)))" -- \<open>Wrong key length\<close>
+value "is_trie 1 (Node (LeafT,Node (LeafF,LeafF)))" -- \<open>Superfluous node\<close>
+
+fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool"
+  where
+  "isin (Node (x,y)) [] = False"
+| "isin LeafT [] = True"
+| "isin LeafF _ = False"
+| "isin (Node (x,y)) (b#bx) = (if b then isin y bx else isin x bx)"
+| "isin LeafT (b#bx) = False"
+
+value "isin (Node (LeafF,Node (LeafT,LeafF))) [True, False]"
+value "isin LeafT []"
+value "isin LeafF []"
+
+fun ins :: "bool list \<Rightarrow> trie \<Rightarrow> trie"
+  where
+  "ins [] _ = LeafT"
+| "ins (b#bx) LeafF = (if b then (Node (LeafF, ins bx LeafF)) else (Node ((ins bx LeafF), LeafF)))"
+| "ins (b#bx) (Node (x,y)) = (if b then (Node (x, ins bx y)) else (Node ((ins bx x),y)))"
+| "ins _ x = x"
+
+value "ins [] LeafF"
+value "ins [] LeafT"
+value "ins [] (Node(LeafF,LeafT))"
+value "ins [True] (Node(LeafF,LeafT))"
+value "ins [False] (Node(LeafF,LeafT))"
+value "ins [False, False] (Node (LeafF,Node (LeafF,LeafT)))"
+value "ins [False] LeafF"
+value "ins [True,True,True] (Node (LeafF,Node (LeafT,LeafF)))"
+
+
+lemma aux1: "\<And>b bx x y bs.
+       (\<And>bs n. is_trie n y \<Longrightarrow> length bx = n \<Longrightarrow> isin (ins bx y) bs = (bx = bs \<or> isin y bs)) \<Longrightarrow>
+       (\<And>bs n. False \<Longrightarrow> is_trie n x \<Longrightarrow> length bx = n \<Longrightarrow> isin (ins bx x) bs = (bx = bs \<or> isin x bs)) \<Longrightarrow>
+       b \<Longrightarrow> isin (Node (x, ins bx y)) bs \<Longrightarrow>
+             \<not> isin (Node (x, y)) bs \<Longrightarrow> is_trie (length bx) x \<Longrightarrow> is_trie (length bx) y \<Longrightarrow> True # bx = bs"
+ proof -
+fix b :: bool and bx :: "bool list" and x :: trie and y :: trie and bsa :: "bool list"
+assume a1: "isin (Node (x, ins bx y)) bsa"
+assume a2: "\<not> isin (Node (x, y)) bsa"
+assume a3: "\<And>bs n. \<lbrakk>is_trie n y; length bx = n\<rbrakk> \<Longrightarrow> isin (ins bx y) bs = (bx = bs \<or> isin y bs)"
+assume a4: "is_trie (length bx) y"
+have "bsa \<noteq> []"
+using a1 by force
+then show "True # bx = bsa"
+  using a4 a3 a2 a1 by (metis (full_types) isin.simps(4) list.exhaust)
+qed
+
+
+
+lemma isin_ins1:
+  assumes "is_trie n t" and "length as = n"
+  shows "isin (ins as t) bs = (as = bs \<or> isin t bs)"
+proof -
+  show ?thesis using assms
+    apply (induction as t arbitrary: bs n rule: ins.induct)
+       apply (auto split:if_splits)
+    using isin.elims(2) apply blast
+    using is_trie.simps(1) isin.elims(2) apply blast
+           apply (metis (full_types) is_trie.simps(2) is_trie.simps(4) isin.simps(1) isin.simps(3) isin.simps(4) length_0_conv length_Cons list.exhaust)
+    using is_trie.elims(3) apply blast
+         apply (smt Suc_length_conv ins.simps(2) is_trie.simps(2) is_trie.simps(4) isin.simps(1) isin.simps(3) isin.simps(4) length_0_conv length_Cons list.exhaust list.inject neq_Nil_conv)
+    using is_trie.elims(3) apply blast
+    
+    using aux1 apply metis
+      apply (metis isin.elims(2) isin.simps(4) trie.distinct(5))
+     apply (smt isin.elims(2) isin.simps(4) trie.distinct(5))
+    by (metis isin.elims(2) isin.simps(4) trie.distinct(5))
+qed
+
+lemma isin_ins2:
+  assumes "is_trie n t" and "length as = n"
+  shows "is_trie n (ins as t)"
+proof -
+  show ?thesis using assms
+   apply (induction as t arbitrary: n rule: ins.induct)
+       apply (auto split:if_splits)
+    using is_trie.elims(3) apply blast
+    using is_trie.elims(3) apply blast
+    using is_trie.elims(3) apply blast
+    using is_trie.elims(3) by blast
+qed
+
+lemma isin_ins:
+  assumes "is_trie n t" and "length as = n"
+  shows "isin (ins as t) bs = (as = bs \<or> isin t bs)"
+    and "is_trie n (ins as t)"
+  using assms(1) assms(2) isin_ins1 apply auto[1]
+  by (simp add: assms(1) assms(2) isin_ins2)
+
+fun node :: "trie \<times> trie \<Rightarrow> trie" where
+  "node (x,y) = (if (x = LeafF \<and> y = LeafF) then LeafF else (Node(x,y)))"
+
+
+fun delete2 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+  "delete2 [] _ = LeafF"
+| "delete2 (b#bx) LeafF = LeafF"
+| "delete2 (b#bx) (Node (x,y)) = (if b then (node (x, delete2 bx y)) else (node ((delete2 bx x),y)))"
+| "delete2 _ x = x"
+
+lemma delaux1:
+  assumes "is_trie n t" and "length as = n"
+  shows "isin (delete2 as t) bs = (as\<noteq>bs \<and> isin t bs)"
+proof -
+  show ?thesis using assms
+   apply (induction as t arbitrary: bs n rule: delete2.induct)
+       apply (auto split!:if_splits)
+              apply (metis gen_length_code(1) ins.simps(1) is_trie.simps(2) isin.simps(3) isin_ins1 length_code)
+             apply (metis isin.elims(2) isin.simps(4) trie.distinct(5))
+            apply (metis isin.elims(2) isin.simps(4) trie.distinct(5))
+           apply (metis (full_types) isin.simps(1) isin.simps(3) isin.simps(4) list.exhaust)
+          apply (smt isin.elims(2) isin.simps(4) trie.simps(7))
+         apply (smt isin.elims(2) isin.simps(4) trie.simps(7))
+        apply (metis isin.elims(2) isin.simps(4) trie.distinct(5))
+       apply (metis isin.elims(2) isin.simps(4) trie.distinct(5))
+      apply (metis (full_types) isin.simps(1) isin.simps(3) isin.simps(4) list.exhaust)
+     apply (smt isin.elims(2) isin.simps(4) trie.simps(7))
+    by (smt isin.elims(2) isin.simps(4) trie.simps(7))
+qed
+
+lemma delaux2:
+  assumes "is_trie n t"
+  shows"(is_trie n (delete2 as t))"
+proof -
+ show ?thesis using assms
+   apply (induction as t arbitrary: n rule: delete2.induct)
+      apply (auto split!:if_splits)
+   using is_trie.elims(3) apply blast
+   using is_trie.elims(3) apply blast
+       apply (metis is_trie.simps(1) is_trie.simps(6) old.nat.exhaust)
+      apply (metis is_trie.simps(1) is_trie.simps(6) not0_implies_Suc)
+     apply (metis is_trie.elims(2) is_trie.simps(4) trie.simps(7))
+    apply (metis is_trie.simps(1) is_trie.simps(6) old.nat.exhaust)
+   by (metis is_trie.simps(1) is_trie.simps(6) not0_implies_Suc)
+qed
+  
+lemma
+  assumes "is_trie n t" and "length as = n"
+  shows "isin (delete2 as t) bs = (as\<noteq>bs \<and> isin t bs)"
+    and "(is_trie n (delete2 as t))"
+  using assms(1) assms(2) delaux1 apply blast
+  by (simp add: assms(1) delaux2)
+
+end
\ No newline at end of file
diff --git a/10/hw10_1_tmpl.thy b/10/hw10_1_tmpl.thy
new file mode 100644
index 0000000..bf61fcd
--- /dev/null
+++ b/10/hw10_1_tmpl.thy
@@ -0,0 +1,134 @@
+(*<*)
+theory hw10_1_tmpl
+imports Main
+begin
+(*>*)
+
+
+text \<open>\NumHomework{Tries with Same-Length Keys}{22.~6.~2018}
+
+  Consider the following trie datatype:
+\<close>
+
+datatype trie = LeafF | LeafT | Node "trie * trie"
+
+text \<open>It is meant to store keys of the same length only.
+  Thus, the @{const Node} constructor stores inner nodes, and there are two
+  types of leaves, @{const LeafF} if this path is not in the set,
+  and @{const LeafT} if it is in the set.
+
+  Define an invariant \<open>is_trie N t\<close> that states that all keys in \<open>t\<close>
+  have length \<open>N\<close>, and that there are no superfluous nodes, i.e.,
+  no nodes of the form @{term \<open>Node (LeafF, LeafF)\<close>}.
+\<close>
+
+fun is_trie :: "nat \<Rightarrow> trie \<Rightarrow> bool"
+where
+  "is_trie 0 (Node (x,y)) \<longleftrightarrow> False"
+| "is_trie 0 _ \<longleftrightarrow> True"
+| "is_trie _ (Node (LeafF, LeafF)) \<longleftrightarrow> False"
+| "is_trie (Suc n) LeafT \<longleftrightarrow> False"
+| "is_trie (Suc n) LeafF \<longleftrightarrow> True"
+(*| "is_trie (Suc 0) (Node (x,y)) \<longleftrightarrow> ((x = LeafF) \<or> (x = LeafT)) \<and> ((y = LeafF) \<or> (y = LeafT))"*)
+| "is_trie (Suc n) (Node (x,y)) \<longleftrightarrow> is_trie n x \<and> is_trie n y"
+
+text \<open>Hint: The following should evaluate to true!\<close>
+value "is_trie 42 LeafF"
+value "is_trie 2 (Node (LeafF,Node (LeafT,LeafF)))"
+text \<open>Whereas these should be false\<close>
+value "is_trie 42 LeafT" -- \<open>Wrong key length\<close>
+value "is_trie 2 (Node (LeafT,Node (LeafT,LeafF)))" -- \<open>Wrong key length\<close>
+value "is_trie 1 (Node (LeafT,Node (LeafF,LeafF)))" -- \<open>Superfluous node\<close>
+
+value "is_trie 1 (Node (LeafT,LeafF))"
+
+
+text \<open>Define membership, insert, and delete functions, and prove them correct! \<close>
+
+fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool"
+  where
+  "isin (Node (x, y)) (b#[]) = (if b then (x = LeafT) else (y = LeafT))"
+| "isin (Node (x, y)) (b#bs) = (if b then (isin x bs) else (isin y bs))"
+| "isin LeafT [] = True"
+| "isin _ _ = False"
+
+value "isin (Node (LeafF,Node (LeafT,LeafF))) [False, True]"
+
+fun ins :: "bool list \<Rightarrow> trie \<Rightarrow> trie"
+  where
+  "ins (b#[]) LeafF = (if b then (Node (LeafT, LeafF)) else (Node(LeafF, LeafT)))"
+| "ins (b#[]) LeafT = (if b then (Node (LeafT, LeafF)) else (Node(LeafF, LeafT)))"
+| "ins (b#[]) (Node(x,y)) = (if b then (Node (LeafT, y)) else (Node(x, LeafT)))"
+| "ins [] x = x"
+| "ins (b#bs) (Node(x,y)) =  (if b then (Node ((ins bs x),y)) else (Node (x, (ins bs y))))"
+| "ins (b#bs) LeafF = (if b then (Node ((ins bs LeafF),LeafF)) else (Node (LeafF, (ins bs LeafF))))"
+| "ins (b#bs) LeafT = (if b then (Node ((ins bs LeafT),LeafF)) else (Node (LeafF, (ins bs LeafT))))"
+
+(*fun ins :: "bool list \<Rightarrow> trie \<Rightarrow> trie"
+  where
+  "ins [] x = LeafT"
+| "ins (b#bs) (Node(x,y)) =  (if b then (Node ((ins bs x),y)) else (Node (x, (ins bs y))))"
+| "ins (b#bs) x = (if b then (Node ((ins bs x),LeafF)) else (Node (LeafF, (ins bs x))))"*)
+
+value "ins [True, False] (Node (LeafF,Node (LeafT,LeafF)))"
+value "ins [False] LeafF"
+value "ins [True,True,True] (Node (LeafF,Node (LeafT,LeafF)))"
+
+
+
+lemma isin_ins1:
+  assumes "is_trie n t" and "length as = n"
+  shows "isin (ins as t) bs = (as = bs \<or> isin t bs)"
+  apply (induction as t arbitrary: bs n rule: ins.induct)
+  
+  
+  
+  
+  
+
+
+lemma isin_ins2:
+  assumes "is_trie n t" and "length as = n"
+  shows "is_trie n (ins as t)"
+proof(induction as)
+  case Nil
+then show ?case
+  by (simp add: assms(1))
+next
+case (Cons a as)
+  then show ?case
+    by (metis One_nat_def ins.simps(2) ins.simps(3) is_trie.simps(2) isin.simps(4) isin_ins1 le_numeral_extra(4) length_Cons list.size(3) not_less_eq_eq not_one_le_zero order_antisym_conv zero_induct)
+qed
+
+
+
+
+lemma isin_ins:
+  assumes "is_trie n t" and "length as = n"
+  shows "isin (ins as t) bs = (as = bs \<or> isin t bs)"
+    and "is_trie n (ins as t)"
+  using assms(1) assms(2) isin_ins1 apply auto[1]
+
+
+fun delete2 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+  "delete2 _ _ = undefined"
+
+lemma
+  assumes "is_trie n t"
+  shows "isin (delete2 as t) bs = (as\<noteq>bs \<and> isin t bs)"
+    and "(is_trie n (delete2 as t))"
+  oops
+
+text \<open>Hints:
+  \<^item> Like in the \<open>delete2\<close> function for standard tries, you may want to define
+    a "smart-constructor" \<open>node :: trie \<times> trie \<Rightarrow> trie\<close> for nodes,
+    that constructs a node and handles the case that both successors are \<open>LeafF\<close>.
+  \<^item> Consider proving auxiliary lemmas about the smart-constructor, instead of
+    always unfolding it with the simplifier.
+\<close>
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/10/hw10_1_tmpl.thy~ b/10/hw10_1_tmpl.thy~
new file mode 100644
index 0000000..d21ae20
--- /dev/null
+++ b/10/hw10_1_tmpl.thy~
@@ -0,0 +1,144 @@
+(*<*)
+theory hw10_1_tmpl
+imports Main
+begin
+(*>*)
+
+
+text \<open>\NumHomework{Tries with Same-Length Keys}{22.~6.~2018}
+
+  Consider the following trie datatype:
+\<close>
+
+datatype trie = LeafF | LeafT | Node "trie * trie"
+
+text \<open>It is meant to store keys of the same length only.
+  Thus, the @{const Node} constructor stores inner nodes, and there are two
+  types of leaves, @{const LeafF} if this path is not in the set,
+  and @{const LeafT} if it is in the set.
+
+  Define an invariant \<open>is_trie N t\<close> that states that all keys in \<open>t\<close>
+  have length \<open>N\<close>, and that there are no superfluous nodes, i.e.,
+  no nodes of the form @{term \<open>Node (LeafF, LeafF)\<close>}.
+\<close>
+
+fun is_trie :: "nat \<Rightarrow> trie \<Rightarrow> bool"
+where
+  "is_trie 0 LeafT \<longleftrightarrow> True"
+| "is_trie _ LeafF \<longleftrightarrow> True"
+| "is_trie _ (Node (LeafF, LeafF)) \<longleftrightarrow> False"
+| "is_trie (Suc n) LeafT \<longleftrightarrow> False"
+| "is_trie 0 (Node (x,y)) \<longleftrightarrow> False"
+| "is_trie (Suc n) (Node (x,y)) \<longleftrightarrow> is_trie n x \<and> is_trie n y"
+
+text \<open>Hint: The following should evaluate to true!\<close>
+value "is_trie 42 LeafF"
+value "is_trie 2 (Node (LeafF,Node (LeafT,LeafF)))"
+text \<open>Whereas these should be false\<close>
+value "is_trie 42 LeafT" -- \<open>Wrong key length\<close>
+value "is_trie 2 (Node (LeafT,Node (LeafT,LeafF)))" -- \<open>Wrong key length\<close>
+value "is_trie 1 (Node (LeafT,Node (LeafF,LeafF)))" -- \<open>Superfluous node\<close>
+
+value "is_trie 1 (Node (LeafT,LeafF))"
+
+
+text \<open>Define membership, insert, and delete functions, and prove them correct! \<close>
+
+fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool"
+  where
+  "isin (Node (x, y)) (b#[]) = (if b then (x = LeafT) else (y = LeafT))"
+| "isin (Node (x, y)) (b#bs) = (if b then (isin x bs) else (isin y bs))"
+| "isin _ _ = False"
+
+value "isin (Node (LeafF,Node (LeafT,LeafF))) [False, True]"
+
+fun ins' :: "bool list \<Rightarrow> trie \<Rightarrow> trie"
+  where
+  "ins' (b#[]) LeafF = (if b then (Node (LeafT, LeafF)) else (Node(LeafF, LeafT)))"
+| "ins' (b#[]) LeafT = (if b then (Node (LeafT, LeafF)) else (Node(LeafF, LeafT)))"
+| "ins' (b#[]) (Node(x,y)) = (if b then (Node (LeafT, y)) else (Node(x, LeafT)))"
+| "ins' [] x = x"
+| "ins' (b#bs) (Node(x,y)) =  (if b then (Node ((ins' bs x),y)) else (Node (x, (ins' bs y))))"
+| "ins' (b#bs) LeafF = (if b then (Node ((ins' bs LeafF),LeafF)) else (Node (LeafF, (ins' bs LeafF))))"
+| "ins' (b#bs) LeafT = (if b then (Node ((ins' bs LeafT),LeafF)) else (Node (LeafF, (ins' bs LeafT))))"
+
+fun ins :: "bool list \<Rightarrow> trie \<Rightarrow> trie"
+  where
+  "ins [] x = LeafT"
+| "ins (b#bs) (Node(x,y)) =  (if b then (Node ((ins bs x),y)) else (Node (x, (ins bs y))))"
+| "ins (b#bs) x = (if b then (Node ((ins bs x),LeafF)) else (Node (LeafF, (ins bs x))))"
+
+value "ins [True, False] (Node (LeafF,Node (LeafT,LeafF)))"
+value "ins [False] LeafF"
+value "ins [True,True,True] (Node (LeafF,Node (LeafT,LeafF)))"
+
+lemma isin_ins1:
+  assumes "is_trie n t" and "length as = n"
+  shows "isin (ins as t) bs = (as = bs \<or> isin t bs)"
+proof (induction as t arbitrary: bs n rule: ins.induct)
+case (1 x)
+  then show ?case
+    apply(auto)
+    
+next
+case (2 b bs x y)
+then show ?case sorry
+next
+case ("3_1" b bs)
+  then show ?case sorry
+next
+  case ("3_2" b bs)
+  then show ?case sorry
+qed
+
+
+
+  
+  
+
+
+lemma isin_ins2:
+  assumes "is_trie n t" and "length as = n"
+  shows "is_trie n (ins as t)"
+proof(induction as)
+  case Nil
+then show ?case
+  by (simp add: assms(1))
+next
+case (Cons a as)
+  then show ?case
+    by (metis One_nat_def ins.simps(2) ins.simps(3) is_trie.simps(2) isin.simps(4) isin_ins1 le_numeral_extra(4) length_Cons list.size(3) not_less_eq_eq not_one_le_zero order_antisym_conv zero_induct)
+qed
+
+
+
+
+lemma isin_ins:
+  assumes "is_trie n t" and "length as = n"
+  shows "isin (ins as t) bs = (as = bs \<or> isin t bs)"
+    and "is_trie n (ins as t)"
+  using assms(1) assms(2) isin_ins1 apply auto[1]
+
+
+fun delete2 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
+  "delete2 _ _ = undefined"
+
+lemma
+  assumes "is_trie n t"
+  shows "isin (delete2 as t) bs = (as\<noteq>bs \<and> isin t bs)"
+    and "(is_trie n (delete2 as t))"
+  oops
+
+text \<open>Hints:
+  \<^item> Like in the \<open>delete2\<close> function for standard tries, you may want to define
+    a "smart-constructor" \<open>node :: trie \<times> trie \<Rightarrow> trie\<close> for nodes,
+    that constructs a node and handles the case that both successors are \<open>LeafF\<close>.
+  \<^item> Consider proving auxiliary lemmas about the smart-constructor, instead of
+    always unfolding it with the simplifier.
+\<close>
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/10/hw10_2_tmpl.thy b/10/hw10_2_tmpl.thy
new file mode 100644
index 0000000..c077b4d
--- /dev/null
+++ b/10/hw10_2_tmpl.thy
@@ -0,0 +1,54 @@
+(*<*)
+theory hw10_2_tmpl
+imports Trie1 "HOL-Library.List_lexord"
+begin
+(*>*)
+(* Incomplete *)
+
+fun path_trav :: "trie \<Rightarrow> bool list \<Rightarrow> bool list list" where
+  "path_trav Leaf bs = []"
+| "path_trav (Node b (x,y)) bs = (if b then ([bs] @ (path_trav x (bs@[True])) @ (path_trav y (bs@[False])))
+                                    else ( (path_trav x (bs@[True])) @ (path_trav y (bs@[False]))))"
+
+fun enum :: "trie \<Rightarrow> bool list list"
+  where
+    "enum Leaf = []"
+  | "enum t = path_trav t []"
+
+value "enum (Node False ((Node True (Leaf, Leaf)),Leaf))"
+value "path_trav (Node False ((Node True (Leaf, Leaf)),Leaf)) []"
+
+lemma enum_correct1: "set (enum t) = { xs. isin t xs }"
+proof(induction rule: isin.induct)
+  case (1 ks)
+then show ?case by auto
+next
+case (2 b l r ks)
+  then show ?case 
+qed
+  
+  oops
+  
+lemma enum_correct2: "sorted_wrt op< (enum t)"
+  
+    oops
+
+lemma enum_correct:
+    "set (enum t) = { xs. isin t xs }" and "sorted_wrt op< (enum t)"
+    oops
+
+
+
+text \<open>
+  Note that Booleans are ordered by \<open>False < True\<close>, and
+  that we imported @{theory "List_lexord"}, which defines
+  a lexicographic ordering on lists, if the elements are ordered.
+\<close>
+
+value "[True,True,False] < [True,True,True,True]"
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/10/hw10_2_tmpl.thy~ b/10/hw10_2_tmpl.thy~
new file mode 100644
index 0000000..f80abbf
--- /dev/null
+++ b/10/hw10_2_tmpl.thy~
@@ -0,0 +1,35 @@
+(*<*)
+theory hw10_2_tmpl
+imports Trie1 "HOL-Library.List_lexord"
+begin
+(*>*)
+
+text \<open>\NumHomework{Enumeration of Keys in Tries}{22.~6.~2018}
+
+  Write a function that enumerates all keys in a trie, in lexicographic order!
+  Prove it correct.
+\<close>
+
+
+  fun enum :: "trie \<Rightarrow> bool list list"
+  where
+    "enum _ = undefined"
+
+
+  lemma enum_correct:
+    "set (enum t) = { xs. isin t xs }" and "sorted_wrt op< (enum t)"
+    oops
+
+text \<open>
+  Note that Booleans are ordered by \<open>False < True\<close>, and
+  that we imported @{theory "List_lexord"}, which defines
+  a lexicographic ordering on lists, if the elements are ordered.
+\<close>
+
+value "[True,True,False] < [True,True,True,True]"
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/11/ex11_tmpl.thy b/11/ex11_tmpl.thy
new file mode 100644
index 0000000..ec762b0
--- /dev/null
+++ b/11/ex11_tmpl.thy
@@ -0,0 +1,197 @@
+(*<*)
+theory ex11_tmpl
+imports
+    "HOL-Data_Structures.Leftist_Heap"
+begin
+(*>*)
+text {* \ExerciseSheet{11}{22.~6.~2018} *}
+
+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 merge 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 _ _ = undefined"
+
+lemma mset_lh_insert: "mset_tree (lh_insert x t) = mset_tree t + {# x #}"
+  sorry
+
+lemma "heap t \<Longrightarrow> heap (lh_insert x t)"
+  sorry
+
+lemma "ltree t \<Longrightarrow> ltree (lh_insert x t)"
+  sorry
+
+
+fun t_lh_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat"
+  where
+  "t_lh_insert _ _ = undefined"
+
+lemma "t_lh_insert x t \<le> rank t + 1"
+  sorry
+
+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 = PUT_CONSTRUCTORS_HERE
+
+locale Bs_Priority_Queue =
+  orig: Priority_Queue where
+    empty = orig_empty and
+    is_empty = orig_is_empty and
+    insert = orig_insert and
+    get_min = orig_get_min and
+    del_min = orig_del_min and
+    invar = orig_invar and
+    mset = 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 = undefined"
+
+  fun is_empty :: "('a,'s) bs_pq \<Rightarrow> bool"
+    where
+    "is_empty _ \<longleftrightarrow> undefined"
+
+  fun insert :: "'a \<Rightarrow> ('a,'s) bs_pq \<Rightarrow> ('a,'s) bs_pq"
+    where
+    "insert _ _ = undefined"
+
+  fun get_min :: "('a,'s) bs_pq \<Rightarrow> 'a"
+    where
+    "get_min _ = undefined"
+
+  fun del_min :: "('a,'s) bs_pq \<Rightarrow> ('a,'s) bs_pq"
+    where
+    "del_min _ = undefined"
+
+  fun invar :: "('a,'s) bs_pq \<Rightarrow> bool"
+    where
+    "invar _ = undefined"
+
+  fun mset :: "('a,'s) bs_pq \<Rightarrow> 'a multiset"
+    where
+    "mset _ = undefined"
+
+  lemmas [simp] = orig.is_empty orig.mset_get_min orig.mset_del_min
+    orig.mset_insert orig.mset_empty
+    orig.invar_empty orig.invar_insert orig.invar_del_min
+
+  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 sorry
+  next
+    case (2 q) -- \<open>and so on\<close>
+    oops
+
+
+end
+
+text\<open>
+\Homework{Heap}{29.~6.~2018}
+
+A binary tree can be encoded as an array \<open>[a\<^sub>1,...,a\<^sub>n]\<close>, such that
+the parent of node \<open>a\<^sub>i\<close> is node \<open>a\<^sub>(\<^sub>i \<^sub>d\<^sub>i\<^sub>v \<^sub>2\<^sub>)\<close>.
+
+Thus, for a heap, each node is greater than or equal to its parent:
+\<close>
+
+definition parent :: "nat \<Rightarrow> nat" where "parent i \<equiv> (i+1) div 2 - 1"
+definition is_heap :: "'a::linorder list \<Rightarrow> bool"
+  where "is_heap h \<equiv> \<forall>i<length h. h!i \<ge> h!parent i"
+
+
+text \<open>A heap with a single defect at index \<open>j\<close> is characterized as follows:
+  The heap property holds for all elements except \<open>j\<close>,
+  and the children of \<open>j\<close> must also be greater than their grand-parent.
+\<close>
+definition is_heap_except :: "nat \<Rightarrow> 'a::linorder list \<Rightarrow> bool" where
+  "is_heap_except j h \<equiv>
+      (\<forall>i<length h. i\<noteq>j \<longrightarrow> h!i \<ge> h!(parent i))
+    \<and> (\<forall>i<length h. parent i = j \<longrightarrow> h!i \<ge> h!(parent j))"
+
+
+
+text \<open>
+  The function \<open>sift_up\<close> corrects a single defect in a heap by
+  iterated swapping of the defect with its parent, until the heap property
+  is restored.
+\<close>
+
+definition "swap i j h \<equiv> h[i:=h!j, j:=h!i]"
+
+(* Required for termination proof of sift_up *)
+lemma parent_less[simp]: "i\<noteq>0 \<Longrightarrow> parent i < i"
+  by (auto simp: parent_def)
+
+fun sift_up where
+  "sift_up h 0 = h"
+| "sift_up h i = (
+    if h!i \<ge> h!parent i then h
+    else sift_up (swap i (parent i) h) (parent i))"
+
+
+text \<open>Show that @{const sift_up} restores the heap
+  and preserves the multiset of elements in the heap\<close>
+
+lemma sift_up_restore_heap:
+  "is_heap_except j h \<Longrightarrow> j<length h \<Longrightarrow> is_heap (sift_up h j)"
+  sorry
+
+
+lemma sift_up_mset: "j<length h \<Longrightarrow> mset (sift_up h j) = mset h"
+  sorry
+
+text \<open>For \textbf{3 bonus points}, add an empty, insert, and get-min
+  function to the heap implementation, and prove their essential properties.
+\<close>
+
+definition emp :: "'a::linorder list" where "emp \<equiv> undefined"
+definition get_min :: "'a::linorder list \<Rightarrow> 'a" where "get_min h \<equiv> undefined"
+definition ins :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where "ins x h = undefined"
+
+lemma invar_empty: "is_heap emp" sorry
+
+lemma mset_empty: "mset emp = {#}" sorry
+
+lemma mset_get_min: "is_heap h \<Longrightarrow> mset h \<noteq> {#} \<Longrightarrow> get_min h = Min_mset (mset h)" sorry
+
+lemma invar_ins: "is_heap h \<Longrightarrow> is_heap (ins x h)" sorry
+
+lemma mset_ins: "mset (ins x h) = mset h + {#x#}" sorry
+
+
+(*<*)
+end
+(*>*)
diff --git a/12/ex12.pdf b/12/ex12.pdf
new file mode 100644
index 0000000..54c49a6
Binary files /dev/null and b/12/ex12.pdf differ
diff --git a/12/ex12.thy b/12/ex12.thy
new file mode 100644
index 0000000..08da4ea
--- /dev/null
+++ b/12/ex12.thy
@@ -0,0 +1,271 @@
+(*<*)
+theory ex12
+imports
+  Complex_Main
+  "HOL-Library.Multiset"
+begin
+(*>*)
+text {* \ExerciseSheet{12}{29.~6.~2018} *}
+
+text \<open>
+  \Exercise{Sparse Binary Numbers}
+
+  Implement operations carry, inc, and add on sparse binary numbers,
+  analogously to the operations link, ins, and meld on binomial heaps.
+
+  Show that the operations have logarithmic worst-case complexity.
+\<close>
+
+type_synonym rank = nat
+type_synonym snat = "rank list"
+
+abbreviation invar :: "snat \<Rightarrow> bool" where "invar s \<equiv> sorted_wrt op< s"
+definition \<alpha> :: "snat \<Rightarrow> nat" where "\<alpha> s = (\<Sum>i\<leftarrow>s. 2^i)"
+
+lemmas [simp] = sorted_wrt_Cons sorted_wrt_append
+
+
+(*<*)
+lemma \<alpha>_Nil[simp]: "\<alpha> [] = 0"
+  unfolding \<alpha>_def by auto
+
+lemma \<alpha>_Cons[simp]: "\<alpha> (r#rs) = 2^r + \<alpha> rs"
+  unfolding \<alpha>_def by auto
+
+lemma \<alpha>_append[simp]: "\<alpha> (rs\<^sub>1@rs\<^sub>2) = \<alpha> rs\<^sub>1 + \<alpha> rs\<^sub>2"
+  unfolding \<alpha>_def by auto
+
+(*>*)
+
+fun carry :: "rank \<Rightarrow> snat \<Rightarrow> snat"
+(*<*)
+  where
+  "carry r [] = [r]"
+| "carry r (r'#rest) = (if r<r' then r#r'#rest else carry (r+1) rest)"
+(*>*)
+
+lemma carry_invar[simp]:
+(*<*)
+  assumes "invar rs"
+  shows "invar (carry r rs)"
+  using assms
+  apply (induction r rs rule: carry.induct)
+  apply (auto)
+  done
+(*>*)
+
+lemma carry_\<alpha>:
+(*<*)
+  assumes "invar rs"
+  assumes "\<forall>r'\<in>set rs. r\<le>r'"
+  shows "\<alpha> (carry r rs) = 2^r + \<alpha> rs"
+  using assms
+  by (induction r rs rule: carry.induct) force+
+(*>*)
+
+(*<*)
+lemma carry_rank_bound:
+  assumes "r' \<in> set (carry r rs)"
+  assumes "\<forall>r'\<in>set rs. r\<^sub>0 < r'"
+  assumes "r\<^sub>0 < r"
+  shows "r\<^sub>0 < r'"
+  using assms
+  by (induction r rs rule: carry.induct) (auto split: if_splits)
+(*>*)
+
+
+definition inc :: "snat \<Rightarrow> snat"
+(*<*)
+  where "inc rs = carry 0 rs"
+(*>*)
+
+lemma inc_invar[simp]: "invar rs \<Longrightarrow> invar (inc rs)"
+(*<*)
+  unfolding inc_def by auto
+(*>*)
+
+lemma inc_\<alpha>[simp]: "invar rs \<Longrightarrow> \<alpha> (inc rs) = Suc (\<alpha> rs)"
+(*<*)
+  unfolding inc_def by (auto simp: carry_\<alpha>)
+(*>*)
+
+fun add :: "snat \<Rightarrow> snat \<Rightarrow> snat"
+(*<*)
+  where
+  "add rs [] = rs"
+| "add [] rs = rs"
+| "add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = (
+    if r\<^sub>1 < r\<^sub>2 then r\<^sub>1#add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2)
+    else if r\<^sub>2<r\<^sub>1 then r\<^sub>2#add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2
+    else carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2)
+    )"
+(*>*)
+
+(*<*)
+lemma add_rank_bound:
+  assumes "r' \<in> set (add rs\<^sub>1 rs\<^sub>2)"
+  assumes "\<forall>r'\<in>set rs\<^sub>1. r < r'"
+  assumes "\<forall>r'\<in>set rs\<^sub>2. r < r'"
+  shows "r < r'"
+  using assms
+  apply (induction rs\<^sub>1 rs\<^sub>2 arbitrary: r' rule: add.induct)
+  apply (auto split: if_splits simp: carry_rank_bound)
+  done
+(*>*)
+
+lemma add_invar[simp]:
+  assumes "invar rs\<^sub>1"
+  assumes "invar rs\<^sub>2"
+  shows "invar (add rs\<^sub>1 rs\<^sub>2)"
+(*<*)
+  using assms
+proof (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct)
+  case (3 r\<^sub>1 rs\<^sub>1 r\<^sub>2 rs\<^sub>2)
+
+  consider (LT) "r\<^sub>1 < r\<^sub>2"
+         | (GT) "r\<^sub>1 > r\<^sub>2"
+         | (EQ) "r\<^sub>1 = r\<^sub>2"
+    using antisym_conv3 by blast
+  then show ?case proof cases
+    case LT
+    then show ?thesis using 3
+      by (force elim!: add_rank_bound)
+  next
+    case GT
+    then show ?thesis using 3
+      by (force elim!: add_rank_bound)
+  next
+    case [simp]: EQ
+
+    from "3.IH"(3) "3.prems" have [simp]: "invar (add rs\<^sub>1 rs\<^sub>2)"
+      by auto
+
+    have "r\<^sub>2 < r'" if "r' \<in> set (add rs\<^sub>1 rs\<^sub>2)" for r'
+      using that
+      apply (rule add_rank_bound)
+      using "3.prems" by auto
+    with EQ show ?thesis by auto
+  qed
+qed simp_all
+(*>*)
+
+lemma add_\<alpha>[simp]:
+  assumes "invar rs\<^sub>1"
+  assumes "invar rs\<^sub>2"
+  shows "\<alpha> (add rs\<^sub>1 rs\<^sub>2) = \<alpha> rs\<^sub>1 + \<alpha> rs\<^sub>2"
+(*<*)
+  using assms
+  apply (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct)
+  apply (auto simp: carry_\<alpha> Suc_leI add_rank_bound)
+  done
+(*>*)
+
+
+lemma size_snat:
+  assumes "invar rs"
+  shows "2^length rs \<le> \<alpha> rs + 1"
+(*<*)
+proof -
+  have "(2::nat)^length rs = (\<Sum>i\<in>{0..<length rs}. 2^i) + 1"
+    by (simp add: sum_power2)
+  also have "\<dots> \<le> \<alpha> rs + 1"
+    using assms unfolding \<alpha>_def
+    by (simp add: sorted_wrt_less_sum_mono_lowerbound)
+  finally show ?thesis .
+qed
+(*>*)
+
+fun t_carry :: "rank \<Rightarrow> snat \<Rightarrow> nat"
+(*<*)
+  where
+  "t_carry r [] = 1"
+| "t_carry r (r'#rest) = (if r<r' then 1 else 1 + t_carry (r+1) rest)"
+(*>*)
+
+definition t_inc :: "snat \<Rightarrow> nat"
+(*<*)
+  where "t_inc rs = t_carry 0 rs"
+(*>*)
+
+lemma t_inc_bound:
+  assumes "invar rs"
+  shows "t_inc rs \<le> log 2 (\<alpha> rs + 1) + 1"
+(*<*)
+proof -
+  have "t_carry r rs \<le> length rs + 1" for r
+    by (induction r rs rule: t_carry.induct) auto
+  hence "t_inc rs \<le> length rs + 1" unfolding t_inc_def by auto
+  hence "(2::nat)^t_inc rs \<le> 2^(length rs + 1)"
+    by (rule power_increasing) auto
+  also have "\<dots> \<le> 2*(\<alpha> rs + 1)" using size_snat[OF \<open>invar rs\<close>] by auto
+  finally have "2 ^ t_inc rs \<le> 2 * (\<alpha> rs + 1)" .
+  from le_log2_of_power[OF this] show ?thesis
+    by (simp only: log_mult of_nat_mult) auto
+qed
+(*>*)
+
+fun t_add :: "snat \<Rightarrow> snat \<Rightarrow> nat"
+(*<*)
+  where
+  "t_add rs [] = 1"
+| "t_add [] rs = 1"
+| "t_add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = 1 + (
+    if r\<^sub>1 < r\<^sub>2 then t_add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2)
+    else if r\<^sub>2<r\<^sub>1 then t_add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2
+    else t_carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2
+    )"
+(*>*)
+
+(*<*)
+lemma l_carry_estimate:
+  "t_carry r rs + length (carry r rs) = 2 + length rs"
+  by (induction r rs rule: carry.induct) auto
+
+lemma l_add_estimate:
+  "length (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1"
+  apply (induction rs\<^sub>1 rs\<^sub>2 rule: t_add.induct)
+  apply (auto simp: l_carry_estimate algebra_simps)
+  done
+(*>*)
+
+lemma t_add_bound:
+  fixes rs\<^sub>1 rs\<^sub>2
+  defines "n\<^sub>1 \<equiv> \<alpha> rs\<^sub>1"
+  defines "n\<^sub>2 \<equiv> \<alpha> rs\<^sub>2"
+  assumes INVARS: "invar rs\<^sub>1" "invar rs\<^sub>2"
+  shows "t_add rs\<^sub>1 rs\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
+(*<*)
+proof -
+  define n where "n = n\<^sub>1 + n\<^sub>2"
+
+  from l_add_estimate[of rs\<^sub>1 rs\<^sub>2]
+  have "t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1" by auto
+  hence "(2::nat)^t_add rs\<^sub>1 rs\<^sub>2 \<le> 2^(2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1)"
+    by (rule power_increasing) auto
+  also have "\<dots> = 2*(2^length rs\<^sub>1)\<^sup>2*(2^length rs\<^sub>2)\<^sup>2"
+    by (auto simp: algebra_simps power_add power_mult)
+  also note INVARS(1)[THEN size_snat]
+  also note INVARS(2)[THEN size_snat]
+  finally have "2 ^ t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2"
+    by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
+  from le_log2_of_power[OF this] have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 \<dots>"
+    by simp
+  also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)"
+    by (simp add: log_mult log_nat_power)
+  also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
+  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n + 1)"
+    by auto
+  also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
+  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
+    by auto
+  also have "log 2 2 \<le> 2" by auto
+  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
+  thus ?thesis unfolding n_def by (auto simp: algebra_simps)
+qed
+(*>*)
+
+
+
+(*<*)
+end
+(*>*)
diff --git a/12/ex12_tmpl.thy b/12/ex12_tmpl.thy
new file mode 100644
index 0000000..0dbd897
--- /dev/null
+++ b/12/ex12_tmpl.thy
@@ -0,0 +1,98 @@
+(*<*)
+theory ex12_tmpl
+imports
+  Complex_Main
+  "HOL-Library.Multiset"
+begin
+(*>*)
+text {* \ExerciseSheet{12}{29.~6.~2018} *}
+
+text \<open>
+  \Exercise{Sparse Binary Numbers}
+
+  Implement operations carry, inc, and add on sparse binary numbers,
+  analogously to the operations link, ins, and meld on binomial heaps.
+
+  Show that the operations have logarithmic worst-case complexity.
+\<close>
+
+type_synonym rank = nat
+type_synonym snat = "rank list"
+
+abbreviation invar :: "snat \<Rightarrow> bool" where "invar s \<equiv> sorted_wrt op< s"
+definition \<alpha> :: "snat \<Rightarrow> nat" where "\<alpha> s = (\<Sum>i\<leftarrow>s. 2^i)"
+
+lemmas [simp] = sorted_wrt_Cons sorted_wrt_append
+
+
+fun carry :: "rank \<Rightarrow> snat \<Rightarrow> snat"
+  where
+  "carry _ _ = undefined"
+
+lemma carry_invar[simp]: specify_something_meaningful oops
+
+lemma carry_\<alpha>: specify_something_meaningful oops
+
+
+definition inc :: "snat \<Rightarrow> snat" where "inc \<equiv> undefined"
+
+lemma inc_invar[simp]: "invar rs \<Longrightarrow> invar (inc rs)" sorry
+
+lemma inc_\<alpha>[simp]: "invar rs \<Longrightarrow> \<alpha> (inc rs) = Suc (\<alpha> rs)" sorry
+
+fun add :: "snat \<Rightarrow> snat \<Rightarrow> snat"
+  where
+  "add _ _ = undefined"
+
+
+lemma add_invar[simp]:
+  assumes "invar rs\<^sub>1"
+  assumes "invar rs\<^sub>2"
+  shows "invar (add rs\<^sub>1 rs\<^sub>2)"
+  sorry
+
+lemma add_\<alpha>[simp]:
+  assumes "invar rs\<^sub>1"
+  assumes "invar rs\<^sub>2"
+  shows "\<alpha> (add rs\<^sub>1 rs\<^sub>2) = \<alpha> rs\<^sub>1 + \<alpha> rs\<^sub>2"
+  sorry
+
+
+(** Size in relation to represented number *)
+lemma size_snat:
+  assumes "invar rs"
+  shows "2^length rs \<le> \<alpha> rs + 1"
+  sorry
+
+
+(** Timing *)
+
+fun t_carry :: "rank \<Rightarrow> snat \<Rightarrow> nat"
+  where
+  "t_carry _ _ = undefined"
+
+definition t_inc :: "snat \<Rightarrow> nat"
+  where "t_inc rs = undefined"
+
+lemma t_inc_bound:
+  assumes "invar rs"
+  shows "t_inc rs \<le> log 2 (\<alpha> rs + 1) + 1"
+  sorry
+
+fun t_add :: "snat \<Rightarrow> snat \<Rightarrow> nat"
+  where
+  "t_add _ _ = undefined"
+
+
+lemma t_add_bound:
+  fixes rs\<^sub>1 rs\<^sub>2
+  defines "n\<^sub>1 \<equiv> \<alpha> rs\<^sub>1"
+  defines "n\<^sub>2 \<equiv> \<alpha> rs\<^sub>2"
+  assumes INVARS: "invar rs\<^sub>1" "invar rs\<^sub>2"
+  shows "t_add rs\<^sub>1 rs\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
+  sorry
+
+
+(*<*)
+end
+(*>*)
diff --git a/12/hw12_tmpl.thy b/12/hw12_tmpl.thy
new file mode 100644
index 0000000..31c6937
--- /dev/null
+++ b/12/hw12_tmpl.thy
@@ -0,0 +1,240 @@
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q \<in> set_mset(mset q) \<Longrightarrow> \<forall>p \<in> set_mset(mset q). snd (get_min q) \<le> snd p"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+
+
+
+
+
+fun mset_tree :: "(('d\<times>'a),'b) tree \<Rightarrow> ('d\<times>'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
+
+type_synonym ('d, 'a) lheap = "(('d\<times>'a),nat)tree"
+
+fun rank :: "('d, 'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d, 'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('d\<times>'a),'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (d,m) r) =
+  (heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). m \<le> y))"
+
+fun ltree :: "('d, 'a) lheap \<Rightarrow> bool" where
+"ltree Leaf = True" |
+"ltree (Node n l a r) =
+ (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
+
+definition node :: "('d, 'a) lheap \<Rightarrow> ('d\<times>'a) \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"node l a r =
+ (let rl = rk l; rr = rk r
+  in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)"
+
+fun get_min :: "('d, 'a) lheap \<Rightarrow> ('d\<times>'a::linorder)" where
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1,a1) r1 =: t1) (Node n2 l2 (d2,a2) r2 =: t2) =
+   (if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2)
+    else node l2 (d2,a2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow>
+    if snd a1 \<le> snd a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::ord) \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
+by(cases t) auto
+
+lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d,a) r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). a \<le> y)"
+by(auto simp add: node_def)
+
+
+subsection "Functional Correctness"
+
+lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2"
+by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps)
+
+lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
+by (auto simp add: insert_def mset_merge)
+
+lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow>  get_min h \<in> set_mset(mset_tree h) \<Longrightarrow> \<forall>(x,y) \<in> set_mset(mset_tree h). snd (get_min h) \<le> y"
+  apply(induction h)
+   apply auto
+   apply blast
+  by blast
+
+lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
+by (cases h) (auto simp: mset_merge)
+
+lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
+proof(induction l r rule: merge.induct)
+  case (3 n1 l1 d1 a1 r1 n2 l2 d2 a2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (d1,a1) (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> a1 \<le> a2"
+    thus ?thesis using 3 by(simp)(auto simp: ltree_node)
+  qed
+qed simp_all
+
+lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"
+proof(induction l r rule: merge.induct)
+  case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un)
+qed simp_all
+
+lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)"
+by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)
+
+lemma heap_insert_aux1_aux1[simp]: "heap \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle>"
+  by(induction x)(auto)
+
+lemma heap_insert_aux1[simp]:  "heap t \<Longrightarrow> heap (merge \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle> t)"
+  apply(induction t)
+  by(auto simp add:heap_merge)
+
+lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
+by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
+
+lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
+by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
+
+lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
+by(cases t)(auto simp add: heap_merge simp del: merge.simps)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case 
+    by (metis (full_types) case_prodE get_min mset_tree.simps(1) prod.sel(2)) 
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
diff --git a/12/hw12_tmpl.thy~ b/12/hw12_tmpl.thy~
new file mode 100644
index 0000000..2a87cb8
--- /dev/null
+++ b/12/hw12_tmpl.thy~
@@ -0,0 +1,240 @@
+theory hw12_tmpl
+imports
+  "HOL-Data_Structures.Base_FDS"
+  "HOL-Data_Structures.Tree2"
+  "HOL-Library.Multiset"
+  Complex_Main
+begin
+
+
+
+text \<open>
+  \Homework{Explicit Priorities}{6.7.2018}
+
+  Modify the priority queue interface to handle multisets of pairs of
+  data and priority, i.e., the new \<open>mset\<close> function has the signature
+  @{text \<open>mset::'q \<Rightarrow> ('d\<times>'a::linorder) multiset\<close>}.
+
+  Next, implement the new interface using leftist heaps.
+  No complexity proofs are required.
+
+  Hints:
+    \<^item> Start with the existing theories, and modify them!
+    \<^item> Be careful to design a good specification for \<open>get_min\<close>!
+
+\<close>
+
+(** This template provides a copy of the relevant theories, ready for modification. *)
+
+
+text \<open>Priority queue interface:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "('d\<times>'a::linorder) \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> ('d\<times>'a::linorder)"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> ('d\<times>'a::linorder) multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q \<in> set_mset(mset q) \<Longrightarrow> \<forall>p \<in> set_mset(mset q). snd (get_min q) \<le> snd p"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+
+
+
+
+
+
+
+
+
+
+
+fun mset_tree :: "(('d\<times>'a),'b) tree \<Rightarrow> ('d\<times>'a) multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
+
+type_synonym ('d, 'a) lheap = "(('d\<times>'a),nat)tree"
+
+fun rank :: "('d, 'a) lheap \<Rightarrow> nat" where
+"rank Leaf = 0" |
+"rank (Node _ _ _ r) = rank r + 1"
+
+fun rk :: "('d, 'a) lheap \<Rightarrow> nat" where
+"rk Leaf = 0" |
+"rk (Node n _ _ _) = n"
+
+text{* The invariants: *}
+
+fun (in linorder) heap :: "(('d\<times>'a),'b) tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node _ l (d,m) r) =
+  (heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). m \<le> y))"
+
+fun ltree :: "('d, 'a) lheap \<Rightarrow> bool" where
+"ltree Leaf = True" |
+"ltree (Node n l a r) =
+ (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
+
+definition node :: "('d, 'a) lheap \<Rightarrow> ('d\<times>'a) \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"node l a r =
+ (let rl = rk l; rr = rk r
+  in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)"
+
+fun get_min :: "('d, 'a) lheap \<Rightarrow> ('d\<times>'a::linorder)" where
+"get_min(Node n l a r) = a"
+
+text \<open>For function \<open>merge\<close>:\<close>
+unbundle pattern_aliases
+declare size_prod_measure[measure_function]
+
+fun merge :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"merge Leaf t2 = t2" |
+"merge t1 Leaf = t1" |
+"merge (Node n1 l1 (d1,a1) r1 =: t1) (Node n2 l2 (d2,a2) r2 =: t2) =
+   (if a1 \<le> a2 then node l1 (d1,a1) (merge r1 t2)
+    else node l2 (d2,a2) (merge r2 t1))"
+
+lemma merge_code: "merge t1 t2 = (case (t1,t2) of
+  (Leaf, _) \<Rightarrow> t2 |
+  (_, Leaf) \<Rightarrow> t1 |
+  (Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow>
+    if snd a1 \<le> snd a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))"
+by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
+
+hide_const (open) insert
+
+definition insert :: "('d\<times>'a::ord) \<Rightarrow> ('d, 'a) lheap \<Rightarrow> ('d, 'a) lheap" where
+"insert x t = merge (Node 1 Leaf x Leaf) t"
+
+fun del_min :: "('d, 'a::ord) lheap \<Rightarrow> ('d, 'a) lheap" where
+"del_min Leaf = Leaf" |
+"del_min (Node n l x r) = merge l r"
+
+
+subsection "Lemmas"
+
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
+by(cases t) auto
+
+lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"
+by(auto simp add: node_def)
+
+lemma heap_node: "heap (node l (d,a) r) \<longleftrightarrow>
+  heap l \<and> heap r \<and> (\<forall>(x,y) \<in> set_mset(mset_tree l + mset_tree r). a \<le> y)"
+by(auto simp add: node_def)
+
+
+subsection "Functional Correctness"
+
+lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2"
+by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps)
+
+lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
+by (auto simp add: insert_def mset_merge)
+
+lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow>  get_min h \<in> set_mset(mset_tree h) \<Longrightarrow> \<forall>(x,y) \<in> set_mset(mset_tree h). snd (get_min h) \<le> y"
+  apply(induction h)
+   apply auto
+   apply blast
+  by blast
+
+lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
+by (cases h) (auto simp: mset_merge)
+
+lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
+proof(induction l r rule: merge.induct)
+  case (3 n1 l1 d1 a1 r1 n2 l2 d2 a2 r2)
+  show ?case (is "ltree(merge ?t1 ?t2)")
+  proof cases
+    assume "a1 \<le> a2"
+    hence "ltree (merge ?t1 ?t2) = ltree (node l1 (d1,a1) (merge r1 ?t2))" by simp
+    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
+      by(simp add: ltree_node)
+    also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by (simp)
+    finally show ?thesis .
+  next (* analogous but automatic *)
+    assume "\<not> a1 \<le> a2"
+    thus ?thesis using 3 by(simp)(auto simp: ltree_node)
+  qed
+qed simp_all
+
+lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"
+proof(induction l r rule: merge.induct)
+  case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un)
+qed simp_all
+
+lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)"
+by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)
+
+lemma heap_insert_aux1_aux1[simp]: "heap \<langle>a, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle>"
+  by(induction x)(auto)
+
+lemma heap_insert_aux1[simp]:  "heap t \<Longrightarrow> heap (merge \<langle>Suc 0, \<langle>\<rangle>, x, \<langle>\<rangle>\<rangle> t)"
+  apply(induction t)
+  by(auto simp add:heap_merge)
+
+lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
+by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
+
+lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
+by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
+
+lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
+by(cases t)(auto simp add: heap_merge simp del: merge.simps)
+
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation lheap: Priority_Queue_Merge
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
+proof(standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case (2 q) show ?case by (cases q) auto
+next
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
+next
+  case 5 thus ?case
+    by (metis (full_types) case_prodE get_min mset_tree.simps(1) prod.sel(2)) 
+next
+  case 6 thus ?case by(simp)
+next
+  case 7 thus ?case by(simp add: heap_insert ltree_insert)
+next
+  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
+qed
+
+
+
+
+
+
+end
diff --git a/13/ex13.pdf b/13/ex13.pdf
new file mode 100644
index 0000000..9595872
Binary files /dev/null and b/13/ex13.pdf differ
diff --git a/13/hw13tmpl.thy b/13/hw13tmpl.thy
new file mode 100644
index 0000000..07829ca
--- /dev/null
+++ b/13/hw13tmpl.thy
@@ -0,0 +1,43 @@
+theory hw13tmpl
+imports Main
+begin
+
+
+fun push :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"push x xs = x # xs"
+
+fun pop :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"pop n xs = drop n xs"
+
+text \<open>You may assume\<close>
+
+definition t_push :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_push x xs = 1"
+
+definition t_pop :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_pop n xs = min n (length xs)"
+
+definition \<Phi> :: "'a list \<Rightarrow> int" where
+"\<Phi> bs = int(length bs)"
+
+lemma \<Phi>_non_neg: "\<Phi> bs \<ge> 0"
+by(simp add: \<Phi>_def)
+
+definition "init = []"
+
+lemma \<Phi>_init: "\<Phi> init = 0"
+by(simp add: \<Phi>_def init_def)
+
+lemma push_const: "int(t_push x xs)  + \<Phi>(push x xs) - \<Phi> xs = 2"
+apply(induction xs rule: push.induct)
+  apply (auto simp add: \<Phi>_def t_push_def)
+  done
+
+lemma pop_const: "int(t_pop n xs) + \<Phi>(pop n xs) - \<Phi> xs = 0"
+  apply(induction xs rule: pop.induct)
+  apply (auto simp add: \<Phi>_def t_pop_def)
+  done
+
+end
+
+
diff --git a/13/hw13tmpl.thy~ b/13/hw13tmpl.thy~
new file mode 100644
index 0000000..ac403d2
--- /dev/null
+++ b/13/hw13tmpl.thy~
@@ -0,0 +1,45 @@
+(*<*)
+theory hw13tmpl
+imports Main
+begin
+(*>*)
+
+text \<open>\Homework{Amortized Complexity}{13.07.2018}
+
+  This is an old exam question, which we have converted to a homework to
+  be done with Isabelle!
+\<close>
+
+text \<open>A ``stack with multipop'' is a list with the following two interface functions:\<close>
+
+fun push :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"push x xs = x # xs"
+
+fun pop :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"pop n xs = drop n xs"
+
+text \<open>You may assume\<close>
+
+definition t_push :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_push x xs = 1"
+
+definition t_pop :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_pop n xs = min n (length xs)"
+
+text \<open>Use the potential method to show that
+the amortized complexity of \<open>push\<close> and \<open>pop\<close> is constant.
+
+Provide complete proofs in Isabelle!
+
+
+
+Original text here was:
+\emph{
+If you need any properties of the auxiliary functions \<open>length\<close>, \<open>drop\<close> and \<open>min\<close>,
+you should state them but you do not need to prove them.}\<close>
+
+(*<*)
+end
+(*>*)
+
+
diff --git a/BeCreative/UFDS.thy b/BeCreative/UFDS.thy
new file mode 100644
index 0000000..a78f0c0
--- /dev/null
+++ b/BeCreative/UFDS.thy
@@ -0,0 +1,169 @@
+theory UFDS
+  imports Main
+begin
+fun fpow where
+  "fpow f 0 = id"
+| "fpow f (Suc n) = f o fpow f n"
+
+lemma fpow_is_compow[simp]: "fpow = op ^^"
+proof (intro ext)
+  fix f n x
+  show "fpow f n x = (f^^n) x"
+    apply (induction n arbitrary: x)
+     apply auto
+    done
+qed
+
+
+
+(*location of array contains parent*)
+
+partial_function (tailrec) find' where
+  "find' ls i = (if ls!i = i then i else find' ls (ls!i))"
+
+thm find'.simps
+
+
+definition "init n = [0..<n]"
+definition "pred ls i = ls!i"
+definition "is_root ls i \<longleftrightarrow> pred ls i = i"
+(*definition find where "find ls i == fpow (pred ls) (length ls) i"*)
+definition "invar ls \<longleftrightarrow> 
+  (set ls \<subseteq> {0..<length ls}) 
+\<and> (\<forall>i<length ls. \<exists>n\<in>{0..<length ls}. is_root ls (fpow (pred ls) n i)) "
+
+
+definition union where "union i j ls = ls[find' ls i := find' ls j]"
+
+type_synonym eqcs = "nat \<Rightarrow> nat set"
+
+definition \<alpha> :: "nat list \<Rightarrow> eqcs" where "\<alpha> ls i = 
+  (if i<length ls then {j. j<length ls \<and> find' ls j = find' ls i} else {i})"
+
+definition union_eqc :: "nat \<Rightarrow> nat \<Rightarrow> eqcs \<Rightarrow> eqcs"
+  where
+  "union_eqc x y eqc i = (if i \<in> eqc x \<union> eqc y then eqc x \<union> eqc y else eqc i)"
+
+value "([5,1,2]::nat list)[1:=2]"
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "length ls = length (union x y ls)"
+  using assms
+proof(induction ls arbitrary: x y)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a ls)
+  then show ?case 
+    unfolding union_def
+    by (metis length_list_update)
+qed
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "invar (union x y ls)"
+  apply(auto simp:invar_def)
+  
+  oops
+
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "\<alpha> (union x y ls) = union_eqc x y (\<alpha> ls)"
+
+
+lemma "invar [0..<N]"
+proof(induction N)
+    case 0
+    then show ?case
+      unfolding invar_def
+      by(auto)
+  next
+    case (Suc N)
+    then show ?case
+      
+      unfolding invar_def
+      apply(auto)
+      have "n = N \<or> n \<in> {0..<N}" (is "?C1 \<or> ?C2")
+      
+      qed
+
+  thm find'.simps
+
+lemma "\<alpha> [0..<N] i = {i}"
+  apply (auto simp add: \<alpha>_def)
+  apply (auto simp add: \<alpha>_def find'.simps split del: if_split)
+
+  apply (subst (asm) find'.simps)
+  apply (subst (asm) (2) find'.simps)
+  apply auto
+  done
+
+lemma "find "
+
+
+fun natbelow :: "nat \<Rightarrow> nat list" where
+  "natbelow 0 = [0]"
+| "natbelow (Suc n) = (Suc n) # natbelow n"
+
+value "rev [1::nat,2,3]"
+
+fun init :: "nat \<Rightarrow> nat list" where
+ "init n = rev (natbelow n)"
+
+value "init 10"
+value "[0..<10]"
+
+term upto
+term upt
+
+fun findParentAux :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat" where
+  "findParentAux n 0 xs  = (xs!n)"
+| "findParentAux n (Suc b) xs = (if (xs!n = n) then n else findParentAux (xs!n) b xs)"
+
+fun findParent :: "nat \<Rightarrow> nat list \<Rightarrow> nat" where
+  "findParent n xs = findParentAux n (size xs) xs"
+
+
+fun isSameSet :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool" where
+  "isSameSet a b l = (findParent a l = findParent b l)"
+
+value "init 10"
+value "findParent 5 [0, 1, 2, 3, 4, 5, 6]"
+value "isSameSet 2 3 [0, 1, 4, 5, 5, 1]"
+
+fun replace :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list" where
+  "replace _ _ [] = []"
+| "replace a b (x#xs) = (if (a = x) then b#xs else x#(replace a b xs))"
+
+value "let ls = [0::nat,1,2,3,4,5,6] in ls[4:=9]"
+
+
+fun union :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list" where
+  "union a b ls = (if (isSameSet a b ls) then ls else (replace (findParent a ls) b ls))"
+
+value "isSameSet 2 3 (union 5 3 [0, 1, 2, 3, 4, 2, 6])"
+value "union 5 0 [0, 1, 2, 3, 4, 2, 6]"
+value "union 1 0 [1, 0]"
+
+fun valid :: "nat list \<Rightarrow> bool" where
+  "valid [] = False"
+| "valid t = (\<forall>x \<in> set t. t!x = x)"
+
+value "valid [1, 0]"
+value "init 10"
+value "valid (init 10)"
+
+fun sizeufd :: "nat list \<Rightarrow> nat" where
+  "sizeufd fn = size fn + 1"
+
+(* here be dragons *)
+
+lemma isSameSetWorks:"\<not> isSameSet a b t \<Longrightarrow> findParent a t \<noteq> findParent b t"
+  by simp
+
+lemma unionWorks:"valid t \<Longrightarrow> n \<ge> max a b \<Longrightarrow> isSameSet a b (union a b (init n))"
+  apply(auto)
+
+end
\ No newline at end of file
diff --git a/BeCreative/UFDS.thy~ b/BeCreative/UFDS.thy~
new file mode 100644
index 0000000..a78f0c0
--- /dev/null
+++ b/BeCreative/UFDS.thy~
@@ -0,0 +1,169 @@
+theory UFDS
+  imports Main
+begin
+fun fpow where
+  "fpow f 0 = id"
+| "fpow f (Suc n) = f o fpow f n"
+
+lemma fpow_is_compow[simp]: "fpow = op ^^"
+proof (intro ext)
+  fix f n x
+  show "fpow f n x = (f^^n) x"
+    apply (induction n arbitrary: x)
+     apply auto
+    done
+qed
+
+
+
+(*location of array contains parent*)
+
+partial_function (tailrec) find' where
+  "find' ls i = (if ls!i = i then i else find' ls (ls!i))"
+
+thm find'.simps
+
+
+definition "init n = [0..<n]"
+definition "pred ls i = ls!i"
+definition "is_root ls i \<longleftrightarrow> pred ls i = i"
+(*definition find where "find ls i == fpow (pred ls) (length ls) i"*)
+definition "invar ls \<longleftrightarrow> 
+  (set ls \<subseteq> {0..<length ls}) 
+\<and> (\<forall>i<length ls. \<exists>n\<in>{0..<length ls}. is_root ls (fpow (pred ls) n i)) "
+
+
+definition union where "union i j ls = ls[find' ls i := find' ls j]"
+
+type_synonym eqcs = "nat \<Rightarrow> nat set"
+
+definition \<alpha> :: "nat list \<Rightarrow> eqcs" where "\<alpha> ls i = 
+  (if i<length ls then {j. j<length ls \<and> find' ls j = find' ls i} else {i})"
+
+definition union_eqc :: "nat \<Rightarrow> nat \<Rightarrow> eqcs \<Rightarrow> eqcs"
+  where
+  "union_eqc x y eqc i = (if i \<in> eqc x \<union> eqc y then eqc x \<union> eqc y else eqc i)"
+
+value "([5,1,2]::nat list)[1:=2]"
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "length ls = length (union x y ls)"
+  using assms
+proof(induction ls arbitrary: x y)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a ls)
+  then show ?case 
+    unfolding union_def
+    by (metis length_list_update)
+qed
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "invar (union x y ls)"
+  apply(auto simp:invar_def)
+  
+  oops
+
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "\<alpha> (union x y ls) = union_eqc x y (\<alpha> ls)"
+
+
+lemma "invar [0..<N]"
+proof(induction N)
+    case 0
+    then show ?case
+      unfolding invar_def
+      by(auto)
+  next
+    case (Suc N)
+    then show ?case
+      
+      unfolding invar_def
+      apply(auto)
+      have "n = N \<or> n \<in> {0..<N}" (is "?C1 \<or> ?C2")
+      
+      qed
+
+  thm find'.simps
+
+lemma "\<alpha> [0..<N] i = {i}"
+  apply (auto simp add: \<alpha>_def)
+  apply (auto simp add: \<alpha>_def find'.simps split del: if_split)
+
+  apply (subst (asm) find'.simps)
+  apply (subst (asm) (2) find'.simps)
+  apply auto
+  done
+
+lemma "find "
+
+
+fun natbelow :: "nat \<Rightarrow> nat list" where
+  "natbelow 0 = [0]"
+| "natbelow (Suc n) = (Suc n) # natbelow n"
+
+value "rev [1::nat,2,3]"
+
+fun init :: "nat \<Rightarrow> nat list" where
+ "init n = rev (natbelow n)"
+
+value "init 10"
+value "[0..<10]"
+
+term upto
+term upt
+
+fun findParentAux :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat" where
+  "findParentAux n 0 xs  = (xs!n)"
+| "findParentAux n (Suc b) xs = (if (xs!n = n) then n else findParentAux (xs!n) b xs)"
+
+fun findParent :: "nat \<Rightarrow> nat list \<Rightarrow> nat" where
+  "findParent n xs = findParentAux n (size xs) xs"
+
+
+fun isSameSet :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool" where
+  "isSameSet a b l = (findParent a l = findParent b l)"
+
+value "init 10"
+value "findParent 5 [0, 1, 2, 3, 4, 5, 6]"
+value "isSameSet 2 3 [0, 1, 4, 5, 5, 1]"
+
+fun replace :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list" where
+  "replace _ _ [] = []"
+| "replace a b (x#xs) = (if (a = x) then b#xs else x#(replace a b xs))"
+
+value "let ls = [0::nat,1,2,3,4,5,6] in ls[4:=9]"
+
+
+fun union :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list" where
+  "union a b ls = (if (isSameSet a b ls) then ls else (replace (findParent a ls) b ls))"
+
+value "isSameSet 2 3 (union 5 3 [0, 1, 2, 3, 4, 2, 6])"
+value "union 5 0 [0, 1, 2, 3, 4, 2, 6]"
+value "union 1 0 [1, 0]"
+
+fun valid :: "nat list \<Rightarrow> bool" where
+  "valid [] = False"
+| "valid t = (\<forall>x \<in> set t. t!x = x)"
+
+value "valid [1, 0]"
+value "init 10"
+value "valid (init 10)"
+
+fun sizeufd :: "nat list \<Rightarrow> nat" where
+  "sizeufd fn = size fn + 1"
+
+(* here be dragons *)
+
+lemma isSameSetWorks:"\<not> isSameSet a b t \<Longrightarrow> findParent a t \<noteq> findParent b t"
+  by simp
+
+lemma unionWorks:"valid t \<Longrightarrow> n \<ge> max a b \<Longrightarrow> isSameSet a b (union a b (init n))"
+  apply(auto)
+
+end
\ No newline at end of file
diff --git a/BeCreative/UnionFind.thy b/BeCreative/UnionFind.thy
new file mode 100644
index 0000000..f0fa84b
--- /dev/null
+++ b/BeCreative/UnionFind.thy
@@ -0,0 +1,118 @@
+theory UnionFind
+  imports Main
+begin
+
+(*Initial definitions*)
+
+definition "init n = [0..<n]"                         (*initial list is a list from 0 to n-1*)
+definition "pred ls i = ls!i"                         (*location at every index points to parent*)
+definition "is_root ls i \<longleftrightarrow> pred ls i = i"           (*if own parent, then root*)
+
+function (domintros) root_of where                    (*function with custom termination*)
+  "root_of ls i = (if is_root ls i then i else root_of ls (ls!i))"
+   apply auto[1]
+  by blast
+
+thm "root_of.psimps"
+thm "root_of.pinduct"
+
+
+(*A list is a valid UFDS if all its indices are less than the length of the list, and the indices terminate*)
+definition "invar ls \<equiv>  \<forall>i<length ls. ls!i < length ls \<and> root_of_dom (ls,i)"  
+
+(*Lemmas*)
+
+(*If an element has itself as a root, it is a root*)
+lemma is_root_corr : "ls!i = i \<Longrightarrow> is_root ls i"
+  apply(subst is_root_def)
+  apply(subst pred_def)
+  by simp
+
+(*The init function sets all the members to themselves as roots*)
+lemma init_corr : "\<forall>i\<in> set(init n). (is_root (init n) i)"
+  apply(subst is_root_def)
+  apply(auto)
+  by (simp add: pred_def init_def)
+  
+(*If a member is a root, it is its own root*)
+lemma root_of_base: "is_root ls i \<Longrightarrow> root_of ls i = i"
+  apply(subst root_of.psimps)
+   apply(auto)
+  using root_of.domintros by blast
+
+(*The root of a non-root member is the same as the root of its parent's member*)
+lemma root_of_step: " \<lbrakk> invar ls; i < length ls; ls!i \<noteq> i \<rbrakk>  \<Longrightarrow> root_of ls i = root_of ls (ls!i)"
+  apply(subst root_of.psimps)
+  apply (simp add: invar_def)
+  by (simp add: pred_def is_root_def)
+  
+(*The root of a parent is the root of its child*)
+lemma root_of_back: " \<lbrakk> invar ls; i < length ls; ls!i \<noteq> i \<rbrakk>  \<Longrightarrow> root_of ls (ls!i) = root_of ls i"
+  by (simp add: root_of_step)
+  
+(*The init function returns a valid UFDS*)
+lemma invar_init: "invar (init n)"
+  apply(subst init_def)
+  apply(subst invar_def)
+  apply(auto)
+  using is_root_corr root_of.domintros by fastforce
+
+(*union of two sets*)
+definition union where "union i j ls = ls[root_of ls i := root_of ls j]"
+
+type_synonym eqcs = "nat \<Rightarrow> nat set"
+
+(*return disjoint set the element belongs to*)
+definition \<alpha> :: "nat list \<Rightarrow> eqcs" where "\<alpha> ls i = 
+  (if i<length ls then {j. j<length ls \<and> root_of ls j = root_of ls i} else {i})"
+
+(*return if an element is part of a disjoint set after uniting two other elements*)
+definition union_eqc :: "nat \<Rightarrow> nat \<Rightarrow> eqcs \<Rightarrow> eqcs"
+  where
+  "union_eqc x y eqc i = (if i \<in> eqc x \<union> eqc y then eqc x \<union> eqc y else eqc i)"
+
+(*Lemmas*)
+
+(*Every disjoint set from init list has only itself as an element*)
+lemma "\<alpha> (init n) i = {i}"
+  apply (auto simp add: init_def \<alpha>_def)
+  using is_root_corr root_of_base by auto
+
+(*Union does not change length of list*)
+lemma length_same : "length ls = length (union a b ls)"
+  by (simp add: union_def)
+
+
+
+
+
+
+(*Lemmas I couldn't prove*)
+lemma length_fixed : "\<lbrakk>invar ls ; x < length ls ; y < length ls ; i < length ls \<rbrakk> \<Longrightarrow> union x y ls ! i < length (union x y ls)"
+  apply(simp add: union_def)
+  apply(subst root_of.psimps)
+   apply(auto)
+  using invar_def apply auto[1]
+  
+  oops
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "\<alpha> (union x y ls) = union_eqc x y (\<alpha> ls)"
+  oops
+  
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "invar (union x y ls)"
+  unfolding invar_def
+proof(intro allI)
+  fix i
+  have "union x y ls ! i < length (union x y ls)" using assms
+    oops
+
+lemma all_have_root: "invar ls \<Longrightarrow> i < length ls \<Longrightarrow> root_of ls i < length ls"
+  oops
+  
+
+end
\ No newline at end of file
diff --git a/BeCreative/UnionFind.thy~ b/BeCreative/UnionFind.thy~
new file mode 100644
index 0000000..efd15e6
--- /dev/null
+++ b/BeCreative/UnionFind.thy~
@@ -0,0 +1,96 @@
+theory UnionFind
+  imports Main
+begin
+
+definition "init n = [0..<n]"
+definition "pred ls i = ls!i"
+definition "is_root ls i \<longleftrightarrow> pred ls i = i"
+
+function (domintros) root_of where
+  "root_of ls i = (if is_root ls i then i else root_of ls (ls!i))"
+   apply auto[1]
+  by blast
+
+thm "root_of.psimps"
+thm "root_of.pinduct"
+
+definition "invar ls \<equiv>  \<forall>i<length ls. ls!i<length ls \<and> root_of_dom (ls,i)"
+
+lemma is_root_corr : "ls!i = i \<Longrightarrow> is_root ls i"
+  apply(subst is_root_def)
+  apply(subst pred_def)
+  by simp
+
+lemma init_corr : "\<forall>i\<in> set(init n). (is_root (init n) i)"
+  apply(subst is_root_def)
+  apply(auto)
+  by (simp add: pred_def init_def)
+  
+
+lemma root_of_base: "is_root ls i \<Longrightarrow> root_of ls i = i"
+  apply(subst root_of.psimps)
+   apply(auto)
+  using root_of.domintros by blast
+
+
+lemma root_of_step: " \<lbrakk> invar ls; i < length ls; ls!i \<noteq> i \<rbrakk>  \<Longrightarrow> root_of ls i = root_of ls (ls!i)"
+  apply(subst root_of.psimps)
+  apply (simp add: invar_def)
+  by (simp add: pred_def is_root_def)
+  
+
+lemma invar_init: "invar (init n)"
+  apply(subst init_def)
+  apply(subst invar_def)
+  apply(auto)
+  using is_root_corr root_of.domintros by fastforce
+
+lemma all_have_root: "invar ls \<Longrightarrow> i < length ls \<Longrightarrow> root_of ls i < length ls"
+  oops
+  
+definition union where "union i j ls = ls[root_of ls i := root_of ls j]"
+
+type_synonym eqcs = "nat \<Rightarrow> nat set"
+
+definition \<alpha> :: "nat list \<Rightarrow> eqcs" where "\<alpha> ls i = 
+  (if i<length ls then {j. j<length ls \<and> root_of ls j = root_of ls i} else {i})"
+
+definition union_eqc :: "nat \<Rightarrow> nat \<Rightarrow> eqcs \<Rightarrow> eqcs"
+  where
+  "union_eqc x y eqc i = (if i \<in> eqc x \<union> eqc y then eqc x \<union> eqc y else eqc i)"
+
+lemma "\<alpha> (init n) i = {i}"
+  apply (auto simp add: init_def \<alpha>_def)
+  using is_root_corr root_of_base by auto
+
+lemma length_same : "length ls = length (union a b ls)"
+  by (simp add: union_def)
+
+
+lemma length_fixed : "\<lbrakk>invar ls ; x < length ls ; y < length ls ; i < length ls \<rbrakk> \<Longrightarrow> union x y ls ! i < length (union x y ls)"
+  apply(simp add: union_def)
+  apply(subst root_of.psimps)
+   apply(auto)
+  using invar_def apply auto[1]
+  
+  oops
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "\<alpha> (union x y ls) = union_eqc x y (\<alpha> ls)"
+  oops
+  
+
+lemma 
+  assumes "invar ls" "x<length ls" "y<length ls"
+  shows "invar (union x y ls)"
+  unfolding invar_def
+proof(intro allI)
+  fix i
+  have "union x y ls ! i < length (union x y ls)" using assms
+    oops
+
+
+  
+
+end
\ No newline at end of file