/[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 8705 - (hide annotations) (download)
Wed Feb 15 06:59:08 2006 UTC (15 years, 5 months ago) by nogin
File size: 5482 byte(s)
- Filter_reflection: module names should not be capitalized.

- OMakefile_theories: rules for generating .p4 and .p4i for the reflected
  theories (these are pretty-printed versions of the generated OCaml code;
  useful for debugging the filter).

- OMakefile_theories: in rev 8704 I've ordered the new dependencies for the
  reflect_% files incorrectly (the theory .SUBDIRS did not have them in
  scope); fixed.

- Filter_prog: generate the show_loading debugging call at the beginning and
  end of every theory.

- A _huge_ number of theory files: removed the manual "show_loading" calls as
  they will now be automatically generated.

1 jyh 5668 doc <:doc<
2 nogin 4354 @module[Czf_itt_set_bvd]
3 jyh 5668
4 nogin 5735 The @tt[Czf_itt_set_bvd] module defines the @emph{image} of a set
5 nogin 4354 under some mapping. Image is defined as a set constructor
6     $@setbvd{x; s; a[x]}$, which builds a new set from an existing
7     set $s$ via some mapping $a[x]$. A set $x$ is a member of
8     $@setbvd{x; s; a[x]}$ if there exists a set $y @in s$ such
9     that $@eq{x; a[y]}$ is true.
10 jyh 5668
11 nogin 4354 The image constructor $@setbvd{z; @collect{x; T; f[x]}; a[z]}$
12     is defined as the set $@collect{y; T; a[f(y)]}$.
13 jyh 5668
14 nogin 7524 @docoff
15 nogin 4354 ----------------------------------------------------------------
16 jyh 5668
17 nogin 4354 @begin[license]
18     This file is part of MetaPRL, a modular, higher order
19     logical framework that provides a logical programming
20     environment for OCaml and other languages.
21 jyh 5668
22 nogin 7563 See the file doc/htmlman/default.html or visit http://metaprl.org/
23     for more information.
24 jyh 5668
25 nogin 4354 Copyright (C) 2002 Xin Yu, Caltech
26 jyh 5668
27 nogin 4354 This program is free software; you can redistribute it and/or
28     modify it under the terms of the GNU General Public License
29     as published by the Free Software Foundation; either version 2
30     of the License, or (at your option) any later version.
31 jyh 5668
32 nogin 4354 This program is distributed in the hope that it will be useful,
33     but WITHOUT ANY WARRANTY; without even the implied warranty of
34     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
35     GNU General Public License for more details.
36 jyh 5668
37 nogin 4354 You should have received a copy of the GNU General Public License
38     along with this program; if not, write to the Free Software
39     Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
40 jyh 5668
41 nogin 4354 Author: Xin Yu
42     @email{xiny@cs.caltech.edu}
43     @end[license]
44     >>
45 xiny 3623
46 nogin 7524
47 nogin 3707 extends Czf_itt_dall
48     extends Czf_itt_dexists
49 nogin 4463 doc docoff
50 xiny 3545
51 nogin 4723 open Lm_debug
52 jyh 5668 open Lm_printf
53 xiny 3545
54 nogin 4541 open Dtactic
55 nogin 4463 open Top_conversionals
56 xiny 3545
57 xiny 3623 (************************************************************************
58     * TERMS *
59     ************************************************************************)
60    
61 nogin 7524
62 xiny 3568 declare set_bvd{'s; x. 'a['x]} (* { a(x) | x in s } *)
63 nogin 7521 doc docoff
64 xiny 3545
65 xiny 3623 (************************************************************************
66     * REWRITES *
67     ************************************************************************)
68    
69 jyh 5668 doc <:doc<
70 nogin 4354 @rewrites
71 jyh 5668
72 nogin 4354 The @tt{set_bvd} term is defined by set induction.
73     >>
74 xiny 3545 prim_rw unfold_set_bvd: set_bvd{'s; x. 'a['x]} <-->
75     set_ind{'s; t, f, g. collect{'t; y. 'a['f 'y]}}
76    
77 nogin 4463 interactive_rw reduce_set_bvd {| reduce |} :
78     set_bvd{collect{'T; x. 'f['x]}; x. 'a['x]} <-->
79 xiny 3545 collect{'T; y. 'a['f['y]]}
80 nogin 4463 doc docoff
81 xiny 3545
82 xiny 3623 (************************************************************************
83     * DISPLAY FORMS *
84     ************************************************************************)
85    
86 xiny 3545 dform set_bvd_df : parens :: except_mode[src] :: set_bvd{'s; x. 'a} =
87 nogin 7563 pushm[0] `"{" slot{'a} mid slot{'x} " " Mpsymbols!member `"s " slot{'s} `"}" popm
88 xiny 3545
89 xiny 3623 (************************************************************************
90     * RULES *
91     ************************************************************************)
92    
93 jyh 5668 doc <:doc<
94 nogin 4354 @rules
95     @modsubsection{Well-formedness}
96 jyh 5668
97 nogin 4354 The set builder $@setbvd{x; s; a[x]}$ is well-formed
98     if $s$ is a set, and $a[x]$ is a family of sets.
99     >>
100 nogin 4169 interactive set_bvd_isset {| intro [] |} :
101 nogin 4570 sequent { <H> >- isset{'s} } -->
102     sequent { <H>; x: set >- isset{'a['x]} } -->
103     sequent { <H> >- isset{set_bvd{'s; x. 'a['x]}} }
104 xiny 3545
105 jyh 5668 doc <:doc<
106 nogin 4354 @modsubsection{Introduction}
107 jyh 5668
108 nogin 4354 A set $y$ is a member of $@setbvd{x; s; a[x]}$
109     if the set builder is well-formed; if $a[x]$ is
110     functional on any set argument $x$; and if
111     $@dexists{z; s; @eq{y; a[z]}}$.
112     >>
113 nogin 4169 interactive set_bvd_member_intro {| intro [] |} :
114 nogin 4570 sequent { <H> >- isset{'s} } -->
115     sequent { <H> >- isset{'y} } -->
116     sequent { <H>; x: set >- isset{'a['x]} } -->
117     sequent { <H> >- fun_set{x. 'a['x]} } -->
118     sequent { <H> >- dexists{'s; z. eq{'y; 'a['z]}} } -->
119     sequent { <H> >- mem{'y; set_bvd{'s; x. 'a['x]}} }
120 xiny 3545
121 jyh 5668 doc <:doc<
122 nogin 4354 @modsubsection{Elimination}
123 jyh 5668
124 nogin 5735 The elimination form for the set builder $@mem{y; @setbvd{x; s; a[x]}}$
125 nogin 4354 produces a witness $@mem{z; s}$ for which $@eq{y; a[z]}$.
126     >>
127 nogin 4169 interactive set_bvd_member_elim {| elim [] |} 'H :
128 nogin 4570 sequent { <H>; x: mem{'y; set_bvd{'s; x. 'a['x]}}; <J['x]> >- isset{'y} } -->
129     sequent { <H>; x: mem{'y; set_bvd{'s; x. 'a['x]}}; <J['x]> >- isset{'s} } -->
130     sequent { <H>; x: mem{'y; set_bvd{'s; x. 'a['x]}}; <J['x]>; z: set >- isset{'a['z]} } -->
131     sequent { <H>; x: mem{'y; set_bvd{'s; x. 'a['x]}}; <J['x]> >- fun_set{x. 'a['x]} } -->
132     sequent { <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] } -->
133     sequent { <H>; x: mem{'y; set_bvd{'s; x. 'a['x]}}; <J['x]> >- 'T['x] }
134 xiny 3545
135 jyh 5668 doc <:doc<
136 nogin 4354 @modsubsection{Functionality}
137 jyh 5668
138 nogin 4354 The image constructor is functional in both the set
139     argument and the mapping.
140     >>
141 nogin 4169 interactive set_bvd_fun {| intro [] |} :
142 nogin 4570 sequent { <H> >- fun_set{z. 'A['z]} } -->
143     sequent { <H>; z: set >- fun_set{x. 'B['z; 'x]} } -->
144     sequent { <H>; z: set >- fun_set{x. 'B['x; 'z]} } -->
145     ["wf"] sequent { <H>; z: set; x: set >- isset{'B['z; 'x]} } -->
146     sequent { <H> >- fun_set{z. set_bvd{'A['z]; y. 'B['z; 'y]}} }
147 nogin 7521 doc docoff
148 xiny 3623
149     (*
150     * -*-
151     * Local Variables:
152     * Caml-master: "editor.run"
153     * End:
154     * -*-
155     *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26