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

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

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

revision 3553 by xiny, Tue Apr 2 07:45:26 2002 UTC revision 3554 by xiny, Tue Apr 2 07:47:14 2002 UTC
# Line 31  Line 31 
31  declare group{'g}  declare group{'g}
32  declare car{'g}         (* The "carrier" set for the group *)  declare car{'g}         (* The "carrier" set for the group *)
33  declare eqG{'g}         (* The equivalence relation for the group *)  declare eqG{'g}         (* The equivalence relation for the group *)
 (* declare eqG{'g; 'a; 'b} (* a and b are equivalent in the group *) *)  
34  declare op{'g; 'a; 'b}  declare op{'g; 'a; 'b}
35  declare id{'g}  declare id{'g}
36  declare inv{'g; 'a}  declare inv{'g; 'a}
 (*  
 prim_rw unfold_eqG : eqG{'g; 'a; 'b} <-->  
    equiv{car{'g}; eqG{'g}; 'a; 'b}  
37    
 let fold_eqG = makeFoldC << eqG{'g; 'a; 'b} >> unfold_eqG  
 *)  
38  dform group_df : except_mode[src] :: group{'g} =  dform group_df : except_mode[src] :: group{'g} =
39     slot{'g} `" group"     slot{'g} `" group"
40    
# Line 50  Line 44 
44  dform eqG_df1 : except_mode[src] :: eqG{'g} =  dform eqG_df1 : except_mode[src] :: eqG{'g} =
45     `"eqG(" slot{'g} `")"     `"eqG(" slot{'g} `")"
46    
 (*dform eqG_df2 : except_mode[src] :: eqG{'g; 'a; 'b} =  
    `"eqG(" slot{'g} `"; " slot{'a}  `"; " slot{'b} `")"  
 *)  
47  dform id_df : except_mode[src] :: id{'g} =  dform id_df : except_mode[src] :: id{'g} =
48     `"id(" slot{'g} `")"     `"id(" slot{'g} `")"
49    
# Line 82  Line 73 
73     sequent ['ext] { 'H >- group{'g} } -->     sequent ['ext] { 'H >- group{'g} } -->
74     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}} }     sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}} }
75    
 (*interactive eqG_elem_wf1 {| intro[] |} 'H :  
    sequent [squash] { 'H >- 'g IN label } -->  
    sequent [squash] { 'H >- isset{'a} } -->  
    sequent [squash] { 'H >- isset{'b} } -->  
    sequent ['ext] { 'H >- "type"{equiv{car{'g}; eqG{'g}; 'a; 'b}} }  
 *)  
 (*interactive eqG_elem_wf2 {| intro[] |} 'H :  
    sequent [squash] { 'H >- 'g IN label } -->  
    sequent ['ext] { 'H >- group{'g} } -->  
    sequent [squash] { 'H >- isset{'a} } -->  
    sequent [squash] { 'H >- isset{'b} } -->  
    sequent ['ext] { 'H >- mem{'a; car{'g}} } -->  
    sequent ['ext] { 'H >- mem{'b; car{'g}} } -->  
    sequent ['ext] { 'H >- mem{pair{'a; 'b}; eqG{'g}} } -->  
    sequent ['ext] { 'H >- equiv{car{'g}; eqG{'g}; 'a; 'b} }  
 *)  
76  interactive op_wf {| intro[] |} 'H :  interactive op_wf {| intro[] |} 'H :
77     sequent [squash] { 'H >- 'g IN label } -->     sequent [squash] { 'H >- 'g IN label } -->
78     sequent [squash] { 'H >- isset{'s1} } -->     sequent [squash] { 'H >- isset{'s1} } -->

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

  ViewVC Help
Powered by ViewVC 1.1.26