merged
authorwenzelm
Wed May 23 17:06:45 2012 +0200 (2012-05-23)
changeset 47969ce4345b06408
parent 47965 8ba6438557bc
parent 47968 3119ad2b5ad3
child 47970 257fc09aa8a1
merged
     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" #>