Package group-mult-sub-thm: Correctness of group multiplication by repeated subtraction

Information

Files

• Package tarball group-mult-sub-thm-1.10.tgz
• Theory source file group-mult-sub-thm.thy (included in the package tarball)

Theorems

⊦ ∀x n. x * n = multSub ⊤ 0 0 x 0 (Fibonacci.encode n)

⊦ ∀x n d f p l.
    x + n = n + x ∧ x + d = d + x ⇒
    multSub ⊤ n d (x * f) (~(x * p)) l =
    n - d + x * Fibonacci.decode.dest f p l ∧
    multSub ⊥ n d (~(x * f)) (x * p) l =
    d - n + x * Fibonacci.decode.dest f p l

External Type Operators

• →
• bool
• Algebra
  • Group
    • group
• Data
  • List
    • list
• Number
  • Natural
    • natural

External Constants

• =
• Algebra
  • Group
    • *
    • +
    • -
    • ~
    • 0
    • multSub
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • List
    • ::
    • []
• Number
  • Natural
    • +
    • bit1
    • zero
    • Fibonacci
      • Fibonacci.decode
        • Fibonacci.decode.dest
      • Fibonacci.encode

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

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

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ t ⇔ t

⊦ ∀x. x * 0 = 0

⊦ ∀x. 0 + x = x

⊦ ∀x. x + 0 = x

⊦ ∀n. Fibonacci.decode (Fibonacci.encode n) = n

⊦ ∀x. x * 1 = x

⊦ ∀x. x + ~x = 0

⊦ ∀x. ~x + x = 0

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

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀f p. Fibonacci.decode.dest f p [] = 0

⊦ ∀l. Fibonacci.decode l = Fibonacci.decode.dest 1 0 l

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀m n. m + n = n + m

⊦ ∀x y. x - y = x + ~y

⊦ ∀x y. ~x + (x + y) = y

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

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

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀x y z. x = y ∧ y = z ⇒ x = z

⊦ ∀x y z. x + y + z = x + (y + z)

⊦ ∀x m n. x * (m + n) = x * m + x * n

⊦ ∀p. p [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l

⊦ ∀b n d f p. multSub b n d f p [] = if b then n - d else d - n

⊦ ∀x n y. x + y = y + x ⇒ x * n + y = y + x * n

⊦ ∀x n y. y + x = x + y ⇒ y + x * n = x * n + y

⊦ ∀f p h t.
    Fibonacci.decode.dest f p (h :: t) =
    let s ← f + p in
    let n ← Fibonacci.decode.dest s f t in
    if h then s + n else n

⊦ ∀b n d f p h t.
    multSub b n d f p (h :: t) =
    let s ← p - f in multSub (¬b) d (if h then n - s else n) s f t

OpenTheory package document generated by opentheory 1.2 (release 20140322)