Package modular-def: modular-def

Information

Files

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

Defined Type Operator

• Number
  • Modular
    • Number.Modular.modular

Defined Constants

• Number
  • Modular
    • Number.Modular.*
    • Number.Modular.+
    • Number.Modular.-
    • Number.Modular.<
    • Number.Modular.≤
    • Number.Modular.¬
    • Number.Modular.fromNatural
    • Number.Modular.toNatural

Theorems

⊦ ∀x. Number.Modular.fromNatural (Number.Modular.toNatural x) = x

⊦ ∀x.
    Number.Modular.toNatural (Number.Modular.fromNatural x) =
    Number.Natural.mod x Number.Modular.modulus

⊦ ∀x.
    Number.Modular.¬ x =
    Number.Modular.fromNatural
      (Number.Natural.- Number.Modular.modulus
         (Number.Modular.toNatural x))

⊦ ∀x y. Number.Modular.< x y ⇔ ¬Number.Modular.≤ y x

⊦ ∀x y. Number.Modular.- x y = Number.Modular.+ x (Number.Modular.¬ y)

⊦ ∀x y.
    Number.Modular.≤ x y ⇔
    Number.Natural.≤ (Number.Modular.toNatural x)
      (Number.Modular.toNatural y)

⊦ ∀x1 y1.
    Number.Modular.fromNatural (Number.Natural.* x1 y1) =
    Number.Modular.* (Number.Modular.fromNatural x1)
      (Number.Modular.fromNatural y1)

⊦ ∀x1 y1.
    Number.Modular.fromNatural (Number.Natural.+ x1 y1) =
    Number.Modular.+ (Number.Modular.fromNatural x1)
      (Number.Modular.fromNatural y1)

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

Input Type Operators

• →
• bool
• Number
  • Natural
    • Number.Natural.natural

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ¬
    • select
    • F
    • T
• Number
  • Modular
    • Number.Modular.equivalent
    • Number.Modular.modulus
  • Natural
    • Number.Natural.*
    • Number.Natural.+
    • Number.Natural.-
    • Number.Natural.<
    • Number.Natural.≤
    • Number.Natural.mod

Assumptions

⊦ T

⊦ ∀x. Number.Modular.equivalent x x

⊦ (∃) = λP. P ((select) P)

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

⊦ ∀t. (λx. t x) = t

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

⊦ ∀x. x = x ⇔ T

⊦ ∀n.
    Number.Natural.< (Number.Natural.mod n Number.Modular.modulus)
      Number.Modular.modulus

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

⊦ ∀n.
    Number.Natural.mod (Number.Natural.mod n Number.Modular.modulus)
      Number.Modular.modulus = Number.Natural.mod n Number.Modular.modulus

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

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

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

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

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

⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃y. ∀x. P x (y x)

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

⊦ ∀x y.
    Number.Natural.< x Number.Modular.modulus ∧
    Number.Natural.< 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 (Number.Natural.* x1 y1)
      (Number.Natural.* x2 y2)

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

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