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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
