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

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

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

revision 3567 by xiny, Sun Mar 24 07:54:36 2002 UTC revision 3568 by xiny, Tue Apr 9 05:57:54 2002 UTC
# Line 1  Line 1 
 include Czf_itt_set  
1  include Czf_itt_dall  include Czf_itt_dall
2  include Czf_itt_dexists  include Czf_itt_dexists
3    
# Line 24  Line 23 
23  open Base_dtactic  open Base_dtactic
24  open Base_auto_tactic  open Base_auto_tactic
25    
26  declare set_bvd{'s; x. 'a['x]}        (* { a(x) | x in s } *)  declare set_bvd{'s; x. 'a['x]}            (* { a(x) | x in s } *)
27    declare setbvd_prop{'s; x. 'p['x]}        (* { x in s | p(x) } *)
28    
29  prim_rw unfold_set_bvd: set_bvd{'s; x. 'a['x]} <-->  prim_rw unfold_set_bvd: set_bvd{'s; x. 'a['x]} <-->
30     set_ind{'s; t, f, g. collect{'t; y. 'a['f 'y]}}     set_ind{'s; t, f, g. collect{'t; y. 'a['f 'y]}}
# Line 35  Line 35 
35  let resource reduce += << set_bvd{collect{'T; x. 'f['x]}; x. 'a['x]} >>, reduce_set_bvd  let resource reduce += << set_bvd{collect{'T; x. 'f['x]}; x. 'a['x]} >>, reduce_set_bvd
36    
37  dform set_bvd_df : parens :: except_mode[src] :: set_bvd{'s; x. 'a} =  dform set_bvd_df : parens :: except_mode[src] :: set_bvd{'s; x. 'a} =
38     pushm[0] `"{" slot{'a} `"| " slot{'x} " " Nuprl_font!member `"s " slot{'s} `"}" popm     pushm[0] `"{" slot{'a} `" | " slot{'x} " " Nuprl_font!member `"s " slot{'s} `"}" popm
39    
40    dform setbvd_prop_df : parens :: except_mode[src] :: setbvd_prop{'s; x. 'p} =
41       pushm[0] `"{" slot{'x} " " Nuprl_font!member `"s " slot{'s} `" | " slot{'p} `"}" popm
42    
43    (*
44     * Propertiess for set builder.
45     *)
46  interactive set_bvd_isset {| intro [] |} 'H :  interactive set_bvd_isset {| intro [] |} 'H :
47     sequent [squash] { 'H >- isset{'s} } -->     sequent [squash] { 'H >- isset{'s} } -->
48     sequent [squash] { 'H; x: set >- isset{'a['x]} } -->     sequent [squash] { 'H; x: set >- isset{'a['x]} } -->
# Line 64  Line 70 
70     sequent ['ext] { 'H; z: set >- fun_set{x. 'B['x; 'z]} } -->     sequent ['ext] { 'H; z: set >- fun_set{x. 'B['x; 'z]} } -->
71     ["wf"] sequent [squash] { 'H; z: set; x: set >- isset{'B['z; 'x]} } -->     ["wf"] sequent [squash] { 'H; z: set; x: set >- isset{'B['z; 'x]} } -->
72     sequent ['ext] { 'H >- fun_set{z. set_bvd{'A['z]; y. 'B['z; 'y]}} }     sequent ['ext] { 'H >- fun_set{z. set_bvd{'A['z]; y. 'B['z; 'y]}} }
73    
74    (*
75     * Axioms for setbvd_prop.
76     *)
77    interactive setbvd_prop_isset {| intro [] |} 'H :
78       sequent [squash] { 'H >- isset{'s} } -->
79       sequent [squash] { 'H; x: set >- "type"{'p['x]} } -->
80       sequent ['ext] { 'H >- isset{setbvd_prop{'s; x. 'p['x]}} }
81    
82    interactive setbvd_prop_member_intro {| intro [] |} 'H :
83       sequent [squash] { 'H >- isset{'s} } -->
84       sequent [squash] { 'H >- isset{'y} } -->
85       sequent [squash] { 'H; z: set >- "type"{'p['z]} } -->
86       sequent ['ext] { 'H >- fun_prop{z. 'p['z]} } -->
87       sequent ['ext] { 'H >- mem{'y; 's} } -->
88       sequent ['ext] { 'H >- 'p['y] } -->
89       sequent ['ext] { 'H >- mem{'y; setbvd_prop{'s; x. 'p['x]}} }
90    
91    interactive setbvd_prop_member_elim {| elim [] |} 'H 'J :
92       sequent [squash] { 'H; u: mem{'y; setbvd_prop{'s; x. 'p['x]}}; 'J['u] >- isset{'s} } -->
93       sequent [squash] { 'H; u: mem{'y; setbvd_prop{'s; x. 'p['x]}}; 'J['u] >- isset{'y} } -->
94       sequent [squash] { 'H; u: mem{'y; setbvd_prop{'s; x. 'p['x]}}; 'J['u]; z: set >- "type"{'p['z]} } -->
95       sequent ['ext] { 'H; u: mem{'y; setbvd_prop{'s; x. 'p['x]}}; 'J['u] >- fun_prop{z. 'p['z]} } -->
96       sequent ['ext] { 'H; u: mem{'y; setbvd_prop{'s; x. 'p['x]}}; 'J['u]; v: mem{'y; 's}; w: 'p['y] >- 'C['u] } -->
97       sequent ['ext] { 'H; u: mem{'y; setbvd_prop{'s; x. 'p['x]}}; 'J['u] >- 'C['u] }

Legend:
Removed from v.3567  
changed lines
  Added in v.3568

  ViewVC Help
Powered by ViewVC 1.1.26