/[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 8705 - (show 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 doc <:doc<
2 @module[Czf_itt_set_bvd]
3
4 The @tt[Czf_itt_set_bvd] module defines the @emph{image} of a set
5 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
11 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
14 @docoff
15 ----------------------------------------------------------------
16
17 @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
22 See the file doc/htmlman/default.html or visit http://metaprl.org/
23 for more information.
24
25 Copyright (C) 2002 Xin Yu, Caltech
26
27 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
32 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
37 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
41 Author: Xin Yu
42 @email{xiny@cs.caltech.edu}
43 @end[license]
44 >>
45
46
47 extends Czf_itt_dall
48 extends Czf_itt_dexists
49 doc docoff
50
51 open Lm_debug
52 open Lm_printf
53
54 open Dtactic
55 open Top_conversionals
56
57 (************************************************************************
58 * TERMS *
59 ************************************************************************)
60
61
62 declare set_bvd{'s; x. 'a['x]} (* { a(x) | x in s } *)
63 doc docoff
64
65 (************************************************************************
66 * REWRITES *
67 ************************************************************************)
68
69 doc <:doc<
70 @rewrites
71
72 The @tt{set_bvd} term is defined by set induction.
73 >>
74 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 interactive_rw reduce_set_bvd {| reduce |} :
78 set_bvd{collect{'T; x. 'f['x]}; x. 'a['x]} <-->
79 collect{'T; y. 'a['f['y]]}
80 doc docoff
81
82 (************************************************************************
83 * DISPLAY FORMS *
84 ************************************************************************)
85
86 dform set_bvd_df : parens :: except_mode[src] :: set_bvd{'s; x. 'a} =
87 pushm[0] `"{" slot{'a} mid slot{'x} " " Mpsymbols!member `"s " slot{'s} `"}" popm
88
89 (************************************************************************
90 * RULES *
91 ************************************************************************)
92
93 doc <:doc<
94 @rules
95 @modsubsection{Well-formedness}
96
97 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 interactive set_bvd_isset {| intro [] |} :
101 sequent { <H> >- isset{'s} } -->
102 sequent { <H>; x: set >- isset{'a['x]} } -->
103 sequent { <H> >- isset{set_bvd{'s; x. 'a['x]}} }
104
105 doc <:doc<
106 @modsubsection{Introduction}
107
108 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 interactive set_bvd_member_intro {| intro [] |} :
114 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
121 doc <:doc<
122 @modsubsection{Elimination}
123
124 The elimination form for the set builder $@mem{y; @setbvd{x; s; a[x]}}$
125 produces a witness $@mem{z; s}$ for which $@eq{y; a[z]}$.
126 >>
127 interactive set_bvd_member_elim {| elim [] |} 'H :
128 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
135 doc <:doc<
136 @modsubsection{Functionality}
137
138 The image constructor is functional in both the set
139 argument and the mapping.
140 >>
141 interactive set_bvd_fun {| intro [] |} :
142 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 doc docoff
148
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