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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

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: 3612 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: 3828 byte(s)
Diff to previous 3519
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 3519 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 26 20:21:12 2002 UTC (19 years, 3 months ago) by nogin
File length: 4944 byte(s)
Diff to previous 3504
String_util cleanup:

- Removed some duplicated and unused string code.
- Removed couple of functions from string_util that were added
to the stdlib String module in recent versions of Ocaml


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: 4958 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: 4041 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: 3193 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: 976 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