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