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

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

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

revision 3556 by xiny, Mon Mar 11 10:03:46 2002 UTC revision 3557 by xiny, Tue Apr 2 08:18:40 2002 UTC
# Line 28  Line 28 
28  open Base_auto_tactic  open Base_auto_tactic
29    
30  declare power{'g; 'z; 'n}  declare power{'g; 'z; 'n}
31  declare cyc_subg{'g; 's; 'a}  declare cyc_subg{'s; 'g; 'a}
32    
33  prim_rw unfold_power : power{'g; 'z; 'n} <-->  prim_rw unfold_power : power{'g; 'z; 'n} <-->
34     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)}}}     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)}}}
35    
36  prim_rw unfold_cyc_subg : cyc_subg{'g; 's; 'a} <-->  prim_rw unfold_cyc_subg : cyc_subg{'s; 'g; 'a} <-->
37     (group{'g} & group{'s} & equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} & (all a: set. all b:set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equal{op{'s; 'a; 'b}; op{'g; 'a; 'b}})))     (group{'s} & group{'g} & mem{'a; car{'g}} & equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} & (all a: set. all b:set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equal{op{'s; 'a; 'b}; op{'g; 'a; 'b}})) & (all a: set. all b: set. (equiv{car{'s}; eqG{'s}; 'a; 'b} => equiv{car{'g}; eqG{'g}; 'a; 'b})))
38    
39  let fold_power = makeFoldC << power{'g; 'z; 'n} >> unfold_power  let fold_power = makeFoldC << power{'g; 'z; 'n} >> unfold_power
40  let fold_cyc_subg = makeFoldC << cyc_subg{'g; 's; 'a} >> unfold_cyc_subg  let fold_cyc_subg = makeFoldC << cyc_subg{'s; 'g; 'a} >> unfold_cyc_subg
41    
42  prec prec_power  dform power_df : parens :: except_mode[src] :: power{'g; 'z; 'n} =
   
 dform power_df : parens :: "prec"[prec_power] :: except_mode[src] :: power{'g; 'z; 'n} =  
43     `"power(" slot{'g} `"; " slot{'z}  `"; " slot{'n} `")"     `"power(" slot{'g} `"; " slot{'z}  `"; " slot{'n} `")"
44    
45  dform cyc_subg_df : except_mode[src] :: cyc_subg{'g; 's; 'a} =  dform cyc_subg_df : except_mode[src] :: cyc_subg{'s; 'g; 'a} =
46     `"cyclic_subgroup(" slot{'g} `"; " slot{'s} `"; " slot{'a} `")"     `"cyclic_subgroup(" slot{'s} `"; " slot{'g} `"; " slot{'a} `")"
47    
48  (*  (*
49   * Properties.   * Properties.
# Line 53  Line 51 
51  (* Power is a set *)  (* Power is a set *)
52  interactive power_wf1 {| intro [] |} 'H :  interactive power_wf1 {| intro [] |} 'H :
53     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
    sequent ['ext] { 'H >- group{'g} } -->  
    sequent [squash] { 'H >- 'n IN int } -->  
54     sequent [squash] { 'H >- isset{'z} } -->     sequent [squash] { 'H >- isset{'z} } -->
55     sequent ['ext] { 'H >- mem{'z; car{'g}} } -->     sequent [squash] { 'H >- 'n IN int } -->
56     sequent ['ext] { 'H >- isset{power{'g; 'z; 'n}} }     sequent ['ext] { 'H >- isset{power{'g; 'z; 'n}} }
57    
58  (* The power of an element in the carrier of a group is also in the carrier *)  (* The power of an element in the carrier of a group is also in the carrier *)
# Line 77  Line 73 
73     sequent ['ext] { 'H >- fun_set{z. power{'g; 'f['z]; 'n}} }     sequent ['ext] { 'H >- fun_set{z. power{'g; 'f['z]; 'n}} }
74    
75  interactive power_equiv_fun {| intro [] |} 'H :  interactive power_equiv_fun {| intro [] |} 'H :
    sequent [squash] { 'H >- isset{'R} } -->  
76     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
77     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
78     sequent [squash] { 'H >- 'n IN int } -->     sequent [squash] { 'H >- 'n IN int } -->
79     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv_fun_set{car{'g}; eqG{'g}; z. 'f['z]} } -->
80     sequent ['ext] { 'H >- equiv_fun_set{car{'g}; 'R; z. 'f['z]} } -->     sequent ['ext] { 'H >- equiv_fun_set{car{'g}; eqG{'g}; z. power{'g; 'f['z]; 'n}} }
    sequent ['ext] { 'H >- equiv_fun_set{car{'g}; 'R; z. power{'g; 'f['z]; 'n}} }  
81    
82  interactive power_equiv_fun1 {| intro [] |} 'H :  interactive power_equiv_fun1 {| intro [] |} 'H :
    sequent [squash] { 'H >- isset{'R} } -->  
83     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
84     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
85     sequent [squash] { 'H >- 'n IN int } -->     sequent [squash] { 'H >- 'n IN int } -->
86     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv_fun_set{car{'g}; eqG{'g}; z. power{'g; 'z; 'n}} }
    sequent ['ext] { 'H >- equiv_fun_set{car{'g}; 'R; z. power{'g; 'z; 'n}} }  
87    
88  (* x ^ (n + 1) * x ^ (-1) = x ^ n *)  (* x ^ (n + 1) * x ^ (-1) = x ^ n *)
89  interactive power_property1 {| intro [] |} 'H :  interactive power_property1 {| intro [] |} 'H :
    sequent [squash] { 'H >- isset{'R} } -->  
90     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
91     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
92     sequent [squash] { 'H >- 'n IN int } -->     sequent [squash] { 'H >- 'n IN int } -->
93     sequent [squash] { 'H >- isset{'x} } -->     sequent [squash] { 'H >- isset{'x} } -->
94     sequent ['ext] { 'H >- mem{'x; car{'g}} } -->     sequent ['ext] { 'H >- mem{'x; car{'g}} } -->
95     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; power{'g; 'x; ('n +@ 1)}; inv{'g; 'x}}; power{'g; 'x; 'n}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; power{'g; 'x; ('n +@ 1)}; inv{'g; 'x}}; power{'g; 'x; 'n}} }
96    
97  (* x ^ n * x = x ^ (n + 1) *)  (* x ^ n * x = x ^ (n + 1) *)
98  interactive power_property2 {| intro [] |} 'H :  interactive power_property2 {| intro [] |} 'H :
    sequent [squash] { 'H >- isset{'R} } -->  
99     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
100     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
101     sequent [squash] { 'H >- 'n IN int } -->     sequent [squash] { 'H >- 'n IN int } -->
102     sequent [squash] { 'H >- isset{'x} } -->     sequent [squash] { 'H >- isset{'x} } -->
103     sequent ['ext] { 'H >- mem{'x; car{'g}} } -->     sequent ['ext] { 'H >- mem{'x; car{'g}} } -->
104     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; power{'g; 'x; 'n}; 'x}; power{'g; 'x; ('n +@ 1)}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; power{'g; 'x; 'n}; 'x}; power{'g; 'x; ('n +@ 1)}} }
105    
106  (* Power simplify *)  (* Power simplify *)
107  interactive power_simplify {| intro [] |} 'H :  interactive power_simplify {| intro [] |} 'H :
    sequent [squash] { 'H >- isset{'R} } -->  
