Structure bisimulationTheory

signature bisimulationTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BISIM_def : thm
    val ETS_def : thm
    val WBISIM_def : thm
    val WTS_def : thm
  
  (*  Theorems  *)
    val BISIM_ID : thm
    val BISIM_IMP_WBISIM : thm
    val BISIM_INV : thm
    val BISIM_O : thm
    val BISIM_REL_IMP_WBISIM_REL : thm
    val BISIM_REL_IS_BISIM : thm
    val BISIM_REL_IS_EQUIV_REL : thm
    val BISIM_REL_RSUBSET_WBISIM_REL : thm
    val BISIM_REL_cases : thm
    val BISIM_REL_coind : thm
    val BISIM_REL_def : thm
    val BISIM_REL_rules : thm
    val BISIM_RUNION : thm
    val ETS_REFL : thm
    val ETS_TRANS : thm
    val ETS_WTS_ETS : thm
    val TS_IMP_ETS : thm
    val TS_IMP_WTS : thm
    val WBISIM_ID : thm
    val WBISIM_INV : thm
    val WBISIM_O : thm
    val WBISIM_REL_IS_EQUIV_REL : thm
    val WBISIM_REL_IS_WBISIM : thm
    val WBISIM_REL_cases : thm
    val WBISIM_REL_coind : thm
    val WBISIM_REL_def : thm
    val WBISIM_REL_rules : thm
    val WBISIM_RUNION : thm
  
  val bisimulation_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [relation] Parent theory of "bisimulation"
   
   [BISIM_def]  Definition
      
      ⊢ ∀ts R.
            BISIM ts R ⇔
            ∀p q l.
                R p q ⇒
                (∀p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ R p' q') ∧
                ∀q'. ts q l q' ⇒ ∃p'. ts p l p' ∧ R p' q'
   
   [ETS_def]  Definition
      
      ⊢ ∀ts tau. ETS ts tau = (λx y. ts x tau y)⃰
   
   [WBISIM_def]  Definition
      
      ⊢ ∀ts tau R.
            WBISIM ts tau R ⇔
            ∀p q.
                R p q ⇒
                (∀l.
                     l ≠ tau ⇒
                     (∀p'. ts p l p' ⇒ ∃q'. WTS ts tau q l q' ∧ R p' q') ∧
                     ∀q'. ts q l q' ⇒ ∃p'. WTS ts tau p l p' ∧ R p' q') ∧
                (∀p'. ts p tau p' ⇒ ∃q'. ETS ts tau q q' ∧ R p' q') ∧
                ∀q'. ts q tau q' ⇒ ∃p'. ETS ts tau p p' ∧ R p' q'
   
   [WTS_def]  Definition
      
      ⊢ ∀ts tau.
            WTS ts tau =
            (λp l q. ∃p' q'. ETS ts tau p p' ∧ ts p' l q' ∧ ETS ts tau q' q)
   
   [BISIM_ID]  Theorem
      
      ⊢ ∀ts. BISIM ts $=
   
   [BISIM_IMP_WBISIM]  Theorem
      
      ⊢ ∀ts tau R. BISIM ts R ⇒ WBISIM ts tau R
   
   [BISIM_INV]  Theorem
      
      ⊢ ∀ts R. BISIM ts R ⇒ BISIM ts Rᵀ
   
   [BISIM_O]  Theorem
      
      ⊢ ∀ts R R'. BISIM ts R ∧ BISIM ts R' ⇒ BISIM ts (R' ∘ᵣ R)
   
   [BISIM_REL_IMP_WBISIM_REL]  Theorem
      
      ⊢ ∀ts tau p q. BISIM_REL ts p q ⇒ WBISIM_REL ts tau p q
   
   [BISIM_REL_IS_BISIM]  Theorem
      
      ⊢ ∀ts. BISIM ts (BISIM_REL ts)
   
   [BISIM_REL_IS_EQUIV_REL]  Theorem
      
      ⊢ ∀ts. equivalence (BISIM_REL ts)
   
   [BISIM_REL_RSUBSET_WBISIM_REL]  Theorem
      
      ⊢ ∀ts tau. BISIM_REL ts ⊆ᵣ WBISIM_REL ts tau
   
   [BISIM_REL_cases]  Theorem
      
      ⊢ ∀ts a0 a1.
            BISIM_REL ts a0 a1 ⇔
            ∀l.
                (∀p'. ts a0 l p' ⇒ ∃q'. ts a1 l q' ∧ BISIM_REL ts p' q') ∧
                ∀q'. ts a1 l q' ⇒ ∃p'. ts a0 l p' ∧ BISIM_REL ts p' q'
   
   [BISIM_REL_coind]  Theorem
      
      ⊢ ∀ts BISIM_REL'.
            (∀a0 a1.
                 BISIM_REL' a0 a1 ⇒
                 ∀l.
                     (∀p'. ts a0 l p' ⇒ ∃q'. ts a1 l q' ∧ BISIM_REL' p' q') ∧
                     ∀q'. ts a1 l q' ⇒ ∃p'. ts a0 l p' ∧ BISIM_REL' p' q') ⇒
            ∀a0 a1. BISIM_REL' a0 a1 ⇒ BISIM_REL ts a0 a1
   
   [BISIM_REL_def]  Theorem
      
      ⊢ ∀ts. BISIM_REL ts = (λp q. ∃R. BISIM ts R ∧ R p q)
   
   [BISIM_REL_rules]  Theorem
      
      ⊢ ∀ts p q.
            (∀l.
                 (∀p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ BISIM_REL ts p' q') ∧
                 ∀q'. ts q l q' ⇒ ∃p'. ts p l p' ∧ BISIM_REL ts p' q') ⇒
            BISIM_REL ts p q
   
   [BISIM_RUNION]  Theorem
      
      ⊢ ∀ts R R'. BISIM ts R ∧ BISIM ts R' ⇒ BISIM ts (R ∪ᵣ R')
   
   [ETS_REFL]  Theorem
      
      ⊢ ∀ts tau p. ETS ts tau p p
   
   [ETS_TRANS]  Theorem
      
      ⊢ ∀ts tau x y z. ETS ts tau x y ∧ ETS ts tau y z ⇒ ETS ts tau x z
   
   [ETS_WTS_ETS]  Theorem
      
      ⊢ ∀ts tau p p1 l p2 p'.
            ETS ts tau p p1 ∧ WTS ts tau p1 l p2 ∧ ETS ts tau p2 p' ⇒
            WTS ts tau p l p'
   
   [TS_IMP_ETS]  Theorem
      
      ⊢ ∀ts tau p q. ts p tau q ⇒ ETS ts tau p q
   
   [TS_IMP_WTS]  Theorem
      
      ⊢ ∀ts tau p l q. ts p l q ⇒ WTS ts tau p l q
   
   [WBISIM_ID]  Theorem
      
      ⊢ ∀ts tau. WBISIM ts tau $=
   
   [WBISIM_INV]  Theorem
      
      ⊢ ∀ts tau R. WBISIM ts tau R ⇒ WBISIM ts tau Rᵀ
   
   [WBISIM_O]  Theorem
      
      ⊢ ∀ts tau R R'.
            WBISIM ts tau R ∧ WBISIM ts tau R' ⇒ WBISIM ts tau (R' ∘ᵣ R)
   
   [WBISIM_REL_IS_EQUIV_REL]  Theorem
      
      ⊢ ∀ts tau. equivalence (WBISIM_REL ts tau)
   
   [WBISIM_REL_IS_WBISIM]  Theorem
      
      ⊢ ∀ts tau. WBISIM ts tau (WBISIM_REL ts tau)
   
   [WBISIM_REL_cases]  Theorem
      
      ⊢ ∀ts tau a0 a1.
            WBISIM_REL ts tau a0 a1 ⇔
            (∀l.
                 l ≠ tau ⇒
                 (∀p'.
                      ts a0 l p' ⇒
                      ∃q'. WTS ts tau a1 l q' ∧ WBISIM_REL ts tau p' q') ∧
                 ∀q'.
                     ts a1 l q' ⇒
                     ∃p'. WTS ts tau a0 l p' ∧ WBISIM_REL ts tau p' q') ∧
            (∀p'.
                 ts a0 tau p' ⇒
                 ∃q'. ETS ts tau a1 q' ∧ WBISIM_REL ts tau p' q') ∧
            ∀q'.
                ts a1 tau q' ⇒
                ∃p'. ETS ts tau a0 p' ∧ WBISIM_REL ts tau p' q'
   
   [WBISIM_REL_coind]  Theorem
      
      ⊢ ∀ts tau WBISIM_REL'.
            (∀a0 a1.
                 WBISIM_REL' a0 a1 ⇒
                 (∀l.
                      l ≠ tau ⇒
                      (∀p'.
                           ts a0 l p' ⇒
                           ∃q'. WTS ts tau a1 l q' ∧ WBISIM_REL' p' q') ∧
                      ∀q'.
                          ts a1 l q' ⇒
                          ∃p'. WTS ts tau a0 l p' ∧ WBISIM_REL' p' q') ∧
                 (∀p'.
                      ts a0 tau p' ⇒
                      ∃q'. ETS ts tau a1 q' ∧ WBISIM_REL' p' q') ∧
                 ∀q'.
                     ts a1 tau q' ⇒
                     ∃p'. ETS ts tau a0 p' ∧ WBISIM_REL' p' q') ⇒
            ∀a0 a1. WBISIM_REL' a0 a1 ⇒ WBISIM_REL ts tau a0 a1
   
   [WBISIM_REL_def]  Theorem
      
      ⊢ ∀ts tau. WBISIM_REL ts tau = (λp q. ∃R. WBISIM ts tau R ∧ R p q)
   
   [WBISIM_REL_rules]  Theorem
      
      ⊢ ∀ts tau p q.
            (∀l.
                 l ≠ tau ⇒
                 (∀p'.
                      ts p l p' ⇒
                      ∃q'. WTS ts tau q l q' ∧ WBISIM_REL ts tau p' q') ∧
                 ∀q'.
                     ts q l q' ⇒
                     ∃p'. WTS ts tau p l p' ∧ WBISIM_REL ts tau p' q') ∧
            (∀p'.
                 ts p tau p' ⇒
                 ∃q'. ETS ts tau q q' ∧ WBISIM_REL ts tau p' q') ∧
            (∀q'.
                 ts q tau q' ⇒
                 ∃p'. ETS ts tau p p' ∧ WBISIM_REL ts tau p' q') ⇒
            WBISIM_REL ts tau p q
   
   [WBISIM_RUNION]  Theorem
      
      ⊢ ∀ts tau R R'.
            WBISIM ts tau R ∧ WBISIM ts tau R' ⇒ WBISIM ts tau (R ∪ᵣ R')
   
   
*)
end

HOL 4, Kananaskis-13