Re: [isabelle-dev] Proper sign of gcd / lcm on type int

[Amine Chaieb]

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 normalize (a*b) = normalize a * normalize b

This inconvinience is of course outeighted by the canonical representative
choice of representatives as Manuel points out.

The drawback on generated code by

> Integer.gcd = PolyML.gcd
> Integer.lcm = abs oo PolyML.lcm


is that in algorithms computing successive gcds, on every recursive call a
normalization step happens. For integers vs PolyML.lcm this might be
unnoticeable, but for more complex structures, appropriate code equations
might be more efficient.

Amine.

On Thu, June 2, 2016 2:19 am, Manuel Eberl wrote:
> Florian has already hinted at it, but I will say it again explicitly:
>
>
> Mathematically, gcd and lcm are not operations on the elements of a
> ring, but on the equivalence classes w.r.t. associatedness (i.e. mutual
> divisibility). In fact, these equivalence classes form a complete lattice
> w.r.t. divisibility, where inf = gcd, sup = lcm, Inf = Gcd, Sup = Lcm, bot
> = 1, top = 0.
>
>
> However, juggling equivalence classes is inconvenient; it is much nicer
> to use representatives, and ideally canonical representatives. This is why,
> in Isabelle, we require that the gcd/lcm be normalised. For natural
> numbers, everything is normalised; for integers, this means that the
> integer is non-negative; for polynomials, it means that the leading
> coefficient is normalised (if the coefficient ring is a field, this means
> the polynomial is zero or must have leading coefficient 1).
>
> I do think that we should enforce the same thing in the ML
> implementation of gcd/lcm. Any definition of gcd/lcm for integers where
> either of them may be negative does not make much sense to me. My guess
> would be that lcm can be negative in the implementation you mentioned
> because the author defined "lcm a b = a * b / gcd a b" with the unstated
> assumption that it is only called for non-negative numbers. Or perhaps
> they thought the sign does not matter.
>
>
> By the way, speaking of GCDs here and of rational numbers in the other
> thread: I am currently working on a theory of normalised fractions for
> arbitrary GCD rings. This builds on top of Amine Chaiebs fraction fields,
> but additionally requires that the numerator and denominator be normalised
> and the denominator be normalised, which makes the representation unique
> and therefore more convenient.
>
> This theory will then easily be instantiable for polynomials and formal
> power series, yielding rational functions and Laurent series, respectively.
> One could even base Isabelle's rational number theory on
> this more general development in the future.
>
>
> Cheers,
>
>
> Manuel
>
>
>
>
> On 31/05/16 21:37, Makarius wrote:
>
>> Dear integer experts,
>>
>>
>> presently on Isabelle/c3896c385c3e and AFP/d9305abd02e9, I am trying to
>>  understand the situation of gcd / lcm for negative arguments.
>>
>> We have the following slightly divergent operations:
>>
>>
>> * HOL gcd / lcm: always >= 0 (via "normalize" which is "abs")
>>
>>
>> * PolyML.IntInf.gcd: always >= 0
>> PolyML.IntInf.lcm: mixed signs, according to product of arguments
>>
>>
>> * Integer.gcd / lcm: mixed signs -- IIRC the implementation was only
>> meant to operate on "nat", which happens to be spelled "int" in ML.
>>
>> My impression is that the HOL definitions are canonical: several number
>>  theory experts have gone over it over the years. Is this correct?
>>
>>
>> An investigation of the (very few) uses of the above Poly/ML and
>> Isabelle/ML operations in Isabelle + AFP supports the following working
>> hypothesis:
>>
>>
>> Integer.gcd / lcm should follow the HOL versions, in "normalizing" the
>> sign, i.e. removing it. (The updated implementation will use
>> PolyML.IntInf gcd for improved performance.)
>>
>>
>>
>> Does this sound like a good idea?
>>
>>
>>
>> Makarius
>> ___
>> isabelle-dev mailing list isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle
>> -dev
>>
>>
> ___
> isabelle-dev mailing list isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-d
> ev
>

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] MIR decision procedure

[Amine Chaieb]

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) cannot generally fail fast.

For the same reason we did not have presburger, or ferrack or the other
procedures (from my thesis) inside arith.

Amine.

