eliminated Args.bang_facts (legacy feature);
authorwenzelm
Sat Mar 06 15:39:16 2010 +0100 (2010-03-06)
changeset 356139d3ff36ad4e1
parent 35612 0a9fb49a086d
child 35614 d7afa8700622
eliminated Args.bang_facts (legacy feature);
NEWS
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/HOL_Specific.tex
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Pure/Isar/args.ML
src/Pure/simplifier.ML
     1.1 --- a/NEWS	Sat Mar 06 15:34:29 2010 +0100
     1.2 +++ b/NEWS	Sat Mar 06 15:39:16 2010 +0100
     1.3 @@ -58,6 +58,9 @@
     1.4  
     1.5  * Type constructors admit general mixfix syntax, not just infix.
     1.6  
     1.7 +* Use of cumulative prems via "!" in some proof methods has been
     1.8 +discontinued (legacy feature).
     1.9 +
    1.10  
    1.11  *** Pure ***
    1.12  
     2.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sat Mar 06 15:34:29 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Mar 06 15:39:16 2010 +0100
     2.3 @@ -364,7 +364,7 @@
     2.4  
     2.5    \indexouternonterm{simpmod}
     2.6    \begin{rail}
     2.7 -    ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
     2.8 +    ('simp' | 'simp\_all') opt? (simpmod *)
     2.9      ;
    2.10  
    2.11      opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
    2.12 @@ -404,9 +404,7 @@
    2.13    proofs this is usually quite well behaved in practice: just the
    2.14    local premises of the actual goal are involved, additional facts may
    2.15    be inserted via explicit forward-chaining (via @{command "then"},
    2.16 -  @{command "from"}, @{command "using"} etc.).  The full context of
    2.17 -  premises is only included if the ``@{text "!"}'' (bang) argument is
    2.18 -  given, which should be used with some care, though.
    2.19 +  @{command "from"}, @{command "using"} etc.).
    2.20  
    2.21    Additional Simplifier options may be specified to tune the behavior
    2.22    further (mostly for unstructured scripts with many accidental local
    2.23 @@ -603,9 +601,9 @@
    2.24  
    2.25    \indexouternonterm{clamod}
    2.26    \begin{rail}
    2.27 -    'blast' ('!' ?) nat? (clamod *)
    2.28 +    'blast' nat? (clamod *)
    2.29      ;
    2.30 -    ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
    2.31 +    ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *)
    2.32      ;
    2.33  
    2.34      clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
    2.35 @@ -629,9 +627,7 @@
    2.36    Any of the above methods support additional modifiers of the context
    2.37    of classical rules.  Their semantics is analogous to the attributes
    2.38    given before.  Facts provided by forward chaining are inserted into
    2.39 -  the goal before commencing proof search.  The ``@{text
    2.40 -  "!"}''~argument causes the full context of assumptions to be
    2.41 -  included as well.
    2.42 +  the goal before commencing proof search.
    2.43  *}
    2.44  
    2.45  
    2.46 @@ -649,9 +645,9 @@
    2.47  
    2.48    \indexouternonterm{clasimpmod}
    2.49    \begin{rail}
    2.50 -    'auto' '!'? (nat nat)? (clasimpmod *)
    2.51 +    'auto' (nat nat)? (clasimpmod *)
    2.52      ;
    2.53 -    ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
    2.54 +    ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *)
    2.55      ;
    2.56  
    2.57      clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
    2.58 @@ -674,8 +670,7 @@
    2.59    here.
    2.60  
    2.61    Facts provided by forward chaining are inserted into the goal before
    2.62 -  doing the search.  The ``@{text "!"}'' argument causes the full
    2.63 -  context of assumptions to be included as well.
    2.64 +  doing the search.
    2.65  
    2.66    \end{description}
    2.67  *}
     3.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Mar 06 15:34:29 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Mar 06 15:39:16 2010 +0100
     3.3 @@ -795,16 +795,15 @@
     3.4    \end{matharray}
     3.5  
     3.6    \begin{rail}
     3.7 -    'iprover' ('!' ?) ( rulemod * )
     3.8 +    'iprover' ( rulemod * )
     3.9      ;
    3.10    \end{rail}
    3.11  
    3.12    The @{method (HOL) iprover} method performs intuitionistic proof
    3.13    search, depending on specifically declared rules from the context,
    3.14    or given as explicit arguments.  Chained facts are inserted into the
    3.15 -  goal before commencing proof search; ``@{method (HOL) iprover}@{text
    3.16 -  "!"}''  means to include the current @{fact prems} as well.
    3.17 -  
    3.18 +  goal before commencing proof search.
    3.19 +
    3.20    Rules need to be classified as @{attribute (Pure) intro},
    3.21    @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
    3.22    ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
     4.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Mar 06 15:34:29 2010 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Mar 06 15:39:16 2010 +0100
     4.3 @@ -384,7 +384,7 @@
     4.4  
     4.5    \indexouternonterm{simpmod}
     4.6    \begin{rail}
     4.7 -    ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
     4.8 +    ('simp' | 'simp\_all') opt? (simpmod *)
     4.9      ;
    4.10  
    4.11      opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
    4.12 @@ -424,9 +424,7 @@
    4.13    proofs this is usually quite well behaved in practice: just the
    4.14    local premises of the actual goal are involved, additional facts may
    4.15    be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
    4.16 -  \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.).  The full context of
    4.17 -  premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) argument is
    4.18 -  given, which should be used with some care, though.
    4.19 +  \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.).
    4.20  
    4.21    Additional Simplifier options may be specified to tune the behavior
    4.22    further (mostly for unstructured scripts with many accidental local
    4.23 @@ -626,9 +624,9 @@
    4.24  
    4.25    \indexouternonterm{clamod}
    4.26    \begin{rail}
    4.27 -    'blast' ('!' ?) nat? (clamod *)
    4.28 +    'blast' nat? (clamod *)
    4.29      ;
    4.30 -    ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
    4.31 +    ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *)
    4.32      ;
    4.33  
    4.34      clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
    4.35 @@ -650,8 +648,7 @@
    4.36    Any of the above methods support additional modifiers of the context
    4.37    of classical rules.  Their semantics is analogous to the attributes
    4.38    given before.  Facts provided by forward chaining are inserted into
    4.39 -  the goal before commencing proof search.  The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''~argument causes the full context of assumptions to be
    4.40 -  included as well.%
    4.41 +  the goal before commencing proof search.%
    4.42  \end{isamarkuptext}%
    4.43  \isamarkuptrue%
    4.44  %
    4.45 @@ -671,9 +668,9 @@
    4.46  
    4.47    \indexouternonterm{clasimpmod}
    4.48    \begin{rail}
    4.49 -    'auto' '!'? (nat nat)? (clasimpmod *)
    4.50 +    'auto' (nat nat)? (clasimpmod *)
    4.51      ;
    4.52 -    ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
    4.53 +    ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *)
    4.54      ;
    4.55  
    4.56      clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
    4.57 @@ -694,8 +691,7 @@
    4.58    here.
    4.59  
    4.60    Facts provided by forward chaining are inserted into the goal before
    4.61 -  doing the search.  The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' argument causes the full
    4.62 -  context of assumptions to be included as well.
    4.63 +  doing the search.
    4.64  
    4.65    \end{description}%
    4.66  \end{isamarkuptext}%
     5.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Mar 06 15:34:29 2010 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Mar 06 15:39:16 2010 +0100
     5.3 @@ -805,15 +805,15 @@
     5.4    \end{matharray}
     5.5  
     5.6    \begin{rail}
     5.7 -    'iprover' ('!' ?) ( rulemod * )
     5.8 +    'iprover' ( rulemod * )
     5.9      ;
    5.10    \end{rail}
    5.11  
    5.12    The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
    5.13    search, depending on specifically declared rules from the context,
    5.14    or given as explicit arguments.  Chained facts are inserted into the
    5.15 -  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.
    5.16 -  
    5.17 +  goal before commencing proof search.
    5.18 +
    5.19    Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
    5.20    \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
    5.21    ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
     6.1 --- a/src/Provers/blast.ML	Sat Mar 06 15:34:29 2010 +0100
     6.2 +++ b/src/Provers/blast.ML	Sat Mar 06 15:39:16 2010 +0100
     6.3 @@ -57,7 +57,7 @@
     6.4                   safe0_netpair: netpair, safep_netpair: netpair,
     6.5                   haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
     6.6    val cla_modifiers: Method.modifier parser list
     6.7 -  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
     6.8 +  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
     6.9  end;
    6.10  
    6.11  signature BLAST =
    6.12 @@ -1309,10 +1309,9 @@
    6.13  val setup =
    6.14    setup_depth_limit #>
    6.15    Method.setup @{binding blast}
    6.16 -    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
    6.17 -      Method.sections Data.cla_modifiers >>
    6.18 -      (fn (prems, NONE) => Data.cla_meth' blast_tac prems
    6.19 -        | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
    6.20 +    (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >>
    6.21 +      (fn NONE => Data.cla_meth' blast_tac
    6.22 +        | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
    6.23      "classical tableau prover";
    6.24  
    6.25  end;
     7.1 --- a/src/Provers/clasimp.ML	Sat Mar 06 15:34:29 2010 +0100
     7.2 +++ b/src/Provers/clasimp.ML	Sat Mar 06 15:39:16 2010 +0100
     7.3 @@ -258,21 +258,21 @@
     7.4  
     7.5  (* methods *)
     7.6  
     7.7 -fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
     7.8 -  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (clasimpset_of ctxt));
     7.9 +fun clasimp_meth tac ctxt = METHOD (fn facts =>
    7.10 +  ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt));
    7.11  
    7.12 -fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
    7.13 -  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
    7.14 +fun clasimp_meth' tac ctxt = METHOD (fn facts =>
    7.15 +  HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt)));
    7.16  
    7.17  
    7.18  fun clasimp_method' tac =
    7.19 -  Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
    7.20 +  Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
    7.21  
    7.22  val auto_method =
    7.23 -  Args.bang_facts -- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
    7.24 -  Method.sections clasimp_modifiers >>
    7.25 -  (fn (prems, NONE) => clasimp_meth (CHANGED_PROP o auto_tac) prems
    7.26 -    | (prems, SOME (m, n)) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)) prems);
    7.27 +  Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
    7.28 +    Method.sections clasimp_modifiers >>
    7.29 +  (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
    7.30 +    | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
    7.31  
    7.32  
    7.33  (* theory setup *)
     8.1 --- a/src/Provers/classical.ML	Sat Mar 06 15:34:29 2010 +0100
     8.2 +++ b/src/Provers/classical.ML	Sat Mar 06 15:39:16 2010 +0100
     8.3 @@ -125,8 +125,8 @@
     8.4    val haz_intro: int option -> attribute
     8.5    val rule_del: attribute
     8.6    val cla_modifiers: Method.modifier parser list
     8.7 -  val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
     8.8 -  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
     8.9 +  val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
    8.10 +  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
    8.11    val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
    8.12    val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    8.13    val setup: theory -> theory
    8.14 @@ -969,14 +969,14 @@
    8.15    Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
    8.16    Args.del -- Args.colon >> K (I, rule_del)];
    8.17  
    8.18 -fun cla_meth tac prems ctxt = METHOD (fn facts =>
    8.19 -  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
    8.20 +fun cla_meth tac ctxt = METHOD (fn facts =>
    8.21 +  ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
    8.22  
    8.23 -fun cla_meth' tac prems ctxt = METHOD (fn facts =>
    8.24 -  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
    8.25 +fun cla_meth' tac ctxt = METHOD (fn facts =>
    8.26 +  HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
    8.27  
    8.28 -fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
    8.29 -fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
    8.30 +fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
    8.31 +fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
    8.32  
    8.33  
    8.34  
     9.1 --- a/src/Pure/Isar/args.ML	Sat Mar 06 15:34:29 2010 +0100
     9.2 +++ b/src/Pure/Isar/args.ML	Sat Mar 06 15:39:16 2010 +0100
     9.3 @@ -57,7 +57,6 @@
     9.4    val type_name: bool -> string context_parser
     9.5    val const: bool -> string context_parser
     9.6    val const_proper: bool -> string context_parser
     9.7 -  val bang_facts: thm list context_parser
     9.8    val goal_spec: ((int -> tactic) -> tactic) context_parser
     9.9    val parse: token list parser
    9.10    val parse1: (string -> bool) -> token list parser
    9.11 @@ -224,11 +223,6 @@
    9.12  
    9.13  (* improper method arguments *)
    9.14  
    9.15 -val bang_facts = Scan.peek (fn context =>
    9.16 -  P.position ($$$ "!") >> (fn (_, pos) =>
    9.17 -    (legacy_feature ("use of cumulative prems (!) in proof method" ^ Position.str_of pos);
    9.18 -      Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
    9.19 -
    9.20  val from_to =
    9.21    P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
    9.22    P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
    10.1 --- a/src/Pure/simplifier.ML	Sat Mar 06 15:34:29 2010 +0100
    10.2 +++ b/src/Pure/simplifier.ML	Sat Mar 06 15:39:16 2010 +0100
    10.3 @@ -15,15 +15,15 @@
    10.4    val simpset_of: Proof.context -> simpset
    10.5    val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
    10.6    val safe_asm_full_simp_tac: simpset -> int -> tactic
    10.7 -  val               simp_tac: simpset -> int -> tactic
    10.8 -  val           asm_simp_tac: simpset -> int -> tactic
    10.9 -  val          full_simp_tac: simpset -> int -> tactic
   10.10 -  val        asm_lr_simp_tac: simpset -> int -> tactic
   10.11 -  val      asm_full_simp_tac: simpset -> int -> tactic
   10.12 -  val          simplify: simpset -> thm -> thm
   10.13 -  val      asm_simplify: simpset -> thm -> thm
   10.14 -  val     full_simplify: simpset -> thm -> thm
   10.15 -  val   asm_lr_simplify: simpset -> thm -> thm
   10.16 +  val simp_tac: simpset -> int -> tactic
   10.17 +  val asm_simp_tac: simpset -> int -> tactic
   10.18 +  val full_simp_tac: simpset -> int -> tactic
   10.19 +  val asm_lr_simp_tac: simpset -> int -> tactic
   10.20 +  val asm_full_simp_tac: simpset -> int -> tactic
   10.21 +  val simplify: simpset -> thm -> thm
   10.22 +  val asm_simplify: simpset -> thm -> thm
   10.23 +  val full_simplify: simpset -> thm -> thm
   10.24 +  val asm_lr_simplify: simpset -> thm -> thm
   10.25    val asm_full_simplify: simpset -> thm -> thm
   10.26  end;
   10.27  
   10.28 @@ -41,10 +41,10 @@
   10.29      -> (theory -> simpset -> term -> thm option) -> simproc
   10.30    val simproc: theory -> string -> string list
   10.31      -> (theory -> simpset -> term -> thm option) -> simproc
   10.32 -  val          rewrite: simpset -> conv
   10.33 -  val      asm_rewrite: simpset -> conv
   10.34 -  val     full_rewrite: simpset -> conv
   10.35 -  val   asm_lr_rewrite: simpset -> conv
   10.36 +  val rewrite: simpset -> conv
   10.37 +  val asm_rewrite: simpset -> conv
   10.38 +  val full_rewrite: simpset -> conv
   10.39 +  val asm_lr_rewrite: simpset -> conv
   10.40    val asm_full_rewrite: simpset -> conv
   10.41    val get_ss: Context.generic -> simpset
   10.42    val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
   10.43 @@ -371,9 +371,9 @@
   10.44    Scan.succeed asm_full_simp_tac);
   10.45  
   10.46  fun simp_method more_mods meth =
   10.47 -  Args.bang_facts -- Scan.lift simp_options --|
   10.48 +  Scan.lift simp_options --|
   10.49      Method.sections (more_mods @ simp_modifiers') >>
   10.50 -    (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts)));
   10.51 +    (fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts));
   10.52  
   10.53  
   10.54