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

theory Exercise10
  imports 
    Main
    "HOL-Library.Code_Target_Numeral" 
begin

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

text \<open>Consider the following function definition\<close>

fun slow_fun :: "nat \<Rightarrow> nat" where
  "slow_fun n = (if n < 2 then 5 * n else 2 * slow_fun (n - 2) + slow_fun (n - 1))" 

text \<open>Execution is quite slow because of the overlapping recursion. An input of 42
  already takes some seconds to compute (depending on the machine).\<close>
value (code) "slow_fun 42"


text \<open>In this exercise we aim at developing a program refinement, 
  such that execution of @{const slow_fun} is efficient
  and such that both @{term "slow_fun 42"} and @{term "slow_fun 420"}
  can be evaluated within a second. Clearly,
  there is a smarter way to compute @{const slow_fun}, e.g., by computing the values
  @{term "slow_fun i"} from i = 0 up to n.\<close>


text \<open>Task 1 (2 points) - Define an efficient algorithm to compute @{const slow_fun}.
  Here, you might require a manual termination proof, but at this point no
  soundness proof is required. State a tentative code-equation for
  @{const slow_fun}, such that @{command quickcheck} is not able to find 
  counter-examples, i.e., your implementation must be correct w.r.t. testing.\<close>


lemma [code]: "slow_fun n = undefined ''tentative code''" 
  quickcheck[expect = no_counterexample]
  oops


text \<open>Task 2 (3 points) - Prove soundness of your efficient implementation,
  and in particular verify the tentative code equation of task 1.\<close>


lemma [code]: "slow_fun n = Code.abort (STR ''todo'') (\<lambda> _. slow_fun n)"
  by simp

value (code) "slow_fun 42" 
value (code) "slow_fun 420" 




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

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 flattening a tree into 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. Flattening 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 flattening 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 flatten_main :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a list" where
  "flatten_main d (Node x ts) = (x # (let n = length ts in 
      if n = 0 then [] 
      else flatten_main (d + 1) (ts ! sel d n)))" 

definition flatten :: "'a tree \<Rightarrow> 'a list" where 
  "flatten = flatten_main 0" 
end

text \<open>Task 1 (3 points) - 
   Implement solution 2 of lecture 10 to get an executable version of @{const flatten},
   called \<open>flatten'\<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 flatten' :: "selfun \<Rightarrow> 'a tree \<Rightarrow> 'a list" 
  where "flatten' = undefined ''todo''" 

export_code flatten' in Haskell module_name Should_Succeed_And_Be_Sensible

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

definition "flatten_specific = flatten (\<lambda> d n. n - 1 - d)" 

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

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

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

text \<open>Task 3 (1 point) - Is it possible to write an executable function
  @{term flatten_impl} such that @{term "flatten sel_fun = flatten_impl sel_fun"}
  whenever @{term sel_fun} is a proper selection function?

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

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

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

export_code flatten_impl in Haskell module_name Flatten
  (* this should succeed and be a sensible implementation *)


end