--- a/src/HOL/TLA/TLA.thy Mon Feb 08 13:02:42 1999 +0100
+++ b/src/HOL/TLA/TLA.thy Mon Feb 08 13:02:56 1999 +0100
@@ -1,7 +1,7 @@
(*
File: TLA/TLA.thy
Author: Stephan Merz
- Copyright: 1997 University of Munich
+ Copyright: 1998 University of Munich
Theory Name: TLA
Logic Image: HOL
@@ -9,79 +9,88 @@
The temporal level of TLA.
*)
-TLA = Action + WF_Rel +
-
-types
- behavior
- temporal = "behavior form"
-
-arities
- behavior :: world
+TLA = Init + WF_Rel +
consts
- (* get first 2 states of behavior *)
- fst_st :: "behavior => state"
- snd_st :: "behavior => state"
-
- Init :: "action => temporal"
- (* define Box and Dmd for both actions and temporals *)
- Box :: "('w::world) form => temporal" ("([](_))" [40] 40)
- Dmd :: "('w::world) form => temporal" ("(<>(_))" [40] 40)
- "~>" :: "[action,action] => temporal" (infixr 22)
- stable :: "action => temporal"
- WF :: "[action,'a stfun] => temporal" ("(WF'(_')'_(_))" [0,60] 55)
- SF :: "[action,'a stfun] => temporal" ("(SF'(_')'_(_))" [0,60] 55)
+ (** abstract syntax **)
+ Box :: ('w::world) form => temporal
+ Dmd :: ('w::world) form => temporal
+ leadsto :: ['w::world form, 'v::world form] => temporal
+ Stable :: stpred => temporal
+ WF :: [action, 'a stfun] => temporal
+ SF :: [action, 'a stfun] => temporal
(* Quantification over (flexible) state variables *)
- EEx :: "('a stfun => temporal) => temporal" (binder "EEX " 10)
- AAll :: "('a stfun => temporal) => temporal" (binder "AALL " 10)
+ EEx :: ('a stfun => temporal) => temporal (binder "Eex " 10)
+ AAll :: ('a stfun => temporal) => temporal (binder "Aall " 10)
+
+ (** concrete syntax **)
+syntax
+ "_Box" :: lift => lift ("([]_)" [40] 40)
+ "_Dmd" :: lift => lift ("(<>_)" [40] 40)
+ "_leadsto" :: [lift,lift] => lift ("(_ ~> _)" [23,22] 22)
+ "_stable" :: lift => lift ("(stable/ _)")
+ "_WF" :: [lift,lift] => lift ("(WF'(_')'_(_))" [0,60] 55)
+ "_SF" :: [lift,lift] => lift ("(SF'(_')'_(_))" [0,60] 55)
+
+ "_EEx" :: [idts, lift] => lift ("(3EEX _./ _)" [0,10] 10)
+ "_AAll" :: [idts, lift] => lift ("(3AALL _./ _)" [0,10] 10)
translations
- "sigma |= Init(A)" == "Init A sigma"
- "sigma |= Box(F)" == "Box F sigma"
- "sigma |= Dmd(F)" == "Dmd F sigma"
- "sigma |= F ~> G" == "op ~> F G sigma"
- "sigma |= stable(A)" == "stable A sigma"
- "sigma |= WF(A)_v" == "WF A v sigma"
- "sigma |= SF(A)_v" == "SF A v sigma"
+ "_Box" == "Box"
+ "_Dmd" == "Dmd"
+ "_leadsto" == "leadsto"
+ "_stable" == "Stable"
+ "_WF" == "WF"
+ "_SF" == "SF"
+ "_EEx v A" == "Eex v. A"
+ "_AAll v A" == "Aall v. A"
+
+ "sigma |= []F" <= "_Box F sigma"
+ "sigma |= <>F" <= "_Dmd F sigma"
+ "sigma |= F ~> G" <= "_leadsto F G sigma"
+ "sigma |= stable P" <= "_stable P sigma"
+ "sigma |= WF(A)_v" <= "_WF A v sigma"
+ "sigma |= SF(A)_v" <= "_SF A v sigma"
+ "sigma |= EEX x. F" <= "_EEx x F sigma"
+ "sigma |= AALL x. F" <= "_AAll x F sigma"
syntax (symbols)
- Box :: "('w::world) form => temporal" ("(\\<box>(_))" [40] 40)
- Dmd :: "('w::world) form => temporal" ("(\\<diamond>(_))" [40] 40)
+ "_Box" :: lift => lift ("(\\<box>_)" [40] 40)
+ "_Dmd" :: lift => lift ("(\\<diamond>_)" [40] 40)
+ "_leadsto" :: [lift,lift] => lift ("(_ \\<leadsto> _)" [23,22] 22)
+ "_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
+ "_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
rules
- dmd_def "(<>F) == .~[].~F"
- boxact_def "([](F::action)) == ([] Init F)"
- leadsto "P ~> Q == [](Init(P) .-> <>Q)"
- stable_def "stable P == [](P .-> P`)"
-
- WF_def "WF(A)_v == <>[] $(Enabled(<A>_v)) .-> []<><A>_v"
- SF_def "SF(A)_v == []<> $(Enabled(<A>_v)) .-> []<><A>_v"
-
- Init_def "(sigma |= Init(F)) == ([[fst_st sigma, snd_st sigma]] |= F)"
+ (* Definitions of derived operators *)
+ dmd_def "TEMP <>F == TEMP ~[]~F"
+ boxInit "TEMP []F == TEMP []Init F"
+ leadsto_def "TEMP F ~> G == TEMP [](Init F --> <>G)"
+ stable_def "TEMP stable P == TEMP []($P --> P$)"
+ WF_def "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
+ SF_def "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v"
+ aall_def "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)"
-(* The following axioms are written "polymorphically", not just for temporal formulas. *)
- normalT "[](F .-> G) .-> ([]F .-> []G)"
- reflT "[]F .-> F" (* F::temporal *)
- transT "[]F .-> [][]F"
- linT "(<>F) .& (<>G) .-> (<>(F .& <>G)) .| (<>(G .& <>F))" (* F,G::temporal *)
- discT "[](F .-> <>(.~F .& <>F)) .-> (F .-> []<>F)"
- primeI "[]P .-> Init(P`)"
- primeE "[](Init(P) .-> []F) .-> Init(P`) .-> (F .-> []F)"
- indT "[](Init(P) .& .~[]F .-> Init(P`) .& F) .-> Init(P) .-> []F"
- allT "(RALL x. [](F(x))) .= ([](RALL x. F(x)))"
+(* Base axioms for raw TLA. *)
+ normalT "|- [](F --> G) --> ([]F --> []G)" (* polymorphic *)
+ reflT "|- []F --> F" (* F::temporal *)
+ transT "|- []F --> [][]F" (* polymorphic *)
+ linT "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
+ discT "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
+ primeI "|- []P --> Init P`"
+ primeE "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
+ indT "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
+ allT "|- (! x. [](F x)) = ([](! x. F x))"
- necT "F ==> []F"
+ necT "|- F ==> |- []F" (* polymorphic *)
(* Flexible quantification: refinement mappings, history variables *)
- aall_def "(AALL x. F(x)) == .~ (EEX x. .~ F(x))"
- eexI "F x .-> (EEX x. F x)"
- historyI "[| sigma |= Init(I); sigma |= []N;
- (!!h s t. (h s = ha s t) & I [[s,t]] --> HI(h)[[s,t]]);
- (!!h s t. (h t = hc s t (h s)) & N [[s,t]] --> HN(h) [[s,t]])
- |] ==> sigma |= (EEX h. Init(HI(h)) .& []HN(h))"
- eexE "[| sigma |= (EEX x. F x);
- (!!x. [| base_var x; (sigma |= F x) |] ==> (G sigma)::bool)
- |] ==> G sigma"
+ eexI "|- F x --> (EEX x. F x)"
+ eexE "[| sigma |= (EEX x. F x); basevars vs;
+ (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
+ |] ==> G sigma"
+ history "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
+end
-end
+ML