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