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