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