I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports Main begin datatype 'a binTree= Leaf | Node 'a "'a binTree" "'a binTree" end

theory Submission imports Defs begin (* Program here the delete function *) (* delete all occurences of an element in a list *) fun delete:: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where "delete x l = undefined" (* Tests to pass *) lemma testDel1: "delete (0::nat) [0,1,2,0,1,2] = [1,2,1,2]" sorry lemma testDel2: "delete (1::nat) [0,1,2,0,1,2] = [0,2,0,2]" sorry lemma testDel3: "delete (4::nat) [0,1,2] = [0,1,2]" sorry (* Program here the expand function *) fun expand:: "'a list \<Rightarrow> 'a list" where "expand l = undefined" (* Tests to pass *) lemma testExpand0: "expand [] = []" sorry lemma testExpand1: "expand [1] = [1,1]" sorry lemma testExpand2: "expand [1,2,3,4,5] = [1,2,3,4,5,5,4,3,2,1]" sorry (* Program here the split1 function *) (* Splits a list 'l' into two sublists, where the first list contains the elements of 'l' that occur at an even position, and the second sublist contains the elements of 'l' that occur at an odd position. Positions start at 0. *) fun split1:: "'a list \<Rightarrow> ('a list * 'a list)" where "split1 l = undefined" (* Tests to pass *) lemma split1Test0: "split1 [] = ([],[])" sorry lemma split1Test1: "split1 [(1::nat)] = ([1],[])" sorry lemma split1Test2: "split1 [(1::nat),2] = ([1],[2])" sorry lemma split1Test3: "split1 [(1::nat),2,6,8,10] = ([1,6,10],[2,8])" sorry (* Program here the split2 function *) (* Splits a list 'l' into two lists such that the first list is a prefix of 'l' that ends with the first occurrence of 'e' in 'l', and the second list is the remainding list. *) fun split2:: "'a \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a list)" where "split2 e l = undefined" (* Tests to pass *) lemma split2Test0: "split2 e [] = ([],[])" sorry lemma split2Test1: "split2 1 [(1::nat)] = ([1],[])" sorry lemma split2Test2: "split2 1 [(1::nat),2] = ([1],[2])" sorry lemma split2Test3: "split2 1 [(2::nat),1] = ([2,1],[])" sorry lemma split2Test4: "split2 6 [(1::nat),2,6,8,10] = ([1,2,6],[8,10])" sorry (* Program here the split3 function *) (* Splits a list into a prefix and the remaining suffix, such that the length of the prefix is half the length of the whole list (if the length of the whole list is odd, then the length of the prefix must be one plus half of the length). *) fun split3:: "'a list \<Rightarrow> ('a list * 'a list)" where "split3 l = undefined" (* Tests to pass *) lemma split3Test0: "split3 [] = ([],[])" sorry lemma split3Test1: "split3 [(1::nat)] = ([1],[])" sorry lemma split3Test2: "split3 [(1::nat),2] = ([1],[2])" sorry lemma split3Test2b: "split3 [(1::nat),1,1,1] = ([1,1],[1,1])" sorry lemma split3Test3: "split3 [(1::nat),2,6,8,10] = ([1,2,6],[8,10])" sorry lemma split3Test4: "split3 [(1::nat),2,6,8,10,12] = ([1,2,6],[8,10,12])" sorry (* Program here the zip function *) (* Merges two lists 'l1' and 'l2' into a single list by taking the first element of 'l1', then the first element of 'l2', then the second element of 'l1', then the second element of 'l2', etc. *) (* the zip function can either be defined using 'fun' or 'function' *) fun zip:: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where "zip l1 l2 = undefined" (* Tests to pass *) lemma testZip1: "zip [(1::nat),3,5,7,9,11,13] [2,4,6,8] = [1,2,3,4,5,6,7,8,9,11,13]" sorry lemma testZip2: "zip [2,4,6,8] [(1::nat),3,5,7,9,11,13] = [2,1,4,3,6,5,8,7,9,11,13]" sorry (* Program here the sumTree function *) (* Sum of all naturals of a tree *) fun sumTree:: "nat binTree \<Rightarrow> nat" where "sumTree t = undefined" (* Tests to pass *) lemma testSumTree0: "(sumTree (Node (1::nat) (Node 2 (Node 4 Leaf Leaf) Leaf) Leaf)) = 7" sorry lemma testSumTree1: "(sumTree (Node (1::nat) (Node 2 (Node 4 Leaf Leaf) (Node 10 Leaf Leaf)) (Node 2 (Node 4 Leaf Leaf) (Node 10 Leaf Leaf)))) = 33" sorry (* Program here the prefix function *) (* prefix traversal of binary tree *) fun prefix:: "'a binTree \<Rightarrow> 'a list" where "prefix t = undefined" (* Tests to pass *) lemma testPrefix0: "prefix (Node (1::nat) Leaf (Node 2 Leaf Leaf)) = [1,2]" sorry lemma testPrefix1: "prefix (Node (1::nat) (Node 2 (Node 4 Leaf Leaf) (Node 10 Leaf Leaf)) (Node 2 (Node 4 Leaf Leaf) (Node 10 Leaf Leaf))) = [1,2,4,10,2,4,10]" sorry end

