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