Re: [isabelle-dev] Problem exception TYPE raised: Loose bound variable
Makarius wrote: It is not so easy to get an exception trace here. Wrapping up Simplifier.generic_simp_tac as shown in the included changeset produces the following result: Exception trace - TYPE (Loose bound variable: B.7, [], [Bound 7]) Sign.type_check(2)typ_of(2) [...] Splitter().mk_case_split_tac(1)inst_lift(7) Hi all, this bug has now been fixed in the development version of Isabelle (see c0c453ce70a7). It has been present at least since 1995 (see e.g. 1d8fa2fc4b9c). The problem occurred when the head of a term (called h in function mk_cntxt) on the path leading to an abstraction that needs to be removed happened to be a bound variable. To avoid this problem, inst_lift now fully instantiates the variable P (denoting the context in which the abstraction occurs) in the trlift theorem and applies it using compose_tac rather that rtac. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] auto raises a TYPE exception
On 05/27/2013 07:54 PM, Makarius wrote:
Here is another example for Isabelle/Pure, without schematic variables with
different types. It may be be tried before/after my change 3b9c31867707 from
today:
[...]
ML {*
val read = Syntax.read_term (Proof_Context.set_mode
Proof_Context.mode_schematic @{context});
val a = read a :: nat = bool;
val x = read ?x :: ?'b;
*}
ML {* Seq.list_of (Unify.hounifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
ML {* Seq.list_of (Unify.unifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
ML {* Pattern.unify @{theory} (a, x) (Envir.empty 15); *}
Before the change, Unify.hounifiers crashes; after the change it is able to
work out the type instantiation correctly. Pattern.unify is still not quite
there, neither before nor after the change.
Hi Markus,
there is a comment at the beginning of unify.ML saying that
Types as well as terms are unified. The outermost functions assume
the terms to be unified already have the same type. In resolution,
this is assured because both have type prop.
So it is the expected behaviour that the unification functions cannot cope with
the above example, since it does not satisfy this precondition.
Greetings,
Stefan
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] auto raises a TYPE exception
On 04/12/2013 02:18 PM, Makarius wrote:
Just for completeness, I am posting here a self-contained example to expose the
problem.
It looks like I need to discuss it further with Stefan Berghofer, because he
made some reforms there in 2005 that now seem to crash on us.
Hi Markus,
it is not particularly surprising that the attached example leads to a TYPE
exception. A
closer look at the disagreement pairs
[(\Andxa\Colon'a. xa \in {a\Colon'a. (?j12\Colon'a \Rightarrow nat) xa + Suc
((?n13\Colon'a \Rightarrow nat) xa) \
\ Suc ((?n6\Colonnat \Rightarrow 'a \Rightarrow nat) (?j12 xa + Suc (?n13
xa)) a)} \Longrightarrow \
\ (Q\Colon'b \Rightarrow bool) ((f\Colon'a \Rightarrow 'b)
xa),
\Andxa\Colon'a. xa \in {a\Colon'a. (?n7\Colon?'b10 \Rightarrow 'a
\Rightarrow nat) ((?a10\Colon'a \Rightarrow ?'b10) xa) a \
\ Suc ((?n6\Colon?'b10 \Rightarrow 'a \Rightarrow
nat) (?a10 xa) a)} \Longrightarrow \
\ (Q\Colon'b \Rightarrow bool) ((f\Colon'a \Rightarrow 'b)
xa)),
(?n13\Colon'a \Rightarrow nat,
\lambdaxa\Colon'a. (?n6\Colonnat \Rightarrow 'a \Rightarrow nat) ((?j12\Colon'a
\Rightarrow nat) xa + Suc ((?n13\Colon'a \Rightarrow nat) xa)) xa),
(\lambdaxa\Colon?'b10. (?n7\Colon?'b10 \Rightarrow 'a \Rightarrow nat) xa
(x\Colon'a),
\lambdaxa\Colon?'b10. (?n6\Colon?'b10 \Rightarrow 'a \Rightarrow nat) xa
(x\Colon'a))];
reveals that the variable ?n6 indeed appears with two distinct types: In lines
2 and 8, it has type
nat = 'a = nat, whereas in lines 5 and 10, it has type ?'b10 = 'a =
nat. This is clearly an
error, and therefore the exception is justified. An interesting question is why
Thm.bicompose_aux
supplies these ill-formed disagreement pairs to Unify.unifiers in the first
place.
Note that before the reforms mentioned above, most of the substitution
functions used in unify.ML
simply ignored types and therefore were likely to produce ill-formed terms when
applied to terms
containing variables with same name but different types.
Greetings,
Stefan
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Max threads Sledgehammer
Hi Markus, On 01/07/2013 10:45 AM, Makarius wrote: On Fri, 4 Jan 2013, Stefan Berghofer wrote: I am currently getting an exception Thread Thread creation failed after some time when compiling HOL with PolyML 5.5.0 on a machine with quite a few CPUs (I am using Isabelle repository version 30bcdd5c8e78). I have the impression that Isabelle just tries to create as many threads as there are CPUs, which exceeds the maximum number of threads allowed by the operating system for a single process. Can you say more about the hardware and operating system here? How many CPUs do you have? it's a server with 24 CPUs of the type Intel(R) Xeon(R) CPU E7450 @ 2.40GHz and 132299948 kB RAM. The operating system is Linux ts-2 3.2.0-0.bpo.4-amd64 #1 SMP Debian 3.2.35-2~bpo60+1 x86_64 GNU/Linux. I've seen problems creating threads on the JVM (e.g. see f7ba30a816b9), but not for Poly/ML 5.5.0. Also note that the default (threads=0) is bounded by 8 at the moment. What could happen here nonetheless is that Poly/ML tries to fork too many GC threads. This was indeed the problem. So how many cores do you have? I reckon it should work until 32 at the least. Well, obviously not :-( You could try ML_OPTIONS=--gcthreads 8 in one of your settings. I tried it successfully with --gcthreads 4, which looks like a reasonable value that is also used in some of the Admin/isatest/settings files. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Max threads Sledgehammer
Hi David, On 01/07/2013 12:31 PM, David Matthews wrote: Is there a limit on the number of threads per process in Linux? I haven't been able to find anything about it. Neither have I. You could certainly hit limits on memory for stacks with a large number of threads particularly if the default stack size is large. What does ulimit -s say? You could try setting that smaller. ulimit -s says 102400 By default without the --gcthreads option Poly/ML 5.5 creates one garbage collection thread for each processor. That's probably more than are useful if you have 24 processors so -gcthreads 4 or 8 might well be a sensible setting. Thanks for the explanation. --gcthreads 4 worked fine for me. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Max threads Sledgehammer
Hi David, On 01/07/2013 12:45 PM, David Matthews wrote: What does Thread.Thread.numProcessors() report? That's the number that will be used for the GC threads. It reports 24. I'm not inclined to put an arbitrary limit on the number of threads. There are certain parts of the GC process such as the sharing detection that can use as much parallelism as there is available. Other parts seem to max out at only a few processors. I'll bear this in mind. The parallel GC is very new and we need some experience of how it works out in practice and whether it needs some tuning. I agree. As long as I can work around the problem by setting --gcthreads to an appropriate value, that's fine for me. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Conversions between ('a * 'a) set and 'a = 'a = bool relations
Florian Haftmann wrote: * This is mainly a question to Stefan: there are some theorems commented out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes. I guess this is due to a higher-order situation, but I would be reassuring if you can confirm that. Hi Florian, I have fixed this bug now, see changeset b1d15637381a. Note that converting the above theorem (and the other theorems in Relation.thy marked with FIXME) to predicate notation requires the generalized versions of theorems INF_INT_eq2 and SUP_UN_eq2, which should replace the more specific versions. Unfortunately, the Relation theory is currently a bit of a mess. Larger blocks of conversion lemmas are commented out for no good reason, which means that they are not tested by our nightly builds, and for some of them it still remains to be examined whether they can be added to the database of predicate/set conversion rules by default without breaking any of the examples in the AFP. What is the strategy for cleaning up this theory? Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Conversions between ('a * 'a) set and 'a = 'a = bool relations
Florian Haftmann wrote: * This is mainly a question to Stefan: there are some theorems commented out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes. I guess this is due to a higher-order situation, but I would be reassuring if you can confirm that. Hi Florian, this looks like a bug. The culprit seems to be function mk_to_pred_inst in inductive_set.ML, which does not handle variables of type ... = T set properly. A similar problem might also occur with to_set. I'll try to fix this before the next release. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] inductive_set vs. 'a set
Quoting Lawrence Paulson l...@cam.ac.uk:
I got this message several times when converting theories. There is
a workaround, but nevertheless, I think this is a bug.
Hi Larry,
the reason for this problem is the removal of the rules pred_equals_eq and
pred_subset_eq from the rule database used for the predicate / set conversion:
http://isabelle.in.tum.de/repos/isabelle/rev/a6cb51c314f2
The conversion of lists_mono to predicate notation already failed before the
re-introduction of the set type, but this did not cause an error message
because the monotonicity rule for listsp was already part of the database
of monotonicity rules, and the ill-formed monotonicity rule was simply
ignored. Now that sets are no longer predicates, the conclusion of the
ill-formed rule
{x. ?A x} = {x. ?B x} == {x. listsp ?A x} = {x. listsp ?B x}
is no longer an inequality between predicates, and so the rule is rejected.
I will revert (parts of) the above changeset, and maybe also the related ones
http://isabelle.in.tum.de/repos/isabelle/rev/0af0f674845d
http://isabelle.in.tum.de/repos/isabelle/rev/a27607030a1c
Do you still remember in which theories you applied your workaround?
Maybe we should take a look at them again.
Greetings,
Stefan
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Divergent renames
Quoting Makarius makar...@sketis.net: On Thu, 1 Dec 2011, Jasmin Christian Blanchette wrote: I just pulled and updated (hg pull -u) from the main repository and got these strange warnings: Fügte 118 Änderungssätze mit 572 Änderungen zu 411 Dateien hinzu warning: detected divergent renames of src/Pure/General/markup.ML to: [...] Anybody knows whether they're harmful? Good question. There is a brief explanation at http://hgbook.red-bean.com/read/mercurial-in-daily-use.html in the section Divergent renames and merging. Hi, I just got the very same warnings when updating my copy of the Isabelle sources. I already got similar warning messages warning: detected divergent renames of src/HOL/Tools/Sledgehammer/sledgehammer.ML to: src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML src/HOL/Tools/Sledgehammer/sledgehammer_run.ML a while ago (January 2011). When I asked Markus about this, he replied to me that he had noticed them as well, but ignored it, and that he had not discovered any negative effects so far. Maybe it is time to look at this issue again rather than ignoring it? Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Alexander Krauss wrote: In particular, Stefan discovered that replacing inductive set definitions by predicates was by no means as easy as everybody had expected. One good example is the small-step relation from Jinja and its various cousins. It had type ((expr * state) * (expr * state)) set, and turning it into a 4-ary predicate (expr = state = expr = state = bool) would cause problems with either version of the transitive closure operator. [Btw, the newer HOL/IMP/Small_Step.thy uses a binary predicate over pairs, which requires massaging the induction rule using [split_format (complete)]]. Hi all, let me take the opportunity to advertise a useful feature of the induct method that avoids such manual massaging of induction rules. For example, the command proof(induct rule: small_step_induct) in HOL/IMP/Types.thy can be replaced by proof(induct (c,s) (c',s') arbitrary: c s c' s' rule: small_step.induct) which allows the standard induction rule small_step.induct to be used instead of the small_step_induct rule produced using split_format, which is a bit of a hack anyway. The above is a shorthand for proof(induct x==(c,s) y==(c',s') arbitrary: c s c' s' rule: small_step.induct) Since revision b0aaec87751c (Jan 2010), the equational constraints arising from such invocations of induct are solved automatically using injectivity / distinctness rules for datatypes, so the rest of the proof script works as if the custom-made induction rule had been applied. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Alexander Krauss wrote: I want to emphasize that the limitation of the code generator mentioned here not only applies to sets-as-predicates but also to maps-as-functions and other abstract types that are often specified in terms of functions (finite maps, almost constant maps, etc.). Thus, having good old 'a set back is does not fully solve this problem as a whole, just one (important) instance of it. My view on this whole topic is outlined in the report I recently sent around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated since last time). In the long run, I would prefer to see flexible transport machinery to move stuff between isomorphic types. Hi Alex, thanks for your excellent report, I fully agree with this view. There is often a tradeoff between executability and conciseness / abstractness of specifications, so I don't think it is a good idea to tweak the logic in such a way that it is more suitable for code generation. For example, HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element from the worklist, which is highly non-executable but more abstract, since one does not have to commit to a particular strategy for selecting the element. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Tobias Nipkow wrote: Am 12/08/2011 11:27, schrieb Alexander Krauss: On 08/12/2011 07:51 AM, Tobias Nipkow wrote: The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Do you know of any more pain, apart from what Florian already mentioned? I think he omitted to mention type classes. It comes up again and again on the mailing list. Really? In the thread http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/ cited by Brian and Alex, Brendan was worried about the fact that one could no longer declare arities for sets. In my reply to his mail, I pointed out that arities for sets could usually be rephrased as arities for functions and booleans. I also asked him to give a concrete example for an arity where this was not possible, but I never got a reply, so I assume that this is not so much of a problem. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Florian Haftmann wrote: just do something like (unfold mem_def) and your proof will be a mess since you have switched to the wrong world. Like any definition of a primitive operator, mem_def is not really intended to be unfolded by the user, so don't be surprised if your proof is a mess after unfolding this definition. You wouldn't unfold the definitions of logical operators like conj or disj either, except for proving introduction- or elimination rules for these operators. * The logical identification of sets and predicates prevents some reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x = A x B x because then expressions like set xs |inter| set ys behave strangely if the are eta-expanded (e.g. due to induction). This sounds more like a problem with the underlying infrastructure that should be fixed, rather than working around the problem by introducing new type constructors. Can you give an example of a proof by induction, where eager eta expansion leads to an unnecessarily complicated proof? Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Odd failure to match local statement with pending goal.
Quoting Alexander Krauss kra...@in.tum.de: The same can be done in low-level ML, using just rtac, which suggests that the error is somewhere in the underlying Thm.biresolution etc. So far, I have not looked any further... Hi Alex and Larry, I guess the culprit is function rename_bvs in Pure/thm.ML, which is used by bicompose_aux. The rationale behind this function is to make rule applications preserve as many of the variable names in the goal as possible, to make it more readable for the user. According to the comment before this function, it renames all bound variables and some unknowns, and I think the some unknowns part is causing the problem. In your example the conclusion of rule R with bound variables s and t is matched against a goal where both bound variables are named c, which causes rename_bvs to rename both schematic variables ?s and ?t in R to ?c. The function already contains a rudimentary check for name clashes, but this has to be extended. Thanks again for narrowing down the problem! Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML
Quoting Lawrence Paulson l...@cam.ac.uk: But I could be wrong, as such checks may be done elsewhere. Does anybody else have a suggestion? Hi Larry and Andreas, there is another occurrence of gconv_rule in Provers/blast.ML (in function timing_depth_tac). Since the exception is thrown when invoking blast, this occurrence of gconv_rule may be the culprit. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
Quoting Lukas Bulwahn bulw...@in.tum.de: Hi, My changes caused this error. I am working on different compilation schemes in Quickcheck. Quickcheck registers its type-class based generator construction in the Datatype package in the HOL image. Hi Lucas, according to the trace, the exception occurs somewhere in the function derive_datatype_props in datatype_data.ML. When taking a quick look at the code, I noticed that thy2 is used in two places (lines 311 and 322) after it has already been modified. Is that intentional, or could this be related to this bug, too? Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Type arguments in datatype declarations
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
The following datatype specification succeeds as expected
datatype ('a, 'b) foo = Nihil | Bar ('a, 'b) bar
and ('a, 'b) bar = Foo ('a, 'b) foo
whereas the following logically equivalent, but differently written
specification fails with a low-level exception in size.ML:
datatype ('a, 'b) foo = Nihil | Bar ('b, 'a) bar
and ('b, 'a) bar = Foo ('a, 'b) foo
Hi Florian,
this is a perfectly legal datatype and therefore should be handled by
the datatype package without prior consolidation or whatever, but
I think this case has just been overlooked when reimplementing the
definition of the size functions using the new infrastructure for
datatype interpretations. I'll try to find out what exactly goes wrong.
Greetings,
Stefan
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Type arguments in datatype declarations
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: thanks for this offer. But this misperception has not only infected size but all datatype tools using the Datatype_Aux.interpret_construction combinator which assumes exactly the same restriction. Therefore my proposal to internally provide a consolidated view of the datatype specifications with type parameter names made uniform, to handle the issue at one place and not in every datatype package extension separately. Hi Florian, why can't we repair interpret_construction so that it handles this case properly? Nevertheless, it would be interesting to see what goes wrong, since your example used to work in older releases of Isabelle without further ado. Greetings, Stefan ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Function package produces duplicate rewrite rule warnings
On 03/05/10 22:34, Brian Huffman wrote: The datatype package produces some extra warning messages now too: ### Ignoring duplicate rewrite rule: ### True == induct_true ### Ignoring duplicate rewrite rule: ### False == induct_false I haven't checked, but I would be willing to bet that this behavior was introduced by the same changeset as the function package warning messages. I wouldn't be surprised if warnings pop up in other packages as well. Hi Brian, no, these warning messages had a different reason. I introduced this problem when adding new infrastructure for the pre-simplification of goals produced by the induct and cases methods. These methods now delete trivial goals (corresponding to cases that cannot occur) and simplify non-trivial goals using injectivity and distinctness theorems for datatypes (as well as other rules that can be declared by the user). The above warning was generated by the code for preprocessing these simplification rules. It should no longer occur in the current repository version of Isabelle. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: bergh...@in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3Room: 01.11.059 85748 Garching, GERMANYhttp://www.in.tum.de/~berghofe ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Multicore performance preview
Makarius wrote: You will need the latest Poly/ML 5.2.1 version to prevent a strange GC deadlock problem in 5.1/5.2. Where can I get the latest version? The latest version offered for download on the Sourceforge page http://sourceforge.net/project/showfiles.php?group_id=148318package_id=163589 is still 5.2 Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3Room: 01.11.059 85748 Garching, GERMANYhttp://www.in.tum.de/~berghofe
[isabelle-dev] NEWS: quickcheck with functions
Dear all,
quickcheck can now also display counterexamples involving functions (using
notation for function updates). For example,
consts app: ('a = 'a) list = 'a = 'a
primrec
app [] x = x
app (f # fs) x = app fs (f x)
lemma app (fs @ gs) x = app fs (app gs x)
quickcheck
oops
now yields something like
Counterexample found:
fs = [arbitrary(0 := -1)]
gs = [arbitrary(0 := 0, -1 := 0)]
x = 0
Greetings,
Stefan
--
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3Room: 01.11.059
85748 Garching, GERMANYhttp://www.in.tum.de/~berghofe
[isabelle-dev] quickcheck on type real
Amine Chaieb wrote: This is perhaps an occasion to advertise Library/Executable_real.thy, which contains a verified implementation of rational numbers to be have like HOL --- So here you would no get an exception when dividing by zero, but just zero as you expect. [...] Brian Huffman wrote: Hello all, I would like to report some bugs I found when using quickcheck on lemmas involving division on reals. When auto_quickcheck is enabled (which it is by default) these bugs cause the lemma command to fail, preventing me from even attempting a proof. The first bug is that sometimes quickcheck fails with a DIVZERO exception. [...] The other bug is a false counterexample; I have no idea what causes it: Hello all, the code generator setup contained in the theories Library/Executable_Real.thy and Library/Executable_Rat.thy have now been integrated into the theories Real/RealDef.thy and Real/Rational.thy. Moreover, I modified the setup in such a way that it also works with the old code generator and therefore with quickcheck, so the abovementioned bugs should now be fixed. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3Room: 01.11.059 85748 Garching, GERMANYhttp://www.in.tum.de/~berghofe
