Email Gateway (Aug 22 2022 at 16:54): Email Gateway (Aug 22 2022 at 16:54):From: Makarius <makarius@sketis.net>
Note that the normal programming interface for abbreviations is
Local_Theory.abbrev. In contrast, Specification.abbreviation is the
user-interface -- it corresponds the 'specification' command in Isar
syntax. When building other definitional packages, the internal
programming interfaces are usually easier to use and more robust than
toplevel commands, e.g. open-ended mechanisms like type-inference and
various "term check" phases are omitted (the results of that are
difficult to predict in general).
The included example illustrates the above situation with proper use of
Local_Theory.abbrev and some further details.
The local theory concept comprises various contexts, notably:
* The hypothetical context is what you build up cumulatively in the
definitional package: lthy, lthy', lthy'' etc. after adding
specifications like Local_Theory.define/note/abbrev.
* The target context is the result that is seen at the end of the
package (sometimes several packages are composed internally). A typical
example is the locale target.
* The foundation (or background) context reduces the fancy local
theory concepts to the reality of the logic at the bottom.
Your observation boils down to the question: What is the meaning of
Local_Theory.abbrev in terms of different context? (Only the first two
matter for regular use, the foundation is merely an implementation detail.)
For Local_Theory.abbrev we see the following, when looking at the
description in Isabelle/ML
http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2017/src/Pure/Isar/local_defs.ML#l118
and the main application in the inductive package
http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2017/src/HOL/Tools/inductive.ML#l1188
(1) In the hypothetical context an abbreviation is more like a local
definition: it needs to be expanded explicitly as required (definitional
packages might have different requirements in different situations).
(2) In the target context an abbreviation is really expanded in the
abstract syntax "term check" phase, this is the normal behavior for
end-users working with the results of such specifications.
I don't remember all the reasons why point 1) emerged the way it works
today -- actually already in Isabelle2007 (November 2007), but here is
some historical evidence for it:
changeset: 25029:3a72718c5ddd
user: wenzelm
date: Sun Oct 14 16:13:45 2007 +0200
files: src/HOL/Tools/inductive_package.ML
description:
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
tuned;
changeset: 25114:7aa178165ee4
user: wenzelm
date: Sat Oct 20 18:54:28 2007 +0200
files: src/HOL/Tools/inductive_package.ML
description:
add_inductive: more careful handling of abbrevs -- do not expand
prematurely;
changeset: 25143:2a1acc88a180
user: wenzelm
date: Mon Oct 22 15:24:58 2007 +0200
files: src/HOL/Bali/DeclConcepts.thy
src/HOL/Tools/inductive_package.ML
description:
abbrevs within inductive definitions may no longer depend on each other
(reflects in internal organization, particularly for output);
In the included Scratch.thy, I have wrapped up an expand operation for
precisely the abbreviated term, by peeking at the definition of
Local_Defs.fixed_abbrev. It could be also done with various export
operations from the modules Proof_Context, Local_Theory, Assumption, but
that also exports wrt. other things added to the context in between,
e.g. actual Local_Theory.define.
The programming interface for Local_Theory.abbrev could be more
convenient in that respect, but it is used so rarely that no serious
demand arose so far. De-facto, the 'inductive' package defines its
meaning and purpose.
Makarius
Scratch.thy
Email Gateway (Aug 22 2022 at 16:59):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Dear Isabelle list,
After I add an abbreviation to a local context, the parser seems to ignore
it.
Is there a way to get parsing without prefixes working for abbreviations in
my local context?
Minimal example of this strange behavior:
theory t imports HOL begin
local_setup {* fn lthy =>
let
val lthy2 = Specification.abbreviation Syntax.mode_default
NONE [] @{term "asd == True"} true lthy
val _ = tracing (@{make_string} (Syntax.read_term lthy2 "asd")
in lthy2 end
*}
Displays "Free asd" rather than "Const True".
Surprisingly, I get "Const True" if I prefix it by the theory
name (as in "t.asd") or if I reset the context, as in:
val lthy3 = Proof_Context.init_global (Proof_Context.theory_of lthy2)
both of which I believe I should not be doing myself, so how can I get
parsing for abbreviations to work in a local context?
Regards,
Cezary
Last updated: Apr 23 2024 at 12:29 UTC