ROOT

chapter "New-Psi"

(*
 * A new formalisation of psi-calculi that no longer requires channels
 * to be symmetric and transitive.
 *)

session NewPsi = "HOL-Nominal" +
  theories
    "Chain"
    "Subst_Term"
    "Agent"
    "Frame"
    "Semantics"
    "Simulation"
    "Bisimulation"
    "Sim_Pres"
    "Bisim_Pres"
    "Sim_Struct_Cong"
    "Structural_Congruence"
    "Bisim_Struct_Cong"
    "Close_Subst"
    "Bisim_Subst"
    "Tau_Chain"    
    "Weak_Bisim_Pres"
    "Weak_Bisim_Struct_Cong"
    "Weak_Bisim_Subst"
    "Weak_Bisimulation"
    "Weak_Cong_Pres"
    "Weak_Congruence"
    "Weak_Cong_Sim_Pres"
    "Weak_Cong_Simulation"
    "Weak_Cong_Struct_Cong"
    "Weaken_Bisimulation"
    "Weakening"
    "Weaken_Simulation"
    "Weaken_Stat_Imp"
    "Weaken_Transition"
    "Weak_Psi_Congruence"
    "Weak_Sim_Pres"
    "Weak_Simulation"
    "Weak_Stat_Imp_Pres"
    "Weak_Stat_Imp"
(*
 * Prove that the new semantics is a conservative extension.
 *)

session OldPsi = NewPsi +
  theories
    "Old_Semantics"
    "Old_Simulation"
    "Old_Bisimulation"
    "Old_Tau_Chain"
    "Old_Weak_Simulation"
    "Old_Weak_Bisimulation"