[isabelle-dev] some results about "lex"

2017-08-24 Thread 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

Re: [isabelle-dev] Towards the Isabelle2017 release

2017-08-24 Thread 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

Re: [isabelle-dev] Towards the Isabelle2017 release

2017-08-24 Thread 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

Re: [isabelle-dev] Towards the Isabelle2017 release

2017-08-24 Thread 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

Re: [isabelle-dev] Towards the Isabelle2017 release

2017-08-24 Thread Viorel Preoteasa
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

Re: [isabelle-dev] Towards the Isabelle2017 release

2017-08-24 Thread Florian Haftmann
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.

Re: [isabelle-dev] Towards the Isabelle2017 release

2017-08-24 Thread 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

Re: [isabelle-dev] Towards the Isabelle2017 release

2017-08-24 Thread 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