src/HOL/Tools/meson.ML
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 15700 970e0293dfb3
child 15736 1bb0399a9517
permissions -rw-r--r--
*** empty log message ***
     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_nnf		: thm -> thm
    18   val skolemize		: thm -> thm
    19   val make_clauses	: thm list -> thm list
    20   val make_horns	: thm list -> thm list
    21   val best_prolog_tac	: (thm -> int) -> thm list -> tactic
    22   val depth_prolog_tac	: thm list -> tactic
    23   val gocls		: thm list -> thm list
    24   val skolemize_prems_tac	: thm list -> int -> tactic
    25   val MESON		: (thm list -> tactic) -> int -> tactic
    26   val best_meson_tac	: (thm -> int) -> int -> tactic
    27   val safe_best_meson_tac	: int -> tactic
    28   val depth_meson_tac	: int -> tactic
    29   val prolog_step_tac'	: thm list -> int -> tactic
    30   val iter_deepen_prolog_tac	: thm list -> tactic
    31   val iter_deepen_meson_tac	: int -> tactic
    32   val meson_tac		: int -> tactic
    33   val negate_head	: thm -> thm
    34   val select_literal	: int -> thm -> thm
    35   val skolemize_tac	: int -> tactic
    36   val make_clauses_tac	: int -> tactic
    37   val meson_setup	: (theory -> theory) list
    38 end
    39 
    40 
    41 structure Meson =
    42 struct
    43 
    44 val not_conjD = thm "meson_not_conjD";
    45 val not_disjD = thm "meson_not_disjD";
    46 val not_notD = thm "meson_not_notD";
    47 val not_allD = thm "meson_not_allD";
    48 val not_exD = thm "meson_not_exD";
    49 val imp_to_disjD = thm "meson_imp_to_disjD";
    50 val not_impD = thm "meson_not_impD";
    51 val iff_to_disjD = thm "meson_iff_to_disjD";
    52 val not_iffD = thm "meson_not_iffD";
    53 val conj_exD1 = thm "meson_conj_exD1";
    54 val conj_exD2 = thm "meson_conj_exD2";
    55 val disj_exD = thm "meson_disj_exD";
    56 val disj_exD1 = thm "meson_disj_exD1";
    57 val disj_exD2 = thm "meson_disj_exD2";
    58 val disj_assoc = thm "meson_disj_assoc";
    59 val disj_comm = thm "meson_disj_comm";
    60 val disj_FalseD1 = thm "meson_disj_FalseD1";
    61 val disj_FalseD2 = thm "meson_disj_FalseD2";
    62 
    63 
    64 (**** Operators for forward proof ****)
    65 
    66 (*raises exception if no rules apply -- unlike RL*)
    67 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    68   | tryres (th, []) = raise THM("tryres", 0, [th]);
    69 
    70 (*Permits forward proof from rules that discharge assumptions*)
    71 fun forward_res nf st =
    72   case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
    73   of SOME(th,_) => th
    74    | NONE => raise THM("forward_res", 0, [st]);
    75 
    76 
    77 (*Are any of the constants in "bs" present in the term?*)
    78 fun has_consts bs =
    79   let fun has (Const(a,_)) = a mem bs
    80 	| has (Const ("Hilbert_Choice.Eps",_) $ _) = false
    81 		     (*ignore constants within @-terms*)
    82 	| has (f$u) = has f orelse has u
    83 	| has (Abs(_,_,t)) = has t
    84 	| has _ = false
    85   in  has  end;
    86 
    87 (* for tracing statements *)
    88  
    89 fun concat_with_and [] str = str
    90 |   concat_with_and (x::[]) str = str^" ("^x^")"
    91 |   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
    92 
    93 
    94 
    95 (**** Clause handling ****)
    96 
    97 fun literals (Const("Trueprop",_) $ P) = literals P
    98   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
    99   | literals (Const("Not",_) $ P) = [(false,P)]
   100   | literals P = [(true,P)];
   101 
   102 (*number of literals in a term*)
   103 val nliterals = length o literals;
   104 
   105 (*to detect, and remove, tautologous clauses*)
   106 fun taut_lits [] = false
   107   | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts;
   108 
   109 (*Include False as a literal: an occurrence of ~False is a tautology*)
   110 fun is_taut th = taut_lits ((true, HOLogic.false_const) ::
   111 			    literals (prop_of th));
   112 
   113 (*Generation of unique names -- maxidx cannot be relied upon to increase!
   114   Cannot rely on "variant", since variables might coincide when literals
   115   are joined to make a clause...
   116   19 chooses "U" as the first variable name*)
   117 val name_ref = ref 19;
   118 
   119 (*Replaces universally quantified variables by FREE variables -- because
   120   assumptions may not contain scheme variables.  Later, call "generalize". *)
   121 fun freeze_spec th =
   122   let val sth = th RS spec
   123       val newname = (name_ref := !name_ref + 1;
   124 		     radixstring(26, "A", !name_ref))
   125   in  read_instantiate [("x", newname)] sth  end;
   126 
   127 fun resop nf [prem] = resolve_tac (nf prem) 1;
   128 
   129 (*Conjunctive normal form, detecting tautologies early.
   130   Strips universal quantifiers and breaks up conjunctions. *)
   131 fun cnf_aux seen (th,ths) =
   132  let val _= (warning ("in cnf_aux, th : "^(string_of_thm th)))
   133  in if taut_lits (literals(prop_of th) @ seen)  
   134   then ths     (*tautology ignored*)
   135   else if not (has_consts ["All","op &"] (prop_of th))  
   136   then th::ths (*no work to do, terminate*)
   137   else (*conjunction?*)
   138 	cnf_aux seen (th RS conjunct1,
   139 		      cnf_aux seen (th RS conjunct2, ths))
   140   handle THM _ => (*universal quant?*)
   141 	cnf_aux  seen (freeze_spec th,  ths)
   142   handle THM _ => (*disjunction?*)
   143     let val tac =
   144 	(METAHYPS (resop (cnf_nil seen)) 1) THEN
   145 	(fn st' => st' |>
   146 		METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
   147     in  Seq.list_of (tac (th RS disj_forward)) @ ths  end end
   148 and cnf_nil seen th = ((warning ("in cnf_nil "));cnf_aux seen (th,[]))
   149 
   150 (*Top-level call to cnf -- it's safe to reset name_ref*)
   151 fun cnf (th,ths) =
   152    (name_ref := 19;  cnf (th RS conjunct1, cnf (th RS conjunct2, ths))
   153     handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths));
   154 
   155 (**** Removal of duplicate literals ****)
   156 
   157 (*Forward proof, passing extra assumptions as theorems to the tactic*)
   158 fun forward_res2 nf hyps st =
   159   case Seq.pull
   160 	(REPEAT
   161 	 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   162 	 st)
   163   of SOME(th,_) => th
   164    | NONE => raise THM("forward_res2", 0, [st]);
   165 
   166 (*Remove duplicates in P|Q by assuming ~P in Q
   167   rls (initially []) accumulates assumptions of the form P==>False*)
   168 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
   169     handle THM _ => tryres(th,rls)
   170     handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
   171 			   [disj_FalseD1, disj_FalseD2, asm_rl])
   172     handle THM _ => th;
   173 
   174 (*Remove duplicate literals, if there are any*)
   175 fun nodups th =
   176     if null(findrep(literals(prop_of th))) then th
   177     else nodups_aux [] th;
   178 
   179 
   180 (**** Generation of contrapositives ****)
   181 
   182 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   183 fun assoc_right th = assoc_right (th RS disj_assoc)
   184 	handle THM _ => th;
   185 
   186 (*Must check for negative literal first!*)
   187 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
   188 
   189 (*For ordinary resolution. *)
   190 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
   191 
   192 (*Create a goal or support clause, conclusing False*)
   193 fun make_goal th =   (*Must check for negative literal first!*)
   194     make_goal (tryres(th, clause_rules))
   195   handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
   196 
   197 (*Sort clauses by number of literals*)
   198 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
   199 
   200 (*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*)
   201 fun sort_clauses ths = sort (make_ord fewerlits) (List.filter (not o is_taut) ths);
   202 
   203 (*Convert all suitable free variables to schematic variables*)
   204 fun generalize th = forall_elim_vars 0 (forall_intr_frees th);
   205 
   206 (*True if the given type contains bool anywhere*)
   207 fun has_bool (Type("bool",_)) = true
   208   | has_bool (Type(_, Ts)) = exists has_bool Ts
   209   | has_bool _ = false;
   210   
   211 (*Is the string the name of a connective? It doesn't matter if this list is
   212   incomplete, since when actually called, the only connectives likely to
   213   remain are & | Not.*)  
   214 fun is_conn c = c mem_string
   215     ["Trueprop", "op &", "op |", "op -->", "op =", "Not", 
   216      "All", "Ex", "Ball", "Bex"];
   217 
   218 (*True if the term contains a function where the type of any argument contains
   219   bool.*)
   220 val has_bool_arg_const = 
   221     exists_Const
   222       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
   223   
   224 (*Raises an exception if any Vars in the theorem mention type bool. That would mean
   225   they are higher-order, and in addition, they could cause make_horn to loop!
   226   Functions taking Boolean arguments are also rejected.*)
   227 fun check_no_bool th =
   228   let val {prop,...} = rep_thm th
   229   in if exists (has_bool o fastype_of) (term_vars prop) orelse
   230         has_bool_arg_const prop
   231   then raise THM ("check_no_bool", 0, [th]) else th
   232   end;
   233 
   234 (*Create a meta-level Horn clause*)
   235 fun make_horn crules th = make_horn crules (tryres(th,crules))
   236 			  handle THM _ => th;
   237 
   238 (*Generate Horn clauses for all contrapositives of a clause*)
   239 fun add_contras crules (th,hcs) =
   240   let fun rots (0,th) = hcs
   241 	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
   242 			rots(k-1, assoc_right (th RS disj_comm))
   243   in case nliterals(prop_of (check_no_bool th)) of
   244 	1 => th::hcs
   245       | n => rots(n, assoc_right th)
   246   end;
   247 
   248 (*Use "theorem naming" to label the clauses*)
   249 fun name_thms label =
   250     let fun name1 (th, (k,ths)) =
   251 	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   252 
   253     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
   254 
   255 (*Find an all-negative support clause*)
   256 fun is_negative th = forall (not o #1) (literals (prop_of th));
   257 
   258 val neg_clauses = List.filter is_negative;
   259 
   260 
   261 (***** MESON PROOF PROCEDURE *****)
   262 
   263 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
   264 	   As) = rhyps(phi, A::As)
   265   | rhyps (_, As) = As;
   266 
   267 (** Detecting repeated assumptions in a subgoal **)
   268 
   269 (*The stringtree detects repeated assumptions.*)
   270 fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv);
   271 
   272 (*detects repetitions in a list of terms*)
   273 fun has_reps [] = false
   274   | has_reps [_] = false
   275   | has_reps [t,u] = (t aconv u)
   276   | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
   277 		  handle INSERT => true;
   278 
   279 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   280 fun TRYALL_eq_assume_tac 0 st = Seq.single st
   281   | TRYALL_eq_assume_tac i st =
   282        TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
   283        handle THM _ => TRYALL_eq_assume_tac (i-1) st;
   284 
   285 (*Loop checking: FAIL if trying to prove the same thing twice
   286   -- if *ANY* subgoal has repeated literals*)
   287 fun check_tac st =
   288   if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   289   then  Seq.empty  else  Seq.single st;
   290 
   291 
   292 (* net_resolve_tac actually made it slower... *)
   293 fun prolog_step_tac horns i =
   294     (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   295     TRYALL eq_assume_tac;
   296 
   297 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   298 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   299 
   300 fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
   301 
   302 
   303 (*Negation Normal Form*)
   304 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   305                not_impD, not_iffD, not_allD, not_exD, not_notD];
   306 
   307 fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
   308     handle THM _ =>
   309         forward_res make_nnf1
   310            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   311     handle THM _ => th;
   312 
   313 fun make_nnf th = make_nnf1 (check_no_bool th);
   314 
   315 (*Pull existential quantifiers (Skolemization)*)
   316 fun skolemize th =
   317   if not (has_consts ["Ex"] (prop_of th)) then th
   318   else ((warning("in meson.skolemize with th: "^(string_of_thm th)));skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
   319                               disj_exD, disj_exD1, disj_exD2])))
   320     handle THM _ =>
   321         skolemize (forward_res skolemize
   322                    (tryres (th, [conj_forward, disj_forward, all_forward])))
   323     handle THM _ => forward_res skolemize (th RS ex_forward);
   324 
   325 
   326 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   327   The resulting clauses are HOL disjunctions.*)
   328 fun make_clauses ths =
   329    ( (warning("in make_clauses ths are:"^(concat_with_and (map string_of_thm ths) ""))); sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
   330 
   331 (*Convert a list of clauses to (contrapositive) Horn clauses*)
   332 fun make_horns ths =
   333     name_thms "Horn#"
   334       (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
   335 
   336 (*Could simply use nprems_of, which would count remaining subgoals -- no
   337   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   338 
   339 fun best_prolog_tac sizef horns =
   340     BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   341 
   342 fun depth_prolog_tac horns =
   343     DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   344 
   345 (*Return all negative clauses, as possible goal clauses*)
   346 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   347 
   348 
   349 fun skolemize_prems_tac prems =
   350     cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
   351     REPEAT o (etac exE);
   352 
   353 (*Shell of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
   354 fun MESON cltac = SELECT_GOAL
   355  (EVERY1 [rtac ccontr,
   356           METAHYPS (fn negs =>
   357                     EVERY1 [skolemize_prems_tac negs,
   358                             METAHYPS (cltac o make_clauses)])]);
   359 
   360 (** Best-first search versions **)
   361 
   362 fun best_meson_tac sizef =
   363   MESON (fn cls =>
   364          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   365                          (has_fewer_prems 1, sizef)
   366                          (prolog_step_tac (make_horns cls) 1));
   367 
   368 (*First, breaks the goal into independent units*)
   369 val safe_best_meson_tac =
   370      SELECT_GOAL (TRY Safe_tac THEN
   371                   TRYALL (best_meson_tac size_of_subgoals));
   372 
   373 (** Depth-first search version **)
   374 
   375 val depth_meson_tac =
   376      MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
   377                              depth_prolog_tac (make_horns cls)]);
   378 
   379 
   380 
   381 (** Iterative deepening version **)
   382 
   383 (*This version does only one inference per call;
   384   having only one eq_assume_tac speeds it up!*)
   385 fun prolog_step_tac' horns =
   386     let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
   387             take_prefix Thm.no_prems horns
   388         val nrtac = net_resolve_tac horns
   389     in  fn i => eq_assume_tac i ORELSE
   390                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   391                 ((assume_tac i APPEND nrtac i) THEN check_tac)
   392     end;
   393 
   394 fun iter_deepen_prolog_tac horns =
   395     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   396 
   397 val iter_deepen_meson_tac =
   398   MESON (fn cls =>
   399          (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
   400                            (has_fewer_prems 1)
   401                            (prolog_step_tac' (make_horns cls))));
   402 
   403 fun meson_claset_tac cs =
   404   SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac);
   405 
   406 val meson_tac = CLASET' meson_claset_tac;
   407 
   408 
   409 (**** Code to support ordinary resolution, rather than Model Elimination ****)
   410 
   411 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
   412   with no contrapositives, for ordinary resolution.*)
   413 
   414 (*Rules to convert the head literal into a negated assumption. If the head
   415   literal is already negated, then using notEfalse instead of notEfalse'
   416   prevents a double negation.*)
   417 val notEfalse = read_instantiate [("R","False")] notE;
   418 val notEfalse' = rotate_prems 1 notEfalse;
   419 
   420 fun negated_asm_of_head th = 
   421     th RS notEfalse handle THM _ => th RS notEfalse';
   422 
   423 (*Converting one clause*)
   424 fun make_meta_clause th = 
   425 	negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th));
   426 
   427 fun make_meta_clauses ths =
   428     name_thms "MClause#"
   429       (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
   430 
   431 (*Permute a rule's premises to move the i-th premise to the last position.*)
   432 fun make_last i th =
   433   let val n = nprems_of th 
   434   in  if 1 <= i andalso i <= n 
   435       then Thm.permute_prems (i-1) 1 th
   436       else raise THM("select_literal", i, [th])
   437   end;
   438 
   439 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   440   double-negations.*)
   441 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   442 
   443 (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   444 fun select_literal i cl = negate_head (make_last i cl);
   445 
   446 (*Top-level Skolemization. Allows part of the conversion to clauses to be
   447   expressed as a tactic (or Isar method).  Each assumption of the selected 
   448   goal is converted to NNF and then its existential quantifiers are pulled
   449   to the front. Finally, all existential quantifiers are eliminated, 
   450   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   451   might generate many subgoals.*)
   452 val skolemize_tac = 
   453   SUBGOAL
   454     (fn (prop,_) =>
   455      let val ts = Logic.strip_assums_hyp prop
   456          val _ = (warning("in meson.skolemize_tac "))
   457          val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "skolem")))
   458          val _ = TextIO.output(outfile, "in skolemize_tac ");
   459          val _ = TextIO.flushOut outfile;
   460          val _ =  TextIO.closeOut outfile
   461      in EVERY1 
   462 	 [METAHYPS
   463 	    (fn hyps => ((warning("in meson.skolemize_tac hyps are: "^(string_of_thm (hd hyps))));cut_facts_tac (map (skolemize o make_nnf) hyps) 1
   464                          THEN REPEAT (etac exE 1))),
   465 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   466      end);
   467 
   468 (*Top-level conversion to meta-level clauses. Each clause has  
   469   leading !!-bound universal variables, to express generality. To get 
   470   disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
   471 val make_clauses_tac = 
   472   SUBGOAL
   473     (fn (prop,_) =>
   474      let val ts = Logic.strip_assums_hyp prop
   475      in EVERY1 
   476 	 [METAHYPS
   477 	    (fn hyps => 
   478               (Method.insert_tac
   479                 (map forall_intr_vars 
   480                   (make_meta_clauses (make_clauses hyps))) 1)),
   481 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   482      end);
   483 
   484 
   485 (*** proof method setup ***)
   486 
   487 fun meson_meth ctxt =
   488   Method.SIMPLE_METHOD' HEADGOAL
   489     (CHANGED_PROP o meson_claset_tac (local_claset_of ctxt));
   490 
   491 val skolemize_meth =
   492   Method.SIMPLE_METHOD' HEADGOAL
   493     (CHANGED_PROP o skolemize_tac);
   494 
   495 val make_clauses_meth =
   496   Method.SIMPLE_METHOD' HEADGOAL
   497     (CHANGED_PROP o make_clauses_tac);
   498 
   499 
   500 val meson_setup =
   501  [Method.add_methods
   502   [("meson", Method.ctxt_args meson_meth, 
   503     "The MESON resolution proof procedure"),
   504    ("skolemize", Method.no_args skolemize_meth, 
   505     "Skolemization into existential quantifiers"),
   506    ("make_clauses", Method.no_args make_clauses_meth, 
   507     "Conversion to !!-quantified meta-level clauses")]];
   508 
   509 end;
   510 
   511 structure BasicMeson: BASIC_MESON = Meson;
   512 open BasicMeson;