ViewVC logotype

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

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: 617 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: 922 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: 767 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.

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: 669 byte(s)
Diff to previous 3501
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 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: 165 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.

   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: 157 byte(s)
Diff to previous 3404
Added and proved complicated properties of subgroups.

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: 112 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