theory week05B_demo imports Main begin

(* Slide 3 *)
datatype 'a mylist = MyNil | MyCons 'a "'a mylist"

term MyNil   (* [] *)
term MyCons
term 1
term "MyCons (1::nat) MyNil" (* [1] *)

term "Cons (1::nat) Nil"

print_theorems

thm mylist.distinct
thm mylist.inject

(* Slide 4 *)
(* enumeration *)
datatype answer = Yes | No | Maybe

thm answer.distinct

(* mutual recursion *)
datatype even = EvenZero | EvenSucc odd
and odd = OddSucc even

print_theorems

thm even.inject
thm odd.inject

(* Slide 7: Datatypes under the hood *)
datatype 'a mylist2 = MyList2 "unit + ('a \<times> 'a mylist2)"

(* unit is a type with exactly one element: ()
    +
   sum types are defined as follows:
    data ('a,'b) Sum = Inl 'a | Inr 'b
   product types are tuples (cartesian products)
 *)
term Inl
term Inr

term MyNil
term "MyList2 (Inl ())"

term "MyCons x xs"
term "MyList2 (Inr (x,xs))"

(* Slides 8 & 9: Datatype Limitations *)
datatype 'a stream = Stream 'a "'a stream"

codatatype 'a stream = Stream 'a "'a stream"

datatype t = C "t \<Rightarrow> bool" | D (* negative occurrence of t *)

(*
  Issue:
   t \<Rightarrow> bool is isomorphic to t set
   (a set is uniquely characterised by its membership function)

  Cantor's theorem:
    for a set X, the cardinality of pow(X) is strictly larger than that of X.

  However, if the above datatype is admitted, because constructors are injective,
  we have an injective function from pow(t) to t, this function is C.

  And therefore, card(pow(t)) \<le> card t, contradicting Cantor's theorem.
 *)

datatype t = C "t set"

datatype t = C "bool \<Rightarrow> t" | D  (* positive occurrence of t *)

(* Slide 10: case construct introduced by datatype *)
term "case xs of [] \<Rightarrow> 1 | (x#xs) \<Rightarrow> x"

value "case 3#xs of [] \<Rightarrow> 1 | (x#xs) \<Rightarrow> x"

term list.case_list (* a function that returns its first argument for empty lists, and so on *)

term "list.case_list 1 (\<lambda>x xs. x) (3#xs)"

thm list.case (* list.case is the case constant for lists *)

(* Whenever we write expressions with nested patterns,
   these are automatically converted (by the parser)
   into trees of applications of case constants
   (process called pattern completion)

   Sometimes, this will produce huge terms that look
   nothing like the original.
 *)
term "case xs of [] \<Rightarrow> 1 | ''hello''#xs \<Rightarrow> 2 | [x] \<Rightarrow> 3"

(* desugared raw syntax tree *)
ML \<open>
@{term "case xs of [] \<Rightarrow> 1 | ''hello''#xs \<Rightarrow> 2 | [x] \<Rightarrow> 3"}
\<close>

(* string is a type synonym for char list

   char is a type synonym for

   bool \<times> bool \<times> bool \<times> bool \<times> bool \<times> bool \<times> bool \<times> bool
 *)
