src/Provers/classical.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 24358 d75af3e90e82
child 26412 0918f5c0bbca
permissions -rw-r--r--
simplified interfaces for outer syntax;
     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' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
   659       swrappers, uwrappers, ...}) =
   660   if pointer_eq (cs, cs') then cs
   661   else
   662     let
   663       val safeIs' = fold rem_thm safeIs safeIs2;
   664       val safeEs' = fold rem_thm safeEs safeEs2;
   665       val hazIs' = fold rem_thm hazIs hazIs2;
   666       val hazEs' = fold rem_thm hazEs hazEs2;
   667       val cs1   = cs addSIs safeIs'
   668                      addSEs safeEs'
   669                      addIs  hazIs'
   670                      addEs  hazEs';
   671       val cs2 = map_swrappers
   672         (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
   673       val cs3 = map_uwrappers
   674         (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
   675     in cs3 end;
   676 
   677 
   678 (**** Simple tactics for theorem proving ****)
   679 
   680 (*Attack subgoals using safe inferences -- matching, not resolution*)
   681 fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   682   appSWrappers cs (FIRST' [
   683         eq_assume_tac,
   684         eq_mp_tac,
   685         bimatch_from_nets_tac safe0_netpair,
   686         FIRST' hyp_subst_tacs,
   687         bimatch_from_nets_tac safep_netpair]);
   688 
   689 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   690 fun safe_steps_tac cs = REPEAT_DETERM1 o
   691         (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   692 
   693 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   694 fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   695 
   696 
   697 (*** Clarify_tac: do safe steps without causing branching ***)
   698 
   699 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   700 
   701 (*version of bimatch_from_nets_tac that only applies rules that
   702   create precisely n subgoals.*)
   703 fun n_bimatch_from_nets_tac n =
   704     biresolution_from_nets_tac (Tactic.orderlist o List.filter (nsubgoalsP n)) true;
   705 
   706 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   707 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   708 
   709 (*Two-way branching is allowed only if one of the branches immediately closes*)
   710 fun bimatch2_tac netpair i =
   711     n_bimatch_from_nets_tac 2 netpair i THEN
   712     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
   713 
   714 (*Attack subgoals using safe inferences -- matching, not resolution*)
   715 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   716   appSWrappers cs (FIRST' [
   717         eq_assume_contr_tac,
   718         bimatch_from_nets_tac safe0_netpair,
   719         FIRST' hyp_subst_tacs,
   720         n_bimatch_from_nets_tac 1 safep_netpair,
   721         bimatch2_tac safep_netpair]);
   722 
   723 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   724 
   725 
   726 (*** Unsafe steps instantiate variables or lose information ***)
   727 
   728 (*Backtracking is allowed among the various these unsafe ways of
   729   proving a subgoal.  *)
   730 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   731   assume_tac                      APPEND'
   732   contr_tac                       APPEND'
   733   biresolve_from_nets_tac safe0_netpair;
   734 
   735 (*These unsafe steps could generate more subgoals.*)
   736 fun instp_step_tac (CS{safep_netpair,...}) =
   737   biresolve_from_nets_tac safep_netpair;
   738 
   739 (*These steps could instantiate variables and are therefore unsafe.*)
   740 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   741 
   742 fun haz_step_tac (CS{haz_netpair,...}) =
   743   biresolve_from_nets_tac haz_netpair;
   744 
   745 (*Single step for the prover.  FAILS unless it makes progress. *)
   746 fun step_tac cs i = safe_tac cs ORELSE appWrappers cs
   747         (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   748 
   749 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   750   allows backtracking from "safe" rules to "unsafe" rules here.*)
   751 fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs
   752         (inst_step_tac cs APPEND' haz_step_tac cs) i;
   753 
   754 (**** The following tactics all fail unless they solve one goal ****)
   755 
   756 (*Dumb but fast*)
   757 fun fast_tac cs =
   758   ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   759 
   760 (*Slower but smarter than fast_tac*)
   761 fun best_tac cs =
   762   ObjectLogic.atomize_prems_tac THEN'
   763   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   764 
   765 (*even a bit smarter than best_tac*)
   766 fun first_best_tac cs =
   767   ObjectLogic.atomize_prems_tac THEN'
   768   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   769 
   770 fun slow_tac cs =
   771   ObjectLogic.atomize_prems_tac THEN'
   772   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   773 
   774 fun slow_best_tac cs =
   775   ObjectLogic.atomize_prems_tac THEN'
   776   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   777 
   778 
   779 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   780 val weight_ASTAR = ref 5;
   781 
   782 fun astar_tac cs =
   783   ObjectLogic.atomize_prems_tac THEN'
   784   SELECT_GOAL
   785     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   786       (step_tac cs 1));
   787 
   788 fun slow_astar_tac cs =
   789   ObjectLogic.atomize_prems_tac THEN'
   790   SELECT_GOAL
   791     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   792       (slow_step_tac cs 1));
   793 
   794 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   795   of much experimentation!  Changing APPEND to ORELSE below would prove
   796   easy theorems faster, but loses completeness -- and many of the harder
   797   theorems such as 43. ****)
   798 
   799 (*Non-deterministic!  Could always expand the first unsafe connective.
   800   That's hard to implement and did not perform better in experiments, due to
   801   greater search depth required.*)
   802 fun dup_step_tac (cs as (CS{dup_netpair,...})) =
   803   biresolve_from_nets_tac dup_netpair;
   804 
   805 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   806 local
   807 fun slow_step_tac' cs = appWrappers cs
   808         (instp_step_tac cs APPEND' dup_step_tac cs);
   809 in fun depth_tac cs m i state = SELECT_GOAL
   810    (safe_steps_tac cs 1 THEN_ELSE
   811         (DEPTH_SOLVE (depth_tac cs m 1),
   812          inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   813                 (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   814         )) i state;
   815 end;
   816 
   817 (*Search, with depth bound m.
   818   This is the "entry point", which does safe inferences first.*)
   819 fun safe_depth_tac cs m =
   820   SUBGOAL
   821     (fn (prem,i) =>
   822       let val deti =
   823           (*No Vars in the goal?  No need to backtrack between goals.*)
   824           case term_vars prem of
   825               []        => DETERM
   826             | _::_      => I
   827       in  SELECT_GOAL (TRY (safe_tac cs) THEN
   828                        DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   829       end);
   830 
   831 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   832 
   833 
   834 
   835 (** context dependent claset components **)
   836 
   837 datatype context_cs = ContextCS of
   838  {swrappers: (string * (Proof.context -> wrapper)) list,
   839   uwrappers: (string * (Proof.context -> wrapper)) list};
   840 
   841 fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
   842   let
   843     fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
   844   in
   845     cs
   846     |> fold_rev (add_wrapper (op addSWrapper)) swrappers
   847     |> fold_rev (add_wrapper (op addWrapper)) uwrappers
   848   end;
   849 
   850 fun make_context_cs (swrappers, uwrappers) =
   851   ContextCS {swrappers = swrappers, uwrappers = uwrappers};
   852 
   853 val empty_context_cs = make_context_cs ([], []);
   854 
   855 fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
   856   if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
   857   else
   858     let
   859       val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
   860       val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
   861       val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
   862       val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
   863     in make_context_cs (swrappers', uwrappers') end;
   864 
   865 
   866 
   867 (** claset data **)
   868 
   869 (* global clasets *)
   870 
   871 structure GlobalClaset = TheoryDataFun
   872 (
   873   type T = claset ref * context_cs;
   874   val empty = (ref empty_cs, empty_context_cs);
   875   fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
   876   val extend = copy;
   877   fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
   878     (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
   879 );
   880 
   881 val print_claset = print_cs o ! o #1 o GlobalClaset.get;
   882 val get_claset = ! o #1 o GlobalClaset.get;
   883 
   884 val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
   885 fun map_context_cs f = GlobalClaset.map (apsnd
   886   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
   887 
   888 val change_claset_of = change o #1 o GlobalClaset.get;
   889 fun change_claset f = change_claset_of (ML_Context.the_context ()) f;
   890 
   891 fun claset_of thy =
   892   let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
   893   in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
   894 val claset = claset_of o ML_Context.the_context;
   895 
   896 fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
   897 fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
   898 
   899 fun AddDs args = change_claset (fn cs => cs addDs args);
   900 fun AddEs args = change_claset (fn cs => cs addEs args);
   901 fun AddIs args = change_claset (fn cs => cs addIs args);
   902 fun AddSDs args = change_claset (fn cs => cs addSDs args);
   903 fun AddSEs args = change_claset (fn cs => cs addSEs args);
   904 fun AddSIs args = change_claset (fn cs => cs addSIs args);
   905 fun Delrules args = change_claset (fn cs => cs delrules args);
   906 
   907 
   908 (* context dependent components *)
   909 
   910 fun add_context_safe_wrapper wrapper = (map_context_cs o apfst)
   911   (AList.update (op =) wrapper);
   912 fun del_context_safe_wrapper name = (map_context_cs o apfst)
   913   (AList.delete (op =) name);
   914 
   915 fun add_context_unsafe_wrapper wrapper = (map_context_cs o apsnd)
   916   (AList.update (op =) wrapper);
   917 fun del_context_unsafe_wrapper name = (map_context_cs o apsnd)
   918   (AList.delete (op =) name);
   919 
   920 
   921 (* local clasets *)
   922 
   923 structure LocalClaset = ProofDataFun
   924 (
   925   type T = claset;
   926   val init = get_claset;
   927 );
   928 
   929 val get_local_claset = LocalClaset.get;
   930 val put_local_claset = LocalClaset.put;
   931 
   932 fun local_claset_of ctxt =
   933   context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
   934 
   935 val print_local_claset = print_cs o local_claset_of;
   936 
   937 
   938 (* generic clasets *)
   939 
   940 fun get_cs (Context.Theory thy) = claset_of thy
   941   | get_cs (Context.Proof ctxt) = local_claset_of ctxt;
   942 
   943 fun map_cs f (Context.Theory thy) = (change_claset_of thy f; Context.Theory thy)
   944   | map_cs f (Context.Proof ctxt) = Context.Proof (LocalClaset.map f ctxt);
   945 
   946 
   947 (* attributes *)
   948 
   949 fun attrib f = Thm.declaration_attribute (fn th =>
   950    fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
   951     | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
   952 
   953 fun safe_dest w = attrib (addSE w o make_elim);
   954 val safe_elim = attrib o addSE;
   955 val safe_intro = attrib o addSI;
   956 fun haz_dest w = attrib (addE w o make_elim);
   957 val haz_elim = attrib o addE;
   958 val haz_intro = attrib o addI;
   959 val rule_del = attrib delrule o ContextRules.rule_del;
   960 
   961 
   962 (* tactics referring to the implicit claset *)
   963 
   964 (*the abstraction over the proof state delays the dereferencing*)
   965 fun Safe_tac st           = safe_tac (claset()) st;
   966 fun Safe_step_tac i st    = safe_step_tac (claset()) i st;
   967 fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
   968 fun Clarify_tac i st      = clarify_tac (claset()) i st;
   969 fun Step_tac i st         = step_tac (claset()) i st;
   970 fun Fast_tac i st         = fast_tac (claset()) i st;
   971 fun Best_tac i st         = best_tac (claset()) i st;
   972 fun Slow_tac i st         = slow_tac (claset()) i st;
   973 fun Slow_best_tac i st    = slow_best_tac (claset()) i st;
   974 fun Deepen_tac m          = deepen_tac (claset()) m;
   975 
   976 
   977 end;
   978 
   979 
   980 
   981 (** concrete syntax of attributes **)
   982 
   983 val introN = "intro";
   984 val elimN = "elim";
   985 val destN = "dest";
   986 val ruleN = "rule";
   987 
   988 val setup_attrs = Attrib.add_attributes
   989  [("swapped", swapped, "classical swap of introduction rule"),
   990   (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
   991     "declaration of Classical destruction rule"),
   992   (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
   993     "declaration of Classical elimination rule"),
   994   (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
   995     "declaration of Classical introduction rule"),
   996   (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
   997     "remove declaration of intro/elim/dest rule")];
   998 
   999 
  1000 
  1001 (** proof methods **)
  1002 
  1003 fun METHOD_CLASET tac ctxt =
  1004   Method.METHOD (tac ctxt (local_claset_of ctxt));
  1005 
  1006 fun METHOD_CLASET' tac ctxt =
  1007   Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
  1008 
  1009 
  1010 local
  1011 
  1012 fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
  1013   let
  1014     val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
  1015     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
  1016     val rules = rules1 @ rules2 @ rules3 @ rules4;
  1017     val ruleq = Drule.multi_resolves facts rules;
  1018   in
  1019     Method.trace ctxt rules;
  1020     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
  1021   end)
  1022   THEN_ALL_NEW Goal.norm_hhf_tac;
  1023 
  1024 fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
  1025   | rule_tac rules _ _ facts = Method.rule_tac rules facts;
  1026 
  1027 fun default_tac rules ctxt cs facts =
  1028   HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
  1029   Class.default_intro_classes_tac facts;
  1030 
  1031 in
  1032   val rule = METHOD_CLASET' o rule_tac;
  1033   val default = METHOD_CLASET o default_tac;
  1034 end;
  1035 
  1036 
  1037 (* contradiction method *)
  1038 
  1039 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
  1040 
  1041 
  1042 (* automatic methods *)
  1043 
  1044 val cla_modifiers =
  1045  [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
  1046   Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
  1047   Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
  1048   Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
  1049   Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
  1050   Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
  1051   Args.del -- Args.colon >> K (I, rule_del)];
  1052 
  1053 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
  1054   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
  1055 
  1056 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
  1057   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
  1058 
  1059 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
  1060 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
  1061 
  1062 
  1063 
  1064 (** setup_methods **)
  1065 
  1066 val setup_methods = Method.add_methods
  1067  [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
  1068   ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
  1069   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
  1070   ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
  1071   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
  1072   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
  1073   ("best", cla_method' best_tac, "classical prover (best-first)"),
  1074   ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
  1075   ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
  1076 
  1077 
  1078 
  1079 (** theory setup **)
  1080 
  1081 val setup = GlobalClaset.init #> setup_attrs #> setup_methods;
  1082 
  1083 
  1084 
  1085 (** outer syntax **)
  1086 
  1087 val _ =
  1088   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
  1089     OuterKeyword.diag
  1090     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
  1091       (Toplevel.node_case
  1092         (Context.cases print_claset print_local_claset)
  1093         (print_local_claset o Proof.context_of)))));
  1094 
  1095 end;