Here is another follow-up to the relcomp story so far:
changeset: 47508:85c6268b4071
tag: tip
user:wenzelm
date:Tue Apr 17 16:48:37 2012 +0200
files: doc-src/TutorialI/Sets/Relations.thy
description:
updated rel_comp ~ relcomp (cf. e1b761c216ac);
Sorry for the inconveniences.
On 04/17/2012 11:55 PM, Makarius wrote:
Here is another follow-up to the relcomp story so far:
changeset: 47508:85c6268b4071
tag: tip
user: wenzelm
date: Tue Apr 17 16:48:37 2012 +0200
files: doc-src/TutorialI/Sets/Relations.thy
description:
updated rel_comp ~
On 04/16/2012 09:13 AM, Christian Sternagel wrote:
Hi all,
On 04/03/2012 02:51 AM, Florian Haftmann wrote:
well, I suggest to augment the existing theory with lemmas transferred
from relpow to relpowp to emphasize that both worlds exists and that
lemmas can be found easier by find_theorems.
On Fri, 13 Apr 2012, Lukas Bulwahn wrote:
Since your changes 07f4bf913230 and b75ce48a93ee were a bit too long
stuck in the pipeline, you then had a non-trivial merge in
e1b761c216ac. It seems that Lukus did not want to redo that via a
variant of rebasing (e.g. plain hg import of individual
On Fri, 13 Apr 2012, Christian Sternagel wrote:
Moreover, incoming changesets needs to be easy to inspect in a few
seconds or minutes. (This is why I always ask to write each log item on
a separate line, but still with a delimiter such as ;).
Indeed. I hope my commit messages have at least
On Fri, 13 Apr 2012, Makarius wrote:
On AFP I've also seen a machine default for fetch merges. This is the
canonical configuration for it:
[extensions]
hgext.fetch =
[defaults]
fetch = -m merged
I won't argue about the exact spelling of the merged, but it should not be
the machine
On Wed, 11 Apr 2012, Christian Sternagel wrote:
On 04/05/2012 12:30 PM, Christian Sternagel wrote:
Hi Lukas,
thanks for testing! (Sorry for the late reply, currently my
internet-connectivity is rather sporadic ;)). Please find attached a hg
bundle that does the name change 'rel_comp -
Hi Makarius,
On 04/13/2012 03:12 AM, Makarius wrote:
I now also know who this mysterious griff from AFP is :-) Seriously,
you have the free choice to specify your user name for Isabelle hg
contributions, but you need to stick to it in the long run. In the
initial warmup-phase you have one
Hi all,
On 03/31/2012 01:10 AM, Florian Haftmann wrote:
PS: I suggest to rename rel_comp into relcomp (to be consistent with
relpow).
This would also mean to rename the corresponding lemmas, although I
would also appreciate consistency. Also the »pred_comp« abbreviation
should be dropped,
Hi Chris,
I have tested your changeset on the testboard, and a couple of AFP
theories break, cf.
http://isabelle.in.tum.de/testboard/Isabelle/report/edd1df5c8daf4109a6366801aaeff7fd
(Some errors are due to your changes, some are due to current work of
others.)
It might be good to provide some
Hi Christian,
Sorry, I'm not familiar with the developer workflow. I do have a
cloned hg repo of Isabelle (from
http://isabelle.in.tum.de/repos/isabelle), but I don't see an
IsaMakefile (which would be required for isabelle make all). Where is
this IsaMakefile located?
it is »isabelle makeall
Hi Christian,
this has been added in
http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can
transfer theorems from the set relations in an ad-hoc using [to_pred].
You can also prove theorems for pred relations by means of … by (fact …
[to_pred]), as has been done in many
Hi Christian,
by the way, I noticed that sometimes [to_pred] yields undesirable
results (containing case-expressions), e.g.,
thm trancl_power[to_pred]
results in
(case ?p of (x, xa) ⇒ ?R^++ x xa) =
(∃n0. case ?p of (x, xa) ⇒ (?R ^^ n) x xa)
is this an inherent problem or could this
Hi Florian,
On 03/31/2012 01:10 AM, Florian Haftmann wrote:
Hi Christian,
To come back to the subject, I'm missing iteration of predicates,
i.e., what _^^n is on relations but for predicates ('a = 'a =
bool).
this has been added in
Dear all,
by the way, I noticed that sometimes [to_pred] yields undesirable
results (containing case-expressions), e.g.,
thm trancl_power[to_pred]
results in
(case ?p of (x, xa) ⇒ ?R^++ x xa) =
(∃n0. case ?p of (x, xa) ⇒ (?R ^^ n) x xa)
is this an inherent problem or could this be repaired
Hi Christian,
To come back to the subject, I'm missing iteration of predicates,
i.e., what _^^n is on relations but for predicates ('a = 'a =
bool).
this has been added in
http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can
transfer theorems from the set relations in an
Hi all,
currently there are two constants
op ^ :: 'b = nat = 'b
op ^^ :: 'b = nat = 'b
making it a bit difficult for the user to choose the correct one in all
situations. As far as I see op ^^ is just syntax for the overloaded
compow. Shouldn't it be possible to unify this (and also relpow)
17 matches
Mail list logo
