--- a/NEWS Sat Mar 06 15:34:29 2010 +0100
+++ b/NEWS Sat Mar 06 15:39:16 2010 +0100
@@ -58,6 +58,9 @@
* Type constructors admit general mixfix syntax, not just infix.
+* Use of cumulative prems via "!" in some proof methods has been
+discontinued (legacy feature).
+
*** Pure ***
--- a/doc-src/IsarRef/Thy/Generic.thy Sat Mar 06 15:34:29 2010 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Sat Mar 06 15:39:16 2010 +0100
@@ -364,7 +364,7 @@
\indexouternonterm{simpmod}
\begin{rail}
- ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
+ ('simp' | 'simp\_all') opt? (simpmod *)
;
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
@@ -404,9 +404,7 @@
proofs this is usually quite well behaved in practice: just the
local premises of the actual goal are involved, additional facts may
be inserted via explicit forward-chaining (via @{command "then"},
- @{command "from"}, @{command "using"} etc.). The full context of
- premises is only included if the ``@{text "!"}'' (bang) argument is
- given, which should be used with some care, though.
+ @{command "from"}, @{command "using"} etc.).
Additional Simplifier options may be specified to tune the behavior
further (mostly for unstructured scripts with many accidental local
@@ -603,9 +601,9 @@
\indexouternonterm{clamod}
\begin{rail}
- 'blast' ('!' ?) nat? (clamod *)
+ 'blast' nat? (clamod *)
;
- ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
+ ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *)
;
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
@@ -629,9 +627,7 @@
Any of the above methods support additional modifiers of the context
of classical rules. Their semantics is analogous to the attributes
given before. Facts provided by forward chaining are inserted into
- the goal before commencing proof search. The ``@{text
- "!"}''~argument causes the full context of assumptions to be
- included as well.
+ the goal before commencing proof search.
*}
@@ -649,9 +645,9 @@
\indexouternonterm{clasimpmod}
\begin{rail}
- 'auto' '!'? (nat nat)? (clasimpmod *)
+ 'auto' (nat nat)? (clasimpmod *)
;
- ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
+ ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *)
;
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
@@ -674,8 +670,7 @@
here.
Facts provided by forward chaining are inserted into the goal before
- doing the search. The ``@{text "!"}'' argument causes the full
- context of assumptions to be included as well.
+ doing the search.
\end{description}
*}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 06 15:34:29 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 06 15:39:16 2010 +0100
@@ -795,16 +795,15 @@
\end{matharray}
\begin{rail}
- 'iprover' ('!' ?) ( rulemod * )
+ 'iprover' ( rulemod * )
;
\end{rail}
The @{method (HOL) iprover} method performs intuitionistic proof
search, depending on specifically declared rules from the context,
or given as explicit arguments. Chained facts are inserted into the
- goal before commencing proof search; ``@{method (HOL) iprover}@{text
- "!"}'' means to include the current @{fact prems} as well.
-
+ goal before commencing proof search.
+
Rules need to be classified as @{attribute (Pure) intro},
@{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
``@{text "!"}'' indicator refers to ``safe'' rules, which may be
--- a/doc-src/IsarRef/Thy/document/Generic.tex Sat Mar 06 15:34:29 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sat Mar 06 15:39:16 2010 +0100
@@ -384,7 +384,7 @@
\indexouternonterm{simpmod}
\begin{rail}
- ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
+ ('simp' | 'simp\_all') opt? (simpmod *)
;
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
@@ -424,9 +424,7 @@
proofs this is usually quite well behaved in practice: just the
local premises of the actual goal are involved, additional facts may
be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
- \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full context of
- premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) argument is
- given, which should be used with some care, though.
+ \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.).
Additional Simplifier options may be specified to tune the behavior
further (mostly for unstructured scripts with many accidental local
@@ -626,9 +624,9 @@
\indexouternonterm{clamod}
\begin{rail}
- 'blast' ('!' ?) nat? (clamod *)
+ 'blast' nat? (clamod *)
;
- ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
+ ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *)
;
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
@@ -650,8 +648,7 @@
Any of the above methods support additional modifiers of the context
of classical rules. Their semantics is analogous to the attributes
given before. Facts provided by forward chaining are inserted into
- the goal before commencing proof search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''~argument causes the full context of assumptions to be
- included as well.%
+ the goal before commencing proof search.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -671,9 +668,9 @@
\indexouternonterm{clasimpmod}
\begin{rail}
- 'auto' '!'? (nat nat)? (clasimpmod *)
+ 'auto' (nat nat)? (clasimpmod *)
;
- ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
+ ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *)
;
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
@@ -694,8 +691,7 @@
here.
Facts provided by forward chaining are inserted into the goal before
- doing the search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' argument causes the full
- context of assumptions to be included as well.
+ doing the search.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 06 15:34:29 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 06 15:39:16 2010 +0100
@@ -805,15 +805,15 @@
\end{matharray}
\begin{rail}
- 'iprover' ('!' ?) ( rulemod * )
+ 'iprover' ( rulemod * )
;
\end{rail}
The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
search, depending on specifically declared rules from the context,
or given as explicit arguments. Chained facts are inserted into the
- goal before commencing proof search; ``\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
-
+ goal before commencing proof search.
+
Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
--- a/src/Provers/blast.ML Sat Mar 06 15:34:29 2010 +0100
+++ b/src/Provers/blast.ML Sat Mar 06 15:39:16 2010 +0100
@@ -57,7 +57,7 @@
safe0_netpair: netpair, safep_netpair: netpair,
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
val cla_modifiers: Method.modifier parser list
- val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
+ val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
end;
signature BLAST =
@@ -1309,10 +1309,9 @@
val setup =
setup_depth_limit #>
Method.setup @{binding blast}
- (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
- Method.sections Data.cla_modifiers >>
- (fn (prems, NONE) => Data.cla_meth' blast_tac prems
- | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
+ (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >>
+ (fn NONE => Data.cla_meth' blast_tac
+ | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
"classical tableau prover";
end;
--- a/src/Provers/clasimp.ML Sat Mar 06 15:34:29 2010 +0100
+++ b/src/Provers/clasimp.ML Sat Mar 06 15:39:16 2010 +0100
@@ -258,21 +258,21 @@
(* methods *)
-fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (clasimpset_of ctxt));
+fun clasimp_meth tac ctxt = METHOD (fn facts =>
+ ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt));
-fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
+fun clasimp_meth' tac ctxt = METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt)));
fun clasimp_method' tac =
- Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
+ Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
val auto_method =
- Args.bang_facts -- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
- Method.sections clasimp_modifiers >>
- (fn (prems, NONE) => clasimp_meth (CHANGED_PROP o auto_tac) prems
- | (prems, SOME (m, n)) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)) prems);
+ Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
+ Method.sections clasimp_modifiers >>
+ (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
+ | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
(* theory setup *)
--- a/src/Provers/classical.ML Sat Mar 06 15:34:29 2010 +0100
+++ b/src/Provers/classical.ML Sat Mar 06 15:39:16 2010 +0100
@@ -125,8 +125,8 @@
val haz_intro: int option -> attribute
val rule_del: attribute
val cla_modifiers: Method.modifier parser list
- val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
- val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
+ val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
+ val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
val setup: theory -> theory
@@ -969,14 +969,14 @@
Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
Args.del -- Args.colon >> K (I, rule_del)];
-fun cla_meth tac prems ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
+fun cla_meth tac ctxt = METHOD (fn facts =>
+ ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
-fun cla_meth' tac prems ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
+fun cla_meth' tac ctxt = METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
-fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
-fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
+fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
+fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
--- a/src/Pure/Isar/args.ML Sat Mar 06 15:34:29 2010 +0100
+++ b/src/Pure/Isar/args.ML Sat Mar 06 15:39:16 2010 +0100
@@ -57,7 +57,6 @@
val type_name: bool -> string context_parser
val const: bool -> string context_parser
val const_proper: bool -> string context_parser
- val bang_facts: thm list context_parser
val goal_spec: ((int -> tactic) -> tactic) context_parser
val parse: token list parser
val parse1: (string -> bool) -> token list parser
@@ -224,11 +223,6 @@
(* improper method arguments *)
-val bang_facts = Scan.peek (fn context =>
- P.position ($$$ "!") >> (fn (_, pos) =>
- (legacy_feature ("use of cumulative prems (!) in proof method" ^ Position.str_of pos);
- Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
-
val from_to =
P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
--- a/src/Pure/simplifier.ML Sat Mar 06 15:34:29 2010 +0100
+++ b/src/Pure/simplifier.ML Sat Mar 06 15:39:16 2010 +0100
@@ -15,15 +15,15 @@
val simpset_of: Proof.context -> simpset
val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
val safe_asm_full_simp_tac: simpset -> int -> tactic
- val simp_tac: simpset -> int -> tactic
- val asm_simp_tac: simpset -> int -> tactic
- val full_simp_tac: simpset -> int -> tactic
- val asm_lr_simp_tac: simpset -> int -> tactic
- val asm_full_simp_tac: simpset -> int -> tactic
- val simplify: simpset -> thm -> thm
- val asm_simplify: simpset -> thm -> thm
- val full_simplify: simpset -> thm -> thm
- val asm_lr_simplify: simpset -> thm -> thm
+ val simp_tac: simpset -> int -> tactic
+ val asm_simp_tac: simpset -> int -> tactic
+ val full_simp_tac: simpset -> int -> tactic
+ val asm_lr_simp_tac: simpset -> int -> tactic
+ val asm_full_simp_tac: simpset -> int -> tactic
+ val simplify: simpset -> thm -> thm
+ val asm_simplify: simpset -> thm -> thm
+ val full_simplify: simpset -> thm -> thm
+ val asm_lr_simplify: simpset -> thm -> thm
val asm_full_simplify: simpset -> thm -> thm
end;
@@ -41,10 +41,10 @@
-> (theory -> simpset -> term -> thm option) -> simproc
val simproc: theory -> string -> string list
-> (theory -> simpset -> term -> thm option) -> simproc
- val rewrite: simpset -> conv
- val asm_rewrite: simpset -> conv
- val full_rewrite: simpset -> conv
- val asm_lr_rewrite: simpset -> conv
+ val rewrite: simpset -> conv
+ val asm_rewrite: simpset -> conv
+ val full_rewrite: simpset -> conv
+ val asm_lr_rewrite: simpset -> conv
val asm_full_rewrite: simpset -> conv
val get_ss: Context.generic -> simpset
val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
@@ -371,9 +371,9 @@
Scan.succeed asm_full_simp_tac);
fun simp_method more_mods meth =
- Args.bang_facts -- Scan.lift simp_options --|
+ Scan.lift simp_options --|
Method.sections (more_mods @ simp_modifiers') >>
- (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts)));
+ (fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts));