commit to push

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

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

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

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

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

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

02/ex0202.thy

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

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