Email Gateway (Aug 19 2022 at 16:01): Email Gateway (Aug 19 2022 at 16:01):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I need a tactic that turns something like P a b c ==> Q a b c into ALL a b c. P a b c --> Q a b c.
How do I do this?
Manuel
Email Gateway (Aug 19 2022 at 16:01):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Manuel,
I don't know whether this is exactly what you want, but perhaps the following snippet is of help:
consts P :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
consts Q :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
axiomatization where foo: "P a b c ⟹ Q a b c"
ML {*
fun transform ctxt thm =
let
val thm' = forall_intr_vars thm
val meta_eq = Object_Logic.atomize ctxt (cprop_of thm')
in
Raw_Simplifier.rewrite_rule ctxt [meta_eq] thm'
end
val new_thm = transform @{context} @{thm foo}
*}
Best,
René
Email Gateway (Aug 19 2022 at 16:01):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
apparently not. My lemma looks like this:
lemma "x ≥ (0::real) ⟹ x*x ≥ 0"
I would now like to apply some tactic to rewrite this to "∀x. x ≥
(0::real) ⟶ x*x ≥ 0".
For some odd reason, your code seems to loop indefinitely on this
example when I try to turn it into a tactic.
Manuel
Email Gateway (Aug 19 2022 at 16:02):From: Lars Noschinski <noschinl@in.tum.de>
There is forall_intr_list (in Drule), which turns free variables into
meta-quantified variables. The tactic Object_Logic.full_atomize_tac will
replace meta implication by object logic implication (and probably other
stuff, too).
-- Lars
Last updated: Nov 21 2024 at 12:39 UTC