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