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 sorry

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

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

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

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>


(* existing formalization about trees from Lecture 09 and Exercise 08 *)

datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree" 

fun set_t :: "'a tree \<Rightarrow> 'a set" where
  "set_t Leaf = {}" 
| "set_t (Node l x r) = set_t l \<union> {x} \<union> set_t r" 

inductive ordered :: "'a :: linorder tree \<Rightarrow> bool" where
  oLeaf: "ordered Leaf" 
| oNode: "ordered l \<Longrightarrow> ordered r 
  \<Longrightarrow> Ball (set_t l) (\<lambda> y. y < x)
  \<Longrightarrow> Ball (set_t r) (\<lambda> y. y > x)
  \<Longrightarrow> ordered (Node l x r)" 

fun member:: "'a :: linorder \<Rightarrow> 'a tree \<Rightarrow> bool" where
  "member x Leaf = False" 
| "member y (Node l x r) = (if x = y then True else if y < x then member y l else member y r)" 

lemma member_correct: "ordered t \<Longrightarrow> member x t = (x \<in> set_t t)" 
  by (induction rule: ordered.induct, auto)

fun insert_t :: "'a :: linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
  "insert_t y Leaf = Node Leaf y Leaf" 
| "insert_t y (Node l x r) = (if x = y then Node l x r else 
      if y < x then Node (insert_t y l) x r else Node l x (insert_t y r))" 

lemma set_insert_t[simp]: "set_t (insert_t x t) = insert x (set_t t)" 
  by (induct t, auto)

lemma ordered_insert_t: "ordered t \<Longrightarrow> ordered (insert_t x t)" 
  by (induction rule: ordered.induct, auto intro!: oNode oLeaf)

fun delete_right :: "'a :: linorder tree \<Rightarrow> 'a tree \<times> 'a" where
  "delete_right (Node l x Leaf) = (l, x)" 
| "delete_right (Node l x r) = (case delete_right r of (r', y) \<Rightarrow> (Node l x r', y))" 

fun delete :: "'a :: linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
  "delete x Leaf = Leaf" 
| "delete x (Node l y r) = (if x < y then Node (delete x l) y r
      else if x > y then Node l y (delete x r)
      else if l = Leaf then r else
        case delete_right l of (l',z) \<Rightarrow> Node l' z r)" 

lemma delete_right: "ordered t \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> delete_right t = (t', x) \<Longrightarrow>
  ordered t' \<and> set_t t = insert x (set_t t') \<and> Ball (set_t t') (\<lambda> y. y < x)" 
proof (induction t arbitrary: t' x rule: ordered.induct)
  case (oNode l r x t' y)
  thus ?case
  proof (cases r)
    case Leaf
    thus ?thesis using oNode by auto
  next
    case Node
    from oNode.prems[unfolded Node, simplified, folded Node]
    obtain r' where dr: "delete_right r = (r',y)" and t': "t' = Node l x r'" 
      by (cases "delete_right r", auto)
    from Node have r: "r \<noteq> Leaf" by auto
    from oNode.IH(2)[OF r dr] oNode.hyps
    show ?thesis unfolding t'
      by (auto intro: ordered.intros)
  qed
qed auto

lemma delete: "ordered t \<Longrightarrow> ordered (delete x t) \<and> set_t (delete x t) = set_t t - {x}" 
proof (induction t rule: ordered.induct)
  case (oNode l r y)
  consider (LT) "x < y" | (EQ) "x = y" "l = Leaf" | (EQ2) "x = y" "l \<noteq> Leaf" | (GT) "x > y" 
    by fastforce
  then show ?case
  proof cases
    case LT
    hence id: "delete x (Node l y r) = Node (delete x l) y r" by simp
    from oNode.IH(1) 
    show ?thesis using oNode.hyps LT unfolding id
      by (auto intro: ordered.intros)
  next
    case EQ
    then show ?thesis using oNode.hyps by auto
  next
    case EQ2
    obtain l' z where del: "delete_right l = (l',z)" by force
    from del EQ2 have id: "delete x (Node l y r) = Node l' z r" by auto
    from delete_right[OF _ EQ2(2) del] oNode.hyps
    have "ordered l' \<and> set_t l = insert z (set_t l') \<and> (\<forall>y\<in>set_t l'. y < z)" by auto
    with oNode.hyps EQ2 show ?thesis unfolding id
      by (auto intro!: ordered.intros)
  next
    case GT
    hence id: "delete x (Node l y r) = Node l y (delete x r)" by auto
    from oNode.IH(2) 
    show ?thesis using oNode.hyps GT unfolding id
      by (auto intro: ordered.intros)
  qed
qed (auto intro: ordered.intros)


typedef (overloaded) ('a :: linorder) otree = "{t :: 'a tree. ordered t}" 
  by (intro exI[of _ Leaf], auto intro: ordered.intros)
  
setup_lifting type_definition_otree

lift_definition empty_o :: "('a :: linorder) otree" is Leaf
  by (auto intro: ordered.intros)

lift_definition insert_o :: "'a :: linorder \<Rightarrow> 'a otree \<Rightarrow> 'a otree" is insert_t
  by (rule ordered_insert_t)

lift_definition delete_o :: "'a :: linorder \<Rightarrow> 'a otree \<Rightarrow> 'a otree" is delete 
  using delete by blast

lift_definition member_o :: "'a :: linorder \<Rightarrow> 'a otree \<Rightarrow> bool" is member .

lift_definition set_o :: "'a :: linorder otree \<Rightarrow> 'a set" is set_t .

lemma empty_o[simp]: "set_o empty_o = {}" 
  apply transfer 
  by auto

lemma insert_o[simp]: "set_o (insert_o x t) = insert x (set_o t)" 
  apply transfer
  using set_insert_t by auto

lemma delete_o[simp]: "set_o (delete_o x t) = (set_o t) - {x}" 
  apply transfer
  using delete by auto

lemma member_o[simp]: "member_o x t = (x \<in> set_o t)" 
  apply transfer
  using member_correct by auto


fun flatten :: "'a tree \<Rightarrow> 'a list" where
  "flatten Leaf = []" 
| "flatten (Node l x r) = flatten l @ x # flatten r" 

lemma flatten_set[simp]: "set (flatten t) = set_t t"  
  by (induction t; fastforce) 
(* end of existing formalization *)



text \<open>In this exercise, we consider data structures that store additional information.
  As a concrete example, we consider a type of pairs (n,t) where n is a natural number,
  t is an ordered tree, and n is exactly the size of the tree, i.e., the cardinality of
  the set of elements in the tree. In this way, the size of the tree can be accessed in
  constant time.\<close>

typedef (overloaded) ('a :: linorder) ctree = "{ (n,t) | (n :: nat) (t :: 'a otree). n = card (set_o t)}" 
  sorry

