src/HOL/Tools/meson.ML
author haftmann
Fri Dec 16 09:00:11 2005 +0100 (2005-12-16)
changeset 18418 bf448d999b7e
parent 18405 afb1a52a7011
child 18508 c5861e128a95
permissions -rw-r--r--
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
     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 th = 
   296   let val {prop,...} = rep_thm th
   297   in if exists (has_bool o fastype_of) (term_vars prop)  orelse
   298         not (Term.is_first_order ["all","All","Ex"] prop) orelse
   299         has_bool_arg_const prop  orelse  
   300         has_meta_conn prop
   301   then raise THM ("check_is_fol", 0, [th]) else th
   302   end;
   303 
   304 fun check_is_fol_term term =
   305     if exists (has_bool o fastype_of) (term_vars term)  orelse
   306         not (Term.is_first_order ["all","All","Ex"] term) orelse
   307         has_bool_arg_const term  orelse  
   308         has_meta_conn term
   309     then raise TERM("check_is_fol_term",[term]) else term;
   310 
   311 
   312 (*Create a meta-level Horn clause*)
   313 fun make_horn crules th = make_horn crules (tryres(th,crules))
   314 			  handle THM _ => th;
   315 
   316 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
   317   is a HOL disjunction.*)
   318 fun add_contras crules (th,hcs) =
   319   let fun rots (0,th) = hcs
   320 	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
   321 			rots(k-1, assoc_right (th RS disj_comm))
   322   in case nliterals(prop_of th) of
   323 	1 => th::hcs
   324       | n => rots(n, assoc_right th)
   325   end;
   326 
   327 (*Use "theorem naming" to label the clauses*)
   328 fun name_thms label =
   329     let fun name1 (th, (k,ths)) =
   330 	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   331 
   332     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
   333 
   334 (*Is the given disjunction an all-negative support clause?*)
   335 fun is_negative th = forall (not o #1) (literals (prop_of th));
   336 
   337 val neg_clauses = List.filter is_negative;
   338 
   339 
   340 (***** MESON PROOF PROCEDURE *****)
   341 
   342 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
   343 	   As) = rhyps(phi, A::As)
   344   | rhyps (_, As) = As;
   345 
   346 (** Detecting repeated assumptions in a subgoal **)
   347 
   348 (*The stringtree detects repeated assumptions.*)
   349 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
   350 
   351 (*detects repetitions in a list of terms*)
   352 fun has_reps [] = false
   353   | has_reps [_] = false
   354   | has_reps [t,u] = (t aconv u)
   355   | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
   356 		  handle INSERT => true;
   357 
   358 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   359 fun TRYALL_eq_assume_tac 0 st = Seq.single st
   360   | TRYALL_eq_assume_tac i st =
   361        TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
   362        handle THM _ => TRYALL_eq_assume_tac (i-1) st;
   363 
   364 (*Loop checking: FAIL if trying to prove the same thing twice
   365   -- if *ANY* subgoal has repeated literals*)
   366 fun check_tac st =
   367   if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   368   then  Seq.empty  else  Seq.single st;
   369 
   370 
   371 (* net_resolve_tac actually made it slower... *)
   372 fun prolog_step_tac horns i =
   373     (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   374     TRYALL eq_assume_tac;
   375 
   376 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   377 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   378 
   379 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
   380 
   381 
   382 (*Negation Normal Form*)
   383 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   384                not_impD, not_iffD, not_allD, not_exD, not_notD];
   385 
   386 fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
   387     handle THM _ =>
   388         forward_res make_nnf1
   389            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   390     handle THM _ => th;
   391 
   392 (*The simplification removes defined quantifiers and occurrences of True and False, 
   393   as well as tags applied to True and False. nnf_ss also includes the one-point simprocs,
   394   which are needed to avoid the various one-point theorems from generating junk clauses.*)
   395 val tag_True = thm "tag_True";
   396 val tag_False = thm "tag_False";
   397 val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False]
   398 
   399 val nnf_ss =
   400     HOL_basic_ss addsimps
   401      (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp]
   402      @ ex_simps @ all_simps @ simp_thms)
   403      addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]
   404      addsplits [split_if];
   405 
   406 fun make_nnf th = th |> simplify nnf_ss
   407                      |> make_nnf1
   408 
   409 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   410   clauses that arise from a subgoal.*)
   411 fun skolemize th =
   412   if not (has_consts ["Ex"] (prop_of th)) then th
   413   else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
   414                               disj_exD, disj_exD1, disj_exD2])))
   415     handle THM _ =>
   416         skolemize (forward_res skolemize
   417                    (tryres (th, [conj_forward, disj_forward, all_forward])))
   418     handle THM _ => forward_res skolemize (th RS ex_forward);
   419 
   420 
   421 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   422   The resulting clauses are HOL disjunctions.*)
   423 fun make_clauses ths =
   424     (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
   425 
   426 
   427 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   428 fun make_horns ths =
   429     name_thms "Horn#"
   430       (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
   431 
   432 (*Could simply use nprems_of, which would count remaining subgoals -- no
   433   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   434 
   435 fun best_prolog_tac sizef horns =
   436     BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   437 
   438 fun depth_prolog_tac horns =
   439     DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   440 
   441 (*Return all negative clauses, as possible goal clauses*)
   442 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   443 
   444 fun skolemize_prems_tac prems =
   445     cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
   446     REPEAT o (etac exE);
   447 
   448 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
   449 fun expand_defs_tac st =
   450   let val defs = filter (can dest_equals) (#hyps (crep_thm st))
   451   in  ProofContext.export_def false defs st  end;
   452 
   453 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
   454 fun MESON cltac i st = 
   455   SELECT_GOAL
   456     (EVERY [rtac ccontr 1,
   457 	    METAHYPS (fn negs =>
   458 		      EVERY1 [skolemize_prems_tac negs,
   459 			      METAHYPS (cltac o make_clauses)]) 1,
   460             expand_defs_tac]) i st
   461   handle THM _ => no_tac st;	(*probably from check_is_fol*)		      
   462 
   463 (** Best-first search versions **)
   464 
   465 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
   466 fun best_meson_tac sizef =
   467   MESON (fn cls =>
   468          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   469                          (has_fewer_prems 1, sizef)
   470                          (prolog_step_tac (make_horns cls) 1));
   471 
   472 (*First, breaks the goal into independent units*)
   473 val safe_best_meson_tac =
   474      SELECT_GOAL (TRY Safe_tac THEN
   475                   TRYALL (best_meson_tac size_of_subgoals));
   476 
   477 (** Depth-first search version **)
   478 
   479 val depth_meson_tac =
   480      MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
   481                              depth_prolog_tac (make_horns cls)]);
   482 
   483 
   484 (** Iterative deepening version **)
   485 
   486 (*This version does only one inference per call;
   487   having only one eq_assume_tac speeds it up!*)
   488 fun prolog_step_tac' horns =
   489     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   490             take_prefix Thm.no_prems horns
   491         val nrtac = net_resolve_tac horns
   492     in  fn i => eq_assume_tac i ORELSE
   493                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   494                 ((assume_tac i APPEND nrtac i) THEN check_tac)
   495     end;
   496 
   497 fun iter_deepen_prolog_tac horns =
   498     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   499 
   500 fun iter_deepen_meson_tac ths =
   501   MESON (fn cls =>
   502            case (gocls (cls@ths)) of
   503            	[] => no_tac  (*no goal clauses*)
   504               | goes => 
   505 		 (THEN_ITER_DEEPEN (resolve_tac goes 1)
   506 				   (has_fewer_prems 1)
   507 				   (prolog_step_tac' (make_horns (cls@ths)))));
   508 
   509 fun meson_claset_tac ths cs =
   510   SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
   511 
   512 val meson_tac = CLASET' (meson_claset_tac []);
   513 
   514 
   515 (**** Code to support ordinary resolution, rather than Model Elimination ****)
   516 
   517 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
   518   with no contrapositives, for ordinary resolution.*)
   519 
   520 (*Rules to convert the head literal into a negated assumption. If the head
   521   literal is already negated, then using notEfalse instead of notEfalse'
   522   prevents a double negation.*)
   523 val notEfalse = read_instantiate [("R","False")] notE;
   524 val notEfalse' = rotate_prems 1 notEfalse;
   525 
   526 fun negated_asm_of_head th = 
   527     th RS notEfalse handle THM _ => th RS notEfalse';
   528 
   529 (*Converting one clause*)
   530 fun make_meta_clause th = 
   531     negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
   532 
   533 fun make_meta_clauses ths =
   534     name_thms "MClause#"
   535       (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
   536 
   537 (*Permute a rule's premises to move the i-th premise to the last position.*)
   538 fun make_last i th =
   539   let val n = nprems_of th 
   540   in  if 1 <= i andalso i <= n 
   541       then Thm.permute_prems (i-1) 1 th
   542       else raise THM("select_literal", i, [th])
   543   end;
   544 
   545 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   546   double-negations.*)
   547 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   548 
   549 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   550 fun select_literal i cl = negate_head (make_last i cl);
   551 
   552 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   553   expressed as a tactic (or Isar method).  Each assumption of the selected 
   554   goal is converted to NNF and then its existential quantifiers are pulled
   555   to the front. Finally, all existential quantifiers are eliminated, 
   556   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   557   might generate many subgoals.*)
   558 
   559 
   560 
   561 val skolemize_tac = 
   562   SUBGOAL
   563     (fn (prop,_) =>
   564      let val ts = Logic.strip_assums_hyp prop
   565      in EVERY1 
   566 	 [METAHYPS
   567 	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
   568                          THEN REPEAT (etac exE 1))),
   569 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   570      end);
   571 
   572 
   573 
   574 (*Top-level conversion to meta-level clauses. Each clause has  
   575   leading !!-bound universal variables, to express generality. To get 
   576   disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
   577 val make_clauses_tac = 
   578   SUBGOAL
   579     (fn (prop,_) =>
   580      let val ts = Logic.strip_assums_hyp prop
   581      in EVERY1 
   582 	 [METAHYPS
   583 	    (fn hyps => 
   584               (Method.insert_tac
   585                 (map forall_intr_vars 
   586                   (make_meta_clauses (make_clauses hyps))) 1)),
   587 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   588      end);
   589      
   590      
   591 (*** setup the special skoklemization methods ***)
   592 
   593 (*No CHANGED_PROP here, since these always appear in the preamble*)
   594 
   595 val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
   596 
   597 val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
   598 
   599 val skolemize_setup =
   600  [Method.add_methods
   601   [("skolemize", Method.no_args skolemize_meth, 
   602     "Skolemization into existential quantifiers"),
   603    ("make_clauses", Method.no_args make_clauses_meth, 
   604     "Conversion to !!-quantified meta-level clauses")]];
   605 
   606 end;
   607 
   608 structure BasicMeson: BASIC_MESON = Meson;
   609 open BasicMeson;