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