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

theory Exercise09
  imports 
    Main
begin

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

text \<open>As it was shown in the lecture, one can create a list type via
  pairs of a natural number (the length) and the index-function.\<close>

definition is_list :: "(nat \<times> (nat \<Rightarrow> 'a)) \<Rightarrow> bool" where 
  "is_list nf = (case nf of (n, f) \<Rightarrow> \<forall> i \<ge> n. f i = undefined)" 

typedef 'a List = "{nf :: (nat \<times> (nat \<Rightarrow> 'a)). is_list nf}" 
  by (auto simp: is_list_def)

text \<open>Task 1: Define the upcoming four standard operations on lists on the representative type.
  (1 point)\<close>

definition cons :: "'a \<Rightarrow> nat \<times> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<times> (nat \<Rightarrow> 'a)" where
  "cons = undefined" 

definition tail :: "nat \<times> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<times> (nat \<Rightarrow> 'a)" where
  "tail = undefined" 

definition head :: "nat \<times> (nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
  "head = undefined" 

definition nil :: "nat \<times> (nat \<Rightarrow> 'a)" where 
  "nil = undefined"  

text \<open>Task 2: Use the lifting package to lift all four definitions from the representative
  type to @{typ "'a List"}
  (1 point)\<close>

setup_lifting type_definition_List

lift_definition NIL :: "'a List" is undefined oops

lift_definition CONS :: "'a \<Rightarrow> 'a List \<Rightarrow> 'a List" is undefined oops

lift_definition TAIL :: "'a List \<Rightarrow> 'a List" is undefined oops

lift_definition HEAD :: "'a List \<Rightarrow> 'a" is undefined oops

text \<open>Task 3: Prove the upcoming three lemmas with the help of the transfer package. 
  These show that the list operations work as expected. (1 point)\<close>

lemma "HEAD (CONS x xs) = x" oops

lemma "TAIL (CONS x xs) = xs" oops

lemma "CONS x xs = CONS y ys \<longleftrightarrow> x = y \<and> xs = ys" oops

text \<open>Task 4: Prove one of the following properties, i.e., 
  either case-analysis or induction. (2 points)
  Of course you can also do both; the induction property is a bit more challenging.\<close>

lemma "xs = NIL \<or> (\<exists> y ys. xs = CONS y ys)" oops

lemma "P NIL \<longrightarrow> (\<forall> x xs. P xs \<longrightarrow> P (CONS x xs)) \<longrightarrow> P ys" oops


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

text \<open>In this exercise the aim is to define a type of distinct and ordered lists
  (which is enforced by @{term "sorted_wrt (<)"}),
  and these sets might then be used to implement operations on sets.\<close>


text \<open>Task 1: Complete the following definitions which should implement basic set
  operations via ordered lists. Here, in particular both the union-operation
  as well as the membership-test \<open>elem_ol\<close> should exploit the order. (3 points)\<close>

typedef (overloaded) ('a :: linorder) olist = "{ xs :: 'a list. sorted_wrt (<) xs}" 
  sorry

lift_definition empty_ol :: "'a :: linorder olist" is undefined sorry

lift_definition singleton_ol :: "'a :: linorder \<Rightarrow> 'a olist" is undefined sorry

lift_definition set_ol :: "'a :: linorder olist \<Rightarrow> 'a set" is undefined sorry

lift_definition union_ol :: "'a :: linorder olist \<Rightarrow> 'a olist \<Rightarrow> 'a olist" is undefined sorry

lift_definition elem_ol :: "'a :: linorder \<Rightarrow> 'a olist \<Rightarrow> bool" is undefined sorry

text \<open>Task 2: Prove the correctness of your implementation (2 points).\<close>

lemma empty_ol: "set_ol empty_ol = {}" sorry

lemma singleton_ol: "set_ol (singleton_ol x) = {x}" sorry

lemma union_ol: "set_ol (union_ol xs1 xs2) = set_ol xs1 \<union> set_ol xs2" sorry

lemma elem_ol: "elem_ol x xs = (x \<in> set_ol xs)" sorry

end