[isabelle-dev] some results about "lex"

[Christian Sternagel]

Dear list,

maybe the following results about "lex" are worthwhile to add to the
library?

lemma lex_append_right:
  "(xs, ys) ∈ lex r ⟹ length vs = length us ⟹ (xs @ us, ys @ vs) ∈ lex r"
  by (force simp: lex_def lexn_conv)

lemma lex_append_left:
  "(ys, zs) ∈ lex r ⟹ (xs @ ys, xs @ zs) ∈ lex r"
  by (induct xs) auto

lemma lex_take_index:
  assumes "(xs, ys) ∈ lex r"
  obtains i where "i < length xs" and "i < length ys" and "take i xs =
take i ys"
and "(xs ! i, ys ! i) ∈ r"
proof -
  obtain n us x xs' y ys' where "(xs, ys) ∈ lexn r n" and "length xs =
n" and "length ys = n"
and "xs = us @ x # xs'" and "ys = us @ y # ys'" and "(x, y) ∈ r"
using assms by (fastforce simp: lex_def lexn_conv)
  then show ?thesis by (intro that [of "length us"]) auto
qed

cheers

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

For the final record:

> \phi is the result of a simple typo accident
see http://isabelle.in.tum.de/repos/isabelle/rev/ba94aeb02fbc

> Concerning \mu and \nu, I am currently investigating whether an import
> swap could re-establish the situation known from Isabelle2016-1

see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Manuel Eberl]

On 2017-08-24 17:34, Florian Haftmann wrote:
> I would still appreciate if someone would take the comment »Deviates
> from the definition given in the library in number theory« as a starting
> point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.

Oh actually I fixed that a few months ago. I even wrote on the mailing
list back then, I think. Those definitions should now be equivalent.

I didn't know there was a totient function in HOL-Algebra, otherwise I
would have removed the duplicate back then.

(By the way, I have lots of additional material on the totient function
and related functions that will come to an AFP near you very soon)

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Manuel Eberl]

Purely out of interest: Does this also hold for filters?

Manuel


On 2017-08-24 20:54, Viorel Preoteasa wrote:
> I have now a file with the new class, and all necessary proofs
> (both distributivity equalities, bool, set, fun interpretations,
> proofs of the old distributivity properties).
> 
> I have also the proof that complete linear order is subclass of
> the new complete distributive lattice class.
> 
> Are there any other subclasses of the current complete distributive
> lattice class? This would be something that could cause problems.
> 
> Otherwise, the existing complete distrib lattice is subclass
> of the one that I implemented, so it should not cause any problems.
> All existing results in the current class can be reused without
> modification.
> 
> My theory works now in Isabelle 2016-1, but I can try it in
> Isabelle2017-RC0 also.
> 
> I can try to integrate it, but I don't know how to test it
> to see if there are any problems with something else.
> 
> For reference, I attach the theory file with the new
> class of complete distributive lattice.
> 
> Best regards,
> 
> Viorel
> 
> 
> 
> On 8/24/2017 6:40 PM, Florian Haftmann wrote:
>> As far as I remember, I introduced the complete_distrib_lattice class
>> after realizing the a complete lattice whose binary operations are
>> distributive is not necessarily a distributive complete lattice.  Hence
>> the specification of that type class has been contrieved without
>> consulting literature.
>>
>> Hence that change should be fine if someone is willing to undertake it
>> before the RC stabilization phase.
>>
>> Cheers,
>> Florian
>>
>> Am 24.08.2017 um 00:42 schrieb Lawrence Paulson:
>>> Sounds good to me. Can anybody think of an objection?
>>> Larry
>>>
 On 23 Aug 2017, at 15:17, Viorel Preoteasa > wrote:

 Hello,

 I am not sure if this is the right place to post this message, but
 it is
 related to  the upcoming release as I am prosing adding something
 to the Isabelle library.

 While working with complete distributive lattices, I noticed that
 the Isabelle class complete_distrib_lattice is weaker compared to
 what it seems to be regarded as a complete distributive lattice.

 As I needed the more general concept, I have developed it,
 and if Isabelle community finds it useful to be in the library,
 then I could provide the proofs or integrate it myself in the
 Complete_Lattice.thy

 The only axiom needed for complete distributive lattices is:

 Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈
 Y)})"

 and from this, the equality and its dual can be proved, as well as
 the existing axioms of complete_distrib_lattice and the instantiation
 to bool, set and fun.

 Best regards,

 Viorel


 On 2017-08-21 21:24, Makarius wrote:
