Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Atomisation of free variables


view this post on Zulip 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

view this post on Zulip 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é

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 12:28 UTC