Jan van Brügge (Jan 22 2022 at 11:38): 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›)
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))))
Yes, there is only one context. Also apply assumption after the tactic solves the goal as expected
Last updated: Jul 15 2022 at 23:21 UTC