Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] making local definitions programmatically

view this post on Zulip Email Gateway (Aug 18 2022 at 11:38):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
Florian Haftmann wrote:

I must confess the qualification conventions appear to me also a
little bit obscure. Generally, most times it is preferable to store
the logical entities stemming from definitions etc. in separate
tables for later usage.

Dear Florian,

Thanks for your help with this; my code now works.

As for this last point, I thought that I would do as you suggest (keep
track of what is returned by LocalTheory.define), but if you check
what it does, you don't actually get a Const back. Instead, the term
returned is a Free, with an unqualified name.

So this doesn't seem to be so helpful. (Perhaps I could take the
defining theorem apart....)

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:38):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Michael,

As for this last point, I thought that I would do as you suggest (keep
track of what is returned by LocalTheory.define), but if you check
what it does, you don't actually get a Const back. Instead, the term
returned is a Free, with an unqualified name.

Concerning this, recall the following:

locale L =
fixes c0 :: "'a \<Rightarrow> 'a"
begin

ML {*
fun def lthy =
let
val ((t, _), lthy') = LocalTheory.define Thm.definitionK
(("c1", NoSyn), (("", []), @{term "\<lambda>x. c0 (c0 x)"})) lthy;
val lthy'' = LocalTheory.restore lthy';
val t' = Morphism.term (ProofContext.export_morphism lthy' lthy'') t;
in (t', lthy'') end;
*}

ML {*
Context.>>> (Context.map_proof_result def)
*}

Definitions in local theories accumulate a hypothetical proof context.
If you want to return to the plain local theory, you can leave the
hypothetical proof context using LocalTheory.restore and export logical
entities (theorems, terms, types, ...) using an appropriate export
morphism which calcuates the difference between the hypothetical proof
context lthy' and the restored plain local theory lthy''.

This approach refrains from assuming anything about a particular naming
policy.

Hope this helps,

Florian
florian.haftmann.vcf
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 11:38):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
Florian Haftmann wrote:

Concerning this, recall the following:

locale L =
fixes c0 :: "'a \<Rightarrow> 'a"
begin

ML {*
fun def lthy =
let
val ((t, _), lthy') = LocalTheory.define Thm.definitionK
(("c1", NoSyn), (("", []), @{term "\<lambda>x. c0 (c0 x)"}))
lthy;
val lthy'' = LocalTheory.restore lthy';
val t' = Morphism.term (ProofContext.export_morphism lthy'
lthy'') t;
in (t', lthy'') end;
*}

ML {*
Context.>>> (Context.map_proof_result def)
*}

This approach refrains from assuming anything about a particular
naming policy.

Ah yes. If I call LocalTheory.restore, I guess I still have to later
call LocalTheory.exit. Is that right?

And another thing: a while back Makarius said that we should avoid all
functions that implicitly manipulate references because these are
unsafe in the presence of threads. Yet it is clear that Context.>>>
must be doing this. Is this function an exception to the general rule?

Thanks,
Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:39):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Michael,

It is helpful to recall the local theory sandwich:

hypothetical proof context (ctxt)
---------------------------------
local theory (lthy)
---------------------------------
background theory (thy)

An lthy is "put on top" of a thy e.g. by means of LocalTheory.init.
LocalTheory.define etc. than accumulate hypothetical entities, resulting
in the hypothetical context ctxt. If necessary, you can "switch back"
to lthy by LocalTheory.restore. Since LocalTheory.define etc. extend
thy, linearity has to be ensured - Local.Theory.exit re-exposed the
"backbone" theory thy.

So much to say about this part of the story.

Now concerning Context.>>(>). These are the only remaining facilities
which update a context destructively; in a certain fashion they are the
sinbin where the (rare) cases when a destructive update is unaviodable
are focused. The runtime framework asserts that concurrent threads do
not interfere here. Of course the best thing is to adhere to explicit
pure updates, but for bootstrap, legacy or explorative issues this
facility is helpful.

Hope this helps

Florian
florian.haftmann.vcf
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 11:45):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
I have a locale L with some number of fixes, f1, f2 and f3, say.

Using LocalTheory.define, I have defined a number of constants in that
locale with eqns

C1 == rhs1
C2 == rhs2

some, none or all of the rhs-es may refer to the fixes. Say each of
C1 and C2 is of type nat.

Subsequently, in the same locale, I want to define a function of the
form

select b == if b then C1 else C2

I want to build the right-hand side for this definition in ML.

What do I put into the conditional term in the place of C1 and C2?

It would be nice if I could just write

Const("C1", nat)

and

Const("C2", nat)

But I guess this won't work, because C1 probably really has a type
that depends on the fixes that appear in rhs1, and likewise C2.
I.e., at the top level, if I do the Isar command

term "L.C1"

I may see that it really has type "fixtype1 => nat", and L.C2 may have
type "fixtype1 => fixtype2 => nat".

So, what do I do?

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:46):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Michael,

the best thing is to use the "check" interface which does the job for you:

Syntax.check_term @{context} (Const ("local.C1", dummyT))

