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