PS: Feerack is quantifier elimination over linear arithmetic (although I
had at some point quite relaxed conditions so it can work inside any dense
linear order with a between "picker", i.e. a function that given l and u
st. l But couldn’t these procedures be included in linarith, or at least in
> “try”?
> Larry
>
>
>> On 13 Nov 2015, at 16:18, Tobias Nipkow  wrote:
>>
>>
>> MIR is "documented" in Amine's IJCAR 2006 paper "Verifying Mixed
>> Real-Integer Quantifier Elimination". Maybe the title gives you a hint
>> what it is good for. Ferrack stands for Ferrante & Rackoff, who
>> invented this QE algorithm. This one may only be "documented" in
>> Amine's PhD.
>>
>
> ___
> isabelle-dev mailing list isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-d
> ev
>

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Amine Chaieb]

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 spirit of development. Also runtime at the time was not 
acceptable. I also remember havin the runtime problem with fun vs. 
primrec (so we left those there too).


  Context: Deep embedding of datatype + normal form on this data type + 
set of recursive functions on syntax preserving normal form. The normal 
Form has conditions on nested patterns -- introduce new constructor for 
these common nested patterns in normal form.


We had combinatorial explosion due to the depth of the patterns (which 
is the main reason to introduce special constructors in the datatype, to 
reduce deep patterns).


The induction priciples with recdef really fitted, i.e. induct auto with 
spice did the job for lemmas you do not expect to spend time thinking as 
a software developer.


One could argue that one should introduce a new data type for normalized 
syntactic elements and perform such computations as needed. I dismissed 
this idea and did not explore it, since it comes with a high price. 
Perhaps there are better ways to do the formalization.


Amine.


On 06/06/2015 08:37 PM, Tobias Nipkow wrote:



On 06/06/2015 20:11, Larry Paulson wrote:
Pattern matching is a convenience, and can always be eliminated 
manually. Is there really no reasonable way to re-express the 
definitions in Cooper.thy?


You can always turn all patterns of the lhs into cases on the rhs and 
derive the individual equations as lemmas. You also need to derive an 
induction principle. I would rather keep recdef than do all that by hand.


Tobias


Larry

On 6 Jun 2015, at 16:11, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote:



The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern matches. I
just tried Cooper.thy and changing one of the recdefs to function 
makes
Isabelle go blue (purple) in the face until one gives up. Hardware 
alone

will not solve that one.

Now one could argue that since we need recdef, we should also keep the
special variant defer_recdef, but if nobody speaks up for it, we don't
have a proof that we really need it and it should go.


At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me that no
application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  
Or do

we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?

Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 







___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Order of sublocale declarations

[Amine Chaieb]

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 is there a deeper sense?


The theory basically defines two locales A and B, which are equivalent 
when the parameter is transformed. Within locale A I have an 
abbreviation depending on a local fixed parameter. Suppose I have proved 
several interesting lemmas for locale A and would like to transfer them 
to locale B and vice vesa. The order in which the sublocale declarations 
between A and B appear indeed matters (in the form of the presence of an 
error related to duplicating the abbreviation declaration)


theory Test
  imports Main
begin

fun iter:: nat \Rightarrow ('a \Rightarrow 'a) \Rightarrow ('a 
\Rightarrow 'a \Rightarrow 'a) \Rightarrow 'a \Rightarrow 'a where

  iter 0 f0 f = f0
  | iter (Suc n) f0 f = (\lambdax. f (iter n f0 f x) x)

locale A = fixes f:: int \Rightarrow int \Rightarrow int
  assumes \And a. f a 1 = a 
begin

abbreviation fpower:: int \Rightarrow nat \Rightarrow int (infixr 
^f 80) where

  fpower x n == iter n (\lambdax. f 0 1) f x
end

locale B  = fixes g :: int \Rightarrow int \Rightarrow int
  assumes \And a. g a 0 = a

definition d:: (int \Rightarrow int \Rightarrow int) \Rightarrow 
(int \Rightarrow int \Rightarrow int)

  where d f = (\lambda a b. 1 - f (1 - a) (1 - b))

lemma dd[simp]: d (d f) = f
  by (simp add: d_def)


lemma AB_iff[simp]: B (d f) = A f
apply (auto simp add: A_def B_def d_def)
apply (erule_tac x=1 -a in allE)
apply simp
done

lemma BA_iff[simp]: A (d g) = B g
  using AB_iff[where f = d g]
  by simp


---

Since A and B are equivalent I introduce a transitional locale for A, 
to avoid infinite sublocale relationship


locale AB = A

Now to sublocale: In this order:

sublocale B  A d g
  unfolding BA_iff ..

sublocale AB  B d f
  unfolding AB_iff ..

I get an error at the second sublocale declaration:

