Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-03-02 10:24:18 -0800 (Sat, 02 Mar 2002)
Revision: 3525
Log message:

      Minor ITT clean-up:
      - No need to use addHiddenLabelT when annotation on a rule will do
      - No need to create a separate tactic for sub resource when dT 0 will do
      - In substT no need to create a complete exception that would be caught right away.
      - Itt_tsub was never actually used, removing files.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-03 18:19:09 -0800 (Sun, 03 Mar 2002)
Revision: 3526
Log message:

      1. Defined functionality in the sense of equivalence relations,
         which is distinct from the functionality for equality.
      2. Added and proved properties of equivalence functionality.
      3. Added and proved functionality properties of equivalence relations
         (both equivalence functionality and equality functionality).
      4. Updated the substitution rules and tactics.
      
      Tactics for equivalence relations:
        equivFunSetT, equivFunMemT, equivRefT, equivSymT,
        equivTransT, equivSubstT
      
      TODO:
        1. Might need to define terms for functionality judgments on
           dependent types (i.e., equiv_dfun_prop).
        2. Implement equivalence class later.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-03 18:20:01 -0800 (Sun, 03 Mar 2002)
Revision: 3527
Log message:

      1. Replaced equality relations with equivalence relations in
         the definition axioms for "op", "inv", and "id".
      2. Defined the equivalence functionality for "op" and "inv".
      3. Changed the tactics for "left and right cancellation laws"
         (i.e., groupCancelLeftT and groupCancelRightT) to make it
         easier to use.
      4. Re-proved all properties.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-03-04 15:15:02 -0800 (Mon, 04 Mar 2002)
Revision: 3528
Log message:

      In process to fix problem (a>=b & b<a) pointed by Alexei.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-03-07 14:55:35 -0800 (Thu, 07 Mar 2002)
Revision: 3529
Log message:

      Fixing a lable problem noticed by Yegor.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-07 15:13:10 -0800 (Thu, 07 Mar 2002)
Revision: 3530
Log message:

      1. Added properties that "e * a = a * e" and "a * e = e * a".
      2. Changed the definition of groups to one-sided (left) definition,
         i.e., groups are defined by the left axioms, and proved the right
         axioms.
      3. Removed the introduction forms of group cancellation laws which
         were put in comments in the last version.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-03-09 23:50:56 -0800 (Sat, 09 Mar 2002)
Revision: 3531
Log message:

      Modify my TODO file so that I actually remember
      what I need to do, for when I finally get around
      to having time to work on it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-03-10 15:29:54 -0800 (Sun, 10 Mar 2002)
Revision: 3532
Log message:

      I am committing David Bustos' changes to the cons build system for Metaprl.
      
      See David's message "cons for MetaPRL" in the newsgroup for more information -
      news://news.metaprl.org:119/20020310131332.A13595@wink.caltech.edu
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-03-11 01:54:10 -0800 (Mon, 11 Mar 2002)
Revision: 3533
Log message:

      I've renamed theories/mc/fir_eval to use my
      (attrocious) prefix so that a file name collision
      with fir_eval in the MC source tree doesn't happen.
      Other files in theories/mc have been changed
      accordingly.
      
      I've renamed mp_mc_theory to just use a .mlz
      file since the .ml and .mli files were the
      exact same and it's a hassle to modify them
      both whenever they need to be changed.
      
      I've updated editor/ml/Conscript so that mpopt
      actually includes the Itt_theory and Mp_mc_theory.
      This makes it much more useful.
      
      mc/Conscript has been updated to reflect new code
      in the MC source tree.
      
      After this, MetaPRL should compile with the
      main trunk of the MC source tree if the MC_ROOT
      environment variable is set appropriately.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 01:57:12 -0800 (Mon, 11 Mar 2002)
Revision: 3534
Log message:

      1. Minor changes in the introduction rule for equivalence relations;
      2. Added tactics "equivSym1T" and "equivTrans1T" for the symmetry and
         transitivity of equivalence relations which are supposed to be
         applied to goals while "equivSymT" and "equivTransT" in the previous
         versions are supposed to be applied to hypotheses;
      3. Added the property that if 'a = 'b then 'a is equivalent to 'b under
         any equivalence relation;
      4. Added in comments the property that if 'a is equivalent to 'b under
         any equivalence relation then 'a = 'b. (This is not proved since I
         don't know how to express the set
         {(a, b): mem{'a; 's}, mem{'b; 's}, equal{'a; 'b}}.)
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 01:57:39 -0800 (Mon, 11 Mar 2002)
Revision: 3535
Log message:

      Added the elimination form of the unique inverse rule.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 01:58:58 -0800 (Mon, 11 Mar 2002)
Revision: 3536
Log message:

      1. Changed the definition of subgroup{'g; 's}; 's is now a "label"
         instead of a "set". In the previous version, it is really hard to
         show that a subgroup is also a group. Now subgroup{'g; 's} is a
         subgroup iff 'g is a group, 's is a group, the carrier set of 's
         is a subset of that of 'g, and they have the same operators;
      2. Rules updated and proved;
      3. Added tactic "subgroupIsectT".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 02:03:46 -0800 (Mon, 11 Mar 2002)
