(* CS576, MP 2 *)

theory mp2
imports mp1
begin

text{* Uses the type of tree defined in mp1 *}
(*
lemma count_length:
fixes t
shows "count t = length (flatten t)"
apply (induct_tac t)
 apply simp
apply simp
done
*)

lemma count_length:
fixes t
shows "count t = length (flatten t)"
proof (induct_tac t)
 show "count Tip = length (flatten Tip)"
 by simp
 next
 fix left_tree right_tree v
 assume LeftIndHyp: "count (left_tree\<Colon> 'a tree) = length (flatten left_tree)"
 assume RightIndHyp: "count (right_tree\<Colon> 'a tree) = length (flatten right_tree)"
 from LeftIndHyp RightIndHyp
 show "count (Node left_tree v right_tree) = 
       length (flatten (Node left_tree v right_tree))"
 by simp
qed

text{* Define a functional

tree_map :: "('a => 'b) => 'a tree => 'b tree"

       to apply a function to the value in every node in a tree.  The
       file will not load past here until you complete the
       definition. *}

primrec tree_map :: "('a => 'b) => 'a tree => 'b tree" where
"tree_map f Tip = Tip" |
"tree_map f (Node l x r) = Node (tree_map f l) (f x) (tree_map f r)"

(*
lemma flatten_tree_map:
fixes f t
shows "flatten(tree_map f t) = map f (flatten t)"
apply (induct_tac t)
 apply simp
apply simp
done
*)

lemma flatten_tree_map:
fixes f t
shows "flatten(tree_map f t) = map f (flatten t)"
proof (induct_tac t)
 show "flatten(tree_map f Tip) = map f (flatten Tip)"
 by simp
 next
 fix left_tree right_tree v
 assume LeftIndHyp: "flatten(tree_map f left_tree) =
                     map f (flatten left_tree)"
 assume RightIndHyp: "flatten(tree_map f right_tree) =
                     map f (flatten right_tree)"
 from LeftIndHyp RightIndHyp
 show "flatten(tree_map f (Node left_tree v right_tree)) =
                     map f (flatten (Node left_tree v right_tree))"
 by simp
qed

text{* Give a primitive recursive definition of 

itflatten :: "'a tree => 'a list => 'a list"

       which is to add the elements of a given tree to the front of a
       given list such that the lemma below will be true.  Do not use
       @ or flatten in your definition. *}

primrec itflatten :: "'a tree => 'a list => 'a list" where
"itflatten Tip list = list" |
"itflatten (Node left_tree label right_tree) list =
  itflatten left_tree (label # itflatten right_tree list)"

lemma [simp]:
fixes t list
shows "\<forall> list. itflatten t list = (flatten t) @ list"
proof (induct_tac t)
 show "\<forall> list. itflatten Tip list = (flatten Tip) @ list"
 by simp
 next
 fix left_tree right_tree v
 assume LeftIndHyp: "\<forall> list. itflatten (left_tree\<Colon>'a tree) list =
                            (flatten left_tree) @ list"
 assume RightIndHyp: "\<forall> list. itflatten (right_tree\<Colon>'a tree) list =
                            (flatten right_tree) @ list"
 from LeftIndHyp RightIndHyp
 show "\<forall> list. itflatten (Node left_tree v right_tree) list =
                            (flatten (Node left_tree v right_tree)) @ list"
 by simp
qed

text{* Hint: to prove this theorem, you will probably want to prove a more
 general lemma first *}
lemma
fixes t
shows "itflatten t [] = flatten t"
by simp

end