simplified method setup;
authorwenzelm
Sun Mar 15 20:25:58 2009 +0100 (2009-03-15)
changeset 305419f168bdc468a
parent 30540 5e2d9604a3d3
child 30542 eb720644facd
child 30543 2ca69af4422a
simplified method setup;
src/HOL/Tools/function_package/lexicographic_order.ML
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Tools/induct_tacs.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Sun Mar 15 20:19:14 2009 +0100
     1.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Sun Mar 15 20:25:58 2009 +0100
     1.3 @@ -220,9 +220,11 @@
     1.4  
     1.5  val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
     1.6  
     1.7 -val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order,
     1.8 -                                 "termination prover for lexicographic orderings")]
     1.9 -     #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
    1.10 +val setup =
    1.11 +  Method.setup @{binding lexicographic_order}
    1.12 +    (Method.sections clasimp_modifiers >> (K lexicographic_order))
    1.13 +    "termination prover for lexicographic orderings"
    1.14 +  #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
    1.15  
    1.16  end;
    1.17  
     2.1 --- a/src/Provers/blast.ML	Sun Mar 15 20:19:14 2009 +0100
     2.2 +++ b/src/Provers/blast.ML	Sun Mar 15 20:25:58 2009 +0100
     2.3 @@ -1306,12 +1306,13 @@
     2.4  (** method setup **)
     2.5  
     2.6  val blast_method =
     2.7 -  Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
     2.8 -    (fn NONE => Data.cla_meth' blast_tac
     2.9 -      | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
    2.10 +  Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
    2.11 +  Method.sections Data.cla_modifiers >>
    2.12 +  (fn (prems, NONE) => Data.cla_meth' blast_tac prems
    2.13 +    | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems);
    2.14  
    2.15  val setup =
    2.16    setup_depth_limit #>
    2.17 -  Method.add_methods [("blast", blast_method, "tableau prover")];
    2.18 +  Method.setup @{binding blast} blast_method "tableau prover";
    2.19  
    2.20  end;
     3.1 --- a/src/Provers/clasimp.ML	Sun Mar 15 20:19:14 2009 +0100
     3.2 +++ b/src/Provers/clasimp.ML	Sun Mar 15 20:25:58 2009 +0100
     3.3 @@ -296,28 +296,30 @@
     3.4  fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
     3.5    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
     3.6  
     3.7 -val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
     3.8 -val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
     3.9  
    3.10 +fun clasimp_method tac =
    3.11 +  Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth tac);
    3.12  
    3.13 -fun auto_args m =
    3.14 -  Method.bang_sectioned_args' clasimp_modifiers
    3.15 -    (Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat))) m;
    3.16 +fun clasimp_method' tac =
    3.17 +  Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
    3.18  
    3.19 -fun auto_meth NONE = clasimp_meth (CHANGED_PROP o auto_tac)
    3.20 -  | auto_meth (SOME (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
    3.21 +val auto_method =
    3.22 +  Args.bang_facts -- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
    3.23 +  Method.sections clasimp_modifiers >>
    3.24 +  (fn (prems, NONE) => clasimp_meth (CHANGED_PROP o auto_tac) prems
    3.25 +    | (prems, SOME (m, n)) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)) prems);
    3.26  
    3.27  
    3.28  (* theory setup *)
    3.29  
    3.30  val clasimp_setup =
    3.31 - (Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
    3.32 -  Method.add_methods
    3.33 -   [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
    3.34 -    ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
    3.35 -    ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
    3.36 -    ("force", clasimp_method' force_tac, "force"),
    3.37 -    ("auto", auto_args auto_meth, "auto"),
    3.38 -    ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]);
    3.39 +  Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
    3.40 +  Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp" #>
    3.41 +  Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
    3.42 +  Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
    3.43 +  Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
    3.44 +  Method.setup @{binding auto} auto_method "auto" #>
    3.45 +  Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
    3.46 +    "clarify simplified goal";
    3.47  
    3.48  end;
     4.1 --- a/src/Provers/classical.ML	Sun Mar 15 20:19:14 2009 +0100
     4.2 +++ b/src/Provers/classical.ML	Sun Mar 15 20:25:58 2009 +0100
     4.3 @@ -149,8 +149,8 @@
     4.4    val cla_modifiers: Method.modifier parser list
     4.5    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
     4.6    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
     4.7 -  val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
     4.8 -  val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
     4.9 +  val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
    4.10 +  val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    4.11    val setup: theory -> theory
    4.12  end;
    4.13  
    4.14 @@ -1025,23 +1025,29 @@
    4.15  fun cla_meth' tac prems ctxt = METHOD (fn facts =>
    4.16    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
    4.17  
    4.18 -val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
    4.19 -val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
    4.20 +fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
    4.21 +fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
    4.22  
    4.23  
    4.24  
    4.25  (** setup_methods **)
    4.26  
    4.27 -val setup_methods = Method.add_methods
    4.28 - [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
    4.29 -  ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
    4.30 -  ("contradiction", Method.no_args contradiction, "proof by contradiction"),
    4.31 -  ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
    4.32 -  ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
    4.33 -  ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
    4.34 -  ("best", cla_method' best_tac, "classical prover (best-first)"),
    4.35 -  ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
    4.36 -  ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
    4.37 +val setup_methods =
    4.38 +  Method.setup @{binding default} (Attrib.thms >> default)
    4.39 +    "apply some intro/elim rule (potentially classical)" #>
    4.40 +  Method.setup @{binding rule} (Attrib.thms >> rule)
    4.41 +    "apply some intro/elim rule (potentially classical)" #>
    4.42 +  Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
    4.43 +    "proof by contradiction" #>
    4.44 +  Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
    4.45 +    "repeatedly apply safe steps" #>
    4.46 +  Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
    4.47 +  Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
    4.48 +  Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
    4.49 +  Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
    4.50 +    "classical prover (iterative deepening)" #>
    4.51 +  Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
    4.52 +    "classical prover (apply safe rules)";
    4.53  
    4.54  
    4.55  
     5.1 --- a/src/Tools/induct_tacs.ML	Sun Mar 15 20:19:14 2009 +0100
     5.2 +++ b/src/Tools/induct_tacs.ML	Sun Mar 15 20:25:58 2009 +0100
     5.3 @@ -26,7 +26,7 @@
     5.4        error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
     5.5    in (u, U) end;
     5.6  
     5.7 -fun gen_case_tac ctxt0 (s, opt_rule) i st =
     5.8 +fun gen_case_tac ctxt0 s opt_rule i st =
     5.9    let
    5.10      val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    5.11      val rule =
    5.12 @@ -46,8 +46,8 @@
    5.13    in res_inst_tac ctxt [(xi, s)] rule i st end
    5.14    handle THM _ => Seq.empty;
    5.15  
    5.16 -fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
    5.17 -fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
    5.18 +fun case_tac ctxt s = gen_case_tac ctxt s NONE;
    5.19 +fun case_rule_tac ctxt s rule = gen_case_tac ctxt s (SOME rule);
    5.20  
    5.21  
    5.22  (* induction *)
    5.23 @@ -63,7 +63,7 @@
    5.24  
    5.25  in
    5.26  
    5.27 -fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
    5.28 +fun gen_induct_tac ctxt0 varss opt_rules i st =
    5.29    let
    5.30      val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    5.31      val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
    5.32 @@ -103,8 +103,8 @@
    5.33  
    5.34  end;
    5.35  
    5.36 -fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);
    5.37 -fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules);
    5.38 +fun induct_tac ctxt args = gen_induct_tac ctxt args NONE;
    5.39 +fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt args (SOME rules);
    5.40  
    5.41  
    5.42  (* method syntax *)
    5.43 @@ -122,11 +122,14 @@
    5.44  in
    5.45  
    5.46  val setup =
    5.47 -  Method.add_methods
    5.48 -   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name_source -- opt_rule) gen_case_tac,
    5.49 -      "unstructured case analysis on types"),
    5.50 -    ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
    5.51 -      "unstructured induction on types")];
    5.52 +  Method.setup @{binding case_tac}
    5.53 +    (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
    5.54 +      (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
    5.55 +    "unstructured case analysis on types" #>
    5.56 +  Method.setup @{binding induct_tac}
    5.57 +    (Args.goal_spec -- varss -- opt_rules >>
    5.58 +      (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
    5.59 +    "unstructured induction on types";
    5.60  
    5.61  end;
    5.62  
     6.1 --- a/src/ZF/Tools/induct_tacs.ML	Sun Mar 15 20:19:14 2009 +0100
     6.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sun Mar 15 20:25:58 2009 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      ZF/Tools/induct_tacs.ML
     6.5 -    ID:         $Id$
     6.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7      Copyright   1994  University of Cambridge
     6.8  
     6.9 @@ -177,11 +176,14 @@
    6.10  (* theory setup *)
    6.11  
    6.12  val setup =
    6.13 -  Method.add_methods
    6.14 -    [("induct_tac", Method.goal_args_ctxt Args.name induct_tac,
    6.15 -      "induct_tac emulation (dynamic instantiation!)"),
    6.16 -     ("case_tac", Method.goal_args_ctxt Args.name exhaust_tac,
    6.17 -      "datatype case_tac emulation (dynamic instantiation!)")];
    6.18 +  Method.setup @{binding induct_tac}
    6.19 +    (Args.goal_spec -- Scan.lift Args.name >>
    6.20 +      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
    6.21 +    "induct_tac emulation (dynamic instantiation!)" #>
    6.22 +  Method.setup @{binding case_tac}
    6.23 +   (Args.goal_spec -- Scan.lift Args.name >>
    6.24 +      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
    6.25 +    "datatype case_tac emulation (dynamic instantiation!)";
    6.26  
    6.27  
    6.28  (* outer syntax *)
     7.1 --- a/src/ZF/Tools/typechk.ML	Sun Mar 15 20:19:14 2009 +0100
     7.2 +++ b/src/ZF/Tools/typechk.ML	Sun Mar 15 20:25:58 2009 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      ZF/Tools/typechk.ML
     7.5 -    ID:         $Id$
     7.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7      Copyright   1999  University of Cambridge
     7.8  
     7.9 @@ -111,10 +110,10 @@
    7.10  (* concrete syntax *)
    7.11  
    7.12  val typecheck_meth =
    7.13 -  Method.only_sectioned_args
    7.14 +  Method.sections
    7.15      [Args.add -- Args.colon >> K (I, TC_add),
    7.16       Args.del -- Args.colon >> K (I, TC_del)]
    7.17 -  (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
    7.18 +  >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))));
    7.19  
    7.20  val _ =
    7.21    OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
    7.22 @@ -126,7 +125,7 @@
    7.23  
    7.24  val setup =
    7.25    Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
    7.26 -  Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
    7.27 +  Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #>
    7.28    Simplifier.map_simpset (fn ss => ss setSolver type_solver);
    7.29  
    7.30  end;