Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Convert an Isabelle term intro prenex normal form

Email Gateway (Aug 19 2022 at 16:37):

From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle experts,

I was wondering if there is a built-in Isabelle command to convert an
Isabelle term into prenex normal form or anyone has ever developed
similar procedures in Isabelle.

For example,

((!x::real. x*x>0) ∧ (?x::real. x=0))

should be able to be cast to something like

(?y::real. !x::real. x*x>0 ∧ y=0)

Many thanks,
Wenda

Last updated: Apr 27 2024 at 04:17 UTC