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