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