Email Gateway (Aug 17 2022 at 14:15): Email Gateway (Aug 17 2022 at 14:15):From: Robert Lamar <rlamar@stetson.edu>
I am attempting to develop a theory of rings which features quotients. So far, I have defined rings through axiomatic classes and ideals through a predicate constant. There are several approaches to defining the quotient ring which present themselves, but the next step would be to prove that the quotient is an instance of the ring class. Is there a straightforward way to do this without specifying a particular ideal? My goal, as I imagine it, is to define a type which is parameterized, essentially, by subsets of "UNIV::('a::ring set)" (or more specifically, by subsets which satisfy my is_ideal predicate). Is this possible? Is there a different (better) way to approach this problem?
Thanks,
Robert Lamar
Stetson University
Email Gateway (Aug 17 2022 at 14:15):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Robert,
what you require are dependent types, but these are not supported by
Isabelle. Instead, we propagate the use of "locales" for
formalisations of algebra. See the main trunk of session HOL-Algebra.
Quotient rings have not been formalised in this framework (neither have
quotient fields, which you could get also with type classes), so this
would be a welcome contribution.
Clemens
Email Gateway (Aug 17 2022 at 14:15):From: Brian Huffman <brianh@csee.ogi.edu>
On Sunday 19 March 2006 21:55, Robert Lamar wrote:
I am attempting to develop a theory of rings which features quotients. So
far, I have defined rings through axiomatic classes and ideals through a
predicate constant. There are several approaches to defining the quotient
ring which present themselves, but the next step would be to prove that the
quotient is an instance of the ring class. Is there a straightforward way
to do this without specifying a particular ideal?
One possibility would be to prove some theorems with type_definition
predicates as assumptions. In the Isabelle sources, HOLCF/Pcpodef.thy
contains several examples of this, such as:
theorem typedef_cpo:
fixes Abs :: "'a::cpo => 'b::po"
assumes type: "type_definition Rep Abs A"
and less: "op << == %x y. Rep x << Rep y"
and adm: "adm (%x. x : A)"
shows "OFCLASS('b, cpo_class)"
Assumption "type" basically says that type 'b is defined as a predicate
subtype of 'a, and is isomorphic to the set A::'a set. An instantiation of
the type_definition predicate is what gets axiomatized whenever you use the
"typedef" command; take a look at HOL/Typedef.thy to see how it is defined.
Assumption "less" says that the overloaded "<<" relation on type 'b is
defined in terms of "<<" on type 'a, and finally "adm" places some
restrictions on the set A. The conclusion is exactly the proposition you
would get as a subgoal if you tried to prove that 'b is an instance of class
"cpo".
My goal, as I imagine
it, is to define a type which is parameterized, essentially, by subsets of
"UNIV::('a::ring set)" (or more specifically, by subsets which satisfy my
is_ideal predicate). Is this possible? Is there a different (better) way
to approach this problem?
In your case, you could prove the following theorem:
theorem typedef_ring:
fixes Abs :: "'a::ring => 'b::{zero,plus,times}"
assumes type: "type_definition Rep Abs A"
and zero: "0 == Abs 0"
and plus: "op + == %x y. Abs (Rep x + Rep y)"
and times: "op * == %x y. Abs (Rep x * Rep y)"
and ideal: "is_ideal A"
shows "OFCLASS('b, ring_class)"
You wouldn't get a parameterized type, but you would be able to define new
types one at a time using typedef, and then prove that each new type is in
the ring class using theorem typedef_ring.
Email Gateway (Aug 17 2022 at 14:15):From: Brian Huffman <brianh@csee.ogi.edu>
Hi Robert,
On Tuesday 28 March 2006 14:28, Robert Lamar wrote:
My only question for the moment arises from my attempt to prove a lemma,
that the sum of two elements of a quotient is in the quotient. I am unable
to get past a certain step, which I isolate in the following lemma:lemma "EX s. S = coset I s ==> EX s. S = {i + s | i. i \<in> I}"
proof -
assume "EX s. S = coset I s"
from this coset_def [of I s] show "EX s. S = {i + s | i. i \<in> I}"
by simp
qedI have defined
constdefs
coset :: "[('a::ring) set, 'a] => 'a set"
"coset I a == {i + a | i. i \<in> I}"
The problem with this proof is caused by your usage of the "of" theorem
attribute. Specifically, coset_def [of I s] instantiates coset_def with the
free variables "I" and "s" (on my system Proof General renders these in
blue), where the term you want to replace uses "s" as a bound variable
(rendered in green). Replace this with coset_def [of I] and the proof works.
and would like to think that it is a straightforward matter of
substitution. However, I know that section 5.11 of the tutorial makes it
clear that reasoning about existential operators can be very tricky. Am I
missing something crucial?Robert Lamar
When you instantiate coset_def with free variables "I" and "s", you get an
assumption that is too weak, since it only asserts the equality for a single
value of "s". For simp to perform a substitution under a quantifier, on a
term containing bound variables, the equality needs to hold for all possible
values of the bound variables. Leaving a variable uninstantiated has the
effect of a universal quantification over that variable, and simp is able to
match it against a bound variable.
It appears that [of I] is still necessary to instantiate the free type
variable in coset_def. Apparently, leaving a type variable uninstantiated
does not have the same effect as an uninstantiated term variable, as far as
simp is concerned; simp cannot match the types and it fails.
As a simpler alternative, you can give coset_def as an argument to simp or
unfold, which avoids the problems with instantiating type variables:
lemma "EX s. S = coset I s ==> EX s. S = {i + s | i. i \<in> I}"
proof -
assume "EX s. S = coset I s"
then show "EX s. S = {i + s | i. i \<in> I}"
by (unfold coset_def)
qed
Last updated: May 03 2024 at 12:27 UTC