text \<open>Task 1 -- 1 point

Prove that the type is non-empty, define the following two functions:
- \<open>set_c :: 'a :: linordered ctree \<Rightarrow> 'a set\<close> returns the elements of the tree as a set
- \<open>card_c :: 'a :: linordered ctree \<Rightarrow> nat\<close> returns the stored size of the tree

and then prove that \<open>card_c\<close> is correct.

Hint: \<open>lift_definition\<close> accepts arbitrary expressions, e.g., \<open>\<lambda> (n,t). something\<close>.
\<close>

setup_lifting type_definition_ctree

consts set_c :: "'a :: linorder ctree \<Rightarrow> 'a set" (* replace by some proper definition *)

consts card_c :: "'a :: linorder ctree \<Rightarrow> nat" (* replace by some proper definition *)

lemma card_c: "card_c t = card (set_c t)" sorry


text \<open>Task 2 -- 2 points

Lift \<open>empty_o\<close>, \<open>insert_o\<close>, \<open>delete_o\<close> and \<open>member_o\<close> from \<open>'a otree\<close> to \<open>'a ctree\<close>
and prove correctness of your implementations. For the reasoning about cardinalities,
it might be useful to also prove that all sets that are represented by a tree are finite.
\<close>

lemma finite_set_o[simp]: "finite (set_o t)" sorry


consts insert_c :: "'a :: linorder \<Rightarrow> 'a ctree \<Rightarrow> 'a ctree" (* replace by some proper definition *)

consts delete_c :: "'a :: linorder \<Rightarrow> 'a ctree \<Rightarrow> 'a ctree" (* replace by some proper definition *)

consts empty_c :: "'a :: linorder ctree" (* replace by some proper definition *)

consts member_c :: "'a :: linorder \<Rightarrow> 'a ctree \<Rightarrow> bool" (* replace by some proper definition *)

lemma empty_c: "set_c empty_c = {}" sorry

lemma insert_c: "set_c (insert_c x t) = insert x (set_c t)" sorry

lemma delete_c: "set_c (delete_c x t) = set_c t - {x}" sorry

lemma member_c: "member_c x t = (x \<in> set_c t)" sorry


text \<open>Task 3 -- 2 points

Now exploit the efficient access to the sizes by formalizing a union-operation
on trees that works as follows: Given two trees, the algorithm first selects the smaller one, 
flattens that into a list, and then iteratively inserts all elements from the list into the larger tree.

Hint: Whereas the flatten-function must first be lifted to work on \<open>'a ctree\<close>, all other functionality
can stay on the abstract level and just use the abstract existing operations, i.e., by using 
definition principles like \<open>fun\<close> and \<open>definition\<close>, but not \<open>lift_definition\<close>.
\<close>

consts flatten_c :: "'a :: linorder ctree \<Rightarrow> 'a list" (* replace by some proper definition *)

lemma flatten_c: "set (flatten_c t) = set_c t" sorry

consts union_c :: "'a :: linorder ctree \<Rightarrow> 'a ctree \<Rightarrow> 'a ctree" (* replace by some proper definition *)

lemma union_c: "set_c (union_c t1 t2) = set_c t1 \<union> set_c t2" 
  sorry

end