Hi Walther,
Is there a chance to make Isabelle2002 run on a Windows PC ?
We see that Poly/ML supports Cygwin since version 5.x; does that mean
that there is no chance with polyml-4.1.3 ?
for the last question, I think there is no chance.
For some time it has been feasible to build Isabelle
Hi Tjark,
some comments in addition to Clemens':
* The documentation for local specification mechanisms is not very
homogeneous. The tutorials on type classes and locales are valuable.
From a user's perspective, however, a unifying discussion (with guidance
on when to use which) is missing.
Has there ever been a deliberate decision whether our IsaMakefiles (in
particular in the AFP) require GNU make or should be content with BSD
make? The issue may become important when we attempt to simplify and
stylize the grown IsaMakefiles in the AFP.
Florian
--
Home:
I just spent some time restoring two broken AFP sessions (see
http://www4.in.tum.de/~haftmann/cgi-bin/testboard.cgi/AFP/report/d96154a03b5c6414a7a0e3309e948260,
one of them due to my own fault).
What is my concern is the recent behaviour of the official AFP isatest:
it reports a lot of sporadic
Am 13.12.2010 10:38, schrieb Tobias Nipkow:
Are you referring to
*** Failed to prepare dependency graph
I remember this also occured, but I am more concerned about the infamous
error 137 and similar. Btw. we sometimes have the situation that during
testing somehow things on NFS seem to
indeed, both theorems are the same, just with different accesses;
recently, we introduced the concept of mandatory qualifiers to avoid the
strange base accesses (e.g. »induct«, »simps«, »intros«), but this has
never been systematically introduces into existing packages.
Is there any reason
Hi Sascha,
There exists a theorem called induct in HOL, which changes after
every datatype declaration. What is the rationale behind this
theorem? Is it required for a particular purpose or just a forgotten
remainder of previous tunings? Shouldn't this suprising behaviour be
eliminated?
Since somebody has to be the first to ask the question: is there
already a schedule for the next release?
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Traditionally the datatype command would accept optional alternative
names used in names of type-related facts etc., e.g.
datatype (foo) /*/ = Bar
With all HOL types being regulary named, the question arises whether we
still have to keep that feature or shall just discontinue it?
Am 03.11.2010 16:26, schrieb Tobias Nipkow:
The 'typedef' command supports a similar option for alternative names;
I am sure that it was originally created for use with non-alphanumeric
type names. One could also ask whether the existence of this feature
for typedef is still justified, when
However in packages often also bindings are created automatically.
Currently I am working on some fragements of a mechanism which analyzes
parts of a theory (most prominently constants and theorems) and
generated new constants and theorems from them. The result, in
particular the new
Hi Brian,
first of all, your report has indeed exposed a flaw in the processing of
class declarations which has been corrected in
http://isabelle.in.tum.de/repos/isabelle/rev/eddda8e38360,
Unfortunately, the processing of class declarations is notoriously
difficult, especially if the infamous
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 = 'b_1) = ... = ('a_n = 'b_n)
= ('a_1, ..., 'a_n) k is = ('b_1, ..., 'b_n) k
for an n-ary type ('a_1, ..., 'a_n) k must satisfy some characteristic
Typically, bindings are created by the user in the theory text and
passed down from there, e.g.
specification (definition) foo :: T
where
P foo
creates a @{binding foo}.
However in packages often also bindings are created automatically.
Currently I am working on some fragements of a
Hi Walther,
in addition to the hints given by Christian, I add that it appears to me
that you just want to do equational rewriting on bare terms. For this
you can use Pattern.rewrite_term
Hope this helps,
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
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 =
Hi Stefan,
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
Hi Stefan,
why can't we repair interpret_construction so that it handles this case
properly?
well, we can extend interpret_construction in such a way but also have
to do so for the tools which use it. This is perhaps not even that
difficult, but it adds considerable complexity to already
The failure has now repeatly occured here:
*** Theory loader: undefined theory entry for Approximation_Ex
*** Failed to finish proof
*** At command by (line 42 of
/mnt/nfsbroy/home/isatest/isadist/Isabelle_04-Sep-2010/src/HOL/Decision_Procs/ex/Approximation_Ex.thy)
i.e. this proof:
Hi Walther,
How can we produce specific patterns (some variables of a term should
become Free, some Var),
in principle, the two syntactic categories of term variables have the
following purpose:
Free -- locally fixed variable, e.g. fixed variable in a proof context
or locally defined
HOL: Scala (2.8 or higher) has been added to the target languages of
the code generator.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description:
Hi all,
with authentic syntax being default and thanks to antiquotations, we
have now reached a state where we could replace all the remaining
unqualified symbol names in HOL.thy (between global and local).
While this should be technically quite easy, there remain two open
questions before
One thing I don't get: if HOL.eq is already taken, why not map the equality
symbol to something else?
Well, eq seems more natural when looking at the traditional xsymbol
syntax \noteq (although the corresponding abbreviation is named
not_equal). When using HOL.equal, there is always an
Hi Walther,
without having intimate knowledge of the matter, I would guess you have
to quote term expressions containing whitespace as you would also in Isar:
So,
parse Parse.term \xxx +++ 111\ end;
instead of
parse Parse.term xxx +++ 111 end;
Hope this helps,
Florian
--
Home:
At http://www4.in.tum.de/~haftmann/misc/locale.gif you can have a look
at preliminary experiments to visualize dependencies between locales
(the corresponding crude code can be found at
http://www4.in.tum.de/~haftmann/misc/Locale_Graph.thy).
Maybe I should consider that for submission to the
Abolished symbol type names: prod and sum replace * and +
respectively. INCOMPATIBILITY.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description:
Hi,
*** Theory loader: failed to load Public_SET (unresolved Event_SET)
*** Theory loader: failed to load Event_SET (unresolved Message_SET)
*** Theory loader: failed to load Message_SET (unresolved Nat_Bijection)
*** Inner lexical error at: × nat (line 15 of /home/pho
It is possible to enter type variables distinguished only by sort
constraint on the Isar level:
lemma
assumes P TYPE('a::order) and Q TYPE('a::group_add)
shows R TYPE('a::power)
using assms proof -
It is not clear to me whether this his always been possible that way or
slipped in due to some
Is there a better name for Rat.normalize?
IMHO, in most contexts, Rat.normalize is a more descriptive name than
normalize. If I had to invent a base name, it would probably be
normalize_rat or rat_normalize... So I would suggest hide (open).
I support this.
Florian
--
Home:
Here are some things from my list:
On my list since two days: cleaning up of the Groebner and Presburger
theories. Lemma duplicates (due to essentially vacious interpretations)
are already spreading through the distribution...
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP
Hi Brian
Every time I use the overloaded constants top and bot (defined in
Orderings.thy), Isabelle prints them out as top_class.top and
bot_class.bot, instead of just top and bot. I find this
annoying, so I tried to find out the reason for this.
class top = preorder +
fixes top :: 'a
'code_reflect' allows to incorporate generated ML code into
runtime environment; replaces immature code_datatype antiquotation.
INCOMPATIBILITY.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hi Thomas,
Isabelle internalizes expressions in two steps:
(1) parse :: raw string (type string) - raw term (type term)
(2) check :: raw term (type term) - internalized term with types
inferred etc. (type term)
It seems to me that most things you want to do can be done using (2)
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 == x)
unfolding
Hi Dominique,
ML {* Thm.axiom (the_context()) Orderings.le_fun_def_raw *};
val it =
ord_fun_inst.less_eq_fun ==
%(f::?'a::{} = ?'b::{}) g::?'a::{} = ?'b::{}.
ALL x::?'a::{}. f x = g x : Thm.thm
This might seem astonishing at first sight but is perfectly ok. A
definition
Hi Mika?l,
Can someone tell we how I can *retrieve the lemmas/rules used by
apply(auto)* , i.e. what were the steps I should have used if I did not
have this auto method ?
Same question for *apply(blast)*
Although it is technically possible, it will usually waste some time and
energy to
Changes culminated over the last 12 months:
Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with
le_inf_iff
- dropped
Hi Lucas,
perhaps the source of the confusion can be found here:
http://isabelle.in.tum.de/repos/isabelle/file/6b31b143f18b/src/Pure/codegen.ML
I.e. due to a misunderstanding of interfacing convention (0 is also a
valid size), Codegn.test_term in Isabelle2009 would increase its size
argument by
Hi Lucas,
indeed the whole quickcheck matter has grown into a complex story.
First, we currently (e.g. following development in the hg repository)
have a kind of fork: there is the old quickcheck, residing in
Pure/codegen.ML, and the new one in HOL/Quickcheck.thy; the most
prominent difference
Hi Lucas,
apply (unfold Product_Type.pair_collapse[symmetric, of al])
The equation Product_Type.pair_collapse[symmetric, of al] can be
unfolded forever, so the method invocation does not terminate, leading
to an unspecified behaviour of the system!
As a quick replacement, consider
Hi Amine,
*** Clash of specifications Sign.sign.size_sign_inst.size_sign_def and
Sign.sign.size_sign_inst.size_sign_def for constant Nat.size_class.size
*** At command theory.
I guess that you have a theory which introduces a type sign. When you
ensure that this theory has Plain as ancestor,
Hi Brian,
The following code works:
datatype 'a bintree = Branch 'a bintree 'a bintree | Tip 'a
definition test1 = (Tip True = Branch (Tip False) (Tip True))
export_code test1 in Haskell file -
but this other example doesn't:
datatype 'a tree = Node 'a 'a tree list
definition test2 =
Dear all,
I think there are different aspects which we should clearly set apart.
a) Keeping theory imports minimal vs. reducing the number of merges
Careful thinking what the logical preliminaries of a particular theory
are is a necessary, valuable and fruitful task -- I would by no means
Hi Brian,
I'm afraid I don't understand why reducing the number of merges by
adding wasp-waists is beneficial. From what I understand, adding
additional theory dependencies could only reduce opportunities for
parallel execution. Is there another technical reason why the amount of
merging
Hi Brian,
Our current policy is the Plain, Main and Complex_Main are either
ancestors or descendants of any theory.
OK, the requirement for Plain I can understand. For Main, it doesn't
seem too unreasonable, assuming it's necessary (since most theory files
import Main anyway).
But
persists.
Florian Haftmann wrote:
Hi Amine,
I have a theory development which used to work not a long time ago. I am
now trying to include it into the distribution.
At some point I can not merge the theories and get:
*** Clash of specifications Permutations.typerep_^_inst.typerep_^_def
:/usr/wiss/chaieb/.repos co
work/Lib
The files are then under Multivariate.
Amine.
PS: Please forgive for still using cvs, but I am applying the first
commandment of Computer science.
Florian Haftmann wrote:
Can you provide me with a theory graph of Permutations and Misc? (Isar
command
OK, seems like you have to change the following:
a) add Fact to the imports of Plain
b) add Main to the imports of Infinite_Set
and to the imports of Finite_Cartesian_Products
Our current policy is the Plain, Main and Complex_Main are either
ancestors or descendants of any theory.
Hope this
Our current policy is that Plain, Main (and Complex_Main) are either
ancestors or descendants of any theory.
This rule does not tell me anything since it is trivally satisfied by
any connected graph containing Plain, Main and Complex_Main.
The rule rules out the following situation:
A
Dear Isabelle developers,
we are now heading towards the next Isabelle release.
Since Isabelle 2008 a lot of changes and improvements have found their
way into the sources. For this reason I would kindly invite you all to
update the NEWS and CONTRIBUTORS in the root of the repository to
Hi Amine,
For now HOL/Fact.thy defines factorials (over natural numbers) and
strangely imports the reals. The theorem involving the reals, however,
hold in any (ordered) (ring/field) of charachteristic Zero.
Apart from that, I have a formalization of Pochhammer's symbol (raising
Dear Amine and Jeremy,
the current development snapshot now has fixed the problem. Switching
to it should be rather safe -- we plan to converge to the next Isabelle
release quite soon and refrain from major changes.
Thanks for your patience. There are still minor issues which I have to
Hi Amine,
sorry for the inconvenience. Currently there is major upheaval going on
in the locale/class area. Im working hard on solving the remaining
problems.
For the moment I suggest going back to an earlier snapshot, e.g.
http://isabelle.in.tum.de/repos/isabelle/rev/bb0f395db245
Chers,
Hi Amine,
I guess you are in the following thygraph situation:
Typrep Real
| / \ |
|/\|
Complex_Main FPS
\ /
\/
\ /
Foo
Real defines type real, Typerep class typerep (;-)). Then both in
Complex_Main and FPS and instance for
wenzelm 1495934
paulson 982335
***
haftmann 413881 **
nipkow 261461
Hi Brian,
Is there any good reason why the constants neg and iszero (defined
in Int.thy) are needed anymore?
if there is a chance to get rid of those, go ahead and try. Perhaps
they play a role for numerals and natural numbers, but this is just a
suspicion.
Cheers
Florian
--
Home:
The switch to hg makes it possible to adapt some file locations (file
names) in the Isabelle distribution which have evolved over time but do
not fit to the logical structure of the distribution any longer,
according to the following table:
src/Provers/* ~ src/Tools/*
src/Pure/Tools/* ~
Amine Chaieb schrieb:
Dear all,
(How) Can I perform an instantiation of a type-constructor with two
arguments, an thereby restricting them to be the same?
This is beyond the type class system of Isabelle. A pity.
Florian
--
http://isabelle.in.tum.de/~haftmann
PGP available:
* Unified theorem tables for both code code generators. Thus [code
func] has disappeared and only [code] remains. INCOMPATIBILITY.
--=20
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in=
formatik_tu_muenchen_de
-- next part --
A
Then what is the point of
undefined_fun: undefined x = undefined
in HOL.thy?
This is essentially pointless and is so soon to be dropped that I didn't
take the effort to even point out to it in my emails, taking the risk
that somebody would have a look a the source ;-)
Florian
Some years ago two further constants were introduces into HOL.thy:
undefined and default. The idea then was to divide the role of
classical arbitrary on two shoulders: undefined should be
unspecified an could be used to fake partiality, whereas default would
be overloaded and could be
While we're at it: what is the general feeling towards migrating the AFP
to svn?
I have no strict opinion on this. Perhaps, if somebody wants to invest
the effort, there are no urgent causes against migrating to SVN. But if
not, staying with CVS is no desaster at all.
Florian
Proofs are much more fragile, notably unstructured ones. One way around
this is to submit theory libraries and applications to
http://afp.sourceforge.net/ where they get updated to latest Isabelle
automagically.
Thanks to all the magicians ;-)
Florian
--
PGP available:
Normalization by evaluation now allows non-leftlinear equations.
Declare with attribute [code nbe].
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-- next part --
A non-text attachment
The overloaded infix syntax ^ for different power operations (natural
power in monoids, function power, relation power) turns more and more
unsatisfactory for a couple of reasons, e.g.:
* The abuse of the type class mechanism to achieve the ^ syntax for
funpow and relpow hinders the enforcement
Tobias Nipkow wrote:
The three obfuscating issues were:
A) Archaic, hardly readable and fragile proof techniques:
* unfolding definitions of predicates over logical formulae instead of
proper intro/elim-rules
This is mere dogma. It is perfectly standard to reason about logical
Amine Chaieb wrote:
I don't see why this argument yields an iff proof of your conjecture.
Sometimes a typo is only a typo, nothing more. I don't want to state a
general guideline for that issue, but only report my (subjective)
experiences concerning particular examples.
Florian
what I forgot to mention:
There is no urgent need that the HOL image contains *all* the
HOL-Complex theories. I also have been thinking about splitting off all
the Analysis stuff into a session HOL-Analysis, but on the other hand a
lot of functions which you naively expect for reals/complexes
* Integrated image HOL-Complex with HOL. Entry points Main.thy and
Complex_Main.thy remain as they are.
* New image HOL-Plain provides a minimal HOL with the most important
tools available (inductive, datatype, primrec, ...). By convention the
corresponding theory Plain should be ancestor of
Instantiation target allows for simultaneous specification of class
instance operations together with an instantiation proof. Type check
phase allows to refer to class operations uniformly. See
HOL/Complex/Complex.thy for an Isar example and HOL/Library/Eval.thy for
an ML interface example.
Florian has suggested making sledgehammer available earlier in the
construction of Main, before PreList at least. This could be useful
to developers. However, it requires Hilbert_Choice, which must also
be introduced earlier.
A PreList-Sledgehammer would be a nice thing to have, but it
Lawrence Paulson wrote:
It needs at least Hilbert_Choice. It could go before Datatype. Some
details need to be worked out to ensure that all theorems in Main.thy
get converted to clause form.
I must confess that I have lost track now. Does only the skolemization
depend on Hilbert-Choice, or
601 - 672 of 672 matches
Mail list logo
