[isabelle-dev] Algebra and number theory in Isabelle/HOL

Wed Nov 12 19:27:01 CET 2014

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
-------------- next part --------------

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141112/05a3f7e3/attachment.sig>