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

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

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_subgroup
3  include Czf_itt_abel_group  include Czf_itt_abel_group
4    include Czf_itt_equiv
5    include Czf_itt_group_bvd
6    include Czf_itt_set_bvd
7    include Czf_itt_inv_image
8    include Czf_itt_coset
9    include Czf_itt_normal_subgroup
10    
11  open Printf  open Printf
12  open Mp_debug  open Mp_debug
# Line 27  Line 32 
32  open Base_auto_tactic  open Base_auto_tactic
33    
34  declare hom{'g1; 'g2; x. 'f['x]}  declare hom{'g1; 'g2; x. 'f['x]}
35    declare kernel{'h; 'g1; 'g2; x. 'f['x]}
36    
37  dform hom_df : parens :: except_mode[src] :: hom{'g1; 'g2; x. 'f} =  dform hom_df : parens :: except_mode[src] :: hom{'g1; 'g2; x. 'f} =
38     `"hom(" slot{'g1} `"; " slot{'g2} `"; " slot{'f} `")"     `"hom(" slot{'g1} `"; " slot{'g2} `"; " slot{'f} `")"
39    
40    dform kernel_df : parens :: except_mode[src] :: kernel{'h; 'g1; 'g2; x. 'f} =
41       `"kernel(" slot{'h} `"; " slot{'g1} `"; " slot{'g2} `"; " slot{'f} `")"
42    
43  (*  (*
44   * g1 and g2 are groups; f is a map of g1 into g2;   * g1 and g2 are groups; f is a map of g1 into g2;
45   * and for all a, b in g1, f(a * b) = f(a) * f(b).   * and for all a, b in g1, f(a * b) = f(a) * f(b).
# Line 38  Line 47 
47  prim_rw unfold_hom : hom{'g1; 'g2; x. 'f['x]} <-->  prim_rw unfold_hom : hom{'g1; 'g2; x. 'f['x]} <-->
48     (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]}})))
49    
50    (*
51     * f is a homomorphism of g1 into g2. The elements of g1,
52     * which are mapped into the identity of g2, form a subgroup
53     * h of g called the kernel of f.
54     *)
55    prim_rw unfold_kernel : kernel{'h; 'g1; 'g2; x. 'f['x]} <-->
56       (hom{'g1; 'g2; x. 'f['x]} & group_bvd{'h; 'g1; setbvd_prop{car{'g1}; x. equiv{car{'g2}; eqG{'g2}; 'f['x]; id{'g2}}}})
57    
58  interactive hom_type {| intro [] |} 'H :  interactive hom_type {| intro [] |} 'H :
59     sequent [squash] { 'H >- 'g1 IN label } -->     sequent [squash] { 'H >- 'g1 IN label } -->
60     sequent [squash] { 'H >- 'g2 IN label } -->     sequent [squash] { 'H >- 'g2 IN label } -->
# Line 146  Line 163 
163  let homInvT t i p =  let homInvT t i p =
164     let j, k = Sequent.hyp_indices p i in     let j, k = Sequent.hyp_indices p i in
165        hom_inv_elim j k t p        hom_inv_elim j k t p
166    
167    (*
168     * Let f: G -> G' be a group homomorphism of G into G'.
169     * If H is a subgroup of G, then f[H] is a subgroup of G'.
170     *)
171    interactive hom_subgroup1 'H hom{'g1; 'g2; x. 'f['x]} 'h1 'h2 :
172       sequent [squash] { 'H >- 'g1 IN label } -->
173       sequent [squash] { 'H >- 'g2 IN label } -->
174       sequent [squash] { 'H >- 'h1 IN label } -->
175       sequent [squash] { 'H >- 'h2 IN label } -->
176       sequent ['ext] { 'H >- group{'h2} } -->
177       sequent ['ext] { 'H >- fun_set{x. 'f['x]} } -->
178       sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} } -->
179       sequent ['ext] { 'H >- subgroup{'h1; 'g1} } -->
180       sequent ['ext] { 'H >- group_bvd{'h2; 'g2; set_bvd{car{'h1}; x. 'f['x]}} } -->
181       sequent ['ext] { 'H >- subgroup{'h2; 'g2} }
182    
183    (*
184     * Let f: G -> G' be a group homomorphism of G into G'.
185     * If H is a subgroup of G', then the inverse image of
186     * H is a subgroup of G.
187     *)
188    interactive hom_subgroup2 'H hom{'g1; 'g2; x. 'f['x]} 'h1 'h2 :
189       sequent [squash] { 'H >- 'g1 IN label } -->
190       sequent [squash] { 'H >- 'g2 IN label } -->
191       sequent [squash] { 'H >- 'h1 IN label } -->
192       sequent [squash] { 'H >- 'h2 IN label } -->
193       sequent ['ext] { 'H >- group{'h1} } -->
194       sequent ['ext] { 'H >- fun_set{x. 'f['x]} } -->
195       sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} } -->
196       sequent ['ext] { 'H >- subgroup{'h2; 'g2} } -->
197       sequent ['ext] { 'H >- group_bvd{'h1; 'g1; inv_image{car{'g1}; x. 'f['x]; car{'h2}}} } -->
198       sequent ['ext] { 'H >- subgroup{'h1; 'g1} }
199    
200    (*
201     * Properties for kernels.
202     *)
203    interactive kernel_type {| intro [] |} 'H :
204       sequent [squash] { 'H >- 'g1 IN label } -->
205       sequent [squash] { 'H >- 'g2 IN label } -->
206       sequent [squash] { 'H >- 'h IN label } -->
207       sequent [squash] { 'H; x: set >- isset{'f['x]} } -->
208       sequent ['ext] { 'H >- "type"{kernel{'h; 'g1; 'g2; x. 'f['x]}} }
209    
210    interactive kernel_intro {| intro [] |} 'H :
211       sequent [squash] { 'H >- 'g1 IN label } -->
212       sequent [squash] { 'H >- 'g2 IN label } -->
213       sequent [squash] { 'H >- 'h IN label } -->
214       sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} } -->
215       sequent ['ext] { 'H >- group_bvd{'h; 'g1; setbvd_prop{car{'g1}; x. equiv{car{'g2}; eqG{'g2}; 'f['x]; id{'g2}}}} } -->
216       sequent ['ext] { 'H >- kernel{'h; 'g1; 'g2; x. 'f['x]} }
217    
218    (*
219     * Let f: G -> G' be a group homomorphism of G into G'.
220     * The kernel of f is a subgroup of G.
221     *)
222    interactive kernel_subgroup 'H hom{'g1; 'g2; x. 'f['x]} 'h :
223       sequent [squash] { 'H >- 'g1 IN label } -->
224       sequent [squash] { 'H >- 'g2 IN label } -->
225       sequent [squash] { 'H >- 'h IN label } -->
226       sequent ['ext] { 'H >- kernel{'h; 'g1; 'g2; x. 'f['x]} } -->
227       sequent ['ext] { 'H >- fun_set{x. 'f['x]} } -->
228       sequent ['ext] { 'H >- subgroup{'h; 'g1} }
229    
230    interactive kernel_subgroup_elim (*{| elim [] |}*) 'H 'J :
231       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g1 IN label } -->
232       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g2 IN label } -->
233       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'h IN label } -->
234       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- fun_set{x. 'f['x]} } -->
235       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u]; v: subgroup{'h; 'g1} >- 'C['u] } -->
236       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'C['u] }
237    
238    let kernelSubgroupT i p =
239       let j, k = Sequent.hyp_indices p i in
240          kernel_subgroup_elim j k p
241    
242    (*
243     * Let f: G1 -> G2 be a group homomorphism of G1 into G2.
244     * Let H be the kernel of f. For any a in G1, the set
245     * { x in G1 | f(x) = f(a) } is the left coset aH of H.
246     *)
247    interactive kernel_lcoset {| intro [] |} 'H :
248       sequent [squash] { 'H >- 'g1 IN label } -->
249       sequent [squash] { 'H >- 'g2 IN label } -->
250       sequent [squash] { 'H >- 'h IN label } -->
251       sequent [squash] { 'H >- isset{'a} } -->
252       sequent ['ext] { 'H >- mem{'a; car{'g1}} } -->
253       sequent ['ext] { 'H >- fun_set{x. 'f['x]} } -->
254       sequent ['ext] { 'H >- kernel{'h; 'g1; 'g2; x. 'f['x]} } -->
255       sequent ['ext] { 'H >- equal{setbvd_prop{car{'g1}; x. equiv{car{'g2}; eqG{'g2}; 'f['x]; 'f['a]}}; lcoset{'h; 'g1; 'a}} }
256    
257    interactive kernel_lcoset1 (*{| elim [] |}*) 'H 'J 'a :
258       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g1 IN label } -->
259       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g2 IN label } -->
260       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'h IN label } -->
261       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- isset{'a} } -->
262       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- mem{'a; car{'g1}} } -->
263       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- fun_set{x. 'f['x]} } -->
264       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u]; v: equal{setbvd_prop{car{'g1}; x. equiv{car{'g2}; eqG{'g2}; 'f['x]; 'f['a]}}; lcoset{'h; 'g1; 'a}} >- 'C['u] } -->
265       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'C['u] }
266    
267    let kernelLcosetT t i p =
268       let j, k = Sequent.hyp_indices p i in
269          kernel_lcoset1 j k t p
270    
271    (*
272     * Let f: G1 -> G2 be a group homomorphism of G1 into G2.
273     * Let H be the kernel of f. For any a in G1, the set
274     * { x in G1 | f(x) = f(a) } is also the right coset Ha of H.
275     *)
276    interactive kernel_rcoset {| intro [] |} 'H :
277       sequent [squash] { 'H >- 'g1 IN label } -->
278       sequent [squash] { 'H >- 'g2 IN label } -->
279       sequent [squash] { 'H >- 'h IN label } -->
280       sequent [squash] { 'H >- isset{'a} } -->
281       sequent ['ext] { 'H >- mem{'a; car{'g1}} } -->
282       sequent ['ext] { 'H >- fun_set{x. 'f['x]} } -->
283       sequent ['ext] { 'H >- kernel{'h; 'g1; 'g2; x. 'f['x]} } -->
284       sequent ['ext] { 'H >- equal{setbvd_prop{car{'g1}; x. equiv{car{'g2}; eqG{'g2}; 'f['x]; 'f['a]}}; rcoset{'h; 'g1; 'a}} }
285    
286    interactive kernel_rcoset1 (*{| elim [] |}*) 'H 'J 'a :
287       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g1 IN label } -->
288       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g2 IN label } -->
289       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'h IN label } -->
290       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- isset{'a} } -->
291       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- mem{'a; car{'g1}} } -->
292       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- fun_set{x. 'f['x]} } -->
293       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u]; v: equal{setbvd_prop{car{'g1}; x. equiv{car{'g2}; eqG{'g2}; 'f['x]; 'f['a]}}; rcoset{'h; 'g1; 'a}} >- 'C['u] } -->
294       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'C['u] }
295    
296    let kernelRcosetT t i p =
297       let j, k = Sequent.hyp_indices p i in
298          kernel_rcoset1 j k t p
299    
300    (*
301     * A group homomorphism f: G1 -> G2 is a one-to-one map
302     * if and only if Ker(f) = {id(g1)}.
303     *)
304    interactive kernel_injection1 (*{| elim [] |}*) 'H 'J :
305       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g1 IN label } -->
306       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g2 IN label } -->
307       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'h IN label } -->
308       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- fun_set{x. 'f['x]} } -->
309       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- equal{car{'h}; setbvd_prop{car{'g1}; x. equiv{car{'g1}; eqG{'g1}; 'x; id{'g1}}}} } -->
310       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- all c: set.all d: set. (mem{'c; car{'g1}} => mem{'d; car{'g1}} => equiv{car{'g2}; eqG{'g2}; 'f['c]; 'f['d]} => equiv{car{'g1}; eqG{'g1}; 'c; 'd}) }
311    
312    interactive kernel_injection2 (*{| elim [] |}*) 'H 'J :
313       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g1 IN label } -->
314       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g2 IN label } -->
315       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'h IN label } -->
316       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- fun_set{x. 'f['x]} } -->
317       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u]; c: set; d: set; u: mem{'c; car{'g1}}; v: mem{'d; car{'g1}}; w: equiv{car{'g2}; eqG{'g2}; 'f['c]; 'f['d]} >- equiv{car{'g1}; eqG{'g1}; 'c; 'd} } -->
318       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- equal{car{'h}; setbvd_prop{car{'g1}; x. equiv{car{'g1}; eqG{'g1}; 'x; id{'g1}}}} }
319    
320    (*
321     * The kernel of a homomorphism f: G1 -> G2 is a normal subgroup of G1.
322     *)
323    interactive kernel_normalSubg (*{| elim [] |}*) 'H 'J :
324       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g1 IN label } -->
325       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g2 IN label } -->
326       sequent [squash] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'h IN label } -->
327       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- fun_set{x. 'f['x]} } -->
328       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u]; v: normal_subg{'h; 'g1} >- 'C['u] } -->
329       sequent ['ext] { 'H; u: kernel{'h; 'g1; 'g2; x. 'f['x]}; 'J['u] >- 'C['u] }
330    
331    let kernelNormalSubgT i p =
332       let j, k = Sequent.hyp_indices p i in
333          kernel_normalSubg j k p

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

  ViewVC Help
Powered by ViewVC 1.1.26