*** Duplicate constant declaration local.fpower vs. local.fpower 
(line 13 of /home/ac/tmp/Test.thy)

*** At command sublocale (line 43 of /home/ac/tmp/Test.thy)

In this order however, everything works fine:

sublocale AB  B d f
  unfolding AB_iff ..

sublocale B  A d g
  unfolding BA_iff ..

Is there a reason I am missing?

Thank you in advance,
Amine
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Order of sublocale declarations

[Amine Chaieb]

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, once 
you open the AB context again (context AB begin). In the first case, 
it shows up immediately, because the sublocale command already 
constructs the context AB enriched with B.


Best,
Andreas


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Order of sublocale declarations

[Amine Chaieb]

Hi Andreas, T

his is of great help. Thank you, especially for the rewriting hint. I 
was thinking modulo that equation.


This solves my concrete problem, but I am still intrigued by the 
behaviour and its reasons.


Amine.

On 01/31/2013 03:21 PM, Andreas Lochbihler wrote:

Hi Amine,

let's look at what happens:

A defines the constant local.fpower as A.fpower f
AB inherits it from A, i.e., we have local.fpower == A.fpower f (1)
B  A d g produces local.fpower == A.fpower (d g)
AB  B d f inherits this as local.fpower == A.fpower (d (d f)) (2)

As the locale infrastructure does not know about d (d f) = f, it 
considers two different declarations of local.fpower from (1) and (2) 
as not being the same and therefore tries to declare both of them - 
which the local context infrastructure rejects.


You can either use prefixes to disambiguate local.fpower like in 
sublocale AB  b!: B d f

This gives you (1) and local.b.fpower == A.fpower (d (d f)).
Or, tell the locale infrastructure to rewrite d (d f) = f:

sublocale AB  B d f where d (d f) == f

The second approach only works if you order the sublocale declarations 
like in your second case. I do not know why, but I believe it has 
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:04 PM, Andreas Lochbihler wrote:

Hi Amine,

the error message in the second case is only delayed: You get it, once
you open the AB context again (context AB begin). In the first case,
it shows up immediately, because the sublocale command already
constructs the context AB enriched with B.

Best,
Andreas




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] the “algebra proof method

[Amine Chaieb]

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 Sources from my thesis and add a few lines on the 
method itself (attributes, installing it etc). The latter is perhaps 
subject to change when you change integration in arith?




Or would it make sense to integrate this functionality with the much better 
known arith method? It could then be a catchall for whatever else gets 
implemented in the general realm of arithmetic. And this reminds me that we 
have a great variety of different arithmetic decision procedures, which I 
imagine can all be invoked via arith, so maybe it indeed makes sense to add 
your algebraic procedures to arith.
As Tobias mentioned, the method is applicable for more general 
structures. Of course the main application are arithmetic domains nat, 
int, real, complex etc...


I think there should be no harm in adding an arith catcher to handle 
such problems, while keeping the algebra method itself for cases where 
the problem is not arithmetic in nature.


The method once installed for a locale, it generates simprocs, 
conversions, etc that could be used. So I would not suggest cutting it 
completely out in favour of an arith-like integration. But as a 
complementary method inside arith it could serve the users well.



Then there are your other research suggestions regarding the computation of a 
Gröbner basis. I'm guessing there that this would take a Ph.D. student due to 
the complexity of the topic itself as well as the need to get to grips with the 
existing code.
I don't think the problem is complex at all. What I suggested is of 
software engineering nature. The student does not need to know about 
Groebner bases at all. The present code has four easily identifiable 
code sections:


 a) Preprocessing the goals into a normal form ---

 b) from the normal form prepare a question to be asked to a Groebner 
bases engine


 c) Groebner Bases engine accepts a question (radical ideal membership) 
and in success returns a certificate for this membership. The 
certificate has a very easy format


 d) in case of success, replay the certificate to create a proof of the 
goal


What i have suggested is to replace (or give more possibilities) for c), 
if that is at all desirable for efficiency reasons. I suggested this, 
because I suspect that you are trying to solve problems from engineering 
or similar fields, where the problems generated are generally much 
larger than typical verification problems.


Similar to what happened with Sledgehammer, SOS, (and Z3?), one could 
use an online service for such problems (again if there is need at all) 
or create one if wanted. Beware however, that the answers to requests 
can be exponentially larger than requests :)


Hope this helps,
Amine.

--

  _
   _ooOoo_
  o888o
  88 . 88
  (| -_- |)
  O\  =  /O
   /`---'\
 .'  \\| |//  `.