lemma bla:
  assumes "x = (case xs of [] \<Rightarrow> (1::nat) | ''hello''#xs \<Rightarrow> 2 | [x] \<Rightarrow> 3 | _ \<Rightarrow> 0)"
  shows "x \<le> 3"
  using assms
  (* alternatively we can case split
  apply(simp split: list.split_asm char.split_asm (* bool.split_asm *))
  *)
  thm list.split
  apply(cases xs; simp) (* cases is like case_tac, but doesn't work on green variables *)
  apply(case_tac a; simp)
   apply(case_tac list; simp)
  (* and so forth... *)
  oops

(* blue variables: top-level free variables from the goal statement *)
(* green variables: bound variables *)
(* orange variables: free variables from a local proof context *)

lemma "length xs = length xs"
proof(induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed


(* Slide 15 *)
(* primrec is short for primitive recursion *)
(* primitive recursion: exactly one clause of the definition per type constructor
   recursive calls must be about the recursive occurences of the type.

   primitive recursion consumes exactly one constructor per recursive call.
 *)
primrec my_sum where
  "my_sum MyNil = 0"
| "my_sum (MyCons x xs) = x + my_sum xs"

value "my_sum (MyCons 3 (MyCons (4::nat) MyNil))"

(* In Isabelle, primitive recursion is more expressive than you might think.
   You can define the ackermann function with primrec.
 *)

(* Slide 17 *)
term "rec_mylist 0 (\<lambda>x xs my_sum_xs. x + my_sum_xs)"

value "rec_mylist 0 (\<lambda>x xs my_sum_xs. x + my_sum_xs) (MyCons (5::nat) (MyCons 3 MyNil))"

find_theorems rec_list
thm List.list.rec


\<comment> \<open> ----------------------------------------------------------------\<close>

text \<open>a recursive data type: \<close>

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

print_theorems

text \<open> distinctness of constructors automatic: \<close>
lemma "Tip ~= Node l x r"
  by simp

text \<open> case syntax, case distinction manual \<close>
lemma "(1::nat) \<le> (case t of Tip \<Rightarrow> 1 | Node l x r \<Rightarrow> x+1)"
  apply(case_tac t)
  apply auto
  done

text \<open> partial cases and dummy patterns: \<close>
term "case t of Node _ b _ => b" 

text \<open> partial case maps to 'undefined': \<close>
lemma "(case Tip of Node _ _ _ => 0) = undefined" by simp

text \<open> nested case and default pattern: \<close>
term "case t of Node (Node _ _ _) x Tip => 0 | _ => 1"


text \<open> infinitely branching: \<close>
datatype 'a inftree = Tp | Nd 'a "nat \<Rightarrow> 'a inftree"

text \<open> mutually recursive \<close> 
datatype 
  ty = Integer | Real | RefT ref
  and
  ref = Class | Array ty







\<comment> \<open> ----------------------------------------------------------------\<close>

text \<open> primitive recursion \<close>

primrec
  app :: "'a list => 'a list => 'a list"
where
  "app Nil ys = ys" |
  "app (Cons x xs) ys = Cons x (app xs ys)"

print_theorems

primrec
  rv :: "'a list => 'a list"
where
  "rv [] = []" |
  "rv (x#xs) = app (rv xs) [x]"


text \<open> on trees \<close>
primrec
  mirror :: "'a tree => 'a tree"
where
  "mirror Tip = Tip" |
  "mirror (Node l x r) = Node (mirror r) x (mirror l)"

print_theorems


text \<open> mutual recursion \<close>
primrec
  has_int :: "ty \<Rightarrow> bool" and
  has_int_ref :: "ref \<Rightarrow> bool"
where
  "has_int Integer       = True" |
  "has_int Real          = False" |
  "has_int (RefT T)      = has_int_ref T" |

  "has_int_ref Class     = False" |
  "has_int_ref (Array T) = has_int T"



\<comment> \<open> ----------------------------------------------------------------\<close>

text \<open> structural induction \<close>

text \<open> discovering lemmas needed to prove a theorem \<close>

(* Often, to prove a lemma by induction, we need to discover other lemmas
   that are themselves provable by induction. *)
theorem rv_rv: "rv (rv xs) = xs"
  apply(induct xs)
   apply simp
  apply simp
  (* TODO *)
  oops




text \<open> induction heuristics \<close>

primrec
  itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  "itrev [] ys = ys" |
  "itrev (x#xs) ys = itrev xs (x#ys)"

lemma "itrev xs [] = rev xs"
  apply(induct xs)
   apply simp
  apply simp (* this induction created a subgoal with a useless induction hypothesis*)
  oops
  (* The issue here: the property that the accumulator is empty, is not an invariant
       that is preserved by each recursive call.
     Therefore: we need to generalise the goal.
    *)

lemma "itrev xs ys = rev xs"
  oops

value "itrev [1::nat,2,3] [4,5,6]"

lemma "itrev xs ys = app (rev xs) ys"
  apply(induct xs)
   apply simp
  apply simp (* we once again have a useless induction hypothesis: ys changes with each
                recursive call, but ys is the exact same in the induction hyp as in
                the conclusion *)
  oops

(* We generalise by universally quantifying ys before induction. *)
lemma "\<And>ys. itrev xs ys = (rev xs) @ ys"
  apply(induct xs)
   apply simp
  apply(drule_tac x="a # ys" in meta_spec)
  apply simp
  done

(* There is a more convenient way to do the same thing *)
lemma bla[simp]: "itrev xs ys = (rev xs) @ ys"
  (* The arbitrary variables are treated as if they were universally quantified *)
  apply(induct xs arbitrary: ys rule: list.induct)
   apply simp
  apply simp
  done

lemma "itrev xs [] = rev xs"
  by simp
  
(* You can use induct for both rule induction and datatype induction.
   If you just type induct xs, Isabelle will try to guess which induction rule
   you want to apply. *)

thm list.induct

inductive Even where
  "Even 0"
| "Even n \<Longrightarrow> Even (Suc(Suc n))"

lemma "Even n \<Longrightarrow> even n"
  apply(induct n rule: Even.induct)
   apply simp
  apply simp
  done


\<comment> \<open> ----------------------------------------------------------------\<close>

(* TODO
primrec
  lsum :: "nat list \<Rightarrow> nat"
where
  ...
 *)

lemma
  "2 * lsum [0 ..< Suc n] = n * (n + 1)"
  oops

lemma 
  "lsum (replicate n a) = n * a"
  oops


text \<open> tail recursive version: \<close>

primrec
  lsumT :: "nat list \<Rightarrow> nat \<Rightarrow> nat" 
where
  "lsumT [] s = ?"
| "..."

lemma lsum_correct:
  "lsumT xs 0 = lsum xs"
  oops

end