Re: [isabelle] Parsing abbreviations in a local context

On 03/03/18 06:05, Cezary Kaliszyk wrote:
> 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?

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
and the main application in the inductive package

  (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
gen_add_inductive_i: treat abbrevs as local defs, expand by export;

changeset:   25114:7aa178165ee4
user:        wenzelm
date:        Sat Oct 20 18:54:28 2007 +0200
files:       src/HOL/Tools/inductive_package.ML
add_inductive: more careful handling of abbrevs -- do not expand

changeset:   25143:2a1acc88a180
user:        wenzelm
date:        Mon Oct 22 15:24:58 2007 +0200
files:       src/HOL/Bali/DeclConcepts.thy
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.

theory Scratch
  imports Main

locale test

local_setup \<open>fn lthy =>
    val (res', lthy') = lthy
      |> Local_Theory.abbrev Syntax.mode_default ((@{binding a}, NoSyn), @{term Nil});
    val res = res' |> apply2 (Morphism.term (Proof_Context.export_morphism lthy lthy'));
    val result = res' |> apply2 (Morphism.term (Local_Theory.target_morphism lthy'));
    val _ = @{print tracing} {res' = res', res = res, result = result};

    (*experiments with Syntax.read_term -- it is UNUSUAL to invoke
      that in the middle of a definitional package!*)
    val t = Syntax.read_term lthy' "a";
    val t' = Syntax.read_term (Local_Theory.target_of lthy') "a";

    (*expand according to Local_Defs.fixed_abbrevs*)
    val expand = Envir.expand_term_frees [(dest_Free (#1 res'), #2 res')];
    val _ = @{print tracing} {t = t, t' = t', t_expanded = expand t};
  in lthy' end;



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.