Hi all,
I tried to build (my own version of) JinjaThreads with the Isabelle
repository version 8cce3a34c122, but it failed with the error message
"Failed to prepare dependency graph". The log of the run ends with:
Loading theory "JinjaThreads"
### Rule already declared as safe introduction (int
> On 17/12/2010, at 10:03 PM, Makarius wrote:
>> On Fri, 17 Dec 2010, Gerwin Klein wrote:
>>> Andreas Lochbihler pointed out that the AFP test is still running polyml
version 5.3 as is most of isatest.
>>>
>>> Any arguments against moving all of this to po
> Are there still users of PG 3.x with recent Isabelle snapshots or versions
> from the repository?
I am using PG 3.7.1.1 with XEmacs 21.4.21 and a recent version from the
Isabelle repository. My motivation for not switching is that PG 4.x did not
seem to work with XEmacs when I tried, and I hav
l exists nor an
exception handler. But I could be wrong, as such checks may be done elsewhere.
Does anybody else have a suggestion?
Larry
Begin forwarded message:
From: Andreas Lochbihler
Date: 27 May 2011 14:51:27 GMT+01:00
To: isabelle-users
Subject: [isabelle] Exception in conv.ML
Hi
g_depth_tac). Since the exception is thrown
when invoking blast, this occurrence of gconv_rule may be the
culprit.
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 60
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.
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Loch
,
Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76
ne] = test_rev test_rev[folded List.null_def]
setup {* Code_Preproc.map_pre (fn ss => ss addcongs [@{thm conj_cong}]) *}
code_thms test2
test2 is still implemented in terms of "test (rev xs)"
How can I unfold test_rev in test2_def?
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas
I am afraid, no. Larry's fix solved the problem for me, so I did not dig any
deeper.
Andreas
Am 09.06.2011 14:29, schrieb Makarius:
On Mon, 30 May 2011, Andreas Lochbihler wrote:
This fix solves the problem with the exception. I tried it with 574613b47583.
Can you add it to the repos
about 12G of memory plus a few more when the heap image is
written.
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-M
uot;
assumes "sorted (map key xs)"
and "\xs. P xs []"
and "\xs y ys. sorted (map key xs) \
P (dropWhile (\x. key x \ key y) xs) ys
\ P xs (y#ys)"
shows "P xs ys"
using assms(2-) assms(1)
apply(induction_schema)
Andreas
--
Karlsruher Institu
ences_induct)
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT
ption is still required. IIRC, I added that
option in 2009 because some glyphs were only availabe when French was loaded,
possibly something with >> and <<.
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerrin
test the subsumed marker of the AFP ;-)
Who is going to move the entry?
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail
ations for interpretation. This possibly
also applies to the where clause although I did not need that for FinFun.
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +
Threads/Examples/BufferExample.thy")
This is probably related to my reworking of FinFuns. I'll try to fix it today.
Best,
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsru
Hi Stefan,
while doing a "testall" on the AFP, I noticed that JinjaThreads no longer
compiles. I get the error
*** exception Match raised (line 146)
***
*** At command "ML" (line 145 of
"/mnt/home/berghofe/isabelle/afp/thys/JinjaThreads/Examples/BufferExample.thy")
This should be now fixed in
rameter appear in a constant's type. Typically in Isabelle,
such constants take an additional argument 'a itself for that purpose, but this
generates less efficient code than boxing values in phantom types of which the
ML/Haskell compiler gets rid again.
Andreas
--
Karlsruher Institut für
rd_class.bar" :: "'b :: ord => 'b :: ord => bool"
b) In (* 2 *), foo and bar both refer to the global constants foo and bar with
sort constraint ord. However, "thm foo_def" prints
foo (?p :: ?'a :: ord) (?n :: ?'a :: ord) = (?n < ?p)
wh
Hi Makarius,
> Side remark:
>
> Does anybody remember a use of the 'apply_end' command?
Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although they
could be fused into the qed. However, I regularly use apply_end when I develop
the method call for qed to finish off all the rema
Hi Amine,
the error message in the second case is only delayed: You get it, once
you open the AB context again (context AB begin). In the first case, it
shows up immediately, because the sublocale command already constructs
the context AB enriched with B.
Best,
Andreas
On 01/31/2013 12:48 P
rote:
Thanks Andreas. Does this mean that this sublocale scenario is
prohibited? And if so, is it due to technical reasons or is there a
fundamental problem here?
Amine.
On 01/31/2013 02:04 PM, Andreas Lochbihler wrote:
Hi Amine,
the error message in the second case is only delayed: You get it,
Dear all,
in the repository (8a635bf2c86c) and in Isabelle2013, there seems to be
something wrong with the enat_eq_cancel simproc in Extended_Nat. Can
someone please look into this? Here's a minimal example:
theory Scratch imports
"~~/src/HOL/Library/Extended_Nat"
begin
definition epred ::
Here's a summary of the story with Containers:
AFP/db25a6127308 to AFP/58dc11da7731 add the Containers entry to AFP-devel in the version
that works with Isabelle2013.
In AFP/664abd899c58, Gerwin dropped the import of Code_Char_ord that Florian removed in
Isabelle/599ff65b85e2. This implicitly
Sorry for the confusion, I never ran sitegen.py myself because I thought that to be the
priviledge of the editors. As Gerwin has found out, I dropped these links manually in
376347e6131a because they all were broken after the update on sourceforge. I decided not
to update them for three reasons:
Hi Florian,
Thanks a lot for fixing this. It now works like a charm.
Andreas
On 29/06/13 08:34, Florian Haftmann wrote:
Hi Andreas,
ML {* Code_Simp.dynamic_value @{theory} @{term example} *}
ML {* Nbe.dynamic_value @{theory} @{term example} *}
The last line just raises Option (line 81 of Ge
Hi Johannes,
I have often run into this problem myself, too, especially in case of non-termination. I
would find it sensible that code_abort deletes the code equation.
Andreas
On 09/07/13 15:28, Johannes Hölzl wrote:
Hi *,
code_abort does not remove the corresponding code equations
(in Isab
Hi Florian,
On 18/07/13 12:00, Florian Haftmann wrote:
Should code_abort remove the code equation for test? Otherwise the
resulting program might be non-terminating.
I have often run into this problem myself, too, especially in case of
non-termination. I would find it sensible that code_abort
Hi Florian,
On 18/07/13 15:07, Florian Haftmann wrote:
The idea is to have an explicit delete declaration, e.g. something like
definition error_case_for_f where [code del]: "error_case_for_f = f"
which will both have the effect of leaving no code equations for
error_case *and* generate excepti
Hi Christian,
the two different size functions become relevant as soon as you have a polymorphic
datatype such as
datatype 'a foo = Foo 'a | Bar "'a foo"
Then, foo_size takes size function for every type variable as additional parameters and
takes them into account, whereas size ignores occu
Hi René,
Florian has reworked the setup for target language numerals. I can at least explain why
you run into the error and provide a workaround.
Code_Target_Nat implements the type nat as an abstract type (code abstype) with
constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must not
Dear all,
in Isabelle abd760a19e22, I get the error "Attempt to perform non-trivial merge of
theories" when I include a bundle from another theory and there are at least two imports.
In the attachment, there's an example.
Best,
Andreas
Scratch.thy
Description: application/extension-thy
Scr
Hi René,
I now pushed this the repository (1774d569b604), but I reuse the existing constant
nat_of_integer instead of a new one.
Andreas
On 12/08/13 13:47, René Thiemann wrote:
Hi Andreas,
Code_Target_Nat implements the type nat as an abstract type (code abstype) with
constructor Code_Tar
2013, Andreas Lochbihler wrote:
I get the error "Attempt to perform non-trivial merge of theories" when I
include a
bundle from another theory and there are at least two imports. In the
attachment,
there's an example.
This should work in Isabelle/ef65d5ee60cf. Are there any rem
Two months ago, Florian replaced code_module with code_identifier (6646bb548c6b). Now, I
am having trouble using the greater capabilities of code_identifier. I would like to
assign a constant to a different module, say
code_identifier constant replicate \ (SML) "My_Module.rep"
Then, code gener
Hi Florian,
newtype in Haskell is not always for free, see for example Joachim's blog post:
http://www.joachim-breitner.de/blog/archives/610-Adding-safe-coercions-to-Haskell.html
Andreas
On 19/09/13 12:58, Florian Haftmann wrote:
Hi Peter,
When using Code_Target_Numeral instead of the old
Hi Jasmin,
I moved this thread from users to devel, because we are now referring to
changesets ;-).
I would appreciate if all these code_aborts that you mention were consolidated
to use Code.abort.
I second this. Cf. http://goo.gl/4kR3vu :)
See now 788730ab7da4, which replaces all code_abo
Hi Florian,
in 2b761d9a74f5, I now have replaced Predicate.not_unique with Code.abort. I decided to
leave Enum.the as is, because there is a special translation for the Eval target such that
Enum.the raises Match instead of Fail (although I do not know whether the specific setup
is important).
we don't want to force users to
have any ordering on list)?
c) If List_lexord is not imported, but the type class instance for String.literal is
required, the generated Haskell code does not compile.
Do you have any ideas or opinions on that?
Best,
Andreas
PS: Similar problems already o
Hi Florian,
a) Char_ord and List_lexord are not tied together, i.e., a user could
import List_lexord, but not Char_ord, define his own version of order on
String.literal and the generated Haskell code compiles, but it is
unsound (even without any further adaptations by the user). One could
solve
Hi Florian,
> Just a remark on
> http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on
> lexicographic orderings in List.thy is now numerous enough but still
> self-contained to justify a separate theory Lexorder.thy.
I agree that a separate theory would be nice. But before do
Hi Jasmin,
In addition, "option" and "list" are now defined using "datatype_new" and registered as
old-style datatypes using "datatype_new_command". I have yet to do some clean up with the set and map
functions and the relators, though.
I saw that you used the discriminator "=", but we already
Hi Jasmin,
On 12/02/14 12:11, Jasmin Blanchette wrote:
Hi Andreas,
I saw that you used the discriminator "=", but we already have functions
Option.is_none and List.null. So far, they have been mainly used for code generation, but
I have found them very convenient in in my codatatype usages w
Hi Jasmin,
On 13/02/14 13:47, Jasmin Blanchette wrote:
Hi Andreas,
Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler
:
In summary, I do not want to replace "_ = None" and "_ = []" with null and
is_none, I'd just like to make null and is_none somewhat official.
I am trying to push a changeset to Coinductive to the AFP, but I always get the following
error message:
remote: abort: could not lock repository /hg/p/afp/code: Permission denied
abort: unexpected response: empty string
Until last week, hg push used to work well. Has anything changed?
And
tomorrow, please let me know.
Cheers,
Gerwin
On 19.02.2014, at 1:45 am, Andreas Lochbihler
wrote:
I am trying to push a changeset to Coinductive to the AFP, but I always get the
following error message:
remote: abort: could not lock repository /hg/p/afp/code: Permission denied
abort
I myself found specification quite convenient and use it occasionally, e.g., in
AFP/Containers/Set_Linorder and a number of my private developments. It's a useful
shortcut to a definition with SOME and deriving the properties later with someI. It would
be good if it works with contexts. I have n
Hi Jasmin,
On 14/03/14 14:18, Jasmin Blanchette wrote:
Another candidate is "Quickcheck_Narrowing.thy". Nothing in "HOL" seems to
depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting
up Quickcheck (and GHC) so that it uses the narrowing strategy.
Hi Jasmin,
On 14/03/14 16:05, Jasmin Blanchette wrote:
Hi Andreas,
Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler
:
On 14/03/14 14:18, Jasmin Blanchette wrote:
Another candidate is "Quickcheck_Narrowing.thy". Nothing in "HOL" seems to
depend on it, and (plea
Hi Jasmin,
> 1. As long as we define new interpretations (hook types) in the HOL image, we
can
> reorganize the imports to avoid the evil scenarios. Problems arise when users
define
> their own interpretations.
I already ran into scenario 3 without registering my own interpretations just by us
Hi Makarius,
Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle time (and
ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great when it comes to
working on small projects or refactoring existing sources. I really like the negative line
spacing set
Hi Makarius,
On 28/04/14 23:10, Makarius wrote:
a) Given some text like
definition foo where "foo = ..."
when I add an attribute like [simp]: after the where, I get a symbol completion
popup to
replace the : with the element sign. Usually, my next thing is to move the
cursor with
the cursor
On 28/04/14 23:18, Makarius wrote:
On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
2. Reactivity when processing large files
With PG, I knew how to control the Isabelle prover. When I edit a large file in
a larger
project like JinjaThreads, every now and then, Isabelle changes the background
On 28/04/14 22:25, Makarius wrote:
On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
My main usage of PG is when I want to construct a complicated proof method call
like
(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp
del: ...)+
that collapses an apply script
But I try to process such
theories with jEdit and only go back to XEmacs/PG when I cannot stand
Isabelle/jEdit any longer (which usually happens when I debug the code
generator setup).
That's an interesting observation. What are the particular properties
of »debugging« here that make PG prefera
On 02/05/14 16:16, Makarius wrote:
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
text ‹
@{term ‹A \un B›}
›
Here the \un works as expected -- the cartouche remains intact
independently of its
content, as long as the funny parentheses are nested properly.
But this correct nesting is
Thanks a lot.
Andreas
On 12/05/14 20:07, Florian Haftmann wrote:
1. Violation of well-sortedness constraints: type ... not an instance of
...
declare [[show_sorts]]
code_thms
Then, I use educated guessing and Emacs' incremental search to navigate
the code equations that have been output unti
Hi Florian,
the simproc unit_eq in
http://isabelle.in.tum.de/repos/isabelle/file/697e0fad9337/src/HOL/Product_Type.thy#l78
rewrites anything of type unit to (), so there's no need to declare the definitions
introduced in 697e0fad9337 as [simp]. One could declare sup_unit_def, inf_unit_def,
Su
There's one use in JinjaThreads which does not fit into the overloading scope: The
constants sc_spurious_wakeups are declared in MM/SC_Collections.thy and MM/SC.thy, but
intentionally not defined. This expresses that the remaining proofs are independent of the
value of the constant, which is in
Quickcheck_Types defines a number of artificial types that quickcheck can use to
instantiate type variables that occur in a theorem. Normally, quickcheck instantiates them
with int provided that the sort constraints do not prevent this. In Enum.thy, there are
already the types finite_X that quic
wrote:
On 11/07/2014 13:43, Andreas Lochbihler wrote:
Quickcheck_Types defines a number of artificial types that quickcheck can use to
instantiate type variables that occur in a theorem. Normally, quickcheck
instantiates them with int provided that the sort constraints do not prevent
thi
The Native_Word entry in the AFP contains a number of quickcheck[narrowing] calls that are
set up such that they are tested only if ISABELLE_GHC is set. Therefore, there cannot be
an error message about quickcheck narrowing if ISABELLE_GHC is not set.
Andreas
On 19/07/14 21:30, Gerwin Klein wr
op it?
Andreas
On 11/07/14 15:54, Andreas Lochbihler wrote:
Quickcheck does not use these types, because it is currently configures to only
use the
types finite_1 to finite_3 from Enum, because the finite_types parameter is set
by
default. Quickcheck internally also seems to work differently dependi
See now 8b7508f848ef. Library/Lattice_Constructions contains the remains of
Library/Quickcheck_Types.
Andreas
On 18/08/14 18:44, Peter Lammich wrote:
However, the constructions might still be useful, as the following comment from
Peter
Lammich's AFP entry Refine_Monadic shows.
(* TODO: L
Hi all,
we have hardly any check that the code generated by the code generator is correct. There
is only the checking option of the command export_code. It calls a target language
compiler to see whether the compiler accepts the code. Since there are more and more
adaptations to serialisation
Hi Florian,
Sorry for the long delay until you get an answer, but I wanted to wait until I can port my
application from Isabelle2013-2 to 2014. The tracing facility seems to provide some basic
means to limit the scope of the tracing. I found the two suggestions for improvement:
1. The rewriti
Dear developers,
Jasmin mentioned to me that his new implementation allows to select which plugins should
be applied. Currently, the code generator has its own manager of plugins
(Code.datatype_interpretation) and I would be very happy if certain plugins could be
disabled selectively upon code
Thanks, Florian. Now I can drop my workarounds.
Andreas
On 20/09/14 15:34, Florian Haftmann wrote:
Generated_Code.hs:29:14:
Ambiguous type variable `a0' in the constraints:
(Prelude.Num a0)
arising from the literal `42' at Generated_Code.hs:29:14-15
(Foo a0) arising
Hi Makarius,
On 22/09/14 11:08, Makarius wrote:
Based on this changeset 469a375212c1, I have augmented some isatest
configurations which
had already ISABELLE_FULL_TEST=true
Thanks for adding this.
### /tmp/isabelle-makarius76888/Code_Test3541773/Generated_Code.scala:4:
warning: Class
Gener
Hi Florian,
Thanks for all this.
2. Meanwhile, I really like the new simplifier tracing facility and
hardly ever use the old [[simp_trace]]. Since the new trace offers a lot
of control over the tracing, would it make sense to base the tracing
facility on the new one?
It would definitely make
Makarius,
I have the impression that your push has not made it to the official afp-code. At least, I
cannot see it on
http://sourceforge.net/p/afp/code/ci/6ff9a8c6405d04f28365434a0e7bd65ea89aad86/log/
although my commits do show up there.
Andreas
On 10/02/15 23:08, Makarius wrote:
On Tue,
Dear Florian,
I myself have never looked in detail through the implementation of the predicate compiler,
but I have been a major user. I previously noticed that it does not go well together with
code_datatype. Here are my 50 cents.
On the one hand, the predicate compiler generates code equati
e2d61
user: Andreas Lochbihler
date:Tue Mar 10 16:35:14 2015 +0100
files: src/HOL/NSA/StarDef.thy
description:
more type class instances
The error message of the NSA "transfer" proof method is a bit obscure.
Makarius
It should now work again in 034a4d15b52e. Sorry for the trouble.
Andreas
PS: The error message is not so obscure if you look at the types. The left hand side talks
about hyper-naturals, the right hand side about nat.
On 12/03/15 13:56, Andreas Lochbihler wrote:
Hi Makarius,
You are right
Dear BNF and Isabelle/jEdit developers,
Today, I noticed that the datatype command in Isabelle/e936c2828bec is sometimes extremely
slow. At the end of this mail, there is a large enumeration type where this shows up.
Processing this definition on my laptop takes about 4 minutes, but the timing
Hi Dmitriy and Jasmin,
Thanks for the hint with plugins. That really speeds things up. I also suspect that the
timing panel does not include the forked proof tactics.
Cheers,
Andreas
On 09/04/15 15:55, Dmitriy Traytel wrote:
Hi Andreas,
rather than going dirty, try:
datatype (plugins only:
nce, and then destroy
the
conjunction. I'm currently testing this on testboard
(http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010).
Cheers,
Dmitriy
On 09.04.2015 16:11, Andreas Lochbihler wrote:
Hi Dmitriy and Jasmin,
Thanks for the hint with plugins. That really speeds things up. I
Hi Dmitriy,
the code plugin defines a new constant (copy of op =) that is used as equality.
datatype x = A | B
export_code equal_x_inst.equal_x in SML
This is precisely the instantiation of the equals type class.
To get it executable (#constructors)^2 equations are proved in a backward
fash
On 06/06/15 17:11, Florian Haftmann wrote:
So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow? Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domai
I am trying to replace some of my old usages of case goal_* with the new goals method. In
the course, I encountered the problem that goal inserts the facts chained in as additional
assumptions of my goals and also for the case bindings. This is unfortunate when I use
goals sequenced after rule.
Hi Makarius,
I had a brief look at the unchecked files in Predice_Compile_Examples. I have never worked
with these theories, so take my comments with a grain of salt.
Predicate_Compile_Quickcheck_Examples:
In dc2236b19a3d, Lukas removed the testers which are used in this theory and replaced t
Hi Florian,
I am continuing this thread on isabelle-dev as you have suggested.
3. For fraction fields over polynomials over rings (rather than
fields), one can use subresultants, but I have not been able to find
them formalised in Isabelle. Are they hidden somewhere? If not, are
there any plans
Hi Florian,
I noticed that the new printing interacts strangely with set comprehensions. In
Isabelle/92858a52e45b, "{(x, y). P x y}" prints as "Collect (uncurry P)" which I find
rather hard to read. Are you aware of this effect and could you please restore the former
situation?
Best,
Andreas
Hi Makarius,
This might be due to my attempt to repair Predicate_Compile_Examples in 78ece168f5b5. I'll
see what I can do.
Andreas
On 15/09/15 16:41, Makarius wrote:
This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:
*** Failed to load theory "Execute_Main" (unresolved "Ja
It should work now again (Isabelle/e4716b792713 and AFP/ec3887abf158).
Sorry for the trouble,
Andreas
On 15/09/15 16:41, Makarius wrote:
This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:
*** Failed to load theory "Execute_Main" (unresolved "Java2Jinja")
*** Failed to load th
Dear Manuel,
consider supports the same syntax as obtains, i.e., you can use "where" as in
consider "x = ∞" | "x = -∞" | y where "x = ereal y"
Andreas
On 23/09/15 08:41, Manuel Eberl wrote:
Is there a way to use ‘consider’ with fixed variables?
E.g. if I have a rule like ereal_cases:
Dear Ondrej,
Thanks a lot for this. Now I can scrap my own semi-working debugging infrastructure for
transfer(_prover).
Just a comments: Can you add a flag to transfer_step such that it outputs the rule it used
as tracing information? My problem is that with big terms, I get a lot of subgoals
MonoBoolTranAlgebra was failing due to my change in Isabelle/90f54d9e63f2 and the removal
of theorem fun_eq in favour of arg_cong (I have not investigated when this happened, but
just adapted the proof scripts), see changesets 53f94abb8704 and 0377b757f016.
Presburger-Automata had a looping call
Hi Larry and Florian,
the sort constraints for open, dist, and norm are changed in
http://isabelle.in.tum.de/repos/isabelle/file/e89cfc004f18/src/HOL/Real_Vector_Spaces.thy#l1218
These constraints were introduced by Brian Huffman in 2d91b2416de8 while he was reworking
the type class hierarchy
Hi Larry,
Type inferences assigns to "dist" the type "'a => 'a => real" where 'a :: metric_space,
and to "norm" the type "'b => real" where 'b :: real_normed_vector (due to the type
constraint manipulations in Real_Vector_Spaces.thy. The theorem dist_norm uses dist and
norm with the sort dist_
I had a look and it should work now in 1cdd27b5d78a (with Isabelle2016-RC0). I do not know
what exactly went wrong or what caused the failure. The problem seems to be related to
some change in theory imports. It seems as if code_pred cannot retrieve the specification
of a constant under certain
Hi Johannes,
Then the dictionary construction for type constructors does not
work in ML! The type signature would be the following:
val test_prod : ('a * 'b) filter
Which apparently is not allow in ML.
This is the famous value restriction (which I also regularly run into)
Dear Manuel,
I have not tried this explicitly, but it looks like the standard problem with type classes
in Scala (see section 7.1 in the code generator tutorial). Probably the problematic code
equations use two type classes with an operation inherited from the same anchestor. The
error message
Applicative_Lifting and Stern_Brocot now (AFP/1c0036f62a32) work with
Isabelle/adcaaf6c9910.
Andreas
On 13/01/16 00:06, Makarius wrote:
The AFP status is much better than last week, but these sessions are still
broken
(Isabelle/7355fd313cf8 and AFP/87337b54f3eb):
Applicative_Lifting
St
Hi Lars,
The theory Uint comes from Native_Word. I'll have a look and see whether this
can be fixed.
Andreas
On 31/01/16 22:21, Lars Hupel wrote:
* archival of the build logs
As a temporary solution, I have now configured Jenkins to retain all
build logs. I've found some pointers how to mak
Native_Word should work again in 203deaf5208d (see also 61aeecc4093d), both with GHC 7.8
and GHC 7.10.
Andreas
On 01/02/16 08:32, Andreas Lochbihler wrote:
Hi Lars,
The theory Uint comes from Native_Word. I'll have a look and see whether this
can be fixed.
Andreas
On 31/01/16 22:21,
Hi Makarius,
How about LaTeX \Mapsto for ===>? This is what I use in my papers following Ondrej and
Brian's paper on lifting.
I'd be happy to have syntax for ===> enabled by default, as it makes transfer and
parametricity rules much easier to read. I have no opinion on --->.
Andreas
On 04/
For published versions, there probably should not be any /devel-entries links. But for
papers under submission, people may have updated their AFP entries and want the reviewers
to access the updated material. At least that is what I used to do for many ITP
submissions. So it might be good to kee
Hi Makarius,
Just a quick feedback on the proof outlines: they are great! But sometimes quotes are
needed around the case name (e.g., if it is a keyword like "try" or "oracle", or if it is
a case of an induction rule by the function package for an equation which has been split
up by the sequen
Hi Johannes,
You could define the syntax for has_integral to be literally
"(f Bochner.has_integral x) s"
and similarly for the other. Additionally, you could declare bundles with the existing
notation
"(f has_integral x) s"
for both of them (like is nowadays done for the Lifting package
1 - 100 of 120 matches
Mail list logo
