src/Provers/classical.ML
author oheimb
Wed Feb 25 20:29:58 1998 +0100 (1998-02-25)
changeset 4653 d60f76680bf4
parent 4651 70dd492a1698
child 4742 a25bb8a260ae
permissions -rw-r--r--
renamed rep_claset to rep_cs
     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 
    22 
    23 (*should be a type abbreviation in signature CLASSICAL*)
    24 type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    25 type wrapper = (int -> tactic) -> (int -> tactic);
    26 
    27 signature CLASET_THY_DATA =
    28 sig
    29   val clasetK: string
    30   exception ClasetData of object ref
    31   val thy_data: string * (object * (object -> object) *
    32     (object * object -> object) * (Sign.sg -> object -> unit))
    33   val fix_methods: object * (object -> object) *
    34     (object * object -> object) * (Sign.sg -> object -> unit) -> unit
    35 end;
    36 
    37 signature CLASSICAL_DATA =
    38 sig
    39   val mp	: thm    	(* [| P-->Q;  P |] ==> Q *)
    40   val not_elim	: thm		(* [| ~P;  P |] ==> R *)
    41   val classical	: thm		(* (~P ==> P) ==> P *)
    42   val sizef 	: thm -> int	(* size function for BEST_FIRST *)
    43   val hyp_subst_tacs: (int -> tactic) list
    44 end;
    45 
    46 signature CLASSICAL =
    47 sig
    48   type claset
    49   val empty_cs: claset
    50   val print_cs: claset -> unit
    51   val print_claset: theory -> unit
    52   val rep_cs: (* BLAST_DATA in blast.ML dependent on this *)
    53     claset -> {safeIs: thm list, safeEs: thm list,
    54 		 hazIs: thm list, hazEs: thm list,
    55 		 swrappers: (string * wrapper) list, 
    56 		 uwrappers: (string * wrapper) list,
    57 		 safe0_netpair: netpair, safep_netpair: netpair,
    58 		 haz_netpair: netpair, dup_netpair: 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 addSaltern 	: claset * (string * (int -> tactic)) -> claset
    73   val addbefore 	: claset * (string * (int -> tactic)) -> claset
    74   val addaltern	 	: claset * (string * (int -> tactic)) -> claset
    75   val appWrappers	: claset -> wrapper
    76   val appSWrappers	: claset -> wrapper
    77 
    78   val claset_ref_of_sg: Sign.sg -> claset ref
    79   val claset_ref_of: theory -> claset ref
    80   val claset_of_sg: Sign.sg -> claset
    81   val claset_of: theory -> claset
    82   val CLASET: (claset -> tactic) -> tactic
    83   val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
    84   val claset: unit -> claset
    85   val claset_ref: unit -> claset ref
    86 
    87   val fast_tac 		: claset -> int -> tactic
    88   val slow_tac 		: claset -> int -> tactic
    89   val weight_ASTAR	: int ref
    90   val astar_tac		: claset -> int -> tactic
    91   val slow_astar_tac 	: claset -> int -> tactic
    92   val best_tac 		: claset -> int -> tactic
    93   val slow_best_tac 	: claset -> int -> tactic
    94   val depth_tac		: claset -> int -> int -> tactic
    95   val deepen_tac	: claset -> int -> int -> tactic
    96 
    97   val contr_tac 	: int -> tactic
    98   val dup_elim		: thm -> thm
    99   val dup_intr		: thm -> thm
   100   val dup_step_tac	: claset -> int -> tactic
   101   val eq_mp_tac		: int -> tactic
   102   val haz_step_tac 	: claset -> int -> tactic
   103   val joinrules 	: thm list * thm list -> (bool * thm) list
   104   val mp_tac		: int -> tactic
   105   val safe_tac 		: claset -> tactic
   106   val safe_step_tac 	: claset -> int -> tactic
   107   val clarify_tac 	: claset -> int -> tactic
   108   val clarify_step_tac 	: claset -> int -> tactic
   109   val step_tac 		: claset -> int -> tactic
   110   val slow_step_tac	: claset -> int -> tactic
   111   val swap		: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
   112   val swapify 		: thm list -> thm list
   113   val swap_res_tac 	: thm list -> int -> tactic
   114   val inst_step_tac 	: claset -> int -> tactic
   115   val inst0_step_tac 	: claset -> int -> tactic
   116   val instp_step_tac 	: claset -> int -> tactic
   117 
   118   val AddDs 		: thm list -> unit
   119   val AddEs 		: thm list -> unit
   120   val AddIs 		: thm list -> unit
   121   val AddSDs		: thm list -> unit
   122   val AddSEs		: thm list -> unit
   123   val AddSIs		: thm list -> unit
   124   val Delrules		: thm list -> unit
   125   val Safe_tac         	: tactic
   126   val Safe_step_tac	: int -> tactic
   127   val Clarify_tac 	: int -> tactic
   128   val Clarify_step_tac 	: int -> tactic
   129   val Step_tac 		: int -> tactic
   130   val Fast_tac 		: int -> tactic
   131   val Best_tac 		: int -> tactic
   132   val Slow_tac 		: int -> tactic
   133   val Slow_best_tac     : int -> tactic
   134   val Deepen_tac	: int -> int -> tactic
   135 end;
   136 
   137 
   138 structure ClasetThyData: CLASET_THY_DATA =
   139 struct
   140 
   141 (* data kind claset -- forward declaration *)
   142 
   143 val clasetK = "claset";
   144 exception ClasetData of object ref;
   145 
   146 local
   147   fun undef _ = raise Match;
   148 
   149   val empty_ref = ref ERROR;
   150   val prep_ext_fn = ref (undef: object -> object);
   151   val merge_fn = ref (undef: object * object -> object);
   152   val print_fn = ref (undef: Sign.sg -> object -> unit);
   153 
   154   val empty = ClasetData empty_ref;
   155   fun prep_ext exn = ! prep_ext_fn exn;
   156   fun merge exn = ! merge_fn exn;
   157   fun print sg exn = ! print_fn sg exn;
   158 in
   159   val thy_data = (clasetK, (empty, prep_ext, merge, print));
   160   fun fix_methods (e, ext, mrg, prt) =
   161     (empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
   162 end;
   163 
   164 
   165 end;
   166 
   167 
   168 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
   169 struct
   170 
   171 local open ClasetThyData Data in
   172 
   173 (*** Useful tactics for classical reasoning ***)
   174 
   175 val imp_elim = (*cannot use bind_thm within a structure!*)
   176   store_thm ("imp_elim", make_elim mp);
   177 
   178 (*Prove goal that assumes both P and ~P.  
   179   No backtracking if it finds an equal assumption.  Perhaps should call
   180   ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
   181 val contr_tac = eresolve_tac [not_elim]  THEN'  
   182                 (eq_assume_tac ORELSE' assume_tac);
   183 
   184 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   185   Could do the same thing for P<->Q and P... *)
   186 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
   187 
   188 (*Like mp_tac but instantiates no variables*)
   189 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
   190 
   191 val swap =
   192   store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical));
   193 
   194 (*Creates rules to eliminate ~A, from rules to introduce A*)
   195 fun swapify intrs = intrs RLN (2, [swap]);
   196 
   197 (*Uses introduction rules in the normal way, or on negated assumptions,
   198   trying rules in order. *)
   199 fun swap_res_tac rls = 
   200     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
   201     in  assume_tac 	ORELSE' 
   202 	contr_tac 	ORELSE' 
   203         biresolve_tac (foldr addrl (rls,[]))
   204     end;
   205 
   206 (*Duplication of hazardous rules, for complete provers*)
   207 fun dup_intr th = zero_var_indexes (th RS classical);
   208 
   209 fun dup_elim th = 
   210     th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd |> 
   211     rule_by_tactic (TRYALL (etac revcut_rl))
   212     handle _ => error ("Bad format for elimination rule\n" ^ string_of_thm th);
   213 
   214 
   215 (**** Classical rule sets ****)
   216 
   217 datatype claset =
   218   CS of {safeIs		: thm list,		(*safe introduction rules*)
   219 	 safeEs		: thm list,		(*safe elimination rules*)
   220 	 hazIs		: thm list,		(*unsafe introduction rules*)
   221 	 hazEs		: thm list,		(*unsafe elimination rules*)
   222 	 swrappers	: (string * wrapper) list, (*for transf. safe_step_tac*)
   223 	 uwrappers	: (string * wrapper) list, (*for transforming step_tac*)
   224 	 safe0_netpair	: netpair,		(*nets for trivial cases*)
   225 	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
   226 	 haz_netpair  	: netpair,		(*nets for unsafe rules*)
   227 	 dup_netpair	: netpair};		(*nets for duplication*)
   228 
   229 (*Desired invariants are
   230 	safe0_netpair = build safe0_brls,
   231 	safep_netpair = build safep_brls,
   232 	haz_netpair = build (joinrules(hazIs, hazEs)),
   233 	dup_netpair = build (joinrules(map dup_intr hazIs, 
   234 				       map dup_elim hazEs))}
   235 
   236 where build = build_netpair(Net.empty,Net.empty), 
   237       safe0_brls contains all brules that solve the subgoal, and
   238       safep_brls contains all brules that generate 1 or more new subgoals.
   239 The theorem lists are largely comments, though they are used in merge_cs and print_cs.
   240 Nets must be built incrementally, to save space and time.
   241 *)
   242 
   243 val empty_cs = 
   244   CS{safeIs	= [],
   245      safeEs	= [],
   246      hazIs	= [],
   247      hazEs	= [],
   248      swrappers  = [],
   249      uwrappers  = [],
   250      safe0_netpair = (Net.empty,Net.empty),
   251      safep_netpair = (Net.empty,Net.empty),
   252      haz_netpair   = (Net.empty,Net.empty),
   253      dup_netpair   = (Net.empty,Net.empty)};
   254 
   255 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   256   let val pretty_thms = map Display.pretty_thm in
   257     Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs));
   258     Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs));
   259     Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs));
   260     Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs))
   261   end;
   262 
   263 fun rep_cs (CS args) = args;
   264 
   265 local 
   266   fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac);
   267 in 
   268   fun appSWrappers (CS{swrappers,...}) = calc_wrap swrappers;
   269   fun appWrappers  (CS{uwrappers,...}) = calc_wrap uwrappers;
   270 end;
   271 
   272 
   273 (*** Adding (un)safe introduction or elimination rules.
   274 
   275     In case of overlap, new rules are tried BEFORE old ones!!
   276 ***)
   277 
   278 (*For use with biresolve_tac.  Combines intr rules with swap to handle negated
   279   assumptions.  Pairs elim rules with true. *)
   280 fun joinrules (intrs,elims) =  
   281     (map (pair true) (elims @ swapify intrs)  @
   282      map (pair false) intrs);
   283 
   284 (*Priority: prefer rules with fewest subgoals, 
   285   then rules added most recently (preferring the head of the list).*)
   286 fun tag_brls k [] = []
   287   | tag_brls k (brl::brls) =
   288       (1000000*subgoals_of_brl brl + k, brl) :: 
   289       tag_brls (k+1) brls;
   290 
   291 fun insert_tagged_list kbrls netpr = foldr insert_tagged_brl (kbrls, netpr);
   292 
   293 (*Insert into netpair that already has nI intr rules and nE elim rules.
   294   Count the intr rules double (to account for swapify).  Negate to give the
   295   new insertions the lowest priority.*)
   296 fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
   297 
   298 fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr);
   299 
   300 val delete = delete_tagged_list o joinrules;
   301 
   302 val mem_thm = gen_mem eq_thm
   303 and rem_thm = gen_rem eq_thm;
   304 
   305 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   306   is still allowed.*)
   307 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
   308        if mem_thm (th, safeIs) then 
   309 	 warning ("Rule already in claset as Safe Intr\n" ^ string_of_thm th)
   310   else if mem_thm (th, safeEs) then
   311          warning ("Rule already in claset as Safe Elim\n" ^ string_of_thm th)
   312   else if mem_thm (th, hazIs) then 
   313          warning ("Rule already in claset as unsafe Intr\n" ^ string_of_thm th)
   314   else if mem_thm (th, hazEs) then 
   315          warning ("Rule already in claset as unsafe Elim\n" ^ string_of_thm th)
   316   else ();
   317 
   318 (*** Safe rules ***)
   319 
   320 fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   321 	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   322 	   th)  =
   323   if mem_thm (th, safeIs) then 
   324 	 (warning ("Ignoring duplicate Safe Intr\n" ^ string_of_thm th);
   325 	  cs)
   326   else
   327   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   328           partition (fn rl => nprems_of rl=0) [th]
   329       val nI = length safeIs + 1
   330       and nE = length safeEs
   331   in warn_dup th cs;
   332      CS{safeIs	= th::safeIs,
   333         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   334 	safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   335 	safeEs	= safeEs,
   336 	hazIs	= hazIs,
   337 	hazEs	= hazEs,
   338 	swrappers    = swrappers,
   339 	uwrappers    = uwrappers,
   340 	haz_netpair  = haz_netpair,
   341 	dup_netpair  = dup_netpair}
   342   end;
   343 
   344 fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   345 		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   346 	   th)  =
   347   if mem_thm (th, safeEs) then 
   348 	 (warning ("Ignoring duplicate Safe Elim\n" ^ string_of_thm th);
   349 	  cs)
   350   else
   351   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   352           partition (fn rl => nprems_of rl=1) [th]
   353       val nI = length safeIs
   354       and nE = length safeEs + 1
   355   in warn_dup th cs;
   356      CS{safeEs	= th::safeEs,
   357         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   358 	safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   359 	safeIs	= safeIs,
   360 	hazIs	= hazIs,
   361 	hazEs	= hazEs,
   362 	swrappers    = swrappers,
   363 	uwrappers    = uwrappers,
   364 	haz_netpair  = haz_netpair,
   365 	dup_netpair  = dup_netpair}
   366   end;
   367 
   368 fun rev_foldl f (e, l) = foldl f (e, rev l);
   369 
   370 val op addSIs = rev_foldl addSI;
   371 val op addSEs = rev_foldl addSE;
   372 
   373 fun cs addSDs ths = cs addSEs (map make_elim ths);
   374 
   375 
   376 (*** Hazardous (unsafe) rules ***)
   377 
   378 fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   379 		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   380 	  th)=
   381   if mem_thm (th, hazIs) then 
   382 	 (warning ("Ignoring duplicate unsafe Intr\n" ^ string_of_thm th);
   383 	  cs)
   384   else
   385   let val nI = length hazIs + 1
   386       and nE = length hazEs
   387   in warn_dup th cs;
   388      CS{hazIs	= th::hazIs,
   389 	haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
   390 	dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
   391 	safeIs 	= safeIs, 
   392 	safeEs	= safeEs,
   393 	hazEs	= hazEs,
   394 	swrappers     = swrappers,
   395 	uwrappers     = uwrappers,
   396 	safe0_netpair = safe0_netpair,
   397 	safep_netpair = safep_netpair}
   398   end;
   399 
   400 fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   401 		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   402 	  th) =
   403   if mem_thm (th, hazEs) then 
   404 	 (warning ("Ignoring duplicate unsafe Elim\n" ^ string_of_thm th);
   405 	  cs)
   406   else
   407   let val nI = length hazIs 
   408       and nE = length hazEs + 1
   409   in warn_dup th cs;
   410      CS{hazEs	= th::hazEs,
   411 	haz_netpair = insert (nI,nE) ([], [th]) haz_netpair,
   412 	dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair,
   413 	safeIs	= safeIs, 
   414 	safeEs	= safeEs,
   415 	hazIs	= hazIs,
   416 	swrappers     = swrappers,
   417 	uwrappers     = uwrappers,
   418 	safe0_netpair = safe0_netpair,
   419 	safep_netpair = safep_netpair}
   420   end;
   421 
   422 val op addIs = rev_foldl addI;
   423 val op addEs = rev_foldl addE;
   424 
   425 fun cs addDs ths = cs addEs (map make_elim ths);
   426 
   427 
   428 (*** Deletion of rules 
   429      Working out what to delete, requires repeating much of the code used
   430 	to insert.
   431      Separate functions delSI, etc., are not exported; instead delrules
   432         searches in all the lists and chooses the relevant delXX functions.
   433 ***)
   434 
   435 fun delSI th 
   436           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   437 		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
   438  if mem_thm (th, safeIs) then
   439    let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
   440    in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   441 	 safep_netpair = delete (safep_rls, []) safep_netpair,
   442 	 safeIs	= rem_thm (safeIs,th),
   443 	 safeEs	= safeEs,
   444 	 hazIs	= hazIs,
   445 	 hazEs	= hazEs,
   446 	 swrappers    = swrappers,
   447 	 uwrappers    = uwrappers,
   448 	 haz_netpair  = haz_netpair,
   449 	 dup_netpair  = dup_netpair}
   450    end
   451  else cs;
   452 
   453 fun delSE th
   454           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   455 	            safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
   456  if mem_thm (th, safeEs) then
   457    let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th]
   458    in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   459 	 safep_netpair = delete ([], safep_rls) safep_netpair,
   460 	 safeIs	= safeIs,
   461 	 safeEs	= rem_thm (safeEs,th),
   462 	 hazIs	= hazIs,
   463 	 hazEs	= hazEs,
   464 	 swrappers    = swrappers,
   465 	 uwrappers    = uwrappers,
   466 	 haz_netpair  = haz_netpair,
   467 	 dup_netpair  = dup_netpair}
   468    end
   469  else cs;
   470 
   471 
   472 fun delI th
   473          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   474 	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
   475  if mem_thm (th, hazIs) then
   476      CS{haz_netpair = delete ([th], []) haz_netpair,
   477 	dup_netpair = delete ([dup_intr th], []) dup_netpair,
   478 	safeIs 	= safeIs, 
   479 	safeEs	= safeEs,
   480 	hazIs	= rem_thm (hazIs,th),
   481 	hazEs	= hazEs,
   482 	swrappers     = swrappers,
   483 	uwrappers     = uwrappers,
   484 	safe0_netpair = safe0_netpair,
   485 	safep_netpair = safep_netpair}
   486  else cs;
   487 
   488 fun delE th
   489 	 (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   490 	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
   491  if mem_thm (th, hazEs) then
   492      CS{haz_netpair = delete ([], [th]) haz_netpair,
   493 	dup_netpair = delete ([], [dup_elim th]) dup_netpair,
   494 	safeIs	= safeIs, 
   495 	safeEs	= safeEs,
   496 	hazIs	= hazIs,
   497 	hazEs	= rem_thm (hazEs,th),
   498 	swrappers     = swrappers,
   499 	uwrappers     = uwrappers,
   500 	safe0_netpair = safe0_netpair,
   501 	safep_netpair = safep_netpair}
   502  else cs;
   503 
   504 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   505 fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) =
   506        if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse
   507 	  mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) 
   508        then delSI th (delSE th (delI th (delE th cs)))
   509        else (warning ("Rule not in claset\n" ^ (string_of_thm th)); 
   510 	     cs);
   511 
   512 val op delrules = foldl delrule;
   513 
   514 
   515 (*** Setting or modifying the wrapper tacticals ***)
   516 
   517 (*Add/replace a safe wrapper*)
   518 fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   519 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   520     addSWrapper new_swrapper  =
   521   CS{safeIs	= safeIs,
   522      safeEs	= safeEs,
   523      hazIs	= hazIs,
   524      hazEs	= hazEs,
   525      swrappers 	= (case assoc_string (swrappers,(fst new_swrapper)) of None =>()
   526 	   | Some x => warning("overwriting safe wrapper "^fst new_swrapper); 
   527 		   overwrite (swrappers, new_swrapper)),
   528      uwrappers  = uwrappers,
   529      safe0_netpair = safe0_netpair,
   530      safep_netpair = safep_netpair,
   531      haz_netpair = haz_netpair,
   532      dup_netpair = dup_netpair};
   533 
   534 (*Add/replace an unsafe wrapper*)
   535 fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   536 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   537     addWrapper new_uwrapper =
   538   CS{safeIs	= safeIs,
   539      safeEs	= safeEs,
   540      hazIs	= hazIs,
   541      hazEs	= hazEs,
   542      swrappers   = swrappers,
   543      uwrappers 	= (case assoc_string (uwrappers,(fst new_uwrapper)) of None =>()
   544 	   | Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper);
   545 		   overwrite (uwrappers, new_uwrapper)),
   546      safe0_netpair = safe0_netpair,
   547      safep_netpair = safep_netpair,
   548      haz_netpair = haz_netpair,
   549      dup_netpair = dup_netpair};
   550 
   551 (*Remove a safe wrapper*)
   552 fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   553 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   554     delSWrapper name =
   555   CS{safeIs	= safeIs,
   556      safeEs	= safeEs,
   557      hazIs	= hazIs,
   558      hazEs	= hazEs,
   559      swrappers 	= (case assoc_string (swrappers, name) of None =>
   560 	   warning("safe wrapper "^ name ^" not in claset") | Some x => (); 
   561 		   filter_out (fn (n,f) => n = name) swrappers),
   562      uwrappers  = uwrappers,
   563      safe0_netpair = safe0_netpair,
   564      safep_netpair = safep_netpair,
   565      haz_netpair = haz_netpair,
   566      dup_netpair = dup_netpair};
   567 
   568 (*Remove an unsafe wrapper*)
   569 fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   570 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   571     delWrapper name =
   572   CS{safeIs	= safeIs,
   573      safeEs	= safeEs,
   574      hazIs	= hazIs,
   575      hazEs	= hazEs,
   576      swrappers  = swrappers,
   577      uwrappers 	= (case assoc_string (uwrappers, name) of None =>
   578 	   warning("unsafe wrapper "^ name ^" not in claset") | Some x => (); 
   579 		   filter_out (fn (n,f) => n = name) uwrappers),
   580      safe0_netpair = safe0_netpair,
   581      safep_netpair = safep_netpair,
   582      haz_netpair = haz_netpair,
   583      dup_netpair = dup_netpair};
   584 
   585 (*compose a safe tactic sequentially before/alternatively after safe_step_tac*)
   586 fun cs addSbefore (name,tac1) = cs addSWrapper (name, 
   587 					fn tac2 => tac1 THEN_MAYBE' tac2);
   588 fun cs addSaltern (name,tac2) = cs addSWrapper (name,
   589 					fn tac1 => tac1 ORELSE'     tac2);
   590 
   591 (*compose a tactic sequentially before/alternatively after the step tactic*)
   592 fun cs addbefore  (name,tac1) = cs addWrapper  (name,
   593 					fn tac2 => tac1 THEN_MAYBE' tac2);
   594 fun cs addaltern  (name,tac2) = cs addWrapper  (name,
   595 					fn tac1 => tac1 APPEND'     tac2);
   596 
   597 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   598   Merging the term nets may look more efficient, but the rather delicate
   599   treatment of priority might get muddled up.*)
   600 fun merge_cs
   601     (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
   602      CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) =
   603   let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
   604       val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
   605       val  hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
   606       val  hazEs' = gen_rems eq_thm ( hazEs2, hazEs)
   607   in cs addSIs safeIs'
   608         addSEs safeEs'
   609         addIs  hazIs'
   610         addEs  hazEs'
   611   end;
   612 
   613 
   614 (**** Simple tactics for theorem proving ****)
   615 
   616 (*Attack subgoals using safe inferences -- matching, not resolution*)
   617 fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
   618   appSWrappers cs (FIRST' [
   619 	eq_assume_tac,
   620 	eq_mp_tac,
   621 	bimatch_from_nets_tac safe0_netpair,
   622 	FIRST' hyp_subst_tacs,
   623 	bimatch_from_nets_tac safep_netpair]);
   624 
   625 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   626 fun safe_tac cs = REPEAT_DETERM_FIRST 
   627 	(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   628 
   629 
   630 (*** Clarify_tac: do safe steps without causing branching ***)
   631 
   632 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   633 
   634 (*version of bimatch_from_nets_tac that only applies rules that
   635   create precisely n subgoals.*)
   636 fun n_bimatch_from_nets_tac n = 
   637     biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true;
   638 
   639 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   640 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   641 
   642 (*Two-way branching is allowed only if one of the branches immediately closes*)
   643 fun bimatch2_tac netpair i =
   644     n_bimatch_from_nets_tac 2 netpair i THEN
   645     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
   646 
   647 (*Attack subgoals using safe inferences -- matching, not resolution*)
   648 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
   649   appSWrappers cs (FIRST' [
   650 	eq_assume_contr_tac,
   651 	bimatch_from_nets_tac safe0_netpair,
   652 	FIRST' hyp_subst_tacs,
   653 	n_bimatch_from_nets_tac 1 safep_netpair,
   654         bimatch2_tac safep_netpair]);
   655 
   656 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   657 
   658 
   659 (*** Unsafe steps instantiate variables or lose information ***)
   660 
   661 (*Backtracking is allowed among the various these unsafe ways of
   662   proving a subgoal.  *)
   663 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   664   assume_tac 			  APPEND' 
   665   contr_tac 			  APPEND' 
   666   biresolve_from_nets_tac safe0_netpair;
   667 
   668 (*These unsafe steps could generate more subgoals.*)
   669 fun instp_step_tac (CS{safep_netpair,...}) =
   670   biresolve_from_nets_tac safep_netpair;
   671 
   672 (*These steps could instantiate variables and are therefore unsafe.*)
   673 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   674 
   675 fun haz_step_tac (CS{haz_netpair,...}) = 
   676   biresolve_from_nets_tac haz_netpair;
   677 
   678 (*Single step for the prover.  FAILS unless it makes progress. *)
   679 fun step_tac cs i = appWrappers cs 
   680 	(K (safe_tac cs) ORELSE' (inst_step_tac cs ORELSE' haz_step_tac cs)) i;
   681 
   682 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   683   allows backtracking from "safe" rules to "unsafe" rules here.*)
   684 fun slow_step_tac cs i = appWrappers cs 
   685 	(K (safe_tac cs) ORELSE' (inst_step_tac cs APPEND' haz_step_tac cs)) i;
   686 
   687 (**** The following tactics all fail unless they solve one goal ****)
   688 
   689 (*Dumb but fast*)
   690 fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   691 
   692 (*Slower but smarter than fast_tac*)
   693 fun best_tac cs = 
   694   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   695 
   696 fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   697 
   698 fun slow_best_tac cs = 
   699   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   700 
   701 
   702 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
   703 val weight_ASTAR = ref 5; 
   704 
   705 fun astar_tac cs = 
   706   SELECT_GOAL ( ASTAR (has_fewer_prems 1
   707 	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   708 	      (step_tac cs 1));
   709 
   710 fun slow_astar_tac cs = 
   711   SELECT_GOAL ( ASTAR (has_fewer_prems 1
   712 	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   713 	      (slow_step_tac cs 1));
   714 
   715 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   716   of much experimentation!  Changing APPEND to ORELSE below would prove
   717   easy theorems faster, but loses completeness -- and many of the harder
   718   theorems such as 43. ****)
   719 
   720 (*Non-deterministic!  Could always expand the first unsafe connective.
   721   That's hard to implement and did not perform better in experiments, due to
   722   greater search depth required.*)
   723 fun dup_step_tac (cs as (CS{dup_netpair,...})) = 
   724   biresolve_from_nets_tac dup_netpair;
   725 
   726 (*Searching to depth m.*)
   727 fun depth_tac cs m i state = 
   728   SELECT_GOAL 
   729    (appWrappers cs
   730     (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
   731 			     (safe_step_tac cs i)) THEN_ELSE
   732      (DEPTH_SOLVE (depth_tac cs m i),
   733       inst0_step_tac cs i  APPEND
   734       COND (K(m=0)) no_tac
   735         ((instp_step_tac cs i APPEND dup_step_tac cs i)
   736 	 THEN DEPTH_SOLVE (depth_tac cs (m-1) i)))) 1)
   737   i state;
   738 
   739 (*Search, with depth bound m.  
   740   This is the "entry point", which does safe inferences first.*)
   741 fun safe_depth_tac cs m = 
   742   SUBGOAL 
   743     (fn (prem,i) =>
   744       let val deti =
   745 	  (*No Vars in the goal?  No need to backtrack between goals.*)
   746 	  case term_vars prem of
   747 	      []	=> DETERM 
   748 	    | _::_	=> I
   749       in  SELECT_GOAL (TRY (safe_tac cs) THEN 
   750 		       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   751       end);
   752 
   753 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   754 
   755 
   756 
   757 (** claset theory data **)
   758 
   759 (* init data kind claset *)
   760 
   761 exception CSData of claset ref;
   762 
   763 local
   764   val empty = CSData (ref empty_cs);
   765 
   766   (*create new references*)
   767   fun prep_ext (ClasetData (ref (CSData (ref cs)))) =
   768     ClasetData (ref (CSData (ref cs)));
   769 
   770   fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) =
   771     ClasetData (ref (CSData (ref (merge_cs (cs1, cs2)))));
   772 
   773   fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs;
   774 in
   775   val _ = fix_methods (empty, prep_ext, merge, print);
   776 end;
   777 
   778 
   779 (* access claset *)
   780 
   781 fun print_claset thy = Display.print_data thy clasetK;
   782 
   783 fun claset_ref_of_sg sg =
   784   (case Sign.get_data sg clasetK of
   785     ClasetData (ref (CSData r)) => r
   786   | _ => sys_error "claset_ref_of_sg");
   787 
   788 val claset_ref_of = claset_ref_of_sg o sign_of;
   789 val claset_of_sg = ! o claset_ref_of_sg;
   790 val claset_of = claset_of_sg o sign_of;
   791 
   792 fun CLASET tacf state = tacf (claset_of_sg (sign_of_thm state)) state;
   793 fun CLASET' tacf i state = tacf (claset_of_sg (sign_of_thm state)) i state;
   794 
   795 val claset = claset_of o Context.get_context;
   796 val claset_ref = claset_ref_of_sg o sign_of o Context.get_context;
   797 
   798 
   799 (* change claset *)
   800 
   801 fun change_claset f x = claset_ref () := (f (claset (), x));
   802 
   803 val AddDs = change_claset (op addDs);
   804 val AddEs = change_claset (op addEs);
   805 val AddIs = change_claset (op addIs);
   806 val AddSDs = change_claset (op addSDs);
   807 val AddSEs = change_claset (op addSEs);
   808 val AddSIs = change_claset (op addSIs);
   809 val Delrules = change_claset (op delrules);
   810 
   811 
   812 (* tactics referring to the implicit claset *)
   813 
   814 (*the abstraction over the proof state delays the dereferencing*)
   815 fun Safe_tac st		  = safe_tac (claset()) st;
   816 fun Safe_step_tac i st	  = safe_step_tac (claset()) i st;
   817 fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
   818 fun Clarify_tac i st	  = clarify_tac (claset()) i st;
   819 fun Step_tac i st	  = step_tac (claset()) i st;
   820 fun Fast_tac i st	  = fast_tac (claset()) i st;
   821 fun Best_tac i st	  = best_tac (claset()) i st;
   822 fun Slow_tac i st	  = slow_tac (claset()) i st;
   823 fun Slow_best_tac i st	  = slow_best_tac (claset()) i st;
   824 fun Deepen_tac m	  = deepen_tac (claset()) m;
   825 
   826 
   827 end; 
   828 end;