1.1 --- a/NEWS Wed May 23 16:03:38 2012 +0200
1.2 +++ b/NEWS Wed May 23 17:06:45 2012 +0200
1.3 @@ -4,6 +4,12 @@
1.4 New in this Isabelle version
1.5 ----------------------------
1.6
1.7 +*** General ***
1.8 +
1.9 +* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
1.10 +is called fastforce / fast_force_tac already since Isabelle2011-1.
1.11 +
1.12 +
1.13
1.14 New in Isabelle2012 (May 2012)
1.15 ------------------------------
2.1 --- a/doc-src/IsarRef/Thy/Generic.thy Wed May 23 16:03:38 2012 +0200
2.2 +++ b/doc-src/IsarRef/Thy/Generic.thy Wed May 23 17:06:45 2012 +0200
2.3 @@ -1094,11 +1094,11 @@
2.4 search: it may, when backtracking from a failed proof attempt, undo
2.5 even the step of proving a subgoal by assumption.
2.6
2.7 - \item @{method fastforce}, @{method slowsimp}, @{method bestsimp} are
2.8 - like @{method fast}, @{method slow}, @{method best}, respectively,
2.9 - but use the Simplifier as additional wrapper. The name @{method fastforce},
2.10 - as opposed to @{text fastsimp}, reflects the behaviour of this popular
2.11 - method better without requiring an understanding of its implementation.
2.12 + \item @{method fastforce}, @{method slowsimp}, @{method bestsimp}
2.13 + are like @{method fast}, @{method slow}, @{method best},
2.14 + respectively, but use the Simplifier as additional wrapper. The name
2.15 + @{method fastforce}, reflects the behaviour of this popular method
2.16 + better without requiring an understanding of its implementation.
2.17
2.18 \item @{method deepen} works by exhaustive search up to a certain
2.19 depth. The start depth is 4 (unless specified explicitly), and the
3.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex Wed May 23 16:03:38 2012 +0200
3.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed May 23 17:06:45 2012 +0200
3.3 @@ -1682,11 +1682,11 @@
3.4 search: it may, when backtracking from a failed proof attempt, undo
3.5 even the step of proving a subgoal by assumption.
3.6
3.7 - \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} are
3.8 - like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
3.9 - but use the Simplifier as additional wrapper. The name \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}},
3.10 - as opposed to \isa{fastsimp}, reflects the behaviour of this popular
3.11 - method better without requiring an understanding of its implementation.
3.12 + \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}
3.13 + are like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}},
3.14 + respectively, but use the Simplifier as additional wrapper. The name
3.15 + \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, reflects the behaviour of this popular method
3.16 + better without requiring an understanding of its implementation.
3.17
3.18 \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain
3.19 depth. The start depth is 4 (unless specified explicitly), and the
4.1 --- a/src/CCL/CCL.thy Wed May 23 16:03:38 2012 +0200
4.2 +++ b/src/CCL/CCL.thy Wed May 23 17:06:45 2012 +0200
4.3 @@ -349,7 +349,7 @@
4.4
4.5 lemma po_lam: "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))"
4.6 apply (rule poXH [THEN iff_trans])
4.7 - apply fastsimp
4.8 + apply fastforce
4.9 done
4.10
4.11 lemmas ccl_porews = po_bot po_pair po_lam
5.1 --- a/src/CCL/Hered.thy Wed May 23 16:03:38 2012 +0200
5.2 +++ b/src/CCL/Hered.thy Wed May 23 17:06:45 2012 +0200
5.3 @@ -118,13 +118,13 @@
5.4 by (simp add: subsetXH UnitXH HTT_rews)
5.5
5.6 lemma BoolF: "Bool <= HTT"
5.7 - by (fastsimp simp: subsetXH BoolXH iff: HTT_rews)
5.8 + by (fastforce simp: subsetXH BoolXH iff: HTT_rews)
5.9
5.10 lemma PlusF: "[| A <= HTT; B <= HTT |] ==> A + B <= HTT"
5.11 - by (fastsimp simp: subsetXH PlusXH iff: HTT_rews)
5.12 + by (fastforce simp: subsetXH PlusXH iff: HTT_rews)
5.13
5.14 lemma SigmaF: "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"
5.15 - by (fastsimp simp: subsetXH SgXH HTT_rews)
5.16 + by (fastforce simp: subsetXH SgXH HTT_rews)
5.17
5.18
5.19 (*** Formation Rules for Recursive types - using coinduction these only need ***)
5.20 @@ -135,7 +135,7 @@
5.21 apply (simp add: subsetXH)
5.22 apply clarify
5.23 apply (erule Nat_ind)
5.24 - apply (fastsimp iff: HTT_rews)+
5.25 + apply (fastforce iff: HTT_rews)+
5.26 done
5.27
5.28 lemma NatF: "Nat <= HTT"
6.1 --- a/src/CCL/Wfd.thy Wed May 23 16:03:38 2012 +0200
6.2 +++ b/src/CCL/Wfd.thy Wed May 23 17:06:45 2012 +0200
6.3 @@ -209,18 +209,18 @@
6.4 apply (unfold Wfd_def)
6.5 apply clarify
6.6 apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
6.7 - apply (fastsimp iff: NatPRXH)
6.8 + apply (fastforce iff: NatPRXH)
6.9 apply (erule Nat_ind)
6.10 - apply (fastsimp iff: NatPRXH)+
6.11 + apply (fastforce iff: NatPRXH)+
6.12 done
6.13
6.14 lemma ListPR_wf: "Wfd(ListPR(A))"
6.15 apply (unfold Wfd_def)
6.16 apply clarify
6.17 apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
6.18 - apply (fastsimp iff: ListPRXH)
6.19 + apply (fastforce iff: ListPRXH)
6.20 apply (erule List_ind)
6.21 - apply (fastsimp iff: ListPRXH)+
6.22 + apply (fastforce iff: ListPRXH)+
6.23 done
6.24
6.25
7.1 --- a/src/CCL/ex/Stream.thy Wed May 23 16:03:38 2012 +0200
7.2 +++ b/src/CCL/ex/Stream.thy Wed May 23 17:06:45 2012 +0200
7.3 @@ -33,7 +33,7 @@
7.4 apply safe
7.5 apply (drule ListsXH [THEN iffD1])
7.6 apply (tactic "EQgen_tac @{context} [] 1")
7.7 - apply fastsimp
7.8 + apply fastforce
7.9 done
7.10
7.11 (*** Mapping the identity function leaves a list unchanged ***)
8.1 --- a/src/HOL/TLA/Action.thy Wed May 23 16:03:38 2012 +0200
8.2 +++ b/src/HOL/TLA/Action.thy Wed May 23 17:06:45 2012 +0200
8.3 @@ -58,11 +58,13 @@
8.4 "s |= Enabled A" <= "_Enabled A s"
8.5 "w |= unchanged f" <= "_unchanged f w"
8.6
8.7 -axioms
8.8 - unl_before: "(ACT $v) (s,t) == v s"
8.9 - unl_after: "(ACT v$) (s,t) == v t"
8.10 +axiomatization where
8.11 + unl_before: "(ACT $v) (s,t) == v s" and
8.12 + unl_after: "(ACT v$) (s,t) == v t" and
8.13
8.14 unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
8.15 +
8.16 +defs
8.17 square_def: "ACT [A]_v == ACT (A | unchanged v)"
8.18 angle_def: "ACT <A>_v == ACT (A & ~ unchanged v)"
8.19
9.1 --- a/src/HOL/TLA/Buffer/DBuffer.thy Wed May 23 16:03:38 2012 +0200
9.2 +++ b/src/HOL/TLA/Buffer/DBuffer.thy Wed May 23 17:06:45 2012 +0200
9.3 @@ -8,35 +8,34 @@
9.4 imports Buffer
9.5 begin
9.6
9.7 -consts
9.8 +axiomatization
9.9 (* implementation variables *)
9.10 - inp :: "nat stfun"
9.11 - mid :: "nat stfun"
9.12 - out :: "nat stfun"
9.13 - q1 :: "nat list stfun"
9.14 - q2 :: "nat list stfun"
9.15 - qc :: "nat list stfun"
9.16 + inp :: "nat stfun" and
9.17 + mid :: "nat stfun" and
9.18 + out :: "nat stfun" and
9.19 + q1 :: "nat list stfun" and
9.20 + q2 :: "nat list stfun" and
9.21 + qc :: "nat list stfun" and
9.22
9.23 - DBInit :: stpred
9.24 - DBEnq :: action
9.25 - DBDeq :: action
9.26 - DBPass :: action
9.27 - DBNext :: action
9.28 + DBInit :: stpred and
9.29 + DBEnq :: action and
9.30 + DBDeq :: action and
9.31 + DBPass :: action and
9.32 + DBNext :: action and
9.33 DBuffer :: temporal
9.34 -
9.35 -axioms
9.36 - DB_base: "basevars (inp,mid,out,q1,q2)"
9.37 +where
9.38 + DB_base: "basevars (inp,mid,out,q1,q2)" and
9.39
9.40 (* the concatenation of the two buffers *)
9.41 - qc_def: "PRED qc == PRED (q2 @ q1)"
9.42 + qc_def: "PRED qc == PRED (q2 @ q1)" and
9.43
9.44 - DBInit_def: "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)"
9.45 - DBEnq_def: "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)"
9.46 - DBDeq_def: "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)"
9.47 + DBInit_def: "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)" and
9.48 + DBEnq_def: "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)" and
9.49 + DBDeq_def: "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)" and
9.50 DBPass_def: "DBPass == ACT Deq inp q1 mid
9.51 & (q2$ = $q2 @ [ mid$ ])
9.52 - & (out$ = $out)"
9.53 - DBNext_def: "DBNext == ACT (DBEnq | DBDeq | DBPass)"
9.54 + & (out$ = $out)" and
9.55 + DBNext_def: "DBNext == ACT (DBEnq | DBDeq | DBPass)" and
9.56 DBuffer_def: "DBuffer == TEMP Init DBInit
9.57 & [][DBNext]_(inp,mid,out,q1,q2)
9.58 & WF(DBDeq)_(inp,mid,out,q1,q2)
10.1 --- a/src/HOL/TLA/Inc/Inc.thy Wed May 23 16:03:38 2012 +0200
10.2 +++ b/src/HOL/TLA/Inc/Inc.thy Wed May 23 17:06:45 2012 +0200
10.3 @@ -11,72 +11,71 @@
10.4 (* program counter as an enumeration type *)
10.5 datatype pcount = a | b | g
10.6
10.7 -consts
10.8 +axiomatization
10.9 (* program variables *)
10.10 - x :: "nat stfun"
10.11 - y :: "nat stfun"
10.12 - sem :: "nat stfun"
10.13 - pc1 :: "pcount stfun"
10.14 - pc2 :: "pcount stfun"
10.15 + x :: "nat stfun" and
10.16 + y :: "nat stfun" and
10.17 + sem :: "nat stfun" and
10.18 + pc1 :: "pcount stfun" and
10.19 + pc2 :: "pcount stfun" and
10.20
10.21 (* names of actions and predicates *)
10.22 - M1 :: action
10.23 - M2 :: action
10.24 - N1 :: action
10.25 - N2 :: action
10.26 - alpha1 :: action
10.27 - alpha2 :: action
10.28 - beta1 :: action
10.29 - beta2 :: action
10.30 - gamma1 :: action
10.31 - gamma2 :: action
10.32 - InitPhi :: stpred
10.33 - InitPsi :: stpred
10.34 - PsiInv :: stpred
10.35 - PsiInv1 :: stpred
10.36 - PsiInv2 :: stpred
10.37 - PsiInv3 :: stpred
10.38 + M1 :: action and
10.39 + M2 :: action and
10.40 + N1 :: action and
10.41 + N2 :: action and
10.42 + alpha1 :: action and
10.43 + alpha2 :: action and
10.44 + beta1 :: action and
10.45 + beta2 :: action and
10.46 + gamma1 :: action and
10.47 + gamma2 :: action and
10.48 + InitPhi :: stpred and
10.49 + InitPsi :: stpred and
10.50 + PsiInv :: stpred and
10.51 + PsiInv1 :: stpred and
10.52 + PsiInv2 :: stpred and
10.53 + PsiInv3 :: stpred and
10.54
10.55 (* temporal formulas *)
10.56 - Phi :: temporal
10.57 + Phi :: temporal and
10.58 Psi :: temporal
10.59 -
10.60 -axioms
10.61 +where
10.62 (* the "base" variables, required to compute enabledness predicates *)
10.63 - Inc_base: "basevars (x, y, sem, pc1, pc2)"
10.64 + Inc_base: "basevars (x, y, sem, pc1, pc2)" and
10.65
10.66 (* definitions for high-level program *)
10.67 - InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0"
10.68 - M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y"
10.69 - M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x"
10.70 + InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0" and
10.71 + M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y" and
10.72 + M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x" and
10.73 Phi_def: "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y)
10.74 - & WF(M1)_(x,y) & WF(M2)_(x,y)"
10.75 + & WF(M1)_(x,y) & WF(M2)_(x,y)" and
10.76
10.77 (* definitions for low-level program *)
10.78 InitPsi_def: "InitPsi == PRED pc1 = #a & pc2 = #a
10.79 - & x = # 0 & y = # 0 & sem = # 1"
10.80 + & x = # 0 & y = # 0 & sem = # 1" and
10.81 alpha1_def: "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
10.82 - & unchanged(x,y,pc2)"
10.83 + & unchanged(x,y,pc2)" and
10.84 alpha2_def: "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
10.85 - & unchanged(x,y,pc1)"
10.86 + & unchanged(x,y,pc1)" and
10.87 beta1_def: "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
10.88 - & unchanged(y,sem,pc2)"
10.89 + & unchanged(y,sem,pc2)" and
10.90 beta2_def: "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
10.91 - & unchanged(x,sem,pc1)"
10.92 + & unchanged(x,sem,pc1)" and
10.93 gamma1_def: "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
10.94 - & unchanged(x,y,pc2)"
10.95 + & unchanged(x,y,pc2)" and
10.96 gamma2_def: "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
10.97 - & unchanged(x,y,pc1)"
10.98 - N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)"
10.99 - N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)"
10.100 + & unchanged(x,y,pc1)" and
10.101 + N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)" and
10.102 + N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)" and
10.103 Psi_def: "Psi == TEMP Init InitPsi
10.104 & [][N1 | N2]_(x,y,sem,pc1,pc2)
10.105 & SF(N1)_(x,y,sem,pc1,pc2)
10.106 - & SF(N2)_(x,y,sem,pc1,pc2)"
10.107 + & SF(N2)_(x,y,sem,pc1,pc2)" and
10.108
10.109 - PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a"
10.110 - PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
10.111 - PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
10.112 + PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a" and
10.113 + PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" and
10.114 + PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" and
10.115 PsiInv_def: "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
10.116
10.117
11.1 --- a/src/HOL/TLA/Memory/MemoryParameters.thy Wed May 23 16:03:38 2012 +0200
11.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy Wed May 23 17:06:45 2012 +0200
11.3 @@ -25,14 +25,14 @@
11.4 (* the initial value stored in each memory cell *)
11.5 InitVal :: "Vals"
11.6
11.7 -axioms
11.8 +axiomatization where
11.9 (* basic assumptions about the above constants and predicates *)
11.10 - BadArgNoMemVal: "BadArg ~: MemVal"
11.11 - MemFailNoMemVal: "MemFailure ~: MemVal"
11.12 - InitValMemVal: "InitVal : MemVal"
11.13 - NotAResultNotVal: "NotAResult ~: MemVal"
11.14 - NotAResultNotOK: "NotAResult ~= OK"
11.15 - NotAResultNotBA: "NotAResult ~= BadArg"
11.16 + BadArgNoMemVal: "BadArg ~: MemVal" and
11.17 + MemFailNoMemVal: "MemFailure ~: MemVal" and
11.18 + InitValMemVal: "InitVal : MemVal" and
11.19 + NotAResultNotVal: "NotAResult ~: MemVal" and
11.20 + NotAResultNotOK: "NotAResult ~= OK" and
11.21 + NotAResultNotBA: "NotAResult ~= BadArg" and
11.22 NotAResultNotMF: "NotAResult ~= MemFailure"
11.23
11.24 lemmas [simp] =
12.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy Wed May 23 16:03:38 2012 +0200
12.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy Wed May 23 17:06:45 2012 +0200
12.3 @@ -28,11 +28,11 @@
12.4 IsLegalRcvArg :: "rpcOp => bool"
12.5 RPCRelayArg :: "rpcOp => memOp"
12.6
12.7 -axioms
12.8 +axiomatization where
12.9 (* RPCFailure is different from MemVals and exceptions *)
12.10 - RFNoMemVal: "RPCFailure ~: MemVal"
12.11 - NotAResultNotRF: "NotAResult ~= RPCFailure"
12.12 - OKNotRF: "OK ~= RPCFailure"
12.13 + RFNoMemVal: "RPCFailure ~: MemVal" and
12.14 + NotAResultNotRF: "NotAResult ~= RPCFailure" and
12.15 + OKNotRF: "OK ~= RPCFailure" and
12.16 BANotRF: "BadArg ~= RPCFailure"
12.17
12.18 defs
13.1 --- a/src/HOL/TLA/TLA.thy Wed May 23 16:03:38 2012 +0200
13.2 +++ b/src/HOL/TLA/TLA.thy Wed May 23 17:06:45 2012 +0200
13.3 @@ -64,34 +64,39 @@
13.4 "_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
13.5 "_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
13.6
13.7 -axioms
13.8 +axiomatization where
13.9 (* Definitions of derived operators *)
13.10 - dmd_def: "TEMP <>F == TEMP ~[]~F"
13.11 - boxInit: "TEMP []F == TEMP []Init F"
13.12 - leadsto_def: "TEMP F ~> G == TEMP [](Init F --> <>G)"
13.13 - stable_def: "TEMP stable P == TEMP []($P --> P$)"
13.14 - WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v"
13.15 - SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v"
13.16 + dmd_def: "\<And>F. TEMP <>F == TEMP ~[]~F"
13.17 +
13.18 +axiomatization where
13.19 + boxInit: "\<And>F. TEMP []F == TEMP []Init F" and
13.20 + leadsto_def: "\<And>F G. TEMP F ~> G == TEMP [](Init F --> <>G)" and
13.21 + stable_def: "\<And>P. TEMP stable P == TEMP []($P --> P$)" and
13.22 + WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v" and
13.23 + SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v" and
13.24 aall_def: "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)"
13.25
13.26 +axiomatization where
13.27 (* Base axioms for raw TLA. *)
13.28 - normalT: "|- [](F --> G) --> ([]F --> []G)" (* polymorphic *)
13.29 - reflT: "|- []F --> F" (* F::temporal *)
13.30 - transT: "|- []F --> [][]F" (* polymorphic *)
13.31 - linT: "|- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))"
13.32 - discT: "|- [](F --> <>(~F & <>F)) --> (F --> []<>F)"
13.33 - primeI: "|- []P --> Init P`"
13.34 - primeE: "|- [](Init P --> []F) --> Init P` --> (F --> []F)"
13.35 - indT: "|- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F"
13.36 - allT: "|- (ALL x. [](F x)) = ([](ALL x. F x))"
13.37 + normalT: "\<And>F G. |- [](F --> G) --> ([]F --> []G)" and (* polymorphic *)
13.38 + reflT: "\<And>F. |- []F --> F" and (* F::temporal *)
13.39 + transT: "\<And>F. |- []F --> [][]F" and (* polymorphic *)
13.40 + linT: "\<And>F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and
13.41 + discT: "\<And>F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and
13.42 + primeI: "\<And>P. |- []P --> Init P`" and
13.43 + primeE: "\<And>P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and
13.44 + indT: "\<And>P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and
13.45 + allT: "\<And>F. |- (ALL x. [](F x)) = ([](ALL x. F x))"
13.46
13.47 - necT: "|- F ==> |- []F" (* polymorphic *)
13.48 +axiomatization where
13.49 + necT: "\<And>F. |- F ==> |- []F" (* polymorphic *)
13.50
13.51 +axiomatization where
13.52 (* Flexible quantification: refinement mappings, history variables *)
13.53 - eexI: "|- F x --> (EEX x. F x)"
13.54 + eexI: "|- F x --> (EEX x. F x)" and
13.55 eexE: "[| sigma |= (EEX x. F x); basevars vs;
13.56 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
13.57 - |] ==> G sigma"
13.58 + |] ==> G sigma" and
13.59 history: "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
13.60
13.61
14.1 --- a/src/Provers/clasimp.ML Wed May 23 16:03:38 2012 +0200
14.2 +++ b/src/Provers/clasimp.ML Wed May 23 17:06:45 2012 +0200
14.3 @@ -173,14 +173,12 @@
14.4
14.5 (* basic combinations *)
14.6
14.7 -fun fast_simp_tac ctxt i =
14.8 - let val _ = legacy_feature "Old name 'fastsimp' - use 'fastforce' instead"
14.9 - in Classical.fast_tac (addss ctxt) i end;
14.10 -
14.11 val fast_force_tac = Classical.fast_tac o addss;
14.12 val slow_simp_tac = Classical.slow_tac o addss;
14.13 val best_simp_tac = Classical.best_tac o addss;
14.14
14.15 +
14.16 +
14.17 (** concrete syntax **)
14.18
14.19 (* attributes *)
14.20 @@ -221,7 +219,6 @@
14.21
14.22 val clasimp_setup =
14.23 Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
14.24 - Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #>
14.25 Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
14.26 Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
14.27 Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>