src/HOL/TLA/TLA.thy

updated;

(*
    File:        TLA/TLA.thy
    ID:          $Id$
    Author:      Stephan Merz
    Copyright:   1998 University of Munich

    Theory Name: TLA
    Logic Image: HOL

The temporal level of TLA.
*)

theory TLA
imports Init
begin

consts
  (** abstract syntax **)
  Box        :: "('w::world) form => temporal"
  Dmd        :: "('w::world) form => temporal"
  leadsto    :: "['w::world form, 'v::world form] => temporal"
  Stable     :: "stpred => temporal"
  WF         :: "[action, 'a stfun] => temporal"
  SF         :: "[action, 'a stfun] => temporal"

  (* Quantification over (flexible) state variables *)
  EEx        :: "('a stfun => temporal) => temporal"       (binder "Eex " 10)
  AAll       :: "('a stfun => temporal) => temporal"       (binder "Aall " 10)

  (** concrete syntax **)
syntax
  "_Box"     :: "lift => lift"                        ("([]_)" [40] 40)
  "_Dmd"     :: "lift => lift"                        ("(<>_)" [40] 40)
  "_leadsto" :: "[lift,lift] => lift"                 ("(_ ~> _)" [23,22] 22)
  "_stable"  :: "lift => lift"                        ("(stable/ _)")
  "_WF"      :: "[lift,lift] => lift"                 ("(WF'(_')'_(_))" [0,60] 55)
  "_SF"      :: "[lift,lift] => lift"                 ("(SF'(_')'_(_))" [0,60] 55)

  "_EEx"     :: "[idts, lift] => lift"                ("(3EEX _./ _)" [0,10] 10)
  "_AAll"    :: "[idts, lift] => lift"                ("(3AALL _./ _)" [0,10] 10)

translations
  "_Box"      ==   "Box"
  "_Dmd"      ==   "Dmd"
  "_leadsto"  ==   "leadsto"
  "_stable"   ==   "Stable"
  "_WF"       ==   "WF"
  "_SF"       ==   "SF"
  "_EEx v A"  ==   "Eex v. A"
  "_AAll v A" ==   "Aall v. A"

  "sigma |= []F"         <= "_Box F sigma"
  "sigma |= <>F"         <= "_Dmd F sigma"
  "sigma |= F ~> G"      <= "_leadsto F G sigma"
  "sigma |= stable P"    <= "_stable P sigma"
  "sigma |= WF(A)_v"     <= "_WF A v sigma"
  "sigma |= SF(A)_v"     <= "_SF A v sigma"
  "sigma |= EEX x. F"    <= "_EEx x F sigma"
  "sigma |= AALL x. F"    <= "_AAll x F sigma"

syntax (xsymbols)
  "_Box"     :: "lift => lift"                        ("(\<box>_)" [40] 40)
  "_Dmd"     :: "lift => lift"                        ("(\<diamond>_)" [40] 40)
  "_leadsto" :: "[lift,lift] => lift"                 ("(_ \<leadsto> _)" [23,22] 22)
  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)

syntax (HTML output)
  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)

axioms
  (* Definitions of derived operators *)
  dmd_def:      "TEMP <>F  ==  TEMP ~[]~F"
  boxInit:      "TEMP []F  ==  TEMP []Init F"
  leadsto_def:  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
  stable_def:   "TEMP stable P  ==  TEMP []($P --> P$)"
  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
  aall_def:     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"

(* Base axioms for raw TLA. *)
  normalT:    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
  reflT:      "|- []F --> F"         (* F::temporal *)
  transT:     "|- []F --> [][]F"     (* polymorphic *)
  linT:       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
  discT:      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
  primeI:     "|- []P --> Init P`"
  primeE:     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
  indT:       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
  allT:       "|- (ALL x. [](F x)) = ([](ALL x. F x))"

  necT:       "|- F ==> |- []F"      (* polymorphic *)

(* Flexible quantification: refinement mappings, history variables *)
  eexI:       "|- F x --> (EEX x. F x)"
  eexE:       "[| sigma |= (EEX x. F x); basevars vs;
                 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
              |] ==> G sigma"
  history:    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"

ML {* use_legacy_bindings (the_context ()) *}

end