theory Check imports Submission begin (* delete *) lemma "delete (0::nat) [0,1,2,0,1,2] = [1,2,1,2]" by (rule Submission.testDel1) lemma "delete (1::nat) [0,1,2,0,1,2] = [0,2,0,2]" by (rule Submission.testDel2) lemma "delete (4::nat) [0,1,2] = [0,1,2]" by (rule Submission.testDel3) (* expand *) lemma "expand [] = []" by (rule Submission.testExpand0) lemma "expand [1] = [1,1]" by (rule Submission.testExpand1) lemma "expand [1,2,3,4,5] = [1,2,3,4,5,5,4,3,2,1]" by (rule Submission.testExpand2) (* split1 *) lemma "split1 [] = ([],[])" by (rule Submission.split1Test0) lemma "split1 [(1::nat)] = ([1],[])" by (rule Submission.split1Test1) lemma "split1 [(1::nat),2] = ([1],[2])" by (rule Submission.split1Test2) lemma "split1 [(1::nat),2,6,8,10] = ([1,6,10],[2,8])" by (rule Submission.split1Test3) (* split2 *) lemma "split2 e [] = ([],[])" by (rule Submission.split2Test0) lemma "split2 1 [(1::nat)] = ([1],[])" by (rule Submission.split2Test1) lemma "split2 1 [(1::nat),2] = ([1],[2])" by (rule Submission.split2Test2) lemma "split2 1 [(2::nat),1] = ([2,1],[])" by (rule Submission.split2Test3) lemma "split2 6 [(1::nat),2,6,8,10] = ([1,2,6],[8,10])" by (rule Submission.split2Test4) (* split3 *) lemma "split3 [] = ([],[])" by (rule Submission.split3Test0) lemma "split3 [(1::nat)] = ([1],[])" by (rule Submission.split3Test1) lemma "split3 [(1::nat),2] = ([1],[2])" by (rule Submission.split3Test2) lemma "split3 [(1::nat),1,1,1] = ([1,1],[1,1])" by (rule Submission.split3Test2b) lemma "split3 [(1::nat),2,6,8,10] = ([1,2,6],[8,10])" by (rule Submission.split3Test3) lemma "split3 [(1::nat),2,6,8,10,12] = ([1,2,6],[8,10,12])" by (rule Submission.split3Test4) (* zip *) lemma "zip [(1::nat),3,5,7,9,11,13] [2,4,6,8] = [1,2,3,4,5,6,7,8,9,11,13]" by (rule Submission.testZip1) lemma "zip [2,4,6,8] [(1::nat),3,5,7,9,11,13] = [2,1,4,3,6,5,8,7,9,11,13]" by (rule Submission.testZip2) (* sumTree *) lemma "(sumTree (Node (1::nat) (Node 2 (Node 4 Leaf Leaf) Leaf) Leaf)) = 7" by (rule Submission.testSumTree0) lemma "(sumTree (Node (1::nat) (Node 2 (Node 4 Leaf Leaf) (Node 10 Leaf Leaf)) (Node 2 (Node 4 Leaf Leaf) (Node 10 Leaf Leaf)))) = 33" by (rule Submission.testSumTree1) (* prefix *) lemma "prefix (Node (1::nat) Leaf (Node 2 Leaf Leaf)) = [1,2]" by (rule Submission.testPrefix0) lemma testPrefix1: "prefix (Node (1::nat) (Node 2 (Node 4 Leaf Leaf) (Node 10 Leaf Leaf)) (Node 2 (Node 4 Leaf Leaf) (Node 10 Leaf Leaf))) = [1,2,4,10,2,4,10]" by (rule Submission.testPrefix1) end

Terms and Conditions