20 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
20 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
21 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
21 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
22 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
22 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
23 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
23 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
24 |
24 |
25 |
25 subsection {* The type of predicate enumerations (a monad) *} |
26 subsection {* Classical rules for reasoning on predicates *} |
|
27 |
|
28 declare predicate1D [Pure.dest?, dest?] |
|
29 declare predicate2I [Pure.intro!, intro!] |
|
30 declare predicate2D [Pure.dest, dest] |
|
31 declare bot1E [elim!] |
|
32 declare bot2E [elim!] |
|
33 declare top1I [intro!] |
|
34 declare top2I [intro!] |
|
35 declare inf1I [intro!] |
|
36 declare inf2I [intro!] |
|
37 declare inf1E [elim!] |
|
38 declare inf2E [elim!] |
|
39 declare sup1I1 [intro?] |
|
40 declare sup2I1 [intro?] |
|
41 declare sup1I2 [intro?] |
|
42 declare sup2I2 [intro?] |
|
43 declare sup1E [elim!] |
|
44 declare sup2E [elim!] |
|
45 declare sup1CI [intro!] |
|
46 declare sup2CI [intro!] |
|
47 declare INF1_I [intro!] |
|
48 declare INF2_I [intro!] |
|
49 declare INF1_D [elim] |
|
50 declare INF2_D [elim] |
|
51 declare INF1_E [elim] |
|
52 declare INF2_E [elim] |
|
53 declare SUP1_I [intro] |
|
54 declare SUP2_I [intro] |
|
55 declare SUP1_E [elim!] |
|
56 declare SUP2_E [elim!] |
|
57 |
|
58 |
|
59 subsection {* Conversion between set and predicate relations *} |
|
60 |
|
61 subsubsection {* Equality *} |
|
62 |
|
63 lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)" |
|
64 by (simp add: set_eq_iff fun_eq_iff) |
|
65 |
|
66 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)" |
|
67 by (simp add: set_eq_iff fun_eq_iff) |
|
68 |
|
69 |
|
70 subsubsection {* Order relation *} |
|
71 |
|
72 lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" |
|
73 by (simp add: subset_iff le_fun_def) |
|
74 |
|
75 lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" |
|
76 by (simp add: subset_iff le_fun_def) |
|
77 |
|
78 |
|
79 subsubsection {* Top and bottom elements *} |
|
80 |
|
81 lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})" |
|
82 by (auto simp add: fun_eq_iff) |
|
83 |
|
84 lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})" |
|
85 by (auto simp add: fun_eq_iff) |
|
86 |
|
87 |
|
88 subsubsection {* Binary intersection *} |
|
89 |
|
90 lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" |
|
91 by (simp add: inf_fun_def) |
|
92 |
|
93 lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" |
|
94 by (simp add: inf_fun_def) |
|
95 |
|
96 |
|
97 subsubsection {* Binary union *} |
|
98 |
|
99 lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" |
|
100 by (simp add: sup_fun_def) |
|
101 |
|
102 lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" |
|
103 by (simp add: sup_fun_def) |
|
104 |
|
105 |
|
106 subsubsection {* Intersections of families *} |
|
107 |
|
108 lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))" |
|
109 by (simp add: INF_apply fun_eq_iff) |
|
110 |
|
111 lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))" |
|
112 by (simp add: INF_apply fun_eq_iff) |
|
113 |
|
114 |
|
115 subsubsection {* Unions of families *} |
|
116 |
|
117 lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))" |
|
118 by (simp add: SUP_apply fun_eq_iff) |
|
119 |
|
120 lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))" |
|
121 by (simp add: SUP_apply fun_eq_iff) |
|
122 |
|
123 |
|
124 subsection {* Predicates as relations *} |
|
125 |
|
126 subsubsection {* Composition *} |
|
127 |
|
128 inductive pred_comp :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75) |
|
129 for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where |
|
130 pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c" |
|
131 |
|
132 inductive_cases pred_compE [elim!]: "(r OO s) a c" |
|
133 |
|
134 lemma pred_comp_rel_comp_eq [pred_set_conv]: |
|
135 "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)" |
|
136 by (auto simp add: fun_eq_iff) |
|
137 |
|
138 |
|
139 subsubsection {* Converse *} |
|
140 |
|
141 inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000) |
|
142 for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where |
|
143 conversepI: "r a b \<Longrightarrow> r^--1 b a" |
|
144 |
|
145 notation (xsymbols) |
|
146 conversep ("(_\<inverse>\<inverse>)" [1000] 1000) |
|
147 |
|
148 lemma conversepD: |
|
149 assumes ab: "r^--1 a b" |
|
150 shows "r b a" using ab |
|
151 by cases simp |
|
152 |
|
153 lemma conversep_iff [iff]: "r^--1 a b = r b a" |
|
154 by (iprover intro: conversepI dest: conversepD) |
|
155 |
|
156 lemma conversep_converse_eq [pred_set_conv]: |
|
157 "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)" |
|
158 by (auto simp add: fun_eq_iff) |
|
159 |
|
160 lemma conversep_conversep [simp]: "(r^--1)^--1 = r" |
|
161 by (iprover intro: order_antisym conversepI dest: conversepD) |
|
162 |
|
163 lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1" |
|
164 by (iprover intro: order_antisym conversepI pred_compI |
|
165 elim: pred_compE dest: conversepD) |
|
166 |
|
167 lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1" |
|
168 by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) |
|
169 |
|
170 lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1" |
|
171 by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) |
|
172 |
|
173 lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>" |
|
174 by (auto simp add: fun_eq_iff) |
|
175 |
|
176 lemma conversep_eq [simp]: "(op =)^--1 = op =" |
|
177 by (auto simp add: fun_eq_iff) |
|
178 |
|
179 |
|
180 subsubsection {* Domain *} |
|
181 |
|
182 inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
|
183 for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where |
|
184 DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a" |
|
185 |
|
186 inductive_cases DomainPE [elim!]: "DomainP r a" |
|
187 |
|
188 lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)" |
|
189 by (blast intro!: Orderings.order_antisym predicate1I) |
|
190 |
|
191 |
|
192 subsubsection {* Range *} |
|
193 |
|
194 inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" |
|
195 for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where |
|
196 RangePI [intro]: "r a b \<Longrightarrow> RangeP r b" |
|
197 |
|
198 inductive_cases RangePE [elim!]: "RangeP r b" |
|
199 |
|
200 lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)" |
|
201 by (blast intro!: Orderings.order_antisym predicate1I) |
|
202 |
|
203 |
|
204 subsubsection {* Inverse image *} |
|
205 |
|
206 definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where |
|
207 "inv_imagep r f = (\<lambda>x y. r (f x) (f y))" |
|
208 |
|
209 lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)" |
|
210 by (simp add: inv_image_def inv_imagep_def) |
|
211 |
|
212 lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)" |
|
213 by (simp add: inv_imagep_def) |
|
214 |
|
215 |
|
216 subsubsection {* Powerset *} |
|
217 |
|
218 definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
219 "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)" |
|
220 |
|
221 lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)" |
|
222 by (auto simp add: Powp_def fun_eq_iff) |
|
223 |
|
224 lemmas Powp_mono [mono] = Pow_mono [to_pred] |
|
225 |
|
226 |
|
227 subsubsection {* Properties of relations *} |
|
228 |
|
229 abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
230 "antisymP r \<equiv> antisym {(x, y). r x y}" |
|
231 |
|
232 abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
233 "transP r \<equiv> trans {(x, y). r x y}" |
|
234 |
|
235 abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where |
|
236 "single_valuedP r \<equiv> single_valued {(x, y). r x y}" |
|
237 |
|
238 (*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*) |
|
239 |
|
240 definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
241 "reflp r \<longleftrightarrow> refl {(x, y). r x y}" |
|
242 |
|
243 definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
244 "symp r \<longleftrightarrow> sym {(x, y). r x y}" |
|
245 |
|
246 definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
247 "transp r \<longleftrightarrow> trans {(x, y). r x y}" |
|
248 |
|
249 lemma reflpI: |
|
250 "(\<And>x. r x x) \<Longrightarrow> reflp r" |
|
251 by (auto intro: refl_onI simp add: reflp_def) |
|
252 |
|
253 lemma reflpE: |
|
254 assumes "reflp r" |
|
255 obtains "r x x" |
|
256 using assms by (auto dest: refl_onD simp add: reflp_def) |
|
257 |
|
258 lemma sympI: |
|
259 "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r" |
|
260 by (auto intro: symI simp add: symp_def) |
|
261 |
|
262 lemma sympE: |
|
263 assumes "symp r" and "r x y" |
|
264 obtains "r y x" |
|
265 using assms by (auto dest: symD simp add: symp_def) |
|
266 |
|
267 lemma transpI: |
|
268 "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" |
|
269 by (auto intro: transI simp add: transp_def) |
|
270 |
|
271 lemma transpE: |
|
272 assumes "transp r" and "r x y" and "r y z" |
|
273 obtains "r x z" |
|
274 using assms by (auto dest: transD simp add: transp_def) |
|
275 |
|
276 |
|
277 subsection {* Predicates as enumerations *} |
|
278 |
|
279 subsubsection {* The type of predicate enumerations (a monad) *} |
|
280 |
26 |
281 datatype 'a pred = Pred "'a \<Rightarrow> bool" |
27 datatype 'a pred = Pred "'a \<Rightarrow> bool" |
282 |
28 |
283 primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where |
29 primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where |
284 eval_pred: "eval (Pred f) = f" |
30 eval_pred: "eval (Pred f) = f" |