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