Perhaps this should be done uniformly for all single-constructor
datatypes, not just pairs. Any case expression with a single branch
could be printed as a let.
- Brian
On Thu, Oct 2, 2014 at 9:13 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
In a private discussion,
On Fri, Jul 11, 2014 at 5:54 AM, Askar Safin safinas...@mail.ru wrote:
Hi. I think I found a bug in the Isabelle 2013-2 (OS: Debian GNU/Linux 7,
Interface: jEdit). For example, I type the following in the jEdit Isabelle
interface:
==begin==
notepad begin
have A == B and C proof -
show
Hi everyone,
I've noticed that recent changesets (up to 00112abe9b25) on testboard
have completed Pure and HOL tests, but the HOL_makeall results never
show up. (The most recent HOL_makeall report is 3253aaf73a01, dated
March 18.)
Does anyone know why this is? Is one of the HOL theories going
On Tue, Mar 18, 2014 at 12:55 PM, Makarius makar...@sketis.net wrote:
Are you actually working together with Johannes Hölzl on these parts, or is
your later change 32b7eafc5a52 merely a coincidence?
We are not working directly together, but I suppose that the same
email conversation with Larry
On Fri, Sep 27, 2013 at 12:16 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
context field_char_0
begin
…
lemma of_rat_minus: of_rat (- a) = - of_rat a
apply transfer
the »- _« (name uminus) gets replaced by a bound variable »uminusa«.
There seems to be a
On Mon, Sep 30, 2013 at 2:34 PM, Makarius makar...@sketis.net wrote:
According to the normal context discipline, free variables are always fixed,
like a local const. We have a few tools that violate that principle and
consequently cause confusion, e.g. the Simplifier. There are sometimes
/6324f30e23b6/src/HOL/ex/Numeral_Representation.thy
Can we delete that, and keep the history inside the history? Or are there
remaining aspects that are not in the official numeral implementation (and
reform) by Brian Huffman?
Numeral_Representation.thy defines a couple of type classes for
subtraction
I discovered a problem with the pretty-printing of some terms (I am
using revision 4392eb046a97).
term (λ(a, b) (c, d). e) x y
case_guard True x
(case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d). e
case_nil)
y
:: 'e
I assume this is a result of the recent changes
printer
just to get this behavior back.
- Brian
On 24.04.2013 02:10, Brian Huffman wrote:
I discovered a problem with the pretty-printing of some terms (I am
using revision 4392eb046a97).
term (λ(a, b) (c, d). e) x y
case_guard True x
(case_cons (case_abs (λa. case_abs (λb. case_elem
It would be nice to get HOLCF case combinators working with this new
system, as the parsing for HOLCF case expressions has been a bit
broken for some time.
Can case combinators and constructor functions with
continuous-function types be made to work with the case_tr (or
case_translation?)
On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner breit...@kit.edu wrote:
Hi,
Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius:
This has got nothing to do with Isabelle's informal conventions but is
all about the target language's formal rules.
The conventions about theory names
were introduced by Brian Huffman here:
changeset: 45775:6c340de26a0d
user:huffman
date:Wed Dec 07 10:50:30 2011 +0100
files: src/HOL/Library/Extended_Nat.thy
description:
add cancellation simprocs for type enat
We should Brian give time to comment
On Fri, Oct 5, 2012 at 10:37 AM, Makarius makar...@sketis.net wrote:
On Thu, 4 Oct 2012, Brian Huffman wrote:
I was reluctant to support closed type definitions at all in HOLCF's
cpodef and friends, preferring to make (open) the default behavior; but in
the end I decided it was more important
On Thu, Oct 4, 2012 at 2:17 PM, Makarius makar...@sketis.net 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
typedef (open) new_type = some set
but as far as I can
On Sun, Jul 29, 2012 at 7:11 PM, Makarius makar...@sketis.net wrote:
The question is if HOL-Plain and HOL-Main still have any purpose. Full HOL
now takes 2min on a reasonably fast machine with 4 cores.
Images like HOL-Plain or HOL-Main are often useful when I am doing
development on libraries
On Thu, Jul 19, 2012 at 8:32 AM, Christian Sternagel
c-ste...@jaist.ac.jp wrote:
I created a repository at
http://sourceforge.net/p/holcf-prelude/
Thanks for setting this up!
PPS: As I mentioned in an earlier mail. I would like to add a constant set
:: 'a Data_List.list = 'a set for
On Wed, Jul 18, 2012 at 8:52 AM, Christian Sternagel
c-ste...@jaist.ac.jp wrote:
On 07/17/2012 07:53 PM, Brian Huffman wrote:
HOLCF/Library/{Nat,Int}_Discrete.thy define cpo instances for types
nat and int, so you can write types like nat - 'a list or
nat\^sub\bottom - 'a list. Decisions about
On Tue, Jul 17, 2012 at 11:04 AM, Christian Sternagel
c-ste...@jaist.ac.jp wrote:
Dear all,
I put together some functions on lists (that I use in some small proof) in
Data_List.thy. While doing so and thinking about functions and proofs I
would need in the future, I stumbled across the
On Thu, May 31, 2012 at 1:36 PM, Makarius makar...@sketis.net wrote:
On Thu, 31 May 2012, Andreas Lochbihler wrote:
At some point, when I have bundles ready to work with the existing
notation commands, we can fine-tune this scheme further, to allow users
to
'include' syntax in local
On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkow nip...@in.tum.de wrote:
How can I see the possible cases in an induction, i.e. Show me cases in PG?
You can type the command print_cases into your theory file (this
also works in PG).
But then the real question is, how do we expect new users to
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
c-ste...@jaist.ac.jp wrote:
is it really the case that currently the only way to obtain ASCII output
using print modes is by specifying the empty string, like
thm () conjE
or did I miss anything? Since this print mode is occasionally
On Thu, Apr 19, 2012 at 4:02 PM, Makarius makar...@sketis.net wrote:
On Tue, 10 Apr 2012, Brian Huffman wrote:
On Tue, Apr 10, 2012 at 3:06 PM, Makarius makar...@sketis.net wrote:
Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error:
*** No code equations
On Thu, Mar 29, 2012 at 7:50 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
As it is now, theory »Code_Nat« is
not announced that prominently, but this is not that critical.
We should at least put an announcement in NEWS about Code_Nat.
However, you have talked about
On Wed, Mar 28, 2012 at 9:15 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Btw. for the moment you have not transferred by additional changes
concerning Efficient_Nat etc. What are your plans for these? To wait
until the transition proper has fortified a little? Or
On Mon, Mar 26, 2012 at 7:23 PM, Makarius makar...@sketis.net wrote:
On Mon, 26 Mar 2012, Lukas Bulwahn wrote:
This problem is reproducible on our testboard servers. At the moment, all
tests of changesets after 2a1953f0d20d have to be manually aborted because
of that reason. I hope you find a
As of 2a1953f0d20d, Isabelle now has a new representation for binary numerals:
*** HOL ***
* The representation of numerals has changed. We now have a datatype
num representing strictly positive binary numerals, along with
functions numeral :: num = 'a and neg_numeral :: num = 'a to
represent
Hello all,
I am writing about the following recent changeset, which adds another
left-fold operator to HOL/List.thy.
author haftmann
Fri Jan 06 10:19:49 2012 +0100 (6 days ago)
changeset 46133 d9fe85d3d2cd
parent 461325a29dbf4c155
child 46134 4b9d4659228a
incorporated canonical
Hi all,
I have been working on a new numeral representation for Isabelle
recently, and I would like to share it with everyone. An overview of
the design is now available on the Isanotes wiki [1]; a patched
version of the Isabelle hg repo is also available [2].
[1]
On Sun, Nov 20, 2011 at 9:52 PM, Makarius makar...@sketis.net wrote:
* Commands 'lemmas' and 'theorems' allow local variables using 'for'
declaration, and results are standardized before being stored. Thus
old-style standard after instantiation or composition of facts
becomes obsolete. Minor
On Fri, Nov 4, 2011 at 8:32 PM, Makarius makar...@sketis.net wrote:
This syntax is only defined for single abstractions, but the categories got
mixed up (the nonterminals via syntax types):
syntax
_lebesgue_integral :: 'a = ('a = real) = ('a, 'b)
measure_space_scheme = real
(\integral
Hello all,
Lately I have been trying to clean up the code of the cancellation
simprocs, and I have come across something I don't understand.
One set of simprocs will cancel factors from inequalities, rewriting
terms like x * z y * z to either x y or y x, depending on
whether it can prove 0 z
Hello all,
This is a follow-up to the conversation on the isabelle-users list
from a few months ago, about confusion that arises when using mutual
induction with the arbitrary option.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-June/msg1.html
At the time I suggested that their
On Wed, Oct 12, 2011 at 4:01 PM, Makarius makar...@sketis.net wrote:
On Wed, 12 Oct 2011, Brian Huffman wrote:
After implementing the warning, I dug through the revision history and
was surprised to find that my new feature actually used to exist! It
was removed in January 2006:
http
On Thu, Sep 22, 2011 at 6:10 AM, Makarius makar...@sketis.net wrote:
On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
On Sun, Sep 18, 2011 at 1:42 AM, Gerwin Klein gerwin.kl...@nicta.com.au wrote:
After not running in the test for quite some time, JinjaThreads now comes
back failing:
*** Undeclared constant: semilattice_sup_class.sup
*** At command definition (line 20 of
On Fri, Sep 16, 2011 at 2:01 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Hi Brian,
I am not totally happy with changes like:
http://isabelle.in.tum.de/reports/Isabelle/rev/4657b4c11138#l1.7
The proof text itself is shorter than before, but in less trivial
On Fri, Aug 26, 2011 at 7:06 AM, Lawrence Paulson l...@cam.ac.uk wrote:
I am trying to process the following declaration in Probability/Sigma_Algebra:
inductive_set
smallest_ccdi_sets :: ('a, 'b) algebra_scheme \Rightarrow 'a set set
.
.
.
monos Pow_mono
I get the following error
On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp schr...@in.tum.de wrote:
On 08/26/2011 06:50 PM, Tobias Nipkow wrote:
I agree. Since predicates are primitive, starting from them is
appropriate.
Tobias
Did I get this right:
the idea is to implement our advanced typedef via a HOL4-style
On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
HOL-Hoare_Parallel FAILED
Also Hoare_Parallel is non-terminating.
I have a patch for this one:
http://isabelle.in.tum.de/repos/isabelle/rev/5e681762d538
Once this changeset gets merged into
On Fri, Aug 26, 2011 at 1:38 PM, Makarius makar...@sketis.net wrote:
On Fri, 26 Aug 2011, Brian Huffman wrote:
Here's one possible approach to the set-axiomatization/typedef issue:
As a new primitive, we could have something like a pred_typedef
operation that uses predicates. This would work
On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp schr...@in.tum.de wrote:
On 08/26/2011 10:38 PM, Makarius wrote:
What is gained from that apart from having two versions of typedef?
I am with you here.
We don't need two primitive versions of typedefs.
This is incorrect: Only the
On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp schr...@in.tum.de wrote:
locale bla =
assume False
typedef empty = {}
Now I have to put up with the fact the semantic interpretation of empty is
the empty set. Formerly only non-empty sets were semantic interpretations of
type constructors.
On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson l...@cam.ac.uk wrote:
I've come across something strange in the file
isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if
anybody could think of an explanation.
A proof works only if I insert before it the following:
Hello everyone,
Isabelle prints out warning messages whenever anyone declares a
duplicate simp rule, intro rule, etc. It would be nice if Isabelle
would print a similar warning whenever a definition reuses a name that
is already in scope in the current context. For example, if a theory
defines a
On Fri, Aug 12, 2011 at 2:27 AM, Alexander Krauss kra...@in.tum.de wrote:
What are, actually, the losses when going back? This has not yet been
touched by this thread at all (except the compatibility/import issue
mentioned by Brian), and at least myself I wouldn't feel comfortable
answering
On Fri, Aug 12, 2011 at 4:07 PM, Makarius makar...@sketis.net wrote:
http://isabelle.in.tum.de/repos/isabelle/rev/13e297dc improves startup
time of the worker thread farm significantly, and I've got real times in the
range of 0.003s -- 0.005s on my old machine from 2 years ago with Proof
On Thu, Aug 11, 2011 at 5:43 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Hello together,
recently in some personal discussions the matter has arisen whether
there would be good reason to re-introduce the ancient set type
constructor. To open the discussion I have
Hello all,
Recently I've been hacking on a bunch of proof scripts using the
development version of Isabelle, and I noticed that when processing
proof scripts, I often get a noticeable pause at uses of simp_all.
The same pause does not occur with Isabelle2011.
Below is a minimal theory file to
Your confusion stems from the fact that your theory file is also
called ms. The simps rules generated by the record command are
qualified by both the theory name and the type name, so the full names
in your example are ms.ms.simps and ms.aut.simps. Referring to
either of these by their full names
, records and datatypes) as
countable
(see ~~/src/HOL/Library/Countable).
It seems that for datatypes we now have such functionality, implemented four
weeks ago by Brian Huffman:
http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f
It comes in the form of a method, so it has
I wrote to Florian about this exact issue back in February 2010.
Florian's recommended solution at the time was to add a new subclass
of archimedean_field that fixes the floor function and assumes a
correctness property about it. This solution is really easy to
implement (see attached diff). If
Obviously, the naturals assign a non-standard meaning to negative numerals.
But are there any types that assign a non-standard meaning to
*positive* numerals? (By standard I mean 2=1+1, 3=1+1+1, 4=1+1+1+1,
etc.) Is there any reason why anyone would ever want to define or use
such a type?
If not
Hello all,
I just noticed this error message from primrec if you write a
specification that is not primitive recursive. Here is a simplified
example:
primrec foo :: nat = nat where
foo 0 = 1 | foo (Suc n) = foo 0
*** Extra variables on rhs: foo
*** The error(s) above occurred in definition
The *_tac-style instantiation might be out of fashion, but the same
parsing rules for indexnames are also used with the where attribute,
which is still quite useful.
- Brian
On Tue, Feb 8, 2011 at 7:59 AM, Lawrence Paulson l...@cam.ac.uk wrote:
Obviously this proposal would involve a
On Tue, Feb 8, 2011 at 9:01 AM, Lawrence Paulson l...@cam.ac.uk wrote:
Historically, the point is that index numbers were regarded as very important
in variable names, while identifiers ending with digits were not seen as
important. And there are other ways of making multiple identifiers.
On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber webe...@in.tum.de wrote:
On Fri, 2011-01-21 at 15:27 +0100, Tobias Nipkow wrote:
One issue can be that if some sort involves multiple type classes, the
corresponding class may not have been defined. That is the one advantage
of sorts: you can create
Hello all,
I recently discovered that warnings about the secondard search path
are generated more often than they ought to be. I am using repository
version 1fa4725c4656.
Create two files A.thy and B.thy with the following contents:
theory A
imports ~~/src/HOL/Library/Cardinality
begin
end
On Thu, Jan 6, 2011 at 8:59 AM, Makarius makar...@sketis.net wrote:
If everybody else manages to wrap up until the beginning of next week, we
have a good chance to release before the end of the month.
This sounds good.
I think a release date of January 2011 still justifies to call the release
On Thu, Dec 2, 2010 at 8:42 AM, Makarius makar...@sketis.net wrote:
Right now there is already a clear warning -- which Proof General happens to
show in a hardly visible way, but that is just one of many problems of Proof
General. In Isabelle/jEdit the warning is hard to miss. I will check
On Tue, Nov 30, 2010 at 8:35 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
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«,
***\let
*** l.27 ...\isaliteral{22}{\isachardoublequoteclose}}
***
{\isaliteral{29}{\isacharp...
***
*** ))
- Brian
Brian Huffman schrieb:
On Fri, Nov 19, 2010 at 7:28 AM, Brian Huffman bri...@cs.pdx.edu wrote:
The latex document generation still doesn't work, though
On Fri, Nov 19, 2010 at 2:40 PM, Joachim Breitner
m...@joachim-breitner.de wrote:
Hi everyone,
[...]
I’m sorry for the trouble my submission causes. When writing the
theories I had planned to actually use the proof document as my project
report, therefore the trouble I went through to have the
Hello everyone,
Recently I noticed that in HOLCF, whenever I do a theorem search for
theorems containing the constant UU (i.e. bottom), the search fails
with an UnequalLengths exception. I tracked the problem down to this
specific theorem from Fun_Cpo.thy: Before this point, find_theorems
UU
)
Find_Theorems.sorted_filter(2)
Find_Theorems.find_theorems(5)find_all(2)
Find_Theorems.find_theorems(5)find_all(1)
Find_Theorems.print_theorems(5)
Toplevel.apply_tr(3)(1)
Runtime.debugging(2)(1)
End of trace
*** exception UnequalLengths raised
*** At command find_theorems
Larry
On 18 Nov 2010, at 16:03, Brian
The effect of my change typedef (open) unit is to remove the
definition of the following constant
unit_def: unit == {True}
thus making the name unit available to users.
- Brian
On Thu, Nov 18, 2010 at 1:58 PM, Makarius makar...@sketis.net wrote:
Hi Brian,
can you say a few words about
On Thu, Nov 18, 2010 at 2:59 PM, Makarius makar...@sketis.net wrote:
On Thu, 18 Nov 2010, Brian Huffman wrote:
The effect of my change typedef (open) unit is to remove the
definition of the following constant
unit_def: unit == {True}
thus making the name unit available to users.
So
On Thu, Nov 18, 2010 at 1:58 PM, Makarius makar...@sketis.net wrote:
For some reason, many people have started to sequeze everything in a single
line (frequent), or imitate the headline/body text format of other projects
with a completely different structure (rare). The reason might be as
On Fri, Nov 12, 2010 at 5:48 AM, Makarius makar...@sketis.net wrote:
On Thu, 11 Nov 2010, Brian Huffman wrote:
Here is the reason I am reluctant to use transparent ascription:
Programmers use modules and signatures as an abstraction mechanism. (I
shouldn't need to explain to anyone
On Wed, Nov 3, 2010 at 5:56 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
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
The log message, Naming in line now with multisets seems to suggest
that consistency was the main motivation for this change. However, the
change had rather the opposite effect, since the expand_*_eq pattern
is much more common in the libraries. (Full disclosure: some, but not
all, of these lemmas
, that for pairs it would be a bit
unusual, although it fits a certain view of pairs.
Tobias
Am 07/09/2010 17:22, schrieb Brian Huffman:
The log message, Naming in line now with multisets seems to suggest
that consistency was the main motivation for this change. However, the
change had rather
On Tue, Jun 15, 2010 at 2:03 AM, Lawrence Paulson l...@cam.ac.uk wrote:
Altering the behaviour of the safe method on locale constants might be
feasible, because it would affect only a few proofs. Can anybody tell me
whether there is an easy way to identify whether a free variable is actually
I think I just found answer to my question:
fun eta_tac i = CONVERSION Thm.eta_conversion i
I had never used CONVERSION until now. I guess that what it does is
apply the conversion to the entire subgoal?
- Brian
On Sat, May 22, 2010 at 12:07 PM, Brian Huffman bri...@cs.pdx.edu wrote:
Does
Hello all,
I recently finished a formalization of real numbers that uses Cauchy
sequences. I thought it might be good to replace the current
formalization (which uses Dedekind cuts) with this new one in time for
the upcoming Isabelle release.
Users should not need to know or care which
On Mon, May 10, 2010 at 12:41 AM, Walther Neuper neu...@ist.tugraz.at wrote:
A comment you ask for: Your assumption, that users should not need to know
or care which construction of reals we use, does not apply in education.
There are several attempts to design educational software for (pure
On Mon, May 10, 2010 at 3:59 AM, Makarius makar...@sketis.net wrote:
This means there are about 1-2 weeks left for bigger changes. Do you manage
to exchange the reals by then?
I can do it today. I have already exchanged the reals and tested
everything in a local clone of the Isabelle repo. I
Hello,
With tracing turned on, one can see that the following lemma is solved
with the help of the linordered_ring_less_cancel_factor simproc (which
is defined in HOL/Tools/numeral_simprocs.ML):
lemma RR: (0::'a::linordered_idom) z == (x*z y*z) = (x y)
by simp
Similarly, the following lemmas
Hello all,
I am looking for some advice on a design decision for the HOLCF fixrec package.
Fixrec uses the simplifier when doing its internal proofs of the
defining equations for a function. Currently it maintains its own
special simpset for this purpose, which users can extend by declaring
Hi Alex,
Thanks for the info about the function package. I'll give a bit more
explanation of the proofs that fixrec does, using an example:
domain 'a LList = LNil | LCons 'a (lazy 'a LList)
fixrec mapL :: ('a - 'b) - 'a LList - 'b LList where
mapL$f$LNil = LNil
| x ~= UU ==
On Mon, May 3, 2010 at 4:55 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
class top = preorder +
fixes top :: 'a
assumes top_greatest [simp]: x \le top
class bot = preorder +
fixes bot :: 'a
assumes bot_least [simp]: bot \le x
The fact that both class
as the function package warning
messages. I wouldn't be surprised if warnings pop up in other packages
as well.
- Brian
On Mon, May 3, 2010 at 12:48 PM, Alexander Krauss kra...@in.tum.de wrote:
Hi Brian,
Thanks for bisecting this, I'll have a look.
Alex
Brian Huffman wrote:
Recent
On Wed, Mar 3, 2010 at 8:54 AM, Makarius makarius at sketis.net wrote:
* For longer projects the timespan of staying in splendid isolation
is limited to 1-3 days (3 is already quite long, and personally I
usually try to stay within the 0.5-1.5 days interval).
...
Of course, the merge
On Fri, Feb 19, 2010 at 8:18 AM, Rafal Kolanski rafalk at cse.unsw.edu.au
wrote:
Looks like it should be @{const apply_rsp} or @{text apply_rsp} or
something. The underscore is throwing it.
That's exactly it. There's actually a second problem of the same kind
later on, in a subsection heading.
From my most recent hg pull:
pulling from ssh://huffman at
atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
searching for changes
adding changesets
adding manifests
adding file changes
added 605 changesets with 1325 changes to 175 files
Wow! What just happened?
-
On Thu, Nov 12, 2009 at 2:06 PM, Andreas Schropp schropp at in.tum.de wrote:
In a sense, eq_reflection is a meta-thereom, but Pure is not a meta-logic,
so it cannot be proven within the system. ?Thus we need to add it as an
axiom.
But we can prove all instances of the eq_reflection
On Thu, Nov 12, 2009 at 1:12 AM, Lawrence Paulson lp15 at cam.ac.uk wrote:
If you do these things, you put an end to all Isabelle logics other than
Isabelle/HOL. Remember, an object logic does not need to possess an equality
symbol or even an implication symbol.
OK, good point. All the
Hello all,
This morning I was looking at the following comment from HOL.thy:
ext:(!!x::'a. (f x ::'b) = g x) == (%x. f x) = (%x. g x)
-- {*Extensionality is built into the meta-logic, and this rule expresses
a related property. It is an eta-expanded version of the
Hello again,
While I'm on the subject of redundant axioms, consider this piece of HOL.thy:
axioms
iff: (P--Q) -- (Q--P) -- (P=Q)
True_or_False: (P=True) | (P=False)
Has anyone else noticed that axiom True_or_False implies axiom
iff? (You can just do a proof by cases on P and Q.) I
I think it's time to bring up the issue of bug tracking again. I just
replied to Peter Lammich on the Isabelle users list about a bug in the
locale package that has been known to exist for at least a year and a
half; it is unclear whether anyone has taken any responsibility for
fixing the bug, or
On Wed, Jul 1, 2009 at 4:46 AM, Amine Chaiebac638 at cam.ac.uk wrote:
I wonder why this restriction has been introduced in the first place. Is
it because sorts can be empty (i.e. there are no possible type
instances)?
That's exactly right. Theorems need to have sort hypotheses to prevent
On Thu, Jun 18, 2009 at 10:55 AM, Makariusmakarius at sketis.net wrote:
?* The main Isabelle repository http://isabelle.in.tum.de/repos/isabelle
? ?always needs to be in a state where
? ? ?isabelle makeall all
? ?finishes succesfully!
This last failure was due to some changes that I pushed
On Thu, Jun 18, 2009 at 2:56 PM, Makariusmakarius at sketis.net wrote:
isabelle makeall TARGETS merely runs isabelle make TARGET in every
logic directory -- this is a very ancient arrangement. ?This means it
stops after the first failure in each directory, but tries the other
directories
Quoting Makarius makarius at sketis.net:
I've found some nice illustrations on the web ...
Mercurial: http://tinyurl.com/cxrbjt
CVS:http://tinyurl.com/dk3gsz
So, you're saying that with Mercurial, you can do a lot more damage?
;-)
- Brian
Quoting Tobias Nipkow nipkow at in.tum.de:
This is exactly the point: recursive functions defined by pattern
matching expect Suc. They tend to dominate the scene in CS-oriented
applications. Hence Suc 0 is made the default. However, for math
applications this tends to be inconvenient, esp in
Quoting Tobias Nipkow nipkow at in.tum.de:
IIRC, 1 used to abbreviate Suc 0. Making 1 = Suc 0 a simp rule
mimiced that.
Aha! The real reason comes out. Now things are starting to make sense...
It allows you to write 1 on the rhs of an equation
because (if used as a simp rule) the 1 will be
Quoting Florian Haftmann florian.haftmann at informatik.tu-muenchen.de:
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
Quoting Florian Haftmann florian.haftmann at informatik.tu-muenchen.de:
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
encourage
Hello,
I have been thinking about all the conflicts caused by the typerep
class, and what should be done about it.
Basically, this is an instance of a more general problem. The Isabelle
libraries define some types, and they also define some type classes.
The problem, stated simply, is
I thought it would be good to clarify my position in a shorter email:
The automatically-generated typerep instances work fine on typedef or
datatype commands, where the instance resides in the same theory as
the type definition.
It is also OK if instances are generated *within Typerep.thy*
Hi Amine,
In the interest of making your proof scripts more robust, I think it
is best to avoid relying on the term ordering whenever possible.
Specifically, if you have a tactic like (simp add: mult_ac) that does
not completely solve the subgoal, and the following tactic relies on
the
1 - 100 of 112 matches
Mail list logo
