Email Gateway (Aug 18 2022 at 20:14): Email Gateway (Aug 18 2022 at 20:14):From: Shuling Wang <wangsl@ios.ac.cn>
Hello,
I need to define the syntax substitution of terms in Isabelle/HOL. So first, for two terms of real, how can I define the syntactic equality?
For example, x::real, y::real, we need to have "x not equal y".
Or are there already good solutions for syntax substitution in Isabelle?
Thanks in advance!
Best,
Shuling
-----邮件原件-----
发件人: cl-isabelle-users-bounces@lists.cam.ac.uk [mailto:cl-isabelle-users-bounces@lists.cam.ac.uk] 代表 cl-isabelle-users-request@lists.cam.ac.uk
发送时间: 2012年6月26日 3:51
收件人: cl-isabelle-users@lists.cam.ac.uk
主题: Cl-isabelle-users Digest, Vol 84, Issue 27
Send Cl-isabelle-users mailing list submissions to
cl-isabelle-users@lists.cam.ac.uk
To subscribe or unsubscribe via the World Wide Web, visit
https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
or, via email, send a message with subject or body 'help' to
cl-isabelle-users-request@lists.cam.ac.uk
You can reach the person managing the list at
cl-isabelle-users-owner@lists.cam.ac.uk
When replying, please edit your Subject line so it is more specific than "Re: Contents of Cl-isabelle-users digest..."
Today's Topics:
1. Re: Trying to rename Lattices.thy (Florian Haftmann)
2. HOLCF code generation (was: Lazy Lists) (Brian Huffman)
3. Re: Trying to rename Lattices.thy (Makarius)
4. Re: Trying to rename Lattices.thy (Makarius)
5. Re: proof dags? (Makarius)
6. Re: timing individual use_thys? (Makarius)
7. Re: timing individual use_thys? (Makarius)
8. Re: Error: No rule to make target HOL.thy (Gottfried Barrow)
Message: 1
Date: Mon, 25 Jun 2012 10:23:30 +0200
From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Subject: Re: [isabelle] Trying to rename Lattices.thy
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <4FE82002.6010801@informatik.tu-muenchen.de>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Files need to be opened in a specific order (and/or you need a lot of reloading files), as jEdit does not yet handle the definition of new commands very well.
AFAIK this restriction does not hold any longer.
Florian
Email Gateway (Aug 18 2022 at 20:18):From: Lars Noschinski <noschinl@in.tum.de>
If you want to do reasoning on the syntax of terms, you need to use a
deep embedding. I.e. define your own datatype to represent terms and
reason then on the structure of this datatype.
-- Lars
Last updated: Apr 26 2024 at 12:28 UTC