# HG changeset patch # User wenzelm # Date 1337784792 -7200 # Node ID 3119ad2b5ad388de9895def994f4e9c715272df2 # Parent c422128d388956469335b75a4bfe13a9adf6c952 eliminated old 'axioms'; diff -r c422128d3889 -r 3119ad2b5ad3 src/HOL/TLA/Action.thy --- 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 _v == ACT (A & ~ unchanged v)" diff -r c422128d3889 -r 3119ad2b5ad3 src/HOL/TLA/Buffer/DBuffer.thy --- 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) diff -r c422128d3889 -r 3119ad2b5ad3 src/HOL/TLA/Inc/Inc.thy --- 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 - & unchanged(x,y,pc2)" + & unchanged(x,y,pc2)" and alpha2_def: "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc - & 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)" diff -r c422128d3889 -r 3119ad2b5ad3 src/HOL/TLA/Memory/MemoryParameters.thy --- 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] = diff -r c422128d3889 -r 3119ad2b5ad3 src/HOL/TLA/Memory/RPCParameters.thy --- 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 diff -r c422128d3889 -r 3119ad2b5ad3 src/HOL/TLA/TLA.thy --- 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\\ _./ _)" [0,10] 10) "_AAll" :: "[idts, lift] => lift" ("(3\\ _./ _)" [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(_v) --> []<>_v" - SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(_v) --> []<>_v" + dmd_def: "\F. TEMP <>F == TEMP ~[]~F" + +axiomatization where + boxInit: "\F. TEMP []F == TEMP []Init F" and + leadsto_def: "\F G. TEMP F ~> G == TEMP [](Init F --> <>G)" and + stable_def: "\P. TEMP stable P == TEMP []($P --> P$)" and + WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(_v) --> []<>_v" and + SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(_v) --> []<>_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: "\F G. |- [](F --> G) --> ([]F --> []G)" and (* polymorphic *) + reflT: "\F. |- []F --> F" and (* F::temporal *) + transT: "\F. |- []F --> [][]F" and (* polymorphic *) + linT: "\F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and + discT: "\F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and + primeI: "\P. |- []P --> Init P`" and + primeE: "\P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and + indT: "\P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and + allT: "\F. |- (ALL x. [](F x)) = ([](ALL x. F x))" - necT: "|- F ==> |- []F" (* polymorphic *) +axiomatization where + necT: "\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)"