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