# HG changeset patch # User wenzelm # Date 1267886356 -3600 # Node ID 9d3ff36ad4e11a5e1cf2eb3c648cf95bc572dec7 # Parent 0a9fb49a086d8014fcf6488632b1752bc1d1b81d eliminated Args.bang_facts (legacy feature); diff -r 0a9fb49a086d -r 9d3ff36ad4e1 NEWS --- 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 *** diff -r 0a9fb49a086d -r 9d3ff36ad4e1 doc-src/IsarRef/Thy/Generic.thy --- 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} *} diff -r 0a9fb49a086d -r 9d3ff36ad4e1 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 diff -r 0a9fb49a086d -r 9d3ff36ad4e1 doc-src/IsarRef/Thy/document/Generic.tex --- 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}% diff -r 0a9fb49a086d -r 9d3ff36ad4e1 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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 diff -r 0a9fb49a086d -r 9d3ff36ad4e1 src/Provers/blast.ML --- 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; diff -r 0a9fb49a086d -r 9d3ff36ad4e1 src/Provers/clasimp.ML --- 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 *) diff -r 0a9fb49a086d -r 9d3ff36ad4e1 src/Provers/classical.ML --- 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); diff -r 0a9fb49a086d -r 9d3ff36ad4e1 src/Pure/Isar/args.ML --- 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) || diff -r 0a9fb49a086d -r 9d3ff36ad4e1 src/Pure/simplifier.ML --- 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));