added some exercises of functional data structures and a script of di…

…screte optimization

Discrete Optimization/cut.py

@@ -0,0 +1,47 @@
+# usage: python3 cut.py
+# change the input!
+
+import numpy as np
+
+# directly insert the subset of A here
+Ab = np.array([[2, 0], [1, 3]])
+
+# insert the vector with respect to which calculate the cut
+v = np.array([1, 2])
+
+# optimum point
+x = np.array([3, 8/3])
+
+# do not edit below this line
+
+# matrix inversion
+Ab_inv = np.linalg.inv(Ab)
+print('Inverse of Ab: \n', Ab_inv)
+
+# multiply the two
+v_Ab_inv = np.matmul(np.transpose(v), Ab_inv)
+print('\nv^t * Ab^t^-1 (column vector): \n', v_Ab_inv)
+
+# now calculate y
+y = v_Ab_inv - np.floor(v_Ab_inv)
+print('\ny^t: \n', y)
+
+# now calculate q
+q = np.matmul(np.transpose(y), Ab)
+print('\nq: \n', q)
+
+# finally, find the cut
+qx = np.matmul(q, x)
+print('\nq^t x*: \n', qx)
+
+string = ''
+
+it = np.nditer(q, flags=['f_index'])
+for i in it:
+	if (i >= 0):
+		string += ' + '
+	#else:
+	#	string += '-'
+	string += str(i)[0:1] + 'x' + str(it.index + 1)
+
+print('\n', string[1:], ' <= abs(', str(qx)[0:4], ') = ', np.floor(qx))

Functional Data Structures/homework01/Check.thy

@@ -0,0 +1,14 @@
+theory Check
+imports Submission
+begin
+
+lemma max_greater: "x \<in> set xs \<Longrightarrow> x\<le>lmax xs"
+  by (rule max_greater)
+
+lemma max_reverse: "lmax (reverse xs) = lmax xs"
+  by (rule max_reverse)
+
+
+end
+
+

Functional Data Structures/homework01/Defs.thy

@@ -0,0 +1,14 @@
+theory Defs
+imports Main
+begin
+
+fun snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
+"snoc [] x = [x]" |
+"snoc (y # ys) x = y # (snoc ys x)"
+
+fun reverse :: "'a list \<Rightarrow> 'a list" (*<*) where
+"reverse [] = []" |
+"reverse (x # xs) = snoc (reverse xs) x" (*>*)
+
+end
+

Functional Data Structures/homework01/Submission.thy

@@ -0,0 +1,25 @@
+theory Submission
+imports Defs
+begin
+
+fun lmax:: "nat list \<Rightarrow> nat" where
+  "lmax [] = 0" |
+  "lmax (x#xs) = (if x > lmax xs then x else lmax xs)"
+
+lemma max_greater:
+  "(x::nat) \<in> set xs \<Longrightarrow> x \<le> lmax xs"
+  by (induct xs) auto
+
+lemma lmax_snoc:
+ "lmax (snoc xs y) = lmax (y#xs)"
+  apply (induct xs)
+  apply (auto)
+  done
+
+lemma max_reverse:
+  "lmax (reverse xs) = lmax xs"
+  apply (induct xs)
+  apply (auto simp add: lmax_snoc)
+  done 
+
+end

Functional Data Structures/homework02/Check.thy

@@ -0,0 +1,21 @@
+theory Check
+  imports Submission
+begin
+
+lemma ldistinct_rev: "ldistinct (rev xs) \<longleftrightarrow> ldistinct xs"
+  by (rule ldistinct_rev) 
+
+lemma length_fold: "length_fold xs = length xs"  
+  by (rule length_fold)    
+
+lemma length_foldr: "length_foldr xs = length xs"  
+  by (rule length_foldr)
+
+lemma slice_append: "slice xs s l1 @ slice xs (s+l1) l2 = slice xs s (l1+l2)"
+  by (rule slice_append)
+
+lemma ldistinct_slice: "ldistinct xs \<Longrightarrow> ldistinct (slice xs s l)"
+  by (rule ldistinct_slice)
+
+end
+

Functional Data Structures/homework02/Defs.thy

@@ -0,0 +1,7 @@
+theory Defs
+  imports Main
+begin
+
+
+end
+

Functional Data Structures/homework02/Homework02.thy

@@ -0,0 +1,163 @@
+theory Homework02
+imports Main
+begin
+
+(* primitive recursive functions *)
+thm fold.simps
+thm foldr.simps
+
+(* folding *)
+definition list_sum':: "nat list \<Rightarrow> nat"  where
+  "list_sum' xs \<equiv> fold (+) xs 0"
+
+thm list_sum'_def
+
+value "list_sum' [1, 2, 3]"
+value "fold (*) [1::nat, 2, 3] 2"
+
+fun list_sum:: "nat list \<Rightarrow> nat" where
+  "list_sum [] = 0" |
+  "list_sum (x#xs) = x + list_sum xs"
+
+lemma lemma_aux: "fold (+) xs a = list_sum xs + a"
+  apply (induction xs arbitrary: a)
+  apply auto
+  done
+
+lemma "list_sum xs = list_sum' xs"
+  apply (auto simp: list_sum'_def lemma_aux)
+  done
+
+
+(* binary trees *)
+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"
+
+value "inorder (Node (Node (Leaf (1::nat)) (Leaf 2)) (Leaf 3))"
+term "fold f (inorder t) s"
+
+fun fold_ltree:: "('a \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> 'a ltree \<Rightarrow> 's \<Rightarrow> 's" where
+  "fold_ltree f (Leaf x) s = f x s" |
+  "fold_ltree f (Node l r) s = fold_ltree f r (fold_ltree f l s)"
+
+lemma "fold f (inorder t) s = fold_ltree f t s"
+  apply (induct t arbitrary: s)
+  apply auto
+  done
+
+fun mirror:: "'a ltree \<Rightarrow> 'a ltree" where
+  "mirror (Leaf x) = Leaf x" |
+  "mirror (Node l r) = (Node (mirror r) (mirror l))"
+
+lemma "inorder (mirror t) = rev (inorder t)"
+  apply (induct t)
+  apply auto
+  done
+
+
+(* list of lists *)
+fun shuffles:: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
+  "shuffles xs [] = [xs]" |
+  "shuffles [] ys = [ys]" |
+  "shuffles (x#xs) (y#ys) = map (\<lambda>xs. x # xs) (shuffles xs (y#ys)) @ 
+                            map (\<lambda>ys. y # ys) (shuffles (x#xs) ys)"
+
+thm shuffles.induct
+
+lemma "zs \<in> set (shuffles xs ys) \<Longrightarrow> length zs = length xs + length ys"
+  apply (induction xs ys arbitrary: zs rule: shuffles.induct)
+    apply auto
+  done
+
+
+(* contains *)
+fun contains:: "'a \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "contains x [] = False" |
+ "contains y (x#xs) = (if x = y then True else contains y xs)"
+
+(* ldistinct *)
+fun ldistinct:: "'a list \<Rightarrow> bool" where
+  "ldistinct [] = True" |
+  "ldistinct (x#xs) = (if contains x xs = True then False else ldistinct xs)"
+
+thm contains.induct
+thm ldistinct.induct
+
+(* show that a reversed list is distinct iff original is distinct *)
+
+lemma lemma1: "contains x (xs @ [a]) = contains x ([a] @ xs)"
+  apply (induction xs)
+   apply (auto)
+  done
+
+lemma lemma2: "contains x (rev xs) = contains x xs"
+  apply (induct xs)
+  apply (auto simp: lemma1)
+  done 
+
+lemma lemma3: "ldistinct (xs @ [x]) = ldistinct ([x] @ xs)"
+  apply (induct xs)
+   apply (auto simp: lemma1)
+  done
+
+lemma "ldistinct (rev xs) \<longleftrightarrow> ldistinct xs"
+  apply (induct xs)
+   apply (auto simp: lemma3 lemma2)
+  done 
+
+
+(* folding *)
+
+fun a::  "'a \<Rightarrow> nat \<Rightarrow> nat" where
+  "a n m = m + 1"
+
+definition length_fold:: "'a list \<Rightarrow> nat" where
+  "length_fold x \<equiv> fold (a) x 0"
+
+definition length_foldr:: "'a list \<Rightarrow> nat" where
+  "length_foldr x \<equiv> foldr (a) x 0" 
+
+lemma length_fold_sum: "fold a xs x = length xs + x"
+  apply (induct xs arbitrary: x)
+   apply auto
+  done
+
+lemma "length_fold xs = length xs"
+  apply (induct xs)
+   apply (auto simp: length_fold_def length_fold_sum)
+  done
+
+lemma "length_foldr xs = length xs"
+  apply (induct xs)
+   apply (auto simp: length_foldr_def length_fold_sum)
+  done
+
+
+(* list slices *)
+fun slice:: "'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list" where
+  "slice [] n l = []" |
+  "slice xs 0 0 = []" |
+  "slice (x#xs) 0 l = Cons x (slice xs 0 (l-1))" |
+  "slice (x#xs) n l = slice xs (n-1) l"
+
+thm slice.induct
+
+value "slice [0, 1 ,2 ,3 ,4 ,5 ,6::int] 0 1"
+value "slice [0 ,1 ,2 ,3 ,4 ,5 ,6 ::int] 2 10"
+value "slice [0 ,1 ,2 ,3 ,4 ,5 ,6 ::int] 10 10" 
+
+(* show that concatenation of two adjacent slices can be expressed as a single slice *)
+lemma l1: "(slice xs s l1) @ slice xs (s + l1) l2 = slice xs s (l1 + l2)"
+  apply (induction xs s l1 rule: slice.induct)
+  apply (auto)
+  done
+
+(* slice of a distinct is distinct *)
+
+lemma "ldistinct xs \<Longrightarrow> ldistinct (slice xs s l)"
+  apply (induct xs arbitrary: s l rule: ldistinct.induct)
+  apply (auto simp: l2)
+  done

Functional Data Structures/homework02/Submission.thy

@@ -0,0 +1,94 @@
+theory Submission
+  imports Defs
+begin
+
+(* distinct *)
+fun contains :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"  
+  where
+  "contains x [] = False" |
+  "contains y (x#xs) = (if x = y then True else contains y xs)"
+
+fun ldistinct:: "'a list \<Rightarrow> bool" 
+  where
+  "ldistinct [] = True" |
+  "ldistinct (x#xs) = ((~ contains x xs) \<and> (ldistinct xs))"
+
+thm contains.induct
+thm ldistinct.induct
+
+lemma lemma1: "contains x (xs @ [a]) = contains x ([a] @ xs)"
+  apply (induction xs)
+   apply (auto)
+  done
+
+lemma lemma2: "contains x (rev xs) = contains x xs"
+  apply (induct xs)
+  apply (auto simp: lemma1)
+  done 
+
+lemma lemma3: "ldistinct (xs @ [x]) = ldistinct ([x] @ xs)"
+  apply (induct xs)
+   apply (auto simp: lemma1)
+  done
+
+lemma ldistinct_rev: "ldistinct (rev xs) \<longleftrightarrow> ldistinct xs"
+  apply (induct xs)
+   apply (auto simp: lemma3 lemma2)
+  done 
+
+
+(* folding *)
+thm fold.simps
+thm foldr.simps
+
+fun a::  "'a ⇒ nat ⇒ nat" where
+  "a n m = m + 1"
+
+definition length_fold:: "'a list ⇒ nat" where
+  "length_fold x ≡ fold (a) x 0"
+
+definition length_foldr:: "'a list ⇒ nat" where
+  "length_foldr x ≡ foldr (a) x 0" 
+
+lemma length_fold_sum: "fold a xs x = length xs + x"
+  apply (induct xs arbitrary: x)
+   apply auto
+  done
+
+lemma length_fold: "length_fold xs = length xs"
+  apply (induct xs)
+   apply (auto simp: length_fold_def length_fold_sum)
+  done
+
+lemma length_foldr: "length_foldr xs = length xs"
+  apply (induct xs)
+   apply (auto simp: length_foldr_def length_fold_sum)
+  done
+
+
+(* slicing *)
+fun slice:: "'a list ⇒ nat ⇒ nat ⇒ 'a list" where
+  "slice [] n l = []" |
+  "slice xs 0 0 = []" |
+  "slice (x#xs) 0 l = Cons x (slice xs 0 (l-1))" |
+  "slice (x#xs) n l = slice xs (n-1) l"
+
+thm slice.induct
+
+lemma slice_append: "slice xs s l1 @ slice xs (s+l1) l2 = slice xs s (l1+l2)"
+  apply (induction xs s l1 rule: slice.induct)
+  apply (auto)
+  done
+
+lemma contain_slice: "contains x (slice xs s l) \<Longrightarrow> contains x xs"
+  apply (induct xs s l rule: slice.induct)
+  apply auto
+  done
+
+lemma ldistinct_slice: "ldistinct xs \<Longrightarrow>  ldistinct (slice xs s l)"
+  apply (induct xs s l rule: slice.induct)
+  apply (auto simp: contain_slice)
+  done
+
+end
+