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?

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

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: Dec 21 2024 at 16:20 UTC