# HG changeset patch
# User paulson
# Date 826911756 -3600
# Node ID c44a012cf95056b173911c159c61e20ea1114d8e
# Parent  3d59c407bd36b2033afe1c3957f99f833ed40f12
New safe_meson_tac uses iterative deepening

diff -r 3d59c407bd36 -r c44a012cf950 src/HOL/ex/meson.ML
--- a/src/HOL/ex/meson.ML	Fri Mar 15 18:41:04 1996 +0100
+++ b/src/HOL/ex/meson.ML	Fri Mar 15 18:42:36 1996 +0100
@@ -203,12 +203,15 @@
 (*number of literals in a term*)
 val nliterals = length o literals;
 
-(*to delete tautologous clauses*)
+(*to detect, and remove, tautologous clauses*)
 fun taut_lits [] = false
   | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts;
 
-val is_taut = taut_lits o literals o prop_of;
+val term_False = term_of (read_cterm (sign_of HOL.thy) 
+			  ("False", Type("bool",[])));
 
+(*Include False as a literal: an occurrence of ~False is a tautology*)
+fun is_taut th = taut_lits ((true,term_False) :: literals (prop_of th));
 
 (*Generation of unique names -- maxidx cannot be relied upon to increase!
   Cannot rely on "variant", since variables might coincide when literals
@@ -293,6 +296,8 @@
 
 (*Must check for negative literal first!*)
 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
+
+(*For Plaisted's postive refinement.  [currently unused] *)
 val refined_clause_rules = [disj_assoc, make_refined_neg_rule, make_pos_rule];
 
 (*Create a goal or support clause, conclusing False*)
@@ -328,7 +333,8 @@
   end;
 
 (*Convert a list of clauses to (contrapositive) Horn clauses*)
-fun make_horns ths = foldr (add_contras clause_rules) (ths,[]);
+fun make_horns ths = 
+    gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[]));
 
 (*Find an all-negative support clause*)
 fun is_negative th = forall (not o #1) (literals (prop_of th));
@@ -354,16 +360,22 @@
   | has_reps ts = (foldl ins_term (Net.empty, ts);  false)
                   handle INSERT => true; 
 
+(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
+fun TRYALL_eq_assume_tac 0 st = Sequence.single st
+  | TRYALL_eq_assume_tac i st = TRYALL_eq_assume_tac (i-1) (eq_assumption i st)
+                                handle THM _ => TRYALL_eq_assume_tac (i-1) st;
+
 (*Loop checking: FAIL if trying to prove the same thing twice
-  -- repeated literals*)
-val check_tac = SUBGOAL (fn (prem,_) =>
-  if has_reps (rhyps(prem,[]))  then  no_tac  else  all_tac); 
+  -- if *ANY* subgoal has repeated literals*)
+fun check_tac st = 
+  if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
+  then  Sequence.null  else  Sequence.single st;
+
 
 (* net_resolve_tac actually made it slower... *)
 fun prolog_step_tac horns i = 
-    (assume_tac i APPEND resolve_tac horns i) THEN
-    (ALLGOALS check_tac) THEN
-    (TRYALL eq_assume_tac);
+    (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
+    TRYALL eq_assume_tac;
 
 
 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
@@ -395,20 +407,52 @@
                     EVERY1 [skolemize_tac negs,
                             METAHYPS (sko_tac o make_clauses)])]);
 
+(** Best-first search versions **)
+
 fun best_meson_tac sizef = 
   MESON (fn cls => 
-         resolve_tac (gocls cls) 1
-         THEN_BEST_FIRST 
-         (has_fewer_prems 1, sizef,
-          prolog_step_tac (make_horns cls) 1));
+         THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
+                         (has_fewer_prems 1, sizef)
+			 (prolog_step_tac (make_horns cls) 1));
 
 (*First, breaks the goal into independent units*)
-val safe_meson_tac =
+val safe_best_meson_tac =
      SELECT_GOAL (TRY (safe_tac HOL_cs) THEN 
                   TRYALL (best_meson_tac size_of_subgoals));
 
+(** Depth-first search version **)
+
 val depth_meson_tac =
      MESON (fn cls => EVERY [resolve_tac (gocls cls) 1, 
                              depth_prolog_tac (make_horns cls)]);
 
+
+
+(** Iterative deepening version **)
+
+(*This version does only one inference per call;
+  having only one eq_assume_tac speeds it up!*)
+fun prolog_step_tac' horns = 
+    let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
+            take_prefix (fn rl => nprems_of rl=0) horns
+        val nrtac = net_resolve_tac horns
+    in  fn i => eq_assume_tac i ORELSE
+                match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
+	        ((assume_tac i APPEND nrtac i) THEN check_tac)
+    end;
+
+fun iter_deepen_prolog_tac horns = 
+    ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
+
+val iter_deepen_meson_tac = 
+  MESON (fn cls => 
+         (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
+	                   (has_fewer_prems 1)
+	                   (prolog_step_tac' (make_horns cls))));
+
+val safe_meson_tac =
+     SELECT_GOAL (TRY (safe_tac HOL_cs) THEN 
+                  TRYALL (iter_deepen_meson_tac));
+
+
 writeln"Reached end of file.";