src/HOL/TLA/TLA.thy
changeset 17309 c43ed29bd197
parent 14565 c6dc17aab88a
child 21624 6f79647cf536
     1.1 --- a/src/HOL/TLA/TLA.thy	Wed Sep 07 20:22:15 2005 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Wed Sep 07 20:22:39 2005 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4 -(* 
     1.5 +(*
     1.6      File:        TLA/TLA.thy
     1.7 +    ID:          $Id$
     1.8      Author:      Stephan Merz
     1.9      Copyright:   1998 University of Munich
    1.10  
    1.11 @@ -9,32 +10,34 @@
    1.12  The temporal level of TLA.
    1.13  *)
    1.14  
    1.15 -TLA  =  Init +
    1.16 +theory TLA
    1.17 +imports Init
    1.18 +begin
    1.19  
    1.20  consts
    1.21    (** abstract syntax **)
    1.22 -  Box        :: ('w::world) form => temporal
    1.23 -  Dmd        :: ('w::world) form => temporal
    1.24 -  leadsto    :: ['w::world form, 'v::world form] => temporal
    1.25 -  Stable     :: stpred => temporal
    1.26 -  WF         :: [action, 'a stfun] => temporal
    1.27 -  SF         :: [action, 'a stfun] => temporal
    1.28 +  Box        :: "('w::world) form => temporal"
    1.29 +  Dmd        :: "('w::world) form => temporal"
    1.30 +  leadsto    :: "['w::world form, 'v::world form] => temporal"
    1.31 +  Stable     :: "stpred => temporal"
    1.32 +  WF         :: "[action, 'a stfun] => temporal"
    1.33 +  SF         :: "[action, 'a stfun] => temporal"
    1.34  
    1.35    (* Quantification over (flexible) state variables *)
    1.36 -  EEx        :: ('a stfun => temporal) => temporal       (binder "Eex " 10)
    1.37 -  AAll       :: ('a stfun => temporal) => temporal       (binder "Aall " 10)
    1.38 +  EEx        :: "('a stfun => temporal) => temporal"       (binder "Eex " 10)
    1.39 +  AAll       :: "('a stfun => temporal) => temporal"       (binder "Aall " 10)
    1.40  
    1.41    (** concrete syntax **)
    1.42  syntax
    1.43 -  "_Box"     :: lift => lift                        ("([]_)" [40] 40)
    1.44 -  "_Dmd"     :: lift => lift                        ("(<>_)" [40] 40)
    1.45 -  "_leadsto" :: [lift,lift] => lift                 ("(_ ~> _)" [23,22] 22)
    1.46 -  "_stable"  :: lift => lift                        ("(stable/ _)")
    1.47 -  "_WF"      :: [lift,lift] => lift                 ("(WF'(_')'_(_))" [0,60] 55)
    1.48 -  "_SF"      :: [lift,lift] => lift                 ("(SF'(_')'_(_))" [0,60] 55)
    1.49 +  "_Box"     :: "lift => lift"                        ("([]_)" [40] 40)
    1.50 +  "_Dmd"     :: "lift => lift"                        ("(<>_)" [40] 40)
    1.51 +  "_leadsto" :: "[lift,lift] => lift"                 ("(_ ~> _)" [23,22] 22)
    1.52 +  "_stable"  :: "lift => lift"                        ("(stable/ _)")
    1.53 +  "_WF"      :: "[lift,lift] => lift"                 ("(WF'(_')'_(_))" [0,60] 55)
    1.54 +  "_SF"      :: "[lift,lift] => lift"                 ("(SF'(_')'_(_))" [0,60] 55)
    1.55  
    1.56 -  "_EEx"     :: [idts, lift] => lift                ("(3EEX _./ _)" [0,10] 10)
    1.57 -  "_AAll"    :: [idts, lift] => lift                ("(3AALL _./ _)" [0,10] 10)
    1.58 +  "_EEx"     :: "[idts, lift] => lift"                ("(3EEX _./ _)" [0,10] 10)
    1.59 +  "_AAll"    :: "[idts, lift] => lift"                ("(3AALL _./ _)" [0,10] 10)
    1.60  
    1.61  translations
    1.62    "_Box"      ==   "Box"
    1.63 @@ -56,43 +59,46 @@
    1.64    "sigma |= AALL x. F"    <= "_AAll x F sigma"
    1.65  
    1.66  syntax (xsymbols)
    1.67 -  "_Box"     :: lift => lift                        ("(\\<box>_)" [40] 40)
    1.68 -  "_Dmd"     :: lift => lift                        ("(\\<diamond>_)" [40] 40)
    1.69 -  "_leadsto" :: [lift,lift] => lift                 ("(_ \\<leadsto> _)" [23,22] 22)
    1.70 -  "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
    1.71 -  "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
    1.72 +  "_Box"     :: "lift => lift"                        ("(\<box>_)" [40] 40)
    1.73 +  "_Dmd"     :: "lift => lift"                        ("(\<diamond>_)" [40] 40)
    1.74 +  "_leadsto" :: "[lift,lift] => lift"                 ("(_ \<leadsto> _)" [23,22] 22)
    1.75 +  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
    1.76 +  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
    1.77  
    1.78  syntax (HTML output)
    1.79 -  "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
    1.80 -  "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
    1.81 +  "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
    1.82 +  "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
    1.83  
    1.84 -rules
    1.85 +axioms
    1.86    (* Definitions of derived operators *)
    1.87 -  dmd_def      "TEMP <>F  ==  TEMP ~[]~F"
    1.88 -  boxInit      "TEMP []F  ==  TEMP []Init F"
    1.89 -  leadsto_def  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
    1.90 -  stable_def   "TEMP stable P  ==  TEMP []($P --> P$)"
    1.91 -  WF_def       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
    1.92 -  SF_def       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
    1.93 -  aall_def     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
    1.94 +  dmd_def:      "TEMP <>F  ==  TEMP ~[]~F"
    1.95 +  boxInit:      "TEMP []F  ==  TEMP []Init F"
    1.96 +  leadsto_def:  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
    1.97 +  stable_def:   "TEMP stable P  ==  TEMP []($P --> P$)"
    1.98 +  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
    1.99 +  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
   1.100 +  aall_def:     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
   1.101  
   1.102  (* Base axioms for raw TLA. *)
   1.103 -  normalT    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
   1.104 -  reflT      "|- []F --> F"         (* F::temporal *)
   1.105 -  transT     "|- []F --> [][]F"     (* polymorphic *)
   1.106 -  linT       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
   1.107 -  discT      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
   1.108 -  primeI     "|- []P --> Init P`"
   1.109 -  primeE     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
   1.110 -  indT       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
   1.111 -  allT       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
   1.112 +  normalT:    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
   1.113 +  reflT:      "|- []F --> F"         (* F::temporal *)
   1.114 +  transT:     "|- []F --> [][]F"     (* polymorphic *)
   1.115 +  linT:       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
   1.116 +  discT:      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
   1.117 +  primeI:     "|- []P --> Init P`"
   1.118 +  primeE:     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
   1.119 +  indT:       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
   1.120 +  allT:       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
   1.121  
   1.122 -  necT       "|- F ==> |- []F"      (* polymorphic *)
   1.123 +  necT:       "|- F ==> |- []F"      (* polymorphic *)
   1.124  
   1.125  (* Flexible quantification: refinement mappings, history variables *)
   1.126 -  eexI       "|- F x --> (EEX x. F x)"
   1.127 -  eexE       "[| sigma |= (EEX x. F x); basevars vs;
   1.128 -		 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) 
   1.129 -	      |] ==> G sigma"
   1.130 -  history    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
   1.131 +  eexI:       "|- F x --> (EEX x. F x)"
   1.132 +  eexE:       "[| sigma |= (EEX x. F x); basevars vs;
   1.133 +                 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
   1.134 +              |] ==> G sigma"
   1.135 +  history:    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
   1.136 +
   1.137 +ML {* use_legacy_bindings (the_context ()) *}
   1.138 +
   1.139  end