next up previous contents
Next: Some theorems about Modulo Up: The Integers Previous: The Integers-Definitions

Basic Lemmas

This file contains some basic theorems about the integers involving the algebraic operators, e.g. commutativity, associativity etc. Note this file takes quite a long time to load.

The variable eq is a generic equality for any set and is defined in the file in the directory lib_sets. Here it is always implicitly specialized to Eq_zed which is the equality defined on the set int in the file lib_int_basics.

 ** Module lib_int_basics_thms Imports lib_integers/lib_int_basics
  times_one_zed = ... : {m|int.1}eq m (times_zed one_zed m)
  middle_four_plus_zed = ... :
    eq (plus_zed (plus_zed a c) (plus_zed b d))
       (plus_zed (plus_zed a b) (plus_zed c d))
  times_plus_dist_r_zed = ... :
    eq (times_zed (plus_zed a b) c)
       (plus_zed (times_zed a c) (times_zed b c))
  times_plus_dist_l_zed = ... :
    eq (times_zed c (plus_zed a b))
       (plus_zed (times_zed c a) (times_zed c b))
  times_resp_eq_l = ... :
    {a,b,x:int.1}(eq a b)->eq (times_zed x a) (times_zed x b)
  plus_commutes_zed = ... : {p,q|int.1}Eq (plus_zed p q) (plus_zed q p)
  times_commutes_zed = ... :
    {p,q|int.1}Eq (times_zed p q) (times_zed q p)
  times_assoc_zed = ... :
    eq (times_zed (times_zed a b) c) (times_zed a (times_zed b c))
  plus_resp_eq = ... :
    {a,b,x,y:int.1}(eq a b)->(eq x y)->eq (plus_zed a x) (plus_zed b y)
  minus_resp_eq = ... :
    {a,b,x,y:int.1}(eq a b)->(eq x y)->
    eq (minus_zed a x) (minus_zed b y)
  times_resp_eq_r = ... :
    {a,b,x:int.1}(eq a b)->eq (times_zed a x) (times_zed b x)
  times_resp_eq = ... :
    {a,b,x,y:int.1}(eq a b)->(eq x y)->
    eq (times_zed a x) (times_zed b y)
  neg_resp_eq = ... : {x,y:int.1}(eq x y)->eq (neg_zed x) (neg_zed y)
  neg_minus = ... :
    {x,y:int.1}eq (plus_zed x (neg_zed y)) (minus_zed x y)
  times_cancel_left_zed = ... :
    {x,y,a:int.1}(not (eq a zero_zed))->
    (eq (times_zed a x) (times_zed a y))->eq x y
  middle_four_times_zed = ... :
    eq (times_zed (times_zed x y) (times_zed a b))
       (times_zed (times_zed x a) (times_zed y b))
  eq_zero_zed_imp = ... : {x:zed}(eq zero_zed x)->Eq x.1 x.2
  imp_eq_zero_zed = ... : {x:zed}(Eq x.1 x.2)->eq zero_zed x
  times_zero_lemma_zed = ... :
    {x,y:zed}(eq (times_zed x y) zero_zed)->
    or (eq zero_zed x) (eq zero_zed y)
  right_dist_minus_times_zed = ... :
    eq (times_zed (minus_zed a b) c)
       (minus_zed (times_zed a c) (times_zed b c))
  times_neg = ... :
    {x,y:int.1}eq (times_zed x (neg_zed y)) (times_zed y (neg_zed x))
  times_neg_both = ... :
    {x,y:int.1}eq (times_zed x y) (times_zed (neg_zed x) (neg_zed y))
  plus_assoc_zed = ... :
    eq (plus_zed (plus_zed a b) c) (plus_zed a (plus_zed b c))
  one_times_zed = ... : {x:int.1}eq (times_zed one_zed x) x
  plus_zero_zed = ... : {x:int.1}eq (plus_zed x zero_zed) x
  minus_zed_is = ... :
    {x,y,z:int.1}iff (eq (minus_zed x y) z) (eq x (plus_zed y z))
  n_minus_n_Eq_zero_zed = ... : {x:int.1}eq (minus_zed x x) zero_zed
  plus_inv_minus_zed = ... :
    {x,y:int.1}eq (plus_zed (minus_zed x y) y) x
  bring_neg_out = ... :
    {x,y:int.1}eq (times_zed (neg_zed x) y) (neg_zed (times_zed x y))
  minus_is_minus_zed = ... :
    {a,b:nat}(Le a b)->eq (minus_zed (b,zero) (a,zero)) (minus b a,zero)

Fri May 24 19:01:27 BST 1996