Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-01 23:28:45 -0800 (Mon, 01 Apr 2002)
Revision: 3552
Log message:

      Removed the introduction rule for "equiv" since it made proofs awkard
      and could be easily substitued with a rewrite rule;
      Reproved related rules.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-01 23:45:26 -0800 (Mon, 01 Apr 2002)
Revision: 3553
Log message:

      1. Added "eqG" to the definition of groups which denotes the equivalence
         relation related with the group. Every group has an equivalence
         relation, which is now explicitly described.
      2. Accordingly, all rules related with equivalence relations in groups
         are updated and reproved.
      3. Added tactics "uniqueInvLeftT" and "uniqueInvRightT" which might not
         be very useful though.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-01 23:47:14 -0800 (Mon, 01 Apr 2002)
Revision: 3554
Log message:

      Removed useless stuffs previously in comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-01 23:49:49 -0800 (Mon, 01 Apr 2002)
Revision: 3555
Log message:

      Updated the definition and rules for abelian groups due to the adding
      of "eqG".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 00:08:36 -0800 (Tue, 02 Apr 2002)
Revision: 3556
Log message:

      1. Changed the representation of subgroups; it looks more natural now.
      2. Updated the definition of subgroups. Since "eqG" was added to the def.
         of groups, the def. of a subgroup must give the description for "eqG".\
      3. Updated all rules and reproved them.
      
      TODO:
      I just realized that the def. for subgroups are not sufficient yet:
        1. "equiv" instead of "equal" should be used for the operations;
        2. the description for "eqG" is not complete; I should also give
           the other side, i.e., if a and b are in s and a is equivalent
           to b under eqG{g}, then a is also equivalent to b under eqG{s}.
      Will correct these soon.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 00:18:40 -0800 (Tue, 02 Apr 2002)
Revision: 3557
Log message:

      1. Changed the representation of cyclic subgroups; it looks more
         natural now.
      2. Updated the definition of cyclic subgroups. Since "eqG" was added
         to the def. of groups, the def. of a cyclic subgroup must give the
         description for "eqG" too.
      3. Updated all rules and reproved them.
      
      The same problems as in subgroups exist here also. Will fix soon.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 00:27:06 -0800 (Tue, 02 Apr 2002)
Revision: 3558
Log message:

      1. Changed the rewrite rule for cyclic groups. Previously it was defined
         by cyclic subgroups; now it is defined directly by its underlying set;
      2. Updated rules due to the adding of "eqG" and reproved them.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 00:46:33 -0800 (Tue, 02 Apr 2002)
Revision: 3559
Log message:

      Changed def of homomorphisms and reproved all rules;
      Added tactics "homIdT" and "homInvT".
      
      Not finished yet. Will do the rest after fixing errors in subgroups
      and cylic subgroups.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 21:27:01 -0800 (Tue, 02 Apr 2002)
Revision: 3560
Log message:

      Changed the definition of subgroups; fixed the errors in defining the
      operation and equivalence relation for subgroups.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-02 21:29:19 -0800 (Tue, 02 Apr 2002)
Revision: 3561
Log message:

      Changed the definition of cyclic subgroups; fixed the previous error in
      defining the operation and equivalence relation for cyclic subgroups.
      Updated related rules.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-03 00:37:31 -0800 (Wed, 03 Apr 2002)
Revision: 3562
Log message:

      So, I've defined the compile function in Mp_mc_compile to actually
      take an Fir.prog, convert the function definitions to terms,
      and then back again, in one big identity operation.  The current
      term representation of the FIR functions is a bit of a hack that
      will need to be cleaned up if anything non-trivial is to be done.
      (Each individual function is fine I hope.  It's the program as a whole
      that's represented rather poorly.  It's essentially a (term SymbolTable.t),
      one term for each fundef in the original Fir.prog.prog_funs.)
      Though, this should be sufficient for basic testing I think.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-04 17:16:49 -0800 (Thu, 04 Apr 2002)
Revision: 3563
Log message:

      Updates to reflect the (ever changing) MC FIR.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-04 23:07:58 -0800 (Thu, 04 Apr 2002)
