Brian Huffman wrote:
I would consider this as an implementation detail, and not worry about
it any further.
Tools that operate on the level of proof terms can then eliminate
eq_reflection, as was pointed out first by Stefan Berghofer some years ago,
IIRC. (I also learned from him that it is
Dominique Unruh wrote:
Dear all,
while trying to export proof terms from Isabelle, I stumbled upon the
following typing issue which might be a bug.
In HOL.thy, an axiom class ord is defined which fixes a constant
less_eq (syntactic sugar is =):
term HOL.ord_class.less_eq;
op =
Florian Haftmann wrote:
Sort constraints on constants are just a pecularity of the parser (and
can be changed internally, c.f. Sign.add_const_constraint), *not* a part
of the logical foundation. To understand, imagine you write down a
nonsense term like (x, y) = 0 ignoring the sort constraint
Florian Haftmann wrote:
Perhaps this is debatable, as one can always prove nonemptyness of
arbitrary types via hidden variables:
definition
metaex :: ('a::{} = prop) = prop
where
metaex P == (!! Q. (!! x. PROP (P x) == PROP Q) == PROP Q)
lemma meta_nonempty : PROP metaex (% x::'a::{}. x
Dominique Unruh wrote:
Dear all,
It looks like you only replied to me. ^^
thanks for the answers.
Let me summarize how I understood things, just to make clear I did not
misunderstand anything:
* Any constant is treated by the kernel as having no sort annotations.
Although this leads
Andreas Schropp wrote:
Let me put this into perspective, in the light of a forthcoming kernel
extension/modification:
in this kernel patch, all sort constaints and type class reasoning
steps are eliminated in proofterms on theorem boundaries, and strip_sorted
Sorry, I mean unconstrained
On 03/01/2010 09:28 PM, Brian Huffman wrote:
Hello all,
I am trying to use profiling to measure the performance of the HOLCF
domain package. I recently discovered that I can enable profiling in
Isabelle with the following command:
ML {* Toplevel.profiling := 1; *}
Here's the output from a
On 08/23/2010 12:30 PM, Thomas Sewell wrote:
Hello again isabelle-dev.
I should clear up some confusion that may have been caused by my mail. I was
trying to avoid repeating all that had been said on this issue, and it seems I
left out some that hadn't been said as well.
This approach avoids
On 08/24/2010 06:35 PM, Makarius wrote:
On Tue, 24 Aug 2010, Andreas Schropp wrote:
Naive questions:
* why is inspecting the whole context infeasible?
* why can't we just collect (and cache?) the Frees occuring in
assumptions managed
by assumption.ML and never delete equalities
On 08/24/2010 07:51 PM, Alexander Krauss wrote:
Andreas Schropp wrote:
On 08/24/2010 06:35 PM, Makarius wrote:
Just like global types/consts/defs, local fixes/assumes merely
generate an infinite collection of consequences. The latter is what
you are working with conceptually
On 08/24/2010 09:13 PM, Andreas Schropp wrote:
On 08/24/2010 07:51 PM, Alexander Krauss wrote:
lemma fixes x shows A x == B x
apply method
and
lemma fixes x
assumes a: A x
shows B x
apply (insert a)
apply method
Safe or not, this is obviously undesirable.
BTW: if you want to be even
On 08/24/2010 10:51 PM, Makarius wrote:
On Tue, 24 Aug 2010, Andreas Schropp wrote:
And actually any tactic can peek at the assumptions, via examination
of the hyps of the goal-state
A tactic must never peek at the hyps field of the goal state, and it
must never peek at the main goal being
On 02/09/2011 03:39 PM, Tobias Nipkow wrote:
If your analogy with lambda calculus is correct, than there are
situations when one must rename something exported from a proof block.
That I do not understand. Take this example:
lemma True
proof-
{ fix n::nat have n=n by auto }
produces ?n2 =
On 08/25/2011 10:45 PM, Florian Haftmann wrote:
Hi all,
thanks to many efforts (thanks particularly to Alex, Brian, Cezary,
Larry) we already have gained some insights whether and how it would be
technically possible to introduce a set type constructor.
Let me ask something stupid:
why
On 08/25/2011 11:26 PM, Florian Haftmann wrote:
Hi Andreas,
Let me ask something stupid:
why exactly do you guys axiomatize 'a set?
Sure it's admissable and all, but why not do this definitionally
via the obvious typedef?
the answer is rather technical: »typedef« in its current
On 08/26/2011 01:08 PM, Makarius wrote:
On Thu, 25 Aug 2011, Andreas Schropp wrote:
Of course I am probably the only one that will ever care about these
things, so whatever.
I have always cared about that, starting about 1994 in my first
investigations what HOL actually is -- there are still
On 08/26/2011 06:33 PM, Brian Huffman wrote:
This approach would let us avoid having to axiomatize the 'a set type.
Thanks for trying to help me, but as I said:
axiomatized set is just a slight inconvenience for me, so if you go for
sets as a seperate type don't bother introducing a new
On 08/26/2011 06:50 PM, Tobias Nipkow wrote:
I agree. Since predicates are primitive, starting from them is appropriate.
Tobias
Did I get this right:
the idea is to implement our advanced typedef via a HOL4-style
predicate typedef?
That doesn't work because HOL4-style typedefs don't
On 08/26/2011 07:08 PM, Brian Huffman wrote:
What exactly are our extensions to typedef?
I enumerated them in the other thread:
local typedefs, sort constraints on type parameters,
overloaded constants in representation sets.
Hopefully I am not missing others.
My understanding of the
On 08/26/2011 07:08 PM, Brian Huffman wrote:
As far as I understand, the typedef package merely issues global
axioms of the form type_definition Rep Abs S, as long as it is
provided with a proof of EX x. x : S.
The global axiom is
EX x. x : A == type_definition Rep Abs A
allowing local
On 08/26/2011 10:38 PM, Makarius wrote:
What is gained from that apart from having two versions of typedef?
I am with you here.
We don't need two primitive versions of typedefs.
The only thing that might be sensible from my POV is using predicates
instead of
sets in the primitive version
On 08/26/2011 11:08 PM, Brian Huffman wrote:
On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schroppschr...@in.tum.de wrote:
locale bla =
assume False
typedef empty = {}
Now I have to put up with the fact the semantic interpretation of empty is
the empty set. Formerly only non-empty sets
On 08/31/2011 04:21 PM, Andreas Schropp wrote:
On 08/30/2011 08:12 PM, Brian Huffman wrote:
However, the nonemptiness proof does rely on type class assumptions:
Indeed, {A. ~ finite A} is actually empty for any finite type 'a.
I think I get your point now: assumptions for type class
On 08/24/2011 08:30 PM, Florian Haftmann wrote:
I don't think it's possible to have it both ways. We need to either say we are
making this change (and then pushing it through) or not making this change.
Having full compatible versions indeed is illusive.
Why exactly?
From a naive POV
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
Good day all. Just wanted to let the Isabelle developers know about the latest
feature David Matthews has added to PolyML, and to let you all know how useful
it is.
The feature allows profiling of objects after garbage collection. When code is
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
There are surprisingly many dummy tasks.
[...]
918632 Task_Queue.dummy_task(1)
val dummy_task = Task(NONE, ~1)
Values are not shared?! What the hell?
___
isabelle-dev mailing list
Hi Isabelle people, esp. Makarius,
it has come to my attention that attributes are
called with a theory, a proof context and a local theory
in this succession.
Is this transforming the input lthy onion from inside out?
The implementation manual states that I have to treat
all of them uniformly.
On 11/13/2011 05:16 PM, Makarius wrote:
On Thu, 10 Nov 2011, Andreas Schropp wrote:
The implementation manual states that I have to treat all of them
uniformly. This means that the attribute transformation on a lthy
would not result in an update of the target context but of the
auxilliary
On 08/04/2013 07:09 PM, Florian Haftmann wrote:
To add a further dimension to the design space, there was once the idea
of a generalized primrec in the manner:
1. recursive specification following some pattern considered »primitive«
2. foundational definition of this specification using a
29 matches
Mail list logo
