/[mojave]/metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
ViewVC logotype

Contents of /metaprl/theories/czf/czf_itt_cyclic_subgroup.mli

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3561 - (show annotations) (download)
Wed Apr 3 05:29:19 2002 UTC (19 years, 4 months ago) by xiny
File size: 1351 byte(s)
Changed the definition of cyclic subgroups; fixed the previous error in
defining the operation and equivalence relation for cyclic subgroups.
Updated related rules.

1 include Czf_itt_group
2 include Czf_itt_subgroup
3 include Itt_int_base
4
5 open Printf
6 open Mp_debug
7 open Refiner.Refiner.TermType
8 open Refiner.Refiner.Term
9 open Refiner.Refiner.TermOp
10 open Refiner.Refiner.TermAddr
11 open Refiner.Refiner.TermMan
12 open Refiner.Refiner.TermSubst
13 open Refiner.Refiner.Refine
14 open Refiner.Refiner.RefineError
15 open Mp_resource
16 open Simple_print
17
18 open Tactic_type
19 open Tactic_type.Tacticals
20 open Tactic_type.Sequent
21 open Tactic_type.Conversionals
22 open Mptop
23 open Var
24
25 open Base_dtactic
26 open Base_auto_tactic
27
28 declare power{'g; 'z; 'n}
29 declare cyc_subg{'s; 'g; 'a}
30
31 rewrite unfold_power : power{'g; 'z; 'n} <-->
32 ind{'n; i, j. op{'g; inv{'g; 'z}; power{'g; 'z; ('n +@ 1)}}; id{'g}; k, l. op{'g; 'z; power{'g; 'z; ('n -@ 1)}}}
33
34 rewrite unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->
35 (group{'s} & group{'g} & mem{'a; car{'g}} & equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} & (all b: set. all c: set. (mem{'b; car{'s}} => mem{'c; car{'s}} => equiv{car{'s}; eqG{'s}; op{'s; 'b; 'c}; op{'g; 'b; 'c}})) & (all b: set. all c: set. (equiv{car{'s}; eqG{'s}; 'b; 'c} => equiv{car{'g}; eqG{'g}; 'b; 'c})) & (all b: set. all c:set. (mem{'b; car{'s}} => mem{'c; car{'s}} => equiv{car{'g}; eqG{'g}; 'b; 'c} => equiv{car{'s}; eqG{'s}; 'b; 'c})))
36
37 topval fold_power : conv
38 topval fold_cyc_subg : conv
39 topval cycsubgSubgroupT: term -> tactic

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26