Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 23:02:02 -0700 (Mon, 08 Apr 2002)
Revision: 3573
Log message:

      1. Defined kernels using "hom" and "group_bvd":
           f is a homomorphism of g1 into g2. The elements of g1,
           which are mapped into the identity of g2, form a subgroup
           h of g called the kernel of f.
      
      2. Added and proved the following properties of homomorphisms:
        i.  Let f: G -> G' be a group homomorphism of G into G'.
            If H is a subgroup of G, then f[H] is a subgroup of G'.
        ii. Let f: G -> G' be a group homomorphism of G into G'.
            If H is a subgroup of G', then the inverse image of
            H is a subgroup of G.
      
      3. Added and proved the following properties of kernels:
        i.  Let f: G -> G' be a group homomorphism of G into G'.
            The kernel of f is a subgroup of G.
        ii. Let f: G1 -> G2 be a group homomorphism of G1 into G2.
            Let H be the kernel of f. For any a in G1, the set
            { x in G1 | f(x) = f(a) } is the left coset aH of H.
        iii.Let f: G1 -> G2 be a group homomorphism of G1 into G2.
            Let H be the kernel of f. For any a in G1, the set
            { x in G1 | f(x) = f(a) } is also the right coset Ha of H.
        iv. A group homomorphism f: G1 -> G2 is a one-to-one map
            if and only if Ker(f) = {id(g1)}.
        v.  The kernel of a homomorphism f: G1 -> G2 is a normal
            subgroup of G1.
      
      Tactics:
         kernelSubgroupT, kernelLcosetT, kernelRcosetT, kernelNormalSubgT
      
      Note:
         The property that "A group homomorphism f: G1 -> G2 is a one-to-
         one map if and only if Ker(f) = {id(g1)}." can also be written
         into a tactics when necessary.
      

Changes	Path
+168 -2	metaprl/theories/czf/czf_itt_hom.ml
+9 -1	metaprl/theories/czf/czf_itt_hom.mli
+12050 -822	metaprl/theories/czf/czf_itt_hom.prla