## Stream: Isabelle/ML

### Topic: ✔ combine premises in goal

#### Jan van Brügge (Jan 22 2022 at 11:38):

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

#### Lukas Stevens (Jan 22 2022 at 11:56):

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›)
``````

#### Jan van Brügge (Jan 22 2022 at 11:57):

I don't know `f` nor `T` statically, so this won't work. I guess the `SUBPROOF` hack it is

#### Lukas Stevens (Jan 22 2022 at 11:58):

But this works for any f and T?

#### Jan van Brügge (Jan 22 2022 at 11:58):

oh, yes of course, I am stupid

#### Jan van Brügge (Jan 22 2022 at 12:32):

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

#### Lukas Stevens (Jan 22 2022 at 12:34):

The types do match, right?

yes

#### Jan van Brügge (Jan 22 2022 at 12:34):

all are `'c`

#### Lukas Stevens (Jan 22 2022 at 12:47):

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

#### Jan van Brügge (Jan 22 2022 at 12:52):

``````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))))
``````

#### Jan van Brügge (Jan 22 2022 at 12:52):

Yes, there is only one context. Also `apply assumption` after the tactic solves the goal as expected

#### Jan van Brügge (Jan 22 2022 at 14:05):

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)
``````

#### Notification Bot (Jan 22 2022 at 14:05):

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

#### Lukas Stevens (Jan 22 2022 at 14:44):

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

#### Dmitriy Traytel (Jan 22 2022 at 17:16):

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

#### Jan van Brügge (Jan 23 2022 at 10:00):

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
])
``````

#### Jan van Brügge (Jan 23 2022 at 10:01):

Is there an `unfold_thms_tac` but restricted to only one subgoal?

#### Dmitriy Traytel (Jan 24 2022 at 07:59):

SELECT_GOAL can be used to restrict a tactic to a subgoal

Last updated: Jun 20 2024 at 12:31 UTC