Revision: 3564
Log message:

      -  Fixed some problems in Mp_mc_fir_eval and proved
         the rewrites in it.
      -  Proved 2 of the deadcode elimination rewrites (in Mp_mc_deadcode).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-05 01:33:57 -0800 (Fri, 05 Apr 2002)
Revision: 3565
Log message:

      Redoing constant elimination, now that I've corrected
      the mistake I made in FIR evaluation.  As a sidenote, I'm not
      completely convinced that I've expressed how division expressions evaluation
      "correctly".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 22:56:39 -0700 (Mon, 08 Apr 2002)
Revision: 3566
Log message:

      Updated to reflect new file names.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 22:57:26 -0700 (Mon, 08 Apr 2002)
Revision: 3567
Log message:

      1. Redefined inverse image. Previously it was defined by introduction
         and elimination rules; now it can be rewritten with "setbvd_prop".
         Actually, after "setbvd_prop" is defined, the "inv_image" is somewhat
         unnecessary. I keep it here just in case that people may want to use
         the concept of inverse image sometimes.
      2. Fixed the error in the previous member elimination rule.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 22:57:54 -0700 (Mon, 08 Apr 2002)
Revision: 3568
Log message:

      Added the definition for setbvd_prop. "set_bvd" and "setbvd_prop" are
      both methods for building sets. The former builds set { a(x) | x in s }
      from set s where a(x) is a function; the latter builds set
      { x in s | p(x) } from all elements x in s satisfying p(x). Both of
      them are very useful. The former is defined by set induction on s; the
      latter is defined by member introduction and elimination rules.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 22:58:44 -0700 (Mon, 08 Apr 2002)
