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