src/HOL/TLA/TLA.thy
author wenzelm
Fri Nov 09 00:09:47 2001 +0100 (2001-11-09)
changeset 12114 a8e860c86252
parent 9517 f58863b1406a
child 14565 c6dc17aab88a
permissions -rw-r--r--
eliminated old "symbols" syntax, use "xsymbols" instead;
     1 (* 
     2     File:        TLA/TLA.thy
     3     Author:      Stephan Merz
     4     Copyright:   1998 University of Munich
     5 
     6     Theory Name: TLA
     7     Logic Image: HOL
     8 
     9 The temporal level of TLA.
    10 *)
    11 
    12 TLA  =  Init +
    13 
    14 consts
    15   (** abstract syntax **)
    16   Box        :: ('w::world) form => temporal
    17   Dmd        :: ('w::world) form => temporal
    18   leadsto    :: ['w::world form, 'v::world form] => temporal
    19   Stable     :: stpred => temporal
    20   WF         :: [action, 'a stfun] => temporal
    21   SF         :: [action, 'a stfun] => temporal
    22 
    23   (* Quantification over (flexible) state variables *)
    24   EEx        :: ('a stfun => temporal) => temporal       (binder "Eex " 10)
    25   AAll       :: ('a stfun => temporal) => temporal       (binder "Aall " 10)
    26 
    27   (** concrete syntax **)
    28 syntax
    29   "_Box"     :: lift => lift                        ("([]_)" [40] 40)
    30   "_Dmd"     :: lift => lift                        ("(<>_)" [40] 40)
    31   "_leadsto" :: [lift,lift] => lift                 ("(_ ~> _)" [23,22] 22)
    32   "_stable"  :: lift => lift                        ("(stable/ _)")
    33   "_WF"      :: [lift,lift] => lift                 ("(WF'(_')'_(_))" [0,60] 55)
    34   "_SF"      :: [lift,lift] => lift                 ("(SF'(_')'_(_))" [0,60] 55)
    35 
    36   "_EEx"     :: [idts, lift] => lift                ("(3EEX _./ _)" [0,10] 10)
    37   "_AAll"    :: [idts, lift] => lift                ("(3AALL _./ _)" [0,10] 10)
    38 
    39 translations
    40   "_Box"      ==   "Box"
    41   "_Dmd"      ==   "Dmd"
    42   "_leadsto"  ==   "leadsto"
    43   "_stable"   ==   "Stable"
    44   "_WF"       ==   "WF"
    45   "_SF"       ==   "SF"
    46   "_EEx v A"  ==   "Eex v. A"
    47   "_AAll v A" ==   "Aall v. A"
    48 
    49   "sigma |= []F"         <= "_Box F sigma"
    50   "sigma |= <>F"         <= "_Dmd F sigma"
    51   "sigma |= F ~> G"      <= "_leadsto F G sigma"
    52   "sigma |= stable P"    <= "_stable P sigma"
    53   "sigma |= WF(A)_v"     <= "_WF A v sigma"
    54   "sigma |= SF(A)_v"     <= "_SF A v sigma"
    55   "sigma |= EEX x. F"    <= "_EEx x F sigma"
    56   "sigma |= AALL x. F"    <= "_AAll x F sigma"
    57 
    58 syntax (xsymbols)
    59   "_Box"     :: lift => lift                        ("(\\<box>_)" [40] 40)
    60   "_Dmd"     :: lift => lift                        ("(\\<diamond>_)" [40] 40)
    61   "_leadsto" :: [lift,lift] => lift                 ("(_ \\<leadsto> _)" [23,22] 22)
    62   "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
    63   "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
    64 
    65 rules
    66   (* Definitions of derived operators *)
    67   dmd_def      "TEMP <>F  ==  TEMP ~[]~F"
    68   boxInit      "TEMP []F  ==  TEMP []Init F"
    69   leadsto_def  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
    70   stable_def   "TEMP stable P  ==  TEMP []($P --> P$)"
    71   WF_def       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
    72   SF_def       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
    73   aall_def     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
    74 
    75 (* Base axioms for raw TLA. *)
    76   normalT    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
    77   reflT      "|- []F --> F"         (* F::temporal *)
    78   transT     "|- []F --> [][]F"     (* polymorphic *)
    79   linT       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
    80   discT      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
    81   primeI     "|- []P --> Init P`"
    82   primeE     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
    83   indT       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
    84   allT       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
    85 
    86   necT       "|- F ==> |- []F"      (* polymorphic *)
    87 
    88 (* Flexible quantification: refinement mappings, history variables *)
    89   eexI       "|- F x --> (EEX x. F x)"
    90   eexE       "[| sigma |= (EEX x. F x); basevars vs;
    91 		 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) 
    92 	      |] ==> G sigma"
    93   history    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
    94 end