/[mojave]/metaprl/theories/czf/czf_itt_group.ml
ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_group.ml

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3553 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 07:45:26 2002 UTC (19 years, 2 months ago) by xiny
File length: 19437 byte(s)
Diff to previous 3535
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.


Revision 3535 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 09:57:39 2002 UTC (19 years, 3 months ago) by xiny
File length: 19834 byte(s)
Diff to previous 3530
Added the elimination form of the unique inverse rule.


Revision 3530 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 7 23:13:10 2002 UTC (19 years, 3 months ago) by xiny
File length: 18736 byte(s)
Diff to previous 3527
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.


Revision 3527 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 4 02:20:01 2002 UTC (19 years, 3 months ago) by xiny
File length: 18703 byte(s)
Diff to previous 3516
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.


Revision 3516 - (view) (download) (annotate) - [select for diffs]
Modified Mon Feb 25 02:24:42 2002 UTC (19 years, 4 months ago) by xiny
File length: 32769 byte(s)
Diff to previous 3498
Replaced equality relations with equivalence relations everywhere in the
context of groups, and re-proved the rules.


Revision 3498 - (view) (download) (annotate) - [select for diffs]
Modified Sun Feb 17 02:09:08 2002 UTC (19 years, 4 months ago) by xiny
File length: 11780 byte(s)
Diff to previous 3494
Changed the definition of groups completely.
The former version is awkward for defining specific groups like
<Z, +> and is lack of generality since only ONE general group is
defined.
The current version adopts a parameter which makes it capable of
handling complicated situations.


Revision 3494 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 7 23:19:33 2002 UTC (19 years, 4 months ago) by xiny
File length: 8337 byte(s)
Diff to previous 3485
Removed tactics "op_assoc1T", "op_assoc2T" (previously as comments),
and "id_elim2T".


Revision 3485 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 30 00:42:11 2002 UTC (19 years, 4 months ago) by xiny
File length: 8530 byte(s)
Diff to previous 3484
Removing some comments.


Revision 3484 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 30 00:36:09 2002 UTC (19 years, 4 months ago) by xiny
File length: 8947 byte(s)
Diff to previous 3404
Now a workable version for groups and cyclic subgroups. Rules proved, examples  added.
Problems left:
   The proofs for rules "power_property1", "power_property2", and "power_simplify" are not yet finished because of some itt problems.


Revision 3404 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 23 07:25:28 2001 UTC (19 years, 9 months ago) by xiny
File length: 8682 byte(s)
Diff to previous 3379
1. Minor changes in czf_itt_group;
2. Define subgroup and abelian group;
3. Define cyclic subgroup and cyclic group. However, there are
   problems with the proofs in czf_itt_cyclic_subgroup.


Revision 3379 - (view) (download) (annotate) - [select for diffs]
Added Fri Sep 14 07:00:13 2001 UTC (19 years, 9 months ago) by xiny
File length: 7800 byte(s)
Definition of algebraic group.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26