author | huffman |
Tue, 01 Jul 2008 06:51:59 +0200 | |
changeset 27418 | 564117b58d73 |
parent 27106 | ff27dc6e7d05 |
child 27824 | 97d2a3797ce0 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Set.thy |
2 |
ID: $Id$ |
|
12257 | 3 |
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel |
923 | 4 |
*) |
5 |
||
11979 | 6 |
header {* Set theory for higher-order logic *} |
7 |
||
15131 | 8 |
theory Set |
26800 | 9 |
imports Orderings |
15131 | 10 |
begin |
11979 | 11 |
|
12 |
text {* A set in HOL is simply a predicate. *} |
|
923 | 13 |
|
2261 | 14 |
|
11979 | 15 |
subsection {* Basic syntax *} |
2261 | 16 |
|
3947 | 17 |
global |
18 |
||
26800 | 19 |
types 'a set = "'a => bool" |
3820 | 20 |
|
923 | 21 |
consts |
11979 | 22 |
"{}" :: "'a set" ("{}") |
23 |
UNIV :: "'a set" |
|
24 |
insert :: "'a => 'a set => 'a set" |
|
25 |
Collect :: "('a => bool) => 'a set" -- "comprehension" |
|
22845 | 26 |
"op Int" :: "'a set => 'a set => 'a set" (infixl "Int" 70) |
27 |
"op Un" :: "'a set => 'a set => 'a set" (infixl "Un" 65) |
|
11979 | 28 |
UNION :: "'a set => ('a => 'b set) => 'b set" -- "general union" |
29 |
INTER :: "'a set => ('a => 'b set) => 'b set" -- "general intersection" |
|
30 |
Union :: "'a set set => 'a set" -- "union of a set" |
|
31 |
Inter :: "'a set set => 'a set" -- "intersection of a set" |
|
32 |
Pow :: "'a set => 'a set set" -- "powerset" |
|
33 |
Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers" |
|
34 |
Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers" |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
35 |
Bex1 :: "'a set => ('a => bool) => bool" -- "bounded unique existential quantifiers" |
11979 | 36 |
image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
37 |
"op :" :: "'a => 'a set => bool" -- "membership" |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
38 |
|
21210 | 39 |
notation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
40 |
"op :" ("op :") and |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
41 |
"op :" ("(_/ : _)" [50, 51] 50) |
11979 | 42 |
|
43 |
local |
|
44 |
||
923 | 45 |
|
11979 | 46 |
subsection {* Additional concrete syntax *} |
2261 | 47 |
|
19363 | 48 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
49 |
range :: "('a => 'b) => 'b set" where -- "of function" |
19363 | 50 |
"range f == f ` UNIV" |
19323 | 51 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
52 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
53 |
"not_mem x A == ~ (x : A)" -- "non-membership" |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
54 |
|
21210 | 55 |
notation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
56 |
not_mem ("op ~:") and |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
57 |
not_mem ("(_/ ~: _)" [50, 51] 50) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
58 |
|
21210 | 59 |
notation (xsymbols) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
60 |
"op Int" (infixl "\<inter>" 70) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
61 |
"op Un" (infixl "\<union>" 65) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
62 |
"op :" ("op \<in>") and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
63 |
"op :" ("(_/ \<in> _)" [50, 51] 50) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
64 |
not_mem ("op \<notin>") and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
65 |
not_mem ("(_/ \<notin> _)" [50, 51] 50) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
66 |
Union ("\<Union>_" [90] 90) and |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
67 |
Inter ("\<Inter>_" [90] 90) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
68 |
|
21210 | 69 |
notation (HTML output) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
70 |
"op Int" (infixl "\<inter>" 70) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
71 |
"op Un" (infixl "\<union>" 65) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
72 |
"op :" ("op \<in>") and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
73 |
"op :" ("(_/ \<in> _)" [50, 51] 50) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
74 |
not_mem ("op \<notin>") and |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
75 |
not_mem ("(_/ \<notin> _)" [50, 51] 50) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
76 |
|
923 | 77 |
syntax |
11979 | 78 |
"@Finset" :: "args => 'a set" ("{(_)}") |
79 |
"@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") |
|
80 |
"@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})") |
|
15535 | 81 |
"@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})") |
22439 | 82 |
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10) |
83 |
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10) |
|
84 |
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10) |
|
85 |
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10) |
|
11979 | 86 |
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10) |
87 |
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
88 |
"_Bex1" :: "pttrn => 'a set => bool => bool" ("(3EX! _:_./ _)" [0, 0, 10] 10) |
22478 | 89 |
"_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST _:_./ _)" [0, 0, 10] 10) |
18674 | 90 |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
91 |
syntax (HOL) |
11979 | 92 |
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10) |
93 |
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
94 |
"_Bex1" :: "pttrn => 'a set => bool => bool" ("(3?! _:_./ _)" [0, 0, 10] 10) |
923 | 95 |
|
96 |
translations |
|
97 |
"{x, xs}" == "insert x {xs}" |
|
98 |
"{x}" == "insert x {}" |
|
13764 | 99 |
"{x. P}" == "Collect (%x. P)" |
15535 | 100 |
"{x:A. P}" => "{x. x:A & P}" |
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset
|
101 |
"UN x y. B" == "UN x. UN y. B" |
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset
|
102 |
"UN x. B" == "UNION UNIV (%x. B)" |
13858 | 103 |
"UN x. B" == "UN x:UNIV. B" |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset
|
104 |
"INT x y. B" == "INT x. INT y. B" |
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset
|
105 |
"INT x. B" == "INTER UNIV (%x. B)" |
13858 | 106 |
"INT x. B" == "INT x:UNIV. B" |
13764 | 107 |
"UN x:A. B" == "UNION A (%x. B)" |
108 |
"INT x:A. B" == "INTER A (%x. B)" |
|
109 |
"ALL x:A. P" == "Ball A (%x. P)" |
|
110 |
"EX x:A. P" == "Bex A (%x. P)" |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
111 |
"EX! x:A. P" == "Bex1 A (%x. P)" |
18674 | 112 |
"LEAST x:A. P" => "LEAST x. x:A & P" |
113 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset
|
114 |
syntax (xsymbols) |
14381
1189a8212a12
Modified UN and INT xsymbol syntax: made index subscript
nipkow
parents:
14335
diff
changeset
|
115 |
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10) |
1189a8212a12
Modified UN and INT xsymbol syntax: made index subscript
nipkow
parents:
14335
diff
changeset
|
116 |
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
117 |
"_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10) |
18674 | 118 |
"_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10) |
14381
1189a8212a12
Modified UN and INT xsymbol syntax: made index subscript
nipkow
parents:
14335
diff
changeset
|
119 |
|
14565 | 120 |
syntax (HTML output) |
121 |
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10) |
|
122 |
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
123 |
"_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10) |
14565 | 124 |
|
15120 | 125 |
syntax (xsymbols) |
15535 | 126 |
"@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})") |
22439 | 127 |
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10) |
128 |
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10) |
|
129 |
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10) |
|
130 |
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10) |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
131 |
|
15120 | 132 |
syntax (latex output) |
22439 | 133 |
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) |
134 |
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) |
|
135 |
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10) |
|
136 |
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10) |
|
15120 | 137 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
138 |
text{* |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
139 |
Note the difference between ordinary xsymbol syntax of indexed |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
140 |
unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
141 |
and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
142 |
former does not make the index expression a subscript of the |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
143 |
union/intersection symbol because this leads to problems with nested |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
144 |
subscripts in Proof General. *} |
2261 | 145 |
|
21333 | 146 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
147 |
subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
21819 | 148 |
"subset \<equiv> less" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
149 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
150 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
151 |
subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
21819 | 152 |
"subset_eq \<equiv> less_eq" |
21333 | 153 |
|
154 |
notation (output) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
155 |
subset ("op <") and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
156 |
subset ("(_/ < _)" [50, 51] 50) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
157 |
subset_eq ("op <=") and |
21333 | 158 |
subset_eq ("(_/ <= _)" [50, 51] 50) |
159 |
||
160 |
notation (xsymbols) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
161 |
subset ("op \<subset>") and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
162 |
subset ("(_/ \<subset> _)" [50, 51] 50) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
163 |
subset_eq ("op \<subseteq>") and |
21333 | 164 |
subset_eq ("(_/ \<subseteq> _)" [50, 51] 50) |
165 |
||
166 |
notation (HTML output) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
167 |
subset ("op \<subset>") and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
168 |
subset ("(_/ \<subset> _)" [50, 51] 50) and |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
169 |
subset_eq ("op \<subseteq>") and |
21333 | 170 |
subset_eq ("(_/ \<subseteq> _)" [50, 51] 50) |
171 |
||
172 |
abbreviation (input) |
|
21819 | 173 |
supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
174 |
"supset \<equiv> greater" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
175 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21384
diff
changeset
|
176 |
abbreviation (input) |
21819 | 177 |
supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
178 |
"supset_eq \<equiv> greater_eq" |
|
179 |
||
180 |
notation (xsymbols) |
|
181 |
supset ("op \<supset>") and |
|
182 |
supset ("(_/ \<supset> _)" [50, 51] 50) and |
|
183 |
supset_eq ("op \<supseteq>") and |
|
184 |
supset_eq ("(_/ \<supseteq> _)" [50, 51] 50) |
|
21333 | 185 |
|
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
186 |
|
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
187 |
subsubsection "Bounded quantifiers" |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
188 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
189 |
syntax (output) |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
190 |
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
191 |
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
192 |
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
193 |
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
194 |
"_setleEx1" :: "[idt, 'a, bool] => bool" ("(3EX! _<=_./ _)" [0, 0, 10] 10) |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
195 |
|
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
196 |
syntax (xsymbols) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
197 |
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subset>_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
198 |
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subset>_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
199 |
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
200 |
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
201 |
"_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10) |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
202 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
203 |
syntax (HOL output) |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
204 |
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
205 |
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
206 |
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
207 |
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
208 |
"_setleEx1" :: "[idt, 'a, bool] => bool" ("(3?! _<=_./ _)" [0, 0, 10] 10) |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
209 |
|
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
210 |
syntax (HTML output) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
211 |
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subset>_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
212 |
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subset>_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
213 |
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10) |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
214 |
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
215 |
"_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10) |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
216 |
|
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
217 |
translations |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
218 |
"\<forall>A\<subset>B. P" => "ALL A. A \<subset> B --> P" |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
219 |
"\<exists>A\<subset>B. P" => "EX A. A \<subset> B & P" |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
220 |
"\<forall>A\<subseteq>B. P" => "ALL A. A \<subseteq> B --> P" |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
221 |
"\<exists>A\<subseteq>B. P" => "EX A. A \<subseteq> B & P" |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19870
diff
changeset
|
222 |
"\<exists>!A\<subseteq>B. P" => "EX! A. A \<subseteq> B & P" |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
223 |
|
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
224 |
print_translation {* |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
225 |
let |
22377 | 226 |
val Type (set_type, _) = @{typ "'a set"}; |
227 |
val All_binder = Syntax.binder_name @{const_syntax "All"}; |
|
228 |
val Ex_binder = Syntax.binder_name @{const_syntax "Ex"}; |
|
229 |
val impl = @{const_syntax "op -->"}; |
|
230 |
val conj = @{const_syntax "op &"}; |
|
231 |
val sbset = @{const_syntax "subset"}; |
|
232 |
val sbset_eq = @{const_syntax "subset_eq"}; |
|
21819 | 233 |
|
234 |
val trans = |
|
235 |
[((All_binder, impl, sbset), "_setlessAll"), |
|
236 |
((All_binder, impl, sbset_eq), "_setleAll"), |
|
237 |
((Ex_binder, conj, sbset), "_setlessEx"), |
|
238 |
((Ex_binder, conj, sbset_eq), "_setleEx")]; |
|
239 |
||
240 |
fun mk v v' c n P = |
|
241 |
if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n) |
|
242 |
then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match; |
|
243 |
||
244 |
fun tr' q = (q, |
|
245 |
fn [Const ("_bound", _) $ Free (v, Type (T, _)), Const (c, _) $ (Const (d, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] => |
|
246 |
if T = (set_type) then case AList.lookup (op =) trans (q, c, d) |
|
247 |
of NONE => raise Match |
|
248 |
| SOME l => mk v v' l n P |
|
249 |
else raise Match |
|
250 |
| _ => raise Match); |
|
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
251 |
in |
21819 | 252 |
[tr' All_binder, tr' Ex_binder] |
14804
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
253 |
end |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
254 |
*} |
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
255 |
|
8de39d3e8eb6
Corrected printer bug for bounded quantifiers Q x<=y. P
nipkow
parents:
14752
diff
changeset
|
256 |
|
11979 | 257 |
text {* |
258 |
\medskip Translate between @{text "{e | x1...xn. P}"} and @{text |
|
259 |
"{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is |
|
260 |
only translated if @{text "[0..n] subset bvs(e)"}. |
|
261 |
*} |
|
262 |
||
263 |
parse_translation {* |
|
264 |
let |
|
265 |
val ex_tr = snd (mk_binder_tr ("EX ", "Ex")); |
|
3947 | 266 |
|
11979 | 267 |
fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1 |
268 |
| nvars _ = 1; |
|
269 |
||
270 |
fun setcompr_tr [e, idts, b] = |
|
271 |
let |
|
272 |
val eq = Syntax.const "op =" $ Bound (nvars idts) $ e; |
|
273 |
val P = Syntax.const "op &" $ eq $ b; |
|
274 |
val exP = ex_tr [idts, P]; |
|
17784 | 275 |
in Syntax.const "Collect" $ Term.absdummy (dummyT, exP) end; |
11979 | 276 |
|
277 |
in [("@SetCompr", setcompr_tr)] end; |
|
278 |
*} |
|
923 | 279 |
|
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
280 |
(* To avoid eta-contraction of body: *) |
11979 | 281 |
print_translation {* |
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
282 |
let |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
283 |
fun btr' syn [A,Abs abs] = |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
284 |
let val (x,t) = atomic_abs_tr' abs |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
285 |
in Syntax.const syn $ x $ A $ t end |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
286 |
in |
13858 | 287 |
[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"), |
288 |
("UNION", btr' "@UNION"),("INTER", btr' "@INTER")] |
|
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
289 |
end |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
290 |
*} |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
291 |
|
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
292 |
print_translation {* |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
293 |
let |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
294 |
val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY")); |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
295 |
|
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
296 |
fun setcompr_tr' [Abs (abs as (_, _, P))] = |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
297 |
let |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
298 |
fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1) |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
299 |
| check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) = |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
300 |
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso |
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
301 |
((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) |
13764 | 302 |
| check _ = false |
923 | 303 |
|
11979 | 304 |
fun tr' (_ $ abs) = |
305 |
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs] |
|
306 |
in Syntax.const "@SetCompr" $ e $ idts $ Q end; |
|
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
307 |
in if check (P, 0) then tr' P |
15535 | 308 |
else let val (x as _ $ Free(xN,_), t) = atomic_abs_tr' abs |
309 |
val M = Syntax.const "@Coll" $ x $ t |
|
310 |
in case t of |
|
311 |
Const("op &",_) |
|
312 |
$ (Const("op :",_) $ (Const("_bound",_) $ Free(yN,_)) $ A) |
|
313 |
$ P => |
|
314 |
if xN=yN then Syntax.const "@Collect" $ x $ A $ P else M |
|
315 |
| _ => M |
|
316 |
end |
|
13763
f94b569cd610
added print translations tha avoid eta contraction for important binders.
nipkow
parents:
13653
diff
changeset
|
317 |
end; |
11979 | 318 |
in [("Collect", setcompr_tr')] end; |
319 |
*} |
|
320 |
||
321 |
||