> Dear Isabelle contributors,
>
> we are now definitely heading towards the Isabelle2017 release.
>
> The first official release candidate Isabelle2017-RC1 is
> anticipated for
> 2/3-Sep-2017, that is a bit less than 2 weeks from now.
>
> That is also the deadline for any significant additions.
>
>
> I have already updated the important files NEWS, CONTRIBUTORS,
> ANNOUNCE
> in Isabelle/5c0a3f63057d, but it seems that many potential entries are
> still missing.
>
> Please provide entries in NEWS and CONTRIBUTORS for all relevant
> things
> you have done since the last release.
>
>
> 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-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 mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

Hi Rene,

> - In the NEWS I read about freeing short constant names like the
>   “Renamed ii to imaginary_unit in order to free up ii as a variable”.
>   I definitely support this kind of change, but at the same time found
>   quite the opposite in HOL-Algebra:
>   If one imports HOL-Algebra.Multiplicative_Group (which we actually do
>   via some transitive import), then \mu (LFP), \nu (GFP) and 
>   \phi (Euler’s totient function) become constants.
>   This was a bit annoying.

thanks for pointing that out.

\phi is the result of a simple typo accident (cf.
http://isabelle.in.tum.de/repos/testboard/rev/6c818fc0c817).

I would still appreciate if someone would take the comment »Deviates
from the definition given in the library in number theory« as a starting
point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.

Concerning \mu and \nu, I am currently investigating whether an import
swap could re-establish the situation known from Isabelle2016-1
(http://isabelle.in.tum.de/repos/testboard/rev/0ad153ee9ece).

> - There have been some changes w.r.t. code-generation which now lead
>   to runtime exception in the generated code. For instance, now
>   I get code like
>   “f x = Code.abort …” 
>   whereas in 2016-1 there was a proper code like
>   “f x = some ordinary right-hand side” 
>   We did not yet isolate the problem and will report later.

OK, I will dig into this after you have isolated it.  Might be well that
this only occurs on certain theory merges.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Thiemann, Rene]

Dear all,

let me share my opinions after porting IsaFoR to yesterdays development version:

- In total the transition from our 2016-1 source went quite smooth 
  (~ 14 hours for whole of IsaFoR)

- Most changes have been caused by integrating session-qualified theory imports.
  This will also require a reform of the splitting of sessions, which previously
  was structured towards a fast build-process, but now should be structured 
more 
  towards logical structure (which is currently reflected in the 
directory-structure).

- In the NEWS I read about freeing short constant names like the
  “Renamed ii to imaginary_unit in order to free up ii as a variable”.
  I definitely support this kind of change, but at the same time found
  quite the opposite in HOL-Algebra:
  If one imports HOL-Algebra.Multiplicative_Group (which we actually do
  via some transitive import), then \mu (LFP), \nu (GFP) and 
  \phi (Euler’s totient function) become constants.
  This was a bit annoying.

- There have been some changes w.r.t. code-generation which now lead
  to runtime exception in the generated code. For instance, now
  I get code like
  “f x = Code.abort …” 
  whereas in 2016-1 there was a proper code like
  “f x = some ordinary right-hand side” 
  We did not yet isolate the problem and will report later.

Cheers,
René  


> Am 21.08.2017 um 20:24 schrieb Makarius :
> 
> Dear Isabelle contributors,
> 
> we are now definitely heading towards the Isabelle2017 release.
> 
> The first official release candidate Isabelle2017-RC1 is anticipated for
> 2/3-Sep-2017, that is a bit less than 2 weeks from now.
> 
> That is also the deadline for any significant additions.
> 
> 
> I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
> in Isabelle/5c0a3f63057d, but it seems that many potential entries are
> still missing.
> 
> Please provide entries in NEWS and CONTRIBUTORS for all relevant things
> you have done since the last release.
> 
> 
>   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-dev