/  \\|||  :  |||//  \
   /  _| -:- |_  \
   |   | \\\  -  /'| |   |
   | \_|  `\`---'//  |_/ |
   \  .-\__ `-. -'__/-.  /
 ___`. .'  /--.--\  `. .'___
  . '  `.___\_|_/___.' _ \.
 | | :  `- \`. ;`. _/; .'/ /  .' ; |
 \  \ `-.   \_\_`. _.'_/_/  -' _.' /
   ===`-.`___`-.__\ \___  /__.-'_.'_.-'
   `=--=-'hjw

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Amine Chaieb]

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.

Am 11/08/2011 14:43, schrieb Florian Haftmann:

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 carried together some
arguments.  I'm pretty sure there are further ones either pro or
contra, for which this mailing list seems a good place to collect
them.

Why (I think) the current state concerning sets is a bad idea: *
There are two worlds (sets and predicates) which are logically the
same but syntactically different.  Although the logic construction
suggests that you can switch easily between both, in practice you
can't – just do something like (unfold mem_def) and your proof will
be a mess since you have switched to the »wrong world«. * Similarly,
there is a vast proof search space for automated tools which is not
worth exploring since it leads to the »wrong world«, making vain
proof attempts lasting longer instead just failing. * The logical
identification of sets and predicates prevents some reasonable simp
rules on predicates: e.g. you cannot have (A |inf| B) x = A x  B x
because then expressions like »set xs |inter| set ys« behave
strangely if the are eta-expanded (e.g. due to induction). * The
missing abstraction for sets prevents straightforward code generation
for them (for the moment, the most pressing, but not the only
issue).

What is your opinion?

In a further e-mail I give some estimations I gained through some
experiments to figure out how feasible a re-introduction would be in
practice.

Btw. the history of the set-elimination can be found here:
http://isabelle.in.tum.de/repos/isabelle/shortlog/26839

Cheers, Florian




___ isabelle-dev mailing
list isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Clash of specifications

[Amine Chaieb]

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 command theory.
 

 I guess that you have a theory which introduces a type sign.  When you
 ensure that this theory has Plain as ancestor, the problem should
 disappear; if not, I think I'll have a look at the offending theories.

 Hope this helps,
   Florian

   

[isabelle-dev] Pending sort hypotheses

[Amine Chaieb]

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 hypotheses to prevent
 proofs like this:
 class impossible =
   assumes impossible: EX x. x ~= x

 lemma False: False
 proof -
   obtain x :: 'a::impossible where x ~= x
 using impossible ..
   then show False by simp
 qed
   

I have nothing against proofs like this one, but I agree that it is a
matter of taste. I would not like to dive into a discussion if this good
or bad :) :)

Amine.

[isabelle-dev] {..n} and {..n}

[Amine Chaieb]

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
 {..n} by the backdoor.
 
 I am tempted to get rid of this and related notations and restrict to
 the canonical SUM k=a..b. t.
 
 Would anybody miss the k=n variant?
 Potential problem: for other types, eg int, k=i cannot be replaced by
 some k=a..i. But SUM k=i, UN k=i over int (let alone real) seem
 unusual.
 
 Feelings?
 
 Tobias
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Repository OK?

[Amine Chaieb]

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 changesets with 900 changes to 440 files (+1 heads)
updating to 30244:aea5d7fa7ef5
414 files updated, 0 files merged, 121 files removed, 0 files unresolved
merging with 30024:f36741094f34
0 files updated, 0 files merged, 0 files removed, 0 files unresolved
new changeset 30245:06b2d7f9f64b merges remote changes with local
bash-3.2$ pwd
/Users/ac638/tools/isabelle
bash-3.2$ cd src/HOL
bash-3.2$ isabelle make HOL-Library
Building Pure ...
Finished Pure (0:00:11 elapsed time, 0:00:07 cpu time, factor 0.63)
make: *** No rule to make target `Option.thy', needed by 
`/Users/ac638/.isabelle/heaps//polyml-5.2.1_x86-darwin/HOL'.  Stop.

[isabelle-dev] Repository OK?