108     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
109     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
    sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->  
110     sequent [squash] { 'H >- 'm IN int } -->     sequent [squash] { 'H >- 'm IN int } -->
111     sequent [squash] { 'H >- 'n IN int } -->     sequent [squash] { 'H >- 'n IN int } -->
112     sequent [squash] { 'H >- isset{'x} } -->     sequent [squash] { 'H >- isset{'x} } -->
113     sequent ['ext] { 'H >- mem{'x; car{'g}} } -->     sequent ['ext] { 'H >- mem{'x; car{'g}} } -->
114     sequent ['ext] { 'H >- equiv{car{'g}; 'R; op{'g; power{'g; 'x; 'm}; power{'g; 'x; 'n}}; power{'g; 'x; ('m +@ 'n)}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; op{'g; power{'g; 'x; 'm}; power{'g; 'x; 'n}}; power{'g; 'x; ('m +@ 'n)}} }
115    
116  (* cyc_subg is a subgroup of G *)  (* cyc_subg is a subgroup of G *)
117  interactive cyc_subg_wf {| intro [] |} 'H :  interactive cyc_subg_wf {| intro [] |} 'H :
118     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
119     sequent [squash] { 'H >- 's IN label } -->     sequent [squash] { 'H >- 's IN label } -->
    sequent ['ext] { 'H >- group{'g} } -->  
    sequent ['ext] { 'H >- group{'s} } -->  
120     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
121     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- "type"{cyc_subg{'s; 'g; 'a}} }
    sequent ['ext] { 'H >- "type"{cyc_subg{'g; 's; 'a}} }  
122    
123  interactive cyc_subg_intro {| intro [] |} 'H :  interactive cyc_subg_intro {| intro [] |} 'H :
124     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
# Line 146  Line 129 
129     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
130     sequent ['ext] { 'H >- equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} } -->     sequent ['ext] { 'H >- equal{car{'s}; collect{int; x. power{'g; 'a; 'x}}} } -->
131     sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'s}}; y: mem{'b; car{'s}} >- equal{op{'s; 'a; 'b}; op{'g; 'a; 'b}} } -->     sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'s}}; y: mem{'b; car{'s}} >- equal{op{'s; 'a; 'b}; op{'g; 'a; 'b}} } -->
132     sequent ['ext] { 'H >- cyc_subg{'g; 's; 'a} }     sequent ['ext] { 'H; a: set; b: set; x: equiv{car{'s}; eqG{'s}; 'a; 'b} >- equiv{car{'g}; eqG{'g}; 'a; 'b} } -->
133       sequent ['ext] { 'H >- cyc_subg{'s; 'g; 'a} }
134    
135  interactive cyc_subg_subgroup 'H 'a :  interactive cyc_subg_subgroup 'H 'a :
136     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
# Line 155  Line 139 
139     sequent ['ext] { 'H >- group{'s} } -->     sequent ['ext] { 'H >- group{'s} } -->
140     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
141     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g}} } -->
142     sequent ['ext] { 'H >- cyc_subg{'g; 's; 'a} } -->     sequent ['ext] { 'H >- cyc_subg{'s; 'g; 'a} } -->
143     sequent ['ext] { 'H >- subgroup{'g; 's} }     sequent ['ext] { 'H >- subgroup{'s; 'g} }
144    
145  let cycsubgSubgroupT t p =  let cycsubgSubgroupT t p =
146     cyc_subg_subgroup (hyp_count_addr p) t p     cyc_subg_subgroup (hyp_count_addr p) t p

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

  ViewVC Help
Powered by ViewVC 1.1.26