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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3545 - (show annotations) (download)
Sun Mar 24 07:54:36 2002 UTC (19 years, 4 months ago) by xiny
File size: 2608 byte(s)
Added the definition for "set builder", i.e., the image of a set s
under some function f: { f(x) | x in s }. I consider this as a necessity
for the set theory.

The "set builder" is defined by a "set-induction" rewrite rule. Also
added and proved properties for it.

1 include Czf_itt_set
2 include Czf_itt_dall
3 include Czf_itt_dexists
4
5 open Printf
6 open Mp_debug
7 open Refiner.Refiner.TermType
8 open Refiner.Refiner.Term
9 open Refiner.Refiner.TermOp
10 open Refiner.Refiner.TermAddr
11 open Refiner.Refiner.TermMan
12 open Refiner.Refiner.TermSubst
13 open Refiner.Refiner.Refine
14 open Refiner.Refiner.RefineError
15 open Mp_resource
16
17 open Tactic_type
18 open Tactic_type.Tacticals
19 open Tactic_type.Sequent
20 open Tactic_type.Conversionals
21 open Mptop
22 open Var
23
24 open Base_dtactic
25 open Base_auto_tactic
26
27 declare set_bvd{'s; x. 'a['x]} (* { a(x) | x in s } *)
28
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 pushm[0] `"{" slot{'a} `"| " slot{'x} " " Nuprl_font!member `"s " slot{'s} `"}" popm
39
40 interactive set_bvd_isset {| intro [] |} 'H :
41 sequent [squash] { 'H >- isset{'s} } -->
42 sequent [squash] { 'H; x: set >- isset{'a['x]} } -->
43 sequent ['ext] { 'H >- isset{set_bvd{'s; x. 'a['x]}} }
44
45 interactive set_bvd_member_intro {| intro [] |} 'H :
46 sequent [squash] { 'H >- isset{'s} } -->
47 sequent [squash] { 'H >- isset{'y} } -->
48 sequent [squash] { 'H; x: set >- isset{'a['x]} } -->
49 sequent ['ext] { 'H >- fun_set{x. 'a['x]} } -->
50 sequent ['ext] { 'H >- dexists{'s; z. eq{'y; 'a['z]}} } -->
51 sequent ['ext] { 'H >- mem{'y; set_bvd{'s; x. 'a['x]}} }
52
53 interactive set_bvd_member_elim {| elim [] |} 'H 'J :
54 sequent [squash] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x] >- isset{'y} } -->
55 sequent [squash] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x] >- isset{'s} } -->
56 sequent [squash] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x]; z: set >- isset{'a['z]} } -->
57 sequent ['ext] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x] >- fun_set{x. 'a['x]} } -->
58 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] } -->
59 sequent ['ext] { 'H; x: mem{'y; set_bvd{'s; x. 'a['x]}}; 'J['x] >- 'T['x] }
60
61 interactive set_bvd_fun {| intro [] |} 'H :
62 sequent ['ext] { 'H >- fun_set{z. 'A['z]} } -->
63 sequent ['ext] { 'H; z: set >- fun_set{x. 'B['z; 'x]} } -->
64 sequent ['ext] { 'H; z: set >- fun_set{x. 'B['x; 'z]} } -->
65 ["wf"] sequent [squash] { 'H; z: set; x: set >- isset{'B['z; 'x]} } -->
66 sequent ['ext] { 'H >- fun_set{z. set_bvd{'A['z]; y. 'B['z; 'y]}} }

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26