I believe Florian's proposal is good. On a proof-engineering level, the
only "inconvinience" is mainly that the property
gcd a b * lcm a b = a * b
does not hold as such but generally I suspect in the form
gcd a b * lcm a b = normalize(a * b) -- The normalize in GCD.thy perhaps
has the property
At the time we decided against it due to the following:
By design arith has to solve its goal or fail fast otherwise. Quantifier
Elimination is just the opposite of both, since its is in its general form
a conversion, and also due to very hard complexity costs (in particular
for this MIR theory)
I remember trying to convert Cooper's as well as other Decision proc's
recdefs to fun, also with the help of Alex but gave up at some point.
I think the killer at the time was rather the induction principle and
not the simp rules. The one derived by recdef really fits the definition
and
Hi,
I came across a situation where the order of sublocale declarations
makes a difference in the theory development, which in this case is not
clear to me. Can anyone please clarify the following behaviour within
the simplified case below? Is the behaviour due to purely technical
reasons or
Thanks Andreas. Does this mean that this sublocale scenario is
prohibited? And if so, is it due to technical reasons or is there a
fundamental problem here?
Amine.
On 01/31/2013 02:04 PM, Andreas Lochbihler wrote:
Hi Amine,
the error message in the second case is only delayed: You get it,
technical reasons; Clemens might be able to tell you more.
Andreas
On 01/31/2013 02:56 PM, Amine Chaieb wrote:
Thanks Andreas. Does this mean that this sublocale scenario is
prohibited? And if so, is it due to technical reasons or is there a
fundamental problem here?
Amine.
On 01/31/2013 02
Hi,
Many thanks for your very detailed response! I wonder what to do next in terms
of documenting this method, and perhaps, developing it further. Is there a
latex source for the information you sent? It could be added to the
documentation somewhere: but where?
I could send the Latex
I am also in favor of the set type-constructor. The issue of
compatibility with other HOL provers could very probably be solved by
the transfer mechanism. If not immediately from the generic setup, the
surely from a tailored one dedicated to this issue, if enough people are
concerned.
Amine.
Thanks Florian, it helps. It is apparently the same issue as with
typerep. I fixed it.
Amine.
Florian Haftmann wrote:
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
Hi Brian,
Many thanks for the explanation. Indeed, if I make Abstract_Rat import
say Complex_Main, the proofs work without the sort assumption. This must
be due to the fact that concrete instances of field (I think) come only
after Main.
That's exactly right. Theorems need to have sort
Is it about removing the {..n} completely or just for SUM?
Amine.
Tobias Nipkow wrote:
On nat, the sets {0..n} and {..n} are the same, which can be irksome.
Hence I discourage the use of {..n}. However, there are notations such
as SUM k=n. t which stand for setsum (%k. t) {..n} and introduce
Hi,
I updated and get the following error. What is Option?
Amine.
bash-3.2$ hg fetch
Password:
pulling from
ssh://chaieb at
atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
searching for changes
adding changesets
adding manifests
adding file changes
added 220
I think somebody removed Option.thy but left the dependency in the
Makefile. This is strange since it is still needed by Extraction
(Plain). theory Extraction imports Option
Amine.
Amine Chaieb wrote:
Hi,
I updated and get the following error. What is Option?
Amine.
bash-3.2$ hg
As long as it is not Coq this looks great. An I am sure with Jasmin's
and Sascha's new ideas and approaches second best won't last very long :)
Amine.
Tobias Nipkow wrote:
Not sure, possibly Leo II. No other ITP is in the competition.
Tobias
Amine Chaieb schrieb:
Second best
I completely agree with Brian (even I can not agree to import Main
instead of theories under Main).
There is only two things I can think of:
1) You can't be serious about this
2) We are all sitting back and watching how things get worse.
The bootstrap process of Main *was* fragile. For
Dear all,
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
and Misc.typerep_^_inst.typerep_^_def
I've moved things up (although this is really artificial).
Misc imports Complex_Main anyway, and I made Permutations import Main,
the problem 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
science.
Florian Haftmann wrote:
Can you provide me with a theory graph of Permutations and Misc? (Isar
command thy_graph, export to ps/pdf)?
Florian
Amine Chaieb schrieb:
I've moved things up (although this is really artificial).
Misc imports Complex_Main anyway, and I made
Florian Haftmann wrote:
Amine Chaieb schrieb:
Do you mean thy_deps? It's not working on my machine.
Yes, thy_deps of course (sorry for the slip). But thy doesn't it work?
cd lib/browser
make
should do the job...
Florian
Can you do
cvs -d
haftmann
OK
Florian Haftmann wrote:
I have to bother you further:
it is necessary to unfold the [HOL] node in the graph (by clicking on
it) because we need to inspect the internal structure of the HOL theories.
Florian
Amine Chaieb schrieb:
Florian Haftmann wrote:
Amine Chaieb schrieb
and the fishing rules...
Our current policy is that Plain, Main and Complex_Main are either
ancestors or descendants of any theory.
But feel free to ask if this is still obscure.
This rule does not tell me anything since it is trivally satisfied by
any connected graph containing
Hi,
I left Fact.thy alone because it is necessary for building HOL. I moved
it upwards though (now it imports Nat instead of RealDef). I added the
other stuff to Binomial since it is Library stuff and not necessary
for building HOL.
This said, I have no objection (or strong opinion about) to
Dear all,
Jeremy (and I) are encountering some (to us) strange problems with the
class-package (it might also be the locale-part, so your expertise is
highly welcome here). I am using Isabelle version 20 minutes ago.
Attached is a small theory illustrating the problem. Originally, line 32
Thanks for the quick answer!
At least we know that it was not because we wrote things in a wrong manner.
best wishes,
Amine.
Florian Haftmann wrote:
Hi Amine,
sorry for the inconvenience. Currently there is major upheaval going on
in the locale/class area. Im working hard on solving
with all the theories imorted by
Complex_Main, it works. Is this behaviour really intended? Maybe I
should reboot?
Best wishes,
Amine.
Amine Chaieb wrote:
Dear all,
When I try to merge two theories I get this (to me new) error message:
*** Clash of specifications
Brian Huffman wrote:
For multivariate polynomials, one way to get these would be to simply
iterate the univariate polynomial type constructor. For example, you
can think of the type 'a poly poly as representing polynomials over
two variables with coefficients in 'a.
Yes that's what I did
Brian Huffman wrote:
I just meant using a typedef, something like
typedef 'a poly = {f :: 'a fps. finite_fps f}
Then the operations like addition, multiplication, etc. could be
defined in terms of the underlying fps operations like this
definition
p * q = Abs_poly (Rep_poly p *
Dear all,
(How) Can I perform an instantiation of a type-constructor with two
arguments, an thereby restricting them to be the same?
Concrete problem:
instantiation fun (type, type) power
begin
end
but I want only to raise functions of type 'a = 'a to powers.
Thank you for any hint!
Very nice job!
Amine.
PS: In Reflected Ferrack you start combutation with True, i.e. @{code
T}, if the input is @{term False}. Fortunately this does not happen
often Even with @{code} we still need to be careful...
Florian Haftmann wrote:
New ML antiquotation 'code': takes constant as
This would have not been possible without merging some classes.
Which?
Just these:
class recpower_semiring = semiring + recpower
class recpower_semiring_1 = semiring_1 + recpower
class recpower_semiring_0 = semiring_0 + recpower
class recpower_ring = ring + recpower
class recpower_ring_1 =
this. (IMHO the key point is that we have to stop to abuse to type
system to achieve the same notation for different operations).
I don't see why the recpower is an abuse of the type system... If I
want to use inside a class, the type is fixed and I see no problem...
This was not my point
This is perhaps an occasion to advertise Library/Executable_real.thy,
which contains a verified implementation of rational numbers to be have
like HOL --- So here you would no get an exception when dividing by
zero, but just zero as you expect.
Florian integrated this into the CVS to work with
32 matches
Mail list logo
