Email Gateway (Dec 06 2023 at 00:35): Email Gateway (Dec 06 2023 at 00:35):From: Ian Hayes <Ian.Hayes@uq.edu.au>
We are trying to understand some theories that use _update_name but we
cannot find any documentation for it.
We've worked out by experiment what it does in that
_update_name x (λ_. a)
where the value of is the identifier v, say, gives
v_update (λ_. a)
Can someone point us to the definition/documentation for _update_name ?
Many thanks in advance
Ian
Email Gateway (Dec 06 2023 at 01:02):From: Ian Hayes <Ian.Hayes@uq.edu.au>
Try again, without underlining.
We are trying to understand some theories that use _update_name but we
cannot find any documentation for it.
We've worked out by experiment what it does in that
_update_name x (λ_. a)
where the value of is the identifier v, say, gives
v_update (λ_. a)
Can someone point us to the definition/documentation for _update_name ?
Many thanks in advance
Ian
Ian Hayes
Mail: School of Electrical Engineering and Computer Science,
University of Queensland, Brisbane, Queensland 4072, Australia
CRICOS 00025B • TEQSA PRV12080
Timezone: GMT+10 hours
Email Gateway (Dec 06 2023 at 01:05):From: Ian Hayes <Ian.Hayes@uq.edu.au>
Try try again, without underlining.
We are trying to understand some theories that use _update_name but we
cannot find any documentation for it.
We've worked out by experiment what it does in that
_update_name x (λ_.a)
where the value of is the identifier v, say, gives
v_update (λ_. a)
Can someone point us to the definition/documentation for _update_name ?
Many thanks in advance
Ian
Ian Hayes
Mail: School of Electrical Engineering and Computer Science,
University of Queensland, Brisbane, Queensland 4072, Australia
CRICOS 00025B • TEQSA PRV12080
Timezone: GMT+10 hours
Email Gateway (Dec 08 2023 at 09:10):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Ian,
I believe those are record update functions. You can find more information in
section 11.6 Records of The Isabelle/Isar Reference Manual.
Best
Tobias
Email Gateway (Dec 08 2023 at 10:37):From: Makarius <makarius@sketis.net>
The formal source is part of the documentation. The canonical "induction over
the sources" works via hypersearch in Isabelle/jEdit. Here are some notable
parameters for it:
Search for: _update_name
X Directory
Filter: *.{ML,thy}
Directory: $ISABELLE_HOME/src
X Search subdirectories
X Hypersearch
X Whole word
This reveals the declaration as syntax constant in pure_thy.ML, the definition
as parse_translation in syntax_trans.ML, using update_name_tr. The latter
Isabelle/ML function is defined as follows:
fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x,
T), ts)
| update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update"
x, T), ts)
| update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
if Term_Position.is_position ty then list_comb (c $ update_name_tr [t]
$ ty, ts)
else
list_comb (c $ update_name_tr [t] $
(Lexicon.fun_type $
(Lexicon.fun_type $ Lexicon.dummy_type $ ty) $
Lexicon.dummy_type), ts)
| update_name_tr ts = raise TERM ("update_name_tr", ts);
Moreover the above hypersearch reveals some example applications, e.g. in
src/HOL/Isar_Examples/Hoare.thy:
translations
"B [a/´x]" ⇀ "⦃´(_update_name x (λ_. a)) ∈ B⦄"
The prose text in that file also talks about "x" (selector) vs "x_update"
(update). That is merely a naming convention.
Note that the Isabelle/HOL record package used to follow precisely that
convention (1998), but in the latter decades more complexity has been piled
up. So if this question is actually about records, it might need further
detailed study of its sources, together with the prose text in the isar-ref
manual.
Makarius
Last updated: Apr 28 2024 at 16:17 UTC