yield a completely inferred and expanded term representing the local
constant C1. This saves you from educated guesses what the expanded
foundation term of a local constant actually is. Note that "check" is a
part of the canonical interface for reading terms:

a) "parse" transforms a string to an abstract term representation
(without further steps like type inference, expanding local constants etc)
b) "check" does the rest

This allows to aggregate "skeleton terms" with dummy types and check
them to get complete internal terms.

Example:

theory Scratch
imports Main
begin

locale L =
fixes c0 :: "'a \<Rightarrow> 'a"
begin

definition
"c1 x = c0 (c0 x)"

definition
"c2 x = c1 (c1 x)"

ML {* Syntax.parse_term @{context} "c1" *}
ML {* Syntax.check_term @{context} (Const ("local.c1", dummyT)) *}

end

Hope this helps
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 11:46):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
Florian Haftmann wrote:

the best thing is to use the "check" interface which does the job
for you:

Syntax.check_term @{context} (Const ("local.C1", dummyT))

yield a completely inferred and expanded term representing the local
constant C1. This saves you from educated guesses what the expanded
foundation term of a local constant actually is. Note that "check"
is a part of the canonical interface for reading terms [...]

This allows to aggregate "skeleton terms" with dummy types and check
them to get complete internal terms.

Example:

locale L =
fixes c0 :: "'a \<Rightarrow> 'a"
begin

definition
"c1 x = c0 (c0 x)"

definition
"c2 x = c1 (c1 x)"

ML {* Syntax.parse_term @{context} "c1" *}
ML {* Syntax.check_term @{context} (Const ("local.c1", dummyT)) *}

end

But can I then pass an expanded term, one which mentions the implicit
locale parameters explicitly, to LocalTheory.define? My experiments
suggest I can't.

If I put this into the locale

ML {* val t = Syntax.check_term @{context} (Const("local.c1", dummyT))
val ctxt' = LocalTheory.define Thm.definitionK
(("c3", NoSyn), (("", []), t))
@{context}
*}

then I get an error "Illegal application of command "consts" in local
theory mode". What should t be to make this definition work? Or
should I be using some other definitional principle?

And is prepending "local." the canonical way to get an acceptable name
for the locale's constants?

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:47):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Michael,

Which Isabelle version are you using? The following works fine with
Isabelle2007:

locale L =
fixes c0 :: "'a � 'a"
begin

definition
"c1 x = c0 (c0 x)"

definition
"c2 x = c1 (c1 x)"

ML {*
val t = Syntax.check_term @{context} (Const ("local.c1", dummyT))
*}

ML {* val (_, ctxt') = LocalTheory.define Thm.definitionK (("c3",
NoSyn), (("", []), t)) @{context} *}

Recently it is now also possible to transform a local context (a local
theory) with ML, using the Context.>> and Context.>>> combinators within
ML sections:

locale L =
fixes c0 :: "'a \<Rightarrow> 'a"
begin

definition
"c1 x = c0 (c0 x)"

definition
"c2 x = c1 (c1 x)"

ML_val {*
val t = Syntax.check_term @{context} (Const ("local.c1", dummyT))
*}

ML {*
Context.>>> (Context.map_proof_result (
LocalTheory.define Thm.definitionK (("c3", NoSyn), (("", []), t))
##> LocalTheory.restore
))
*}

ML {* @{term c3} *}
thm c3_def

end

Hope this helps
Florian
florian.haftmann.vcf
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 11:47):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
Florian Haftmann wrote:

ML {* val t = Syntax.check_term @{context} (Const("local.c1", dummyT))
val ctxt' = LocalTheory.define Thm.definitionK
(("c3", NoSyn), (("", []), t))
@{context}
*}

Which Isabelle version are you using? The following works fine with
Isabelle2007 [...]

I just tried it again; and now it works. This is very strange, but
I'll assume I messed up my previous experiment. Thanks for your help!

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:47):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
A further hint I want to add: LocalTheory.define etc. return the
defined entity as a term. Normally it is the best to use these directly
to build up other definitions, lemmas etc. This saves you from
referring to suspected names of constants altogether.

Florian
florian.haftmann.vcf
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 11:48):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
Florian Haftmann wrote:

A further hint I want to add: LocalTheory.define etc. return the
defined entity as a term. Normally it is the best to use these
directly to build up other definitions, lemmas etc. This saves you
from referring to suspected names of constants altogether.

It seems I have have apply Context.map_proof_result for this to be
useful. If I omit this (as below), then the result includes a term
that is a Free (not a Const), with no parameters.

locale L =
fixes c0 :: "'a => 'a"
begin

definition
"c1 x = c0 (c0 x)"

definition
"c2 x = c1 (c1 x)"

ML {*
val t = Syntax.check_term @{context} (Const ("local.c1", dummyT))
*}

ML {* val (result, ctxt') = LocalTheory.define Thm.definitionK (("c3",
NoSyn), (("", []), t)) @{context} *}

end

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:48):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
Michael Norrish wrote:

Florian Haftmann wrote:

