Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] coprime predicate [was: 2 new commits to Code

Email Gateway (Aug 22 2022 at 16:27):

From: Akihisa Yamada <akihisa.yamada@uibk.ac.at>
Dear Florian (and the list),

• The locales in HOL-Algebra are really generic in the sense that they
  have an explicit carrier and hence are not tied to the HOL type system.

Actually I've tried to make classes based on carrier-aware locales. (One
goal was to reuse algorithms for our matrices which form a ring only if
carrier conditions are met, and in principle, one can merge HOL-Algebra
locales and Groups.thy.)

The only obstacle here was that rewrites on prop doesn't work (as I
would expect):

locale magma =
fixes f (infixl "❙*" 70) and member
assumes closed: "⋀a b. member a ⟹ member b ⟹ member (a ❙* b)"

sublocale times ⊆ mult: magma where member = "λx. True" and f = "op *"
rewrites xx: "⋀P. (True ⟹ PROP P) ≡ P"
by (unfold_locales, simp_all)

thm mult.closed (* "True ⟹ True ⟹ True", why not "True"? *)
thm mult.closed[unfold xx] (* True *)

AFAIU now, the problem is that "irreducible" has a too specific type.

Yes, and I think (comm_)monoid_mult is the fitting place in the current
classes (same for coprime, IMO).

What I don't understand is the matter of dvd and commutativity; IMHO in
an algebraic structure without commutativity you have to distinguish
left and right divisors, of which there is currently no trace.

I don't plan to do non-commutative factorization, so this is just
observation not request: The current definition of "dvd" is right and
HOL-Algebra's "factors" is left. Fundamentally they could be defined two
sided and current definitions could be lemmas in commutative settings.

Cheers,
Akihisa

Is it OK to move this discussion to the Isabelle mailing list?
Particulary the matter of "irreducible" is beyond my knowledge.

Cheers,
Florian

Email Gateway (Aug 22 2022 at 16:27):

From: Akihisa Yamada <akihisa.yamada@uibk.ac.at>

The current definition of "dvd" is right and HOL-Algebra's "factors" is left.
Sorry for confusion, both are "right".

Best regards,
Akihisa

Email Gateway (Aug 22 2022 at 16:28):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Akihisa,

I don't think you can reuse those locales directly.

But you can reuse ambitious proof results using ephemeral
interpretation, roughly:

context some_class
begin

interpretation some_local_with_carrier where …
<proof> -- ‹yields a lot of facts including
ambitious_result_formulated_for_locale>, although not in nice shape›

lemma <ambitious_result_formulated_for_class>
<proof using ambitious_result_formulated_for_locale>

end

Cheers,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 16:30):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Good question. Experimentally I found out that the less ambitious
rewrite ‹(True ⟹ True) ≡ Trueprop True› works as expected.

I think that question can only be answered by experts on either the
module system or the simplifier or even both.

Personally, I would not recommend a persistent direct interpretation
between locales that are structurally that different; ephemeral
interpretation is less implicit and more verbose but gives you much more
control which results are actually propagated without flooding the fact
name space with practically unusable theorems.

Cheers,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 16:33):

From: Akihisa Yamada <akihisa.yamada@uibk.ac.at>
Dear Florian,

On 2017/11/30 17:24, Florian Haftmann wrote:

Dear Akihisa,

Actually I've tried to make classes based on carrier-aware locales. (One
goal was to reuse algorithms for our matrices which form a ring only if
carrier conditions are met, and in principle, one can merge HOL-Algebra
locales and Groups.thy.)

The only obstacle here was that rewrites on prop doesn't work (as I
would expect):

locale magma =
  fixes f (infixl "❙*" 70) and member
  assumes closed: "⋀a b. member a ⟹ member b ⟹ member (a ❙* b)"

sublocale times ⊆ mult: magma where member = "λx. True" and f = "op *"
  rewrites xx: "⋀P. (True ⟹ PROP P) ≡ P"
  by (unfold_locales, simp_all)

thm mult.closed (* "True ⟹ True ⟹ True", why not "True"? *)
thm mult.closed[unfold xx] (* True *)

I don't think you can reuse those locales directly.

But you can reuse ambitious proof results using ephemeral
interpretation, roughly:

context some_class
begin

interpretation some_local_with_carrier where …
<proof> -- ‹yields a lot of facts including
ambitious_result_formulated_for_locale>, although not in nice shape›

lemma <ambitious_result_formulated_for_class>
<proof using ambitious_result_formulated_for_locale>

end

thank you for the tip, but why <<rewrites "⋀P. (True ⟹ PROP P) ≡ P">>
does/should not work?

Cheers,
Akihisa

Cheers,
Florian

Last updated: Nov 21 2024 at 12:39 UTC