section \<open>Proof of concept for residue rings over int using type numerals\<close>
theory Residue_Ring imports Main "HOL-Library.Type_Length" begin
class len2 = len0 + assumes len_ge_2 [iff]: "2 \ LENGTH('a)" begin
subclass len proof show"0 < LENGTH('a)"using len_ge_2 by arith qed
lemma len_not_eq_Suc_0 [simp]: "LENGTH('a) \ Suc 0" using len_ge_2 by arith
end
instance bit0 and bit1 :: (len) len2 by standard (simp_all add: Suc_le_eq)
quotient_type (overloaded) 'a residue_ring = int / "\k l. k mod int (LENGTH('a)) = l mod int (LENGTH('a::len2))" by (auto intro!: equivpI reflpI sympI transpI)
context semiring_1 begin
lift_definition repr :: "'b::len2 residue_ring \ 'a" is"\k. of_nat (nat (k mod int (LENGTH('b))))" by simp
end
instantiation residue_ring :: (len2) comm_ring_1 begin
lift_definition zero_residue_ring :: "'a residue_ring" is 0 .
lift_definition one_residue_ring :: "'a residue_ring" is 1 .
lift_definition plus_residue_ring :: "'a residue_ring \ 'a residue_ring \ 'a residue_ring" is plus by (fact mod_add_cong)
lift_definition uminus_residue_ring :: "'a residue_ring \ 'a residue_ring" is uminus by (fact mod_minus_cong)
lift_definition minus_residue_ring :: "'a residue_ring \ 'a residue_ring \ 'a residue_ring" is minus by (fact mod_diff_cong)
lift_definition times_residue_ring :: "'a residue_ring \ 'a residue_ring \ 'a residue_ring" is times by (fact mod_mult_cong)
instance by (standard; transfer) (simp_all add: algebra_simps mod_eq_0_iff_dvd)
lemma [transfer_rule]: "((=) ===> pcr_residue_ring) int of_nat" by (rule transfer_rule_of_nat; transfer_prover)
end
end
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.11Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
