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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3568 - (hide annotations) (download)
Tue Apr 9 05:57:54 2002 UTC (19 years, 3 months ago) by xiny
File size: 4161 byte(s)
Added the definition for setbvd_prop. "set_bvd" and "setbvd_prop" are
both methods for building sets. The former builds set { a(x) | x in s }
from set s where a(x) is a function; the latter builds set
{ x in s | p(x) } from all elements x in s satisfying p(x). Both of
them are very useful. The former is defined by set induction on s; the
latter is defined by member introduction and elimination rules.

1 xiny 3545 include Czf_itt_dall
2     include Czf_itt_dexists
3    
4     open Printf
5     open Mp_debug
6     open Refiner.Refiner.TermType
7     open Refiner.Refiner.Term
8     open Refiner.Refiner.TermOp
9     open Refiner.Refiner.TermAddr
10     open Refiner.Refiner.TermMan
11     open Refiner.Refiner.TermSubst
12     open Refiner.Refiner.Refine
13     open Refiner.Refiner.RefineError
14     open Mp_resource
15    
16     open Tactic_type
17     open Tactic_type.Tacticals
18     open Tactic_type.Sequent
19     open Tactic_type.Conversionals
20     open Mptop
21     open Var
22    
23     open Base_dtactic
24     open Base_auto_tactic
25    
26 xiny 3568 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 xiny 3545
29     prim_rw unfold_set_bvd: set_bvd{'s; x. 'a['x]} <-->
30     set_ind{'s; t, f, g. collect{'t; y. 'a['f 'y]}}
31    
32     interactive_rw reduce_set_bvd : set_bvd{collect{'T; x. 'f['x]}; x. 'a['x]} <-->
33     collect{'T; y. 'a['f['y]]}
34    
35     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} =
38 xiny 3568 pushm[0] `"{" slot{'a} `" | " slot{'x} " " Nuprl_font!member `"s " slot{'s} `"}" popm
39 xiny 3545
40 xiny 3568 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 xiny 3545 interactive set_bvd_isset {| intro [] |} 'H :
47     sequent [squash] { 'H >- isset{'s} } -->
48     sequent [squash] { 'H; x: set >- isset{'a['x]} } -->
49     sequent ['ext] { 'H >- isset{set_bvd{'s; x. 'a['x]}} }
50    
51     interactive set_bvd_member_intro {| intro [] |} 'H :
52     sequent [squash] { 'H >- isset{'s} } -->
53     sequent [squash] { 'H >- isset{'y} } -->
54     sequent [squash] { 'H; x: set >- isset{'a['x]} } -->
55     sequent ['ext] { 'H >- fun_set{x. 'a['x]} } -->
56     sequent ['ext] { 'H >- dexists{'s; z. eq{'y; 'a['z]}} } -->
57     sequent ['ext] { 'H >- mem{'y; set_bvd{'s; x. 'a['x]}} }
58    
59     interactive set_bvd_member_elim {| elim [] |} 'H 'J :
60     sequent [squash] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x] >- isset{'y} } -->
61     sequent [squash] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x] >- isset{'s} } -->
62     sequent [squash] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x]; z: set >- isset{'a['z]} } -->
63     sequent ['ext] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x] >- fun_set{x. 'a['x]} } -->
64     sequent ['ext] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x]; z: set; u: mem{'z; 's}; v: eq{'y; 'a['z]} >- 'T['x] } -->
65     sequent ['ext] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x] >- 'T['x] }
66    
67     interactive set_bvd_fun {| intro [] |} 'H :
68     sequent ['ext] { 'H >- fun_set{z. 'A['z]} } -->
69     sequent ['ext] { 'H; z: set >- fun_set{x. 'B['z; 'x]} } -->
70     sequent ['ext] { 'H; z: set >- fun_set{x. 'B['x; 'z]} } -->
71     ["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]}} }
73 xiny 3568
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] }

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26