src/HOL/Tools/meson.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21174 4d733b76b5fa
child 21588 cd0dc678a205
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     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 finish_cnf	: thm list -> thm list
    19   val make_nnf		: thm -> thm
    20   val make_nnf1		: thm -> thm
    21   val skolemize		: thm -> thm
    22   val make_clauses	: thm list -> thm list
    23   val make_horns	: thm list -> thm list
    24   val best_prolog_tac	: (thm -> int) -> thm list -> tactic
    25   val depth_prolog_tac	: thm list -> tactic
    26   val gocls		: thm list -> thm list
    27   val skolemize_prems_tac	: thm list -> int -> tactic
    28   val MESON		: (thm list -> tactic) -> int -> tactic
    29   val best_meson_tac	: (thm -> int) -> int -> tactic
    30   val safe_best_meson_tac	: int -> tactic
    31   val depth_meson_tac	: int -> tactic
    32   val prolog_step_tac'	: thm list -> int -> tactic
    33   val iter_deepen_prolog_tac	: thm list -> tactic
    34   val iter_deepen_meson_tac	: thm list -> int -> tactic
    35   val meson_tac		: int -> tactic
    36   val negate_head	: thm -> thm
    37   val select_literal	: int -> thm -> thm
    38   val skolemize_tac	: int -> tactic
    39   val make_clauses_tac	: int -> tactic
    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 
    70 (** First-order Resolution **)
    71 
    72 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
    73 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    74 
    75 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
    76 
    77 (*FIXME: currently does not "rename variables apart"*)
    78 fun first_order_resolve thA thB =
    79   let val thy = theory_of_thm thA
    80       val tmA = concl_of thA
    81       fun match pat = Pattern.first_order_match thy (pat,tmA) (tyenv0,tenv0)
    82       val Const("==>",_) $ tmB $ _ = prop_of thB
    83       val (tyenv,tenv) = match tmB
    84       val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    85   in  thA RS (cterm_instantiate ct_pairs thB)  end
    86   handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
    87 
    88 (*raises exception if no rules apply -- unlike RL*)
    89 fun tryres (th, rls) = 
    90   let fun tryall [] = raise THM("tryres", 0, th::rls)
    91         | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
    92   in  tryall rls  end;
    93   
    94 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    95   e.g. from conj_forward, should have the form
    96     "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
    97   and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
    98 fun forward_res nf st =
    99   let fun forward_tacf [prem] = rtac (nf prem) 1
   100         | forward_tacf prems = 
   101             error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
   102                    string_of_thm st ^
   103                    "\nPremises:\n" ^
   104                    cat_lines (map string_of_thm prems))
   105   in
   106     case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
   107     of SOME(th,_) => th
   108      | NONE => raise THM("forward_res", 0, [st])
   109   end;
   110 
   111 (*Are any of the logical connectives in "bs" present in the term?*)
   112 fun has_conns bs =
   113   let fun has (Const(a,_)) = false
   114         | has (Const("Trueprop",_) $ p) = has p
   115         | has (Const("Not",_) $ p) = has p
   116         | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
   117         | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
   118         | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
   119         | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
   120 	| has _ = false
   121   in  has  end;
   122   
   123 
   124 (**** Clause handling ****)
   125 
   126 fun literals (Const("Trueprop",_) $ P) = literals P
   127   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
   128   | literals (Const("Not",_) $ P) = [(false,P)]
   129   | literals P = [(true,P)];
   130 
   131 (*number of literals in a term*)
   132 val nliterals = length o literals;
   133 
   134 
   135 (*** Tautology Checking ***)
   136 
   137 fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) = 
   138       signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
   139   | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
   140   | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
   141   
   142 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
   143 
   144 (*Literals like X=X are tautologous*)
   145 fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
   146   | taut_poslit (Const("True",_)) = true
   147   | taut_poslit _ = false;
   148 
   149 fun is_taut th =
   150   let val (poslits,neglits) = signed_lits th
   151   in  exists taut_poslit poslits
   152       orelse
   153       exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
   154   end
   155   handle TERM _ => false;	(*probably dest_Trueprop on a weird theorem*)		      
   156 
   157 
   158 (*** To remove trivial negated equality literals from clauses ***)
   159 
   160 (*They are typically functional reflexivity axioms and are the converses of
   161   injectivity equivalences*)
   162   
   163 val not_refl_disj_D = thm"meson_not_refl_disj_D";
   164 
   165 (*Is either term a Var that does not properly occur in the other term?*)
   166 fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
   167   | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
   168   | eliminable _ = false;
   169 
   170 fun refl_clause_aux 0 th = th
   171   | refl_clause_aux n th =
   172        case HOLogic.dest_Trueprop (concl_of th) of
   173 	  (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => 
   174             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
   175 	| (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => 
   176 	    if eliminable(t,u) 
   177 	    then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
   178 	    else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
   179 	| (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
   180 	| _ => (*not a disjunction*) th;
   181 
   182 fun notequal_lits_count (Const ("op |", _) $ P $ Q) = 
   183       notequal_lits_count P + notequal_lits_count Q
   184   | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
   185   | notequal_lits_count _ = 0;
   186 
   187 (*Simplify a clause by applying reflexivity to its negated equality literals*)
   188 fun refl_clause th = 
   189   let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
   190   in  zero_var_indexes (refl_clause_aux neqs th)  end
   191   handle TERM _ => th;	(*probably dest_Trueprop on a weird theorem*)		      
   192 
   193 
   194 (*** The basic CNF transformation ***)
   195 
   196 val max_clauses = ref 20;
   197 
   198 fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
   199 fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
   200 
   201 (*Estimate the number of clauses in order to detect infeasible theorems*)
   202 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
   203   | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
   204   | signed_nclauses b (Const("op &",_) $ t $ u) = 
   205       if b then sum (signed_nclauses b t) (signed_nclauses b u)
   206            else prod (signed_nclauses b t) (signed_nclauses b u)
   207   | signed_nclauses b (Const("op |",_) $ t $ u) = 
   208       if b then prod (signed_nclauses b t) (signed_nclauses b u)
   209            else sum (signed_nclauses b t) (signed_nclauses b u)
   210   | signed_nclauses b (Const("op -->",_) $ t $ u) = 
   211       if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
   212            else sum (signed_nclauses (not b) t) (signed_nclauses b u)
   213   | signed_nclauses b (Const("op =",_) $ t $ u) = 
   214       if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
   215                     (prod (signed_nclauses (not b) u) (signed_nclauses b t))
   216            else sum (prod (signed_nclauses b t) (signed_nclauses b u))
   217                     (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
   218   | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
   219   | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
   220   | signed_nclauses _ _ = 1; (* literal *)
   221 
   222 val nclauses = signed_nclauses true;
   223 
   224 fun too_many_clauses t = nclauses t >= !max_clauses;
   225 
   226 (*Replaces universally quantified variables by FREE variables -- because
   227   assumptions may not contain scheme variables.  Later, call "generalize". *)
   228 fun freeze_spec th =
   229   let val newname = gensym "mes_"
   230       val spec' = read_instantiate [("x", newname)] spec
   231   in  th RS spec'  end;
   232 
   233 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
   234   and then normalized via function nf. The normal form is given to resolve_tac,
   235   presumably to instantiate a Boolean variable.*)
   236 fun resop nf [prem] = resolve_tac (nf prem) 1;
   237 
   238 (*Any need to extend this list with 
   239   "HOL.type_class","Code_Generator.eq_class","ProtoPure.term"?*)
   240 val has_meta_conn = 
   241     exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
   242 
   243 fun apply_skolem_ths (th, rls) = 
   244   let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
   245         | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
   246   in  tryall rls  end;
   247   
   248 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
   249   Strips universal quantifiers and breaks up conjunctions.
   250   Eliminates existential quantifiers using skoths: Skolemization theorems.*)
   251 fun cnf skoths (th,ths) =
   252   let fun cnf_aux (th,ths) =
   253   	if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   254         else if not (has_conns ["All","Ex","op &"] (prop_of th))  
   255 	then th::ths (*no work to do, terminate*)
   256 	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   257 	    Const ("op &", _) => (*conjunction*)
   258 		cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
   259 	  | Const ("All", _) => (*universal quantifier*)
   260 	        cnf_aux (freeze_spec th,  ths)
   261 	  | Const ("Ex", _) => 
   262 	      (*existential quantifier: Insert Skolem functions*)
   263 	      cnf_aux (apply_skolem_ths (th,skoths), ths)
   264 	  | Const ("op |", _) => (*disjunction*)
   265 	      let val tac =
   266 		  (METAHYPS (resop cnf_nil) 1) THEN
   267 		   (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
   268 	      in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
   269 	  | _ => (*no work to do*) th::ths 
   270       and cnf_nil th = cnf_aux (th,[])
   271   in 
   272     if too_many_clauses (concl_of th) 
   273     then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
   274     else cnf_aux (th,ths)
   275   end;
   276 
   277 (*Convert all suitable free variables to schematic variables, 
   278   but don't discharge assumptions.*)
   279 fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
   280 
   281 fun make_cnf skoths th = cnf skoths (th, []);
   282 
   283 (*Generalization, removal of redundant equalities, removal of tautologies.*)
   284 fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
   285 
   286 
   287 (**** Removal of duplicate literals ****)
   288 
   289 (*Forward proof, passing extra assumptions as theorems to the tactic*)
   290 fun forward_res2 nf hyps st =
   291   case Seq.pull
   292 	(REPEAT
   293 	 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   294 	 st)
   295   of SOME(th,_) => th
   296    | NONE => raise THM("forward_res2", 0, [st]);
   297 
   298 (*Remove duplicates in P|Q by assuming ~P in Q
   299   rls (initially []) accumulates assumptions of the form P==>False*)
   300 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
   301     handle THM _ => tryres(th,rls)
   302     handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
   303 			   [disj_FalseD1, disj_FalseD2, asm_rl])
   304     handle THM _ => th;
   305 
   306 (*Remove duplicate literals, if there are any*)
   307 fun nodups th =
   308   if has_duplicates (op =) (literals (prop_of th))
   309     then nodups_aux [] th
   310     else th;
   311 
   312 
   313 (**** Generation of contrapositives ****)
   314 
   315 fun is_left (Const ("Trueprop", _) $ 
   316                (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
   317   | is_left _ = false;
   318                
   319 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   320 fun assoc_right th = 
   321   if is_left (prop_of th) then assoc_right (th RS disj_assoc)
   322   else th;
   323 
   324 (*Must check for negative literal first!*)
   325 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
   326 
   327 (*For ordinary resolution. *)
   328 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
   329 
   330 (*Create a goal or support clause, conclusing False*)
   331 fun make_goal th =   (*Must check for negative literal first!*)
   332     make_goal (tryres(th, clause_rules))
   333   handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
   334 
   335 (*Sort clauses by number of literals*)
   336 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
   337 
   338 fun sort_clauses ths = sort (make_ord fewerlits) ths;
   339 
   340 (*True if the given type contains bool anywhere*)
   341 fun has_bool (Type("bool",_)) = true
   342   | has_bool (Type(_, Ts)) = exists has_bool Ts
   343   | has_bool _ = false;
   344   
   345 (*Is the string the name of a connective? Really only | and Not can remain, 
   346   since this code expects to be called on a clause form.*)  
   347 val is_conn = member (op =)
   348     ["Trueprop", "op &", "op |", "op -->", "Not", 
   349      "All", "Ex", "Ball", "Bex"];
   350 
   351 (*True if the term contains a function--not a logical connective--where the type 
   352   of any argument contains bool.*)
   353 val has_bool_arg_const = 
   354     exists_Const
   355       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
   356       
   357 (*Raises an exception if any Vars in the theorem mention type bool. 
   358   Also rejects functions whose arguments are Booleans or other functions.*)
   359 fun is_fol_term t =
   360     not (exists (has_bool o fastype_of) (term_vars t)  orelse
   361 	 not (Term.is_first_order ["all","All","Ex"] t) orelse
   362 	 has_bool_arg_const t  orelse  
   363 	 has_meta_conn t);
   364 
   365 fun rigid t = not (is_Var (head_of t));
   366 
   367 fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
   368   | ok4horn (Const ("Trueprop",_) $ t) = rigid t
   369   | ok4horn _ = false;
   370 
   371 (*Create a meta-level Horn clause*)
   372 fun make_horn crules th = 
   373   if ok4horn (concl_of th) 
   374   then make_horn crules (tryres(th,crules)) handle THM _ => th
   375   else th;
   376 
   377 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
   378   is a HOL disjunction.*)
   379 fun add_contras crules (th,hcs) =
   380   let fun rots (0,th) = hcs
   381 	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
   382 			rots(k-1, assoc_right (th RS disj_comm))
   383   in case nliterals(prop_of th) of
   384 	1 => th::hcs
   385       | n => rots(n, assoc_right th)
   386   end;
   387 
   388 (*Use "theorem naming" to label the clauses*)
   389 fun name_thms label =
   390     let fun name1 (th, (k,ths)) =
   391 	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   392 
   393     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
   394 
   395 (*Is the given disjunction an all-negative support clause?*)
   396 fun is_negative th = forall (not o #1) (literals (prop_of th));
   397 
   398 val neg_clauses = List.filter is_negative;
   399 
   400 
   401 (***** MESON PROOF PROCEDURE *****)
   402 
   403 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
   404 	   As) = rhyps(phi, A::As)
   405   | rhyps (_, As) = As;
   406 
   407 (** Detecting repeated assumptions in a subgoal **)
   408 
   409 (*The stringtree detects repeated assumptions.*)
   410 fun ins_term (net,t) = Net.insert_term (op aconv) (t,t) net;
   411 
   412 (*detects repetitions in a list of terms*)
   413 fun has_reps [] = false
   414   | has_reps [_] = false
   415   | has_reps [t,u] = (t aconv u)
   416   | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
   417 		  handle Net.INSERT => true;
   418 
   419 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   420 fun TRYING_eq_assume_tac 0 st = Seq.single st
   421   | TRYING_eq_assume_tac i st =
   422        TRYING_eq_assume_tac (i-1) (eq_assumption i st)
   423        handle THM _ => TRYING_eq_assume_tac (i-1) st;
   424 
   425 fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
   426 
   427 (*Loop checking: FAIL if trying to prove the same thing twice
   428   -- if *ANY* subgoal has repeated literals*)
   429 fun check_tac st =
   430   if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   431   then  Seq.empty  else  Seq.single st;
   432 
   433 
   434 (* net_resolve_tac actually made it slower... *)
   435 fun prolog_step_tac horns i =
   436     (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   437     TRYALL_eq_assume_tac;
   438 
   439 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   440 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   441 
   442 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
   443 
   444 
   445 (*Negation Normal Form*)
   446 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   447                not_impD, not_iffD, not_allD, not_exD, not_notD];
   448 
   449 fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
   450   | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
   451   | ok4nnf _ = false;
   452 
   453 fun make_nnf1 th = 
   454   if ok4nnf (concl_of th) 
   455   then make_nnf1 (tryres(th, nnf_rls))
   456     handle THM _ =>
   457         forward_res make_nnf1
   458            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   459     handle THM _ => th
   460   else th;
   461 
   462 (*The simplification removes defined quantifiers and occurrences of True and False. 
   463   nnf_ss also includes the one-point simprocs,
   464   which are needed to avoid the various one-point theorems from generating junk clauses.*)
   465 val nnf_simps =
   466      [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, 
   467       if_False, if_cancel, if_eq_cancel, cases_simp];
   468 val nnf_extra_simps =
   469       thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
   470 
   471 val nnf_ss =
   472     HOL_basic_ss addsimps nnf_extra_simps 
   473                  addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
   474 
   475 fun make_nnf th = case prems_of th of
   476     [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
   477 	     |> simplify nnf_ss  
   478 	     |> make_nnf1
   479   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   480 
   481 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   482   clauses that arise from a subgoal.*)
   483 fun skolemize th =
   484   if not (has_conns ["Ex"] (prop_of th)) then th
   485   else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
   486                               disj_exD, disj_exD1, disj_exD2])))
   487     handle THM _ =>
   488         skolemize (forward_res skolemize
   489                    (tryres (th, [conj_forward, disj_forward, all_forward])))
   490     handle THM _ => forward_res skolemize (th RS ex_forward);
   491 
   492 
   493 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   494   The resulting clauses are HOL disjunctions.*)
   495 fun make_clauses ths =
   496     (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
   497 
   498 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   499 fun make_horns ths =
   500     name_thms "Horn#"
   501       (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
   502 
   503 (*Could simply use nprems_of, which would count remaining subgoals -- no
   504   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   505 
   506 fun best_prolog_tac sizef horns =
   507     BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   508 
   509 fun depth_prolog_tac horns =
   510     DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   511 
   512 (*Return all negative clauses, as possible goal clauses*)
   513 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   514 
   515 fun skolemize_prems_tac prems =
   516     cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
   517     REPEAT o (etac exE);
   518 
   519 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
   520 fun expand_defs_tac st =
   521   let val defs = filter (can dest_equals) (#hyps (crep_thm st))
   522   in  PRIMITIVE (LocalDefs.def_export false defs) st  end;
   523 
   524 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
   525 fun MESON cltac i st = 
   526   SELECT_GOAL
   527     (EVERY [rtac ccontr 1,
   528 	    METAHYPS (fn negs =>
   529 		      EVERY1 [skolemize_prems_tac negs,
   530 			      METAHYPS (cltac o make_clauses)]) 1,
   531             expand_defs_tac]) i st
   532   handle THM _ => no_tac st;	(*probably from make_meta_clause, not first-order*)		      
   533 
   534 (** Best-first search versions **)
   535 
   536 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
   537 fun best_meson_tac sizef =
   538   MESON (fn cls =>
   539          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   540                          (has_fewer_prems 1, sizef)
   541                          (prolog_step_tac (make_horns cls) 1));
   542 
   543 (*First, breaks the goal into independent units*)
   544 val safe_best_meson_tac =
   545      SELECT_GOAL (TRY Safe_tac THEN
   546                   TRYALL (best_meson_tac size_of_subgoals));
   547 
   548 (** Depth-first search version **)
   549 
   550 val depth_meson_tac =
   551      MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
   552                              depth_prolog_tac (make_horns cls)]);
   553 
   554 
   555 (** Iterative deepening version **)
   556 
   557 (*This version does only one inference per call;
   558   having only one eq_assume_tac speeds it up!*)
   559 fun prolog_step_tac' horns =
   560     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   561             take_prefix Thm.no_prems horns
   562         val nrtac = net_resolve_tac horns
   563     in  fn i => eq_assume_tac i ORELSE
   564                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   565                 ((assume_tac i APPEND nrtac i) THEN check_tac)
   566     end;
   567 
   568 fun iter_deepen_prolog_tac horns =
   569     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   570 
   571 fun iter_deepen_meson_tac ths = MESON 
   572  (fn cls =>
   573       case (gocls (cls@ths)) of
   574 	   [] => no_tac  (*no goal clauses*)
   575 	 | goes => 
   576 	     let val horns = make_horns (cls@ths)
   577 	         val _ = if !Output.show_debug_msgs 
   578 	                 then Output.debug ("meson method called:\n" ^ 
   579 	     	                  space_implode "\n" (map string_of_thm (cls@ths)) ^ 
   580 	     	                  "\nclauses:\n" ^ 
   581 	     	                  space_implode "\n" (map string_of_thm horns))
   582 	     	         else ()
   583 	     in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
   584 	     end
   585  );
   586 
   587 fun meson_claset_tac ths cs =
   588   SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
   589 
   590 val meson_tac = CLASET' (meson_claset_tac []);
   591 
   592 
   593 (**** Code to support ordinary resolution, rather than Model Elimination ****)
   594 
   595 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
   596   with no contrapositives, for ordinary resolution.*)
   597 
   598 (*Rules to convert the head literal into a negated assumption. If the head
   599   literal is already negated, then using notEfalse instead of notEfalse'
   600   prevents a double negation.*)
   601 val notEfalse = read_instantiate [("R","False")] notE;
   602 val notEfalse' = rotate_prems 1 notEfalse;
   603 
   604 fun negated_asm_of_head th = 
   605     th RS notEfalse handle THM _ => th RS notEfalse';
   606 
   607 (*Converting one clause*)
   608 fun make_meta_clause th = 
   609   negated_asm_of_head (make_horn resolution_clause_rules th);
   610   
   611 fun make_meta_clauses ths =
   612     name_thms "MClause#"
   613       (distinct Drule.eq_thm_prop (map make_meta_clause ths));
   614 
   615 (*Permute a rule's premises to move the i-th premise to the last position.*)
   616 fun make_last i th =
   617   let val n = nprems_of th 
   618   in  if 1 <= i andalso i <= n 
   619       then Thm.permute_prems (i-1) 1 th
   620       else raise THM("select_literal", i, [th])
   621   end;
   622 
   623 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   624   double-negations.*)
   625 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   626 
   627 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   628 fun select_literal i cl = negate_head (make_last i cl);
   629 
   630 
   631 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   632   expressed as a tactic (or Isar method).  Each assumption of the selected 
   633   goal is converted to NNF and then its existential quantifiers are pulled
   634   to the front. Finally, all existential quantifiers are eliminated, 
   635   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   636   might generate many subgoals.*)
   637 
   638 fun skolemize_tac i st = 
   639   let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
   640   in 
   641      EVERY' [METAHYPS
   642 	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
   643                          THEN REPEAT (etac exE 1))),
   644             REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
   645   end
   646   handle Subscript => Seq.empty;
   647 
   648 (*Top-level conversion to meta-level clauses. Each clause has  
   649   leading !!-bound universal variables, to express generality. To get 
   650   disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
   651 val make_clauses_tac = 
   652   SUBGOAL
   653     (fn (prop,_) =>
   654      let val ts = Logic.strip_assums_hyp prop
   655      in EVERY1 
   656 	 [METAHYPS
   657 	    (fn hyps => 
   658               (Method.insert_tac
   659                 (map forall_intr_vars 
   660                   (make_meta_clauses (make_clauses hyps))) 1)),
   661 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   662      end);
   663      
   664      
   665 (*** setup the special skoklemization methods ***)
   666 
   667 (*No CHANGED_PROP here, since these always appear in the preamble*)
   668 
   669 val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
   670 
   671 val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
   672 
   673 val skolemize_setup =
   674   Method.add_methods
   675     [("skolemize", Method.no_args skolemize_meth, 
   676       "Skolemization into existential quantifiers"),
   677      ("make_clauses", Method.no_args make_clauses_meth, 
   678       "Conversion to !!-quantified meta-level clauses")];
   679 
   680 end;
   681 
   682 structure BasicMeson: BASIC_MESON = Meson;
   683 open BasicMeson;