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

Diff of /metaprl/theories/czf/czf_itt_hom.mli

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3572 by xiny, Tue Apr 2 08:46:33 2002 UTC revision 3573 by xiny, Tue Apr 9 06:02:02 2002 UTC
# Line 1  Line 1 
 include Czf_itt_set  
1  include Czf_itt_group  include Czf_itt_group
2  include Czf_itt_equiv  include Czf_itt_equiv
3    include Czf_itt_group_bvd
4    include Czf_itt_set_bvd
5    
6  open Printf  open Printf
7  open Mp_debug  open Mp_debug
# Line 25  Line 26 
26  open Base_auto_tactic  open Base_auto_tactic
27    
28  declare hom{'g1; 'g2; x. 'f['x]}  declare hom{'g1; 'g2; x. 'f['x]}
29    declare kernel{'h; 'g1; 'g2; x. 'f['x]}
30    
31  rewrite unfold_hom : hom{'g1; 'g2; x. 'f['x]} <-->  rewrite unfold_hom : hom{'g1; 'g2; x. 'f['x]} <-->
32     (group{'g1} & group{'g2} & (all a: set. (mem{'a; car{'g1}} => mem{'f['a]; car{'g2}})) & (all a: set. all b: set. (mem{'a; car{'g1}} => mem{'b; car{'g1}} => equiv{car{'g1}; eqG{'g1}; 'a; 'b} => equiv{car{'g2}; eqG{'g2}; 'f['a]; 'f['b]})) & (all a: set. all b: set. (mem{'a; car{'g1}} => mem{'b; car{'g1}} => equiv{car{'g2}; eqG{'g2}; 'f[op{'g1; 'a; 'b}]; op{'g2; 'f['a]; 'f['b]}})))     (group{'g1} & group{'g2} & (all a: set. (mem{'a; car{'g1}} => mem{'f['a]; car{'g2}})) & (all a: set. all b: set. (mem{'a; car{'g1}} => mem{'b; car{'g1}} => equiv{car{'g1}; eqG{'g1}; 'a; 'b} => equiv{car{'g2}; eqG{'g2}; 'f['a]; 'f['b]})) & (all a: set. all b: set. (mem{'a; car{'g1}} => mem{'b; car{'g1}} => equiv{car{'g2}; eqG{'g2}; 'f[op{'g1; 'a; 'b}]; op{'g2; 'f['a]; 'f['b]}})))
33    
34    rewrite unfold_kernel : kernel{'h; 'g1; 'g2; x. 'f['x]} <-->
35       (hom{'g1; 'g2; x. 'f['x]} & group_bvd{'h; 'g1; setbvd_prop{car{'g1}; x. equiv{car{'g2}; eqG{'g2}; 'f['x]; id{'g2}}}})
36    
37  topval homIdT : int -> tactic  topval homIdT : int -> tactic
38  topval homInvT : term -> int -> tactic  topval homInvT : term -> int -> tactic
39    topval kernelSubgroupT : int -> tactic
40    topval kernelLcosetT : term -> int -> tactic
41    topval kernelRcosetT : term -> int -> tactic
42    topval kernelNormalSubgT : int -> tactic

Legend:
Removed from v.3572  
changed lines
  Added in v.3573

  ViewVC Help
Powered by ViewVC 1.1.26