--- a/src/HOL/TLA/Action.thy Wed May 23 16:22:27 2012 +0200
+++ b/src/HOL/TLA/Action.thy Wed May 23 16:53:12 2012 +0200
@@ -58,11 +58,13 @@
"s |= Enabled A" <= "_Enabled A s"
"w |= unchanged f" <= "_unchanged f w"
-axioms
- unl_before: "(ACT $v) (s,t) == v s"
- unl_after: "(ACT v$) (s,t) == v t"
+axiomatization where
+ unl_before: "(ACT $v) (s,t) == v s" and
+ unl_after: "(ACT v$) (s,t) == v t" and
unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
+
+defs
square_def: "ACT [A]_v == ACT (A | unchanged v)"
angle_def: "ACT <A>_v == ACT (A & ~ unchanged v)"
--- a/src/HOL/TLA/Buffer/DBuffer.thy Wed May 23 16:22:27 2012 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.thy Wed May 23 16:53:12 2012 +0200
@@ -8,35 +8,34 @@
imports Buffer
begin
-consts
+axiomatization
(* implementation variables *)
- inp :: "nat stfun"
- mid :: "nat stfun"
- out :: "nat stfun"
- q1 :: "nat list stfun"
- q2 :: "nat list stfun"
- qc :: "nat list stfun"
+ inp :: "nat stfun" and
+ mid :: "nat stfun" and
+ out :: "nat stfun" and
+ q1 :: "nat list stfun" and
+ q2 :: "nat list stfun" and
+ qc :: "nat list stfun" and
- DBInit :: stpred
- DBEnq :: action
- DBDeq :: action
- DBPass :: action
- DBNext :: action
+ DBInit :: stpred and
+ DBEnq :: action and
+ DBDeq :: action and
+ DBPass :: action and
+ DBNext :: action and
DBuffer :: temporal
-
-axioms
- DB_base: "basevars (inp,mid,out,q1,q2)"
+where
+ DB_base: "basevars (inp,mid,out,q1,q2)" and
(* the concatenation of the two buffers *)
- qc_def: "PRED qc == PRED (q2 @ q1)"
+ qc_def: "PRED qc == PRED (q2 @ q1)" and
- DBInit_def: "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)"
- DBEnq_def: "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)"
- DBDeq_def: "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)"
+ DBInit_def: "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)" and
+ DBEnq_def: "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)" and
+ DBDeq_def: "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)" and
DBPass_def: "DBPass == ACT Deq inp q1 mid
& (q2$ = $q2 @ [ mid$ ])
- & (out$ = $out)"
- DBNext_def: "DBNext == ACT (DBEnq | DBDeq | DBPass)"
+ & (out$ = $out)" and
+ DBNext_def: "DBNext == ACT (DBEnq | DBDeq | DBPass)" and
DBuffer_def: "DBuffer == TEMP Init DBInit
& [][DBNext]_(inp,mid,out,q1,q2)
& WF(DBDeq)_(inp,mid,out,q1,q2)
--- a/src/HOL/TLA/Inc/Inc.thy Wed May 23 16:22:27 2012 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Wed May 23 16:53:12 2012 +0200
@@ -11,72 +11,71 @@
(* program counter as an enumeration type *)
datatype pcount = a | b | g
-consts
+axiomatization
(* program variables *)
- x :: "nat stfun"
- y :: "nat stfun"
- sem :: "nat stfun"
- pc1 :: "pcount stfun"
- pc2 :: "pcount stfun"
+ x :: "nat stfun" and
+ y :: "nat stfun" and
+ sem :: "nat stfun" and
+ pc1 :: "pcount stfun" and
+ pc2 :: "pcount stfun" and
(* names of actions and predicates *)
- M1 :: action
- M2 :: action
- N1 :: action
- N2 :: action
- alpha1 :: action
- alpha2 :: action
- beta1 :: action
- beta2 :: action
- gamma1 :: action
- gamma2 :: action
- InitPhi :: stpred
- InitPsi :: stpred
- PsiInv :: stpred
- PsiInv1 :: stpred
- PsiInv2 :: stpred
- PsiInv3 :: stpred
+ M1 :: action and
+ M2 :: action and
+ N1 :: action and
+ N2 :: action and
+ alpha1 :: action and
+ alpha2 :: action and
+ beta1 :: action and
+ beta2 :: action and
+ gamma1 :: action and
+ gamma2 :: action and
+ InitPhi :: stpred and
+ InitPsi :: stpred and
+ PsiInv :: stpred and
+ PsiInv1 :: stpred and
+ PsiInv2 :: stpred and
+ PsiInv3 :: stpred and
(* temporal formulas *)
- Phi :: temporal
+ Phi :: temporal and
Psi :: temporal
-
-axioms
+where
(* the "base" variables, required to compute enabledness predicates *)
- Inc_base: "basevars (x, y, sem, pc1, pc2)"
+ Inc_base: "basevars (x, y, sem, pc1, pc2)" and
(* definitions for high-level program *)
- InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0"
- M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y"
- M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x"
+ InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0" and
+ M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y" and
+ M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x" and
Phi_def: "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y)
- & WF(M1)_(x,y) & WF(M2)_(x,y)"
+ & WF(M1)_(x,y) & WF(M2)_(x,y)" and
(* definitions for low-level program *)
InitPsi_def: "InitPsi == PRED pc1 = #a & pc2 = #a
- & x = # 0 & y = # 0 & sem = # 1"
+ & x = # 0 & y = # 0 & sem = # 1" and
alpha1_def: "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
- & unchanged(x,y,pc2)"
+ & unchanged(x,y,pc2)" and
alpha2_def: "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
- & unchanged(x,y,pc1)"
+ & unchanged(x,y,pc1)" and
beta1_def: "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
- & unchanged(y,sem,pc2)"
+ & unchanged(y,sem,pc2)" and
beta2_def: "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
- & unchanged(x,sem,pc1)"
+ & unchanged(x,sem,pc1)" and
gamma1_def: "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
- & unchanged(x,y,pc2)"
+ & unchanged(x,y,pc2)" and
gamma2_def: "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
- & unchanged(x,y,pc1)"
- N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)"
- N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)"
+ & unchanged(x,y,pc1)" and
+ N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)" and
+ N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)" and
Psi_def: "Psi == TEMP Init InitPsi
& [][N1 | N2]_(x,y,sem,pc1,pc2)
& SF(N1)_(x,y,sem,pc1,pc2)
- & SF(N2)_(x,y,sem,pc1,pc2)"
+ & SF(N2)_(x,y,sem,pc1,pc2)" and
- PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a"
- PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
- PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
+ PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a" and
+ PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" and
+ PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" and
PsiInv_def: "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Wed May 23 16:22:27 2012 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Wed May 23 16:53:12 2012 +0200
@@ -25,14 +25,14 @@
(* the initial value stored in each memory cell *)
InitVal :: "Vals"
-axioms
+axiomatization where
(* basic assumptions about the above constants and predicates *)
- BadArgNoMemVal: "BadArg ~: MemVal"
- MemFailNoMemVal: "MemFailure ~: MemVal"
- InitValMemVal: "InitVal : MemVal"
- NotAResultNotVal: "NotAResult ~: MemVal"
- NotAResultNotOK: "NotAResult ~= OK"
- NotAResultNotBA: "NotAResult ~= BadArg"
+ BadArgNoMemVal: "BadArg ~: MemVal" and
+ MemFailNoMemVal: "MemFailure ~: MemVal" and
+ InitValMemVal: "InitVal : MemVal" and
+ NotAResultNotVal: "NotAResult ~: MemVal" and
+ NotAResultNotOK: "NotAResult ~= OK" and
+ NotAResultNotBA: "NotAResult ~= BadArg" and
NotAResultNotMF: "NotAResult ~= MemFailure"
lemmas [simp] =
--- a/src/HOL/TLA/Memory/RPCParameters.thy Wed May 23 16:22:27 2012 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Wed May 23 16:53:12 2012 +0200
@@ -28,11 +28,11 @@
IsLegalRcvArg :: "rpcOp => bool"
RPCRelayArg :: "rpcOp => memOp"
-axioms
+axiomatization where
(* RPCFailure is different from MemVals and exceptions *)
- RFNoMemVal: "RPCFailure ~: MemVal"
- NotAResultNotRF: "NotAResult ~= RPCFailure"
- OKNotRF: "OK ~= RPCFailure"
+ RFNoMemVal: "RPCFailure ~: MemVal" and
+ NotAResultNotRF: "NotAResult ~= RPCFailure" and
+ OKNotRF: "OK ~= RPCFailure" and
BANotRF: "BadArg ~= RPCFailure"
defs
--- a/src/HOL/TLA/TLA.thy Wed May 23 16:22:27 2012 +0200
+++ b/src/HOL/TLA/TLA.thy Wed May 23 16:53:12 2012 +0200
@@ -64,34 +64,39 @@
"_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
"_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
-axioms
+axiomatization where
(* 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"
+ dmd_def: "\<And>F. TEMP <>F == TEMP ~[]~F"
+
+axiomatization where
+ boxInit: "\<And>F. TEMP []F == TEMP []Init F" and
+ leadsto_def: "\<And>F G. TEMP F ~> G == TEMP [](Init F --> <>G)" and
+ stable_def: "\<And>P. TEMP stable P == TEMP []($P --> P$)" and
+ WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v" and
+ SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v" and
aall_def: "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)"
+axiomatization where
(* 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: "|- (ALL x. [](F x)) = ([](ALL x. F x))"
+ normalT: "\<And>F G. |- [](F --> G) --> ([]F --> []G)" and (* polymorphic *)
+ reflT: "\<And>F. |- []F --> F" and (* F::temporal *)
+ transT: "\<And>F. |- []F --> [][]F" and (* polymorphic *)
+ linT: "\<And>F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and
+ discT: "\<And>F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and
+ primeI: "\<And>P. |- []P --> Init P`" and
+ primeE: "\<And>P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and
+ indT: "\<And>P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and
+ allT: "\<And>F. |- (ALL x. [](F x)) = ([](ALL x. F x))"
- necT: "|- F ==> |- []F" (* polymorphic *)
+axiomatization where
+ necT: "\<And>F. |- F ==> |- []F" (* polymorphic *)
+axiomatization where
(* Flexible quantification: refinement mappings, history variables *)
- eexI: "|- F x --> (EEX x. F x)"
+ eexI: "|- F x --> (EEX x. F x)" and
eexE: "[| sigma |= (EEX x. F x); basevars vs;
(!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
- |] ==> G sigma"
+ |] ==> G sigma" and
history: "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"