Revision: 3537
Log message:

      1. Changed the definition of cyclic subgroups from cyclic_subgroup{'g;
         'a} to cyc_subg{'g; 's; 'a} where 's was added to represent the group
         of the cyclic_subgroup itself;
      2. Added the functionality (both equality and equivalence) of the "power"
         operation;
      3. Updated the properties of the power operation from "equal" to "equiv";
      4. Updated and proved rules about cyclic subgroups;
      5. Added tactic "cycsubgSubgroupT".
      
      Problem:
        czf_itt_cyclic_subgroup.prla could not be committed. It gave the message
         "cvs server: sticky tag `1.5' for file `czf_itt_cyclic_subgroup.prla'
          is not a branch".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 02:04:22 -0800 (Mon, 11 Mar 2002)
Revision: 3538
Log message:

      1. Changed the definition of cyclic groups from cyclic_group{'g;'a}
         which represented the carrier set of the cyclic group to
         cycgroup{'g; 'a} which is a "type" and can be rewritted as
         cyc_subg{'g; 'g; 'a};
      2. Updated and proved rules about cyclic groups;
      3. Added tactic "cycgroupAbelT".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 02:35:54 -0800 (Mon, 11 Mar 2002)
Revision: 3539
Log message:

      This completes the committion of czf_itt_cyclic_subgroup.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-03-11 08:03:51 -0800 (Mon, 11 Mar 2002)
Revision: 3540
Log message:

      Updated theories/mc/Makefile to
      reflect new file names (oops!).
      Changed editor/ml/Conscript to use a more
      appropriate mechanism for declaring the
      hidden dependencies of mpopt.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-03-14 13:25:51 -0800 (Thu, 14 Mar 2002)
Revision: 3541
Log message:

      Added a "favicon" to default.html install.html (Mozilla-only since IE wants them to be .ico)
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-03-21 10:55:45 -0800 (Thu, 21 Mar 2002)
Revision: 3542
Log message:

      Arithmetic relations in conclusion is also processed now.
      TODO:
      - "bug"(a>=b & a<b) still here but I know why it is happening
      - resources! I finally realized what to do with it!
      - not_equal support
      - multiplication support
      - negation (not a<b) support but I'm not sure
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-23 23:22:12 -0800 (Sat, 23 Mar 2002)
Revision: 3543
Log message:

        Added and proved the rule for the property "if a is equivalent to b
        under any equivalence relation, then a is equal to b". It is proved
        by the use of "set builder" defined in Czf_itt_set_bvd.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-23 23:43:47 -0800 (Sat, 23 Mar 2002)
Revision: 3544
Log message:

      Changed the definition of abelian groups completely. An abelian
      group is now defined under equivalence relations instead of equality
      relations, and there is a reduction rule for it.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-23 23:54:36 -0800 (Sat, 23 Mar 2002)
Revision: 3545
Log message:

      Added the definition for "set builder", i.e., the image of a set s
      under some function f: { f(x) | x in s }. I consider this as a necessity
      for the set theory.
      
      The "set builder" is defined by a "set-induction" rewrite rule. Also
      added and proved properties for it.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-24 00:21:13 -0800 (Sun, 24 Mar 2002)
Revision: 3546
Log message:

      Added the module for the inverse image of set t in set s under function f:
         { x in s | f(x) in t }
      
      I didn't find a direct way to define it, so I define it using axioms.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-24 00:26:30 -0800 (Sun, 24 Mar 2002)
Revision: 3547
Log message:

      Defined homomorphism for groups. A map f of a group G into a group G'
      is a homomorphism if f(a * b) = f(a) * f(b).
      
      Proved some properties of homomorphism with the definition.
      
      Since I would redo groups soon, this homomorphism file is not complete.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-24 00:29:36 -0800 (Sun, 24 Mar 2002)
Revision: 3548
Log message:

      Updated to reflect new file names.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-24 03:01:50 -0800 (Sun, 24 Mar 2002)
Revision: 3549
Log message:

      1. The original equivTransT was wrong. Changed the original equivTrans1T
         and equivSym1T into equivTransT and equivSymT; Changed the original
         equivSymT to equivSym1T and removed equivTrans1T.
      2. Added the "fold" form for "equiv".
      3. Reproved rules in the file.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-03-24 14:35:29 -0800 (Sun, 24 Mar 2002)
Revision: 3550
Log message:

      Updating files to reflect the newest version of the MC FIR (which happens to be
      in the websplit branch).  In the process, I've also moved every file in this
      theory to use the same prefix for the filenames. I've also removed quite
      a few files that have been dead for a while now.
      
      Right now, the "connect" files are not compiled in by default since they will
      only compile against the websplit branch of MC and not the trunk.
      
      Lastly, since the definition of FIR evaluation is a bit more precise now,
      the need to seperately define constant elimination has been removed.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-03-30 18:48:35 -0800 (Sat, 30 Mar 2002)
Revision: 3551
Log message:

      Test cases for the "connection" code are pretty much complete.
      I've fixed a few bugs that cropped up (including a major one
      in Mp_mc_term_op).  What's needed now is the final set of functions
      to take an entire MC Fir.prog to some sort of MetaPRL term.