Re: [isabelle] Presenting theories - equality symbols and abbreviations



Hello Filip,

With regard to your third question: I think "definition" and "fun" are rather different, so it makes sense to have different "==" and "=" symbols. 

> definition f where "f x == (x <-> True)" 


just means "define f as the function taking x to (x <-> True)", but

> fun f where "f x = (x <-> True)"


allows "f" to appear recursively on the RHS too, so it means "define f as the least fixed point of the equality f x = (x <-> True)".

John

On 11 Mar 2012, at 07:14, filip at matf.bg.ac.rs wrote:

> Hello,
> I am trying to generate LaTeX-ed proof documents from my Isabelle/HOL
> theories and I have several technical questions.
> 
> (1) Suppose I have a definition like
> 
> definition f where "f x == x <-> True"
> 
> When I use @{thm f_def[no_vars]}, in LaTeX, I get
> 
> f x == x = True
> 
> So, = is printed, although I used the <-> symbol. Is there a way to
> persuade the system to print <-> for equality on bool type? It would be
> convenient if this could be done globally, so I could be sure that <-> is
> consistently used in the whole proof document.
> 
> (2) If f is an abbreviation like
> 
> abbreviation f where "f x == x <-> True"
> 
> Is there a way to print it later using some antiquotation (as I used @{thm
> f_def[no_vars]}, when f was a definition).
> 
> (3) I noticed that function definitions do not allow using == but only =.
> For example, I am not allowed to write:
> 
> fun f where "f (a, b) == a > b"
> 
> but only
> 
> fun f where "f (a, b) = (a > b)"
> 
> That seems a bit inconsistent with definitions made by using the
> definition keyword. Is it maybe somehow possible to make @{thm
> f.simps[no_vars]} print == instead of = so in LaTeX I get
> 
> f (a, b) == a > b
> 
> I prefer this notation (since it emphasizes that something holds by
> definition, since it does not require additional parentheses and since it
> is consistent with definitions given using the definition keyword).
> 
> Thank you very much for your answers!
> Filip
> 
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.