/[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 3568 - (show 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 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 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]} <-->
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 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 :
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
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