A further hint I want to add: LocalTheory.define etc. return the
defined entity as a term. Normally it is the best to use these
directly to build up other definitions, lemmas etc. This saves you
from referring to suspected names of constants altogether.

It seems I have have apply Context.map_proof_result for this to be
useful. If I omit this (as below), then the result includes a term
that is a Free (not a Const), with no parameters.

It seems I was confused. Context.map_proof_result is no use.
Whatever I do, LocalTheory.define doesn't return anything other than
an unadorned Free.

It seems that if I want to refer to other local constants, I should
construct a

Const("local." ^ myconstname, dummyT)

and then Syntax.check it.

Is this best practice?

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:48):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Michael,

Definitions in local theories accumulate a hypothetical proof context.
If you want to return to the plain local theory, you can leave the
hypothetical proof context using LocalTheory.restore and export logical
entities (theorems, terms, types, ...) using an appropriate export
morphism which calcuates the difference between the hypothetical proof
context lthy' and the restored plain local theory lthy''.

Anyway, it is also possible (and most times more convenient) to
continue within the hypothetical context with defines, notes etc.
These are exported into the local theory context implicitly without
further ado.

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 11:48):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
Florian Haftmann wrote:

Definitions in local theories accumulate a hypothetical proof
context. If you want to return to the plain local theory, you can
leave the hypothetical proof context using LocalTheory.restore and
export logical entities (theorems, terms, types, ...) using an
appropriate export morphism which calcuates the difference between
the hypothetical proof context lthy' and the restored plain local
theory lthy''.

I need to make definitions inside a locale that I have set up
programmatically. Within that program, I can't do nice things like
@{term "...localeconst...."} (as in your example), because the
code doing this is not itself in a locale.

Here's a specific question about check_term.

If I have a theory fragment of the following form:

theory Scratch
imports Main
begin

locale L =
fixes x :: nat
begin
definition "y = x + 3"
end

term L.y
thm L.y_def

ML {*
val lthy = TheoryTarget.init (SOME "Scratch.L")
(Context.deref @{theory_ref})
val t = Syntax.check_term lthy (Const(<string>, dummyT))
*}

The only way I can avoid an "unknown const" error is to have

<string> = "Scratch.L.y"

I thought the point of check_term was that I could have "local.y"
there, and have it work. Have I set up my lthy local_theory value
incorrectly?

(In my simple example, I recognise that I could also write

<string> = @{const_name "L.y"}

This is no use in my real circumstances, where the locale L has been
set up in code, so there is no fixed string "L.y" I could provide to
@{const_name}. Indeed, both the "L" and the "y" are constructed
strings in my code.)

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:49):

From: Simon Winwood <sjw@cse.unsw.edu.au>
This works for me:

ML {*
val lthy = TheoryTarget.init (SOME "Scratch.L") (Context.deref @{theory_ref})
val t = Syntax.check_term lthy (Const(LocalTheory.full_name lthy "y", dummyT))
*}

I guess that check_term doesn't expand the name it is given.
That first line is ugly, better (IMHO) is:

val lthy = TheoryTarget.context "L" @{theory}

Simon

At Tue, 29 Apr 2008 16:39:39 +1000,
Michael Norrish wrote:

Florian Haftmann wrote:
[...]

I need to make definitions inside a locale that I have set up
programmatically. Within that program, I can't do nice things like
@{term "...localeconst...."} (as in your example), because the
code doing this is not itself in a locale.

Here's a specific question about check_term.

If I have a theory fragment of the following form:

theory Scratch
imports Main
begin

locale L =
fixes x :: nat
begin
definition "y = x + 3"
end

term L.y
thm L.y_def

ML {*
val lthy = TheoryTarget.init (SOME "Scratch.L")
(Context.deref @{theory_ref})
val t = Syntax.check_term lthy (Const(<string>, dummyT))
*}

The only way I can avoid an "unknown const" error is to have

<string> = "Scratch.L.y"

I thought the point of check_term was that I could have "local.y"
there, and have it work. Have I set up my lthy local_theory value
incorrectly?

(In my simple example, I recognise that I could also write

<string> = @{const_name "L.y"}

This is no use in my real circumstances, where the locale L has been
set up in code, so there is no fixed string "L.y" I could provide to
@{const_name}. Indeed, both the "L" and the "y" are constructed
strings in my code.)

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 11:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Michael,

a possibility to get the internal (fully qualified) identifier of a
constant is to lookup the constant table explicitly, as done here in
line "val c = ...":

theory Scratch
imports Main
begin

locale L =
fixes n :: nat
begin

definition "m = n + 3"

end

ML {*
val lthy = TheoryTarget.init (SOME "Scratch.L") @{theory};
val c = Consts.intern (ProofContext.consts_of lthy) "m";
val t = Syntax.check_term lthy (Const (c, dummyT));
*}

The subsequent check_term internalizes the abbreviation etc.

I must confess the qualification conventions appear to me also a little
bit obscure. Generally, most times it is preferable to store the
logical entities stemming from definitions etc. in separate tables for
later usage.

Hope this helps
Florian
florian.haftmann.vcf
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC