Theory Powerstream

theory Powerstream
imports BNF_Nonuniform_Fixpoint Eisbach
theory Powerstream
imports "../code/BNF_Nonuniform_Fixpoint" "~~/src/HOL/Eisbach/Eisbach"
begin

method parametricity_prover =
  (match premises in
     bi_unique[transfer_rule]: "bi_unique P" and
     left_total[transfer_rule]: "left_total P" for P  ‹transfer_prover›)
  
nonuniform_codatatype 'a pstream = PSCons (pshd: 'a) (pstl: "('a × 'a) pstream")

declare pstream.map_sel[simp] pstream.map_cong[intro!]

(*
nonuniform_primcorecursive psconst :: "'a ⇒ 'a pstream" where
  "psconst x = PSCons x (psconst (x, x))"
*)

consts psconst :: "'a ⇒ 'a pstream"
axiomatization where
  psconst_ctr: "⋀x. psconst x = PSCons x (psconst (x, x))" and
  psconst_transfer[transfer_rule]: "⋀R. bi_unique R ⟹ rel_fun R (rel_pstream R) psconst psconst"
  
lemma psconst_sel[simp]:
  "pshd (psconst x) = x"
  "pstl (psconst x) = psconst (x, x)"
  by (subst psconst_ctr, auto)+
  
nonuniform_coinduct "λl r :: 'a pstream. ∃x xs. l = psconst x ∧ r = map_pstream (λ_ :: 'a. x) xs" in
  "(psconst x :: 'a pstream) = map_pstream (λ_ :: 'a. x) xs"
  by parametricity_prover force+
  
  
end