Package modular-equiv: Definitions and theorems about modular equivalence

Information

Files

• Package tarball modular-equiv-1.0.tgz
• Theory file modular-equiv.thy (included in the package tarball)

Defined Constant

• Number
  • Modular
    • Number.Modular.equivalent

Theorems

⊦ ∀x. Number.Modular.equivalent x x

⊦ ∀x y.
    Number.Modular.equivalent x y ⇔
    x mod Number.Modular.modulus = y mod Number.Modular.modulus

⊦ ∀x y z.
    Number.Modular.equivalent x y ∧ Number.Modular.equivalent y z ⇒
    Number.Modular.equivalent x z

⊦ ∀x y.
    Number.Modular.equivalent x = Number.Modular.equivalent y ⇔
    x mod Number.Modular.modulus = y mod Number.Modular.modulus

⊦ ∀x y.
    x < Number.Modular.modulus ∧ y < Number.Modular.modulus ∧
    Number.Modular.equivalent x = Number.Modular.equivalent y ⇒ x = y

⊦ ∀x1 x2 y1 y2.
    Number.Modular.equivalent x1 x2 ∧ Number.Modular.equivalent y1 y2 ⇒
    Number.Modular.equivalent (x1 * y1) (x2 * y2)

⊦ ∀x1 x2 y1 y2.
    Number.Modular.equivalent x1 x2 ∧ Number.Modular.equivalent y1 y2 ⇒
    Number.Modular.equivalent (x1 + y1) (x2 + y2)

Input Type Operators

• →
• bool
• Number
  • Natural
    • natural

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ¬
    • F
    • T
• Number
  • Modular
    • Number.Modular.modulus
  • Natural
    • *
    • +
    • <
    • mod

Assumptions

⊦ T

⊦ ∀t. (∀x. t) ⇔ t

⊦ (∀) = λP. P = λx. T

⊦ ∀x. x = x ⇔ T

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀n. n < Number.Modular.modulus ⇒ n mod Number.Modular.modulus = n

⊦ (∧) = λp q. (λf. f p q) = λf. f T T

⊦ ∀f g. f = g ⇔ ∀x. f x = g x

⊦ ∀m n.
    m mod Number.Modular.modulus * (n mod Number.Modular.modulus) mod
    Number.Modular.modulus = m * n mod Number.Modular.modulus

⊦ ∀m n.
    (m mod Number.Modular.modulus + n mod Number.Modular.modulus) mod
    Number.Modular.modulus = (m + n) mod Number.Modular.modulus

⊦ ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t)

⊦ ∀t. (T ⇒ t ⇔ t) ∧ (t ⇒ T ⇔ T) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬t)