Email Gateway (Aug 18 2022 at 13:25): Email Gateway (Aug 18 2022 at 13:25):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi all,
I am currently converting my theories to Isabelle 2009 and stumbled
across the following problem with locales:
In Isabelle 2008, things like the following worked very well:
locale foo =
fixes x :: "'a => 'a => bool"
and y :: "'a => 'a => bool"
and P :: "'a => bool"
and xs :: "'a => 'a => bool" ("_ ->* _")
defines xs_def: "xs == (%a b. x a b & y a b)^**"
assumes "a ->* b ==> P b"
interpretation f: foo["%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
"%a.True"]
apply(simp)
apply(unfold_locales)
apply(rule TrueI)
done
Here, I use the defines feature to introduce an abbreviation and
notation for some complex term which can then be used to state the
assumptions. Inside the locale, the defined parameter behaves like a
definition whereas when interpreting these locales, these definitions
are automatically unfolded.
If I try to do this to Isabelle 2009, everything seems to break. The
locale definition works as before, but interpreting foo is terrible:
1st try:
interpretation f: foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
"%a.True"
This does not work because the defined parameter is not instantiated,
but left as a free variable, which must be shown equal to the definition
of xs in the locale.
2nd try:
interpretation f: foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
"%a. True"
"(%a b. a > 0 & b <= Suc 0 & a < 10)^**"
Now the explicit parameter is given, but unfold_locales nor
intro_locales longer work any longer (empty result sequence). It seems
that I have to prove the interpretation manually by (rule foo.intro,
simp_all).
Can I still do this trick of having parameters defined in a locale
declaration that are unfolded automatically for all interpretations and
that can be used in the assumptions (with additional syntax)?
How must interpretations be written such that such defined parameters
need not be specified?
Why do unfold_locales/intro_locales not work here? What else should I use?
Regards,
Andreas Lochbihler
Email Gateway (Aug 18 2022 at 13:26):From: Clemens Ballarin <ballarin@in.tum.de>
Quoting Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>:
locale foo =
fixes x :: "'a => 'a => bool"
and y :: "'a => 'a => bool"
and P :: "'a => bool"
and xs :: "'a => 'a => bool" ("_ ->* _")
defines xs_def: "xs == (%a b. x a b & y a b)^**"
assumes "a ->* b ==> P b"interpretation f: foo["%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
"%a.True"]
The feature that defined parameters may be omitted in interpretation
has been withdrawn in an attempt to make defines more similar to
assumes.
2nd try:
interpretation f: foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
"%a. True"
"(%a b. a > 0 & b <= Suc 0 & a < 10)^**"Now the explicit parameter is given, but unfold_locales nor
intro_locales longer work any longer (empty result sequence).
In apply-style you can do "apply -" to break up the goal followed by
explicit goal addressing ("apply unfold_locales [1]" or similar). In
proper Isar proofs, "proof" breaks up the goal for you.
Clemens
Email Gateway (Aug 18 2022 at 13:26):From: Makarius <makarius@sketis.net>
In fact, this break up of simultaneous goals is implicit in any regular method
application (with the exception of special simultaneous methods like "induct").
This means you can finish the proof script like this:
interpretation f:
foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10" "%a. True"
"(%a b. a > 0 & b <= Suc 0 & a < 10)^**"
apply (unfold_locales)[1]
apply (rule TrueI)
apply simp
done
Makarius
Email Gateway (Aug 18 2022 at 13:26):From: Brian Huffman <brianh@cs.pdx.edu>
So what (if any) is the difference between "defines" and "assumes" now? It
seems that with the current locale package, locale "foo" might as well be
defined as below, with "assumes xs_def". Am I missing something?
locale foo =
fixes x :: "'a => 'a => bool"
and y :: "'a => 'a => bool"
and P :: "'a => bool"
and xs :: "'a => 'a => bool" ("_ ->* _")
assumes xs_def: "xs == (%a b. x a b & y a b)^**"
assumes "a ->* b ==> P b"
Last updated: Nov 21 2024 at 12:39 UTC