src/HOL/Tools/meson.ML
author paulson
Tue Jun 28 15:28:04 2005 +0200 (2005-06-28)
changeset 16588 8de758143786
parent 16563 a92f96951355
child 16801 4bb13fa6ae72
permissions -rw-r--r--
stricter first-order check for meson
     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 case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   142 	    Const ("op &", _) => (*conjunction*)
   143 		cnf_aux seen (th RS conjunct1,
   144 			      cnf_aux seen (th RS conjunct2, ths))
   145 	  | Const ("All", _) => (*universal quantifier*)
   146 	        cnf_aux seen (freeze_spec th,  ths)
   147 	  | Const ("Ex", _) => 
   148 	      (*existential quantifier: Insert Skolem functions*)
   149 	      cnf_aux seen (tryres (th,skoths), ths)
   150 	  | Const ("op |", _) => (*disjunction*)
   151 	      let val tac =
   152 		  (METAHYPS (resop (cnf_nil seen)) 1) THEN
   153 		   (fn st' => st' |>  
   154 		      METAHYPS 
   155 		        (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
   156 	      in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
   157 	  | _ => (*no work to do*) th::ths 
   158       and cnf_nil seen th = (cnf_aux seen (th,[]))
   159   in 
   160     name_ref := 19;  (*It's safe to reset this in a top-level call to cnf*)
   161     (cnf skoths (th RS conjunct1, cnf skoths (th RS conjunct2, ths))
   162      handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths))
   163   end;
   164 
   165 (*Convert all suitable free variables to schematic variables, 
   166   but don't discharge assumptions.*)
   167 fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
   168 
   169 fun make_cnf skoths th = map generalize (cnf skoths (th, []));
   170 
   171 
   172 (**** Removal of duplicate literals ****)
   173 
   174 (*Forward proof, passing extra assumptions as theorems to the tactic*)
   175 fun forward_res2 nf hyps st =
   176   case Seq.pull
   177 	(REPEAT
   178 	 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   179 	 st)
   180   of SOME(th,_) => th
   181    | NONE => raise THM("forward_res2", 0, [st]);
   182 
   183 (*Remove duplicates in P|Q by assuming ~P in Q
   184   rls (initially []) accumulates assumptions of the form P==>False*)
   185 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
   186     handle THM _ => tryres(th,rls)
   187     handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
   188 			   [disj_FalseD1, disj_FalseD2, asm_rl])
   189     handle THM _ => th;
   190 
   191 (*Remove duplicate literals, if there are any*)
   192 fun nodups th =
   193     if null(findrep(literals(prop_of th))) then th
   194     else nodups_aux [] th;
   195 
   196 
   197 (**** Generation of contrapositives ****)
   198 
   199 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   200 fun assoc_right th = assoc_right (th RS disj_assoc)
   201 	handle THM _ => th;
   202 
   203 (*Must check for negative literal first!*)
   204 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
   205 
   206 (*For ordinary resolution. *)
   207 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
   208 
   209 (*Create a goal or support clause, conclusing False*)
   210 fun make_goal th =   (*Must check for negative literal first!*)
   211     make_goal (tryres(th, clause_rules))
   212   handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
   213 
   214 (*Sort clauses by number of literals*)
   215 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
   216 
   217 (*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*)
   218 fun sort_clauses ths =
   219     sort (make_ord fewerlits) (List.filter (not o is_taut) ths);
   220 
   221 (*True if the given type contains bool anywhere*)
   222 fun has_bool (Type("bool",_)) = true
   223   | has_bool (Type(_, Ts)) = exists has_bool Ts
   224   | has_bool _ = false;
   225   
   226 (*Is the string the name of a connective? It doesn't matter if this list is
   227   incomplete, since when actually called, the only connectives likely to
   228   remain are & | Not.*)  
   229 fun is_conn c = c mem_string
   230     ["Trueprop", "op &", "op |", "op -->", "op =", "Not", 
   231      "All", "Ex", "Ball", "Bex"];
   232 
   233 (*True if the term contains a function where the type of any argument contains
   234   bool.*)
   235 val has_bool_arg_const = 
   236     exists_Const
   237       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
   238       
   239 val has_meta_conn = 
   240     exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]);
   241   
   242 (*Raises an exception if any Vars in the theorem mention type bool; they
   243   could cause make_horn to loop! Also rejects functions whose arguments are 
   244   Booleans or other functions.*)
   245 fun check_is_fol th = 
   246   let val {prop,...} = rep_thm th
   247   in if exists (has_bool o fastype_of) (term_vars prop)  orelse
   248         not (Term.is_first_order ["all","All","Ex"] prop) orelse
   249         has_bool_arg_const prop  orelse  
   250         has_meta_conn prop
   251   then raise THM ("check_is_fol", 0, [th]) else th
   252   end;
   253 
   254 (*Create a meta-level Horn clause*)
   255 fun make_horn crules th = make_horn crules (tryres(th,crules))
   256 			  handle THM _ => th;
   257 
   258 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
   259   is a HOL disjunction.*)
   260 fun add_contras crules (th,hcs) =
   261   let fun rots (0,th) = hcs
   262 	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
   263 			rots(k-1, assoc_right (th RS disj_comm))
   264   in case nliterals(prop_of th) of
   265 	1 => th::hcs
   266       | n => rots(n, assoc_right th)
   267   end;
   268 
   269 (*Use "theorem naming" to label the clauses*)
   270 fun name_thms label =
   271     let fun name1 (th, (k,ths)) =
   272 	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   273 
   274     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
   275 
   276 (*Is the given disjunction an all-negative support clause?*)
   277 fun is_negative th = forall (not o #1) (literals (prop_of th));
   278 
   279 val neg_clauses = List.filter is_negative;
   280 
   281 
   282 (***** MESON PROOF PROCEDURE *****)
   283 
   284 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
   285 	   As) = rhyps(phi, A::As)
   286   | rhyps (_, As) = As;
   287 
   288 (** Detecting repeated assumptions in a subgoal **)
   289 
   290 (*The stringtree detects repeated assumptions.*)
   291 fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv);
   292 
   293 (*detects repetitions in a list of terms*)
   294 fun has_reps [] = false
   295   | has_reps [_] = false
   296   | has_reps [t,u] = (t aconv u)
   297   | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
   298 		  handle INSERT => true;
   299 
   300 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   301 fun TRYALL_eq_assume_tac 0 st = Seq.single st
   302   | TRYALL_eq_assume_tac i st =
   303        TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
   304        handle THM _ => TRYALL_eq_assume_tac (i-1) st;
   305 
   306 (*Loop checking: FAIL if trying to prove the same thing twice
   307   -- if *ANY* subgoal has repeated literals*)
   308 fun check_tac st =
   309   if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   310   then  Seq.empty  else  Seq.single st;
   311 
   312 
   313 (* net_resolve_tac actually made it slower... *)
   314 fun prolog_step_tac horns i =
   315     (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   316     TRYALL eq_assume_tac;
   317 
   318 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   319 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   320 
   321 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
   322 
   323 
   324 (*Negation Normal Form*)
   325 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   326                not_impD, not_iffD, not_allD, not_exD, not_notD];
   327 
   328 fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
   329     handle THM _ =>
   330         forward_res make_nnf1
   331            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   332     handle THM _ => th;
   333 
   334 (*The simplification removes defined quantifiers and occurrences of True and False.*)
   335 val nnf_ss = HOL_basic_ss addsimps Ex1_def::Ball_def::Bex_def::simp_thms;
   336 
   337 fun make_nnf th = th |> simplify nnf_ss
   338                      |> check_is_fol |> make_nnf1
   339 
   340 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   341   clauses that arise from a subgoal.*)
   342 fun skolemize th =
   343   if not (has_consts ["Ex"] (prop_of th)) then th
   344   else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
   345                               disj_exD, disj_exD1, disj_exD2])))
   346     handle THM _ =>
   347         skolemize (forward_res skolemize
   348                    (tryres (th, [conj_forward, disj_forward, all_forward])))
   349     handle THM _ => forward_res skolemize (th RS ex_forward);
   350 
   351 
   352 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   353   The resulting clauses are HOL disjunctions.*)
   354 fun make_clauses ths =
   355     (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
   356 
   357 
   358 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   359 fun make_horns ths =
   360     name_thms "Horn#"
   361       (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
   362 
   363 (*Could simply use nprems_of, which would count remaining subgoals -- no
   364   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   365 
   366 fun best_prolog_tac sizef horns =
   367     BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   368 
   369 fun depth_prolog_tac horns =
   370     DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   371 
   372 (*Return all negative clauses, as possible goal clauses*)
   373 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   374 
   375 fun skolemize_prems_tac prems =
   376     cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
   377     REPEAT o (etac exE);
   378 
   379 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
   380 fun MESON cltac i st = 
   381   SELECT_GOAL
   382    (EVERY1 [rtac ccontr,
   383 	    METAHYPS (fn negs =>
   384 		      EVERY1 [skolemize_prems_tac negs,
   385 			      METAHYPS (cltac o make_clauses)])]) i st
   386   handle THM _ => no_tac st;	(*probably from check_is_fol*)		      
   387 
   388 (** Best-first search versions **)
   389 
   390 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
   391 fun best_meson_tac sizef =
   392   MESON (fn cls =>
   393          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   394                          (has_fewer_prems 1, sizef)
   395                          (prolog_step_tac (make_horns cls) 1));
   396 
   397 (*First, breaks the goal into independent units*)
   398 val safe_best_meson_tac =
   399      SELECT_GOAL (TRY Safe_tac THEN
   400                   TRYALL (best_meson_tac size_of_subgoals));
   401 
   402 (** Depth-first search version **)
   403 
   404 val depth_meson_tac =
   405      MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
   406                              depth_prolog_tac (make_horns cls)]);
   407 
   408 
   409 (** Iterative deepening version **)
   410 
   411 (*This version does only one inference per call;
   412   having only one eq_assume_tac speeds it up!*)
   413 fun prolog_step_tac' horns =
   414     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   415             take_prefix Thm.no_prems horns
   416         val nrtac = net_resolve_tac horns
   417     in  fn i => eq_assume_tac i ORELSE
   418                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   419                 ((assume_tac i APPEND nrtac i) THEN check_tac)
   420     end;
   421 
   422 fun iter_deepen_prolog_tac horns =
   423     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   424 
   425 fun iter_deepen_meson_tac ths =
   426   MESON (fn cls =>
   427            case (gocls (cls@ths)) of
   428            	[] => no_tac  (*no goal clauses*)
   429               | goes => 
   430 		 (THEN_ITER_DEEPEN (resolve_tac goes 1)
   431 				   (has_fewer_prems 1)
   432 				   (prolog_step_tac' (make_horns (cls@ths)))));
   433 
   434 fun meson_claset_tac ths cs =
   435   SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
   436 
   437 val meson_tac = CLASET' (meson_claset_tac []);
   438 
   439 
   440 (**** Code to support ordinary resolution, rather than Model Elimination ****)
   441 
   442 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
   443   with no contrapositives, for ordinary resolution.*)
   444 
   445 (*Rules to convert the head literal into a negated assumption. If the head
   446   literal is already negated, then using notEfalse instead of notEfalse'
   447   prevents a double negation.*)
   448 val notEfalse = read_instantiate [("R","False")] notE;
   449 val notEfalse' = rotate_prems 1 notEfalse;
   450 
   451 fun negated_asm_of_head th = 
   452     th RS notEfalse handle THM _ => th RS notEfalse';
   453 
   454 (*Converting one clause*)
   455 fun make_meta_clause th = 
   456     negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
   457 
   458 fun make_meta_clauses ths =
   459     name_thms "MClause#"
   460       (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
   461 
   462 (*Permute a rule's premises to move the i-th premise to the last position.*)
   463 fun make_last i th =
   464   let val n = nprems_of th 
   465   in  if 1 <= i andalso i <= n 
   466       then Thm.permute_prems (i-1) 1 th
   467       else raise THM("select_literal", i, [th])
   468   end;
   469 
   470 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   471   double-negations.*)
   472 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   473 
   474 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   475 fun select_literal i cl = negate_head (make_last i cl);
   476 
   477 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   478   expressed as a tactic (or Isar method).  Each assumption of the selected 
   479   goal is converted to NNF and then its existential quantifiers are pulled
   480   to the front. Finally, all existential quantifiers are eliminated, 
   481   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   482   might generate many subgoals.*)
   483 val skolemize_tac = 
   484   SUBGOAL
   485     (fn (prop,_) =>
   486      let val ts = Logic.strip_assums_hyp prop
   487      in EVERY1 
   488 	 [METAHYPS
   489 	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
   490                          THEN REPEAT (etac exE 1))),
   491 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   492      end);
   493 
   494 (*Top-level conversion to meta-level clauses. Each clause has  
   495   leading !!-bound universal variables, to express generality. To get 
   496   disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
   497 val make_clauses_tac = 
   498   SUBGOAL
   499     (fn (prop,_) =>
   500      let val ts = Logic.strip_assums_hyp prop
   501      in EVERY1 
   502 	 [METAHYPS
   503 	    (fn hyps => 
   504               (Method.insert_tac
   505                 (map forall_intr_vars 
   506                   (make_meta_clauses (make_clauses hyps))) 1)),
   507 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   508      end);
   509      
   510      
   511 (*** setup the special skoklemization methods ***)
   512 
   513 (*No CHANGED_PROP here, since these always appear in the preamble*)
   514 
   515 val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
   516 
   517 val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
   518 
   519 val skolemize_setup =
   520  [Method.add_methods
   521   [("skolemize", Method.no_args skolemize_meth, 
   522     "Skolemization into existential quantifiers"),
   523    ("make_clauses", Method.no_args make_clauses_meth, 
   524     "Conversion to !!-quantified meta-level clauses")]];
   525 
   526 end;
   527 
   528 structure BasicMeson: BASIC_MESON = Meson;
   529 open BasicMeson;