Package modular-thm: modular-thm

Information

name	modular-thm
version	1.1
description	modular-thm
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2011-03-17
show	Data.Bool

Files

Package tarball modular-thm-1.1.tgz
Theory file modular-thm.thy (included in the package tarball)

Theorems

⊦ ∀x. Number.Natural.< (Number.Modular.toNatural x) Number.Modular.modulus

⊦ ∀x.
Number.Natural.div (Number.Modular.toNatural x)
Number.Modular.modulus = Number.Numeral.zero

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

⊦ ∀x y. Number.Modular.toNatural x = Number.Modular.toNatural y ⇒ x = y

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

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

Input Type Operators

→
bool
Number
- Modular
  - Number.Modular.modular
- Natural
  - Number.Natural.natural

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ¬
  - T
Number
- Modular
  - Number.Modular.+
  - Number.Modular.<
  - Number.Modular.≤
  - Number.Modular.fromNatural
  - Number.Modular.modulus
  - Number.Modular.toNatural
- Natural
  - Number.Natural.+
  - Number.Natural.<
  - Number.Natural.≤
  - Number.Natural.div
  - Number.Natural.mod
- Numeral
  - Number.Numeral.zero

Assumptions

⊦ T

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

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

⊦ ∀x. x = x ⇔ T

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

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

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

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

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

⊦ ∀m n. ¬Number.Natural.≤ m n ⇔ Number.Natural.< n m

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

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

⊦ ∀m n. Number.Natural.< m n ⇒ Number.Natural.div m n = Number.Numeral.zero

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