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