Email Gateway (Aug 22 2022 at 20:27): Email Gateway (Aug 22 2022 at 20:27):From: "John F. Hughes" <jfh@cs.brown.edu>
I'm still trying to understand locales. Following
https://isabelle.in.tum.de/doc/locales.pdf, I defined the "partial order"
locale describe there, and followed step by step through the example; the
results I got had slightly different formatting in some cases, but were
otherwise reasonable.
I thought I could test it out on my own locales, which involve affine
planes. (I'm eager to show that the Euclidean plane is an affine plane). To
do a minimal test, I wrote this:
theory Scratch2
imports Main
begin
locale aff =
fixes meets :: "'p ⇒ 'p ⇒ bool"
(* assumes refl: "meets a a = True" *)
print_locale! aff
thm aff_def
fun meets2 :: "nat ⇒ nat ⇒ bool" where
"meets2 a b = (a = b)"
theorem "aff meets2"
try
The actual "meets" procedures I'll be using have the form 'a -> 'b -> bool,
but I thought I'd simplify for early testing. Right after the commented-out
line, Isabelle reports that the locale "aff" has been defined, and I can
print it just fine. But at "thm aff_def", it turns out that "aff_def" is
undefined. If I uncomment the "assumes refl" line, then it actually IS
defined. And the theorem at the bottom -- that "meets2" has all the
properties required to be an "aff", is easy to prove with "simp".
But leaving that line commented out, there are two oddities, The first is
that aff_def is undefined, as I mentioned. Then second is that when I let
"try" attempt to prove the theorem at the bottom, which I believe to be
true, Nitpick finds a counterexample. I'm assuming (since there's something
about "free variable: aff =" in those results that the predicate "aff" has
somehow not been recognized or defined, but frankly, I'm baffled. Can
anyone clear up my confusion?
Email Gateway (Aug 22 2022 at 20:27):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear John,
If a locale makes no assumptions, i.e., it only fixes parameters, there's nothing to be
shown. Accordingly, the locale command does not define a locale predicate for such
locales. That's why aff_def does not exist. When you look at your theorem, you'll see that
aff is a free variable of the theorem, not a constant.
Best,
Andreas
Email Gateway (Aug 22 2022 at 20:27):From: "John F. Hughes" <jfh@cs.brown.edu>
I admit that I may have overgeneralized, thinking that the example in
Ballarin's tutorial was a model showing what happened during a generic
locale-definition, rather than during this specific locale-definition.
I find the choice not to include aff_def a baffling bit of software
engineering (why not always introduce the predicate, and sometimes have
it be a predicate that's always true? If you don't, then every proof you do
about locales has to have two cases, etc. I probably just don't understand
something deeper that's going on.)
Also, to match the definition of "aff", there needs to be an actual
function of the correct type -- the predicate shouldn't be completely
vacuous, and indeed, the type-def inherent in the argument to "add_def" (in
the case where we do have assumptions) ensures this, so it's actually doing
something useful. It's a pity (to me) that it's not there unless there are
assumptions.
Email Gateway (Aug 22 2022 at 20:28):From: Tjark Weber <tjark.weber@it.uu.se>
John,
Note that there is a dedicated command "interpretation" to interpret a
locale in a theory, described in Section 5 of Ballarin's tutorial.
Thus, you probably don't want/need to refer to aff_def directly even
when it exists, and instead of
theorem "aff meets2"
<proof>
you likely want to use
interpretation foo: aff meets2
<proof>
This automatically generates the right proof obligations, and works
regardless of whether aff actually makes any assumptions.
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Last updated: Apr 26 2024 at 04:17 UTC