Given a goal like this:

```
⋀a x. f x ⟹ x = T a ⟹ Q
```

what is the best way to rewrite the premises to

```
⋀a. f (T a) ⟹ Q
```

? I could hack something together with `SUBPROOF`

but there has to be a better way

You could do this:

```
lemma a: "(⋀a x. f x ⟹ x = T a ⟹ PROP Q) ≡ (⋀a. f (T a) ⟹ PROP Q)"
proof
fix a assume "⋀a x. f x ⟹ x = T a ⟹ PROP Q" "f (T a)"
from this(1)[OF this(2), of a] show "PROP Q" by simp
next
fix a x assume "⋀a. f (T a) ⟹ PROP Q" "f x" "x = T a"
from this(1)[of a] this(2,3) show "PROP Q" by simp
qed
lemma "⋀a x. f x ⟹ x = T a ⟹ Q"
apply(tactic ‹CONVERSION (Conv.rewr_conv @{thm a}) 1›)
```

I don't know `f`

nor `T`

statically, so this won't work. I guess the `SUBPROOF`

hack it is

But this works for any f and T?

oh, yes of course, I am stupid

Weird, now I am at `⋀b3 z3. b3 = z3 ⟹ b3 = z3`

but `assume_tac`

fails

The types do match, right?

yes

all are `'c`

You can try printing the term literally without pretty-printing. Also the context you pass in is the right one?

```
Const ("Pure.all", "('c ⇒ prop) ⇒ prop") $
Abs ("b3", "'c",
Const ("Pure.all", "('c ⇒ prop) ⇒ prop") $
Abs ("z3", "'c",
Const ("Pure.imp", "prop ⇒ prop ⇒ prop") $
(Const ("HOL.Trueprop", "bool ⇒ prop") $ (Const ("HOL.eq", "'c ⇒ 'c ⇒ bool") $ Bound 1 $ Bound 0)) $
(Const ("HOL.Trueprop", "bool ⇒ prop") $
(Const ("HOL.eq", "'c ⇒ 'c ⇒ bool") $ Bound 1 $ Bound 0))))
```

Yes, there is only one context. Also `apply assumption`

after the tactic solves the goal as expected

I ended up using `SUBPROOF`

anyways, because it is easier to branch on the goal and then I can just use `Local_Defs.unfold0`

```
Subgoal.FOCUS (fn {context, prems = [p1, p2], ...} =>
if HOLogic.dest_Trueprop (Thm.prop_of p2) = @{term False} then
rtac ctxt @{thm FalseE} 1 THEN
rtac ctxt p2 1
else
resolve_tac ctxt F_wit_thms 1 THEN
rtac ctxt (unfold context [p2] p1) 1
) ctxt)
```

Jan van Brügge has marked this topic as resolved.

Just keep in mind that Subgoal.FOCUS is quite expensive in general

There is also hypsubst_tac that would work here if T does not depend on x.

Ah, yes that is the tactic that I originally wanted. Now without `Subgoal.FOCUS`

:

```
(
K (unfold_thms_tac ctxt @{thms False_implies_equals}) THEN'
rtac ctxt @{thm TrueI}
) ORELSE' (EVERY' [
hyp_subst_tac ctxt,
dresolve_tac ctxt F_wit_thms,
assume_tac ctxt
])
```

Is there an `unfold_thms_tac`

but restricted to only one subgoal?

SELECT_GOAL can be used to restrict a tactic to a subgoal

Last updated: Jun 20 2024 at 12:31 UTC