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