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