/[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 3558 by xiny, Sun Mar 24 08:26:30 2002 UTC revision 3559 by xiny, Tue Apr 2 08:46:33 2002 UTC
# Line 14  Line 14 
14  open Refiner.Refiner.Refine  open Refiner.Refiner.Refine
15  open Refiner.Refiner.RefineError  open Refiner.Refiner.RefineError
16  open Mp_resource  open Mp_resource
17    open Simple_print
18    
19  open Tactic_type  open Tactic_type
20  open Tactic_type.Tacticals  open Tactic_type.Tacticals
# Line 25  Line 26 
26  open Base_dtactic  open Base_dtactic
27  open Base_auto_tactic  open Base_auto_tactic
28    
29  declare hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]}  declare hom{'g1; 'g2; x. 'f['x]}
30    
31  dform hom_df : parens :: except_mode[src] :: hom{'g1; 'g2; 'r1; 'r2; x. 'f} =  dform hom_df : parens :: except_mode[src] :: hom{'g1; 'g2; x. 'f} =
32     `"hom(" slot{'g1} `"; " slot{'g2} `"; " slot{'r1} `"; " slot{'r2} `"; " slot{'f} `")"     `"hom(" slot{'g1} `"; " slot{'g2} `"; " slot{'f} `")"
33    
34  (*  (*
35   * g1 and g2 are groups; r1 and r2 are equivalence   * g1 and g2 are groups; f is a map of g1 into g2;
  * relations on g1 and g2; f is a map of g1 into g2;  
36   * 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).
37   *)   *)
38  prim_rw unfold_hom : hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} <-->  prim_rw unfold_hom : hom{'g1; 'g2; x. 'f['x]} <-->
39     (group{'g1} & group{'g2} & isset{'r1} & isset{'r2} & equiv{car{'g1}; 'r1} & equiv{car{'g2}; 'r2} & fun_set{x. 'f['x]} & "dall"{car{'g1}; a. mem{'f['a]; car{'g2}}} & (all a: set. all b: set. (mem{'a; car{'g1}} => mem{'b; car{'g1}} => equiv{car{'g2}; 'r2; '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]}})))
40    
41  interactive hom_type {| intro [] |} 'H :  interactive hom_type {| intro [] |} 'H :
42     sequent [squash] { 'H >- 'g1 IN label } -->     sequent [squash] { 'H >- 'g1 IN label } -->
43     sequent [squash] { 'H >- 'g2 IN label } -->     sequent [squash] { 'H >- 'g2 IN label } -->
    sequent ['ext] { 'H >- group{'g1} } -->  
    sequent ['ext] { 'H >- group{'g2} } -->  
    sequent [squash] { 'H >- isset{'r1} } -->  
    sequent [squash] { 'H >- isset{'r2} } -->  
44     sequent [squash] { 'H; x: set >- isset{'f['x]} } -->     sequent [squash] { 'H; x: set >- isset{'f['x]} } -->
45     sequent ['ext] { 'H >- "type"{hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]}} }     sequent ['ext] { 'H >- "type"{hom{'g1; 'g2; x. 'f['x]}} }
46    
47  interactive hom_intro {| intro [] |} 'H :  interactive hom_intro {| intro [] |} 'H :
48     sequent [squash] { 'H >- 'g1 IN label } -->     sequent [squash] { 'H >- 'g1 IN label } -->
49     sequent [squash] { 'H >- 'g2 IN label } -->     sequent [squash] { 'H >- 'g2 IN label } -->
50     sequent ['ext] { 'H >- group{'g1} } -->     sequent ['ext] { 'H >- group{'g1} } -->
51     sequent ['ext] { 'H >- group{'g2} } -->     sequent ['ext] { 'H >- group{'g2} } -->
    sequent ['ext] { 'H >- fun_set{z. 'f['z]} } -->  
52     sequent ['ext] { 'H; x: set; y: mem{'x; car{'g1}} >- mem{'f['x]; car{'g2}} } -->     sequent ['ext] { 'H; x: set; y: mem{'x; car{'g1}} >- mem{'f['x]; car{'g2}} } -->
53     sequent [squash] { 'H >- isset{'r1} } -->     sequent ['ext] { 'H; c: set; d: set; x1: mem{'c; car{'g1}}; y1: mem{'d; car{'g1}}; u: equiv{car{'g1}; eqG{'g1}; 'c; 'd} >- equiv{car{'g2}; eqG{'g2}; 'f['c]; 'f['d]} } -->
54     sequent [squash] { 'H >- isset{'r2} } -->     sequent ['ext] { 'H; e: set; g: set; x2: mem{'e; car{'g1}}; y2: mem{'g; car{'g1}} >- equiv{car{'g2}; eqG{'g2}; 'f[op{'g1; 'e; 'g}]; op{'g2; 'f['e]; 'f['g]}} } -->
55     sequent ['ext] { 'H >- equiv{car{'g1}; 'r1} } -->     sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} }
    sequent ['ext] { 'H >- equiv{car{'g2}; 'r2} } -->  
    sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'g1}}; y: mem{'b; car{'g1}} >- equiv{car{'g2}; 'r2; 'f[op{'g1; 'a; 'b}]; op{'g2; 'f['a]; 'f['b]}} } -->  
    sequent ['ext] { 'H >- hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} }  