[Amine Chaieb]

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 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 changesets with 900 changes to 440 files (+1 heads)
 updating to 30244:aea5d7fa7ef5
 414 files updated, 0 files merged, 121 files removed, 0 files unresolved
 merging with 30024:f36741094f34
 0 files updated, 0 files merged, 0 files removed, 0 files unresolved
 new changeset 30245:06b2d7f9f64b merges remote changes with local
 bash-3.2$ pwd
 /Users/ac638/tools/isabelle
 bash-3.2$ cd src/HOL
 bash-3.2$ isabelle make HOL-Library
 Building Pure ...
 Finished Pure (0:00:11 elapsed time, 0:00:07 cpu time, factor 0.63)
 make: *** No rule to make target `Option.thy', needed by 
 `/Users/ac638/.isabelle/heaps//polyml-5.2.1_x86-darwin/HOL'.  Stop.
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] [Fwd: Isabelle, refute and nitpick]

[Amine Chaieb]

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??? But who is roaring ahead?


 Amine.

 Tobias Nipkow wrote:

 
 :-)

 Tobias

  Original-Nachricht 
 Betreff: Isabelle, refute and nitpick
 Datum: Tue, 3 Mar 2009 02:32:44 -0500 (EST)
 Von: geoff at cs.miami.edu
 Antwort an: geoff at cs.miami.edu
 An: Tobias Nipkow Tobias.Nipkow at informatik.tu-muenchen.de,  Jasmin
 Blanchette jasmin.blanchette at gmail.com

 Hi Tobias, Jasmin,

 Just a short note to let you know that the automatic Isabelle-refute system
 has been very useful in the TPTP world. It has found countermodels that
 have
 revealed several bugs in problem encodings, and also pointed to deeper
 theoretical issues in Chris Benzmuller's encoding of modal logic into
 higher-order logic. I'm looking forward to Isabelle 2009, so we can create
 a version of the system with strategy scheduling of refute and nitpick.

 Cheers,

 Geoff

 P.S. Soon I'll be send you all the results of our testing of Isabelle on
 the new higher-order TPTP. It looks like it's the second best system! I
 hope you will enter it into the new THF division of CASC at CADE-22.

 Geoff Sutcliffe   http://www.cs.miami.edu/~geoff
 Department of Computer ScienceEmail : geoff at cs.miami.edu
 University of Miami   Phone : +1 305 2842158/2842268
 (Director of Undergraduate Studies)   FAX   : +1 305 2842264
 - My cat is not a float. Every string should learn to swim. --
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
   
   

[isabelle-dev] Typerep again

[Amine Chaieb]

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 these new problems I 
must consult the Thesaurus for a better word (I might choose flimsy 
since it stand for both fragile, and unconvincing/implausible).

Amine.

Florian Haftmann wrote:
 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 Complex_Main? Are you serious? Implementing this policy would
 require changes to a LOT of theories: HOLCF, every subdirectory of
 src/HOL, all the AFP contributions, all user-created Isabelle theories
 in the entire world that import Main, etc.
 
 The any here is supposed to range over all theories in the HOL image;
  indeed Complex_Main need not be taken too serious since the fragile
 tool bootstraps are already finished with Main.
 
 Cheers,
   Florian
 
 
 
 
 
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Typerep again

[Amine Chaieb]

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 for constant 
Typerep.typerep_class.typerep
*** At command theory.


Since an etiologic solution does not seem to exist, can you give a way 
to come around these situations temporarily. They just cost time and 
nerves...

I would be happy with the ugliest hack.

Amine.

[isabelle-dev] Typerep again

[Amine Chaieb]

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 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 for constant
 Typerep.typerep_class.typerep
 *** At command theory.
 
 is it possible to make both Permutations and Misc to inherit from Main?
 
   Florian
 

[isabelle-dev] Typerep again

[Amine Chaieb]

Do you mean thy_deps? It's not working on my machine.
Can you do

cvs -d 
haftmann at cvsbroy.informatik.tu-muenchen.de:/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 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 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 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 for constant
 Typerep.typerep_class.typerep
 *** At command theory.
 is it possible to make both Permutations and Misc to inherit from Main?

 Florian

 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
 

[isabelle-dev] Typerep again

[Amine Chaieb]

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 at cvsbroy.informatik.tu-muenchen.de:/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 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 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 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 for constant
 Typerep.typerep_class.typerep
 *** At command theory.
 is it possible to make both Permutations and Misc to inherit from Main?

 Florian

 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

 
 
 
 
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-- next part --
A non-text attachment was scrubbed...
Name: Misc
Type: video/x-flv
Size: 914 bytes
Desc: not available
URL: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/7edfb161/attachment.flv
-- next part --
A non-text attachment was scrubbed...
Name: permutations
Type: video/x-flv
Size: 715 bytes
Desc: not available
URL: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/7edfb161/attachment-0001.flv

[isabelle-dev] Typerep again

