(* CS576, MP 1 *) (* Your name goes here! *) (* Score: ? / 8 *) theory mp1 imports Main begin datatype 'a tree = Leaf 'a | Node "'a tree" 'a "'a tree" text {* Define a function "root_label" that gives the label at the root of a tree given by the dataype above. You should be able to prove the two subsequent theorems about "root_label" *} definition root_label :: "'a tree \ 'a" where "root_label tree \ undefined (* You should replace this. *)" text {* Remove sorry from each of the lemmas below and give a proof. You should use simplification. You can add a theorem thm to the rewrites used by the method simp in a proof with proof (simp add: thm) The above definition generates a theorem called root_label_def *} (* 1 pt *) lemma root_label_Leaf: "root_label (Leaf x) = x" sorry (* 1 pt *) lemma root_label_Node: "root_label (Node left x right) = x" sorry primrec mirror :: "'a tree \ 'a tree" where "mirror (Leaf x) = (Leaf x)" | "mirror (Node xs x ys) = Node (mirror ys) x (mirror xs)" text{* Remove sorry from the lemma below and give a proof. You can perform case analysis on a term tm in a proof by proof (case_tac tm) *} (* 2 pts *) lemma root_label_mirror: "root_label (mirror tree) = root_label tree" sorry primrec flatten :: "'a tree \ 'a list" where "flatten (Leaf x) = [x]" | "flatten (Node xs x ys) = (flatten xs) @ (x # (flatten ys))" text {* Remove sorry from each of the lemmas below and give a proof. You can perform induction by proof (induct_tac tm) where you replace tm by the expression (typically a variable) over which you are inducting. You can modify expressions by equational rewriting using theorems declared as simplifications (such as the equations given by primrec) with proof simp When there are no more goals left, you can finish the proof with qed *} (* 2 pts *) lemma mirror_mirror: "mirror(mirror t) = t" sorry (* 2 pts *) lemma flatten_mirror: "flatten(mirror t) = rev(flatten t)" sorry text {* The function count should return the number of labels in a tree. The count of Leaf is 1. The count of a Node is one more than the sum of the count of the left and right subtrees. Define count by primitive recursion, in a manner similar to what was done with mirror and flatten. *} (* 2 pts *) (* primrec ... *) (* 2 pts *) lemma count_mirror: "count (mirror t) = count t" sorry end