The only easy way to do this at the moment would be to
- Define a fake constant with the name of the binder you want, but which does
nothing. E.g.,
Define`AE x = x`;
- Make it a binder :
set_fixity “AE” Binder;
- Define your real constant as below:
Define`almost_everywhere m P = …`
- Then
associate_restriction ("AE", "almost_everywhere")
Then, you can get the sort of effect you want by writing
``AE x::m. P``
The m will be a free variable, and the x will be bound in P. If you do a
dest_term on it, you will get
COMB(``almost_everywhere m``, ``\x. P``)
In some future update to HOL, I’d like to make it possible to use the
set-membership epsilon instead of the ::, which is not a great piece of syntax.
I hope this helps. I will think about your second question some more.
Michael
On 7/2/17, 07:58, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
Hi,
Suppose I have the following definition about a predicate P (with a measure
space m):
val almost_everywhere_def = Define `
almost_everywhere m P = ?N. null_set m N /\ !x. x IN (UNIV DIFF N) ==>
P x`;
(I think you can safely think it as `almost_everywhere m P = !x. P x`.)
Now my purpose is to define a syntax "AE x in m. P”, which has the meaning:
``almost_everywhere m (\x. P)``. The main difficulty is that, x is not a free
variable.
If I try to define it in this (wrong) way:
val AE_def = Define `AE x m P = almost_everywhere m (\x. P)`;
val _ = add_rule { term_name = "AE", fixity = Prefix 1000, (* make sure
lower than limit "-->" *)
pp_elements = [ PPBlock ([TOK "AE", BreakSpace(1,2), TM,
BreakSpace(1,0), TOK "in"],
(PP.CONSISTENT, 0)),
BreakSpace(1,2), TM, HardSpace 0, TOK ".",
BreakSpace(1,0) ],
paren_style = OnlyIfNecessary,
block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)) };
A test term like the following looks good but actually not:
> ``AE x in p. (\j. (X_n j x)) --> (X x)``;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it =
``AE x in p. ((λj. X_n j x) --> X x)``:
term
because somehow the outside “x” is a free variable in this term. So I have
no way to further define my final concept:
val converge_AE_def = Define `converge_AE p X_n X = AE x in p. (\j. (X_n j
x)) --> (X x)`;
Can anyone suggest a correct way to define the “AE” syntax?
P. S. furthermore, is it possible to define a pretty printer for the last
definition “converge_AE p X_n X”, to make it printing into the following form?
X_n --> X (p-a.e.)
Best Regards,
Chun Tian
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
