Library Applications

Application to the bisimulation case


Require Export Settings.
Require Import Theory.

Section Modular.

  Variables A X: Type.
  Variable TX: reduction_t A X.

  Let F := Comp (chaining_l (expand TX TX)) (chaining_r (bisim TX TX)).
  Let G := Comp (star (X:=X)) (Union2 (identity (X:=X) (Y:=X)) (constant (bisim TX TX))).

  Lemma F_mon: monotonic TX TX F.
  Lemma G_wmon: wmonotonic TX TX G.

  Lemma FG: contains F G.

  Lemma G_reverse: forall R, eeq (trans (G R)) (G (trans R)).

  Variable R: relation X.
  Hypothesis HRt: evolve_t TX TX R (F R).
  Hypothesis HRa: evolve_a TX TX R (G R).
  Hypothesis HRt': evolve_t TX TX (trans R) (F (trans R)).
  Hypothesis HRa': evolve_a TX TX (trans R) (G (trans R)).

Theorem 2.5
  Theorem upto: incl R (bisim TX TX).

End Modular.

Section Controlled.

  Variables A X: Type.
  Variable TX: reduction_t A X.

  Variables B B': relation X.
  Hypothesis HB: bicontrolled TX B.
  Hypothesis HB': bicontrolled TX B'.

  Let F := chaining_r (X:=X) (bisim TX TX).
  Let G := Comp (star (X:=X)) (Union2 (identity (X:=X) (Y:=X)) (constant (bisim TX TX))).

  Let F_mon: monotonic TX TX F.

  Let FG: contains F G.

  Let BG: contains (chaining_l (star B)) G.

  Let B'G: contains (chaining_l (star B')) G.

  Variable R: relation X.
  Hypothesis HRt: evolve_t TX TX R (comp (star B) (F R)).
  Hypothesis HRa: evolve_a TX TX R (G R).
  Hypothesis HRt': evolve_t TX TX (trans R) (comp (star B') (F (trans R))).
  Hypothesis HRa': evolve_a TX TX (trans R) (G (trans R)).

Theorem 3.6
  Theorem upto_ctrl: incl R (bisim TX TX).

End Controlled.