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