|
[isabelle-dev] Partial functions
|
| |
Hi Roger,
Isabelle/HOL is a logic of total function, so very function is defined for all values of the argument type. So, if you declare the type "nat => nat", it is always defined on all natural numbers. As you have found out yourself, you can create types for subsets of natural numbers, but you won't get happy with that, because all of your formalisation will... more »
|
|
|
Be nice to have short tutorials on Quotient Types and Lifting
|
| |
No one needs to respond to this, but I make this a global request, rather than just mention it in another email I'm working on.
I've been getting some mileage out of a short example using lifting that Brian Huffman provided me on Stackoverflow, and just using what I see in the sources as templates, but I don't have any real understanding of... more »
|
|
|
Want to use Rep_Integ or lifting after [quot_del] in Int.thy
|
| |
Hi,
I want to recover the ordered pair part of an int. I actually have a simple solution like this:
definition myI :: "int => nat * nat" where
"myI x = (nat x, nat (-x))"
In the process of getting to the above definition, I was trying to get the ordered pair using lower level methods. Even though I have a... more »
|
|
|
record in a locale?
|
| |
Is it correct that you cannot define a record in the context of a locale?
If so, is there a commonly used work around that is not so verbose as
nested products?
Thanks,
Randy
|
|
|
Discharging one (trivial) case without nesting the proof
|
| |
Dear Isabelle users (and devs),
Chrisoph’s question ([link]) proofs
by cases reminded me of a feature wish that I wanted to talk about for a
while.
In pen-and-paper proofs, if there are corner cases for which the result
is immediate, I just mention them at the beginning and continue with the... more »
|
|
|
32-bit libraries seem required for linux?
|
| |
Hi,
I'm running 64-bit ubuntu server, and the installation instructions currently say the 32-bit libraries are "optional, for improved performance of Poly/ML", but the libraries appear actually to be required.
A web search for the error message didn't find the solution, so I thought I'd post my experience for the next person, and maybe word will get back to the maintainer of the page with the error ([link]).... more »
|
|
|
call for applications summer school VTSA 2013
|
| |
Summer School on Verification Technology, Systems and Applications
September 2-6, 2013, Nancy, France
The summer school on verification technology, systems & applications focuses on fundamental aspects of verification techniques, their implementation, and their use for concrete applications. It is organized by the Universities of Li ge and of Luxembourg, the Max-Planck-Institut f r Informatik in Saarbr cken, and the Inria Research Center in Nancy, and will take place at the Inria Center in Nancy, France from September 2-6, 2013.... more »
|
|
|