Revision: 3569
Log message:

      Defined "group builder" group_bvd{'h; 'g; 's} which build a group
      h from group g where the underlying set of h is s, the operation
      and equivalence relation in h are the same as in g. The only use
      for the introduction of group_bvd is to make codes cleaner, nicer,
      or easier to understand. (See examples in Czf_itt_subgroup,
      Czf_itt_cyclic_subgroup, and Czf_itt_hom.)
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 22:59:41 -0700 (Mon, 08 Apr 2002)
Revision: 3570
Log message:

      Updated the definition of subgroups and cyclic subgroups utilizing
      group_bvd. They look much cleaner now.
      Also updated related rules and their proofs.
      

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

      Defined cosets for subgroups:
        Let H be a subgroup of a group G. aH = {ah | h in H} is the left
        coset of H containing a, while Ha = {ha | h in H} is the right
        coset of H containing a.
      
      The cosets of H are subsets of G.
      
      Suppose f: G1 -> G2 is a group homomorphism of G1 into G2; H is the
      kernel of f. For any a in G1, aH = Ha = { x in G1 | f(x) = f(a) }.
      (This is proved in Czf_itt_hom.)
      

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

      Defined normal subgroups:
        A subgroup H of a group G is normal if its left and right cosets
        coincide, that is, if gH = Ha for all g in G.
      
      All subgroups of abelian groups are normal.
      
      The kernel of a homomorphism f: G1 -> G2 is a normal subgroup of G1.
      (This is proved in Czf_itt_hom.)
      
      Note/TODO:
        There is a standared way to show that two sets are equal;
        show that each is a subset of the other.
        I fould this method very useful and wrote it up as a tactic
        "equalSubsetT", but I cannot prove it. It is better put in
        Czf_itt_subset.
      

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 by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 23:02:28 -0700 (Mon, 08 Apr 2002)
Revision: 3574
Log message:

      1. Defined group isomorphisms based on group homomorphisms. An
         isomorphism f: G1 -> G2 is a homomorphism that is one-to-one
         and onto G2. That is, an isomorphism f: G1 -> G2 is a
         homomorphism where f is a bijection.
      2. Also defined and proved the functionality rules (both equality
         and equivalence) for isomorphisms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-11 22:37:53 -0700 (Thu, 11 Apr 2002)
Revision: 3576
Log message:

      These updates to the Conscripts allow for a compiles,
      started in the MC source tree, to optionally
      compile MetaPRL.  Nothing in MetaPRL itself should be
      affected by these changes.  The only important
      thing to note that is "#", in INCPATH's
      has been replaced by $env->{MP}, which is set
      in the toplevel Conscript.  "#" will refer to the
      wrong root if the compile is started in MC.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-04-16 12:59:11 -0700 (Tue, 16 Apr 2002)
Revision: 3577
Log message:

      I am adding to CVS the "UI Design Goals and Ideas" document that was written last Fall.
      
      This is the version from September 25, 2001.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-04-16 12:59:37 -0700 (Tue, 16 Apr 2002)
Revision: 3578
Log message:

      This is the version from October 22, 2001.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-04-16 13:09:49 -0700 (Tue, 16 Apr 2002)
Revision: 3579
Log message:

      Added names.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-19 01:09:21 -0700 (Fri, 19 Apr 2002)
Revision: 3580
Log message:

      Comitting more changes to reflect the ever changing MC FIR.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-04-24 16:51:09 -0700 (Wed, 24 Apr 2002)
Revision: 3582
Log message:

      Added "make latex" target.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-24 22:26:29 -0700 (Wed, 24 Apr 2002)
Revision: 3583
Log message:

      Committing a much needed update of the README file.
      Currently contains a brief introduction to the motiviations
      that led to this theory's creation and some notes
      about compiling MetaPRL with MC (the Mojave Compiler).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-04-25 08:28:40 -0700 (Thu, 25 Apr 2002)
Revision: 3584
Log message:

      - Added the comment module to the theories.pdf ("make latex").
      
      - Added a hack allowing to override a theory display with another theory's
      display. This is necessary for bootstrapping reasons - it allows one
      to get a reasonable output of a theory (e.g. Comment) that is defined before
      all essential display forms (e.g. the Summary ones) are there.
      
      - Added debugging code to make it easier to find dforms that cause
      zone begin/end mismatch (and used it to get rid of all
      the "Unballanced buffer" warnings in "make latex").
      
      - Minor dforms&comments updates.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-04-26 16:58:23 -0700 (Fri, 26 Apr 2002)
Revision: 3585
Log message:

      Correct a typo in CZF documentation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-04-26 18:42:23 -0700 (Fri, 26 Apr 2002)
Revision: 3586
Log message:

      Noop commit - I've only fixed the CRLF/LF mixed line terminators.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-26 19:43:27 -0700 (Fri, 26 Apr 2002)
Revision: 3587
Log message:

      Adding file to specify which modules to print documentation for.
      (And adding .cvsignore to ignore generated files.)
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-26 19:45:24 -0700 (Fri, 26 Apr 2002)
Revision: 3588
Log message:

      Updating modules so that they generate documentation
      for theories.pdf.  Right now, it's _very_ minimal and
      not so useful.  Hopefully, I will get around to updating
      them and making them decent.
      
      Also updating the README file to properly reflect the
      name of our research group at Caltech.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-26 21:44:46 -0700 (Fri, 26 Apr 2002)
Revision: 3589
Log message:

      Adding yet another term that I forgot for the FIR.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-27 12:52:38 -0700 (Sat, 27 Apr 2002)
Revision: 3590
Log message:

      Adding some documentation.  Still have a long ways to go
      in fully documenting everything.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-04-28 12:51:58 -0700 (Sun, 28 Apr 2002)
Revision: 3591
Log message:

      - Added an option to be have "THEORIES=all" in mk/config
      (instead of THEORIES="long list of theories").
      I will change all my nightly scripts to use THEORIES=all.
      
      - Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex
      that would automatically contain \inputs corresponding to TEXTHEORIES.
      (Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES
      was changed).
      
      - Minor fixes in some display forms.
      
      - Removed theories/caml that never had anything useful.
      
      - Removed a few files from theories/ocaml_doc that seemed to be there by accident
      (Jason, can you confirm?).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-29 16:15:57 -0700 (Mon, 29 Apr 2002)
Revision: 3592
Log message:

      Some more documentation.  I'll be able to document more things
      when the MC developers document their stuff a bit more.
      I've changed the order in which the modules of the mc theory
      are printed so that I can put an overview of the theory
      in Mp_mc_theory and have that serve as an introduction to the
      rest of the modules.  (This over view is not currently in there,
      but should be on my next commit.)
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-04-29 17:41:41 -0700 (Mon, 29 Apr 2002)
Revision: 3593
Log message:

      Change the documentation in czf_fol again (union -> +).
      Also change the documentation for records.