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