src/Provers/classical.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 21646 c07b5b0e8492
child 21689 58abd6d8abd1
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     1 (*  Title:      Provers/classical.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Theorem prover for classical reasoning, including predicate calculus, set
     7 theory, etc.
     8 
     9 Rules must be classified as intro, elim, safe, hazardous (unsafe).
    10 
    11 A rule is unsafe unless it can be applied blindly without harmful results.
    12 For a rule to be safe, its premises and conclusion should be logically
    13 equivalent.  There should be no variables in the premises that are not in
    14 the conclusion.
    15 *)
    16 
    17 (*higher precedence than := facilitates use of references*)
    18 infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
    19   addSWrapper delSWrapper addWrapper delWrapper
    20   addSbefore addSafter addbefore addafter
    21   addD2 addE2 addSD2 addSE2;
    22 
    23 
    24 (*should be a type abbreviation in signature CLASSICAL*)
    25 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    26 type wrapper = (int -> tactic) -> (int -> tactic);
    27 
    28 signature CLASSICAL_DATA =
    29 sig
    30   val mp        : thm           (* [| P-->Q;  P |] ==> Q *)
    31   val not_elim  : thm           (* [| ~P;  P |] ==> R *)
    32   val classical : thm           (* (~P ==> P) ==> P *)
    33   val sizef     : thm -> int    (* size function for BEST_FIRST *)
    34   val hyp_subst_tacs: (int -> tactic) list
    35 end;
    36 
    37 signature BASIC_CLASSICAL =
    38 sig
    39   type claset
    40   val empty_cs: claset
    41   val print_cs: claset -> unit
    42   val print_claset: theory -> unit
    43   val rep_cs:
    44     claset -> {safeIs: thm list, safeEs: thm list,
    45                  hazIs: thm list, hazEs: thm list,
    46                  swrappers: (string * wrapper) list,
    47                  uwrappers: (string * wrapper) list,
    48                  safe0_netpair: netpair, safep_netpair: netpair,
    49                  haz_netpair: netpair, dup_netpair: netpair,
    50                  xtra_netpair: ContextRules.netpair}
    51   val merge_cs          : claset * claset -> claset
    52   val addDs             : claset * thm list -> claset
    53   val addEs             : claset * thm list -> claset
    54   val addIs             : claset * thm list -> claset
    55   val addSDs            : claset * thm list -> claset
    56   val addSEs            : claset * thm list -> claset
    57   val addSIs            : claset * thm list -> claset
    58   val delrules          : claset * thm list -> claset
    59   val addSWrapper       : claset * (string * wrapper) -> claset
    60   val delSWrapper       : claset *  string            -> claset
    61   val addWrapper        : claset * (string * wrapper) -> claset
    62   val delWrapper        : claset *  string            -> claset
    63   val addSbefore        : claset * (string * (int -> tactic)) -> claset
    64   val addSafter         : claset * (string * (int -> tactic)) -> claset
    65   val addbefore         : claset * (string * (int -> tactic)) -> claset
    66   val addafter          : claset * (string * (int -> tactic)) -> claset
    67   val addD2             : claset * (string * thm) -> claset
    68   val addE2             : claset * (string * thm) -> claset
    69   val addSD2            : claset * (string * thm) -> claset
    70   val addSE2            : claset * (string * thm) -> claset
    71   val appSWrappers      : claset -> wrapper
    72   val appWrappers       : claset -> wrapper
    73 
    74   val change_claset_of: theory -> (claset -> claset) -> unit
    75   val change_claset: (claset -> claset) -> unit
    76   val claset_of: theory -> claset
    77   val claset: unit -> claset
    78   val CLASET: (claset -> tactic) -> tactic
    79   val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
    80   val local_claset_of   : Proof.context -> claset
    81 
    82   val fast_tac          : claset -> int -> tactic
    83   val slow_tac          : claset -> int -> tactic
    84   val weight_ASTAR      : int ref
    85   val astar_tac         : claset -> int -> tactic
    86   val slow_astar_tac    : claset -> int -> tactic
    87   val best_tac          : claset -> int -> tactic
    88   val first_best_tac    : claset -> int -> tactic
    89   val slow_best_tac     : claset -> int -> tactic
    90   val depth_tac         : claset -> int -> int -> tactic
    91   val deepen_tac        : claset -> int -> int -> tactic
    92 
    93   val contr_tac         : int -> tactic
    94   val dup_elim          : thm -> thm
    95   val dup_intr          : thm -> thm
    96   val dup_step_tac      : claset -> int -> tactic
    97   val eq_mp_tac         : int -> tactic
    98   val haz_step_tac      : claset -> int -> tactic
    99   val joinrules         : thm list * thm list -> (bool * thm) list
   100   val mp_tac            : int -> tactic
   101   val safe_tac          : claset -> tactic
   102   val safe_steps_tac    : claset -> int -> tactic
   103   val safe_step_tac     : claset -> int -> tactic
   104   val clarify_tac       : claset -> int -> tactic
   105   val clarify_step_tac  : claset -> int -> tactic
   106   val step_tac          : claset -> int -> tactic
   107   val slow_step_tac     : claset -> int -> tactic
   108   val swapify           : thm list -> thm list
   109   val swap_res_tac      : thm list -> int -> tactic
   110   val inst_step_tac     : claset -> int -> tactic
   111   val inst0_step_tac    : claset -> int -> tactic
   112   val instp_step_tac    : claset -> int -> tactic
   113 
   114   val AddDs             : thm list -> unit
   115   val AddEs             : thm list -> unit
   116   val AddIs             : thm list -> unit
   117   val AddSDs            : thm list -> unit
   118   val AddSEs            : thm list -> unit
   119   val AddSIs            : thm list -> unit
   120   val Delrules          : thm list -> unit
   121   val Safe_tac          : tactic
   122   val Safe_step_tac     : int -> tactic
   123   val Clarify_tac       : int -> tactic
   124   val Clarify_step_tac  : int -> tactic
   125   val Step_tac          : int -> tactic
   126   val Fast_tac          : int -> tactic
   127   val Best_tac          : int -> tactic
   128   val Slow_tac          : int -> tactic
   129   val Slow_best_tac     : int -> tactic
   130   val Deepen_tac        : int -> int -> tactic
   131 end;
   132 
   133 signature CLASSICAL =
   134 sig
   135   include BASIC_CLASSICAL
   136   val swap: thm  (* ~P ==> (~Q ==> P) ==> Q *)
   137   val classical_rule: thm -> thm
   138   val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   139   val del_context_safe_wrapper: string -> theory -> theory
   140   val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   141   val del_context_unsafe_wrapper: string -> theory -> theory
   142   val get_claset: theory -> claset
   143   val print_local_claset: Proof.context -> unit
   144   val get_local_claset: Proof.context -> claset
   145   val put_local_claset: claset -> Proof.context -> Proof.context
   146   val safe_dest: int option -> attribute
   147   val safe_elim: int option -> attribute
   148   val safe_intro: int option -> attribute
   149   val haz_dest: int option -> attribute
   150   val haz_elim: int option -> attribute
   151   val haz_intro: int option -> attribute
   152   val rule_del: attribute
   153   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   154   val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   155   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   156   val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
   157   val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
   158   val setup: theory -> theory
   159 end;
   160 
   161 
   162 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
   163 struct
   164 
   165 local open Data in
   166 
   167 (** classical elimination rules **)
   168 
   169 (*
   170 Classical reasoning requires stronger elimination rules.  For
   171 instance, make_elim of Pure transforms the HOL rule injD into
   172 
   173     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
   174 
   175 Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF
   176 FAILED"; classical_rule will strenthen this to
   177 
   178     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
   179 *)
   180 
   181 fun classical_rule rule =
   182   if ObjectLogic.is_elim rule then
   183     let
   184       val rule' = rule RS classical;
   185       val concl' = Thm.concl_of rule';
   186       fun redundant_hyp goal =
   187         concl' aconv Logic.strip_assums_concl goal orelse
   188           (case Logic.strip_assums_hyp goal of
   189             hyp :: hyps => exists (fn t => t aconv hyp) hyps
   190           | _ => false);
   191       val rule'' =
   192         rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
   193           if i = 1 orelse redundant_hyp goal
   194           then Tactic.etac thin_rl i
   195           else all_tac))
   196         |> Seq.hd
   197         |> Drule.zero_var_indexes
   198         |> PureThy.put_name_hint (PureThy.get_name_hint rule);
   199     in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
   200   else rule;
   201 
   202 
   203 
   204 (*** Useful tactics for classical reasoning ***)
   205 
   206 val imp_elim = (*cannot use bind_thm within a structure!*)
   207   store_thm ("imp_elim", Thm.transfer (the_context ()) (classical_rule (Tactic.make_elim mp)));
   208 
   209 (*Prove goal that assumes both P and ~P.
   210   No backtracking if it finds an equal assumption.  Perhaps should call
   211   ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
   212 val contr_tac = eresolve_tac [not_elim]  THEN'
   213                 (eq_assume_tac ORELSE' assume_tac);
   214 
   215 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   216   Could do the same thing for P<->Q and P... *)
   217 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
   218 
   219 (*Like mp_tac but instantiates no variables*)
   220 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
   221 
   222 val swap =
   223   store_thm ("swap", Thm.transfer (the_context ())
   224     (rule_by_tactic (etac thin_rl 1) (not_elim RS classical)));
   225 
   226 (*Creates rules to eliminate ~A, from rules to introduce A*)
   227 fun swapify intrs = intrs RLN (2, [swap]);
   228 fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, swap))) x;
   229 
   230 (*Uses introduction rules in the normal way, or on negated assumptions,
   231   trying rules in order. *)
   232 fun swap_res_tac rls =
   233     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
   234     in  assume_tac      ORELSE'
   235         contr_tac       ORELSE'
   236         biresolve_tac (foldr addrl [] rls)
   237     end;
   238 
   239 (*Duplication of hazardous rules, for complete provers*)
   240 fun dup_intr th = zero_var_indexes (th RS classical);
   241 
   242 fun dup_elim th =
   243     rule_by_tactic (TRYALL (etac revcut_rl))
   244       ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd);
   245 
   246 (**** Classical rule sets ****)
   247 
   248 datatype claset =
   249   CS of {safeIs         : thm list,                (*safe introduction rules*)
   250          safeEs         : thm list,                (*safe elimination rules*)
   251          hazIs          : thm list,                (*unsafe introduction rules*)
   252          hazEs          : thm list,                (*unsafe elimination rules*)
   253          swrappers      : (string * wrapper) list, (*for transforming safe_step_tac*)
   254          uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
   255          safe0_netpair  : netpair,                 (*nets for trivial cases*)
   256          safep_netpair  : netpair,                 (*nets for >0 subgoals*)
   257          haz_netpair    : netpair,                 (*nets for unsafe rules*)
   258          dup_netpair    : netpair,                 (*nets for duplication*)
   259          xtra_netpair   : ContextRules.netpair};   (*nets for extra rules*)
   260 
   261 (*Desired invariants are
   262         safe0_netpair = build safe0_brls,
   263         safep_netpair = build safep_brls,
   264         haz_netpair = build (joinrules(hazIs, hazEs)),
   265         dup_netpair = build (joinrules(map dup_intr hazIs,
   266                                        map dup_elim hazEs))
   267 
   268 where build = build_netpair(Net.empty,Net.empty),
   269       safe0_brls contains all brules that solve the subgoal, and
   270       safep_brls contains all brules that generate 1 or more new subgoals.
   271 The theorem lists are largely comments, though they are used in merge_cs and print_cs.
   272 Nets must be built incrementally, to save space and time.
   273 *)
   274 
   275 val empty_netpair = (Net.empty, Net.empty);
   276 
   277 val empty_cs =
   278   CS{safeIs     = [],
   279      safeEs     = [],
   280      hazIs      = [],
   281      hazEs      = [],
   282      swrappers  = [],
   283      uwrappers  = [],
   284      safe0_netpair = empty_netpair,
   285      safep_netpair = empty_netpair,
   286      haz_netpair   = empty_netpair,
   287      dup_netpair   = empty_netpair,
   288      xtra_netpair  = empty_netpair};
   289 
   290 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
   291   let val pretty_thms = map Display.pretty_thm in
   292     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   293       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   294       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   295       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
   296       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
   297       Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
   298     |> Pretty.chunks |> Pretty.writeln
   299   end;
   300 
   301 fun rep_cs (CS args) = args;
   302 
   303 local
   304   fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l;
   305 in
   306   fun appSWrappers (CS{swrappers,...}) = wrap swrappers;
   307   fun appWrappers  (CS{uwrappers,...}) = wrap uwrappers;
   308 end;
   309 
   310 
   311 (*** Adding (un)safe introduction or elimination rules.
   312 
   313     In case of overlap, new rules are tried BEFORE old ones!!
   314 ***)
   315 
   316 (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
   317   assumptions.  Pairs elim rules with true. *)
   318 fun joinrules (intrs, elims) =
   319   (map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs;
   320 
   321 fun joinrules' (intrs, elims) =
   322   map (pair true) elims @ map (pair false) intrs;
   323 
   324 (*Priority: prefer rules with fewest subgoals,
   325   then rules added most recently (preferring the head of the list).*)
   326 fun tag_brls k [] = []
   327   | tag_brls k (brl::brls) =
   328       (1000000*subgoals_of_brl brl + k, brl) ::
   329       tag_brls (k+1) brls;
   330 
   331 fun tag_brls' _ _ [] = []
   332   | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
   333 
   334 fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
   335 
   336 (*Insert into netpair that already has nI intr rules and nE elim rules.
   337   Count the intr rules double (to account for swapify).  Negate to give the
   338   new insertions the lowest priority.*)
   339 fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
   340 fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
   341 
   342 fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
   343 fun delete x = delete_tagged_list (joinrules x);
   344 fun delete' x = delete_tagged_list (joinrules' x);
   345 
   346 val mem_thm = member Drule.eq_thm_prop
   347 and rem_thm = remove Drule.eq_thm_prop;
   348 
   349 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   350   is still allowed.*)
   351 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   352        if mem_thm safeIs th then
   353          warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
   354   else if mem_thm safeEs th then
   355          warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   356   else if mem_thm hazIs th then
   357          warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
   358   else if mem_thm hazEs th then
   359          warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
   360   else ();
   361 
   362 
   363 (*** Safe rules ***)
   364 
   365 fun addSI w th
   366   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   367              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   368   if mem_thm safeIs th then
   369          (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
   370           cs)
   371   else
   372   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   373           List.partition Thm.no_prems [th]
   374       val nI = length safeIs + 1
   375       and nE = length safeEs
   376   in warn_dup th cs;
   377      CS{safeIs  = th::safeIs,
   378         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   379         safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   380         safeEs  = safeEs,
   381         hazIs   = hazIs,
   382         hazEs   = hazEs,
   383         swrappers    = swrappers,
   384         uwrappers    = uwrappers,
   385         haz_netpair  = haz_netpair,
   386         dup_netpair  = dup_netpair,
   387         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
   388   end;
   389 
   390 fun addSE w th
   391   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   392              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   393   if mem_thm safeEs th then
   394          (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
   395           cs)
   396   else if has_fewer_prems 1 th then
   397     	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   398   else
   399   let
   400       val th' = classical_rule th
   401       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   402           List.partition (fn rl => nprems_of rl=1) [th']
   403       val nI = length safeIs
   404       and nE = length safeEs + 1
   405   in warn_dup th cs;
   406      CS{safeEs  = th::safeEs,
   407         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   408         safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   409         safeIs  = safeIs,
   410         hazIs   = hazIs,
   411         hazEs   = hazEs,
   412         swrappers    = swrappers,
   413         uwrappers    = uwrappers,
   414         haz_netpair  = haz_netpair,
   415         dup_netpair  = dup_netpair,
   416         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
   417   end;
   418 
   419 fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   420 fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   421 
   422 (*Give new theorem a name, if it has one already.*)
   423 fun name_make_elim th =
   424     if has_fewer_prems 1 th then
   425     	error("Ill-formed destruction rule\n" ^ string_of_thm th)
   426     else
   427     case PureThy.get_name_hint th of
   428         "" => Tactic.make_elim th
   429       | a  => PureThy.put_name_hint (a ^ "_dest") (Tactic.make_elim th);
   430 
   431 fun cs addSDs ths = cs addSEs (map name_make_elim ths);
   432 
   433 
   434 (*** Hazardous (unsafe) rules ***)
   435 
   436 fun addI w th
   437   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   438              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   439   if mem_thm hazIs th then
   440          (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
   441           cs)
   442   else
   443   let val nI = length hazIs + 1
   444       and nE = length hazEs
   445   in warn_dup th cs;
   446      CS{hazIs   = th::hazIs,
   447         haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
   448         dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
   449         safeIs  = safeIs,
   450         safeEs  = safeEs,
   451         hazEs   = hazEs,
   452         swrappers     = swrappers,
   453         uwrappers     = uwrappers,
   454         safe0_netpair = safe0_netpair,
   455         safep_netpair = safep_netpair,
   456         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   457   end
   458   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   459          error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   460 
   461 fun addE w th
   462   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   463             safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   464   if mem_thm hazEs th then
   465          (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
   466           cs)
   467   else if has_fewer_prems 1 th then
   468     	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   469   else
   470   let
   471       val th' = classical_rule th
   472       val nI = length hazIs
   473       and nE = length hazEs + 1
   474   in warn_dup th cs;
   475      CS{hazEs   = th::hazEs,
   476         haz_netpair = insert (nI,nE) ([], [th']) haz_netpair,
   477         dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair,
   478         safeIs  = safeIs,
   479         safeEs  = safeEs,
   480         hazIs   = hazIs,
   481         swrappers     = swrappers,
   482         uwrappers     = uwrappers,
   483         safe0_netpair = safe0_netpair,
   484         safep_netpair = safep_netpair,
   485         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair}
   486   end;
   487 
   488 fun cs addIs ths = fold_rev (addI NONE) ths cs;
   489 fun cs addEs ths = fold_rev (addE NONE) ths cs;
   490 
   491 fun cs addDs ths = cs addEs (map name_make_elim ths);
   492 
   493 
   494 (*** Deletion of rules
   495      Working out what to delete, requires repeating much of the code used
   496         to insert.
   497 ***)
   498 
   499 fun delSI th
   500           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   501                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   502  if mem_thm safeIs th then
   503    let val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th]
   504    in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   505          safep_netpair = delete (safep_rls, []) safep_netpair,
   506          safeIs = rem_thm th safeIs,
   507          safeEs = safeEs,
   508          hazIs  = hazIs,
   509          hazEs  = hazEs,
   510          swrappers    = swrappers,
   511          uwrappers    = uwrappers,
   512          haz_netpair  = haz_netpair,
   513          dup_netpair  = dup_netpair,
   514          xtra_netpair = delete' ([th], []) xtra_netpair}
   515    end
   516  else cs;
   517 
   518 fun delSE th
   519           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   520                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   521   if mem_thm safeEs th then
   522     let
   523       val th' = classical_rule th
   524       val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
   525     in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   526          safep_netpair = delete ([], safep_rls) safep_netpair,
   527          safeIs = safeIs,
   528          safeEs = rem_thm th safeEs,
   529          hazIs  = hazIs,
   530          hazEs  = hazEs,
   531          swrappers    = swrappers,
   532          uwrappers    = uwrappers,
   533          haz_netpair  = haz_netpair,
   534          dup_netpair  = dup_netpair,
   535          xtra_netpair = delete' ([], [th]) xtra_netpair}
   536     end
   537   else cs;
   538 
   539 
   540 fun delI th
   541          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   542                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   543  if mem_thm hazIs th then
   544      CS{haz_netpair = delete ([th], []) haz_netpair,
   545         dup_netpair = delete ([dup_intr th], []) dup_netpair,
   546         safeIs  = safeIs,
   547         safeEs  = safeEs,
   548         hazIs   = rem_thm th hazIs,
   549         hazEs   = hazEs,
   550         swrappers     = swrappers,
   551         uwrappers     = uwrappers,
   552         safe0_netpair = safe0_netpair,
   553         safep_netpair = safep_netpair,
   554         xtra_netpair = delete' ([th], []) xtra_netpair}
   555  else cs
   556  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   557         error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   558 
   559 
   560 fun delE th
   561          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   562                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   563   let val th' = classical_rule th in
   564     if mem_thm hazEs th then
   565      CS{haz_netpair = delete ([], [th']) haz_netpair,
   566         dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   567         safeIs  = safeIs,
   568         safeEs  = safeEs,
   569         hazIs   = hazIs,
   570         hazEs   = rem_thm th hazEs,
   571         swrappers     = swrappers,
   572         uwrappers     = uwrappers,
   573         safe0_netpair = safe0_netpair,
   574         safep_netpair = safep_netpair,
   575         xtra_netpair = delete' ([], [th]) xtra_netpair}
   576      else cs
   577    end;
   578 
   579 
   580 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   581 fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   582   let val th' = Tactic.make_elim th in
   583     if mem_thm safeIs th orelse mem_thm safeEs th orelse
   584       mem_thm hazIs th orelse mem_thm hazEs th orelse
   585       mem_thm safeEs th' orelse mem_thm hazEs th'
   586     then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   587     else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs)
   588   end;
   589 
   590 fun cs delrules ths = fold delrule ths cs;
   591 
   592 
   593 (*** Modifying the wrapper tacticals ***)
   594 fun update_swrappers
   595 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   596     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
   597  CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   598     swrappers = f swrappers, uwrappers = uwrappers,
   599     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   600     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   601 
   602 fun update_uwrappers
   603 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   604     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
   605  CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   606     swrappers = swrappers, uwrappers = f uwrappers,
   607     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   608     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   609 
   610 
   611 (*Add/replace a safe wrapper*)
   612 fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers =>
   613     overwrite_warn (swrappers, new_swrapper)
   614        ("Overwriting safe wrapper " ^ fst new_swrapper));
   615 
   616 (*Add/replace an unsafe wrapper*)
   617 fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
   618     overwrite_warn (uwrappers, new_uwrapper)
   619         ("Overwriting unsafe wrapper "^fst new_uwrapper));
   620 
   621 (*Remove a safe wrapper*)
   622 fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
   623   let val swrappers' = filter_out (equal name o fst) swrappers in
   624     if length swrappers <> length swrappers' then swrappers'
   625     else (warning ("No such safe wrapper in claset: "^ name); swrappers)
   626   end);
   627 
   628 (*Remove an unsafe wrapper*)
   629 fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
   630   let val uwrappers' = filter_out (equal name o fst) uwrappers in
   631     if length uwrappers <> length uwrappers' then uwrappers'
   632     else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers)
   633   end);
   634 
   635 (* compose a safe tactic alternatively before/after safe_step_tac *)
   636 fun cs addSbefore  (name,    tac1) =
   637     cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   638 fun cs addSafter   (name,    tac2) =
   639     cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   640 
   641 (*compose a tactic alternatively before/after the step tactic *)
   642 fun cs addbefore   (name,    tac1) =
   643     cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
   644 fun cs addafter    (name,    tac2) =
   645     cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
   646 
   647 fun cs addD2     (name, thm) =
   648     cs addafter  (name, datac thm 1);
   649 fun cs addE2     (name, thm) =
   650     cs addafter  (name, eatac thm 1);
   651 fun cs addSD2    (name, thm) =
   652     cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   653 fun cs addSE2    (name, thm) =
   654     cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   655 
   656 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   657   Merging the term nets may look more efficient, but the rather delicate
   658   treatment of priority might get muddled up.*)
   659 fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
   660      CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
   661   let val safeIs' = fold rem_thm safeIs safeIs2
   662       val safeEs' = fold rem_thm safeEs safeEs2
   663       val hazIs' = fold rem_thm hazIs hazIs2
   664       val hazEs' = fold rem_thm hazEs hazEs2
   665       val cs1   = cs addSIs safeIs'
   666                      addSEs safeEs'
   667                      addIs  hazIs'
   668                      addEs  hazEs'
   669       val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers);
   670       val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers);
   671   in cs3
   672   end;
   673 
   674 
   675 (**** Simple tactics for theorem proving ****)
   676 
   677 (*Attack subgoals using safe inferences -- matching, not resolution*)
   678 fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   679   appSWrappers cs (FIRST' [
   680         eq_assume_tac,
   681         eq_mp_tac,
   682         bimatch_from_nets_tac safe0_netpair,
   683         FIRST' hyp_subst_tacs,
   684         bimatch_from_nets_tac safep_netpair]);
   685 
   686 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   687 fun safe_steps_tac cs = REPEAT_DETERM1 o
   688         (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   689 
   690 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   691 fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   692 
   693 
   694 (*** Clarify_tac: do safe steps without causing branching ***)
   695 
   696 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   697 
   698 (*version of bimatch_from_nets_tac that only applies rules that
   699   create precisely n subgoals.*)
   700 fun n_bimatch_from_nets_tac n =
   701     biresolution_from_nets_tac (Tactic.orderlist o List.filter (nsubgoalsP n)) true;
   702 
   703 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   704 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   705 
   706 (*Two-way branching is allowed only if one of the branches immediately closes*)
   707 fun bimatch2_tac netpair i =
   708     n_bimatch_from_nets_tac 2 netpair i THEN
   709     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
   710 
   711 (*Attack subgoals using safe inferences -- matching, not resolution*)
   712 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   713   appSWrappers cs (FIRST' [
   714         eq_assume_contr_tac,
   715         bimatch_from_nets_tac safe0_netpair,
   716         FIRST' hyp_subst_tacs,
   717         n_bimatch_from_nets_tac 1 safep_netpair,
   718         bimatch2_tac safep_netpair]);
   719 
   720 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   721 
   722 
   723 (*** Unsafe steps instantiate variables or lose information ***)
   724 
   725 (*Backtracking is allowed among the various these unsafe ways of
   726   proving a subgoal.  *)
   727 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   728   assume_tac                      APPEND'
   729   contr_tac                       APPEND'
   730   biresolve_from_nets_tac safe0_netpair;
   731 
   732 (*These unsafe steps could generate more subgoals.*)
   733 fun instp_step_tac (CS{safep_netpair,...}) =
   734   biresolve_from_nets_tac safep_netpair;
   735 
   736 (*These steps could instantiate variables and are therefore unsafe.*)
   737 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   738 
   739 fun haz_step_tac (CS{haz_netpair,...}) =
   740   biresolve_from_nets_tac haz_netpair;
   741 
   742 (*Single step for the prover.  FAILS unless it makes progress. *)
   743 fun step_tac cs i = safe_tac cs ORELSE appWrappers cs
   744         (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   745 
   746 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   747   allows backtracking from "safe" rules to "unsafe" rules here.*)
   748 fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs
   749         (inst_step_tac cs APPEND' haz_step_tac cs) i;
   750 
   751 (**** The following tactics all fail unless they solve one goal ****)
   752 
   753 (*Dumb but fast*)
   754 fun fast_tac cs =
   755   ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   756 
   757 (*Slower but smarter than fast_tac*)
   758 fun best_tac cs =
   759   ObjectLogic.atomize_tac THEN'
   760   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   761 
   762 (*even a bit smarter than best_tac*)
   763 fun first_best_tac cs =
   764   ObjectLogic.atomize_tac THEN'
   765   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   766 
   767 fun slow_tac cs =
   768   ObjectLogic.atomize_tac THEN'
   769   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   770 
   771 fun slow_best_tac cs =
   772   ObjectLogic.atomize_tac THEN'
   773   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   774 
   775 
   776 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   777 val weight_ASTAR = ref 5;
   778 
   779 fun astar_tac cs =
   780   ObjectLogic.atomize_tac THEN'
   781   SELECT_GOAL
   782     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   783       (step_tac cs 1));
   784 
   785 fun slow_astar_tac cs =
   786   ObjectLogic.atomize_tac THEN'
   787   SELECT_GOAL
   788     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   789       (slow_step_tac cs 1));
   790 
   791 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   792   of much experimentation!  Changing APPEND to ORELSE below would prove
   793   easy theorems faster, but loses completeness -- and many of the harder
   794   theorems such as 43. ****)
   795 
   796 (*Non-deterministic!  Could always expand the first unsafe connective.
   797   That's hard to implement and did not perform better in experiments, due to
   798   greater search depth required.*)
   799 fun dup_step_tac (cs as (CS{dup_netpair,...})) =
   800   biresolve_from_nets_tac dup_netpair;
   801 
   802 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   803 local
   804 fun slow_step_tac' cs = appWrappers cs
   805         (instp_step_tac cs APPEND' dup_step_tac cs);
   806 in fun depth_tac cs m i state = SELECT_GOAL
   807    (safe_steps_tac cs 1 THEN_ELSE
   808         (DEPTH_SOLVE (depth_tac cs m 1),
   809          inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   810                 (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   811         )) i state;
   812 end;
   813 
   814 (*Search, with depth bound m.
   815   This is the "entry point", which does safe inferences first.*)
   816 fun safe_depth_tac cs m =
   817   SUBGOAL
   818     (fn (prem,i) =>
   819       let val deti =
   820           (*No Vars in the goal?  No need to backtrack between goals.*)
   821           case term_vars prem of
   822               []        => DETERM
   823             | _::_      => I
   824       in  SELECT_GOAL (TRY (safe_tac cs) THEN
   825                        DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   826       end);
   827 
   828 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   829 
   830 
   831 
   832 (** context dependent claset components **)
   833 
   834 datatype context_cs = ContextCS of
   835  {swrappers: (string * (Proof.context -> wrapper)) list,
   836   uwrappers: (string * (Proof.context -> wrapper)) list};
   837 
   838 fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
   839   let
   840     fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
   841   in
   842     cs |> fold_rev (add_wrapper (op addSWrapper)) swrappers
   843     |> fold_rev (add_wrapper (op addWrapper)) uwrappers
   844   end;
   845 
   846 fun make_context_cs (swrappers, uwrappers) =
   847   ContextCS {swrappers = swrappers, uwrappers = uwrappers};
   848 
   849 val empty_context_cs = make_context_cs ([], []);
   850 
   851 fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
   852   let
   853     val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
   854     val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
   855 
   856     val swrappers' = merge_alists swrappers1 swrappers2;
   857     val uwrappers' = merge_alists uwrappers1 uwrappers2;
   858   in make_context_cs (swrappers', uwrappers') end;
   859 
   860 
   861 
   862 (** claset data **)
   863 
   864 (* global claset *)
   865 
   866 structure GlobalClaset = TheoryDataFun
   867 (struct
   868   val name = "Provers/claset";
   869   type T = claset ref * context_cs;
   870 
   871   val empty = (ref empty_cs, empty_context_cs);
   872   fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
   873   val extend = copy;
   874   fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
   875     (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
   876   fun print _ (ref cs, _) = print_cs cs;
   877 end);
   878 
   879 val print_claset = GlobalClaset.print;
   880 val get_claset = ! o #1 o GlobalClaset.get;
   881 
   882 val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
   883 fun map_context_cs f = GlobalClaset.map (apsnd
   884   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
   885 
   886 val change_claset_of = change o #1 o GlobalClaset.get;
   887 fun change_claset f = change_claset_of (Context.the_context ()) f;
   888 
   889 fun claset_of thy =
   890   let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
   891   in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
   892 val claset = claset_of o Context.the_context;
   893 
   894 fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
   895 fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
   896 
   897 fun AddDs args = change_claset (fn cs => cs addDs args);
   898 fun AddEs args = change_claset (fn cs => cs addEs args);
   899 fun AddIs args = change_claset (fn cs => cs addIs args);
   900 fun AddSDs args = change_claset (fn cs => cs addSDs args);
   901 fun AddSEs args = change_claset (fn cs => cs addSEs args);
   902 fun AddSIs args = change_claset (fn cs => cs addSIs args);
   903 fun Delrules args = change_claset (fn cs => cs delrules args);
   904 
   905 
   906 (* context dependent components *)
   907 
   908 fun add_context_safe_wrapper wrapper = map_context_cs (apfst (merge_alists [wrapper]));
   909 fun del_context_safe_wrapper name = map_context_cs (apfst (filter_out (equal name o #1)));
   910 
   911 fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd (merge_alists [wrapper]));
   912 fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1)));
   913 
   914 
   915 (* local claset *)
   916 
   917 structure LocalClaset = ProofDataFun
   918 (struct
   919   val name = "Provers/claset";
   920   type T = claset;
   921   val init = get_claset;
   922   fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
   923 end);
   924 
   925 val print_local_claset = LocalClaset.print;
   926 val get_local_claset = LocalClaset.get;
   927 val put_local_claset = LocalClaset.put;
   928 
   929 fun local_claset_of ctxt =
   930   context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
   931 
   932 
   933 (* attributes *)
   934 
   935 fun attrib f = Thm.declaration_attribute (fn th =>
   936    fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
   937     | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
   938 
   939 fun safe_dest w = attrib (addSE w o name_make_elim);
   940 val safe_elim = attrib o addSE;
   941 val safe_intro = attrib o addSI;
   942 fun haz_dest w = attrib (addE w o name_make_elim);
   943 val haz_elim = attrib o addE;
   944 val haz_intro = attrib o addI;
   945 val rule_del = attrib delrule o ContextRules.rule_del;
   946 
   947 
   948 (* tactics referring to the implicit claset *)
   949 
   950 (*the abstraction over the proof state delays the dereferencing*)
   951 fun Safe_tac st           = safe_tac (claset()) st;
   952 fun Safe_step_tac i st    = safe_step_tac (claset()) i st;
   953 fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
   954 fun Clarify_tac i st      = clarify_tac (claset()) i st;
   955 fun Step_tac i st         = step_tac (claset()) i st;
   956 fun Fast_tac i st         = fast_tac (claset()) i st;
   957 fun Best_tac i st         = best_tac (claset()) i st;
   958 fun Slow_tac i st         = slow_tac (claset()) i st;
   959 fun Slow_best_tac i st    = slow_best_tac (claset()) i st;
   960 fun Deepen_tac m          = deepen_tac (claset()) m;
   961 
   962 
   963 end;
   964 
   965 
   966 
   967 (** concrete syntax of attributes **)
   968 
   969 val introN = "intro";
   970 val elimN = "elim";
   971 val destN = "dest";
   972 val ruleN = "rule";
   973 
   974 val setup_attrs = Attrib.add_attributes
   975  [("swapped", swapped, "classical swap of introduction rule"),
   976   (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
   977     "declaration of Classical destruction rule"),
   978   (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
   979     "declaration of Classical elimination rule"),
   980   (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
   981     "declaration of Classical introduction rule"),
   982   (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
   983     "remove declaration of intro/elim/dest rule")];
   984 
   985 
   986 
   987 (** proof methods **)
   988 
   989 fun METHOD_CLASET tac ctxt =
   990   Method.METHOD (tac ctxt (local_claset_of ctxt));
   991 
   992 fun METHOD_CLASET' tac ctxt =
   993   Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
   994 
   995 
   996 local
   997 
   998 fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
   999   let
  1000     val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
  1001     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
  1002     val rules = rules1 @ rules2 @ rules3 @ rules4;
  1003     val ruleq = Drule.multi_resolves facts rules;
  1004   in
  1005     Method.trace ctxt rules;
  1006     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
  1007   end)
  1008   THEN_ALL_NEW Goal.norm_hhf_tac;
  1009 
  1010 fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
  1011   | rule_tac rules _ _ facts = Method.rule_tac rules facts;
  1012 
  1013 fun default_tac rules ctxt cs facts =
  1014   HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
  1015   ClassPackage.default_intro_classes_tac facts;
  1016 
  1017 in
  1018   val rule = METHOD_CLASET' o rule_tac;
  1019   val default = METHOD_CLASET o default_tac;
  1020 end;
  1021 
  1022 
  1023 (* contradiction method *)
  1024 
  1025 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
  1026 
  1027 
  1028 (* automatic methods *)
  1029 
  1030 val cla_modifiers =
  1031  [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
  1032   Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
  1033   Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
  1034   Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
  1035   Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
  1036   Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
  1037   Args.del -- Args.colon >> K (I, rule_del)];
  1038 
  1039 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
  1040   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
  1041 
  1042 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
  1043   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
  1044 
  1045 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
  1046 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
  1047 
  1048 
  1049 
  1050 (** setup_methods **)
  1051 
  1052 val setup_methods = Method.add_methods
  1053  [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
  1054   ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
  1055   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
  1056   ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
  1057   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
  1058   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
  1059   ("best", cla_method' best_tac, "classical prover (best-first)"),
  1060   ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
  1061   ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
  1062 
  1063 
  1064 
  1065 (** theory setup **)
  1066 
  1067 val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
  1068 
  1069 
  1070 
  1071 (** outer syntax **)
  1072 
  1073 val print_clasetP =
  1074   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
  1075     OuterKeyword.diag
  1076     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
  1077       (Toplevel.node_case
  1078         (Context.cases print_claset print_local_claset)
  1079         (print_local_claset o Proof.context_of)))));
  1080 
  1081 val _ = OuterSyntax.add_parsers [print_clasetP];
  1082 
  1083 
  1084 end;