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