src/Provers/classical.ML
author wenzelm
Sat Dec 30 16:08:03 2006 +0100 (2006-12-30)
changeset 21963 416a5338d2bb
parent 21689 58abd6d8abd1
child 22095 07875394618e
permissions -rw-r--r--
removed obsolete name_hint handling;
     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 print_local_claset: Proof.context -> unit
   144   val get_local_claset: Proof.context -> claset
   145   val put_local_claset: claset -> Proof.context -> Proof.context
   146   val safe_dest: 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 Drule.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 local
   303   fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l;
   304 in
   305   fun appSWrappers (CS{swrappers,...}) = wrap swrappers;
   306   fun appWrappers  (CS{uwrappers,...}) = wrap uwrappers;
   307 end;
   308 
   309 
   310 (*** Adding (un)safe introduction or elimination rules.
   311 
   312     In case of overlap, new rules are tried BEFORE old ones!!
   313 ***)
   314 
   315 (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
   316   assumptions.  Pairs elim rules with true. *)
   317 fun joinrules (intrs, elims) =
   318   (map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs;
   319 
   320 fun joinrules' (intrs, elims) =
   321   map (pair true) elims @ map (pair false) intrs;
   322 
   323 (*Priority: prefer rules with fewest subgoals,
   324   then rules added most recently (preferring the head of the list).*)
   325 fun tag_brls k [] = []
   326   | tag_brls k (brl::brls) =
   327       (1000000*subgoals_of_brl brl + k, brl) ::
   328       tag_brls (k+1) brls;
   329 
   330 fun tag_brls' _ _ [] = []
   331   | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
   332 
   333 fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
   334 
   335 (*Insert into netpair that already has nI intr rules and nE elim rules.
   336   Count the intr rules double (to account for swapify).  Negate to give the
   337   new insertions the lowest priority.*)
   338 fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
   339 fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
   340 
   341 fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
   342 fun delete x = delete_tagged_list (joinrules x);
   343 fun delete' x = delete_tagged_list (joinrules' x);
   344 
   345 val mem_thm = member Drule.eq_thm_prop
   346 and rem_thm = remove Drule.eq_thm_prop;
   347 
   348 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   349   is still allowed.*)
   350 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   351        if mem_thm safeIs th then
   352          warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
   353   else if mem_thm safeEs th then
   354          warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   355   else if mem_thm hazIs th then
   356          warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
   357   else if mem_thm hazEs th then
   358          warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
   359   else ();
   360 
   361 
   362 (*** Safe rules ***)
   363 
   364 fun addSI w th
   365   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   366              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   367   if mem_thm safeIs th then
   368          (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
   369           cs)
   370   else
   371   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   372           List.partition Thm.no_prems [th]
   373       val nI = length safeIs + 1
   374       and nE = length safeEs
   375   in warn_dup th cs;
   376      CS{safeIs  = th::safeIs,
   377         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   378         safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   379         safeEs  = safeEs,
   380         hazIs   = hazIs,
   381         hazEs   = hazEs,
   382         swrappers    = swrappers,
   383         uwrappers    = uwrappers,
   384         haz_netpair  = haz_netpair,
   385         dup_netpair  = dup_netpair,
   386         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
   387   end;
   388 
   389 fun addSE w th
   390   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   391              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   392   if mem_thm safeEs th then
   393          (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
   394           cs)
   395   else if has_fewer_prems 1 th then
   396     	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   397   else
   398   let
   399       val th' = classical_rule th
   400       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   401           List.partition (fn rl => nprems_of rl=1) [th']
   402       val nI = length safeIs
   403       and nE = length safeEs + 1
   404   in warn_dup th cs;
   405      CS{safeEs  = th::safeEs,
   406         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   407         safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   408         safeIs  = safeIs,
   409         hazIs   = hazIs,
   410         hazEs   = hazEs,
   411         swrappers    = swrappers,
   412         uwrappers    = uwrappers,
   413         haz_netpair  = haz_netpair,
   414         dup_netpair  = dup_netpair,
   415         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
   416   end;
   417 
   418 fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   419 fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   420 
   421 fun make_elim th =
   422     if has_fewer_prems 1 th then
   423     	error("Ill-formed destruction rule\n" ^ string_of_thm th)
   424     else Tactic.make_elim th;
   425 
   426 fun cs addSDs ths = cs addSEs (map make_elim ths);
   427 
   428 
   429 (*** Hazardous (unsafe) rules ***)
   430 
   431 fun addI w th
   432   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   433              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   434   if mem_thm hazIs th then
   435          (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
   436           cs)
   437   else
   438   let val nI = length hazIs + 1
   439       and nE = length hazEs
   440   in warn_dup th cs;
   441      CS{hazIs   = th::hazIs,
   442         haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
   443         dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
   444         safeIs  = safeIs,
   445         safeEs  = safeEs,
   446         hazEs   = hazEs,
   447         swrappers     = swrappers,
   448         uwrappers     = uwrappers,
   449         safe0_netpair = safe0_netpair,
   450         safep_netpair = safep_netpair,
   451         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   452   end
   453   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   454          error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   455 
   456 fun addE w th
   457   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   458             safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   459   if mem_thm hazEs th then
   460          (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
   461           cs)
   462   else if has_fewer_prems 1 th then
   463     	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   464   else
   465   let
   466       val th' = classical_rule th
   467       val nI = length hazIs
   468       and nE = length hazEs + 1
   469   in warn_dup th cs;
   470      CS{hazEs   = th::hazEs,
   471         haz_netpair = insert (nI,nE) ([], [th']) haz_netpair,
   472         dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair,
   473         safeIs  = safeIs,
   474         safeEs  = safeEs,
   475         hazIs   = hazIs,
   476         swrappers     = swrappers,
   477         uwrappers     = uwrappers,
   478         safe0_netpair = safe0_netpair,
   479         safep_netpair = safep_netpair,
   480         xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair}
   481   end;
   482 
   483 fun cs addIs ths = fold_rev (addI NONE) ths cs;
   484 fun cs addEs ths = fold_rev (addE NONE) ths cs;
   485 
   486 fun cs addDs ths = cs addEs (map make_elim ths);
   487 
   488 
   489 (*** Deletion of rules
   490      Working out what to delete, requires repeating much of the code used
   491         to insert.
   492 ***)
   493 
   494 fun delSI th
   495           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   496                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   497  if mem_thm safeIs th then
   498    let val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th]
   499    in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   500          safep_netpair = delete (safep_rls, []) safep_netpair,
   501          safeIs = rem_thm th safeIs,
   502          safeEs = safeEs,
   503          hazIs  = hazIs,
   504          hazEs  = hazEs,
   505          swrappers    = swrappers,
   506          uwrappers    = uwrappers,
   507          haz_netpair  = haz_netpair,
   508          dup_netpair  = dup_netpair,
   509          xtra_netpair = delete' ([th], []) xtra_netpair}
   510    end
   511  else cs;
   512 
   513 fun delSE th
   514           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   515                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   516   if mem_thm safeEs th then
   517     let
   518       val th' = classical_rule th
   519       val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
   520     in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   521          safep_netpair = delete ([], safep_rls) safep_netpair,
   522          safeIs = safeIs,
   523          safeEs = rem_thm th safeEs,
   524          hazIs  = hazIs,
   525          hazEs  = hazEs,
   526          swrappers    = swrappers,
   527          uwrappers    = uwrappers,
   528          haz_netpair  = haz_netpair,
   529          dup_netpair  = dup_netpair,
   530          xtra_netpair = delete' ([], [th]) xtra_netpair}
   531     end
   532   else cs;
   533 
   534 
   535 fun delI th
   536          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   537                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   538  if mem_thm hazIs th then
   539      CS{haz_netpair = delete ([th], []) haz_netpair,
   540         dup_netpair = delete ([dup_intr th], []) dup_netpair,
   541         safeIs  = safeIs,
   542         safeEs  = safeEs,
   543         hazIs   = rem_thm th hazIs,
   544         hazEs   = hazEs,
   545         swrappers     = swrappers,
   546         uwrappers     = uwrappers,
   547         safe0_netpair = safe0_netpair,
   548         safep_netpair = safep_netpair,
   549         xtra_netpair = delete' ([th], []) xtra_netpair}
   550  else cs
   551  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   552         error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   553 
   554 
   555 fun delE th
   556          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   557                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   558   let val th' = classical_rule th in
   559     if mem_thm hazEs th then
   560      CS{haz_netpair = delete ([], [th']) haz_netpair,
   561         dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   562         safeIs  = safeIs,
   563         safeEs  = safeEs,
   564         hazIs   = hazIs,
   565         hazEs   = rem_thm th hazEs,
   566         swrappers     = swrappers,
   567         uwrappers     = uwrappers,
   568         safe0_netpair = safe0_netpair,
   569         safep_netpair = safep_netpair,
   570         xtra_netpair = delete' ([], [th]) xtra_netpair}
   571      else cs
   572    end;
   573 
   574 
   575 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   576 fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   577   let val th' = Tactic.make_elim th in
   578     if mem_thm safeIs th orelse mem_thm safeEs th orelse
   579       mem_thm hazIs th orelse mem_thm hazEs th orelse
   580       mem_thm safeEs th' orelse mem_thm hazEs th'
   581     then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   582     else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs)
   583   end;
   584 
   585 fun cs delrules ths = fold delrule ths cs;
   586 
   587 
   588 (*** Modifying the wrapper tacticals ***)
   589 fun update_swrappers
   590 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   591     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
   592  CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   593     swrappers = f swrappers, uwrappers = uwrappers,
   594     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   595     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   596 
   597 fun update_uwrappers
   598 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   599     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f =
   600  CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   601     swrappers = swrappers, uwrappers = f uwrappers,
   602     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   603     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   604 
   605 
   606 (*Add/replace a safe wrapper*)
   607 fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers =>
   608     overwrite_warn (swrappers, new_swrapper)
   609        ("Overwriting safe wrapper " ^ fst new_swrapper));
   610 
   611 (*Add/replace an unsafe wrapper*)
   612 fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
   613     overwrite_warn (uwrappers, new_uwrapper)
   614         ("Overwriting unsafe wrapper "^fst new_uwrapper));
   615 
   616 (*Remove a safe wrapper*)
   617 fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
   618   let val swrappers' = filter_out (equal name o fst) swrappers in
   619     if length swrappers <> length swrappers' then swrappers'
   620     else (warning ("No such safe wrapper in claset: "^ name); swrappers)
   621   end);
   622 
   623 (*Remove an unsafe wrapper*)
   624 fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
   625   let val uwrappers' = filter_out (equal name o fst) uwrappers in
   626     if length uwrappers <> length uwrappers' then uwrappers'
   627     else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers)
   628   end);
   629 
   630 (* compose a safe tactic alternatively before/after safe_step_tac *)
   631 fun cs addSbefore  (name,    tac1) =
   632     cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   633 fun cs addSafter   (name,    tac2) =
   634     cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   635 
   636 (*compose a tactic alternatively before/after the step tactic *)
   637 fun cs addbefore   (name,    tac1) =
   638     cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
   639 fun cs addafter    (name,    tac2) =
   640     cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
   641 
   642 fun cs addD2     (name, thm) =
   643     cs addafter  (name, datac thm 1);
   644 fun cs addE2     (name, thm) =
   645     cs addafter  (name, eatac thm 1);
   646 fun cs addSD2    (name, thm) =
   647     cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   648 fun cs addSE2    (name, thm) =
   649     cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   650 
   651 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   652   Merging the term nets may look more efficient, but the rather delicate
   653   treatment of priority might get muddled up.*)
   654 fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
   655      CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
   656   let val safeIs' = fold rem_thm safeIs safeIs2
   657       val safeEs' = fold rem_thm safeEs safeEs2
   658       val hazIs' = fold rem_thm hazIs hazIs2
   659       val hazEs' = fold rem_thm hazEs hazEs2
   660       val cs1   = cs addSIs safeIs'
   661                      addSEs safeEs'
   662                      addIs  hazIs'
   663                      addEs  hazEs'
   664       val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers);
   665       val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers);
   666   in cs3
   667   end;
   668 
   669 
   670 (**** Simple tactics for theorem proving ****)
   671 
   672 (*Attack subgoals using safe inferences -- matching, not resolution*)
   673 fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   674   appSWrappers cs (FIRST' [
   675         eq_assume_tac,
   676         eq_mp_tac,
   677         bimatch_from_nets_tac safe0_netpair,
   678         FIRST' hyp_subst_tacs,
   679         bimatch_from_nets_tac safep_netpair]);
   680 
   681 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   682 fun safe_steps_tac cs = REPEAT_DETERM1 o
   683         (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   684 
   685 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   686 fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   687 
   688 
   689 (*** Clarify_tac: do safe steps without causing branching ***)
   690 
   691 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   692 
   693 (*version of bimatch_from_nets_tac that only applies rules that
   694   create precisely n subgoals.*)
   695 fun n_bimatch_from_nets_tac n =
   696     biresolution_from_nets_tac (Tactic.orderlist o List.filter (nsubgoalsP n)) true;
   697 
   698 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   699 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   700 
   701 (*Two-way branching is allowed only if one of the branches immediately closes*)
   702 fun bimatch2_tac netpair i =
   703     n_bimatch_from_nets_tac 2 netpair i THEN
   704     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
   705 
   706 (*Attack subgoals using safe inferences -- matching, not resolution*)
   707 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   708   appSWrappers cs (FIRST' [
   709         eq_assume_contr_tac,
   710         bimatch_from_nets_tac safe0_netpair,
   711         FIRST' hyp_subst_tacs,
   712         n_bimatch_from_nets_tac 1 safep_netpair,
   713         bimatch2_tac safep_netpair]);
   714 
   715 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   716 
   717 
   718 (*** Unsafe steps instantiate variables or lose information ***)
   719 
   720 (*Backtracking is allowed among the various these unsafe ways of
   721   proving a subgoal.  *)
   722 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   723   assume_tac                      APPEND'
   724   contr_tac                       APPEND'
   725   biresolve_from_nets_tac safe0_netpair;
   726 
   727 (*These unsafe steps could generate more subgoals.*)
   728 fun instp_step_tac (CS{safep_netpair,...}) =
   729   biresolve_from_nets_tac safep_netpair;
   730 
   731 (*These steps could instantiate variables and are therefore unsafe.*)
   732 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   733 
   734 fun haz_step_tac (CS{haz_netpair,...}) =
   735   biresolve_from_nets_tac haz_netpair;
   736 
   737 (*Single step for the prover.  FAILS unless it makes progress. *)
   738 fun step_tac cs i = safe_tac cs ORELSE appWrappers cs
   739         (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   740 
   741 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   742   allows backtracking from "safe" rules to "unsafe" rules here.*)
   743 fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs
   744         (inst_step_tac cs APPEND' haz_step_tac cs) i;
   745 
   746 (**** The following tactics all fail unless they solve one goal ****)
   747 
   748 (*Dumb but fast*)
   749 fun fast_tac cs =
   750   ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   751 
   752 (*Slower but smarter than fast_tac*)
   753 fun best_tac cs =
   754   ObjectLogic.atomize_tac THEN'
   755   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   756 
   757 (*even a bit smarter than best_tac*)
   758 fun first_best_tac cs =
   759   ObjectLogic.atomize_tac THEN'
   760   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   761 
   762 fun slow_tac cs =
   763   ObjectLogic.atomize_tac THEN'
   764   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   765 
   766 fun slow_best_tac cs =
   767   ObjectLogic.atomize_tac THEN'
   768   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   769 
   770 
   771 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   772 val weight_ASTAR = ref 5;
   773 
   774 fun astar_tac cs =
   775   ObjectLogic.atomize_tac THEN'
   776   SELECT_GOAL
   777     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   778       (step_tac cs 1));
   779 
   780 fun slow_astar_tac cs =
   781   ObjectLogic.atomize_tac THEN'
   782   SELECT_GOAL
   783     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   784       (slow_step_tac cs 1));
   785 
   786 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   787   of much experimentation!  Changing APPEND to ORELSE below would prove
   788   easy theorems faster, but loses completeness -- and many of the harder
   789   theorems such as 43. ****)
   790 
   791 (*Non-deterministic!  Could always expand the first unsafe connective.
   792   That's hard to implement and did not perform better in experiments, due to
   793   greater search depth required.*)
   794 fun dup_step_tac (cs as (CS{dup_netpair,...})) =
   795   biresolve_from_nets_tac dup_netpair;
   796 
   797 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   798 local
   799 fun slow_step_tac' cs = appWrappers cs
   800         (instp_step_tac cs APPEND' dup_step_tac cs);
   801 in fun depth_tac cs m i state = SELECT_GOAL
   802    (safe_steps_tac cs 1 THEN_ELSE
   803         (DEPTH_SOLVE (depth_tac cs m 1),
   804          inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   805                 (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   806         )) i state;
   807 end;
   808 
   809 (*Search, with depth bound m.
   810   This is the "entry point", which does safe inferences first.*)
   811 fun safe_depth_tac cs m =
   812   SUBGOAL
   813     (fn (prem,i) =>
   814       let val deti =
   815           (*No Vars in the goal?  No need to backtrack between goals.*)
   816           case term_vars prem of
   817               []        => DETERM
   818             | _::_      => I
   819       in  SELECT_GOAL (TRY (safe_tac cs) THEN
   820                        DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   821       end);
   822 
   823 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   824 
   825 
   826 
   827 (** context dependent claset components **)
   828 
   829 datatype context_cs = ContextCS of
   830  {swrappers: (string * (Proof.context -> wrapper)) list,
   831   uwrappers: (string * (Proof.context -> wrapper)) list};
   832 
   833 fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
   834   let
   835     fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
   836   in
   837     cs |> fold_rev (add_wrapper (op addSWrapper)) swrappers
   838     |> fold_rev (add_wrapper (op addWrapper)) uwrappers
   839   end;
   840 
   841 fun make_context_cs (swrappers, uwrappers) =
   842   ContextCS {swrappers = swrappers, uwrappers = uwrappers};
   843 
   844 val empty_context_cs = make_context_cs ([], []);
   845 
   846 fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
   847   let
   848     val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
   849     val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
   850 
   851     val swrappers' = merge_alists swrappers1 swrappers2;
   852     val uwrappers' = merge_alists uwrappers1 uwrappers2;
   853   in make_context_cs (swrappers', uwrappers') end;
   854 
   855 
   856 
   857 (** claset data **)
   858 
   859 (* global claset *)
   860 
   861 structure GlobalClaset = TheoryDataFun
   862 (struct
   863   val name = "Provers/claset";
   864   type T = claset ref * context_cs;
   865 
   866   val empty = (ref empty_cs, empty_context_cs);
   867   fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
   868   val extend = copy;
   869   fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
   870     (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
   871   fun print _ (ref cs, _) = print_cs cs;
   872 end);
   873 
   874 val print_claset = GlobalClaset.print;
   875 val get_claset = ! o #1 o GlobalClaset.get;
   876 
   877 val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
   878 fun map_context_cs f = GlobalClaset.map (apsnd
   879   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
   880 
   881 val change_claset_of = change o #1 o GlobalClaset.get;
   882 fun change_claset f = change_claset_of (Context.the_context ()) f;
   883 
   884 fun claset_of thy =
   885   let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
   886   in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
   887 val claset = claset_of o Context.the_context;
   888 
   889 fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
   890 fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
   891 
   892 fun AddDs args = change_claset (fn cs => cs addDs args);
   893 fun AddEs args = change_claset (fn cs => cs addEs args);
   894 fun AddIs args = change_claset (fn cs => cs addIs args);
   895 fun AddSDs args = change_claset (fn cs => cs addSDs args);
   896 fun AddSEs args = change_claset (fn cs => cs addSEs args);
   897 fun AddSIs args = change_claset (fn cs => cs addSIs args);
   898 fun Delrules args = change_claset (fn cs => cs delrules args);
   899 
   900 
   901 (* context dependent components *)
   902 
   903 fun add_context_safe_wrapper wrapper = map_context_cs (apfst (merge_alists [wrapper]));
   904 fun del_context_safe_wrapper name = map_context_cs (apfst (filter_out (equal name o #1)));
   905 
   906 fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd (merge_alists [wrapper]));
   907 fun del_context_unsafe_wrapper name = map_context_cs (apsnd (filter_out (equal name o #1)));
   908 
   909 
   910 (* local claset *)
   911 
   912 structure LocalClaset = ProofDataFun
   913 (struct
   914   val name = "Provers/claset";
   915   type T = claset;
   916   val init = get_claset;
   917   fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
   918 end);
   919 
   920 val print_local_claset = LocalClaset.print;
   921 val get_local_claset = LocalClaset.get;
   922 val put_local_claset = LocalClaset.put;
   923 
   924 fun local_claset_of ctxt =
   925   context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
   926 
   927 
   928 (* attributes *)
   929 
   930 fun attrib f = Thm.declaration_attribute (fn th =>
   931    fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
   932     | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
   933 
   934 fun safe_dest w = attrib (addSE w o make_elim);
   935 val safe_elim = attrib o addSE;
   936 val safe_intro = attrib o addSI;
   937 fun haz_dest w = attrib (addE w o make_elim);
   938 val haz_elim = attrib o addE;
   939 val haz_intro = attrib o addI;
   940 val rule_del = attrib delrule o ContextRules.rule_del;
   941 
   942 
   943 (* tactics referring to the implicit claset *)
   944 
   945 (*the abstraction over the proof state delays the dereferencing*)
   946 fun Safe_tac st           = safe_tac (claset()) st;
   947 fun Safe_step_tac i st    = safe_step_tac (claset()) i st;
   948 fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
   949 fun Clarify_tac i st      = clarify_tac (claset()) i st;
   950 fun Step_tac i st         = step_tac (claset()) i st;
   951 fun Fast_tac i st         = fast_tac (claset()) i st;
   952 fun Best_tac i st         = best_tac (claset()) i st;
   953 fun Slow_tac i st         = slow_tac (claset()) i st;
   954 fun Slow_best_tac i st    = slow_best_tac (claset()) i st;
   955 fun Deepen_tac m          = deepen_tac (claset()) m;
   956 
   957 
   958 end;
   959 
   960 
   961 
   962 (** concrete syntax of attributes **)
   963 
   964 val introN = "intro";
   965 val elimN = "elim";
   966 val destN = "dest";
   967 val ruleN = "rule";
   968 
   969 val setup_attrs = Attrib.add_attributes
   970  [("swapped", swapped, "classical swap of introduction rule"),
   971   (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
   972     "declaration of Classical destruction rule"),
   973   (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
   974     "declaration of Classical elimination rule"),
   975   (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
   976     "declaration of Classical introduction rule"),
   977   (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
   978     "remove declaration of intro/elim/dest rule")];
   979 
   980 
   981 
   982 (** proof methods **)
   983 
   984 fun METHOD_CLASET tac ctxt =
   985   Method.METHOD (tac ctxt (local_claset_of ctxt));
   986 
   987 fun METHOD_CLASET' tac ctxt =
   988   Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
   989 
   990 
   991 local
   992 
   993 fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
   994   let
   995     val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
   996     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
   997     val rules = rules1 @ rules2 @ rules3 @ rules4;
   998     val ruleq = Drule.multi_resolves facts rules;
   999   in
  1000     Method.trace ctxt rules;
  1001     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
  1002   end)
  1003   THEN_ALL_NEW Goal.norm_hhf_tac;
  1004 
  1005 fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
  1006   | rule_tac rules _ _ facts = Method.rule_tac rules facts;
  1007 
  1008 fun default_tac rules ctxt cs facts =
  1009   HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
  1010   ClassPackage.default_intro_classes_tac facts;
  1011 
  1012 in
  1013   val rule = METHOD_CLASET' o rule_tac;
  1014   val default = METHOD_CLASET o default_tac;
  1015 end;
  1016 
  1017 
  1018 (* contradiction method *)
  1019 
  1020 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
  1021 
  1022 
  1023 (* automatic methods *)
  1024 
  1025 val cla_modifiers =
  1026  [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
  1027   Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
  1028   Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
  1029   Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
  1030   Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
  1031   Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
  1032   Args.del -- Args.colon >> K (I, rule_del)];
  1033 
  1034 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
  1035   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
  1036 
  1037 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
  1038   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
  1039 
  1040 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
  1041 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
  1042 
  1043 
  1044 
  1045 (** setup_methods **)
  1046 
  1047 val setup_methods = Method.add_methods
  1048  [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
  1049   ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
  1050   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
  1051   ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
  1052   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
  1053   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
  1054   ("best", cla_method' best_tac, "classical prover (best-first)"),
  1055   ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
  1056   ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
  1057 
  1058 
  1059 
  1060 (** theory setup **)
  1061 
  1062 val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
  1063 
  1064 
  1065 
  1066 (** outer syntax **)
  1067 
  1068 val print_clasetP =
  1069   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
  1070     OuterKeyword.diag
  1071     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
  1072       (Toplevel.node_case
  1073         (Context.cases print_claset print_local_claset)
  1074         (print_local_claset o Proof.context_of)))));
  1075 
  1076 val _ = OuterSyntax.add_parsers [print_clasetP];
  1077 
  1078 
  1079 end;