Hi all, thanks for the valuable comments.
Apart from integrating feedback, I added one aim which clarifies my
intention:
* Give a suitable algebraic foundation for number-theory-related
material in @{text ‹HOL-Main›} (@{const gcd}, @{const div},
@{const mod}}) to provide generic theorems without pulling (too
much) algebra into. Key insight: class hierarchy may be augmented
later by additional intermediate points.
> I noticed a remark about the treatment of signs in integer division. You
> mention two constraints but overlook a third: standard textbooks say that the
> remainder should have the same sign as the divisor, so that for example -1
> mod 2 = 1 and therefore -1 div 2 = -1. Computer hardware get this wrong.
Thanks for that bit of information.
> * Take care about the names of the algebraic structures. By PIR
> (principal ideal ring) some authors mean a commutative ring with
> identity in which every ideal is principal, using the name PID
> (principal ideal domain) for integral domains in which every ideal is
> principal. But other authors say that a PIR is an integral domain in
> which every ideal is principal. The same happens to Euclidean
> domain/Euclidean ring, Unique Factorization Domain/Factorial ring and so
> on. It would be desirable to follow the same convention for every structure.
Concerning this agenda I do not see a point where I touch the questions
of ring ideals anyway (this might seem strange to an algebraist). The
only existing type class we have in HOL-Main involving »domain« are the
type classes for integral domains (semi)dom and I treat those as given
as they are.
> * In the first assumption of the factorial_semiring class, maybe is "a
> is not an unit" instead of "a is not 1"?
Yes, indeed. Thanks for checking.
> * If an operation is_prime is fixed in a factorial_semiring class, as
> far as I know then it would not be possible to prove that each euclidean
> ring is a factorial ring by means of subclasses (unless the
> euclidean_ring class is changed). Could is_prime be a definition in the
> comm_ring class? In addition, prime and irreducible elements are defined
> in commutative rings (there they are different, but in UFD they are the
> same).
Yes, something like that. The details can easily worked out (or
changed) once the specifications are there.
Thanks a lot,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
section \<open>An agenda for refining and augmenting existing algebraic
material in Isabelle/HOL\<close>
theory Agenda_Algebra
imports Main "~~/src/HOL/GCD" "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
"~~/src/HOL/Library/Multiset"
begin
(*<*)
no_notation quotient (infixl "'/'/" 90)
class \<dots>
(*>*)
subsection \<open>Preliminaries: established principles of the hierarchy
of algebraic type classes in Isabelle\<close>
text \<open>
* Aim: pragmatic application, not meta-theory.
* Direct specification of operations.
* Specifications refer to whole type, not (restricted) carrier.
* Not too much specificational detail: class hierarchy may be augmented later
by
additional intermediate points.
* Clever use of abbreviations (examples: @{abbrev even}, @{abbrev odd},
\<dots>).
* For each @{text ring} there is also a @{text semiring} if natural numbers
are an instance.
* Use syntactic classes to be able to reuse syntax. Only then.
* Locale fragments for common properties regardless of a particular syntax.
\<close>
subsection \<open>Overall aims\<close>
text \<open>
* Give a suitable algebraic foundation for number-theory-related material in
@{text \<open>HOL-Main\<close>} (@{const gcd}, @{const div}, @{const mod}})
to provide
generic theorems without pulling (too much) algebra into. Key insight:
class hierarchy may be augmented later by additional intermediate points.
* Establish type classes for typical algebraic structures: rings with @{const
gcd},
factorial rings, euclidean rings.
* Get rid of last occurrences of watering-can interpretations in @{text
\<open>HOL-Complex_Main\<close>}.
* Simplify type class hierarchy if possible. Avoid technical type classes
whenever possible.
* More common material for number theory.
* Give a solid foundation for a simplified, less technical @{text
\<open>HOL-Word\<close>}.
\<close>
subsection \<open>First iteration\<close>
subsubsection \<open>Concerning @{theory Euclidean_Algorithm}\<close>
text \<open>
* Eliminate proof warnings.
* Distribute generic lemmas to appropriate places.
* Get rid of auxiliary definitions: @{const is_unit} is an ideal candidate
for an (input?)
abbreviation. @{const ring_inv} could stand well without being defined at
all.
\<close>
subsubsection \<open>Concerning @{const gcd}\<close>
text \<open>
* Provide explicit type class for (semi)rings with @{const gcd}:
\<close>
class semiring_gcd = comm_semiring_1 (*or stricter?*) + gcd +
assumes gcd_dvd1: "gcd a b dvd a"
and gcd_dvd2: "gcd a b dvd b"
and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b
\<Longrightarrow> c dvd gcd a b"
class ring_gcd = comm_ring_1 (*or stricter?*) + semiring_gcd
text \<open>
* Generalize existing theorems as far as appropriate, also using material
from @{theory Euclidean_Algorithm}.
* Adapt existing @{theory Euclidean_Algorithm} to be subclass of that
ring structures.
* Provide typical instances on available types.
\<close>
subsubsection \<open>Refinement of division on @{text \<int>}\<close>
lemma sgn_mod:
fixes k l :: int
assumes "l \<noteq> 0" and "k mod l \<noteq> 0"
shows "sgn (k mod l) = sgn l"
proof (cases "l < 0")
case False with `l \<noteq> 0` have "l > 0" by simp
then have "k mod l \<ge> 0" by simp
with `k mod l \<noteq> 0` have "k mod l > 0" by simp
with `l > 0` show ?thesis by simp
next
case True
then have "k mod l \<le> 0" by simp
with `k mod l \<noteq> 0` have "k mod l < 0" by simp
with `l < 0` show ?thesis by simp
qed
text \<open>
* Develop division on @{text \<int>} from @{text \<nat>} to avoid separate
bootstrap.
* Note 1: sign of division is determined by the obviously desirable facts
@{lemma "b \<noteq> 0 \<Longrightarrow> a * b div b = (a::int)" by (fact
div_mult_self2_is_id)},
@{lemma "a div b * b + a mod b = (a::int)" by (fact mod_div_equality)}
and the mathematical convention @{thm sgn_mod}.
This seems to support the current (though slightly confusing) sign
rules for @{text \<int>}.
* The mentioned rules for sign determination maybe also generalize
to arbitrary ring structures where @{const sgn} corresponds to
\<guillemotright>unit extraction\<guillemotleft>.
* Independent simp rules for division on @{text \<nat>}.
\<close>
subsubsection \<open>Concerning @{text \<open>HOL-Word\<close>}\<close>
text \<open>
* Find suitable characterization for @{prop "v dvd w"} on @{text word} in
terms
of @{prop "k dvd l"} @{text int} (or even @{text nat}):
missing so far and surely needed for further steps.
\<close>
subsubsection \<open>Refinement class hierarchy to constructively reflect the
concept of
partial inverse operations\<close>
text \<open>
To understand, have a look at @{class cancel_ab_semigroup_add} with
specification @{lemma "a + b = a + c \<Longrightarrow> b =
(c::'a::cancel_ab_semigroup_add)"
by (fact add_imp_eq)}. This violates the principle of direct specification of
operations.
Why? Its formulation implies that @{term "plus a"} is an injective operation
and thus there is an (underspecified) inverse operation @{text "_ - a"}.
The inability to use that inverse operation directly makes proofs unnecessary
complicated and has created strange constructions in the class hierarchy to
accomplish certain lemmas concerning @{text "_ dvd _"}.
Hence:
* Turn @{text cancel} type classes into constructive ones:
\<close>
class cancel_ab_semigroup_add = ab_semigroup_add + minus +
assumes add_diff_cancel: "a + b - b = a"
text \<open>
* Unify @{text "_ / _"} and @{text "_ dvd _"} logically. This provides
the desired (underspecified) multiplicative inverse operations.
It is still possible to have separate syntax for fields and (euclidean)
rings.
For simplicity we just use @{text "_ // _"} here.
\<close>
class divide =
fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/'/" 70)
class semiring_no_zero_divisors = semiring_0 + divide +
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0
\<Longrightarrow> a * b \<noteq> 0"
assumes mult_div_cancel: "b \<noteq> 0 \<Longrightarrow> a * b // b = a"
class ring_no_zero_divisors = ring + semiring_no_zero_divisors
class semiring_div = semiring_no_zero_divisors + \<dots> -- \<open>augments
@{text "_ mod _"}\<close>
class field = ring_no_zero_divisors + \<dots> -- \<open>augments @{text
inverse}\<close>
text \<open>
* Generalize existing theorems for @{text "_ dvd _"} accordingly.
\<close>
subsection \<open>Second iteration\<close>
subsubsection \<open>Algebra\<close>
text \<open>
The steps here are not so well-specified at the moment but can be worked out
after the first iteration.
* Separate generic divisibility machinery (units, normalization) from
@{theory Euclidean_Algorithm} into a separate theory.
* Use this to create a theory on factorial rings. Two approaches can
be thought of, the first one would be the preferred one if it
works out. The second one could stand as a separate thing.
The choice here has significant effect on the further steps.
\<close>
class factorial_semiring = semiring_no_zero_divisors + comm_semiring_1 +
\<dots> +
fixes is_prime :: "'a \<Rightarrow> bool" -- \<open>FIXME should be
defined at a lower floor\<close>
assumes "is_prime p \<Longrightarrow> a dvd p \<Longrightarrow> \<not>
a dvd 1 \<Longrightarrow> p dvd a"
assumes "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow>
\<not> p dvd a \<Longrightarrow> p dvd b"
class constructive_factorial_semiring = factorial_semiring +
fixes primes_of :: "'a \<Rightarrow> 'a multiset"
assumes is_prime_primes_of: "p \<in># primes_of a \<Longrightarrow>
is_prime p"
assumes primes_of_prod_dvd: "msetprod (primes_of a) dvd a"
assumes dvd_primes_of_prod: "a dvd msetprod (primes_of a)"
text \<open>
* Prove that each euclidean ring is a factorial ring.
* Prove that each factorial ring is a gcd ring.
* Integrate this appropriately into @{text \<open>HOL-Main\<close>}. There
are good chances
that only the euclidean ring has to be integrated here, with the factorial
ring being a more general case in a library theory: we are only interested
in @{text \<nat>} and @{text \<int>} in @{text \<open>HOL-Main\<close>}.
* Provide typical instances.
* Augment gcd somehow to establish @{text "(dvd, gcd)"} as semilattice.
* Maybe get rid of @{class semiring_numeral_div}. For this it may be
interesting
to note that in @{class linordered_idom} the operations @{const sgn},
@{const abs}
and @{text "_ > 0"} seem to provide everything to formulate divisibility.
\<close>
subsubsection \<open>@{text \<open>HOL-Word\<close>}\<close>
text \<open>
With all that equipment we are able to do a complete iteration over @{text
\<open>HOL-Word\<close>},
particularly:
* Revisit type classes.
* Eliminate duplicates.
* Simplify technical definitions to algebraic ones.
* \<dots>
\<close>
subsection \<open>Slightly related topics\<close>
text \<open>
* Provide a suitable tool for inspecting and analysing the class hierarchy,
e. g. class
graph with annotated specifications etc. Either repair existing graph
browser and
use as base or swallow the bitter pill and provide an alternative dot
backend.
* A formalisation of the Gaussian integers (e. g. as a student project).
This is a nice
but still simple application of number theory beyond the
\<guillemotright>boring\<guillemotleft> standards @{text \<nat>}, @{text \<int>}
etc. Gaussian integers @{text \<open>\<int> + i\<int>\<close>} form an
euclidean ring!
* Inspect and tune specific simp rules for @{text presburger} and @{text
algebra}
(further candidates?). Seems to be rather historic\<dots>
* Consider using dedicated named theorems slot for numeral simps, to have a
simple
@{text \<open>simp del: \<dots>\<close>} at hand.
* Find mathematical conventions concerning precedence of @{text \<open>_ mod
_\<close>}. Not sure
whether it is canonical to have it the same as @{text \<open>_ *
_\<close>}, @{text \<open>_ / _\<close>}.
* Operation @{term "real :: 'a::real_of \<Rightarrow> real"} is a slight
accident. Better prefer
explicit @{const of_nat}, @{const of_int} etc. and let implicit coercion do
the rest.
\<close>
end
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
