/[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 3559 by xiny, Tue Apr 2 08:08:36 2002 UTC revision 3560 by xiny, Wed Apr 3 05:27:01 2002 UTC
# Line 30  Line 30 
30  declare subgroup{'s; 'g}  declare subgroup{'s; 'g}
31    
32  prim_rw unfold_subgroup : subgroup{'s; 'g} <-->  prim_rw unfold_subgroup : subgroup{'s; 'g} <-->
33     (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})))     (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})))
34    
35  dform subgroup_df : except_mode[src] :: subgroup{'s; 'g} =  dform subgroup_df : except_mode[src] :: subgroup{'s; 'g} =
36     `"subgroup(" slot{'s} `"; " slot{'g} `")"     `"subgroup(" slot{'s} `"; " slot{'g} `")"
# Line 38  Line 38 
38  (*  (*
39   * Axioms   * Axioms
40   *)   *)
41  interactive subgroup_type {| intro [] |} 'H :  interactive subgroup_wf {| intro [] |} 'H :
42     sequent [squash] { 'H >- 's IN label } -->     sequent [squash] { 'H >- 's IN label } -->
43     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
44     sequent ['ext] { 'H >- "type"{subgroup{'s; 'g}} }     sequent ['ext] { 'H >- "type"{subgroup{'s; 'g}} }
# Line 49  Line 49 
49     sequent ['ext] { 'H >- group{'s} } -->     sequent ['ext] { 'H >- group{'s} } -->
50     sequent ['ext] { 'H >- group{'g} } -->     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}} >- equiv{car{'s}; eqG{'s}; op{'s; 'a; 'b}; op{'g; 'a; 'b}} } -->
53     sequent ['ext] { 'H; a: set; b: set; x: equiv{car{'s}; eqG{'s}; 'a; 'b} >- equiv{car{'g}; eqG{'g}; 'a; 'b} } -->     sequent ['ext] { 'H; c: set; d: set; u: equiv{car{'s}; eqG{'s}; 'c; 'd} >- equiv{car{'g}; eqG{'g}; 'c; 'd} } -->
54       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} } -->
55     sequent ['ext] { 'H >- subgroup{'s; 'g} }     sequent ['ext] { 'H >- subgroup{'s; 'g} }
56    
57  interactive subgroup_equiv {| intro [] |} 'H :  interactive subgroup_equiv {| intro [] |} 'H :
# Line 84  Line 85 
85     sequent ['ext] { 'H >- subgroup{'h1; 'g} } -->     sequent ['ext] { 'H >- subgroup{'h1; 'g} } -->
86     sequent ['ext] { 'H >- subgroup{'h2; 'g} } -->     sequent ['ext] { 'H >- subgroup{'h2; 'g} } -->
87     sequent ['ext] { 'H >- equal{car{'h}; ."isect"{car{'h1}; car{'h2}}} } -->     sequent ['ext] { 'H >- equal{car{'h}; ."isect"{car{'h1}; car{'h2}}} } -->
88     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}} } -->     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}} } -->
89     sequent ['ext] { 'H; a: set; b: set; x: equiv{car{'h}; eqG{'h}; 'a; 'b} >- equiv{car{'h1}; eqG{'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} } -->
90       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.3559  
changed lines
  Added in v.3560

  ViewVC Help
Powered by ViewVC 1.1.26