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