theory hawk
  imports Main "HOL-Library.BNF_Corec"
begin

type_synonym 
  time=nat

text \<open>Define the type of signals as a codatatype (i.e., as a stream of elements)\<close>
codatatype 'a signal = Signal (head: 'a) (rest: "'a signal")
  for map: lift \<comment> \<open>The canonical map operator on the \<close>

text \<open>Conversion function from the codatatype view to the view as a function @{typ \<open>time \<Rightarrow> 'a\<close>}\<close>
fun at :: "'a signal \<Rightarrow> time \<Rightarrow> 'a" where
  "at (Signal x xs) 0 = x"
| "at (Signal x xs) (Suc n) = at xs n"

text \<open>Inverse to @{term at}\<close>
primcorec from_series :: "(time \<Rightarrow> 'a) \<Rightarrow> 'a signal" where
  "from_series f = Signal (f 0) (from_series (f \<circ> Suc))"

text \<open>@{typ \<open>'a signal\<close>} is isomorphic to @{typ \<open>time \<Rightarrow> 'a\<close>}\<close>
lemma at_from_series: "at (from_series f) = f"
proof
  fix n
  show "at (from_series f) n = f n"
    by(induction n arbitrary: f)(subst from_series.code; simp; fail)+
qed

lemma at_0: "at xs 0 = head xs"
  by(cases xs) simp

lemma at_Suc: "at xs (Suc n) = at (rest xs) n"
  by(cases xs) simp

lemma from_series_at: "from_series (at xs) = xs"
  by(coinduction arbitrary: xs)(auto simp add: o_def at_0 at_Suc)

text \<open>Define the constant signal by primitive corecursion. It would also work to just use @{term from_series}.\<close>
primcorec constantInt :: "nat \<Rightarrow> nat signal" where
  "constantInt x = Signal x (constantInt x)"

text \<open>The selector function would also be primitively corecursive, but we nevertheless
  define it with @{command corec} because then we can register it as a friend, i.e.,
  it can appear in the context of corecursive calls in later corecursive definitions. 
\<close>
corec (friend) sel :: "bool signal \<Rightarrow> 'a signal \<Rightarrow> 'a signal \<Rightarrow> 'a signal" where
  "sel bs xs ys = Signal (if head bs then head xs else head ys) (sel (rest bs) (rest xs) (rest ys))"

abbreviation (input) delay :: "'a \<Rightarrow> 'a signal \<Rightarrow> 'a signal" where
  "delay \<equiv> Signal" \<comment> \<open>The constructor of the codatatype is exactly the delay operator.\<close>

text \<open>
  We could define @{text "inc"} corecursively via the equation given below to @command{friend_of_corec}.
  But since the original theory had defined it via the @{term lift} operation, let's stick to that
  and establish friendliness separately.
\<close>
definition inc :: "nat signal \<Rightarrow> nat signal" where
  "inc as = lift Suc as"

friend_of_corec inc where
  "inc as = Signal (Suc (head as)) (inc (rest as))"
  subgoal by(cases as)(simp add: inc_def) \<comment> \<open>Prove that the equation indeed describes @{term inc}\<close>
  subgoal by transfer_prover \<comment> \<open>The friendliness condition: @{term inc} inspects the argument signal at most at the head before it produces at least one new value.\<close>
  done

corec nextSig :: "bool signal \<Rightarrow> nat signal" where
  \<comment> \<open>The corecursive call is guarded by the @{term delay} constructor and appears under the friendly
  operators @{term sig} and @{term inc}.\<close>
  "nextSig bs = delay 0 (sel bs (constantInt 0) (inc (nextSig bs)))"

definition outputSig :: "bool signal \<Rightarrow> nat signal" where
  "outputSig bS = sel bS (constantInt 0) (inc (nextSig bS))"

corec outSig1 :: "bool signal \<Rightarrow> nat signal" where
  "outSig1 bS =sel bS (constantInt 0) (inc (delay 0 (outSig1 bS)))"

definition resetCounter :: "bool signal \<Rightarrow> nat signal" where
  "resetCounter b = outputSig b"