Patrick Nicodemus (Oct 29 2023 at 01:45): Patrick Nicodemus (Oct 29 2023 at 01:45):This code works fine:
theory Scratch2
imports Main
begin
locale endomap =
fixes T :: "'a ⇒ 'a"
(*assumes hyp : "T x = T x"*)
definition (in endomap) fixpt where
"fixpt f = (T f = f)"
theorem (in endomap) abc:
"endomap.fixpt T f ⟹ (T f = f)"
by (simp add: endomap.fixpt_def)
When I uncomment the assumption assumes hyp : "T x = T x" it breaks the proof at the end.
What's going on there?
Patrick Nicodemus (Oct 29 2023 at 01:46):I thought unfold_locales might have something to do with it but apprently not.
Patrick Nicodemus (Oct 29 2023 at 01:50):Huh, ok. I see now that removing the word "endomap" repairs the proof.
But why is the locale behavior that the choice of whether to use "assumes" or not affects the namespacing rules
Patrick Nicodemus (Oct 29 2023 at 02:13):I am starting to see what's going on, I think I need to spend more time learning about locales.
I see now that when you add an assumption hyp it changes the statement of the theorem fixpt_defwhich "guards" the definition of fixpt so that it's only applicable once you've proven that T is an instance of the endomap locale (satisfies the predicate)
Last updated: Apr 28 2024 at 12:28 UTC