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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3570 - (hide 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 xiny 3404 include Czf_itt_group
2 xiny 3570 include Czf_itt_group_bvd
3 xiny 3404 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 xiny 3502 declare power{'g; 'z; 'n}
30 xiny 3557 declare cyc_subg{'s; 'g; 'a}
31 xiny 3404
32 xiny 3502 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 xiny 3487
35 xiny 3557 rewrite unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->
36 xiny 3570 (group{'s} & group{'g} & mem{'a; car{'g}} & group_bvd{'s; 'g; collect{int; x. power{'g; 'a; 'x}}})
37 xiny 3404
38     topval fold_power : conv
39 xiny 3537 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