/[mojave]/metaprl/theories/czf/czf_itt_subgroup.prla
ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_subgroup.prla

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3570 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 9 05:59:41 2002 UTC (19 years, 2 months ago) by xiny
File length: 106885 byte(s)
Diff to previous 3560
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. They look much cleaner now.
Also updated related rules and their proofs.


Revision 3560 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 3 05:27:01 2002 UTC (19 years, 2 months ago) by xiny
File length: 98550 byte(s)
Diff to previous 3556
Changed the definition of subgroups; fixed the errors in defining the
operation and equivalence relation for subgroups.


Revision 3556 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 08:08:36 2002 UTC (19 years, 2 months ago) by xiny
File length: 84360 byte(s)
Diff to previous 3536
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.


Revision 3536 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 09:58:58 2002 UTC (19 years, 3 months ago) by xiny
File length: 79666 byte(s)
Diff to previous 3504
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".


Revision 3504 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 21 07:56:36 2002 UTC (19 years, 4 months ago) by xiny
File length: 65057 byte(s)
Diff to previous 3501
Redefined subgroups. Now subgroup{'g; 's} is a "type" where 's is the
underlying set for the subgroup and it is no longer defined by axioms,
but by introduction and elimination rules which make the descriptions
and proving of subgroup-related properties more straight-forward.


Revision 3501 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 19 03:44:19 2002 UTC (19 years, 4 months ago) by xiny
File length: 38745 byte(s)
Diff to previous 3490
Changed the definition of subgroups to subgroup{'g; 's} where 'g, 's,
and subgroup{'g; 's} are all labels.
Proved the properties of subgroups with this definition.

TODO:
   I would adopt another definition of subgroups where 's is a "set"
   and subgroup{'g; 's} is a "type".


Revision 3490 - (view) (download) (annotate) - [select for diffs]
Modified Sat Feb 2 07:13:21 2002 UTC (19 years, 4 months ago) by xiny
File length: 39860 byte(s)
Diff to previous 3405
Added and proved complicated properties of subgroups.


Revision 3405 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 23 07:33:50 2001 UTC (19 years, 9 months ago) by xiny
File length: 24610 byte(s)
Diff to previous 3404
recommit .prla files


Revision 3404 - (view) (download) (annotate) - [select for diffs]
Added Sun Sep 23 07:25:28 2001 UTC (19 years, 9 months ago) by xiny
File length: 24618 byte(s)
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.


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