/[mojave]/metaprl/theories/czf/czf_itt_cyclic_group.ml
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_cyclic_group.ml

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

revision 3557 by xiny, Mon Mar 11 10:04:22 2002 UTC revision 3558 by xiny, Tue Apr 2 08:27:06 2002 UTC
# Line 1  Line 1 
1  include Czf_itt_equiv  include Czf_itt_equiv
2  include Czf_itt_group  include Czf_itt_group
3  include Czf_itt_cyclic_subgroup  include Czf_itt_cyclic_subgroup
4  include Czf_itt_subgroup  include Czf_itt_abel_group
 include Czf_itt_subset  
 include Itt_logic  
5    
6  open Printf  open Printf
7  open Mp_debug  open Mp_debug
# Line 31  Line 29 
29  declare cycgroup{'g; 'a}  declare cycgroup{'g; 'a}
30    
31  prim_rw unfold_cycgroup : cycgroup{'g; 'a} <-->  prim_rw unfold_cycgroup : cycgroup{'g; 'a} <-->
32     cyc_subg{'g; 'g; 'a}     (group{'g} & mem{'a; car{'g}} & equal{car{'g}; collect{int; x. power{'g; 'a; 'x}}})
33    
34  let fold_cycgroup = makeFoldC << cycgroup{'g; 'a} >> unfold_cycgroup  let fold_cycgroup = makeFoldC << cycgroup{'g; 'a} >> unfold_cycgroup
35    
# Line 40  Line 38 
38    
39  interactive cycgroup_wf {| intro [] |} 'H :  interactive cycgroup_wf {| intro [] |} 'H :
40     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
    sequent ['ext] { 'H >- group{'g} } -->  
41     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
    sequent ['ext] { 'H >- mem{'a; car{'g}} } -->  
42     sequent ['ext] { 'H >- "type"{cycgroup{'g; 'a}} }     sequent ['ext] { 'H >- "type"{cycgroup{'g; 'a}} }
43    
44  interactive cycgroup_intro {| intro [] |} 'H :  interactive cycgroup_intro {| intro [] |} 'H :
# Line 55  Line 51 
51    
52  (* Every cyclic group is abelian *)  (* Every cyclic group is abelian *)
53  interactive cycgroup_abel 'H 'a :  interactive cycgroup_abel 'H 'a :
    sequent [squash] { 'H >- isset{'R} } -->  
54     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
55     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
56     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
57     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
58     sequent ['ext] { 'H >- cycgroup{'g; 'a} } -->     sequent ['ext] { 'H >- cycgroup{'g; 'a} } -->
59     sequent [squash] { 'H >- isset{'s1} } -->     sequent ['ext] { 'H >- abel{'g} }
    sequent [squash] { 'H >- isset{'s2} } -->  
    sequent ['ext] { 'H >- mem{'s1; car{'g}} } -->  
    sequent ['ext] { 'H >- mem{'s2; car{'g}} } -->  
    sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; 's1; 's2}; op{'g; 's2; 's1}} }  
60    
61  let cycgroupAbelT t p =  let cycgroupAbelT t p =
62     cycgroup_abel (hyp_count_addr p) t p     cycgroup_abel (hyp_count_addr p) t p

Legend:
Removed from v.3557  
changed lines
  Added in v.3558

  ViewVC Help
Powered by ViewVC 1.1.26