[Amine Chaieb]

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:
 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 at cvsbroy.informatik.tu-muenchen.de:/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 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 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 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 for constant
 Typerep.typerep_class.typerep
 *** At command theory.
 is it possible to make both Permutations and Misc to inherit from
 Main?

 Florian

 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



 

 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

 

 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
 
 
 
 
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-- next part --
A non-text attachment was scrubbed...
Name: permutations
Type: video/x-flv
Size: 7248 bytes
Desc: not available
URL: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/9148bfd9/attachment-0002.flv
-- next part --
A non-text attachment was scrubbed...
Name: Misc
Type: video/x-flv
Size: 13179 bytes
Desc: not available
URL: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090209/9148bfd9/attachment-0003.flv

[isabelle-dev] Typerep again

[Amine Chaieb]

  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 Plain, Main and Complex_Main.

Do you mean that in the imports section of any theory one of the words 
Plain, Main or complex Main should appear?

Can you give a precise description of what happens and how we should 
circumvent these problems. I completely disagree with a rule that 
obliges to import from a higher theory than necessary. This is just not 
natural. If this mechanism is so important in HOL then it should be 
either clarified to the developers and users or it should be done in a 
manner not be noticed in a negative way.

Amine

[isabelle-dev] Factorials and binomial coefficients

[Amine Chaieb]

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 merging 
these developments.

Best wishes,
Amine.

Florian Haftmann wrote:
 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
 factorials) which generalize factorials (I have also relation theorems
 to fact) and the generalized binomial coefficient.

 Since Fact.thy is needed for building HOL but Library/Binomial is not,
 my question is whether we should unify these two developments or should
 I add my formalization into Libray or ex? Any comments are welcome!
 
 I would encourage to go the way through:  replace Binomial/Fact by your
 development.
 
 In the examples you sent with your rewrite orientation problem there is
 still a separate Fact.thy (which a few dozens of lines).  I would
 strongly suggest to integrate this into your Binomal.thy
 
 Thanks a lot,
   Florian
 

[isabelle-dev] problems with the class-package

[Amine Chaieb]

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
looked like:

  embed_nat_even: !!x. even (embed_nat x) = even x and


but now Isabelle complains about types (apparently inside even_odd we
are not allowed to use even with a different type, even if we have
already provided an instance).


Anyway, when we introduce a silly definition or abbreviation even_nat
which is even over nat, we get the following strange error that some
tactic in class-package failed. Any idea what this is? In the best case
of course someone could tell how to fix it, so we can at least process
the theory...

Here is the error:


