products/Sources/formale Sprachen/Isabelle/HOL/ex image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Residue_Ring.thy   Sprache: Isabelle

Original von: Isabelle©

(*  Author:  Florian Haftmann, TUM
*)


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)

end

context
  includes lifting_syntax
begin

lemma [transfer_rule]:
  "((\) ===> pcr_residue_ring) of_bool of_bool"
  by (unfold of_bool_def [abs_def]; transfer_prover)

lemma [transfer_rule]:
  "((=) ===> pcr_residue_ring) numeral numeral"
  by (rule transfer_rule_numeral; transfer_prover)

lemma [transfer_rule]:
  "((=) ===> pcr_residue_ring) int of_nat"
  by (rule transfer_rule_of_nat; transfer_prover)

end

end

¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

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.


Bot Zugriff