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

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

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

revision 3555 by xiny, Mon Mar 11 09:58:58 2002 UTC revision 3556 by xiny, Tue Apr 2 08:08:36 2002 UTC
# Line 23  Line 23 
23  open Base_dtactic  open Base_dtactic
24  open Base_auto_tactic  open Base_auto_tactic
25    
26  (* subgroup{'g; 's} is a type representing the subgroup  (* subgroup{'s; 'g} is a type representing the subgroup
27   * of the group represented by 'g, where 's is a label   * of the group represented by 'g, where 's is a label
28   * representing the subgroup which itself is also a group.   * representing the subgroup which itself is also a group.
29   *)   *)
30  declare subgroup{'g; 's}  declare subgroup{'s; 'g}
31    
32  prim_rw unfold_subgroup : subgroup{'g; 's} <-->  prim_rw unfold_subgroup : subgroup{'s; 'g} <-->
33     (group{'g} & group{'s} & subset{car{'s}; car{'g}} & (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} & subset{car{'s}; car{'g}} & (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})))
34    
35  dform subgroup_df : except_mode[src] :: subgroup{'g; 's} =  dform subgroup_df : except_mode[src] :: subgroup{'s; 'g} =
36     `"subgroup(" slot{'g} `"; " slot{'s} `")"     `"subgroup(" slot{'s} `"; " slot{'g} `")"
37    
38  (*  (*
39   * Axioms   * Axioms
40   *)   *)
41  interactive subgroup_type {| intro [] |} 'H :  interactive subgroup_type {| intro [] |} 'H :
    sequent [squash] { 'H >- 'g IN label } -->  
