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