combinScript.sml
1(* ===================================================================== *)
2(* FILE : combinScript.sml *)
3(* DESCRIPTION : Basic combinator definitions and some theorems about *)
4(* them. Translated from hol88. *)
5(* *)
6(* AUTHOR : (c) Tom Melham, University of Cambridge *)
7(* DATE : 87.02.26 *)
8(* TRANSLATOR : Konrad Slind, University of Calgary *)
9(* DATE : September 15, 1991 *)
10(* AUGMENTED : (kxs) added C and W combinators *)
11(* ===================================================================== *)
12Theory combin[bare]
13Libs
14 HolKernel Parse boolLib computeLib
15
16
17(*---------------------------------------------------------------------------*)
18(* Some basic combinators: function composition, S, K, I, W, and C. *)
19(*---------------------------------------------------------------------------*)
20
21fun def (s,l) p = Q.new_definition_at (DB_dtype.mkloc(s,l,false)) p
22
23val K_DEF = def(#(FILE),#(LINE))("K_DEF", ‘K = \x y. x’);
24val S_DEF = def(#(FILE),#(LINE))("S_DEF[compute]", ‘S = \f g x. f x (g x)’);
25val I_DEF = def(#(FILE),#(LINE))("I_DEF", ‘I = S K (K:'a->'a->'a)’);
26val C_DEF = def(#(FILE),#(LINE))("C_DEF[compute]", ‘C = \f x y. f y x’);
27val W_DEF = def(#(FILE),#(LINE))("W_DEF[compute]", ‘W = \f x. f x x’);
28val o_DEF = def(#(FILE),#(LINE))("o_DEF", ‘$o f g = \x. f(g x)’);
29val _ = set_fixity "o" (Infixr 800)
30val APP_DEF = def(#(FILE),#(LINE))("APP_DEF[compute]",‘$:> x f = f x’);
31
32val UPDATE_def = def(#(FILE),#(LINE))("UPDATE_def",
33 `UPDATE a b = \f c. if a = c then b else f c`);
34
35val _ = set_fixity ":>" (Infixl 310);
36val _ = set_mapped_fixity {tok = "=+", fixity = Infix(NONASSOC, 320),
37 term_name = "UPDATE"}
38val _ = Parse.Unicode.unicode_version {tmnm = "o", u = UTF8.chr 0x2218}
39val _ = TeX_notation {hol = "o", TeX = ("\\HOLTokenCompose", 1)}
40val _ = TeX_notation {hol = UTF8.chr 0x2218, TeX = ("\\HOLTokenCompose", 1)}
41
42
43val _ = add_ML_dependency "combinpp";
44val _ = combinpp.enable_dictsyntax()
45
46val _ = combinpp.new_form {
47 left = "(|", right = "|)",
48 upd_term_name = (“UPDATE k v f”, "UPDATE"),
49 lookup_term_name = NONE
50 }
51
52val _ = combinpp.new_form {
53 left = UnicodeChars.lensel, right = UnicodeChars.lenser,
54 upd_term_name = (“UPDATE k v f”, "UPDATE"),
55 lookup_term_name = NONE
56 }
57
58val s = term_to_string “UPDATE k v f”
59val _ = print ("Printing of term gives: \"" ^ s ^ "\"\n")
60
61fun texparen (s, h) =
62 TeX_notation {TeX = ("\\HOLToken" ^ s ^ "Lens{}", 1), hol = h}
63val _ = List.app texparen [("L",UnicodeChars.lensel), ("L", "(|"),
64 ("R",UnicodeChars.lenser), ("R", "|)")]
65val _ = TeX_notation {TeX = ("\\HOLTokenMapto{}", 1), hol = "↦"}
66val _ = TeX_notation {TeX = ("\\HOLTokenMapto{}", 1), hol = "|->"}
67
68local
69open OpenTheoryMap
70fun cnm s nm = OpenTheory_const_name {const={Thy="combin",Name = s}, name = nm}
71in
72 val _ = cnm "K" (["Function"],"const")
73 val _ = cnm "C" (["Function"],"flip")
74 val _ = cnm "I" (["Function"],"id")
75 val _ = cnm "o" (["Function"],"o")
76 val _ = cnm "S" (["Function","Combinator"],"s")
77 val _ = cnm "W" (["Function","Combinator"],"w")
78end
79
80(*---------------------------------------------------------------------------*
81 * In I_DEF, the type constraint is necessary in order to meet one of *
82 * the criteria for a definition : the tyvars of the lhs must be a *
83 * superset of those on the rhs. *
84 *---------------------------------------------------------------------------*)
85
86Theorem o_THM[compute]:
87 !f g x. (f o g) x = f(g x)
88Proof
89 REPEAT GEN_TAC
90 THEN PURE_REWRITE_TAC [ o_DEF ]
91 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
92 THEN REFL_TAC
93QED
94
95Theorem o_ASSOC:
96 !f g h. f o (g o h) = (f o g) o h
97Proof
98 REPEAT GEN_TAC
99 THEN REWRITE_TAC [ o_DEF ]
100 THEN CONV_TAC (REDEPTH_CONV BETA_CONV)
101 THEN REFL_TAC
102QED
103
104Theorem o_ASSOC' = GSYM o_ASSOC
105
106Theorem o_ABS_L:
107 (\x:'a. f x:'c) o (g:'b -> 'a) = (\x. f (g x))
108Proof
109 REWRITE_TAC [FUN_EQ_THM, o_THM] THEN BETA_TAC THEN REWRITE_TAC []
110QED
111
112Theorem o_ABS_R:
113 f o (\x. g x) = (\x. f (g x))
114Proof
115 REWRITE_TAC [FUN_EQ_THM, o_THM] THEN BETA_TAC THEN REWRITE_TAC []
116QED
117
118Theorem K_THM[compute]:
119 !x y. K x y = x
120Proof
121 REPEAT GEN_TAC
122 THEN PURE_REWRITE_TAC [ K_DEF ]
123 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
124 THEN REFL_TAC
125QED
126
127Theorem K_PARTIAL : (* from seqTheory *)
128 !x. K x = \z. x
129Proof
130 GEN_TAC >> PURE_REWRITE_TAC [K_DEF]
131 >> BETA_TAC >> REFL_TAC
132QED
133
134Theorem S_THM:
135 !f g x. S f g x = f x (g x)
136Proof
137 REPEAT GEN_TAC
138 THEN PURE_REWRITE_TAC [ S_DEF ]
139 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
140 THEN REFL_TAC
141QED
142
143Theorem S_ABS_L:
144 S (\x. f x) g = \x. (f x) (g x)
145Proof
146 REWRITE_TAC [FUN_EQ_THM, S_THM] THEN BETA_TAC THEN REWRITE_TAC []
147QED
148
149Theorem S_ABS_R:
150 S f (\x. g x) = \x. (f x) (g x)
151Proof
152 REWRITE_TAC [FUN_EQ_THM, S_THM] THEN BETA_TAC THEN REWRITE_TAC[]
153QED
154
155Theorem C_THM:
156 !f x y. C f x y = f y x
157Proof
158 REPEAT GEN_TAC
159 THEN PURE_REWRITE_TAC [ C_DEF ]
160 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
161 THEN REFL_TAC
162QED
163
164Theorem C_ABS_L:
165 C (\x. f x) y = (\x. f x y)
166Proof
167 REWRITE_TAC [FUN_EQ_THM, C_THM] THEN BETA_TAC THEN REWRITE_TAC []
168QED
169
170Theorem W_THM:
171 !f x. W f x = f x x
172Proof
173 REPEAT GEN_TAC
174 THEN PURE_REWRITE_TAC [ W_DEF ]
175 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
176 THEN REFL_TAC
177QED
178
179Theorem I_THM[compute]:
180 !x. I x = x
181Proof
182 REPEAT GEN_TAC
183 THEN PURE_REWRITE_TAC [ I_DEF, S_THM, K_THM ]
184 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
185 THEN REFL_TAC
186QED
187
188Theorem I_EQ_IDABS:
189 I = \x. x
190Proof
191 REWRITE_TAC[FUN_EQ_THM] >> BETA_TAC >> REWRITE_TAC[I_THM]
192QED
193
194Theorem I_o_ID:
195 !f. (I o f = f) /\ (f o I = f)
196Proof
197 REWRITE_TAC [I_THM, o_THM, FUN_EQ_THM]
198QED
199
200Theorem K_o_THM[compute]:
201 (!f v. K v o f = K v) /\ (!f v. f o K v = K (f v))
202Proof
203 REWRITE_TAC [o_THM, K_THM, FUN_EQ_THM]
204QED
205
206Theorem UPDATE_APPLY:
207 (!a x f. (a =+ x) f a = x) /\
208 (!a b x f. a <> b ==> ((a =+ x) f b = f b))
209Proof
210 REWRITE_TAC [UPDATE_def]
211 THEN BETA_TAC
212 THEN REWRITE_TAC []
213 THEN REPEAT STRIP_TAC
214 THEN ASM_REWRITE_TAC []
215QED
216
217Theorem UPDATE_APPLY1 = cj 1 UPDATE_APPLY
218
219Theorem APPLY_UPDATE_THM[compute]:
220 !f a b c. (a =+ b) f c = (if a = c then b else f c)
221Proof
222 PURE_REWRITE_TAC [UPDATE_def]
223 THEN BETA_TAC THEN REWRITE_TAC []
224QED
225
226Theorem UPDATE_COMMUTES:
227 !f a b c d. ~(a = b) ==> ((a =+ c) ((b =+ d) f) = (b =+ d) ((a =+ c) f))
228Proof
229 REPEAT STRIP_TAC
230 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM]
231 THEN BETA_TAC THEN GEN_TAC
232 THEN NTAC 2 COND_CASES_TAC
233 THEN BETA_TAC
234 THEN PURE_ASM_REWRITE_TAC []
235 THEN NTAC 2 (POP_ASSUM (fn th => RULE_ASSUM_TAC (PURE_REWRITE_RULE [th])))
236 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC []
237QED
238
239Theorem UPDATE_EQ:
240 !f a b c. (a =+ c) ((a =+ b) f) = (a =+ c) f
241Proof
242 REPEAT STRIP_TAC
243 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM]
244 THEN TRY GEN_TAC THEN BETA_TAC
245 THEN NTAC 2 (TRY COND_CASES_TAC)
246 THEN BETA_TAC THEN ASM_REWRITE_TAC []
247QED
248
249Theorem UPDATE_APPLY_ID:
250 !f a b. (f a = b) = ((a =+ b) f = f)
251Proof
252 REPEAT GEN_TAC
253 THEN EQ_TAC
254 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM]
255 THENL [
256 REPEAT STRIP_TAC
257 THEN BETA_TAC
258 THEN COND_CASES_TAC
259 THEN1 POP_ASSUM (fn th => ASM_REWRITE_TAC [SYM th])
260 THEN REWRITE_TAC [],
261 BETA_TAC THEN STRIP_TAC
262 THEN POP_ASSUM (Q.SPEC_THEN `a` ASSUME_TAC)
263 THEN RULE_ASSUM_TAC (REWRITE_RULE [])
264 THEN ASM_REWRITE_TAC []]
265QED
266
267val UPDATE_APPLY_ID' = GSYM UPDATE_APPLY_ID
268Theorem UPDATE_APPLY_ID_RWT =
269 CONJ UPDATE_APPLY_ID'
270 (CONV_RULE (STRIP_QUANT_CONV (LAND_CONV (REWR_CONV EQ_SYM_EQ)))
271 UPDATE_APPLY_ID')
272
273
274Theorem UPDATE_APPLY_IMP_ID =
275 GEN_ALL (fst (EQ_IMP_RULE (SPEC_ALL UPDATE_APPLY_ID)));
276
277Theorem APPLY_UPDATE_ID:
278 !f a. (a =+ f a) f = f
279Proof
280 REWRITE_TAC [GSYM UPDATE_APPLY_ID]
281QED
282
283Theorem UPD11_SAME_BASE:
284 !f a b c d.
285 ((a =+ c) f = (b =+ d) f) <=>
286 a = b /\ c = d \/
287 a <> b /\ (a =+ c) f = f /\ (b =+ d) f = f
288Proof
289 REPEAT GEN_TAC
290 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM]
291 THEN BETA_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC []
292 THEN ASM_CASES_TAC ``a = b`` THEN ASM_REWRITE_TAC []
293 THENL [
294 POP_ASSUM (fn th => RULE_ASSUM_TAC (PURE_REWRITE_RULE [th]))
295 THEN POP_ASSUM (Q.SPEC_THEN `b` ASSUME_TAC)
296 THEN RULE_ASSUM_TAC (REWRITE_RULE [])
297 THEN ASM_REWRITE_TAC [],
298 GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC []
299 THEN POP_ASSUM (fn th => RULE_ASSUM_TAC (PURE_REWRITE_RULE [th]))
300 THEN FIRST_ASSUM (Q.SPEC_THEN `x` ASSUME_TAC)
301 THEN Q.PAT_ASSUM `~(a = x)` (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th]))
302 THEN ASM_REWRITE_TAC []
303 ]
304QED
305
306Theorem SAME_KEY_UPDATE_DIFFER:
307 !f1 f2 a b c. ~(b = c) ==> ~((a =+ b) f = (a =+ c) f)
308Proof
309 REPEAT GEN_TAC THEN STRIP_TAC
310 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM]
311 THEN BETA_TAC
312 THEN STRIP_TAC
313 THEN POP_ASSUM (Q.SPEC_THEN `a` ASSUME_TAC)
314 THEN RULE_ASSUM_TAC (REWRITE_RULE [])
315 THEN POP_ASSUM (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th]))
316 THEN POP_ASSUM CONTR_TAC
317QED
318
319Theorem UPD11_SAME_KEY_AND_BASE:
320 !f a b c. ((a =+ b) f = (a =+ c) f) = (b = c)
321Proof
322 REPEAT GEN_TAC THEN EQ_TAC
323 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM]
324 THEN BETA_TAC THEN STRIP_TAC
325 THEN ASM_REWRITE_TAC []
326 THEN POP_ASSUM (Q.SPEC_THEN `a` ASSUME_TAC)
327 THEN RULE_ASSUM_TAC (REWRITE_RULE [])
328 THEN ASM_REWRITE_TAC []
329QED
330
331Theorem UPD_SAME_KEY_UNWIND:
332 !f1 f2 a b c.
333 ((a =+ b) f1 = (a =+ c) f2) ==>
334 (b = c) /\ !v. (a =+ v) f1 = (a =+ v) f2
335Proof
336 PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM]
337 THEN BETA_TAC THEN REPEAT STRIP_TAC
338 THENL [
339 POP_ASSUM (Q.SPEC_THEN `a` ASSUME_TAC)
340 THEN RULE_ASSUM_TAC (REWRITE_RULE [])
341 THEN ASM_REWRITE_TAC [],
342 COND_CASES_TAC THEN REWRITE_TAC []
343 THEN FIRST_ASSUM (Q.SPEC_THEN `x` ASSUME_TAC)
344 THEN Q.PAT_ASSUM `~(a = x)` (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th]))
345 THEN ASM_REWRITE_TAC []]
346QED
347
348(*---------------------------------------------------------------------------*)
349(* Theorems using combinators to specify let-movements *)
350(*---------------------------------------------------------------------------*)
351
352Theorem GEN_LET_RAND:
353 P (LET f v) = LET (P o f) v
354Proof
355 REWRITE_TAC [LET_THM, o_THM]
356QED
357
358Theorem GEN_LET_RATOR:
359 (LET f v) x = LET (C f x) v
360Proof
361 REWRITE_TAC [LET_THM, C_THM]
362QED
363
364Theorem LET_FORALL_ELIM:
365 LET f v = (!) (S ((==>) o Abbrev o (C (=) v)) f)
366Proof
367 REWRITE_TAC [S_DEF, LET_THM, C_DEF] THEN BETA_TAC THEN
368 REWRITE_TAC [o_THM, markerTheory.Abbrev_def] THEN BETA_TAC THEN
369 EQ_TAC THEN REPEAT STRIP_TAC THENL [
370 ASM_REWRITE_TAC [],
371 FIRST_X_ASSUM MATCH_MP_TAC THEN REFL_TAC
372 ]
373QED
374
375Theorem GEN_literal_case_RAND:
376 P (literal_case f v) = literal_case (P o f) v
377Proof
378 REWRITE_TAC [literal_case_THM, o_THM]
379QED
380
381Theorem GEN_literal_case_RATOR:
382 (literal_case f v) x = literal_case (C f x) v
383Proof
384 REWRITE_TAC [literal_case_THM, C_THM]
385QED
386
387Theorem literal_case_FORALL_ELIM:
388 literal_case f v = (!) (S ((==>) o Abbrev o (C (=) v)) f)
389Proof
390 REWRITE_TAC [S_DEF, literal_case_THM, C_DEF] THEN BETA_TAC THEN
391 REWRITE_TAC [o_THM, markerTheory.Abbrev_def] THEN BETA_TAC THEN
392 EQ_TAC THEN REPEAT STRIP_TAC THENL [
393 ASM_REWRITE_TAC [],
394 FIRST_X_ASSUM MATCH_MP_TAC THEN REFL_TAC
395 ]
396QED
397
398(* ----------------------------------------------------------------------
399 Predicates on functions
400 ---------------------------------------------------------------------- *)
401
402val ASSOC_DEF = new_definition("ASSOC_DEF",
403 ``
404 ASSOC (f:'a->'a->'a) <=> (!x y z. f x (f y z) = f (f x y) z)
405 ``);
406
407val COMM_DEF = new_definition("COMM_DEF",
408 ``
409 COMM (f:'a->'a->'b) <=> (!x y. f x y = f y x)
410 ``);
411
412val FCOMM_DEF = new_definition("FCOMM_DEF",
413 ``
414 FCOMM (f:'a->'b->'a) (g:'c->'a->'a) <=> (!x y z. g x (f y z) = f (g x y) z)
415 ``);
416
417val RIGHT_ID_DEF = new_definition("RIGHT_ID_DEF",
418 ``
419 RIGHT_ID (f:'a->'b->'a) e <=> (!x. f x e = x)
420 ``);
421
422val LEFT_ID_DEF = new_definition("LEFT_ID_DEF",
423 ``
424 LEFT_ID (f:'a->'b->'b) e <=> (!x. f e x = x)
425 ``);
426
427val MONOID_DEF = new_definition("MONOID_DEF",
428 ``
429 MONOID (f:'a->'a->'a) e <=>
430 ASSOC f /\ RIGHT_ID f e /\ LEFT_ID f e
431 ``);
432
433(* ======================================================================== *)
434(* Theorems about operators *)
435(* ======================================================================== *)
436
437Theorem ASSOC_CONJ: ASSOC $/\
438Proof
439 REWRITE_TAC[ASSOC_DEF,CONJ_ASSOC]
440QED
441
442Theorem ASSOC_SYM =
443 CONV_RULE
444 (STRIP_QUANT_CONV (RHS_CONV (STRIP_QUANT_CONV SYM_CONV)))
445 ASSOC_DEF;
446
447
448Theorem ASSOC_DISJ:
449 ASSOC $\/
450Proof
451 REWRITE_TAC[ASSOC_DEF,DISJ_ASSOC]
452QED
453
454Theorem FCOMM_ASSOC:
455 !f: 'a->'a->'a. FCOMM f f = ASSOC f
456Proof
457 REWRITE_TAC[ASSOC_DEF,FCOMM_DEF]
458QED
459
460Theorem MONOID_CONJ_T:
461 MONOID $/\ T
462Proof
463 REWRITE_TAC[MONOID_DEF,CONJ_ASSOC, LEFT_ID_DEF,ASSOC_DEF,RIGHT_ID_DEF]
464QED
465
466Theorem MONOID_DISJ_F:
467 MONOID $\/ F
468Proof
469 REWRITE_TAC[MONOID_DEF,DISJ_ASSOC,
470 LEFT_ID_DEF,ASSOC_DEF,RIGHT_ID_DEF]
471QED
472
473(*---------------------------------------------------------------------------*)
474(* Congruence rule for composition. Grist for the termination condition *)
475(* extractor. *)
476(*---------------------------------------------------------------------------*)
477
478Theorem o_CONG:
479 !a1 a2 g1 g2 f1 f2.
480 a1 = a2 /\
481 (!x. x = a2 ==> g1 x = g2 x) /\
482 (!y. y = g2 a2 ==> f1 y = f2 y)
483 ==>
484 (f1 o g1) a1 = (f2 o g2) a2
485Proof
486 REPEAT STRIP_TAC THEN
487 Q.PAT_X_ASSUM `a1 = a2` (SUBST_ALL_TAC o SYM) THEN
488 POP_ASSUM (MP_TAC o Q.SPEC `g1 a1`) THEN
489 POP_ASSUM (MP_TAC o Q.SPEC `a1`) THEN
490 REWRITE_TAC[o_DEF] THEN BETA_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[]
491QED
492
493(*---------------------------------------------------------------------------*)
494(* Tag combinator equal to K. Used in generating ML from HOL *)
495(*---------------------------------------------------------------------------*)
496
497val FAIL_DEF = Q.new_definition("FAIL_DEF", `FAIL = \x y. x`);
498
499Theorem FAIL_THM: FAIL x y = x
500Proof
501 REPEAT GEN_TAC
502 THEN PURE_REWRITE_TAC [ FAIL_DEF ]
503 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
504 THEN REFL_TAC
505QED
506
507
508Overload flip = “C”
509
510val _ = remove_ovl_mapping "C" {Name="C", Thy = "combin"}
511
512(* ------------------------------------------------------------------------- *)
513(* "Extensional" functions, mapping to a fixed value ARB outside the domain. *)
514(* Even though these are still total, they're a conveniently better model *)
515(* of the partial function space (e.g. the space has the right cardinality). *)
516(* *)
517(* (Ported from HOL-Light's sets.ml by Chun Tian) *)
518(* ------------------------------------------------------------------------- *)
519
520(* NOTE: the original definition in HOL-Light was:
521
522 EXTENSIONAL s = {f :'a->'b | !x. x NOTIN s ==> f x = ARB}
523 *)
524val EXTENSIONAL_def = new_definition
525 ("EXTENSIONAL_def",
526 “EXTENSIONAL s (f :'a->'b) <=> !x. ~(x IN s) ==> f x = ARB”);
527
528Theorem IN_EXTENSIONAL :
529 !s (f :'a->'b). f IN EXTENSIONAL s <=> (!x. ~(x IN s) ==> f x = ARB)
530Proof
531 REWRITE_TAC [IN_DEF]
532 >> BETA_TAC
533 >> rpt GEN_TAC
534 >> REWRITE_TAC [FUN_EQ_THM, EXTENSIONAL_def, IN_DEF]
535 >> BETA_TAC
536 >> REWRITE_TAC []
537QED
538
539Theorem IN_EXTENSIONAL_UNDEFINED :
540 !s (f :'a->'b) x. f IN EXTENSIONAL s /\ ~(x IN s) ==> f x = ARB
541Proof
542 REWRITE_TAC [IN_EXTENSIONAL]
543 >> rpt STRIP_TAC
544 >> FIRST_X_ASSUM MATCH_MP_TAC
545 >> ASM_REWRITE_TAC []
546QED
547
548(* ------------------------------------------------------------------------- *)
549(* Restriction of a function to an EXTENSIONAL one on a subset. *)
550(* *)
551(* NOTE: It's put here, so that RESTRICT in relationTheory can be defined *)
552(* upon RESTRICTION. More theorems about RESTRICTION and EXTENSIONAL *)
553(* are in pred_setTheory. *)
554(* ------------------------------------------------------------------------- *)
555
556val RESTRICTION = new_definition
557 ("RESTRICTION",
558 “RESTRICTION s (f :'a->'b) x = if x IN s then f x else ARB”);
559
560Theorem RESTRICTION_THM :
561 !s (f :'a->'b). RESTRICTION s f = \x. if x IN s then f x else ARB
562Proof
563 rpt GEN_TAC
564 >> REWRITE_TAC[FUN_EQ_THM, RESTRICTION]
565 >> BETA_TAC
566 >> REWRITE_TAC []
567QED
568
569Theorem RESTRICTION_DEFINED :
570 !s (f :'a->'b) x. x IN s ==> RESTRICTION s f x = f x
571Proof
572 rpt GEN_TAC
573 >> REWRITE_TAC [RESTRICTION]
574 >> COND_CASES_TAC >> REWRITE_TAC []
575QED
576
577Theorem RESTRICTION_UNDEFINED :
578 !s (f :'a->'b) x. ~(x IN s) ==> RESTRICTION s f x = ARB
579Proof
580 rpt GEN_TAC
581 >> REWRITE_TAC [RESTRICTION]
582 >> COND_CASES_TAC >> REWRITE_TAC []
583QED
584
585Theorem RESTRICTION_EQ :
586 !s (f :'a->'b) x y. x IN s /\ f x = y ==> RESTRICTION s f x = y
587Proof
588 rpt STRIP_TAC
589 >> POP_ASSUM (fn th => (ONCE_REWRITE_TAC [SYM th]))
590 >> MATCH_MP_TAC RESTRICTION_DEFINED
591 >> ASM_REWRITE_TAC []
592QED
593
594(* NOTE: HOL-Light doesn't have this theorem. *)
595Theorem EXTENSIONAL_RESTRICTION :
596 !s (f :'a->'b). EXTENSIONAL s (RESTRICTION s (f :'a -> 'b))
597Proof
598 REWRITE_TAC [EXTENSIONAL_def, RESTRICTION, IN_DEF]
599 >> BETA_TAC
600 >> rpt STRIP_TAC
601 >> reverse COND_CASES_TAC >- REFL_TAC
602 >> POP_ASSUM MP_TAC
603 >> ASM_REWRITE_TAC []
604QED