42     sequent [squash] { 'H >- 's IN label } -->     sequent [squash] { 'H >- 's IN label } -->
43     sequent ['ext] { 'H >- group{'g} } -->     sequent [squash] { 'H >- 'g IN label } -->
44     sequent ['ext] { 'H >- group{'s} } -->     sequent ['ext] { 'H >- "type"{subgroup{'s; 'g}} }
    sequent ['ext] { 'H >- "type"{subgroup{'g; 's}} }  
45    
46  interactive subgroup_intro {| intro [] |} 'H :  interactive subgroup_intro {| intro [] |} 'H :
    sequent [squash] { 'H >- 'g IN label } -->  
47     sequent [squash] { 'H >- 's IN label } -->     sequent [squash] { 'H >- 's IN label } -->
48     sequent ['ext] { 'H >- group{'g} } -->     sequent [squash] { 'H >- 'g IN label } -->
49     sequent ['ext] { 'H >- group{'s} } -->     sequent ['ext] { 'H >- group{'s} } -->
50       sequent ['ext] { 'H >- group{'g} } -->
51     sequent ['ext] { 'H >- subset{car{'s}; car{'g}} } -->     sequent ['ext] { 'H >- subset{car{'s}; car{'g}} } -->
52     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}} } -->
53     sequent ['ext] { 'H >- subgroup{'g; 's} }     sequent ['ext] { 'H; a: set; b: set; x: equiv{car{'s}; eqG{'s}; 'a; 'b} >- equiv{car{'g}; eqG{'g}; 'a; 'b} } -->
54       sequent ['ext] { 'H >- subgroup{'s; 'g} }
55    
56  interactive subgroup_equiv_elim {| elim [] |} 'H 'J 's :  interactive subgroup_equiv {| intro [] |} 'H :
57     sequent [squash] { 'H; x: equiv{car{'g}; 'R}; 'J['x] >- 'g IN label } -->     sequent [squash] { 'H >- 's IN label } -->
58     sequent [squash] { 'H; x: equiv{car{'g}; 'R}; 'J['x] >- 's IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
59     sequent [squash] { 'H; x: equiv{car{'g}; 'R}; 'J['x] >- isset{'R} } -->     sequent ['ext] { 'H >- subgroup{'s; 'g} } -->
60     sequent ['ext] { 'H; x: equiv{car{'g}; 'R}; 'J['x] >- subgroup{'g; 's} } -->     sequent ['ext] { 'H >- equiv{car{'s}; eqG{'g}} }
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R}; 'J['x]; y: equiv{car{'s}; 'R} >- 'C['x] } -->  
    sequent ['ext] { 'H; x: equiv{car{'g}; 'R}; 'J['x] >- 'C['x] }  
61    
62  interactive subgroup_id {| intro [] |} 'H :  interactive subgroup_id {| intro [] |} 'H :
    sequent [squash] { 'H >- 'g IN label } -->  
63     sequent [squash] { 'H >- 's IN label } -->     sequent [squash] { 'H >- 's IN label } -->
64     sequent [squash] { 'H >- isset{'R} } -->     sequent [squash] { 'H >- 'g IN label } -->
65     sequent ['ext] { 'H >- subgroup{'g; 's} } -->     sequent ['ext] { 'H >- subgroup{'s; 'g} } -->
66     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; id{'s}; id{'g}} }
    sequent ['ext] { 'H >- equiv{car{'g}; 'R; id{'s}; id{'g}} }  
67    
68  interactive subgroup_inv {| intro [] |} 'H :  interactive subgroup_inv {| intro [] |} 'H :
    sequent [squash] { 'H >- 'g IN label } -->  
69     sequent [squash] { 'H >- 's IN label } -->     sequent [squash] { 'H >- 's IN label } -->
70     sequent [squash] { 'H >- isset{'R} } -->     sequent [squash] { 'H >- 'g IN label } -->
71     sequent [squash] { 'H >- isset{'a} } -->     sequent [squash] { 'H >- isset{'a} } -->
72     sequent ['ext] { 'H >- mem{'a; car{'s}} } -->     sequent ['ext] { 'H >- mem{'a; car{'s}} } -->
73     sequent ['ext] { 'H >- subgroup{'g; 's} } -->     sequent ['ext] { 'H >- subgroup{'s; 'g} } -->
74     sequent ['ext] { 'H >- equiv{car{'g}; 'R} } -->     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; inv{'s; 'a}; inv{'g; 'a}} }
    sequent ['ext] { 'H >- equiv{car{'g}; 'R; inv{'s; 'a}; inv{'g; 'a}} }  
75    
76  (* Properties *)  (* Properties *)
77  (* The intersections of subgroups H1 and H2 of a group G is again a subgroup of G. *)  (* The intersections of subgroups H1 and H2 of a group G is again a subgroup of G. *)
# Line 88  Line 81 
81     sequent [squash] { 'H >- 'h2 IN label } -->     sequent [squash] { 'H >- 'h2 IN label } -->
82     sequent [squash] { 'H >- 'h IN label } -->     sequent [squash] { 'H >- 'h IN label } -->
83     sequent ['ext] { 'H >- group{'h} } -->     sequent ['ext] { 'H >- group{'h} } -->
84     sequent ['ext] { 'H >- subgroup{'g; 'h1} } -->     sequent ['ext] { 'H >- subgroup{'h1; 'g} } -->
85     sequent ['ext] { 'H >- subgroup{'g; 'h2} } -->     sequent ['ext] { 'H >- subgroup{'h2; 'g} } -->
86     sequent ['ext] { 'H >- equal{car{'h}; ."isect"{car{'h1}; car{'h2}}} } -->     sequent ['ext] { 'H >- equal{car{'h}; ."isect"{car{'h1}; car{'h2}}} } -->
87     sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'h}}; x: mem{'b; car{'h}} >- equal{op{'h; 'a; 'b}; op{'g; 'a; 'b}} } -->     sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'h}}; x: mem{'b; car{'h}} >- equal{op{'h; 'a; 'b}; op{'h1; 'a; 'b}} } -->
88     sequent ['ext] { 'H >- subgroup{'g; 'h} }     sequent ['ext] { 'H; a: set; b: set; x: equiv{car{'h}; eqG{'h}; 'a; 'b} >- equiv{car{'h1}; eqG{'h1}; 'a; 'b} } -->
89       sequent ['ext] { 'H >- subgroup{'h; 'g} }
90    
91  let subgroupIsectT t1 t2 p =  let subgroupIsectT t1 t2 p =
92     subgroup_isect (hyp_count_addr p) t1 t2 p     subgroup_isect (hyp_count_addr p) t1 t2 p

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

  ViewVC Help
Powered by ViewVC 1.1.26