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.
            R p q ⇒
            ∀l. (∀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-14