/[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 3570 - (show annotations) (download)
Tue Apr 9 05:59:41 2002 UTC (19 years, 3 months ago) by xiny
File size: 1021 byte(s)
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. They look much cleaner now.
Also updated related rules and their proofs.

1 include Czf_itt_group
2 include Czf_itt_group_bvd
3 include Czf_itt_subgroup
4 include Itt_int_base
5
6 open Printf
7 open Mp_debug
8 open Refiner.Refiner.TermType
9 open Refiner.Refiner.Term
10 open Refiner.Refiner.TermOp
11 open Refiner.Refiner.TermAddr
12 open Refiner.Refiner.TermMan
13 open Refiner.Refiner.TermSubst
14 open Refiner.Refiner.Refine
15 open Refiner.Refiner.RefineError
16 open Mp_resource
17 open Simple_print
18
19 open Tactic_type
20 open Tactic_type.Tacticals
21 open Tactic_type.Sequent
22 open Tactic_type.Conversionals
23 open Mptop
24 open Var
25
26 open Base_dtactic
27 open Base_auto_tactic
28
29 declare power{'g; 'z; 'n}
30 declare cyc_subg{'s; 'g; 'a}
31
32 rewrite unfold_power : power{'g; 'z; 'n} <-->
33 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)}}}
34
35 rewrite unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->
36 (group{'s} & group{'g} & mem{'a; car{'g}} & group_bvd{'s; 'g; collect{int; x. power{'g; 'a; 'x}}})
37
38 topval fold_power : conv
39 topval fold_cyc_subg : conv
40 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