Library CatSem.RPCF.RPCF_syntax_rep

Require Export CatSem.PCF.PCF_RMonad.
Require Export CatSem.RPCF.RPCF_rep.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Transparent Obligations.
Unset Automatic Introduction.

Obligation Tactic := simpl; intros;
         unfold Rsubst_star_map; simpl;
        apply clos_refl_trans_1n_contains;
        apply relorig;
        try apply app_abs;
        try constructor.

Program Instance PCFE_rep_struct :
       PCFPO_rep_struct PCFEM PCF.Arrow PCF.Bool PCF.Nat := {
  app r s := PCFApp r s;
  abs r s := PCFAbs r s;
  rec t := PCFRec t ;
  tttt := PCFconsts ttt ;
  ffff := PCFconsts fff;
  Succ := PCFconsts succ;
  Pred := PCFconsts preds;
  CondN := PCFconsts condN;
  CondB := PCFconsts condB;
  Zero := PCFconsts zero ;
  nats m := PCFconsts (Nats m);
  bottom t := PCFbottom t
}.

Definition PCFE_rep : PCFPO_rep :=
  Build_PCFPO_rep (Sorts:=PCF.Sorts) (Arrow:=PCF.Arrow)
   (pcf_rep_monad:=PCFEM)
   PCFE_rep_struct.