[isabelle-dev] quickcheck on type real

2007-09-03 Thread Florian Haftmann
(1) I discovered a slip in the implementation of Rat.inv which did not normalize negative rats; this might explain the strange behaviour of equality (fixed in CVS). (2) I strongly support Amine's issue: all code generator frameworks should use the verified rational numbers. Why I have refrained

[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy

2007-09-14 Thread Florian Haftmann
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

[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy

2007-09-14 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2007-11-29 Thread Florian Haftmann
* Command instance now takes list of definitions in the same manner as the definition command. Most notably, object equality is now possible. Type inference is more canonical than it used to be. INCOMPATIBILITY: in some cases explicit type annotations are required. Florian

[isabelle-dev] NEWS

2007-12-19 Thread Florian Haftmann
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.

[isabelle-dev] HOL vs. HOL-Complex

2008-07-02 Thread Florian Haftmann
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

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Florian Haftmann
Dear all, last week I spent some considerable time and energy to get rid of the locale (open) feature, which was in most cases straight forward and trivial -- except the issue of MicroJava, Jinja, JinjaThreads. I think it is worth to document my experiences here for the future. The three

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Florian Haftmann
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

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2008-07-01 Thread Florian Haftmann
* 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

[isabelle-dev] Relation_Power.thy

2008-09-02 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2008-09-16 Thread Florian Haftmann
HOL/Main: command value now integrates different evaluation mechanisms. The result of the first successful evaluation mechanism is printed. In square brackets a particular named evaluation mechanisms may be specified (currently, [SML], [code] or [nbe] -- suggestions for better syntax welcome).

[isabelle-dev] NEWS

2008-09-25 Thread Florian Haftmann
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

[isabelle-dev] [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)

2008-09-27 Thread Florian Haftmann
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:

[isabelle-dev] [Fwd: SourceForge.net CVS Migration and Downtime Announcement]

2008-09-30 Thread Florian Haftmann
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

[isabelle-dev] An ARBITRARY question

2008-10-02 Thread Florian Haftmann
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

[isabelle-dev] An ARBITRARY question

2008-10-03 Thread Florian Haftmann
I wonder whether it is wise to have three of these. People are going to attach more significance to them than they deserve. I am inclined to think that we should get rid of arbitrary. Larry I also think that two would be better than three; technically undefined is the same as arbitrary, and

[isabelle-dev] An ARBITRARY question

2008-10-03 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2008-10-10 Thread Florian Haftmann
* 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

[isabelle-dev] instantiation

2008-10-27 Thread Florian Haftmann
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:

[isabelle-dev] instantiation

2008-10-28 Thread Florian Haftmann
:( I also failed a few weeks ago to instantiate the fold combinator to iterate function composition ... Hmmm... perhaps fold (op o) id id is what you want in that case. But is this restriction fundamental or does it happen to be there? Well, the type classes in Isabelle are an instance of

[isabelle-dev] Directory layout

2008-12-01 Thread Florian Haftmann
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/* ~

[isabelle-dev] Numeral simplification: neg and iszero

2008-12-03 Thread Florian Haftmann
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:

[isabelle-dev] Number of line changes per user in the Isabelle repository

2009-01-18 Thread Florian Haftmann
wenzelm 1495934 paulson 982335 *** haftmann 413881 ** nipkow 261461

[isabelle-dev] typrep?

2009-01-20 Thread Florian Haftmann
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

[isabelle-dev] typrep?

2009-01-21 Thread Florian Haftmann
Hi all over there, some comments on my behalf: a) The Typerep theory if used by Imperative_HOL, but this is *not* its only application; it is also used for evaluation using code generation (value [code]) -- indeed, I added this immediately after the 2008 release in order to gain some experience

[isabelle-dev] typrep?

2009-01-21 Thread Florian Haftmann
Hi Amine, wrt to d) and e) (Users/Developers, HOL is difficult). This theory is for now a using HOL, but of course I want to develop it in a manner that it could become part of HOL. The situation you mention in d) and e) has not to be this way and we should not take it for granted that HOL

[isabelle-dev] typrep?

2009-01-21 Thread Florian Haftmann
and is incorporated via Code_Eval.thy (stupid name btw.) in Plain.thy. d) In List.thy, the conventional strings are established as types string = char list This would yield a complete setup of typerep since Plain.thy, which leaves only a minimal risk of producing bad thygraphs. Florian Florian Haftmann

[isabelle-dev] NEWS

2009-01-22 Thread Florian Haftmann
* Class declaration: sc. base sort must not be given in import list any longer but is inferred from the specification. Particularly in HOL, write class foo = ... instead of class foo = type + ... Florian -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available:

[isabelle-dev] problems with the class-package

2009-01-23 Thread Florian Haftmann
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,

[isabelle-dev] Factorials and binomial coefficients

2009-02-02 Thread Florian Haftmann
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

[isabelle-dev] NEWS and CONTRIBUTORS

2009-02-04 Thread Florian Haftmann
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

[isabelle-dev] Typerep again

2009-02-09 Thread Florian Haftmann
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

[isabelle-dev] Typerep again

2009-02-09 Thread Florian Haftmann
:/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

[isabelle-dev] Typerep again

2009-02-09 Thread Florian Haftmann
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

[isabelle-dev] Typerep again

2009-02-09 Thread Florian Haftmann
Please do not give me fish but teach me how to fish! Hmmm... I had been thinking I was doing both: the fish... 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 and the fishing rules... Our current policy is

[isabelle-dev] Typerep again

2009-02-09 Thread Florian Haftmann
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

[isabelle-dev] Typerep again

2009-02-10 Thread Florian Haftmann
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

[isabelle-dev] A better policy for the typerep class

2009-02-11 Thread Florian Haftmann
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

[isabelle-dev] A better policy for the typerep class

2009-02-11 Thread Florian Haftmann
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

[isabelle-dev] Bug report: code generation for eq with indirect-recursive datatypes

2009-02-23 Thread Florian Haftmann
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 =

[isabelle-dev] Bug report: code generation for eq with indirect-recursive datatypes

2009-02-23 Thread Florian Haftmann
Hi Brian, However, if I try to generate OCaml or SML code, the second one still fails, but with a different error this time: *** Illegal mutual dependencies: tree :: eq, eq_class.eq [tree] *** At command export_code. What do you think? This is the situation as reported in sect. 1.2.6 of

[isabelle-dev] Performance of class command

2009-02-25 Thread Florian Haftmann
Hi Brian, Sometimes the class command can be rather slow, for example: I don't know what the class command is doing behind the scenes, but is it supposed to be taking this long? Should this be considered a performance bug? Without a closer look at this I would deem that this is due to the

[isabelle-dev] problems with the class-package

2009-02-02 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2009-03-06 Thread Florian Haftmann
New predicate strict_mono classifies strict functions on partial orders. With strict functions on linear orders, reasoning about (in)equalities is facilitated by theorems strict_mono_eq, strict_mono_eq and strict_mono_eq. Florian -- Home: http://wwwbroy.in.tum.de/~haftmann PGP

[isabelle-dev] NEWS

2009-03-06 Thread Florian Haftmann
Amine Chaieb schrieb: Florian, facilitated by theorems strict_mono_eq, strict_mono_eq and strict_mono_eq. should have been strict_mono_eq, strict_mono_less_eq, strict_mono_less ;-) Florian P.S. Even today we are facing difficult problems, which are very difficult... -- Home:

[isabelle-dev] Strange phenomenon with presburger

2009-03-10 Thread Florian Haftmann
lemma \Andm n x. x \in P \Longrightarrow Suc (2 * m) = 2 * n \Longrightarrow False apply presburger done lemma \Andm n x. P x \Longrightarrow Suc (2 * m) = 2 * n \Longrightarrow False apply presburger -- fails This phenomenon already occurs in Isabelle 2008 and still persists. The confusing

[isabelle-dev] For casual mercurial users

2009-03-11 Thread Florian Haftmann
People who are not constantly busy with the Isabelle repository itself will hardly follow each changeset explicitly. Then I recommend to use hg update with verbose flag: hg update -v resp. hg pull -u -v This then imitates the CVS style output which tells explicitly which files

[isabelle-dev] antiquotation @{thm[locale=...

2009-05-17 Thread Florian Haftmann
What happened to this option? I cannot run one of my draft papers anymore. How do I have to write it these days? I couldn't find anything in NEWS. text (in ...) {* ... @{thm ...} *} should work. It could be the case that the locale= option was never part of an official release and thus has

[isabelle-dev] changeset 31457: class replaces axclass

2009-06-05 Thread Florian Haftmann
Hi Brian, I'm just wondering about why the class command is an improvement over axclass in this situation: http://isabelle.in.tum.de/repos/isabelle/rev/d1cb222438d8 Perhaps not improvement, but replacement; before Isabelle 2009, there were still situations which class could not cope with,

[isabelle-dev] Bug report: code generation with class constant called open

2009-06-08 Thread Florian Haftmann
Hi Brian, thanks for reporting this. I hope to eliminate this problem within this day. Hope this helps, Florian Brian Huffman schrieb: Hi all, I recently tried to make some changes to the topological_space class in RealVector.thy (I moved the definition of open here from

[isabelle-dev] Clash of specifications

2009-07-03 Thread Florian Haftmann
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,

[isabelle-dev] Interrupt exception

2009-07-13 Thread Florian Haftmann
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

[isabelle-dev] [isabelle] counter example checking from ML

2009-09-21 Thread Florian Haftmann
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

[isabelle-dev] counter example checking from ML

2009-09-22 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2009-09-25 Thread Florian Haftmann
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

[isabelle-dev] Explicit behaviour of apply(auto) ?

2009-10-02 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2009-10-09 Thread Florian Haftmann
New generalized style concept for printing terms: write @{foo (style) ...} instead of @{foo_style style ...} (old form is still retained for backward compatibility). Styles can be also applied for antiquotations prop, term_type and typeof. Florian -- Home:

[isabelle-dev] Typing problem in autogenerated axiom

2009-11-28 Thread Florian Haftmann
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

[isabelle-dev] Typing problem in autogenerated axiom

2009-11-30 Thread Florian Haftmann
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

[isabelle-dev] copying contexts

2009-12-02 Thread Florian Haftmann
Hi Lukas, AFAIK Theory.copy is the appropriate interface. Hope this helps 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 -- next part -- A

[isabelle-dev] Method parsing, YXML and term construction.

2010-02-08 Thread Florian Haftmann
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)

[isabelle-dev] NEWS

2010-04-29 Thread Florian Haftmann
'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:

Re: [isabelle-dev] top and bot

2010-05-03 Thread Florian Haftmann
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

Re: [isabelle-dev] Towards the next Isabelle release

2010-05-07 Thread Florian Haftmann
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

[isabelle-dev] power_2_eq_1_iff

2010-05-17 Thread Florian Haftmann
Hi Brian, http://isabelle.in.tum.de/repos/isabelle/diff/001d1aad99de/src/HOL/Nat_Numeral.thy adds power_2_eq_1_iff as [simp], which breaks Fermat_3_4 in AFP. Although this can be repaired easily, I have the feeling that this rule which, if applied to an assumption, produces disjunctive proofs,

Re: [isabelle-dev] Rat.normalize

2010-05-26 Thread Florian Haftmann
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:

[isabelle-dev] Type variables differing only in sort constraint

2010-05-27 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2010-07-02 Thread Florian Haftmann
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:

Re: [isabelle-dev] how to run the SET protocol..

2010-07-02 Thread Florian Haftmann
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

[isabelle-dev] Locale dependencies

2010-07-21 Thread Florian Haftmann
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

Re: [isabelle-dev] Parse.term

2010-08-12 Thread Florian Haftmann
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:

[isabelle-dev] Deglobalizing HOL.thy

2010-08-19 Thread Florian Haftmann
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

Re: [isabelle-dev] Deglobalizing HOL.thy

2010-08-19 Thread Florian Haftmann
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

[isabelle-dev] NEWS

2010-08-27 Thread Florian Haftmann
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:

Re: [isabelle-dev] produce term patterns

2010-09-03 Thread Florian Haftmann
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

Re: [isabelle-dev] Spike in isatest performance charts

2010-09-03 Thread Florian Haftmann
Today's isatest indicates a significant drop in performance: http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M8/HOL-Metis_Examples.png I added

Re: [isabelle-dev] Recent instabilities of HOL-Decision_Procs

2010-09-06 Thread Florian Haftmann
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:

[isabelle-dev] Type arguments in datatype declarations

2010-09-27 Thread Florian Haftmann
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 =

Re: [isabelle-dev] Type arguments in datatype declarations

2010-09-27 Thread Florian Haftmann
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

Re: [isabelle-dev] Type arguments in datatype declarations

2010-09-27 Thread Florian Haftmann
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

Re: [isabelle-dev] use term patterns, was: 'produce term patterns'

2010-10-01 Thread Florian Haftmann
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:

[isabelle-dev] Declaration depending on user proofs

2010-10-07 Thread Florian Haftmann
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

[isabelle-dev] Binding with implicit rename

2010-10-07 Thread Florian Haftmann
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

Re: [isabelle-dev] Binding with implicit rename

2010-10-08 Thread Florian Haftmann
Hi Christian, to me the liberal flag seems rather ad-hoc. Wouldn't a proper hierarchical naming solve this problem (maybe by introducing an automatic sub-module Internal/Auto/Whatever for any theory T, such that automatic names may be referred to by using T.Whatever.automatic_name). we

Re: [isabelle-dev] Binding with implicit rename

2010-10-26 Thread Florian Haftmann
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

Re: [isabelle-dev] type errors when defining subclasses of HOLCF type classes

2010-10-26 Thread Florian Haftmann
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

Re: [isabelle-dev] Declaration depending on user proofs

2010-11-03 Thread Florian Haftmann
So what are the aesthetic and technical reasons here? Well, already some time ago I had the impression that there is a fear of keyword number explosion. Personally, I indeed don't care much. Of course the »global« nature of keywords makes it difficult to do ad-hoc experimentation with new

[isabelle-dev] Datatype alt_names

2010-11-03 Thread Florian Haftmann
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?

Re: [isabelle-dev] Datatype alt_names

2010-11-03 Thread Florian Haftmann
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

[isabelle-dev] Some Isabelle staticics

2010-11-05 Thread Florian Haftmann
I had to made some Isabelle statistics which maybe are interesting (just ignore the German fragements): Lines of code in *.ML and *.thy files (tip): http://www4.in.tum.de/~haftmann/misc/isabelle_stat/stat_loc.png Number of submissions in the AFP:

[isabelle-dev] Scheduler for next release

2010-11-16 Thread Florian Haftmann
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

Re: [isabelle-dev] theorem induct

2010-11-29 Thread Florian Haftmann
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?

Re: [isabelle-dev] theorem induct

2010-11-30 Thread Florian Haftmann
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

[isabelle-dev] sporadic failures of AFP tests

2010-12-13 Thread Florian Haftmann
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

Re: [isabelle-dev] sporadic failures of AFP tests

2010-12-13 Thread Florian Haftmann
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

Re: [isabelle-dev] stone age for another reason

2010-12-17 Thread Florian Haftmann
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

Re: [isabelle-dev] Local Specification Mechanisms: Brief Experience Report

2010-12-17 Thread Florian Haftmann
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.

[isabelle-dev] GNU vs. BSD make

2010-12-17 Thread Florian Haftmann
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:

Re: [isabelle-dev] JinjaThreads

2010-12-19 Thread Florian Haftmann
Hi all, it seems indeed that JinjaThreads since recently runs out of memory even on macbroy2 with parallelism, c.f. last afp isatest log: Running HOL-Word-JinjaThreads ... poly(19058,0xa00a0540) malloc: *** mmap(size=16777216) failed (error code=12) *** error: can't allocate region *** set a

  1   2   3   4   5   6   7   8   >