Basic functional programming

Definitions File

theory Defs
imports Main 
begin

datatype 'a binTree= Leaf | Node 'a "'a binTree" "'a binTree"

end

Template File

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

Check File

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