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