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