/[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 3545 - (hide 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 xiny 3545 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