src/HOL/Tools/meson.ML
author haftmann
Tue May 09 10:09:37 2006 +0200 (2006-05-09)
changeset 19599 a5c7eb37d14f
parent 19204 b8f7de7ef629
child 19728 6c47d9295dca
permissions -rw-r--r--
added DatatypeHooks
     1 (*  Title:      HOL/Tools/meson.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 The MESON resolution proof procedure for HOL.
     7 
     8 When making clauses, avoids using the rewriter -- instead uses RS recursively
     9 
    10 NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E.  ELIMINATES NEED FOR
    11 FUNCTION nodups -- if done to goal clauses too!
    12 *)
    13 
    14 signature BASIC_MESON =
    15 sig
    16   val size_of_subgoals	: thm -> int
    17   val make_cnf		: thm list -> thm -> thm list
    18   val make_nnf		: thm -> thm
    19   val make_nnf1		: thm -> thm
    20   val skolemize		: thm -> thm
    21   val make_clauses	: thm list -> thm list
    22   val make_horns	: thm list -> thm list
    23   val best_prolog_tac	: (thm -> int) -> thm list -> tactic
    24   val depth_prolog_tac	: thm list -> tactic
    25   val gocls		: thm list -> thm list
    26   val skolemize_prems_tac	: thm list -> int -> tactic
    27   val MESON		: (thm list -> tactic) -> int -> tactic
    28   val best_meson_tac	: (thm -> int) -> int -> tactic
    29   val safe_best_meson_tac	: int -> tactic
    30   val depth_meson_tac	: int -> tactic
    31   val prolog_step_tac'	: thm list -> int -> tactic
    32   val iter_deepen_prolog_tac	: thm list -> tactic
    33   val iter_deepen_meson_tac	: thm list -> int -> tactic
    34   val meson_tac		: int -> tactic
    35   val negate_head	: thm -> thm
    36   val select_literal	: int -> thm -> thm
    37   val skolemize_tac	: int -> tactic
    38   val make_clauses_tac	: int -> tactic
    39   val check_is_fol_term : term -> term
    40 end
    41 
    42 
    43 structure Meson =
    44 struct
    45 
    46 val not_conjD = thm "meson_not_conjD";
    47 val not_disjD = thm "meson_not_disjD";
    48 val not_notD = thm "meson_not_notD";
    49 val not_allD = thm "meson_not_allD";
    50 val not_exD = thm "meson_not_exD";
    51 val imp_to_disjD = thm "meson_imp_to_disjD";
    52 val not_impD = thm "meson_not_impD";
    53 val iff_to_disjD = thm "meson_iff_to_disjD";
    54 val not_iffD = thm "meson_not_iffD";
    55 val conj_exD1 = thm "meson_conj_exD1";
    56 val conj_exD2 = thm "meson_conj_exD2";
    57 val disj_exD = thm "meson_disj_exD";
    58 val disj_exD1 = thm "meson_disj_exD1";
    59 val disj_exD2 = thm "meson_disj_exD2";
    60 val disj_assoc = thm "meson_disj_assoc";
    61 val disj_comm = thm "meson_disj_comm";
    62 val disj_FalseD1 = thm "meson_disj_FalseD1";
    63 val disj_FalseD2 = thm "meson_disj_FalseD2";
    64 
    65 val depth_limit = ref 2000;
    66 
    67 (**** Operators for forward proof ****)
    68 
    69 (*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*)
    70 fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb);
    71 
    72 (*raises exception if no rules apply -- unlike RL*)
    73 fun tryres (th, rls) = 
    74   let fun tryall [] = raise THM("tryres", 0, th::rls)
    75         | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls)
    76   in  tryall rls  end;
    77   
    78 (*Permits forward proof from rules that discharge assumptions*)
    79 fun forward_res nf st =
    80   case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
    81   of SOME(th,_) => th
    82    | NONE => raise THM("forward_res", 0, [st]);
    83 
    84 
    85 (*Are any of the constants in "bs" present in the term?*)
    86 fun has_consts bs =
    87   let fun has (Const(a,_)) = a mem bs
    88 	| has (Const ("Hilbert_Choice.Eps",_) $ _) = false
    89 		     (*ignore constants within @-terms*)
    90 	| has (f$u) = has f orelse has u
    91 	| has (Abs(_,_,t)) = has t
    92 	| has _ = false
    93   in  has  end;
    94   
    95 
    96 (**** Clause handling ****)
    97 
    98 fun literals (Const("Trueprop",_) $ P) = literals P
    99   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
   100   | literals (Const("Not",_) $ P) = [(false,P)]
   101   | literals P = [(true,P)];
   102 
   103 (*number of literals in a term*)
   104 val nliterals = length o literals;
   105 
   106 
   107 (*** Tautology Checking ***)
   108 
   109 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) = 
   110       signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
   111   | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
   112   | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
   113   
   114 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
   115 
   116 (*Literals like X=X are tautologous*)
   117 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
   118   | taut_poslit (Const("True",_)) = true
   119   | taut_poslit _ = false;
   120 
   121 fun is_taut th =
   122   let val (poslits,neglits) = signed_lits th
   123   in  exists taut_poslit poslits
   124       orelse
   125       exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits)
   126   end;
   127 
   128 
   129 (*** To remove trivial negated equality literals from clauses ***)
   130 
   131 (*They are typically functional reflexivity axioms and are the converses of
   132   injectivity equivalences*)
   133   
   134 val not_refl_disj_D = thm"meson_not_refl_disj_D";
   135 
   136 fun refl_clause_aux 0 th = th
   137   | refl_clause_aux n th =
   138        case HOLogic.dest_Trueprop (concl_of th) of
   139 	  (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => 
   140             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
   141 	| (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => 
   142 	    if is_Var t orelse is_Var u then (*Var inequation: delete or ignore*)
   143 		(refl_clause_aux (n-1) (th RS not_refl_disj_D)    (*delete*)
   144 		 handle THM _ => refl_clause_aux (n-1) (th RS disj_comm))  (*ignore*)
   145 	    else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
   146 	| (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
   147 	| _ => (*not a disjunction*) th;
   148 
   149 fun notequal_lits_count (Const ("op |", _) $ P $ Q) = 
   150       notequal_lits_count P + notequal_lits_count Q
   151   | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
   152   | notequal_lits_count _ = 0;
   153 
   154 (*Simplify a clause by applying reflexivity to its negated equality literals*)
   155 fun refl_clause th = 
   156   let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
   157   in  zero_var_indexes (refl_clause_aux neqs th)  end;
   158 
   159 
   160 (*** The basic CNF transformation ***)
   161 
   162 (*Generation of unique names -- maxidx cannot be relied upon to increase!
   163   Cannot rely on "variant", since variables might coincide when literals
   164   are joined to make a clause...
   165   19 chooses "U" as the first variable name*)
   166 val name_ref = ref 19;
   167 
   168 (*Replaces universally quantified variables by FREE variables -- because
   169   assumptions may not contain scheme variables.  Later, call "generalize". *)
   170 fun freeze_spec th =
   171   let val names = add_term_names (prop_of th, [])
   172       val newname = (name_ref := !name_ref + 1;
   173 		     variant names (radixstring(26, "A", !name_ref)))
   174       val spec' = read_instantiate [("x", newname)] spec
   175   in  th RS spec'  end;
   176 
   177 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
   178   and then normalized via function nf. The normal form is given to resolve_tac,
   179   presumably to instantiate a Boolean variable.*)
   180 fun resop nf [prem] = resolve_tac (nf prem) 1;
   181 
   182 val has_meta_conn = 
   183     exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
   184   
   185 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
   186   Strips universal quantifiers and breaks up conjunctions.
   187   Eliminates existential quantifiers using skoths: Skolemization theorems.*)
   188 fun cnf skoths (th,ths) =
   189   let fun cnf_aux (th,ths) =
   190         if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
   191         else if not (has_consts ["All","Ex","op &"] (prop_of th))  
   192 	then th::ths (*no work to do, terminate*)
   193 	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   194 	    Const ("op &", _) => (*conjunction*)
   195 		cnf_aux (th RS conjunct1,
   196 			      cnf_aux (th RS conjunct2, ths))
   197 	  | Const ("All", _) => (*universal quantifier*)
   198 	        cnf_aux (freeze_spec th,  ths)
   199 	  | Const ("Ex", _) => 
   200 	      (*existential quantifier: Insert Skolem functions*)
   201 	      cnf_aux (tryres (th,skoths), ths)
   202 	  | Const ("op |", _) => (*disjunction*)
   203 	      let val tac =
   204 		  (METAHYPS (resop cnf_nil) 1) THEN
   205 		   (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
   206 	      in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
   207 	  | _ => (*no work to do*) th::ths 
   208       and cnf_nil th = cnf_aux (th,[])
   209   in 
   210     name_ref := 19;  (*It's safe to reset this in a top-level call to cnf*)
   211     cnf_aux (th,ths)
   212   end;
   213 
   214 (*Convert all suitable free variables to schematic variables, 
   215   but don't discharge assumptions.*)
   216 fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
   217 
   218 fun make_cnf skoths th = 
   219   filter (not o is_taut) 
   220     (map (refl_clause o generalize) (cnf skoths (th, [])));
   221 
   222 
   223 (**** Removal of duplicate literals ****)
   224 
   225 (*Forward proof, passing extra assumptions as theorems to the tactic*)
   226 fun forward_res2 nf hyps st =
   227   case Seq.pull
   228 	(REPEAT
   229 	 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   230 	 st)
   231   of SOME(th,_) => th
   232    | NONE => raise THM("forward_res2", 0, [st]);
   233 
   234 (*Remove duplicates in P|Q by assuming ~P in Q
   235   rls (initially []) accumulates assumptions of the form P==>False*)
   236 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
   237     handle THM _ => tryres(th,rls)
   238     handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
   239 			   [disj_FalseD1, disj_FalseD2, asm_rl])
   240     handle THM _ => th;
   241 
   242 (*Remove duplicate literals, if there are any*)
   243 fun nodups th =
   244     if null(findrep(literals(prop_of th))) then th
   245     else nodups_aux [] th;
   246 
   247 
   248 (**** Generation of contrapositives ****)
   249 
   250 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   251 fun assoc_right th = assoc_right (th RS disj_assoc)
   252 	handle THM _ => th;
   253 
   254 (*Must check for negative literal first!*)
   255 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
   256 
   257 (*For ordinary resolution. *)
   258 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
   259 
   260 (*Create a goal or support clause, conclusing False*)
   261 fun make_goal th =   (*Must check for negative literal first!*)
   262     make_goal (tryres(th, clause_rules))
   263   handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
   264 
   265 (*Sort clauses by number of literals*)
   266 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
   267 
   268 fun sort_clauses ths = sort (make_ord fewerlits) ths;
   269 
   270 (*True if the given type contains bool anywhere*)
   271 fun has_bool (Type("bool",_)) = true
   272   | has_bool (Type(_, Ts)) = exists has_bool Ts
   273   | has_bool _ = false;
   274   
   275 (*Is the string the name of a connective? It doesn't matter if this list is
   276   incomplete, since when actually called, the only connectives likely to
   277   remain are & | Not.*)  
   278 fun is_conn c = c mem_string
   279     ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", 
   280      "All", "Ex", "Ball", "Bex"];
   281 
   282 (*True if the term contains a function where the type of any argument contains
   283   bool.*)
   284 val has_bool_arg_const = 
   285     exists_Const
   286       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
   287       
   288 (*Raises an exception if any Vars in the theorem mention type bool; they
   289   could cause make_horn to loop! Also rejects functions whose arguments are 
   290   Booleans or other functions.*)
   291 fun is_fol_term t =
   292     not (exists (has_bool o fastype_of) (term_vars t)  orelse
   293 	 not (Term.is_first_order ["all","All","Ex"] t) orelse
   294 	 has_bool_arg_const t  orelse  
   295 	 has_meta_conn t);
   296 
   297 (*FIXME: replace this by the boolean-valued version above!*)
   298 fun check_is_fol_term t =
   299     if is_fol_term t then t else raise TERM("check_is_fol_term",[t]);
   300 
   301 fun check_is_fol th = (check_is_fol_term (prop_of th); th);
   302 
   303 
   304 (*Create a meta-level Horn clause*)
   305 fun make_horn crules th = make_horn crules (tryres(th,crules))
   306 			  handle THM _ => th;
   307 
   308 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
   309   is a HOL disjunction.*)
   310 fun add_contras crules (th,hcs) =
   311   let fun rots (0,th) = hcs
   312 	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
   313 			rots(k-1, assoc_right (th RS disj_comm))
   314   in case nliterals(prop_of th) of
   315 	1 => th::hcs
   316       | n => rots(n, assoc_right th)
   317   end;
   318 
   319 (*Use "theorem naming" to label the clauses*)
   320 fun name_thms label =
   321     let fun name1 (th, (k,ths)) =
   322 	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   323 
   324     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
   325 
   326 (*Is the given disjunction an all-negative support clause?*)
   327 fun is_negative th = forall (not o #1) (literals (prop_of th));
   328 
   329 val neg_clauses = List.filter is_negative;
   330 
   331 
   332 (***** MESON PROOF PROCEDURE *****)
   333 
   334 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
   335 	   As) = rhyps(phi, A::As)
   336   | rhyps (_, As) = As;
   337 
   338 (** Detecting repeated assumptions in a subgoal **)
   339 
   340 (*The stringtree detects repeated assumptions.*)
   341 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
   342 
   343 (*detects repetitions in a list of terms*)
   344 fun has_reps [] = false
   345   | has_reps [_] = false
   346   | has_reps [t,u] = (t aconv u)
   347   | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
   348 		  handle INSERT => true;
   349 
   350 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   351 fun TRYING_eq_assume_tac 0 st = Seq.single st
   352   | TRYING_eq_assume_tac i st =
   353        TRYING_eq_assume_tac (i-1) (eq_assumption i st)
   354        handle THM _ => TRYING_eq_assume_tac (i-1) st;
   355 
   356 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
   357 
   358 (*Loop checking: FAIL if trying to prove the same thing twice
   359   -- if *ANY* subgoal has repeated literals*)
   360 fun check_tac st =
   361   if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   362   then  Seq.empty  else  Seq.single st;
   363 
   364 
   365 (* net_resolve_tac actually made it slower... *)
   366 fun prolog_step_tac horns i =
   367     (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   368     TRYALL_eq_assume_tac;
   369 
   370 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   371 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   372 
   373 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
   374 
   375 
   376 (*Negation Normal Form*)
   377 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   378                not_impD, not_iffD, not_allD, not_exD, not_notD];
   379 
   380 fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
   381     handle THM _ =>
   382         forward_res make_nnf1
   383            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   384     handle THM _ => th;
   385 
   386 (*The simplification removes defined quantifiers and occurrences of True and False, 
   387   as well as tags applied to True and False. nnf_ss also includes the one-point simprocs,
   388   which are needed to avoid the various one-point theorems from generating junk clauses.*)
   389 val tag_True = thm "tag_True";
   390 val tag_False = thm "tag_False";
   391 val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False]
   392 
   393 val nnf_ss =
   394     HOL_basic_ss addsimps
   395      (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] @
   396       thms"split_ifs" @ ex_simps @ all_simps @ simp_thms)
   397      addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
   398 
   399 fun make_nnf th = th |> simplify nnf_ss
   400                      |> make_nnf1
   401 
   402 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   403   clauses that arise from a subgoal.*)
   404 fun skolemize th =
   405   if not (has_consts ["Ex"] (prop_of th)) then th
   406   else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
   407                               disj_exD, disj_exD1, disj_exD2])))
   408     handle THM _ =>
   409         skolemize (forward_res skolemize
   410                    (tryres (th, [conj_forward, disj_forward, all_forward])))
   411     handle THM _ => forward_res skolemize (th RS ex_forward);
   412 
   413 
   414 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   415   The resulting clauses are HOL disjunctions.*)
   416 fun make_clauses ths =
   417     (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
   418 
   419 
   420 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   421 fun make_horns ths =
   422     name_thms "Horn#"
   423       (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
   424 
   425 (*Could simply use nprems_of, which would count remaining subgoals -- no
   426   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   427 
   428 fun best_prolog_tac sizef horns =
   429     BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   430 
   431 fun depth_prolog_tac horns =
   432     DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   433 
   434 (*Return all negative clauses, as possible goal clauses*)
   435 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   436 
   437 fun skolemize_prems_tac prems =
   438     cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
   439     REPEAT o (etac exE);
   440 
   441 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
   442 fun expand_defs_tac st =
   443   let val defs = filter (can dest_equals) (#hyps (crep_thm st))
   444   in  LocalDefs.def_export false defs st  end;
   445 
   446 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
   447 fun MESON cltac i st = 
   448   SELECT_GOAL
   449     (EVERY [rtac ccontr 1,
   450 	    METAHYPS (fn negs =>
   451 		      EVERY1 [skolemize_prems_tac negs,
   452 			      METAHYPS (cltac o make_clauses)]) 1,
   453             expand_defs_tac]) i st
   454   handle TERM _ => no_tac st;	(*probably from check_is_fol*)		      
   455 
   456 (** Best-first search versions **)
   457 
   458 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
   459 fun best_meson_tac sizef =
   460   MESON (fn cls =>
   461          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   462                          (has_fewer_prems 1, sizef)
   463                          (prolog_step_tac (make_horns cls) 1));
   464 
   465 (*First, breaks the goal into independent units*)
   466 val safe_best_meson_tac =
   467      SELECT_GOAL (TRY Safe_tac THEN
   468                   TRYALL (best_meson_tac size_of_subgoals));
   469 
   470 (** Depth-first search version **)
   471 
   472 val depth_meson_tac =
   473      MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
   474                              depth_prolog_tac (make_horns cls)]);
   475 
   476 
   477 (** Iterative deepening version **)
   478 
   479 (*This version does only one inference per call;
   480   having only one eq_assume_tac speeds it up!*)
   481 fun prolog_step_tac' horns =
   482     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   483             take_prefix Thm.no_prems horns
   484         val nrtac = net_resolve_tac horns
   485     in  fn i => eq_assume_tac i ORELSE
   486                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   487                 ((assume_tac i APPEND nrtac i) THEN check_tac)
   488     end;
   489 
   490 fun iter_deepen_prolog_tac horns =
   491     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   492 
   493 fun iter_deepen_meson_tac ths =
   494   MESON (fn cls =>
   495            case (gocls (cls@ths)) of
   496            	[] => no_tac  (*no goal clauses*)
   497               | goes => 
   498 		 (THEN_ITER_DEEPEN (resolve_tac goes 1)
   499 				   (has_fewer_prems 1)
   500 				   (prolog_step_tac' (make_horns (cls@ths)))));
   501 
   502 fun meson_claset_tac ths cs =
   503   SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
   504 
   505 val meson_tac = CLASET' (meson_claset_tac []);
   506 
   507 
   508 (**** Code to support ordinary resolution, rather than Model Elimination ****)
   509 
   510 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
   511   with no contrapositives, for ordinary resolution.*)
   512 
   513 (*Rules to convert the head literal into a negated assumption. If the head
   514   literal is already negated, then using notEfalse instead of notEfalse'
   515   prevents a double negation.*)
   516 val notEfalse = read_instantiate [("R","False")] notE;
   517 val notEfalse' = rotate_prems 1 notEfalse;
   518 
   519 fun negated_asm_of_head th = 
   520     th RS notEfalse handle THM _ => th RS notEfalse';
   521 
   522 (*Converting one clause*)
   523 fun make_meta_clause th = 
   524     negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
   525 
   526 fun make_meta_clauses ths =
   527     name_thms "MClause#"
   528       (distinct Drule.eq_thm_prop (map make_meta_clause ths));
   529 
   530 (*Permute a rule's premises to move the i-th premise to the last position.*)
   531 fun make_last i th =
   532   let val n = nprems_of th 
   533   in  if 1 <= i andalso i <= n 
   534       then Thm.permute_prems (i-1) 1 th
   535       else raise THM("select_literal", i, [th])
   536   end;
   537 
   538 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   539   double-negations.*)
   540 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   541 
   542 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   543 fun select_literal i cl = negate_head (make_last i cl);
   544 
   545 
   546 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   547   expressed as a tactic (or Isar method).  Each assumption of the selected 
   548   goal is converted to NNF and then its existential quantifiers are pulled
   549   to the front. Finally, all existential quantifiers are eliminated, 
   550   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   551   might generate many subgoals.*)
   552 
   553 fun skolemize_tac i st = 
   554   let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
   555   in 
   556      EVERY' [METAHYPS
   557 	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
   558                          THEN REPEAT (etac exE 1))),
   559             REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
   560   end
   561   handle Subscript => Seq.empty;
   562 
   563 (*Top-level conversion to meta-level clauses. Each clause has  
   564   leading !!-bound universal variables, to express generality. To get 
   565   disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
   566 val make_clauses_tac = 
   567   SUBGOAL
   568     (fn (prop,_) =>
   569      let val ts = Logic.strip_assums_hyp prop
   570      in EVERY1 
   571 	 [METAHYPS
   572 	    (fn hyps => 
   573               (Method.insert_tac
   574                 (map forall_intr_vars 
   575                   (make_meta_clauses (make_clauses hyps))) 1)),
   576 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   577      end);
   578      
   579      
   580 (*** setup the special skoklemization methods ***)
   581 
   582 (*No CHANGED_PROP here, since these always appear in the preamble*)
   583 
   584 val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
   585 
   586 val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
   587 
   588 val skolemize_setup =
   589   Method.add_methods
   590     [("skolemize", Method.no_args skolemize_meth, 
   591       "Skolemization into existential quantifiers"),
   592      ("make_clauses", Method.no_args make_clauses_meth, 
   593       "Conversion to !!-quantified meta-level clauses")];
   594 
   595 end;
   596 
   597 structure BasicMeson: BASIC_MESON = Meson;
   598 open BasicMeson;