src/Provers/classical.ML
changeset 30541 9f168bdc468a
parent 30528 7173bf123335
child 30558 2ef9892114fd
     1.1 --- a/src/Provers/classical.ML	Sun Mar 15 20:19:14 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Mar 15 20:25:58 2009 +0100
     1.3 @@ -149,8 +149,8 @@
     1.4    val cla_modifiers: Method.modifier parser list
     1.5    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
     1.6    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
     1.7 -  val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
     1.8 -  val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
     1.9 +  val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
    1.10 +  val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    1.11    val setup: theory -> theory
    1.12  end;
    1.13  
    1.14 @@ -1025,23 +1025,29 @@
    1.15  fun cla_meth' tac prems ctxt = METHOD (fn facts =>
    1.16    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
    1.17  
    1.18 -val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
    1.19 -val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
    1.20 +fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
    1.21 +fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
    1.22  
    1.23  
    1.24  
    1.25  (** setup_methods **)
    1.26  
    1.27 -val setup_methods = Method.add_methods
    1.28 - [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
    1.29 -  ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
    1.30 -  ("contradiction", Method.no_args contradiction, "proof by contradiction"),
    1.31 -  ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
    1.32 -  ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
    1.33 -  ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
    1.34 -  ("best", cla_method' best_tac, "classical prover (best-first)"),
    1.35 -  ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
    1.36 -  ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
    1.37 +val setup_methods =
    1.38 +  Method.setup @{binding default} (Attrib.thms >> default)
    1.39 +    "apply some intro/elim rule (potentially classical)" #>
    1.40 +  Method.setup @{binding rule} (Attrib.thms >> rule)
    1.41 +    "apply some intro/elim rule (potentially classical)" #>
    1.42 +  Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
    1.43 +    "proof by contradiction" #>
    1.44 +  Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
    1.45 +    "repeatedly apply safe steps" #>
    1.46 +  Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
    1.47 +  Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
    1.48 +  Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
    1.49 +  Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
    1.50 +    "classical prover (iterative deepening)" #>
    1.51 +  Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
    1.52 +    "classical prover (apply safe rules)";
    1.53  
    1.54  
    1.55