[isabelle] The syntactic equality



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 at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] 代表 cl-isabelle-users-request at lists.cam.ac.uk
发送时间: 2012年6月26日 3:51
收件人: cl-isabelle-users at lists.cam.ac.uk
主题: Cl-isabelle-users Digest, Vol 84, Issue 27

Send Cl-isabelle-users mailing list submissions to
	cl-isabelle-users at 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 at lists.cam.ac.uk

You can reach the person managing the list at
	cl-isabelle-users-owner at 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 at informatik.tu-muenchen.de>
Subject: Re: [isabelle] Trying to rename Lattices.thy
To: cl-isabelle-users at lists.cam.ac.uk
Message-ID: <4FE82002.6010801 at 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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



------------------------------

Message: 2
Date: Mon, 25 Jun 2012 10:24:06 +0200
From: Brian Huffman <huffman at in.tum.de>
Subject: [isabelle] HOLCF code generation (was:  Lazy Lists)
To: Lawrence Paulson <lp15 at cam.ac.uk>
Cc: Christian Sternagel <c-sterna at jaist.ac.jp>,	isabelle-users
	<isabelle-users at cl.cam.ac.uk>,	Andreas Lochbihler
	<andreas.lochbihler at kit.edu>
Message-ID:
	<CAAMXsiY2zYtrSHMNuNf7dPpcO=VBQvh7hu25FWx41exOnNJ0kQ at mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1

On Mon, Jun 25, 2012 at 9:54 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> [...] HOLCF is explicitly a theory of computation; [...] Such a pity if it doesn't yet support code generation.
>
> Larry

One obstacle to code generation in HOLCF is the application operator:
If you have a HOLCF function "foo" with equation "foo\<cdot>x = x", the code generator will try to interpret this as a defining equation for "op \<cdot>" (because that is the top-most constant on the lhs) instead of "foo", as intended.

If there is demand for code generation in HOLCF, it would probably be worthwhile to put some effort into implementing it. It might be easy to modify the code generator to handle application operators.

Alternatively, we could implement some new HOLCF automation: We could define full-function-space copies of constants with continuous-function types, and translate code equations involving \<cdot> to use these copies.

- Brian



------------------------------

Message: 3
Date: Mon, 25 Jun 2012 10:37:21 +0200 (CEST)
From: Makarius <makarius at sketis.net>
Subject: Re: [isabelle] Trying to rename Lattices.thy
To: cl-isabelle-users at lists.cam.ac.uk
Cc: Tjark Weber <webertj at in.tum.de>,	Gottfried Barrow
	<gottfried.barrow at gmx.com>
Message-ID:
	<alpine.LNX.2.00.1206251031210.13435 at macbroy22.informatik.tu-muenchen.de>
	
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed

On Sun, 24 Jun 2012, Tjark Weber wrote:

> On Sat, 2012-06-23 at 23:56 -0500, Gottfried Barrow wrote:
>> I'm trying to rename HOL/Lattices.thy so I can load it, experiment 
>> with it, and mark it up, but it's picky about what it's name can be.
>
> "Yea, don't do that."
>
> Isabelle/HOL is based upon a complex bootstrapping process, with 
> intertwined setup of theories and proof tools. If you import Main, you 
> get a reasonably clean entry point. If you import anything below Main, 
> you may be exposed to the intricacies of this process.

Indeed.  Importing anything apart from Main or Complex_Main means you investigate the way Isabelle/HOL is bootstrapped, so it is no good for applications, but sometimes helps to understand how things work.


> If you are sure this is what you want, you can load Lattices.thy (and 
> other theories that are part of Isabelle/HOL) by choosing Pure as the 
> logic image for your session: e.g.,
>
>  isabelle jedit -l Pure Isabelle2012/src/HOL/Lattices.thy

Yes, this is the official workaround to peek into parts of the Isabelle/HOL session, until the next big reform of the theory loader in connection with the interactive document model.

In rare cases one does have to rename such an intermediate theory, but then the obvious thing is to turn Lattices into Lattices1, say.  This might require some other renaming nonetheless, as you have noticed already.


 	Makarius



------------------------------

Message: 4
Date: Mon, 25 Jun 2012 10:39:48 +0200 (CEST)
From: Makarius <makarius at sketis.net>
Subject: Re: [isabelle] Trying to rename Lattices.thy
To: cl-isabelle-users at lists.cam.ac.uk
Message-ID:
	<alpine.LNX.2.00.1206251037290.13435 at macbroy22.informatik.tu-muenchen.de>
	
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed

On Mon, 25 Jun 2012, Florian Haftmann wrote:

>> 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.

See Isabelle2012/NEWS:

   * Prover IDE (PIDE) improvements:
     - support for user-defined Isar commands within the running session

For most practical situation you just load the theory that you have in mind, and it should all work as expected.  (There might still be an odd boundary case where one final "File / Reload" in jEdit is needed after all new commands have been defined via loading the imports.)


 	Makarius



------------------------------

Message: 5
Date: Mon, 25 Jun 2012 13:31:40 +0200 (CEST)
From: Makarius <makarius at sketis.net>
Subject: Re: [isabelle] proof dags?
To: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>
Cc: John Wickerson <jpw48 at cam.ac.uk>
Message-ID:
	<alpine.LNX.2.00.1206251325510.20686 at macbroy22.informatik.tu-muenchen.de>
	
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed

On Sat, 2 Jun 2012, John Wickerson wrote:

> It seems to me that proving a lemma in Isabelle is much like building 
> a dag, where the facts are nodes and the implications between facts 
> are arrows. When several nodes "line up" in a simple chain we can use 
> the Isar construction "hence"; and for some other dag shapes the 
> "moreover/ultimately" pattern works. But in general, one needs to 
> invent names sometimes when the underlying proof dag doesn't conform 
> to one of these templates.
>
> I was wondering: has there been any work on a UI that lets the user 
> construct this dag *directly*? I'm imagining a sort of drag-and-drop 
> interface that lets me drag arrows between boxes and move boxes around 
> a canvas, and so on.

I have occasionally pondered the question how the implicit dependency structure and the primary Isar text can be linked in a user interface. 
This means some kind of augmented text editing as in Isabelle/jEdit with a bit more than just a boring tree view on the side.  jEdit also has notions for drag-and-drop of text pieces and various operations on collections of text intervals.

So one mainly needs to link existing concepts for plain text with the structural information of the semantic document model.  Advanced IDEs for programming languages probably have something to offer here already, but I don't know anything from first sight.

If anybody can point to examples from Eclipse, Netbeans, IntelliJ IDEA, or even Visiual Studio, I would be interested to study them to learn how it fits into the proof document model.


 	Makarius



------------------------------

Message: 6
Date: Mon, 25 Jun 2012 14:55:49 +0200 (CEST)
From: Makarius <makarius at sketis.net>
Subject: Re: [isabelle] timing individual use_thys?
To: isabelle-users <isabelle-users at cl.cam.ac.uk>
Cc: Christoph Sprenger <sprenger at inf.ethz.ch>
Message-ID:
	<alpine.LNX.2.00.1206251449590.23959 at macbroy22.informatik.tu-muenchen.de>
	
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed

On Thu, 21 Jun 2012, Christoph Sprenger wrote:

> I would like to time the processing of individual use_thys commands in 
> ROOT.ML files.
>
> If I remember correctly, in earlier versions of Isabelle there was a 
> variant of the use_thy ML commands that returned timing information 
> (something like time_use_thy?). Is there a replacement or alternative 
> to achieve the same effect?

You get the old behaviour back via "Toplevel.timing := true" in ROOT.ML. 
There is a general snag, though, since parallel theory processing makes it difficult to get sensible timing results.  So another (temporary) "Multithreading.max_threads := 1" might help.


 	Makarius



------------------------------

Message: 7
Date: Mon, 25 Jun 2012 15:01:24 +0200 (CEST)
From: Makarius <makarius at sketis.net>
Subject: Re: [isabelle] timing individual use_thys?
To: cl-isabelle-users at lists.cam.ac.uk
Cc: Christian Sternagel <c-sterna at jaist.ac.jp>
Message-ID:
	<alpine.LNX.2.00.1206251456080.23959 at macbroy22.informatik.tu-muenchen.de>
	
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed

On Thu, 21 Jun 2012, Christian Sternagel wrote:

> Dear Christoph,
>
> your question seems very familiar :o)
>
> I would suggest to have a look at the section "Measuring Time" of the 
> Isabelle Programming Tutorial:
>
> http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-
> file/tip/progtutorial.pdf

The timing_wrapper proposed there appears to be a clone of an older version of the standard timeit/timeap wrappers, which go back to Larry from the depths of time, but have been continously updated.

So the Cookbook version is a bit outdated, but it is right in using Timing.message to present the result to the user, not a projection of any of the record components that "happen to work best on my laptop".

Over time that semi-formal timing output might evolve further, to give better readings for the parallel evaluation environment that is standard for quite some years already.


 	Makarius



------------------------------

Message: 8
Date: Mon, 25 Jun 2012 14:50:45 -0500
From: Gottfried Barrow <gottfried.barrow at gmx.com>
Subject: Re: [isabelle] Error: No rule to make target `HOL.thy`
To: cl-isabelle-users at lists.cam.ac.uk
Message-ID: <4FE8C115.9030201 at gmx.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

 > make. *** No rule to make target `HOL.thy`, needed by `cygdrive/e  > /E_main/home/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86-cygwin
 > /HOL'. Stop.

Uh, that's because in trying to copy HOL.thy some number of days back, I moved it, so it was missing from ~/src/HOL. I guess usedir worked because it uses the already built heap for HOL. With the file there, it builds and makes like it's supposed to.

--GB



On 6/21/2012 3:15 PM, gottfried.barrow at gmx.com wrote:
> Hi,
>
> Using Isabelle2011-1, I do this and it creates the heap and 
> browser_info for HOL in my ~/.isabelle/Isabelle2011-1
>
> cd /cygdrive/e/Isabelle2011-1/src/HOL
> isabelle make
>
> I do the same for Isabelle2012, and I get the error shown:
>
> cd /cygdrive/e/Isabelle2012/src/HOL
> isabelle make
>
> make[1]: Entering directory `/cycgdrive/e/Isabelle2012/src/Pure'
> make[1]: Nothing to be done for `Pure`.
> make[1]: Leaving directory `/cycgdrive/e/Isabelle2012/src/Pure'
> make. *** No rule to make target `HOL.thy`, needed by `cygdrive/e 
> /E_main/home/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86-cygwin
> /HOL'. Stop.
>
> I also get the same error if I try to do ./build in $ISABELLE_HOME.
>
> However, I can build sessions with usedir like this:
>
> cd /cygdrive/e/Isabelle2012/src/HOL/Lattice
> isabelle usedir -b HOL Lattice
>
> For both Isabelle2011-1 and Isabelle2012 I have the following set:
>
> ISABELLE_USEDIR_OPTIONS="-i true -g true -M max -p 1 -q 2 -v true -V 
> outline=/proof,/ML"
>
> Regards,
> GB
>
>
>
>
>




End of Cl-isabelle-users Digest, Vol 84, Issue 27
*************************************************






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