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