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!]
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