--- 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)
------------------------------
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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 ***)
--- 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 <A>_v == ACT (A & ~ unchanged v)"
--- 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)
--- 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<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: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] =
--- 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
--- 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\<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)"
--- 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" #>