Fix bug in ABS_TAC when free and bound names clashed

Closes #1420

help/Docfiles/Tactic.ABS_TAC.doc

@@ -15,11 +15,12 @@ Tactic
 tactic.
 
 \DESCRIBE
-When applied to a goal of the form {A ?- (\x. f x) = (\y. g u)}, the tactic {ABS_TAC}
-strips away the lambda abstractions:
+When applied to a goal of the form {A ?- (\x. M) = (\y. N)} (where {M}
+and {N} may or may not mention their respective bound variables), the
+tactic {ABS_TAC} strips away the lambda abstractions:
 {
     A ?- (\x. f x) = (\y. g y)
-   ===========================  ABS_TAC
+   ============================  ABS_TAC
             A ?- f x = g x
 }
 
@@ -28,6 +29,11 @@ strips away the lambda abstractions:
 Fails unless the goal has the above form, namely an equation both sides of
 which consist of a lamdba abstraction.
 
+\COMMENT
+When the lambda abstractions' bound variables conflict with existing
+free variables in the goal, variants of those names may occur in the
+goal that results.
+
 \SEEALSO
 Tactic.AP_TERM_TAC, Tactic.AP_THM_TAC.
 \ENDDOC

src/1/Tactic.sml

@@ -713,15 +713,17 @@ end
 
 val BINOP_TAC = MK_COMB_TAC THENL [AP_TERM_TAC, ALL_TAC]
 
-(*---------------------------------------------------------------------------*
- * ABS_TAC: inverts the ABS inference rule.                                  *
- *                                                                           *
- *   \x. f x = \x. g x                                                       *
- * =====================                                                     *
- *       f x = g x                                                           *
- *                                                                           *
- * Added: TT 2009.12.23                                                      *
- *---------------------------------------------------------------------------*)
+(* ----------------------------------------------------------------------
+    ABS_TAC: inverts the ABS inference rule.
+
+       G ?-  (\x. M) = (\y. N)
+      ========================== (x and y may or may not appear in M, N)
+       G ?-  M[x:=v] = N[y:=v]
+
+    v chosen to be x, y, or some variant as necessary to avoid clashing
+    with existing free variables.
+
+   ---------------------------------------------------------------------- *)
 
 local
    fun ER s = ERR "ABS_TAC" s
@@ -731,12 +733,21 @@ in
          val (lhs, rhs) = with_exn dest_eq gl (ER "not an equation")
          val (x, g) = with_exn dest_abs lhs (ER "lhs not an abstraction")
          val (y, f) = with_exn dest_abs rhs (ER "rhs not an abstraction")
-         val f_thm = if aconv x y then REFL rhs else ALPHA_CONV x rhs
-         val (_, f') = dest_abs (rand (concl f_thm))
+         val avoids = FVL (gl::asl) empty_tmset
+         val var_to_use =
+             if HOLset.member(avoids, x) then
+               if HOLset.member(avoids, y) then
+                 variant (HOLset.listItems avoids) x
+               else y
+             else x
+         val (dty,rty) = dom_rng (type_of lhs)
+         val funeq_rwt = FUN_EQ_THM
+                           |> INST_TYPE [alpha |-> dty, beta |-> rty]
+                           |> SPECL [lhs, rhs]
       in
-         ([(asl, mk_eq (g, f'))],
-          CONV_RULE (RHS_CONV (K (GSYM f_thm))) o ABS x o Lib.trye hd)
-      end
+        CONV_TAC (K funeq_rwt) THEN X_GEN_TAC var_to_use THEN
+        CONV_TAC (BINOP_CONV BETA_CONV)
+      end (asl,gl)
 end
 
 (*---------------------------------------------------------------------------*

src/1/selftest.sml

@@ -3,6 +3,17 @@ open HolKernel Parse boolTheory boolLib
 open testutils
 val _ = set_trace "Unicode" 0
 
+val goal_compare = pair_compare(list_compare Term.compare, Term.compare)
+val goals_compare = list_compare goal_compare
+fun goals_eq gs1 gs2 = goals_compare (gs1, gs2) = EQUAL
+
+fun listp p xs = "[" ^ String.concatWith ", " (map p xs) ^ "]"
+fun pairp (p1, p2) (x,y) = "(" ^ p1 x ^ ", " ^ p2 y ^ ")"
+
+val goal_toString =
+    pairp (listp term_to_string, term_to_string)
+val goals_toString = listp goal_toString
+
 val _ = tprint "Preterm free variables 1"
 val _ = require (check_result null) (Preterm.ptfvs o Parse.Preterm) ‘\x. x’
 
@@ -1369,3 +1380,15 @@ in
     ThmAttribute.extract_attributes
     "foo[A1=v1  v3,*]"
 end
+
+val _ = let
+  val _ = tprint "ABS_TAC with name conflation"
+  val t = “(\a:bool. T = T) = (\b. (a:bool) = a)”
+  val expected = [([], “(T = T) = (a = a:bool)”)]
+in
+  require_msg
+    (check_result (goals_eq expected o fst))
+    (goals_toString o fst)
+    (VALID ABS_TAC)
+    ([], t)
+end