src/Provers/classical.ML
author wenzelm
Tue Jul 25 00:13:49 2000 +0200 (2000-07-25 ago)
changeset 9441 e729ea747250
parent 9408 d3d56e1d2ec1
child 9449 2f814053a6cc
permissions -rw-r--r--
added clarify method;
removed unofficial improper methods;
     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 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 Intr\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 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 Intr\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 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 Intr\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 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     (case assoc_string (swrappers,(fst new_swrapper)) of None =>()
   687 	   | Some x => warning("overwriting safe wrapper "^fst new_swrapper); 
   688 		   overwrite (swrappers, new_swrapper)));
   689 
   690 (*Add/replace an unsafe wrapper*)
   691 fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
   692     (case assoc_string (uwrappers,(fst new_uwrapper)) of None =>()
   693 	   | Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper);
   694 		   overwrite (uwrappers, new_uwrapper)));
   695 
   696 (*Remove a safe wrapper*)
   697 fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
   698     let val (del,rest) = partition (fn (n,_) => n=name) swrappers
   699     in if null del then (warning ("No such safe wrapper in claset: "^ name); 
   700 			 swrappers) else rest end);
   701 
   702 (*Remove an unsafe wrapper*)
   703 fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
   704     let val (del,rest) = partition (fn (n,_) => n=name) uwrappers
   705     in if null del then (warning ("No such unsafe wrapper in claset: " ^ name);
   706                          uwrappers) else rest end);
   707 
   708 (*compose a safe tactic sequentially before/alternatively after safe_step_tac*)
   709 fun cs addSbefore  (name,    tac1) = 
   710     cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   711 fun cs addSaltern  (name,    tac2) = 
   712     cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   713 
   714 (*compose a tactic sequentially before/alternatively after the step tactic*)
   715 fun cs addbefore   (name,    tac1) = 
   716     cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
   717 fun cs addaltern   (name,    tac2) =
   718     cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
   719 
   720 fun cs addD2     (name, thm) = 
   721     cs addaltern (name, dtac thm THEN' atac);
   722 fun cs addE2     (name, thm) = 
   723     cs addaltern (name, etac thm THEN' atac);
   724 fun cs addSD2     (name, thm) = 
   725     cs addSaltern (name, dmatch_tac [thm] THEN' eq_assume_tac);
   726 fun cs addSE2     (name, thm) = 
   727     cs addSaltern (name, ematch_tac [thm] THEN' eq_assume_tac);
   728 
   729 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   730   Merging the term nets may look more efficient, but the rather delicate
   731   treatment of priority might get muddled up.*)
   732 fun merge_cs
   733     (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...},
   734      CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,
   735         xtraIs=xtraIs2, xtraEs=xtraEs2,	swrappers, uwrappers, ...}) =
   736   let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
   737       val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
   738       val  hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
   739       val  hazEs' = gen_rems eq_thm ( hazEs2, hazEs)
   740       val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs)
   741       val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs)
   742       val cs1   = cs addSIs safeIs'
   743 		     addSEs safeEs'
   744 		     addIs  hazIs'
   745 		     addEs  hazEs'
   746 		     addXIs xtraIs'
   747 		     addXEs xtraEs'
   748       val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers);
   749       val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers);
   750   in cs3 
   751   end;
   752 
   753 
   754 (**** Simple tactics for theorem proving ****)
   755 
   756 (*Attack subgoals using safe inferences -- matching, not resolution*)
   757 fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
   758   appSWrappers cs (FIRST' [
   759 	eq_assume_tac,
   760 	eq_mp_tac,
   761 	bimatch_from_nets_tac safe0_netpair,
   762 	FIRST' hyp_subst_tacs,
   763 	bimatch_from_nets_tac safep_netpair]);
   764 
   765 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   766 fun safe_steps_tac cs = REPEAT_DETERM1 o 
   767 	(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   768 
   769 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   770 fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   771 
   772 
   773 (*** Clarify_tac: do safe steps without causing branching ***)
   774 
   775 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   776 
   777 (*version of bimatch_from_nets_tac that only applies rules that
   778   create precisely n subgoals.*)
   779 fun n_bimatch_from_nets_tac n = 
   780     biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true;
   781 
   782 fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   783 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   784 
   785 (*Two-way branching is allowed only if one of the branches immediately closes*)
   786 fun bimatch2_tac netpair i =
   787     n_bimatch_from_nets_tac 2 netpair i THEN
   788     (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
   789 
   790 (*Attack subgoals using safe inferences -- matching, not resolution*)
   791 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
   792   appSWrappers cs (FIRST' [
   793 	eq_assume_contr_tac,
   794 	bimatch_from_nets_tac safe0_netpair,
   795 	FIRST' hyp_subst_tacs,
   796 	n_bimatch_from_nets_tac 1 safep_netpair,
   797         bimatch2_tac safep_netpair]);
   798 
   799 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   800 
   801 
   802 (*** Unsafe steps instantiate variables or lose information ***)
   803 
   804 (*Backtracking is allowed among the various these unsafe ways of
   805   proving a subgoal.  *)
   806 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   807   assume_tac 			  APPEND' 
   808   contr_tac 			  APPEND' 
   809   biresolve_from_nets_tac safe0_netpair;
   810 
   811 (*These unsafe steps could generate more subgoals.*)
   812 fun instp_step_tac (CS{safep_netpair,...}) =
   813   biresolve_from_nets_tac safep_netpair;
   814 
   815 (*These steps could instantiate variables and are therefore unsafe.*)
   816 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   817 
   818 fun haz_step_tac (CS{haz_netpair,...}) = 
   819   biresolve_from_nets_tac haz_netpair;
   820 
   821 (*Single step for the prover.  FAILS unless it makes progress. *)
   822 fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
   823 	(inst_step_tac cs ORELSE' haz_step_tac cs) i;
   824 
   825 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   826   allows backtracking from "safe" rules to "unsafe" rules here.*)
   827 fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
   828 	(inst_step_tac cs APPEND' haz_step_tac cs) i;
   829 
   830 (**** The following tactics all fail unless they solve one goal ****)
   831 
   832 (*Dumb but fast*)
   833 fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   834 
   835 (*Slower but smarter than fast_tac*)
   836 fun best_tac cs = 
   837   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   838 
   839 (*even a bit smarter than best_tac*)
   840 fun first_best_tac cs = 
   841   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   842 
   843 fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   844 
   845 fun slow_best_tac cs = 
   846   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   847 
   848 
   849 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
   850 val weight_ASTAR = ref 5; 
   851 
   852 fun astar_tac cs = 
   853   SELECT_GOAL ( ASTAR (has_fewer_prems 1
   854 	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   855 	      (step_tac cs 1));
   856 
   857 fun slow_astar_tac cs = 
   858   SELECT_GOAL ( ASTAR (has_fewer_prems 1
   859 	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   860 	      (slow_step_tac cs 1));
   861 
   862 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   863   of much experimentation!  Changing APPEND to ORELSE below would prove
   864   easy theorems faster, but loses completeness -- and many of the harder
   865   theorems such as 43. ****)
   866 
   867 (*Non-deterministic!  Could always expand the first unsafe connective.
   868   That's hard to implement and did not perform better in experiments, due to
   869   greater search depth required.*)
   870 fun dup_step_tac (cs as (CS{dup_netpair,...})) = 
   871   biresolve_from_nets_tac dup_netpair;
   872 
   873 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   874 local
   875 fun slow_step_tac' cs = appWrappers cs 
   876 	(instp_step_tac cs APPEND' dup_step_tac cs);
   877 in fun depth_tac cs m i state = SELECT_GOAL 
   878    (safe_steps_tac cs 1 THEN_ELSE 
   879 	(DEPTH_SOLVE (depth_tac cs m 1),
   880 	 inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   881 		(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   882         )) i state;
   883 end;
   884 
   885 (*Search, with depth bound m.  
   886   This is the "entry point", which does safe inferences first.*)
   887 fun safe_depth_tac cs m = 
   888   SUBGOAL 
   889     (fn (prem,i) =>
   890       let val deti =
   891 	  (*No Vars in the goal?  No need to backtrack between goals.*)
   892 	  case term_vars prem of
   893 	      []	=> DETERM 
   894 	    | _::_	=> I
   895       in  SELECT_GOAL (TRY (safe_tac cs) THEN 
   896 		       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   897       end);
   898 
   899 fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   900 
   901 
   902 
   903 (** claset theory data **)
   904 
   905 (* theory data kind 'Provers/claset' *)
   906 
   907 structure GlobalClasetArgs =
   908 struct
   909   val name = "Provers/claset";
   910   type T = claset ref;
   911 
   912   val empty = ref empty_cs;
   913   fun copy (ref cs) = (ref cs): T;            (*create new reference!*)
   914   val prep_ext = copy;
   915   fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2));
   916   fun print _ (ref cs) = print_cs cs;
   917 end;
   918 
   919 structure GlobalClaset = TheoryDataFun(GlobalClasetArgs);
   920 val print_claset = GlobalClaset.print;
   921 val claset_ref_of_sg = GlobalClaset.get_sg;
   922 val claset_ref_of = GlobalClaset.get;
   923 
   924 
   925 (* access claset *)
   926 
   927 val claset_of_sg = ! o claset_ref_of_sg;
   928 val claset_of = claset_of_sg o Theory.sign_of;
   929 
   930 fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state;
   931 fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state;
   932 
   933 val claset = claset_of o Context.the_context;
   934 val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context;
   935 
   936 
   937 (* change claset *)
   938 
   939 fun change_claset f x = claset_ref () := (f (claset (), x));
   940 
   941 val AddDs = change_claset (op addDs);
   942 val AddEs = change_claset (op addEs);
   943 val AddIs = change_claset (op addIs);
   944 val AddSDs = change_claset (op addSDs);
   945 val AddSEs = change_claset (op addSEs);
   946 val AddSIs = change_claset (op addSIs);
   947 val AddXDs = change_claset (op addXDs);
   948 val AddXEs = change_claset (op addXEs);
   949 val AddXIs = change_claset (op addXIs);
   950 val Delrules = change_claset (op delrules);
   951 
   952 
   953 (* proof data kind 'Provers/claset' *)
   954 
   955 structure LocalClasetArgs =
   956 struct
   957   val name = "Provers/claset";
   958   type T = claset;
   959   val init = claset_of;
   960   fun print _ cs = print_cs cs;
   961 end;
   962 
   963 structure LocalClaset = ProofDataFun(LocalClasetArgs);
   964 val print_local_claset = LocalClaset.print;
   965 val get_local_claset = LocalClaset.get;
   966 val put_local_claset = LocalClaset.put;
   967 
   968 
   969 (* attributes *)
   970 
   971 fun change_global_cs f (thy, th) =
   972   let val r = claset_ref_of thy
   973   in r := f (! r, [th]); (thy, th) end;
   974 
   975 fun change_local_cs f (ctxt, th) =
   976   let val cs = f (get_local_claset ctxt, [th])
   977   in (put_local_claset cs ctxt, th) end;
   978 
   979 val safe_dest_global = change_global_cs (op addSDs);
   980 val safe_elim_global = change_global_cs (op addSEs);
   981 val safe_intro_global = change_global_cs (op addSIs);
   982 val haz_dest_global = change_global_cs (op addDs);
   983 val haz_elim_global = change_global_cs (op addEs);
   984 val haz_intro_global = change_global_cs (op addIs);
   985 val xtra_dest_global = change_global_cs (op addXDs);
   986 val xtra_elim_global = change_global_cs (op addXEs);
   987 val xtra_intro_global = change_global_cs (op addXIs);
   988 val delrule_global = change_global_cs (op delrules);
   989 
   990 val safe_dest_local = change_local_cs (op addSDs);
   991 val safe_elim_local = change_local_cs (op addSEs);
   992 val safe_intro_local = change_local_cs (op addSIs);
   993 val haz_dest_local = change_local_cs (op addDs);
   994 val haz_elim_local = change_local_cs (op addEs);
   995 val haz_intro_local = change_local_cs (op addIs);
   996 val xtra_dest_local = change_local_cs (op addXDs);
   997 val xtra_elim_local = change_local_cs (op addXEs);
   998 val xtra_intro_local = change_local_cs (op addXIs);
   999 val delrule_local = change_local_cs (op delrules);
  1000 
  1001 
  1002 (* tactics referring to the implicit claset *)
  1003 
  1004 (*the abstraction over the proof state delays the dereferencing*)
  1005 fun Safe_tac st		  = safe_tac (claset()) st;
  1006 fun Safe_step_tac i st	  = safe_step_tac (claset()) i st;
  1007 fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
  1008 fun Clarify_tac i st	  = clarify_tac (claset()) i st;
  1009 fun Step_tac i st	  = step_tac (claset()) i st;
  1010 fun Fast_tac i st	  = fast_tac (claset()) i st;
  1011 fun Best_tac i st	  = best_tac (claset()) i st;
  1012 fun Slow_tac i st	  = slow_tac (claset()) i st;
  1013 fun Slow_best_tac i st	  = slow_best_tac (claset()) i st;
  1014 fun Deepen_tac m	  = deepen_tac (claset()) m;
  1015 
  1016 
  1017 end; 
  1018 
  1019 
  1020 
  1021 (** concrete syntax of attributes **)
  1022 
  1023 (* add / del rules *)
  1024 
  1025 val introN = "intro";
  1026 val elimN = "elim";
  1027 val destN = "dest";
  1028 val delN = "del";
  1029 val delruleN = "delrule";
  1030 
  1031 val colon = Args.$$$ ":";
  1032 val query = Args.$$$ "?";
  1033 val bang = Args.$$$ "!";
  1034 val query_colon = Args.$$$ "?:";
  1035 val bang_colon = Args.$$$ "!:";
  1036 
  1037 fun cla_att change xtra haz safe = Attrib.syntax
  1038   (Scan.lift ((query >> K xtra || bang >> K haz || Scan.succeed safe) >> change));
  1039 
  1040 fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
  1041 val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local);
  1042 
  1043 
  1044 (* setup_attrs *)
  1045 
  1046 fun elimify x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
  1047 
  1048 val setup_attrs = Attrib.add_attributes
  1049  [("elimify", (elimify, elimify), "turn destruct rule into elimination rule (classical)"),
  1050   (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declare destruction rule"),
  1051   (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declare elimination rule"),
  1052   (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declare introduction rule"),
  1053   (delruleN, del_attr, "undeclare rule")];
  1054 
  1055 
  1056 
  1057 (** proof methods **)
  1058 
  1059 (* get nets (appropriate order for semi-automatic methods) *)
  1060 
  1061 local
  1062   val imp_elim_netpair = insert (0, 0) ([], [imp_elim]) empty_netpair;
  1063   val not_elim_netpair = insert (0, 0) ([], [Data.not_elim]) empty_netpair;
  1064 in
  1065   fun get_nets (CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair, ...}) =
  1066     [imp_elim_netpair, safe0_netpair, safep_netpair, not_elim_netpair, haz_netpair, dup_netpair, xtra_netpair];
  1067 end;
  1068 
  1069 
  1070 (* METHOD_CLASET' *)
  1071 
  1072 fun METHOD_CLASET' tac ctxt =
  1073   Method.METHOD (HEADGOAL o tac (get_local_claset ctxt));
  1074 
  1075 
  1076 val trace_rules = ref false;
  1077 
  1078 local
  1079 
  1080 fun trace rules i =
  1081   if not (! trace_rules) then ()
  1082   else Pretty.writeln (Pretty.big_list ("trying standard rule(s) on goal #" ^ string_of_int i ^ ":")
  1083     (map Display.pretty_thm rules));
  1084 
  1085 
  1086 fun order_rules xs = map snd (Tactic.orderlist xs);
  1087 
  1088 fun find_rules concl nets =
  1089   let fun rules_of (inet, _) = order_rules (Net.unify_term inet concl)
  1090   in flat (map rules_of nets) end;
  1091 
  1092 fun find_erules [] _ = []
  1093   | find_erules (fact :: _) nets =
  1094       let
  1095         fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm;
  1096         fun erules_of (_, enet) = order_rules (may_unify enet fact);
  1097       in flat (map erules_of nets) end;
  1098 
  1099 
  1100 fun some_rule_tac cs facts =
  1101   let
  1102     val nets = get_nets cs;
  1103     val erules = find_erules facts nets;
  1104 
  1105     val tac = SUBGOAL (fn (goal, i) =>
  1106       let
  1107         val irules = find_rules (Logic.strip_assums_concl goal) nets;
  1108         val rules = erules @ irules;
  1109         val ruleq = Method.multi_resolves facts rules;
  1110       in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end);
  1111   in tac end;
  1112 
  1113 fun rule_tac [] cs facts = some_rule_tac cs facts
  1114   | rule_tac rules _ facts = Method.rule_tac rules facts;
  1115 
  1116 in
  1117   val rule = METHOD_CLASET' o rule_tac;
  1118 end;
  1119 
  1120 
  1121 (* intro / elim methods *)
  1122 
  1123 local
  1124 
  1125 fun intro_elim_tac netpair_of res_tac rules cs facts =
  1126   let
  1127     val tac =
  1128       if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))
  1129       else res_tac rules;
  1130   in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end;
  1131 
  1132 val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) Tactic.match_tac;
  1133 val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) Tactic.ematch_tac;
  1134 
  1135 in
  1136   val intro = METHOD_CLASET' o intro_tac;
  1137   val elim = METHOD_CLASET' o elim_tac;
  1138 end;
  1139 
  1140 
  1141 (* contradiction method *)
  1142 
  1143 val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
  1144 
  1145 
  1146 (* automatic methods *)
  1147 
  1148 val cla_modifiers =
  1149  [Args.$$$ destN -- query_colon >> K ((I, xtra_dest_local):Method.modifier),
  1150   Args.$$$ destN -- bang_colon >> K (I, haz_dest_local),
  1151   Args.$$$ destN -- colon >> K (I, safe_dest_local),
  1152   Args.$$$ elimN -- query_colon >> K (I, xtra_elim_local),
  1153   Args.$$$ elimN -- bang_colon >> K (I, haz_elim_local),
  1154   Args.$$$ elimN -- colon >> K (I, safe_elim_local),
  1155   Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
  1156   Args.$$$ introN -- bang_colon >> K (I, haz_intro_local),
  1157   Args.$$$ introN -- colon >> K (I, safe_intro_local),
  1158   Args.$$$ delN -- colon >> K (I, delrule_local)];
  1159 
  1160 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
  1161   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
  1162 
  1163 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
  1164   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
  1165 
  1166 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
  1167 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
  1168 
  1169 
  1170 
  1171 (** setup_methods **)
  1172 
  1173 val setup_methods = Method.add_methods
  1174  [("default", Method.thms_ctxt_args rule, "apply some rule (classical)"),
  1175   ("rule", Method.thms_ctxt_args rule, "apply some rule (classical)"),
  1176   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
  1177   ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
  1178   ("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
  1179   ("clarify", cla_method' clarify_tac, "repeatedly apply safe steps"),
  1180   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
  1181   ("best", cla_method' best_tac, "classical prover (best-first)")];
  1182 
  1183 
  1184 
  1185 (** theory setup **)
  1186 
  1187 val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
  1188 
  1189 
  1190 
  1191 (** outer syntax **)
  1192 
  1193 val print_clasetP =
  1194   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
  1195     OuterSyntax.Keyword.diag
  1196     (Scan.succeed (Toplevel.no_timing o (Toplevel.keep
  1197       (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))));
  1198 
  1199 val _ = OuterSyntax.add_parsers [print_clasetP];
  1200 
  1201 
  1202 end;