CatSem.RPCF.RPCF_rep

Require Export CatSem.RPCF.RPCF_rep.
Require Export CatSem.CAT.eq_fibre.

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

Notation "M [( s )]" := (FIB_RMOD_HOM M s) (at level 30).
Notation "f 'X' g" := (product_mor _ f g)(at level 30).
Notation "f ** rho" := (colax_PbRMod_Hom f rho)(at level 34).

Notation "'IsoPF'" := (colax_Pb_Fib _ _ _).
Notation "'IsoFP'" := (colax_Fib_Pb _ _ _).
Notation "'IsoXP'" := (colax_PROD_PM _ _ _ _ ).

Notation "*--->*" := (unit_rmod _ ).

Section rep_hom.

Variables P R : PCFPO_rep.

Section Rep_Hom_Class.

Variable Sorts_map : Sorts P -> Sorts R.
Hypothesis HArrow : forall u v, Sorts_map (u ~~> v) = Sorts_map u ~~> Sorts_map v.
Hypothesis HBool : Sorts_map (Bool _ ) = Bool _ .
Hypothesis HNat : Sorts_map (Nat _ ) = Nat _ .

Variable f : colax_RMonad_Hom P R
    (G1:=RETYPE (fun t => Sorts_map t))
    (G2:=RETYPE_PO (fun t => Sorts_map t))
  (RT_NT (fun t => Sorts_map t)).

Obligation Tactic :=
        intros; simpl; repeat (rew_all || auto).

Implicit Arguments Succ [Sorts P Arrow Bool Nat PCFPO_rep_struct].
Implicit Arguments CondB [Sorts P Arrow Bool Nat PCFPO_rep_struct].
Implicit Arguments CondN [Sorts P Arrow Bool Nat PCFPO_rep_struct].
Implicit Arguments Pred [Sorts P Arrow Bool Nat PCFPO_rep_struct].
Implicit Arguments Zero [Sorts P Arrow Bool Nat PCFPO_rep_struct].
Implicit Arguments ffff [Sorts P Arrow Bool Nat PCFPO_rep_struct].
Implicit Arguments tttt [Sorts P Arrow Bool Nat PCFPO_rep_struct].
Implicit Arguments Nat [p].
Implicit Arguments Bool [p].

Program Definition Succ_hom' :=
  Succ ;; f [(Nat ~~> Nat )] ;;

                Fib_eq_RMod _ ( _ );;

                IsoPF
           ==
           *--->* ;;

           f ** (Succ ).

Print Succ_hom'.

Program Definition CondB_hom' := CondB ;;
                f [( _ )] ;;
                Fib_eq_RMod _ ( _ );;

                IsoPF
           ==
           *--->* ;;

           f ** (CondB ).

Program Definition CondN_hom' := CondN ;;
                f [( _ )] ;;
                Fib_eq_RMod _ _ ;;
                IsoPF
           ==
           *--->* ;;

           f ** (CondN ).

Program Definition Pred_hom' := Pred ;;
                f [( _ )] ;;
                Fib_eq_RMod _ _ ;;
                IsoPF
           ==
           *--->* ;;

           f ** (Pred ) .

Program Definition Zero_hom' := Zero ;;
                f [( _ )] ;;
                Fib_eq_RMod _ _;;
                IsoPF
           ==
           *--->* ;;

           f ** (Zero ).

Program Definition fff_hom' := ffff ;;
                f [( _ )] ;;
                Fib_eq_RMod _ _ ;;
                IsoPF
           ==
           *--->* ;;

           f ** (ffff ).

Program Definition ttt_hom' := tttt ;;
                f [( _ )] ;;
                Fib_eq_RMod _ _ ;;
                IsoPF
           ==
           *--->* ;;

           f ** (tttt ).

Program Definition bottom_hom' := forall u,
           bottom u ;;
                f [( _ )] ;;

             IsoPF
           ==
           *--->* ;;

           f ** (bottom (_)).

Program Definition nats_hom' := forall m,
           nats m ;;
                f [( _ )] ;;
                Fib_eq_RMod _ ( _ );;
                IsoPF
           ==
           *--->* ;;

           f ** (nats m).

Check colax_PbRMod_Hom.
Locate "*".
Locate "**".

Program Definition app_hom' := forall u v,

             (f [(u ~~> v)] ;;
              Fib_eq_RMod _ (HArrow _ _);;
               IsoPF ) X
             (f [(u)] ;;

              IsoPF )
            ;;

             IsoXP
            ;;

           f ** (app _ _ )
           ==
           app u v;;
             f [( _ )] ;; IsoPF.

Print app_hom'.

Program Definition rec_hom' := forall t,
      rec t ;;
         f [( _ )] ;; IsoPF

      ==
      f [( _ )] ;;
      Fib_eq_RMod _ (HArrow _ _) ;;

        IsoPF ;;
      f ** (rec (_ t)) .

Program Definition abs_hom' := forall u v,
     abs u v ;;
         f [( _ )]

             ==
        DerFib_RMod_Hom _ _ _ ;;

        IsoPF ;;
        f ** (abs (_ u) (_ v)) ;;

        IsoFP ;;
        Fib_eq_RMod _ (eq_sym (HArrow _ _ )) .
Print abs_hom'.

Class PCFPO_rep_Hom_struct := {

  CondB_hom : CondB_hom'
;
  CondN_hom : CondN_hom'
;
  Pred_hom : Pred_hom'
;
  Zero_hom : Zero_hom'
;
  Succ_hom : Succ_hom'
;
  fff_hom : fff_hom'

;
  ttt_hom : ttt_hom'
;
  bottom_hom : bottom_hom'
;
  nats_hom : nats_hom'
;

  app_hom : app_hom'
;

  rec_hom : rec_hom'
;
  abs_hom : abs_hom'
}.

End Rep_Hom_Class.

Record PCFPO_rep_Hom := {
  Sorts_map : Sorts P -> Sorts R ;
  HArrow : forall u v, Sorts_map (u ~~> v) = Sorts_map u ~~> Sorts_map v;
  HNat : Sorts_map (Nat _ ) = Nat R ;
  HBool : Sorts_map (Bool _ ) = Bool R ;
  rep_Hom_monad :> colax_RMonad_Hom P R (RT_NT (fun t => Sorts_map t));
  rep_colax_Hom_monad_struct :> PCFPO_rep_Hom_struct
                 HArrow HBool HNat rep_Hom_monad
}.

End rep_hom.

Existing Instance rep_colax_Hom_monad_struct.

Library CatSem.RPCF.RPCF_rep_hom