Re: [isabelle-dev] Binding with implicit rename
Hi Florian,
to me the liberal flag seems rather ad-hoc. Wouldn't a proper
hierarchical naming solve this problem (maybe by introducing an
automatic "sub-module" Internal/Auto/Whatever for any theory T, such
that automatic names may be referred to by using T.Whatever.automatic_name).
Admittedly, after reading once more through the above paragraph, my own
suggestion seems rather ad-hoc ... Nevertheless, maybe it gives rise to
discussion ;)
cheers
chris
On 10/07/2010 09:23 AM, Florian Haftmann wrote:
Typically, bindings are created by the user in the theory text and
passed down from there, e.g.
specification (definition) foo :: T
where
"P foo"
creates a @{binding foo}.
However in packages often also bindings are created automatically.
Currently I am working on some fragements of a mechanism which analyzes
parts of a theory (most prominently constants and theorems) and
generated new constants and theorems from them. The result, in
particular the new constants, are highly unpredictable, and the user is
not really interested in the number or names of the new constants. The
situation is somehow similar to the predicate compiler, but even less
tamed. To ensure that the new constants do not clash with existing
ones, the bindings for them have to be distilled carefully and a rather
unsatisfactory way. I am asking myself whether this could be
dramatically simplified by giving bindings a »liberal« flag: this could
be set e.g. using a function Binding.liberal :: binding -> binding; on
declaration in a namespace, the basename of a liberal binding would be
modified if it would clash with an existing declaration. User-space
binding would stay non-liberal an issue an error on clashing.
I think such a liberal binding mechanism would be helpful for all kind
of tools which provide automatic, rather unpredictable theory extensions.
Any opinions?
Florian
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Binding with implicit rename
Typically, bindings are created by the user in the theory text and
passed down from there, e.g.
specification (definition) foo :: T
where
"P foo"
creates a @{binding foo}.
However in packages often also bindings are created automatically.
Currently I am working on some fragements of a mechanism which analyzes
parts of a theory (most prominently constants and theorems) and
generated new constants and theorems from them. The result, in
particular the new constants, are highly unpredictable, and the user is
not really interested in the number or names of the new constants. The
situation is somehow similar to the predicate compiler, but even less
tamed. To ensure that the new constants do not clash with existing
ones, the bindings for them have to be distilled carefully and a rather
unsatisfactory way. I am asking myself whether this could be
dramatically simplified by giving bindings a »liberal« flag: this could
be set e.g. using a function Binding.liberal :: binding -> binding; on
declaration in a namespace, the basename of a liberal binding would be
modified if it would clash with an existing declaration. User-space
binding would stay non-liberal an issue an error on clashing.
I think such a liberal binding mechanism would be helpful for all kind
of tools which provide automatic, rather unpredictable theory extensions.
Any opinions?
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Declaration depending on user proofs
On 10/07/2010 09:11 AM, Florian Haftmann wrote:
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 => 'b_1) => ... => ('a_n => 'b_n)
=> ('a_1, ..., 'a_n) k is => ('b_1, ..., 'b_n) k
for an n-ary type ('a_1, ..., 'a_n) k must satisfy some characteristic
properties like
map_k f_1 ... f_n o map_k g_1 ... g_n =
map_k (f_1 o g_1) ... (f_n o g_n)
To declare something as a type mapper, the following command could be
introduced
type_mapper map_k
which would issue an appropriate declaration. Attributes are
inappropriate here since the user cannot be expected to write down the
theorems to prove explicitly.
However I am always reluctant to introduce new keywords, both for
aesthetic and technical reasons. So I am asking myself whether we
should introduce a command for generic user-proof-dependent
declarations, e.g.
prove
Here different parsers could be registered under the umbrella of the
same command. Some possible instances:
prove type_mapper: map_l
prove isomorphism: Fset.Fset Fset.member
Any opinions?
Florian
The code_pred command for the invocation of the predicate compiler could
also fit under this umbrella.
So the syntax would change from "code_pred" to "prove code_pred" which
is actually better, because then users are not surprised
that the command sets up some goal state (in most cases the empty goal)
for the user to prove.
Lukas
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Declaration depending on user proofs
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 => 'b_1) => ... => ('a_n => 'b_n)
=> ('a_1, ..., 'a_n) k is => ('b_1, ..., 'b_n) k
for an n-ary type ('a_1, ..., 'a_n) k must satisfy some characteristic
properties like
map_k f_1 ... f_n o map_k g_1 ... g_n =
map_k (f_1 o g_1) ... (f_n o g_n)
To declare something as a type mapper, the following command could be
introduced
type_mapper map_k
which would issue an appropriate declaration. Attributes are
inappropriate here since the user cannot be expected to write down the
theorems to prove explicitly.
However I am always reluctant to introduce new keywords, both for
aesthetic and technical reasons. So I am asking myself whether we
should introduce a command for generic user-proof-dependent
declarations, e.g.
prove
Here different parsers could be registered under the umbrella of the
same command. Some possible instances:
prove type_mapper: map_l
prove isomorphism: Fset.Fset Fset.member
Any opinions?
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
