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