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

theory Exercise01
  imports 
    Main
begin

declare [[names_short]]

text \<open>Binary relations encoded as predicates.\<close>

type_synonym 'a rel = "'a \<Rightarrow> 'a \<Rightarrow> bool" 

text \<open>Definition of transitive closure from the lecture\<close>

definition "trans_cl (R :: 'a rel) a b = 
  (\<exists> (f :: nat \<Rightarrow> 'a) (n :: nat). f 0 = a \<and> f n = b \<and> n \<noteq> 0 \<and> 
    (\<forall> i. i < n \<longrightarrow> R (f i) (f (i + 1))))" 

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

text \<open>Specify a predicate for sub-relation, i.e., intuitively  
    @{term "subrel R S"} should encode @{term "R \<subseteq> S"}.\<close>

definition subrel :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> bool" where
  "subrel R S = undefined"  

text \<open>Prove the following lemma on paper, using natural deduction, box-proofs,
  or any other similar mechanism. Be informal at steps where you don't know how
  the exact reasoning rules looks like. You may treat the constants @{const subrel}
  and @{const trans_cl} as if they were just abbreviations.\<close>

lemma "subrel R (trans_cl R)" oops


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

datatype 'a list = Nil | Cons 'a "'a list" 

definition test_list :: "nat list" where
  "test_list = Cons 2 (Cons 4 (Cons 9 (Cons 5 (Cons 3 Nil))))" 

text \<open>Define a function that implements insertion sort. 
  Of course, you may add auxiliary functions.\<close>

fun ins_sort :: "'a :: linorder list \<Rightarrow> 'a list" where
  "ins_sort xs = xs" (* clearly, this is wrong *)

text \<open>With "value" we can evaluate (executable) expressions. So the following
  line applies insertion sort on the test-list.\<close>
value "ins_sort test_list" 


section \<open>Exercise 3 -- 4 points\<close>

text \<open>The file Demo01.thy from the lecture contains a sortedness-predicate.\<close>

fun is_sorted :: "'a :: linorder list \<Rightarrow> bool" where
  "is_sorted (Cons x (Cons y ys)) = (x \<le> y \<and> is_sorted (Cons y ys))"
| "is_sorted _ = True" 

text \<open>just a test: a correct implementation 
    of @{const ins_sort} should deliver True\<close>
value "is_sorted (ins_sort test_list)" 

text \<open>The following (unproven) lemma is useful, but it does not specify that 
  the @{const ins_sort} algorithm does not drop or invent any elements.
  E.g., if you would have defined @{term "ins_sort xs = Nil"}, then 
  the following lemma is trivially satisfied.\<close>
lemma "is_sorted (ins_sort xs)" 
  oops

text \<open>Specify a property that all list-elements are contained in some other list (ignoring duplicates)
    and then formulate a lemma that @{const ins_sort} preserves the set of elements.
    The auxiliary property @{term sub_list} (and other auxiliary property)
    might be useful. Here, @{term "sub_list xs ys"} should be true iff all elements
    of @{term xs} also occur in @{term ys}.\<close>

fun sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
  "sub_list xs ys = undefined ''TODO''" 

lemma "TODO: specify that ins_sort preserves elements" 
  oops

end