# HG changeset patch # User wenzelm # Date 1337785605 -7200 # Node ID ce4345b06408547e6635c64a142a747ab6c7aa14 # Parent 8ba6438557bc64d00d9bf12039f3f1ed09d469ba# Parent 3119ad2b5ad388de9895def994f4e9c715272df2 merged diff -r 8ba6438557bc -r ce4345b06408 NEWS --- a/NEWS Wed May 23 16:03:38 2012 +0200 +++ b/NEWS Wed May 23 17:06:45 2012 +0200 @@ -4,6 +4,12 @@ New in this Isabelle version ---------------------------- +*** General *** + +* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which +is called fastforce / fast_force_tac already since Isabelle2011-1. + + New in Isabelle2012 (May 2012) ------------------------------ diff -r 8ba6438557bc -r ce4345b06408 doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Wed May 23 16:03:38 2012 +0200 +++ b/doc-src/IsarRef/Thy/Generic.thy Wed May 23 17:06:45 2012 +0200 @@ -1094,11 +1094,11 @@ search: it may, when backtracking from a failed proof attempt, undo even the step of proving a subgoal by assumption. - \item @{method fastforce}, @{method slowsimp}, @{method bestsimp} are - like @{method fast}, @{method slow}, @{method best}, respectively, - but use the Simplifier as additional wrapper. The name @{method fastforce}, - as opposed to @{text fastsimp}, reflects the behaviour of this popular - method better without requiring an understanding of its implementation. + \item @{method fastforce}, @{method slowsimp}, @{method bestsimp} + are like @{method fast}, @{method slow}, @{method best}, + respectively, but use the Simplifier as additional wrapper. The name + @{method fastforce}, reflects the behaviour of this popular method + better without requiring an understanding of its implementation. \item @{method deepen} works by exhaustive search up to a certain depth. The start depth is 4 (unless specified explicitly), and the diff -r 8ba6438557bc -r ce4345b06408 doc-src/IsarRef/Thy/document/Generic.tex --- a/doc-src/IsarRef/Thy/document/Generic.tex Wed May 23 16:03:38 2012 +0200 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed May 23 17:06:45 2012 +0200 @@ -1682,11 +1682,11 @@ search: it may, when backtracking from a failed proof attempt, undo even the step of proving a subgoal by assumption. - \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} are - like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively, - but use the Simplifier as additional wrapper. The name \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, - as opposed to \isa{fastsimp}, reflects the behaviour of this popular - method better without requiring an understanding of its implementation. + \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} + are like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, + respectively, but use the Simplifier as additional wrapper. The name + \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, reflects the behaviour of this popular method + better without requiring an understanding of its implementation. \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain depth. The start depth is 4 (unless specified explicitly), and the diff -r 8ba6438557bc -r ce4345b06408 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/CCL/CCL.thy Wed May 23 17:06:45 2012 +0200 @@ -349,7 +349,7 @@ lemma po_lam: "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))" apply (rule poXH [THEN iff_trans]) - apply fastsimp + apply fastforce done lemmas ccl_porews = po_bot po_pair po_lam diff -r 8ba6438557bc -r ce4345b06408 src/CCL/Hered.thy --- a/src/CCL/Hered.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/CCL/Hered.thy Wed May 23 17:06:45 2012 +0200 @@ -118,13 +118,13 @@ by (simp add: subsetXH UnitXH HTT_rews) lemma BoolF: "Bool <= HTT" - by (fastsimp simp: subsetXH BoolXH iff: HTT_rews) + by (fastforce simp: subsetXH BoolXH iff: HTT_rews) lemma PlusF: "[| A <= HTT; B <= HTT |] ==> A + B <= HTT" - by (fastsimp simp: subsetXH PlusXH iff: HTT_rews) + by (fastforce simp: subsetXH PlusXH iff: HTT_rews) lemma SigmaF: "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT" - by (fastsimp simp: subsetXH SgXH HTT_rews) + by (fastforce simp: subsetXH SgXH HTT_rews) (*** Formation Rules for Recursive types - using coinduction these only need ***) @@ -135,7 +135,7 @@ apply (simp add: subsetXH) apply clarify apply (erule Nat_ind) - apply (fastsimp iff: HTT_rews)+ + apply (fastforce iff: HTT_rews)+ done lemma NatF: "Nat <= HTT" diff -r 8ba6438557bc -r ce4345b06408 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/CCL/Wfd.thy Wed May 23 17:06:45 2012 +0200 @@ -209,18 +209,18 @@ apply (unfold Wfd_def) apply clarify apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *}) - apply (fastsimp iff: NatPRXH) + apply (fastforce iff: NatPRXH) apply (erule Nat_ind) - apply (fastsimp iff: NatPRXH)+ + apply (fastforce iff: NatPRXH)+ done lemma ListPR_wf: "Wfd(ListPR(A))" apply (unfold Wfd_def) apply clarify apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *}) - apply (fastsimp iff: ListPRXH) + apply (fastforce iff: ListPRXH) apply (erule List_ind) - apply (fastsimp iff: ListPRXH)+ + apply (fastforce iff: ListPRXH)+ done diff -r 8ba6438557bc -r ce4345b06408 src/CCL/ex/Stream.thy --- a/src/CCL/ex/Stream.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/CCL/ex/Stream.thy Wed May 23 17:06:45 2012 +0200 @@ -33,7 +33,7 @@ apply safe apply (drule ListsXH [THEN iffD1]) apply (tactic "EQgen_tac @{context} [] 1") - apply fastsimp + apply fastforce done (*** Mapping the identity function leaves a list unchanged ***) diff -r 8ba6438557bc -r ce4345b06408 src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/HOL/TLA/Action.thy Wed May 23 17:06:45 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 8ba6438557bc -r ce4345b06408 src/HOL/TLA/Buffer/DBuffer.thy --- a/src/HOL/TLA/Buffer/DBuffer.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/HOL/TLA/Buffer/DBuffer.thy Wed May 23 17:06:45 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 8ba6438557bc -r ce4345b06408 src/HOL/TLA/Inc/Inc.thy --- a/src/HOL/TLA/Inc/Inc.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/HOL/TLA/Inc/Inc.thy Wed May 23 17:06:45 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 8ba6438557bc -r ce4345b06408 src/HOL/TLA/Memory/MemoryParameters.thy --- a/src/HOL/TLA/Memory/MemoryParameters.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy Wed May 23 17:06:45 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 8ba6438557bc -r ce4345b06408 src/HOL/TLA/Memory/RPCParameters.thy --- a/src/HOL/TLA/Memory/RPCParameters.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/HOL/TLA/Memory/RPCParameters.thy Wed May 23 17:06:45 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 8ba6438557bc -r ce4345b06408 src/HOL/TLA/TLA.thy --- a/src/HOL/TLA/TLA.thy Wed May 23 16:03:38 2012 +0200 +++ b/src/HOL/TLA/TLA.thy Wed May 23 17:06:45 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)" diff -r 8ba6438557bc -r ce4345b06408 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Wed May 23 16:03:38 2012 +0200 +++ b/src/Provers/clasimp.ML Wed May 23 17:06:45 2012 +0200 @@ -173,14 +173,12 @@ (* basic combinations *) -fun fast_simp_tac ctxt i = - let val _ = legacy_feature "Old name 'fastsimp' - use 'fastforce' instead" - in Classical.fast_tac (addss ctxt) i end; - val fast_force_tac = Classical.fast_tac o addss; val slow_simp_tac = Classical.slow_tac o addss; val best_simp_tac = Classical.best_tac o addss; + + (** concrete syntax **) (* attributes *) @@ -221,7 +219,6 @@ val clasimp_setup = Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #> - Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #> Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #> Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #> Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>