src/Provers/classical.ML
changeset 30609 983e8b6e4e69
parent 30558 2ef9892114fd
child 31945 d5f186aa0bed
     1.1 --- a/src/Provers/classical.ML	Fri Mar 20 17:04:44 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Mar 20 17:12:37 2009 +0100
     1.3 @@ -69,11 +69,7 @@
     1.4    val appSWrappers      : claset -> wrapper
     1.5    val appWrappers       : claset -> wrapper
     1.6  
     1.7 -  val change_claset: (claset -> claset) -> unit
     1.8    val claset_of: theory -> claset
     1.9 -  val claset: unit -> claset
    1.10 -  val CLASET: (claset -> tactic) -> tactic
    1.11 -  val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
    1.12    val local_claset_of   : Proof.context -> claset
    1.13  
    1.14    val fast_tac          : claset -> int -> tactic
    1.15 @@ -107,24 +103,6 @@
    1.16    val inst_step_tac     : claset -> int -> tactic
    1.17    val inst0_step_tac    : claset -> int -> tactic
    1.18    val instp_step_tac    : claset -> int -> tactic
    1.19 -
    1.20 -  val AddDs             : thm list -> unit
    1.21 -  val AddEs             : thm list -> unit
    1.22 -  val AddIs             : thm list -> unit
    1.23 -  val AddSDs            : thm list -> unit
    1.24 -  val AddSEs            : thm list -> unit
    1.25 -  val AddSIs            : thm list -> unit
    1.26 -  val Delrules          : thm list -> unit
    1.27 -  val Safe_tac          : tactic
    1.28 -  val Safe_step_tac     : int -> tactic
    1.29 -  val Clarify_tac       : int -> tactic
    1.30 -  val Clarify_step_tac  : int -> tactic
    1.31 -  val Step_tac          : int -> tactic
    1.32 -  val Fast_tac          : int -> tactic
    1.33 -  val Best_tac          : int -> tactic
    1.34 -  val Slow_tac          : int -> tactic
    1.35 -  val Slow_best_tac     : int -> tactic
    1.36 -  val Deepen_tac        : int -> int -> tactic
    1.37  end;
    1.38  
    1.39  signature CLASSICAL =
    1.40 @@ -870,23 +848,9 @@
    1.41  fun map_context_cs f = GlobalClaset.map (apsnd
    1.42    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
    1.43  
    1.44 -fun change_claset f = Context.>> (Context.map_theory (map_claset f));
    1.45 -
    1.46  fun claset_of thy =
    1.47    let val (cs, ctxt_cs) = GlobalClaset.get thy
    1.48    in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
    1.49 -val claset = claset_of o ML_Context.the_global_context;
    1.50 -
    1.51 -fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
    1.52 -fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
    1.53 -
    1.54 -fun AddDs args = change_claset (fn cs => cs addDs args);
    1.55 -fun AddEs args = change_claset (fn cs => cs addEs args);
    1.56 -fun AddIs args = change_claset (fn cs => cs addIs args);
    1.57 -fun AddSDs args = change_claset (fn cs => cs addSDs args);
    1.58 -fun AddSEs args = change_claset (fn cs => cs addSEs args);
    1.59 -fun AddSIs args = change_claset (fn cs => cs addSIs args);
    1.60 -fun Delrules args = change_claset (fn cs => cs delrules args);
    1.61  
    1.62  
    1.63  (* context dependent components *)
    1.64 @@ -930,21 +894,6 @@
    1.65  val rule_del = attrib delrule o ContextRules.rule_del;
    1.66  
    1.67  
    1.68 -(* tactics referring to the implicit claset *)
    1.69 -
    1.70 -(*the abstraction over the proof state delays the dereferencing*)
    1.71 -fun Safe_tac st           = safe_tac (claset()) st;
    1.72 -fun Safe_step_tac i st    = safe_step_tac (claset()) i st;
    1.73 -fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
    1.74 -fun Clarify_tac i st      = clarify_tac (claset()) i st;
    1.75 -fun Step_tac i st         = step_tac (claset()) i st;
    1.76 -fun Fast_tac i st         = fast_tac (claset()) i st;
    1.77 -fun Best_tac i st         = best_tac (claset()) i st;
    1.78 -fun Slow_tac i st         = slow_tac (claset()) i st;
    1.79 -fun Slow_best_tac i st    = slow_best_tac (claset()) i st;
    1.80 -fun Deepen_tac m          = deepen_tac (claset()) m;
    1.81 -
    1.82 -
    1.83  end;
    1.84  
    1.85  
    1.86 @@ -972,15 +921,12 @@
    1.87  
    1.88  (** proof methods **)
    1.89  
    1.90 -fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt));
    1.91 -fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
    1.92 -
    1.93 -
    1.94  local
    1.95  
    1.96 -fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
    1.97 +fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
    1.98    let
    1.99      val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
   1.100 +    val CS {xtra_netpair, ...} = local_claset_of ctxt;
   1.101      val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
   1.102      val rules = rules1 @ rules2 @ rules3 @ rules4;
   1.103      val ruleq = Drule.multi_resolves facts rules;
   1.104 @@ -990,16 +936,15 @@
   1.105    end)
   1.106    THEN_ALL_NEW Goal.norm_hhf_tac;
   1.107  
   1.108 -fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
   1.109 -  | rule_tac rules _ _ facts = Method.rule_tac rules facts;
   1.110 +in
   1.111  
   1.112 -fun default_tac rules ctxt cs facts =
   1.113 -  HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
   1.114 +fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
   1.115 +  | rule_tac _ rules facts = Method.rule_tac rules facts;
   1.116 +
   1.117 +fun default_tac ctxt rules facts =
   1.118 +  HEADGOAL (rule_tac ctxt rules facts) ORELSE
   1.119    Class.default_intro_tac ctxt facts;
   1.120  
   1.121 -in
   1.122 -  val rule = METHOD_CLASET' o rule_tac;
   1.123 -  val default = METHOD_CLASET o default_tac;
   1.124  end;
   1.125  
   1.126  
   1.127 @@ -1033,9 +978,11 @@
   1.128  (** setup_methods **)
   1.129  
   1.130  val setup_methods =
   1.131 -  Method.setup @{binding default} (Attrib.thms >> default)
   1.132 +  Method.setup @{binding default}
   1.133 +   (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
   1.134      "apply some intro/elim rule (potentially classical)" #>
   1.135 -  Method.setup @{binding rule} (Attrib.thms >> rule)
   1.136 +  Method.setup @{binding rule}
   1.137 +    (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
   1.138      "apply some intro/elim rule (potentially classical)" #>
   1.139    Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
   1.140      "proof by contradiction" #>