Added HINT_EXISTS_TAC.

help/Docfiles/Tactic.HINT_EXISTS_TAC.doc

@@ -0,0 +1,65 @@
+\DOC HINT_EXISTS_TAC.doc
+
+\TYPE {HINT_EXISTS_TAC : tactic}
+
+
+\SYNOPSIS
+Reduces an existentially quantified goal by finding a witness which, from the
+assumption list, satisfies at least partially the body of the existential.
+
+\DESCRIBE
+When applied to a goal {?x. t1 /\ ... /\ tn}, the tactic {HINT_EXISTS_TAC}
+looks for an assumption of the form {ti[u/x]}, where {i} belongs to {1..n},
+and reduces the goal by taking {u} as a witness for {x}.
+
+\FAILURE
+Fails unless the goal contains an assumption of the expected form.
+
+\EXAMPLE
+- The goal:
+{
+   b = 0, a < 1, c > 0 ?- ?x. x < 1
+}
+is turned by {HINT_EXISTS_TAC} into:
+{
+   b = 0, a < 1, c > 0 ?- a < 1
+}
+
+- However the tactic also allows to make progress if only one conjunct of the
+  existential is satisfied. For instance, the goal:
+{
+   b = 0, a < 1, c > 0 ?- ?x. x < 1 /\ x + x = c
+}
+is turned by {HINT_EXISTS_TAC} into:
+{
+   b = 0, a < 1, c > 0 ?- a < 1 /\ a + a = c
+}
+
+- The location of the conjunct does not matter, the goal:
+{
+   b = 0, a < 1, c > 0 ?- ?x. x + x = c /\ x < 1
+}
+is turned by {HINT_EXISTS_TAC} into:
+{
+   b = 0, a < 1, c > 0 ?- a + a = c /\ a < 1
+}
+
+- It can be convenient to chain the call to {HINT_EXISTS_TAC} with one to
+  {ASM_REWRITE_TAC} in order to remove automatically the satisfied conjunct:
+{
+   b = 0, a < 1, c > 0 ?- ?x. x + x = c /\ x < 1
+}
+is turned by {HINT_EXISTS_TAC THEN ASM_REWRITE_TAC[]} into:
+{
+   b = 0, a < 1, c > 0 ?- a + a = c
+}
+
+\USES
+Avoid providing a witness explicitly, in order to make the tactic script less
+fragile.
+
+
+\SEEALSO Tactic.EXISTS_TAC.
+
+
+\ENDDOC

src/1/Tactic.sig

@@ -73,4 +73,5 @@ sig
   val DEEP_INTRO_TAC        : thm -> tactic
 
   val SELECT_ELIM_TAC       : tactic
+  val HINT_EXISTS_TAC       : tactic
 end;

src/1/Tactic.sml

@@ -999,4 +999,29 @@ fun DEEP_INTRO_TAC th = DEEP_INTROk_TAC th ALL_TAC
 
 val SELECT_ELIM_TAC = DEEP_INTRO_TAC SELECT_ELIM_THM
 
+
+(*----------------------------------------------------------------------*
+ *  HINT_EXISTS_TAC                                                     *
+ *    instantiates an existential by using hints from the assumptions.  *
+ *----------------------------------------------------------------------*)
+
+fun HINT_EXISTS_TAC g =
+  let
+    val (hs,c) = g
+    val (v,c') = dest_exists c
+    val (vs,c') = strip_exists c'
+    fun hyp_match c h =
+      if exists (C mem vs) (free_vars c) then fail () else match_term c h
+    val (subs,_) = tryfind (C tryfind hs o hyp_match) (strip_conj c')
+    val witness =
+      case subs of
+         [] => v
+        |[{redex = u, residue = t}] =>
+            if u = v then t else failwith "HINT_EXISTS_TAC not applicable"
+        |_ => failwith "HINT_EXISTS_TAC not applicable"
+  in
+    EXISTS_TAC witness g
+  end;
+
+
 end (* Tactic *)