Email Gateway (Aug 19 2022 at 14:50): Email Gateway (Aug 19 2022 at 14:50):From: Peter Lammich <lammich@in.tum.de>
Hi,
I stumbled over the following (unexpected, undocumented) behaviour of
the lemmas command:
thm norm_hhf_eq
(* (PROP ?phi ==> (!!x. PROP ?psi x))
== (!!x. PROP ?phi ==> PROP ?psi x) *)
lemmas foo = norm_hhf_eq
(* lemma foo: (!!x. PROP ?phi ==> PROP ?psi x)
== (!!x. PROP ?phi ==> PROP ?psi x) *)
So, obviously, there is some normalization going on. What normalization
is exactly applied?
The isar-ref manual says:
"Results are standardized before being stored, i.e. schematic
variables are renamed to enforce index 0 uniformly."
but nothing about other normalizations.
Is there a way, other than raw isabelle-ML declaration, to avoid this
normalization and just give a name to a list of theorems?
Email Gateway (Aug 19 2022 at 14:50):From: Peter Lammich <lammich@in.tum.de>
Addition: Local_Theory.notes already performs this normalization,
so I am unable to give another name to this theorem at all!
Email Gateway (Aug 19 2022 at 14:51):From: Makarius <makarius@sketis.net>
On Fri, 11 Jul 2014, Peter Lammich wrote:
I stumbled over the following (unexpected, undocumented) behaviour of
the lemmas command:
I am surprised that the normal Isabelle rule normalization is unexpected.
It is documented in many places, e.g. the "implementation" manual section
2.4 Object-level rules.
Is there a way, other than raw isabelle-ML declaration, to avoid this
normalization and just give a name to a list of theorems?
There are some tricks with the "prop" marker to protect Pure propositions
(covered in the same manual). This is for unusual situations where this
is really needed.
Normally it is better to work with the system and its canonical rule
format, not against it.
Makarius
Last updated: Apr 16 2024 at 08:18 UTC