56    
57  interactive hom_fun {| intro [] |} 'H :  interactive hom_fun {| intro [] |} 'H :
58     sequent [squash] { 'H >- 'g1 IN label } -->     sequent [squash] { 'H >- 'g1 IN label } -->
59     sequent [squash] { 'H >- 'g2 IN label } -->     sequent [squash] { 'H >- 'g2 IN label } -->
60     sequent ['ext] { 'H >- group{'g1} } -->     sequent ['ext] { 'H >- group{'g1} } -->
61     sequent ['ext] { 'H >- group{'g2} } -->     sequent ['ext] { 'H >- group{'g2} } -->
62     sequent ['ext] { 'H >- fun_set{z. 'r2['z]} } -->     sequent ['ext] { 'H; z: set; x1: set; y1: mem{'x1; car{'g1}} >- mem{'f['z; 'x1]; car{'g2}} } -->
    sequent ['ext] { 'H >- fun_set{z. 'r1['z]} } -->  
    sequent ['ext] { 'H; z: set >- fun_set{x. 'f['z; 'x]} } -->  
63     sequent ['ext] { 'H; z: set >- fun_set{x. 'f['x; 'z]} } -->     sequent ['ext] { 'H; z: set >- fun_set{x. 'f['x; 'z]} } -->
64       sequent ['ext] { 'H >- fun_prop{z. hom{'g1; 'g2; y. 'f['z; 'y]}} }
65    
66    interactive hom_equiv_fun {| intro [] |} 'H :
67       sequent [squash] { 'H >- 'g1 IN label } -->
68       sequent [squash] { 'H >- 'g2 IN label } -->
69       sequent ['ext] { 'H >- group{'g1} } -->
70       sequent ['ext] { 'H >- group{'g2} } -->
71     sequent [squash] { 'H; z: set; x: set >- isset{'f['z; 'x]} } -->     sequent [squash] { 'H; z: set; x: set >- isset{'f['z; 'x]} } -->
72     sequent ['ext] { 'H; z: set; x: set; y: mem{'x; car{'g1}} >- mem{'f['z; 'x]; car{'g2}} } -->     sequent ['ext] { 'H; z1: set; x1: set; y1: mem{'x1; car{'g1}} >- mem{'f['z1; 'x1]; car{'g2}} } -->
73     sequent ['ext] { 'H >- fun_prop{z. hom{'g1; 'g2; 'r1['z]; 'r2['z]; y. 'f['z; 'y]}} }     sequent ['ext] { 'H; z3: set; c: set; d: set; x3: mem{'c; car{'g1}}; y3: mem{'d; car{'g1}}; v: equiv{car{'g1}; eqG{'g1}; 'c; 'd} >- equiv{car{'g2}; eqG{'g2}; 'f['c; 'z3]; 'f['d; 'z3]} } -->
74       sequent ['ext] { 'H >- equiv_fun_prop{car{'g1}; eqG{'g1}; z. hom{'g1; 'g2; y. 'f['z; 'y]}} }
75    
76  (*  (*
77   * Trivial homomorphism   * Trivial homomorphism
# Line 86  Line 84 
84     sequent [squash] { 'H >- 'g2 IN label } -->     sequent [squash] { 'H >- 'g2 IN label } -->
85     sequent ['ext] { 'H >- group{'g1} } -->     sequent ['ext] { 'H >- group{'g1} } -->
86     sequent ['ext] { 'H >- group{'g2} } -->     sequent ['ext] { 'H >- group{'g2} } -->
87     sequent ['ext] { 'H >- fun_set{z. 'f['z]} } -->     sequent ['ext] { 'H; x: set; y: mem{'x; car{'g1}} >- equiv{car{'g2}; eqG{'g2}; 'f['x]; id{'g2}} } -->
88     sequent [squash] { 'H >- isset{'r1} } -->     sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} }
    sequent [squash] { 'H >- isset{'r2} } -->  
    sequent ['ext] { 'H >- equiv{car{'g1}; 'r1} } -->  
    sequent ['ext] { 'H >- equiv{car{'g2}; 'r2} } -->  
    sequent ['ext] { 'H; x: set; y: mem{'x; car{'g1}} >- equiv{car{'g2}; 'r2; 'f['x]; id{'g2}} } -->  
    sequent ['ext] { 'H >- hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} }  
89    
90  (*  (*
91   * Let f: G -> G' be a group homomorphism of G ONTO G'. If G is abelian,   * Let f: G -> G' be a group homomorphism of G ONTO G'. If G is abelian,
92   * then G' must be abelian.   * then G' must be abelian.
93   *)   *)
94  interactive hom_abel 'H hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} :  interactive hom_abel 'H hom{'g1; 'g2; x. 'f['x]} :
95     sequent [squash] { 'H >- 'g1 IN label } -->     sequent [squash] { 'H >- 'g1 IN label } -->
96     sequent [squash] { 'H >- 'g2 IN label } -->     sequent [squash] { 'H >- 'g2 IN label } -->
97     sequent [squash] { 'H >- isset{'r1} } -->     sequent ['ext] { 'H; x: set; y: mem{'x; car{'g2}} >- exst z: set. (mem{'z; car{'g1}} & equiv{car{'g2}; eqG{'g2}; 'x; 'f['z]}) } -->
98     sequent [squash] { 'H >- isset{'r2} } -->     sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} } -->
99     sequent ['ext] { 'H; x: set; y: mem{'x; car{'g2}} >- "dexists"{car{'g1}; z. equiv{car{'g2}; 'r2; 'x; 'f['z]}} } -->     sequent ['ext] { 'H >- abel{'g1} } -->
100     sequent ['ext] { 'H >- hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} } -->     sequent ['ext] { 'H >- abel{'g2} }
    sequent ['ext] { 'H >- abel{'g1; 'r1} } -->  
    sequent ['ext] { 'H >- abel{'g2; 'r2} }  
101    
102  (*  (*
103   * properties   * properties
104   *)   *)
105  (*  (*
106   * Let f: G -> G' be a group homomorphism of G ONTO G'.   * Let f: G -> G' be a group homomorphism of G into G'.
107   * If e is the identity in G, then f(e) is the identity e' in G'.   * If e is the identity in G, then f(e) is the identity e' in G'.
108   *)   *)
109  interactive hom_id 'H hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} :  interactive hom_id {| intro [] |} 'H hom{'g1; 'g2; x. 'f['x]} :
110     sequent [squash] { 'H >- 'g1 IN label } -->     sequent [squash] { 'H >- 'g1 IN label } -->
111     sequent [squash] { 'H >- 'g2 IN label } -->     sequent [squash] { 'H >- 'g2 IN label } -->
112     sequent [squash] { 'H >- isset{'r1} } -->     sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} } -->
113     sequent [squash] { 'H >- isset{'r2} } -->     sequent ['ext] { 'H >- equiv{car{'g2}; eqG{'g2}; 'f[id{'g1}]; id{'g2}} }
114     sequent ['ext] { 'H >- hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} } -->  
115     sequent ['ext] { 'H >- equiv{car{'g2}; 'r2; 'f[id{'g1}]; id{'g2}} }  interactive hom_id_elim (*{| elim [] |}*) 'H 'J :
116       sequent [squash] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g1 IN label } -->
117       sequent [squash] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g2 IN label } -->
118       sequent ['ext] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u]; v: equiv{car{'g2}; eqG{'g2}; 'f[id{'g1}]; id{'g2}} >- 'C['u] } -->
119       sequent ['ext] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u] >- 'C['u] }
120    
121    let homIdT i p =
122       let j, k = Sequent.hyp_indices p i in
123          hom_id_elim j k p
124    
125  (*  (*
126   * Let f: G -> G' be a group homomorphism of G ONTO G'.   * Let f: G -> G' be a group homomorphism of G into G'.
127   * For any a in G, f(inv(a)) = inv(f(a)).   * For any a in G, f(inv(a)) = inv(f(a)).
128   *)   *)
129  interactive hom_inv 'H 'a hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} :  interactive hom_inv {| intro [] |} 'H 'a hom{'g1; 'g2; x. 'f['x]} :
130     sequent [squash] { 'H >- 'g1 IN label } -->     sequent [squash] { 'H >- 'g1 IN label } -->
131     sequent [squash] { 'H >- 'g2 IN label } -->     sequent [squash] { 'H >- 'g2 IN label } -->
132     sequent [squash] { 'H >- isset{'r1} } -->     sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} } -->
    sequent [squash] { 'H >- isset{'r2} } -->  
 (*   sequent [squash] { 'H; x: set >- isset{'f['x]} } -->*)  
    sequent ['ext] { 'H >- hom{'g1; 'g2; 'r1; 'r2; x. 'f['x]} } -->  
133     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
134     sequent ['ext] { 'H >- mem{'a; car{'g1}} } -->     sequent ['ext] { 'H >- mem{'a; car{'g1}} } -->
135     sequent ['ext] { 'H >- equiv{car{'g2}; 'r2; 'f[inv{'g1; 'a}]; inv{'g2; 'f['a]}} }     sequent ['ext] { 'H >- equiv{car{'g2}; eqG{'g2}; 'f[inv{'g1; 'a}]; inv{'g2; 'f['a]}} }
136    
137    interactive hom_inv_elim (*{| elim [] |}*) 'H 'J 'a :
138       sequent [squash] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g1 IN label } -->
139       sequent [squash] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u] >- 'g2 IN label } -->
140       sequent ['ext] { 'H >- hom{'g1; 'g2; x. 'f['x]} } -->
141       sequent [squash] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u] >- isset{'a} } -->
142       sequent ['ext] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u] >- mem{'a; car{'g1}} } -->
143       sequent ['ext] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u]; v: equiv{car{'g2}; eqG{'g2}; 'f[inv{'g1; 'a}]; inv{'g2; 'f['a]}} >- 'C['u] } -->
144       sequent ['ext] { 'H; u: hom{'g1; 'g2; x. 'f['x]}; 'J['u] >- 'C['u] }
145    
146    let homInvT t i p =
147       let j, k = Sequent.hyp_indices p i in
148          hom_inv_elim j k t p

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

  ViewVC Help
Powered by ViewVC 1.1.26