*** Tactic failed.
*** The error(s) above occurred for the goal statement:
*** (!!x::nat. image_nat (embed_nat_class.embed_nat x))
*** == (!!x::'a::type.
*** image_nat x == embed_nat_class.embed_nat (return_nat x) = x)
*** == (!!(x::nat) y::nat.
*** (embed_nat_class.embed_nat x = embed_nat_class.embed_nat
y) =
*** (x = y))
*** == (!!(x::nat) y::nat.
*** (embed_nat_class.embed_nat x
***   embed_nat_class.embed_nat y) =
*** (x  y))
*** == (!!(x::nat) y::nat.
*** (embed_nat_class.embed_nat x
***  = embed_nat_class.embed_nat y) =
*** (x = y))
*** == (!!(x::nat) y::nat.
*** (embed_nat_class.embed_nat x dvd
***  embed_nat_class.embed_nat y) =
*** (x dvd y))
*** == (!!x::nat.
*** even (embed_nat_class.embed_nat x) =
even_nat x)
*** == (0::'a::type) = embed_nat_class.embed_nat 0
*** == (1::'a::type) =
embed_nat_class.embed_nat 1
*** == (2::'a::type) =
*** embed_nat_class.embed_nat 2
*** == (3::'a::type) =
***   embed_nat_class.embed_nat 3
***   == (!!(x::nat) y::nat.
***   embed_nat_class.embed_nat x + embed_nat_class.embed_nat y =
***   embed_nat_class.embed_nat (x + y))
***   == (!!(x::nat) y::nat.
***   y = x
***   == embed_nat_class.embed_nat x -
***   embed_nat_class.embed_nat y =
***   embed_nat_class.embed_nat (x - y))
***   == (!!(x::nat) y::nat.
***   embed_nat_class.embed_nat x *
***   embed_nat_class.embed_nat y =
***   embed_nat_class.embed_nat (x * y))
***   == (!!(x::nat) n::nat.
***   embed_nat_class.embed_nat x ^ n =
***   embed_nat_class.embed_nat (x ^ n))
***   == (!!(x::nat) y::nat.
***   embed_nat_class.embed_nat x div
***   embed_nat_class.embed_nat y =
***   embed_nat_class.embed_nat (x div y))
***   == (!!(x::nat) y::nat.
***   embed_nat_class.embed_nat x mod
***   embed_nat_class.embed_nat y =
***   embed_nat_class.embed_nat (x mod y))
***   == ??.Strange.embed_nat op * op div op
mod op -
***(1::'a::type) op = op  op +
(0::'a::type)
***number_of even op ^
embed_nat_class.embed_nat
***return_nat image_nat
*** At command class.


Best wishes,

Amine.



-- next part --
An embedded and charset-unspecified text was scrubbed...
Name: Strange.thy
URL: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090123/11939013/attachment.ksh

[isabelle-dev] problems with the class-package

[Amine Chaieb]

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 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,
   Florian

   

[isabelle-dev] typrep?

[Amine Chaieb]

This behaviour is even more strange than I thought.


I am trying to merge my theory with Complex_Main . The latter looks like:


theory Complex_Main

imports
  Main
  Real
  Fundamental_Theorem_Algebra
  Log
  Ln
  Taylor
  Integration
  FrechetDeriv
begin

end


Now when I merge my theory 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
 Complex_Main.typerep_real_inst.typerep_real_def and
 FPS.typerep_real_inst.typerep_real_def for constant
 Typerep.typerep_class.typerep

 *** At command theory.



 What does it mean? I do not mention typerep, nor typerep_real, no real
 at all. I guess it has something to do with the typedef package, but
 what is it?


 Any hint is welcome.

 Best wishes,

 Amine.

 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
   

[isabelle-dev] Polynomial theory

[Amine Chaieb]

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 with the list representation, but every thing is
outside the logic as soon as you want to reason about the different
variables etc...

 If you want something more general (maybe you want to reason about
 polynomials with an arbitrary number of variables) then maybe a monoid
 ring (http://en.wikipedia.org/wiki/Monoid_ring) would be a good
 generalization to use. This could be a type constructor with two
 parameters, one for the ring of coefficients, and one for the monoid
 of exponents. Then ('a, nat) monoid_ring would represent univariate
 polynomials, and ('a, 'b multiset) monoid_ring could represent
 multivariate polynomials, where 'b is a finite type indexing all of
 the indeterminate variables. I'm not sure why a Vectors theory would
 be necessary.

Not necessary, but they can be useful. One way to formalize multivariate
polynomials is to consider the (finite) vectors nat^'n, these formalize
the monomials (the elements of the vector are the powers of each
variable), a formalization of 'a['n] is then the set of all functions
p:: nat^'n = 'a such that ALL x. (ALL i: dimension of 'n. x_i  N) --
p x = 0 for some N. The function p associates with each monomial a
coefficient.
Immediately we obtain 'a poly isomorphic to 'a[1].

 I have thought about formal power series as well, and I had noticed
 that many proofs about addition and multiplication are the same as
 with polynomials. I think it would be simple to define one in terms of
 the other. If you don't do it already, we would want to define 'a fps
 using a typedef, rather than as a type synonym. Then we could define
 addition, multiplication, etc. on 'a fps, and give instances for
 group, ring, and idom classes. 

All that and much more is done.

 Then we could define 'a poly as the subset of finite elements of 'a
 fps. We just need to prove that operations like addition and
 multiplication preserve the finite property, and we could inherit
 all of the other properties of those operations from 'a fps.
I am interested in what you say here. Do you think it is possible to
define (as you say above) without  construction a new type? or using
classes?

Best wishes,
Amine.

[isabelle-dev] Polynomial theory

[Amine Chaieb]

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 * Rep_poly q)

 Then the transfer of theorems from fps (like, say, associativity of
 multiplication) would not be automatic, but they would be really easy
 proofs.

OK, that sound reasonable. I was thinking of that + a very simple tactic
to transfer the important theorems after a basic set of theorems about
conserving finiteness.  I will try that in my theory as soon as I can.

I was hoping that there is a way not to introduce a new type, and that
for once HOL behaves as nice as set-theory. But I should give up the
latter anyway...

Amine.

[isabelle-dev] instantiation

[Amine Chaieb]

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!

best wishes,
Amine.

[isabelle-dev] NEWS

[Amine Chaieb]

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 argument, generates
 corresponding code in background and inserts name of the corresponding
 resulting ML value/function/datatype constructor binding in place.  All
 occurences of 'code' with a single ML block are generated simultaneously.
 Provides a generic and safe interface for instrumentalizing code
 generation.  See HOL/ex/Code_Antiq for a toy example, or
 HOL/Complex/ex/ReflectedFerrack  for a more ambitious application.  In
 future you ought refrain from  ad-hoc compiling generated SML code on
 the ML toplevel.
 Note that (for technical reasons) 'code' cannot refer to constants for
 which user-defined serializations are set.  Refer to the corresponding
 ML counterpart directly in that cases.
 
   Florian
 
 
 
 
 
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] classes

[Amine Chaieb]

 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 = ring_1 + recpower
subclass (in recpower_ring_1) recpower_ring by unfold_locales
subclass (in recpower_ring_1) recpower_ring by unfold_locales
class recpower_comm_semiring_1 = recpower + comm_semiring_1
class recpower_comm_ring_1 = recpower + comm_ring_1
subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by 
unfold_locales
class recpower_idom = recpower + idom
subclass (in recpower_idom) recpower_comm_ring_1 by unfold_locales
class idom0 = idom + ring_char_0
class recpower_idom0 = recpower + idom0
subclass (in recpower_idom0) recpower_idom by unfold_locales
subclass (in idom0) comm_ring_1 by unfold_locales


 And what exactly does merging mean? Do you just add a new class which 
 inherits from both existing classes? Then it would be a conservative 
 extension...?

Yes, see above.

 
 When you changed things locally, what effects did it have on other theories?
 

I just added these at the beginning of my theory, so I have no idea what 
would happen if they were in HOL. I also did not try to do more than 
needed, just what I needed to make Polynomials local.

 I think I like this future, but I still agree with Makarius: Unless 
 there is something severely broken in the current state of affairs, we 
 should really be disciplined and wait for the release first.
 

The release Idea (as far as I understood Makarius) is that the system 
should freeze for a couple of weeks while we are *using* it and report 
our experience. That's all I did, just report (while bemoaning, I must 
admit). I leave it to others to decide if this is important to change 
now of not. I myself think it quite manageable to fix in a reasonable 
time but I also fully understand that this release-preparation time is 
critical.

Regardless of release, there are several subtle issues with classes 
which need to be fixed.

 And in fact your proposal is more of the visionary kind than of the 
 fixes a pressing problem kind, isn't it?

It is not really a pressing problem. The other problem (parsing/type 
inference) I reported locally on the TUM list, is in my opinion pressing 
-- Thanks for Makarius who fixed it.

Amine.

[isabelle-dev] class recpower and other classes...

[Amine Chaieb]

  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 at least. I want(ed) to have merge point for the 
so many nice-looking classes, so that the interesting theorem can be 
proved inside the locale and not only inside axclasses.

Amine.

[isabelle-dev] quickcheck on type real

[Amine Chaieb]

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 his code generator, 
but trying the first lemma with quickcheck, I get the error

*** Unable to generate code for term:
*** of_int a / of_int b
*** required by:
*** Abstract_Rat.INum, Executable_Real.Real, HOL.inverse_class.divide 
def1, Top
*** At command quickcheck.

Maybe this is good motivation to get these theories work for Stefan's 
Code generator and quickcheck.

Amine.


Brian Huffman wrote:
 Hello all,
 
 I would like to report some bugs I found when using quickcheck on lemmas 
 involving division on reals. When auto_quickcheck is enabled (which it is by 
 default) these bugs cause the lemma command to fail, preventing me from 
 even attempting a proof.
 
 The first bug is that sometimes quickcheck fails with a DIVZERO exception. 
 This could probably be fixed by changing rat.ML to return zero when dividing 
 by zero.
 
 ML {* Codegen.auto_quickcheck := false; *}
 
 lemma (a::real) = 1 / (1 / a)
   quickcheck
 
 *** DIVZERO
 *** At command quickcheck.
 
 The same error is also appears with other, more useful lemmas like this one:
 
 lemma real_divide_cancel_lemma:
   (b = 0  == a = 0)  == (a / b::real) * (b / c) = a / c
 
 The other bug is a false counterexample; I have no idea what causes it:
 
 lemma inverse (a::real) = (1 / a)
   quickcheck
 
 Test data size: 0
 
 Test data size: 1
 
 
 Counterexample found:
 a = -1
 
 I am using the current CVS version of Isabelle, by the way.
 
 - Brian
 
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev