Re: [isabelle-dev] SCHEDULER: disposed 4 dead worker threads

2013-12-14 Thread Christian Urban
Sorry about being a harbinger of bad news. But this message about dead worker threads shows up pretty frequently with me. Though it has not caused any problems I am aware of. My guess is that I notice this message already for at least a year. It is in fact so frequent that I assumed this is

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

2013-08-05 Thread Christian Urban
On 04/08/13 21:20, Christian Urban wrote: On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote: I.e. everything that is defined by the new package and falls into the fragment of the old package can be registered as an old datatype benefiting from

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

2013-08-04 Thread Christian Urban
On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote: I.e. everything that is defined by the new package and falls into the fragment of the old package can be registered as an old datatype benefiting from all the infrastructure built around it (e.g. size function,

Re: [isabelle-dev] adhoc overloading

2013-07-17 Thread Christian Urban
On Wednesday, July 17, 2013 at 13:43:34 (+0900), Christian Sternagel wrote: @all: please let me know, in case anybody finds localized ad-hoc overloading useful. An aside: I'm currently using localized ad-hoc overloading for a port of Nominal2's permutation type, where I use

Re: [isabelle-dev] [isabelle] the sound of a sledgehammer

2013-02-17 Thread Christian Urban
On Sunday, February 17, 2013 at 17:06:46 (+0100), Tjark Weber wrote: On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote: * Sledgehammer spontaneously acts asynchronously of certain open problems in the text, depending on certain parameters like time outs. Triggering

[isabelle-dev] typedef (open) legacy

2012-10-04 Thread Christian Urban
Hi, Closed type definitions with typedef new_type = some set are considered legacy. The warning message suggests to use typedef (open) new_type = some set but as far as I can see, this does not introduce a definition for the set underlying the type. For example the theorem

Re: [isabelle-dev] typedef (open) legacy

2012-10-04 Thread Christian Urban
Thanks a lot for all replies! Christian On Thursday, October 4, 2012 at 14:17:48 (+0200), Makarius wrote: On Thu, 4 Oct 2012, Christian Urban wrote: Closed type definitions with typedef new_type = some set are considered legacy. The warning message suggests to use

Re: [isabelle-dev] Checked assume command

2012-09-05 Thread Christian Urban
On Wednesday, September 5, 2012 at 13:24:27 (+0200), Makarius wrote: On Tue, 4 Sep 2012, Lars Noschinski wrote: As an user, an easy method to test whether the current set of assumptions still fit one of the pending goals is fix P show P sorry. As I don't know any scenario where

Re: [isabelle-dev] repository and components etc.

2012-08-29 Thread Christian Urban
On Wednesday, August 29, 2012 at 21:45:35 (+0200), Makarius wrote: It is still used for isatest runs, but it does not have to be made public as a crippled distribution that lacks most add-on components. If it is only a small effort, I am happy to keep it. The add-on components can

Re: [isabelle-dev] Building nightly snapshots

2012-08-23 Thread Christian Urban
On Thursday, August 23, 2012 at 22:37:22 (+0200), Makarius wrote: On Thu, 23 Aug 2012, Christian Urban wrote: (1) copying etc/settings, etc/components and contrib/* from the current working snapshot Wait, this sounds suspicious. What is the current working snapshot

[isabelle-dev] Building nightly snapshots

2012-08-22 Thread Christian Urban
Dear All, I am used to building the nightly snapshots, which in the olden days was conveniently done by the build script. Well, times change. ;o) I remember (and again verified just now) that with the snapshot from 14 August I can build Isabelle with ./bin/isabelle build -v -s -c

Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support isabelle build Options

2012-08-17 Thread Christian Urban
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote: Tjark, you have no business here. I assume something got here lost in translation. Otherwise, we should all make reasonable effort to welcome everybody on both, the isabelle-users and isabelle-dev lists. After all, we like to

Re: [isabelle-dev] isabelle build

2012-08-06 Thread Christian Urban
On Monday, August 6, 2012 at 12:09:54 (+0200), Makarius wrote: Did everybody try the isabelle build tool? Are there any problems left, apart from retraining fingers after 16 years of usedir/make/makeall? I just did. Building of heaps worked nicely. But two questions: 1) I transferred two

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-23 Thread Christian Urban
the simplifier opportunities for wild exploration will just slow everything down. Yours, Thomas. On 23/05/12 02:23, Christian Urban wrote: Dear All, Assuming that this is about the bowels of the simplifier, I hope this is the right place to ask the following question

[isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Christian Urban
Dear All, Assuming that this is about the bowels of the simplifier, I hope this is the right place to ask the following question. The simplifier has a subgoaler, which helps with rewriting conditional lemmas. This simplifiying/subgoaling process seems to be not transitive (probably is not

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Christian Urban
On Tuesday, May 22, 2012 at 20:59:28 (+0200), Tobias Nipkow wrote: but am at least as confused as you are: [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: atom v ♯ (x1, x2) ⟹ atom v ♯ x1 [1]Applying instance of rewrite rule ??.unknown: ?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯

[isabelle-dev] Nominal and FinFuns from the AFP

2012-05-10 Thread Christian Urban
Dear All, In Nominal I am usually relying on types that are defined in HOL or that I define myself. However, I now came across the FinFun development in the AFP by Andreas Lochbihler (thanks to Larry). The finfun type seems to be rather useful to Nominal users, since it has finite support, in

Re: [isabelle-dev] Merge-Sort Implementation (and a question on induction_schema)

2011-11-02 Thread Christian Urban
I was about to suggest the same as Andreas. For what it is worth, here is my proof of this lemma. lemma sorted_merge_induct[consumes 1, case_names Nil IH]: fixes key::'b = 'a assumes sorted (map key xs) and !!xs. P xs [] and !!xs y ys. sorted (map key xs) == P (dropWhile (%x. key x

[isabelle-dev] NEWS - Redundant lemmas

2011-09-20 Thread Christian Urban
Hi All, Somebody recently added in the NEWS the entry Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset, UNION_eq_Union_image,

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-09-03 Thread Christian Urban
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: I will now examine HOL-Nominal more closer, and after that come up with a next report about the distribution. There should be no problems in principle. Early versions of Nominal (1) worked perfectly with an explicit

[isabelle-dev] Bind raised in auto

2011-09-02 Thread Christian Urban
Hi, I just applied in a proof-script the following tactic apply(auto simp add: f_def dest: l3) and received the error message *** exception Bind raised (line 934 of raw_simplifier.ML) *** At command apply Is this supposed to happen? f_def is from a function I defined and l3 is a

Re: [isabelle-dev] Bind raised in auto

2011-09-02 Thread Christian Urban
Makarius writes: The check_conv function also provides some extra trace, if simp_trace/simp_debug is enabled. See the sources: trace_thm (fn () = Proved wrong thm (Check subgoaler?)) ss thm'; trace_term false (fn () = Should have proved:) ss prop0; NONE

[isabelle-dev] Datatype alt_names

2010-11-03 Thread Christian Urban
I am not sure whether this is relevant, but I have recently introduced a similar feature in Nominal2. There the problem is that one often defines several mutual-recursive nominal datatypes, like nominal_datatype foo1 = .. and foo2 = .. and foon = .. with n being

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

2010-09-30 Thread Christian Urban
Hi Walther, Here my guess what is going on: Given val t = @{term a + b * x = (0 ::real)}; val pat = parse_patt thy ?l = (?r ::real); val precond = @{term l is_polynomial}; we match val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty); in order to get an environment for

[isabelle-dev] error in cook book ?

2010-09-07 Thread Christian Urban
Hi Nils, Nils Jähnig writes: Hi, 1) i'm reading the cook book, and in chapter 6, page 135 on the bottom (latest draft from August 28th) , there is a piece of code including Simplifier.simproc_global_i, which gives an error. i went with simproc_i, this seems ok. This is

[isabelle-dev] Sane Mercurial history

2010-03-04 Thread Christian Urban
On the topic of Mercurial: There is a nice 6-part tutorial about it at http://hginit.com/01.html Maybe too basic for the seasoned users, but funny nonetheless. And an example for a very crisp-clear piece of writing. Christian Makarius writes: On Wed, 3 Mar 2010, Brian Huffman wrote:

[isabelle-dev] Pattern.match -- a minute

2010-03-03 Thread Christian Urban
Dear Walther, About your second question: there is a section about using the function Pattern.match in the Programming Tutorial ([1], Section 3.3). It should explain how to do such pattern match examples. The main contortion below probably comes from the parsing of input. Since the

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

2007-09-14 Thread Christian Urban
Lawrence Paulson writes: 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. We previously put some effort