src/HOL/TLA/TLA.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 12114 a8e860c86252
child 17309 c43ed29bd197
permissions -rw-r--r--
use more symbols in HTML output
     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 syntax (HTML output)
    66   "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
    67   "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
    68 
    69 rules
    70   (* Definitions of derived operators *)
    71   dmd_def      "TEMP <>F  ==  TEMP ~[]~F"
    72   boxInit      "TEMP []F  ==  TEMP []Init F"
    73   leadsto_def  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
    74   stable_def   "TEMP stable P  ==  TEMP []($P --> P$)"
    75   WF_def       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
    76   SF_def       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
    77   aall_def     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
    78 
    79 (* Base axioms for raw TLA. *)
    80   normalT    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
    81   reflT      "|- []F --> F"         (* F::temporal *)
    82   transT     "|- []F --> [][]F"     (* polymorphic *)
    83   linT       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
    84   discT      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
    85   primeI     "|- []P --> Init P`"
    86   primeE     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
    87   indT       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
    88   allT       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
    89 
    90   necT       "|- F ==> |- []F"      (* polymorphic *)
    91 
    92 (* Flexible quantification: refinement mappings, history variables *)
    93   eexI       "|- F x --> (EEX x. F x)"
    94   eexE       "[| sigma |= (EEX x. F x); basevars vs;
    95 		 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) 
    96 	      |] ==> G sigma"
    97   history    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
    98 end