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

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

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

revision 3554 by xiny, Sun Mar 24 07:43:47 2002 UTC revision 3555 by xiny, Tue Apr 2 07:49:49 2002 UTC
# Line 25  Line 25 
25  open Base_dtactic  open Base_dtactic
26  open Base_auto_tactic  open Base_auto_tactic
27    
28  declare abel{'g; 'r}  declare abel{'g}
29    
30  prim_rw unfold_abel: abel{'g; 'r} <-->  prim_rw unfold_abel: abel{'g} <-->
31     (group{'g} & isset{'r} & equiv{car{'g}; 'r} & (all a: set. all b: set. (mem{'a; car{'g}} => mem{'b; car{'g}} => equiv{car{'g}; 'r; op{'g; 'a; 'b}; op{'g; 'b; 'a}})))     (group{'g} & (all a: set. all b: set. (mem{'a; car{'g}} => mem{'b; car{'g}} => equiv{car{'g}; eqG{'g}; op{'g; 'a; 'b}; op{'g; 'b; 'a}})))
32    
33  dform abel_df : except_mode[src] :: abel{'g; 'r} =  dform abel_df : except_mode[src] :: abel{'g} =
34     `"abel(" slot{'g} `"; " slot{'r} `")"     `"abel(" slot{'g} `")"
35    
36  interactive abel_type {| intro [] |} 'H :  interactive abel_type {| intro [] |} 'H :
37     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
38     sequent [squash] { 'H >- isset{'r} } -->     sequent ['ext] { 'H >- "type"{abel{'g}} }
    sequent ['ext] { 'H >- group{'g} } -->  
    sequent ['ext] { 'H >- "type"{abel{'g; 'r}} }  
39    
40  interactive abel_intro {| intro[] |} 'H :  interactive abel_intro {| intro[] |} 'H :
41     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
42     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
43     sequent [squash] { 'H >- isset{'r} } -->     sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'g}}; y: mem{'b; car{'g}} >- equiv{car{'g}; eqG{'g}; op{'g; 'a; 'b}; op{'g; 'b; 'a}} } -->
44     sequent ['ext] { 'H >- equiv{car{'g}; 'r} } -->     sequent ['ext] { 'H >- abel{'g} }
    sequent ['ext] { 'H; a: set; b: set; x: mem{'a; car{'g}}; y: mem{'b; car{'g}} >- equiv{car{'g}; 'r; op{'g; 'a; 'b}; op{'g; 'b; 'a}} } -->  
    sequent ['ext] { 'H >- abel{'g; 'r} }  

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

  ViewVC Help
Powered by ViewVC 1.1.26