Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Hi Rene, >> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and >> thus very hardly different from syntactic classes, so there is no loss >> of generality here. > > I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 > have > the three essential lemmas: > > gcd_dvd1, gcd_dvd2, and gcd_greatest. indeed, but these are exactly the assumptions of the type class. > And since you want to include the patch anyway, why not include at least the > instance now? It sits on top of a couple of other patches definitely not suitable for inclusion by now. 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] Isabelle2016-RC0: potential changes
Dear all, > > I have already some post-release patches in the pipeline which would add > this instance anyway. So, there is no demand for action here at the moment. > > Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and > thus very hardly different from syntactic classes, so there is no loss > of generality here. I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 have the three essential lemmas: gcd_dvd1, gcd_dvd2, and gcd_greatest. And since you want to include the patch anyway, why not include at least the instance now? Cheers, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Hi all, > This is probably a question for Florian. I introduced Euclidean rings to > allow a more systematic derivation of (constructive) GCDs about two > years ago or so. > > Since then, Florian cleaned this up and improved it a lot, but from what > I gathered, there is much to be done yet. I should probably have taken > care of this already, but I never quite found the time; I shall attempt > to do that this year. > > As for the release, perhaps Florian can comment on whether anything > speaks against moving this instance into the Polynomial theory. I have already some post-release patches in the pipeline which would add this instance anyway. So, there is no demand for action here at the moment. Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and thus very hardly different from syntactic classes, so there is no loss of generality here. Cheers, Florian > > > Cheers, > > Manuel > > > On 12/01/16 09:21, Thiemann, Rene wrote: >> Hi Manuel, >> >>> I added the efficient code equations for fact and binomial, and >>> similar ones for pochhammer and gbinomial. >>> >>> I also adapted everything from Square_Free_Factorization and >>> Missing_Polynomial that seemed to be of general interest to me >>> (especially the generalisation of the type of pderiv). >> >> thanks a lot; in the meantime, I deleted this material from the >> AFP-entries. >> >>> >>> I also noticed the ring_gcd instance for polynomials. Finalising the >>> changes to the GCD class hierarchy and updating the AFP entries that >>> rely on half-finished versions of this change (such as Echelon_Form) >>> is something that I should probably take care of soon, but definitely >>> not before the 2016 release – hopefully before the 2017 one. >> >> The absence of the ring_gcd instance for polynomials is strange from >> my perspective: In Isabelle 2015 we had >> >>instantiation poly :: (field) gcd >> >> where the gcd-class contained the important properties of a gcd. >> >> In Isabelle 2016-RC0 there also is >> >>instantiation poly :: (field) gcd >> >> but now the gcd-class is purely syntactic. Here, to get the same >> properties of a gcd (and more), the corresponding instance would be >> >>instantiation poly :: (field) semiring_gcd (or ring_gcd) >> >> So why should the small proof below be not integrated for the 2016 >> release? Otherwise, there >> is no class-based gcd for polynomials available for 2016, in contrast >> to 2015. >> >> instance poly :: (field) ring_gcd >> proof >>fix a b :: "'a poly" >>show "normalize (gcd a b) = gcd a b" by (simp add: >> normalize_poly_def poly_gcd_monic) >>show "lcm a b = normalize (a * b) div gcd a b" >>proof (cases "a * b = 0") >> case False >> show ?thesis unfolding lcm_poly_def normalize_poly_def >> by (subst div_smult_right, insert False, auto simp: div_smult_left) >> (metis coeff_degree_mult divide_divide_eq_left >> divide_inverse_commute inverse_eq_divide) >>next >> case True >> thus ?thesis by (metis div_0 lcm_poly_def normalize_0) >>qed >> qed auto >> >> >> Cheers, >> René >> -- 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] Isabelle2016-RC0: potential changes
On Thu, 14 Jan 2016, Florian Haftmann wrote: Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and thus very hardly different from syntactic classes, so there is no loss of generality here. I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 have the three essential lemmas: gcd_dvd1, gcd_dvd2, and gcd_greatest. indeed, but these are exactly the assumptions of the type class. And since you want to include the patch anyway, why not include at least the instance now? It sits on top of a couple of other patches definitely not suitable for inclusion by now. Does it mean this thread is closed concerning Isabelle2016? We can probably afford a few more days to stabilize the conclusion of the various "potential changes". (I can't contribute anything myself, because I don't know these parts of the library.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
On Mon, 11 Jan 2016, Manuel Eberl wrote: I also noticed the ring_gcd instance for polynomials. Finalising the changes to the GCD class hierarchy and updating the AFP entries that rely on half-finished versions of this change (such as Echelon_Form) is something that I should probably take care of soon, but definitely not before the 2016 release – hopefully before the 2017 one. Note that 2016 is what could be called an "Isabelle leap-year". With a release near the start, there needs to be a second one near the end. The distance between releases is constant at approx. 8-10 months. At some point we've tried to target exactly 12 months, but that resulted in 25 months, and a commitment to the strict 8-10 months rule afterwards. Interestingly, the Coq guys are trying for years to target 12 months as well, but the 8.5 release is already much longer in the pipeline. (More than 3 years?) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Hi Manuel, > I added the efficient code equations for fact and binomial, and similar ones > for pochhammer and gbinomial. > > I also adapted everything from Square_Free_Factorization and > Missing_Polynomial that seemed to be of general interest to me (especially > the generalisation of the type of pderiv). thanks a lot; in the meantime, I deleted this material from the AFP-entries. > > I also noticed the ring_gcd instance for polynomials. Finalising the changes > to the GCD class hierarchy and updating the AFP entries that rely on > half-finished versions of this change (such as Echelon_Form) is something > that I should probably take care of soon, but definitely not before the 2016 > release – hopefully before the 2017 one. The absence of the ring_gcd instance for polynomials is strange from my perspective: In Isabelle 2015 we had instantiation poly :: (field) gcd where the gcd-class contained the important properties of a gcd. In Isabelle 2016-RC0 there also is instantiation poly :: (field) gcd but now the gcd-class is purely syntactic. Here, to get the same properties of a gcd (and more), the corresponding instance would be instantiation poly :: (field) semiring_gcd (or ring_gcd) So why should the small proof below be not integrated for the 2016 release? Otherwise, there is no class-based gcd for polynomials available for 2016, in contrast to 2015. instance poly :: (field) ring_gcd proof fix a b :: "'a poly" show "normalize (gcd a b) = gcd a b" by (simp add: normalize_poly_def poly_gcd_monic) show "lcm a b = normalize (a * b) div gcd a b" proof (cases "a * b = 0") case False show ?thesis unfolding lcm_poly_def normalize_poly_def by (subst div_smult_right, insert False, auto simp: div_smult_left) (metis coeff_degree_mult divide_divide_eq_left divide_inverse_commute inverse_eq_divide) next case True thus ?thesis by (metis div_0 lcm_poly_def normalize_0) qed qed auto Cheers, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
On Tue, 12 Jan 2016, Manuel Eberl wrote: So why should the small proof below be not integrated for the 2016 release? This is probably a question for Florian. I introduced Euclidean rings to allow a more systematic derivation of (constructive) GCDs about two years ago or so. As for the release, perhaps Florian can comment on whether anything speaks against moving this instance into the Polynomial theory. I can't say anything specific about these parts of the library, but generally I would be glad to see this sorted out for this release. There is approximately all of this week left to add such small things -- and to get AFP into proper shape as well. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle2016-RC0: potential changes
Dear all, there are some changes I would like to add for the upcoming release. It would be nice, if someone can integrate them: - improved code equations for binomial coefficients and certain divmod-algorithms. (cf. http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html) - change type in definition and lemmas about pderiv from real to arbitrary fields, or even more general, cf. lines starting with (* TODO: inform Isabelle developers *) in http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Square_Free_Factorization.html - change type of divides_degree from complex to 'a :: idom, cf beginning of http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_Polynomial.html Moreover, everything of http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_* http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Missing_* can freely be moved from the AFP into the distribution, where I ask the developers to judge which parts belong in the distribution and which are too specific, etc. With best regards, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
I already moved a few small lemmas. I also defined the notion of an algebraic number; as soon as your AFP entry works with the development version of Isabelle again (is that already the case?), I will prove equivalence of my definition in Poly_Deriv.thy to your definition in Algebraic_Numbers and adapt the AFP entry accordingly. (I needed this for Liouville_Numbers) As for the binomial numbers: that looks a bit suboptimal to me. I would have expected something like "listprod [k+1..n] div fact (n - k)" plus an additional check if "2*k >= n", reducing "n choose k" to "n choose (n - k)" if appropriate. (Not sure what code generation makes of "listprod [k+1..n]", a code_unfold rule to compute this efficiently with an accumulator and without constructing the list explicitly might be required. Same for "fact".) Cheers, Manuel On 11/01/16 09:57, Thiemann, Rene wrote: Dear all, there are some changes I would like to add for the upcoming release. It would be nice, if someone can integrate them: - improved code equations for binomial coefficients and certain divmod-algorithms. (cf. http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html) - change type in definition and lemmas about pderiv from real to arbitrary fields, or even more general, cf. lines starting with (* TODO: inform Isabelle developers *) in http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Square_Free_Factorization.html - change type of divides_degree from complex to 'a :: idom, cf beginning of http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_Polynomial.html Moreover, everything of http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_* http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Missing_* can freely be moved from the AFP into the distribution, where I ask the developers to judge which parts belong in the distribution and which are too specific, etc. With best regards, René ___ 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] Isabelle2016-RC0: potential changes
I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of
algebraic number.
Oh, yes, you're right. It's in
https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
.
Its definitely not optimal, and you’re right that one can improve it
by using an inline-version of listprod [k+1..n], but even the version
that is mentioned in Algebraic_Numbers/Improved_Code_Equations.html is
by far better than the current setup, since that just uses the
recursive direct definition of binomial. (I noticed this since I got
timeouts in my experiments with algebraic numbers and one of the
culprits was binomial!)
I suggest this:
function fold_atLeastAtMost_nat where
[simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
(if a > b then acc else fold_atLeastAtMost_nat f (a+1)
b (f a acc))"
by pat_completeness auto
termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto
lemma fold_atLeastAtMost_nat:
assumes "comp_fun_commute f"
shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"
using assms
proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)
case (1 f a b acc)
interpret comp_fun_commute f by fact
show ?case
proof (cases "a > b")
case True
thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto
next
case False
with 1 show ?thesis
by (subst fold_atLeastAtMost_nat.simps)
(auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)
qed
qed
lemma setprod_atLeastAtMost_code:
"setprod f {a..b} = fold_atLeastAtMost_nat (λa acc. f a * acc) a b 1"
proof -
have "comp_fun_commute (λa. op * (f a))"
by unfold_locales (auto simp: o_def mult_ac)
thus ?thesis
by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
qed
lemma fact_altdef': "fact n = of_nat (∏{1..n})"
by (induction n)
(simp_all add: setprod_nat_ivl_Suc' of_nat_mult [symmetric]
One_nat_def [symmetric]
del: of_nat_Suc of_nat_add of_nat_mult One_nat_def)
lemma fact_code [code]:
"fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a ::
semiring_char_0)"
proof -
have "fact n = (of_nat (∏{1..n}) :: 'a)" by (simp add: fact_altdef')
also have "∏{1..n} = ∏{2..n}"
by (intro setprod.mono_neutral_right) auto
also have "… = fold_atLeastAtMost_nat (op *) 2 n 1"
by (simp add: setprod_atLeastAtMost_code)
finally show ?thesis .
qed
lemma binomial_code [code]:
"(n choose k) =
(if k > n then 0
else if 2 * k > n then (n choose (n - k))
else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"
proof -
{
assume "k ≤ n"
hence "{1..n} = {1..n-k} ∪ {n-k+1..n}" by auto
hence "(fact n :: nat) = fact (n-k) * ∏{n-k+1..n}"
by (simp add: setprod.union_disjoint fact_altdef_nat)
}
thus ?thesis by (auto simp: binomial_altdef_nat mult_ac
setprod_atLeastAtMost_code)
qed
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Hi Manuel, > I already moved a few small lemmas. Thanks. > I also defined the notion of an algebraic number; as soon as your AFP entry > works with the development version of Isabelle again (is that already the > case?), Yes, it should work. (At least, on Friday afternoon, it worked) > I will prove equivalence of my definition in Poly_Deriv.thy to your > definition in Algebraic_Numbers and adapt the AFP entry accordingly. I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of algebraic number. > As for the binomial numbers: that looks a bit suboptimal to me. > I would have expected something like "listprod [k+1..n] div fact (n - k)" > plus an additional check if "2*k >= n", reducing "n choose k" to "n choose (n > - k)" if appropriate. > (Not sure what code generation makes of "listprod [k+1..n]", a code_unfold > rule to compute this efficiently with an accumulator and without constructing > the list explicitly might be required. Same for "fact“.) Its definitely not optimal, and you’re right that one can improve it by using an inline-version of listprod [k+1..n], but even the version that is mentioned in Algebraic_Numbers/Improved_Code_Equations.html is by far better than the current setup, since that just uses the recursive direct definition of binomial. (I noticed this since I got timeouts in my experiments with algebraic numbers and one of the culprits was binomial!) Cheers, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
>> I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of >> algebraic number. > Oh, yes, you're right. It's in > https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy > . Ah, I see. Indeed: definitely equivalent. > >> Its definitely not optimal, and you’re right that one can improve it by >> using an inline-version of listprod [k+1..n], but even the version that is >> mentioned in Algebraic_Numbers/Improved_Code_Equations.html is by far better >> than the current setup, since that just uses the recursive direct definition >> of binomial. (I noticed this since I got timeouts in my experiments with >> algebraic numbers and one of the culprits was binomial!) > > I suggest this: > > > function fold_atLeastAtMost_nat where > [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc = > (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a > acc))" > by pat_completeness auto > termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto > ... Looks good from my viewpoint. Best, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
I added the efficient code equations for fact and binomial, and similar ones for pochhammer and gbinomial. I also adapted everything from Square_Free_Factorization and Missing_Polynomial that seemed to be of general interest to me (especially the generalisation of the type of pderiv). I also noticed the ring_gcd instance for polynomials. Finalising the changes to the GCD class hierarchy and updating the AFP entries that rely on half-finished versions of this change (such as Echelon_Form) is something that I should probably take care of soon, but definitely not before the 2016 release – hopefully before the 2017 one. Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
