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