1.1 --- a/src/HOL/TLA/TLA.thy	Wed May 23 16:22:27 2012 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Wed May 23 16:53:12 2012 +0200
     1.3 @@ -64,34 +64,39 @@
     1.4    "_EEx"     :: "[idts, lift] => lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
     1.5    "_AAll"    :: "[idts, lift] => lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
     1.6  
     1.7 -axioms
     1.8 +axiomatization where
     1.9    (* Definitions of derived operators *)
    1.10 -  dmd_def:      "TEMP <>F  ==  TEMP ~[]~F"
    1.11 -  boxInit:      "TEMP []F  ==  TEMP []Init F"
    1.12 -  leadsto_def:  "TEMP F ~> G  ==  TEMP [](Init F --> <>G)"
    1.13 -  stable_def:   "TEMP stable P  ==  TEMP []($P --> P$)"
    1.14 -  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
    1.15 -  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v"
    1.16 +  dmd_def:      "\<And>F. TEMP <>F  ==  TEMP ~[]~F"
    1.17 +
    1.18 +axiomatization where
    1.19 +  boxInit:      "\<And>F. TEMP []F  ==  TEMP []Init F" and
    1.20 +  leadsto_def:  "\<And>F G. TEMP F ~> G  ==  TEMP [](Init F --> <>G)" and
    1.21 +  stable_def:   "\<And>P. TEMP stable P  ==  TEMP []($P --> P$)" and
    1.22 +  WF_def:       "TEMP WF(A)_v  ==  TEMP <>[] Enabled(<A>_v) --> []<><A>_v" and
    1.23 +  SF_def:       "TEMP SF(A)_v  ==  TEMP []<> Enabled(<A>_v) --> []<><A>_v" and
    1.24    aall_def:     "TEMP (AALL x. F x)  ==  TEMP ~ (EEX x. ~ F x)"
    1.25  
    1.26 +axiomatization where
    1.27  (* Base axioms for raw TLA. *)
    1.28 -  normalT:    "|- [](F --> G) --> ([]F --> []G)"    (* polymorphic *)
    1.29 -  reflT:      "|- []F --> F"         (* F::temporal *)
    1.30 -  transT:     "|- []F --> [][]F"     (* polymorphic *)
    1.31 -  linT:       "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
    1.32 -  discT:      "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
    1.33 -  primeI:     "|- []P --> Init P`"
    1.34 -  primeE:     "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
    1.35 -  indT:       "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
    1.36 -  allT:       "|- (ALL x. [](F x)) = ([](ALL x. F x))"
    1.37 +  normalT:    "\<And>F G. |- [](F --> G) --> ([]F --> []G)" and    (* polymorphic *)
    1.38 +  reflT:      "\<And>F. |- []F --> F" and         (* F::temporal *)
    1.39 +  transT:     "\<And>F. |- []F --> [][]F" and     (* polymorphic *)
    1.40 +  linT:       "\<And>F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and
    1.41 +  discT:      "\<And>F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and
    1.42 +  primeI:     "\<And>P. |- []P --> Init P`" and
    1.43 +  primeE:     "\<And>P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and
    1.44 +  indT:       "\<And>P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and
    1.45 +  allT:       "\<And>F. |- (ALL x. [](F x)) = ([](ALL x. F x))"
    1.46  
    1.47 -  necT:       "|- F ==> |- []F"      (* polymorphic *)
    1.48 +axiomatization where
    1.49 +  necT:       "\<And>F. |- F ==> |- []F"      (* polymorphic *)
    1.50  
    1.51 +axiomatization where
    1.52  (* Flexible quantification: refinement mappings, history variables *)
    1.53 -  eexI:       "|- F x --> (EEX x. F x)"
    1.54 +  eexI:       "|- F x --> (EEX x. F x)" and
    1.55    eexE:       "[| sigma |= (EEX x. F x); basevars vs;
    1.56                   (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
    1.57 -              |] ==> G sigma"
    1.58 +              |] ==> G sigma" and
    1.59    history:    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
    1.60  
    1.61