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