On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
wrote:
> HOL-Probability FAILED
This is now fixed in the main repo; the following changeset should be
merged back into isabelle_set:
http://isabelle.in.tum.de/repos/isabelle/rev/c10485a6a7af
___
isabell
On Fri, Aug 26, 2011 at 5:45 AM, Florian Haftmann <
florian.haftm...@informatik.tu-muenchen.de> wrote:
>
> [...] According to my knowledge, the following session produce
> problems: [...]
> HOL-Quotient_Examples FAILED
>
Please propagare the isabelle changeset:
http://isabelle.in.tum.de/repos/isab
On Fri, Aug 26, 2011 at 2:02 PM, Andreas Schropp wrote:
>
> So you suggest using e.g.
> if EX x. x : A then A
> else {0}
> instead of A as the semantic interpretation?
> Interesting!
Yes, this is exactly the kind of thing I meant. You could use any
nonempty set you want in place of {0}, of cour
On 08/26/2011 11:08 PM, Brian Huffman wrote:
On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp 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 were semantic inter
On 08/26/2011 11:08 PM, Makarius wrote:
On Fri, 26 Aug 2011, Andreas Schropp wrote:
This is not really a problem, but complicates my conservativity
argument. Before local typedefs the proof of (EX x. x : A) was
global. Actually Makarius' attitude on this was that those
non-emptiness proofs "s
On Fri, 26 Aug 2011, Andreas Schropp wrote:
Most importantly you are missing (indirectly) overloaded constants in
representing sets of typedefs. E.g.
typedef 'a matrix = {f . finite (nonzero_positions f) }
depends on nonzero_positions, which depends on the
overloaded constant zero['a].
If we tr
On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp 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 were semantic interpretations of
> type constructors. The way
On Fri, 26 Aug 2011, Andreas Schropp wrote:
This is not really a problem, but complicates my conservativity argument.
Before local typedefs the proof of (EX x. x : A) was global. Actually
Makarius' attitude on this was that those non-emptiness proofs "should be
global most of the time", but he
On Fri, 26 Aug 2011, Brian Huffman wrote:
What is gained from that apart from having two versions of typedef?
In the current version of Isabelle, not much (although I personally
think that a predicate-based variant of typedef would have value). But
assuming we go ahead and reintroduce "'a se
On 08/26/2011 10:51 PM, Makarius wrote:
On Fri, 26 Aug 2011, Andreas Schropp wrote:
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 :
On 08/26/2011 10:50 PM, Brian Huffman wrote:
On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp wrote:
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 typede
On Fri, 26 Aug 2011, Andreas Schropp wrote:
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
On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp wrote:
> 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.
This is incorrect: Only the predicate-based typed
The global axiom is
EX x. x : A ==> type_definition Rep Abs A
allowing local typedefs whenever non-emptiness of A is
derivable, even using assumptions in the context.
This is an interesting discussion, but totally off-topic in this thread
(whose main content is already growing very large.)
On Fri, Aug 26, 2011 at 1:38 PM, Makarius wrote:
> On Fri, 26 Aug 2011, Brian Huffman wrote:
>
>> Here's one possible approach to the set-axiomatization/typedef issue:
>>
>> As a new primitive, we could have something like a "pred_typedef"
>> operation that uses predicates. This would work just li
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 (fea
On Fri, 26 Aug 2011, Brian Huffman wrote:
Here's one possible approach to the set-axiomatization/typedef issue:
As a new primitive, we could have something like a "pred_typedef"
operation that uses predicates. This would work just like the
new_type_definition facility of HOL4, etc.
The type
On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
wrote:
> HOL-Hoare_Parallel FAILED
> Also Hoare_Parallel is non-terminating.
I have a patch for this one:
http://isabelle.in.tum.de/repos/isabelle/rev/5e681762d538
Once this changeset gets merged into the isabelle_set repo,
Hoare_Parallel shoul
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 l
On 08/26/2011 07:02 PM, Brian Huffman wrote:
With ordinary "typedef", I have to do this:
typedef (open) bar = "{x. is_bar x}"
But then it generates rules of the wrong form:
x : {x. is_bar x} ==> Rep_bar (Abs_bar x) = x
Rep_bar x : {x. is_bar x}
And I have to do an extra step to get the rules
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 lo
On Fri, Aug 26, 2011 at 9:43 AM, Andreas Schropp wrote:
> On 08/26/2011 07:02 PM, Brian Huffman wrote:
>>
>> I didn't suggest the idea merely for your benefit. I think this
>> approach would give Isabelle a nicer, simpler logical foundation.
>>
>>
>
> What is this logical foundation of Isabelle th
On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp wrote:
> 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 predi
On 08/26/2011 07:02 PM, Brian Huffman wrote:
I didn't suggest the idea merely for your benefit. I think this
approach would give Isabelle a nicer, simpler logical foundation.
What is this logical foundation of Isabelle that you have in mind?
AFAIK I am the only trying to provide a semantic
On Fri, Aug 26, 2011 at 9:20 AM, Andreas Schropp wrote:
> 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 yo
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 featur
I agree. Since predicates are primitive, starting from them is appropriate.
Tobias
Am 26/08/2011 18:33, schrieb Brian Huffman:
> Here's one possible approach to the set-axiomatization/typedef issue:
>
> As a new primitive, we could have something like a "pred_typedef"
> operation that uses predi
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 p
Here's one possible approach to the set-axiomatization/typedef issue:
As a new primitive, we could have something like a "pred_typedef"
operation that uses predicates. This would work just like the
new_type_definition facility of HOL4, etc.
The type "'a set" could be introduced definitionally usi
I took a look at some of these. HOL-Library fails in your own Cset.thy, where
presumably you know what you are doing (particularly as this theory involves
execution I should stay away from it). Similarly I'm not sure I'm the right
person to fix HOL-Nominal or HOL-MicroJava. PG is very fragile ju
Thank you, that may be a useful workaround. But isn't the current behaviour
simply wrong? It transforms a monotonicity theorem into something of the wrong
format.
Larry
On 26 Aug 2011, at 17:07, Brian Huffman wrote:
> On Fri, Aug 26, 2011 at 7:06 AM, Lawrence Paulson wrote:
>> I am trying to p
On Fri, Aug 26, 2011 at 7:06 AM, Lawrence Paulson wrote:
> I am trying to process the following declaration in Probability/Sigma_Algebra:
>
> inductive_set
> smallest_ccdi_sets :: "('a, 'b) algebra_scheme \ 'a set set"
> .
> .
> .
> monos Pow_mono
>
> I get the following error message (for t
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
I am trying to process the following declaration in Probability/Sigma_Algebra:
inductive_set
smallest_ccdi_sets :: "('a, 'b) algebra_scheme \ 'a set set"
.
.
.
monos Pow_mono
I get the following error message (for the version with set types):
*** Bad monotonicity theorem:
*** {x. ?A x
I shall take a look at this one. If anybody else is working on it, please let
me know as soon as possible.
Larry
On 25 Aug 2011, at 21:45, Florian Haftmann wrote:
> HOL-Probability FAILED
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://ma
On Thu, 25 Aug 2011, Andreas Schropp wrote:
Haha, very funny! We are a long distance from the "ancient HOL
primitive" already: local typedefs, sort constraints on type parameters,
overloaded constants in representation sets. Perhaps you remember there
was quite a suprise regarding those "meta-
On Thu, 25 Aug 2011, Florian Haftmann wrote:
I remember that once there was a discussion how AFP theories could be
referenced in theory headers using an environment variable AFP_THEORIES
or something similar.
Maybe the afp could be turned into an optional Isabelle component, e.g.
at ~~/contri
Florian,
Amongst the set/pred emails this one doesn't seem to have garnered much
response:
On 17/08/2011, at 9:18 PM, Florian Haftmann wrote:
> I repeatedly stumble over duplication among the Isabelle distribution
> and the AFP [..]
I too would be keen to see some way of moving reusable (espec
indeed yes I'm the person who decided that this primitive should introduce a
type as a copy of an existing non-empty set. I have always preferred sets to
predicates and the examples I have looked at lately have only strengthened my
view. Not to mention numerous occasions when people have re-inve
39 matches
Mail list logo
