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