chapter \<open>Exercise Sheet -- Week 10\<close>

theory Exercise10
  imports 
    Main
begin

text \<open>Consider rose trees, i.e., trees where each node might have arbitrarily many
  children.\<close>

datatype 'a tree = Node 'a "'a tree list" 

text \<open>Here is a function to generate some rose tree from a number.\<close>

fun example_tree :: "nat \<Rightarrow> nat tree" where
  "example_tree x = Node x (map example_tree [y . y \<leftarrow> [0 ..< x], \<not> (y dvd x)])" 

value (code) "example_tree 13" 

text \<open>In this exercise we are interested in traversing a tree and return a list, where
  a selection function is used to determine which child to select. Here, the
  selection may depend on the current depth \<open>d\<close> of the tree 
  as well as on the number \<open>n\<close> of children. Traversing stops if there are no children.

  Clearly, the selection must be within range. This is modeled via the following context.\<close>

context
  fixes sel :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
  assumes sel_in_range: "\<And> d n. n \<noteq> 0 \<Longrightarrow> sel d n < n" 
begin

text \<open>Termination of the traversal algorithm can be shown with the help of 
  @{thm[source] sel_in_range}.\<close>

lemma [termination_simp]: "ts \<noteq> [] \<Longrightarrow> 
  size (ts ! sel d (length ts)) < Suc (size_list size ts)" 
  using sel_in_range[of "length ts" d]
  using not_less_eq nth_mem size_list_estimation by fastforce

fun traverse_main :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a list" where
  "traverse_main d (Node x ts) = (x # (let n = length ts in 
      if n = 0 then [] 
      else traverse_main (d + 1) (ts ! sel d n)))" 

definition traverse :: "'a tree \<Rightarrow> 'a list" where 
  "traverse = traverse_main 0" 
end



section \<open>Exercise 1 -- 5 points\<close>

text \<open>In this exercise we will consider solution 2 of lecture to get an executable version.\<close>

text \<open>Task 1 (2 points) - 
   Implement solution 2 of lecture 10 to get an executable version of @{const traverse},
   called \<open>traverse'\<close>.\<close>

typedef selfun = "{sel :: nat \<Rightarrow> nat \<Rightarrow> nat. (\<forall> d n. n \<noteq> 0 \<longrightarrow> sel d n < n)}" 
  sorry (* remove this sorry *)


definition traverse' :: "selfun \<Rightarrow> 'a tree \<Rightarrow> 'a list" 
  where "traverse' = undefined ''todo''" 

export_code traverse' in Haskell module_name Traverse_Prime
(* this should succeed and be sensible *)

text \<open>Task 2 (1 point) - We now consider a specific selection function.\<close>

definition "traverse_specific = traverse (\<lambda> d n. n - 1 - d)" 

text \<open>Provide a code equation for @{const traverse_specific} such that the
  following proof "by eval" is accepted.\<close>

lemma [code]: "traverse_specific = undefined ''TODO''" sorry

lemma "traverse_specific (example_tree 13) = [13, 12, 10, 7, 3, 0]" by eval

text \<open>Task 3 (2 points) - Is it possible to write an executable function
  @{term traverse_impl} which is based on @{const traverse'},
  such that @{term "traverse sel_fun = traverse_impl sel_fun"}
  whenever @{term sel_fun} is a proper selection function?

  Either define @{term traverse_impl} correspondingly or argue why this is not possible.\<close>

definition traverse_impl :: "(nat \<Rightarrow> nat \<Rightarrow> nat) \<Rightarrow> 'a tree \<Rightarrow> 'a list" where
  "traverse_impl = undefined ''is it possible?''" 

lemma traverse_impl: assumes "\<And> d n. n \<noteq> 0 \<Longrightarrow> sel d n < n"
  shows "traverse_impl sel tree = traverse sel tree" 
  (* possible? *)
  oops

export_code traverse_impl in Haskell module_name Traverse_Impl
(* this should succeed and be a sensible implementation *)



section \<open>Exercise 2 - 5 points\<close>

text \<open>Task 1 - 2.5 points\<close>

text \<open>Use solution 3 to implement @{const traverse}, i.e.,
  via @{command partial_function}. Of course you cannot just copy the
  definition of @{const traverse_main}, since that function is not 
  tail-recursive and also it uses pattern matching in left-hand sides.\<close>

partial_function (tailrec) traverse_main_pf :: "(nat \<Rightarrow> nat \<Rightarrow> nat) \<Rightarrow> _" where
  [code]: "traverse_main_pf sel = ''TODO''" 

definition traverse_pf :: "(nat \<Rightarrow> nat \<Rightarrow> nat) \<Rightarrow> 'a tree \<Rightarrow> 'a list" 
  where "traverse_pf sel t = undefined traverse_main_pf sel t" 

(* a simple sanity check should be accepted *)
value (code) "traverse_pf (\<lambda> d n. n - 1 - d) (example_tree 13)" 
lemma "traverse_pf (\<lambda> d n. n - 1 - d) (example_tree 13) = [13, 12, 10, 7, 3, 0]" by eval

text \<open>Task 2 - 2.5 points\<close>

text \<open>Prove soundness of your implementation.\<close>

lemma traverse_pf: assumes "\<And> d n. n \<noteq> 0 \<Longrightarrow> sel d n < n"
  shows "traverse_pf sel tree = traverse sel tree"
  sorry

end