Parent Directory | Revision Log
Links to HEAD: | (view) (download) (annotate) |
Sticky Revision: |
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.
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".
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.
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".
Added and proved complicated properties of subgroups.
recommit .prla files
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.
ViewVC Help | |
Powered by ViewVC 1.1.26 |