/[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 3569 by xiny, Wed Apr 3 05:27:01 2002 UTC revision 3570 by xiny, Tue Apr 9 05:59:41 2002 UTC
# Line 3  Line 3 
3  include Czf_itt_group  include Czf_itt_group
4  include Czf_itt_subset  include Czf_itt_subset
5  include Czf_itt_isect  include Czf_itt_isect
6    include Czf_itt_group_bvd
7    
8  open Printf  open Printf
9  open Mp_debug  open Mp_debug
# Line 30  Line 31 
31  declare subgroup{'s; 'g}  declare subgroup{'s; 'g}
32    
33  prim_rw unfold_subgroup : subgroup{'s; 'g} <-->  prim_rw unfold_subgroup : subgroup{'s; 'g} <-->
34     (group{'s} & group{'g} & subset{car{'s}; car{'g}} & (all a: set. all b: set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equiv{car{'s}; eqG{'s}; 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})) & (all a: set. all b: set. (mem{'a; car{'s}} => mem{'b; car{'s}} => equiv{car{'g}; eqG{'g}; 'a; 'b} => equiv{car{'s}; eqG{'s}; 'a; 'b})))     (group{'s} & group{'g} & subset{car{'s}; car{'g}} & group_bvd{'s; 'g; car{'s}})
35    
36  dform subgroup_df : except_mode[src] :: subgroup{'s; 'g} =  dform subgroup_df : except_mode[src] :: subgroup{'s; 'g} =
37     `"subgroup(" slot{'s} `"; " slot{'g} `")"     `"subgroup(" slot{'s} `"; " slot{'g} `")"
# Line 54  Line 55 
55     sequent ['ext] { 'H; p: set; q: set; x: mem{'p; car{'s}}; y: mem{'q; car{'s}}; v: equiv{car{'g}; eqG{'g}; 'p; 'q} >- equiv{car{'s}; eqG{'s}; 'p; 'q} } -->     sequent ['ext] { 'H; p: set; q: set; x: mem{'p; car{'s}}; y: mem{'q; car{'s}}; v: equiv{car{'g}; eqG{'g}; 'p; 'q} >- equiv{car{'s}; eqG{'s}; 'p; 'q} } -->
56     sequent ['ext] { 'H >- subgroup{'s; 'g} }     sequent ['ext] { 'H >- subgroup{'s; 'g} }
57    
58    (*
59     * Properties.
60     *)
61  interactive subgroup_equiv {| intro [] |} 'H :  interactive subgroup_equiv {| intro [] |} 'H :
62     sequent [squash] { 'H >- 's IN label } -->     sequent [squash] { 'H >- 's IN label } -->
63     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
# Line 81  Line 85 
85     sequent [squash] { 'H >- 'h1 IN label } -->     sequent [squash] { 'H >- 'h1 IN label } -->
86     sequent [squash] { 'H >- 'h2 IN label } -->     sequent [squash] { 'H >- 'h2 IN label } -->
87     sequent [squash] { 'H >- 'h IN label } -->     sequent [squash] { 'H >- 'h IN label } -->
    sequent ['ext] { 'H >- group{'h} } -->  
88     sequent ['ext] { 'H >- subgroup{'h1; 'g} } -->     sequent ['ext] { 'H >- subgroup{'h1; 'g} } -->
89     sequent ['ext] { 'H >- subgroup{'h2; 'g} } -->     sequent ['ext] { 'H >- subgroup{'h2; 'g} } -->
90     sequent ['ext] { 'H >- equal{car{'h}; ."isect"{car{'h1}; car{'h2}}} } -->     sequent ['ext] { 'H >- group_bvd{'h; 'h1; ."isect"{car{'h1}; car{'h2}}} } -->
    sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'h}}; y: mem{'b; car{'h}} >- equiv{car{'h}; eqG{'h}; op{'h; 'a; 'b}; op{'h1; 'a; 'b}} } -->  
    sequent ['ext] { 'H; c: set; d: set; u: equiv{car{'h}; eqG{'h}; 'c; 'd} >- equiv{car{'h1}; eqG{'h1}; 'c; 'd} } -->  
    sequent ['ext] { 'H; e: set; f: set; x1: mem{'e; car{'h}}; y1: mem{'f; car{'h}}; v: equiv{car{'h1}; eqG{'h1}; 'e; 'f} >- equiv{car{'h}; eqG{'h}; 'e; 'f} } -->  
91     sequent ['ext] { 'H >- subgroup{'h; 'g} }     sequent ['ext] { 'H >- subgroup{'h; 'g} }
92    
93  let subgroupIsectT t1 t2 p =  let subgroupIsectT t1 t2 p =

Legend:
Removed from v.3569  
changed lines
  Added in v.3570

  ViewVC Help
Powered by ViewVC 1.1.26