Library HOC04DefLTS

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.


Inductive label : Type :=
 | LabOut : chan → wfprocess → label
 | LabIn : chan → label
 | LabRem : var → label
 | Tau.


Inductive abstraction : Set :=
 | AbsPure : var → wfprocess → abstraction
 | AbsPar1 : abstraction → wfprocess → abstraction
 | AbsPar2 : wfprocess → abstraction → abstraction.

Inductive agent : Set :=
 | AA : abstraction → agent
 | AP : wfprocess → agent.

Definition par_ag1 (a : agent) (p : wfprocess) : agent :=
  match a with
    | AA f ⇒ AA (AbsPar1 f p)
    | AP q ⇒ AP (wfp_Par q p)
  end.

Definition par_ag2 (p : wfprocess) (a : agent) : agent :=
  match a with
    | AA f ⇒ AA (AbsPar2 p f)
    | AP q ⇒ AP (wfp_Par p q)
  end.

Inductive const_abs : abstraction → Prop :=
 | CAbs : ∀ X (p : wfprocess), X \notin GV p → const_abs (AbsPure X p)
 | CAbsPar1 : ∀ f p, const_abs f → const_abs (AbsPar1 f p)
 | CAbsPar2 : ∀ f p, const_abs f → const_abs (AbsPar2 p f).

Hint Resolve CAbs CAbsPar1 CAbsPar2.

Fixpoint const_abs_dec (fp : abstraction): bool :=
  match fp with
    | AbsPure X p ⇒ ifb (X # p) then true else false
    | AbsPar1 fp p ⇒ const_abs_dec fp
    | AbsPar2 p fp ⇒ const_abs_dec fp
  end.

Instance const_abs_decidable : ∀ (f:abstraction), Decidable (const_abs f).
Proof.
  intros.
  applys¬ decidable_make (const_abs_dec f).
  inductions f; simpls¬.
  cases_if; try rename f into Hf; symmetry.
    applys¬ isTrue_true.
    apply isTrue_false. intro H1. inverts¬ H1.
    rewrite isTrue_def in ×. cases_if; cases_if¬.
      inverts H. false.
      false¬ H.
    rewrite isTrue_def in ×. cases_if; cases_if¬.
      inverts H. false.
      false¬ H.
Qed.

Fixpoint sizeAbs (fp :abstraction) : nat :=
  match fp with
    | AbsPure X p ⇒ sizeX X p
    | AbsPar1 fp p ⇒ sizeAbs fp
    | AbsPar2 p fp ⇒ sizeAbs fp
  end.

Fixpoint wfp_inst_Abs (fp : abstraction) (q : wfprocess) : wfprocess :=
  match fp with
    | AbsPure X p ⇒ wfp_subst q X p
    | AbsPar1 fp p ⇒ wfp_Par (wfp_inst_Abs fp q) p
    | AbsPar2 p fp ⇒ wfp_Par p (wfp_inst_Abs fp q)
  end.


Reserved Notation "{{ p -- l ->> ap }}" (at level 60).

Inductive transition : wfprocess → label → agent → Prop :=
 | TrOut : ∀ a p, {{wfp_Send a p -- LabOut a p ->> AP wfp_Nil}}
 | TrIn : ∀ a X p, {{wfp_Abs a X p -- LabIn a ->> AA (AbsPure X p)}}
 | TrRem : ∀ X, {{wfp_Gvar X -- LabRem X ->> AP wfp_Nil}}
 | TrAct1 : ∀ p q l ap, (transition p l ap) → (transition (wfp_Par p q) l (par_ag1 ap q))
 | TrAct2 : ∀ p q l aq, (transition q l aq) → (transition (wfp_Par p q) l (par_ag2 p aq))
 | TrTau1 : ∀ a p p´ q p´´ fq,
    (transition p (LabOut a p´´) (AP p´)) →
    (transition q (LabIn a) (AA fq)) →
    (transition (wfp_Par p q) Tau (AP (wfp_Par p´ (wfp_inst_Abs fq p´´))))
 | TrTau2 : ∀ a p q q´ q´´ fp,
    (transition p (LabIn a) (AA fp)) →
    (transition q (LabOut a q´´) (AP q´)) →
    (transition (wfp_Par p q) Tau (AP (wfp_Par (wfp_inst_Abs fp q´´) q´)))
where "{{ p -- l ->> ap }}" := (transition p l ap).

Hint Resolve TrOut TrIn TrRem TrAct1 TrAct2 TrTau1 TrTau2.