sumScript.sml
1(* ===================================================================== *)
2(* FILE : sumScript.sml *)
3(* DESCRIPTION : Creates a theory containing the logical definition of *)
4(* the sum type operator. The sum type is defined and *)
5(* the following `axiomatization` is proven from the *)
6(* definition of the type: *)
7(* *)
8(* |- !f g. ?!h. (h o INL = f) /\ (h o INR = g) *)
9(* *)
10(* Using this axiom, the following standard theorems are *)
11(* proven. *)
12(* *)
13(* |- ISL (INL a) |- ISR (INR b) *)
14(* |- ~ISL (INR b) |- ~ISR (INL a) *)
15(* |- OUTL (INL a) = a |- OUTR (INR b) = b *)
16(* |- ISL(x) ==> INL (OUTL x)=x *)
17(* |- ISR(x) ==> INR (OUTR x)=x *)
18(* |- !x. ISL x \/ ISR x *)
19(* *)
20(* Also defines an infix SUM such that f SUM g denotes *)
21(* the unique function asserted to exist by the axiom. *)
22(* Translated from hol88. *)
23(* *)
24(* AUTHOR : (c) Tom Melham, University of Cambridge *)
25(* DATE : 86.11.24 *)
26(* REVISED : 87.03.14 *)
27(* TRANSLATOR : Konrad Slind, University of Calgary *)
28(* DATE : September 15, 1991 *)
29(* ===================================================================== *)
30
31Theory sum[bare]
32Ancestors[qualified]
33 (* done to keep Holmake happy - satTheory is an ancestor of BasicProvers *)
34 sat
35Libs
36 HolKernel Parse boolLib BasicProvers quotientLib boolSimps
37 simpLib DefnBase[qualified] OpenTheoryMap[qualified]
38
39fun simp ths = simpLib.asm_simp_tac (srw_ss()) ths (* don't eta reduce *)
40
41val o_DEF = combinTheory.o_DEF
42and o_THM = combinTheory.o_THM;
43
44(* ---------------------------------------------------------------------*)
45(* Introduce the new type. *)
46(* *)
47(* The sum of types `:'a` and `:'b` will be represented by a certain *)
48(* subset of type `:bool->'a->'b->bool`. A left injection of value *)
49(* `p:'a` will be represented by: `\b x y. x=p /\ b`. A right injection*)
50(* of value `q:'b` will be represented by: `\b x y. x=q /\ ~b`. *)
51(* The predicate IS_SUM_REP is true of just those objects of the type *)
52(* `:bool->'a->'b->bool` which are representations of some injection. *)
53(* ---------------------------------------------------------------------*)
54
55
56val IS_SUM_REP =
57 new_definition
58 ("IS_SUM_REP",
59 “IS_SUM_REP (f:bool->'a->'b->bool) =
60 ?v1 v2. (f = \b x y.(x=v1) /\ b) \/
61 (f = \b x y.(y=v2) /\ ~b)”);
62
63(* Prove that there exists some object in the representing type that *)
64(* lies in the subset of legal representations. *)
65
66val EXISTS_SUM_REP =
67 TAC_PROOF(([], “?f:bool -> 'a -> 'b -> bool. IS_SUM_REP f”),
68 EXISTS_TAC “\b x (y:'b). (x = @(x:'a).T) /\ b” THEN
69 PURE_ONCE_REWRITE_TAC [IS_SUM_REP] THEN
70 EXISTS_TAC “@(x:'a).T” THEN
71 REWRITE_TAC []);
72
73(* ---------------------------------------------------------------------*)
74(* Use the type definition mechanism to introduce the new type. *)
75(* The theorem returned is: |- ?rep. TYPE_DEFINITION IS_SUM_REP rep *)
76(* ---------------------------------------------------------------------*)
77
78val sum_TY_DEF = new_type_definition ("sum", EXISTS_SUM_REP);
79val _ = add_infix_type {Prec = 60, ParseName = SOME "+", Name = "sum",
80 Assoc = HOLgrammars.RIGHT}
81
82
83(*---------------------------------------------------------------------------*)
84(* Define a representation function, REP_sum, from the type ('a,'b)sum to *)
85(* the representing type bool->'a->'b->bool, and the inverse abstraction *)
86(* function ABS_sum, and prove some trivial lemmas about them. *)
87(*---------------------------------------------------------------------------*)
88
89val sum_ISO_DEF = define_new_type_bijections
90 {name = "sum_ISO_DEF",
91 ABS = "ABS_sum",
92 REP = "REP_sum",
93 tyax = sum_TY_DEF};
94
95
96val R_A = GEN_ALL (SYM (SPEC_ALL (CONJUNCT2 sum_ISO_DEF)))
97and R_11 = SYM(SPEC_ALL (prove_rep_fn_one_one sum_ISO_DEF))
98and A_ONTO = REWRITE_RULE [IS_SUM_REP] (prove_abs_fn_onto sum_ISO_DEF);
99
100(* --------------------------------------------------------------------- *)
101(* The definitions of the constants INL and INR follow: *)
102(* --------------------------------------------------------------------- *)
103
104(* Define the injection function INL:'a->('a,'b)sum *)
105val INL_DEF = new_definition("INL_DEF[notuserdef]",
106 “!e.(INL:'a->(('a,'b)sum)) e = ABS_sum(\b x (y:'b). (x = e) /\ b)”);
107
108(* Define the injection function INR:'b->( 'a,'b )sum *)
109val INR_DEF = new_definition("INR_DEF[notuserdef]",
110 “!e.(INR:'b->(('a,'b)sum)) e = ABS_sum(\b (x:'a) y. (y = e) /\ ~b)”);
111
112(* --------------------------------------------------------------------- *)
113(* The proof of the `axiom` for sum types follows. *)
114(* --------------------------------------------------------------------- *)
115
116val SIMP = REWRITE_RULE [];
117fun REWRITE1_TAC th = REWRITE_TAC [th];
118
119(* Prove that REP_sum(INL v) gives the representation of INL v. *)
120val REP_INL = TAC_PROOF(([],
121 “REP_sum (INL v) = \b x (y:'b). ((x:'a) = v) /\ b”),
122 PURE_REWRITE_TAC [INL_DEF,R_A,IS_SUM_REP] THEN
123 EXISTS_TAC “v:'a” THEN
124 REWRITE_TAC[]);
125
126
127(* Prove that REP_sum(INR v) gives the representation of INR v. *)
128val REP_INR = TAC_PROOF(([],
129 “REP_sum (INR v) = \b (x:'a) y. ((y:'b) = v) /\ ~b”),
130 PURE_REWRITE_TAC [INR_DEF,R_A,IS_SUM_REP] THEN
131 MAP_EVERY EXISTS_TAC [“v:'a”,“v:'b”] THEN
132 DISJ2_TAC THEN
133 REFL_TAC);
134
135(* Prove that INL is one-to-one *)
136Theorem INL_11:
137 (INL x = ((INL y):('a,'b)sum)) = (x = y)
138Proof
139 EQ_TAC THENL
140 [PURE_REWRITE_TAC [R_11,REP_INL] THEN
141 CONV_TAC (REDEPTH_CONV (FUN_EQ_CONV ORELSEC BETA_CONV)) THEN
142 DISCH_THEN (ACCEPT_TAC o SIMP o SPECL [“T”,“x:'a”,“y:'b”]),
143 DISCH_THEN SUBST1_TAC THEN REFL_TAC]
144QED
145
146(* Prove that INR is one-to-one *)
147Theorem INR_11:
148 (INR x = (INR y:('a,'b)sum)) = (x = y)
149Proof
150 EQ_TAC THENL
151 [PURE_REWRITE_TAC [R_11,REP_INR] THEN
152 CONV_TAC (REDEPTH_CONV (FUN_EQ_CONV ORELSEC BETA_CONV)) THEN
153 DISCH_THEN (ACCEPT_TAC o SYM o SIMP o SPECL[“F”,“x:'a”,“y:'b”]),
154 DISCH_THEN SUBST1_TAC THEN REFL_TAC]
155QED
156
157Theorem INR_INL_11[simp] =
158 CONJ (GEN_ALL INL_11) (GEN_ALL INR_11);
159
160(* Prove that left injections and right injections are not equal. *)
161Theorem INR_neq_INL:
162 !v1 v2. ~(INR v2 :('a,'b)sum = INL v1)
163Proof
164 PURE_REWRITE_TAC [R_11,REP_INL,REP_INR] THEN
165 REPEAT GEN_TAC THEN
166 CONV_TAC (REDEPTH_CONV (FUN_EQ_CONV ORELSEC BETA_CONV)) THEN
167 DISCH_THEN (CONTR_TAC o SIMP o SPECL [“T”,“v1:'a”,“v2:'b”])
168QED
169
170(*----------------------------------------------------------------------*)
171(* The abstract `axiomatization` of the sum type consists of the single *)
172(* theorem given below: *)
173(* *)
174(* sum_axiom |- !f g. ?!h. (h o INL = f) /\ (h o INR = g) *)
175(* *)
176(* The definitions of the usual operators ISL, OUTL, etc. follow from *)
177(* this axiom. *)
178(*----------------------------------------------------------------------*)
179
180Theorem sum_axiom:
181 !(f:'a->'c).
182 !(g:'b->'c).
183 ?!h. ((h o INL) = f) /\ ((h o INR) = g)
184Proof
185PURE_REWRITE_TAC [boolTheory.EXISTS_UNIQUE_DEF,o_DEF] THEN
186CONV_TAC (REDEPTH_CONV (BETA_CONV ORELSEC FUN_EQ_CONV)) THEN
187REPEAT (FILTER_STRIP_TAC “x:('a,'b)sum->'c”) THENL
188[EXISTS_TAC (“\(x:('a,'b)sum). if (?v1. x = INL v1)
189 then f(@v1.x = INL v1)
190 else g(@v2.x = INR v2):'c”) THEN
191 simpLib.SIMP_TAC boolSimps.bool_ss [
192 INL_11,INR_11,INR_neq_INL,SELECT_REFL_2
193 ],
194 REPEAT GEN_TAC THEN DISCH_THEN (CONJUNCTS_THEN2 MP_TAC
195 (REWRITE1_TAC o (CONV_RULE (ONCE_DEPTH_CONV SYM_CONV)))) THEN
196 REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC (SPEC “s:('a,'b)sum” A_ONTO) THEN
197 ASM_REWRITE_TAC (map (SYM o SPEC_ALL) [INL_DEF,INR_DEF])]
198QED
199
200
201(* ---------------------------------------------------------------------*)
202(* We also prove a version of sum_axiom which is in a form suitable for *)
203(* use with the recursive type definition tools. *)
204(* ---------------------------------------------------------------------*)
205
206Theorem sum_Axiom0[local]:
207 !f:'a->'c.
208 !g:'b->'c.
209 ?!h. (!x. h(INL x) = f x) /\
210 (!y. h(INR y) = g y)
211Proof
212 let val cnv = CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) sum_axiom
213 val rew = SPEC_ALL (REWRITE_RULE [o_THM] cnv)
214 in
215 MATCH_ACCEPT_TAC rew
216 end
217QED
218
219Theorem sum_INDUCT =
220 Prim_rec.prove_induction_thm sum_Axiom0;
221
222Theorem sum_Axiom:
223 !(f:'a -> 'c) (g:'b -> 'c).
224 ?h. (!x. h (INL x) = f x) /\ (!y. h (INR y) = g y)
225Proof
226 REPEAT GEN_TAC THEN
227 STRIP_ASSUME_TAC
228 ((SPECL [Term`f:'a -> 'c`, Term`g:'b -> 'c`] o
229 Ho_Rewrite.REWRITE_RULE [EXISTS_UNIQUE_THM]) sum_Axiom0) THEN
230 EXISTS_TAC (Term`h:'a + 'b -> 'c`) THEN
231 ASM_REWRITE_TAC []
232QED
233
234val [sum_case_def] = Prim_rec.define_case_constant sum_Axiom
235val _ = export_rewrites ["sum_case_def"]
236Overload case = ``sum_CASE``
237
238
239val _ = TypeBase.export $ TypeBasePure.gen_datatype_info
240 {ax=sum_Axiom, case_defs=[sum_case_def], ind=sum_INDUCT}
241
242Theorem FORALL_SUM:
243 (!s. P s) <=> (!x. P (INL x)) /\ (!y. P (INR y))
244Proof
245 EQ_TAC THENL [DISCH_TAC THEN ASM_REWRITE_TAC [],
246 MATCH_ACCEPT_TAC sum_INDUCT]
247QED
248
249(* !P. (?s. P s) <=> (?x. P (INL x)) \/ (?y. P (INR y)) *)
250Theorem EXISTS_SUM =
251 FORALL_SUM |> Q.INST [`P` |-> `\x. ~P x`] |> AP_TERM ``$~``
252 |> CONV_RULE (BINOP_CONV (SIMP_CONV bool_ss []))
253 |> Q.GEN `P`
254
255
256Theorem sum_CASES =
257 hd (Prim_rec.prove_cases_thm sum_INDUCT);
258
259Theorem sum_distinct[simp]:
260 !x:'a y:'b. ~(INL x = INR y)
261Proof
262 REPEAT STRIP_TAC THEN
263 STRIP_ASSUME_TAC ((BETA_RULE o REWRITE_RULE [EXISTS_UNIQUE_DEF] o
264 Q.ISPECL [`\x:'a. T`, `\y:'b. F`]) sum_Axiom) THEN
265 FIRST_X_ASSUM (MP_TAC o AP_TERM (Term`h:'a + 'b -> bool`)) THEN
266 ASM_REWRITE_TAC []
267QED
268
269Theorem sum_distinct1 = GSYM sum_distinct;
270
271(* ---------------------------------------------------------------------*)
272(* The definitions of ISL, ISR, OUTL, OUTR follow. *)
273(* ---------------------------------------------------------------------*)
274
275val ISL = new_recursive_definition {
276 def = “ISL (INL x) = T /\ ISL (INR y) = F”,
277 name = "ISL[simp,compute]",
278 rec_axiom = sum_Axiom
279};
280
281val ISR = new_recursive_definition {
282 def = “ISR(INR x) = T /\ ISR(INL y) = F”, name = "ISR[simp,compute]",
283 rec_axiom = sum_Axiom
284};
285
286val OUTL = new_recursive_definition {
287 def = “OUTL (INL x) = x”, name = "OUTL[simp,compute]",
288 rec_axiom = sum_Axiom
289};
290
291val OUTR = new_recursive_definition {
292 def = “OUTR(INR x:'a+'b) = x”, name = "OUTR[simp,compute]",
293 rec_axiom = sum_Axiom
294};
295
296val _ = TypeBase.general_update “:'a + 'b”
297 (TypeBasePure.put_recognizers [ISL, ISR] o
298 TypeBasePure.put_destructors [OUTL, OUTR] o
299 TypeBasePure.put_lift (
300 mk_var("sumSyntax.lift_sum",
301 “:'type -> ('a -> 'term) ->
302 ('b -> 'term) -> ('a,'b)sum -> 'term”)
303 ))
304
305(* ---------------------------------------------------------------------*)
306(* Prove the following standard theorems about the sum type. *)
307(* *)
308(* |- ISL(s) ==> INL (OUTL s)=s *)
309(* |- ISR(s) ==> INR (OUTR s)=s *)
310(* |- !s. ISL s \/ ISR s *)
311(* *)
312(* ---------------------------------------------------------------------*)
313(* First, get the existence and uniqueness parts of sum_axiom. *)
314(* *)
315(* sum_EXISTS: *)
316(* |- !f g. ?h. (!x. h(INL x) = f x) /\ (!x. h(INR x) = g x) *)
317(* *)
318(* sum_UNIQUE: *)
319(* |- !f g x y. *)
320(* ((!x. x(INL x) = f x) /\ (!x. x(INR x) = g x)) /\ *)
321(* ((!x. y(INL x) = f x) /\ (!x. y(INR x) = g x)) ==> *)
322(* (!s. x s = y s) *)
323(* ---------------------------------------------------------------------*)
324
325(* GEN_ALL gives problems, so changed to be more precise. kls. *)
326val [sum_EXISTS,sum_UNIQUE] =
327 let val cnv = CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) sum_axiom
328 val rew = SPEC_ALL (REWRITE_RULE [o_THM] cnv)
329 val [a,b] = CONJUNCTS (CONV_RULE EXISTS_UNIQUE_CONV rew)
330 in
331 map (GENL [“f :'a -> 'c”, “g :'b -> 'c”])
332 [ a, BETA_RULE (CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) b) ]
333 end;
334
335(* Prove that: !x. ISL(x) \/ ISR(x) *)
336Theorem ISL_OR_ISR:
337 !x:('a,'b)sum. ISL(x) \/ ISR(x)
338Proof
339 STRIP_TAC THEN
340 STRIP_ASSUME_TAC (SPEC “x:('a,'b)sum” sum_CASES) THEN
341 ASM_REWRITE_TAC [ISL,ISR]
342QED
343
344(* Prove that: |- !x. ISL(x) ==> INL (OUTL x) = x *)
345Theorem INL[simp]:
346 !x:('a,'b)sum. ISL(x) ==> (INL (OUTL x) = x)
347Proof
348 STRIP_TAC THEN
349 STRIP_ASSUME_TAC (SPEC “x:('a,'b)sum” sum_CASES) THEN
350 ASM_REWRITE_TAC [ISL,OUTL]
351QED
352
353(* Prove that: |- !x. ISR(x) ==> INR (OUTR x) = x *)
354Theorem INR[simp]:
355 !x:('a,'b)sum. ISR(x) ==> (INR (OUTR x) = x)
356Proof
357 STRIP_TAC THEN
358 STRIP_ASSUME_TAC (SPEC “x:('a,'b)sum” sum_CASES) THEN
359 ASM_REWRITE_TAC [ISR,OUTR]
360QED
361
362Theorem sum_case_cong =
363 Prim_rec.case_cong_thm sum_CASES sum_case_def;
364
365
366(* ----------------------------------------------------------------------
367 SUM_MAP
368 ---------------------------------------------------------------------- *)
369
370val SUM_MAP_def = Prim_rec.new_recursive_definition{
371 name = "SUM_MAP_def[simp,compute]",
372 def = ``(SUM_MAP f g (INL (a:'a)) = INL (f a:'c)) /\
373 (SUM_MAP f g (INR (b:'b)) = INR (g b:'d))``,
374 rec_axiom = sum_Axiom};
375val _ = temp_set_mapped_fixity{tok = "++", term_name = "SUM_MAP",
376 fixity = Infixl 480}
377
378Theorem SUM_MAP:
379 !f g (z:'a + 'b).
380 (f ++ g) z = if ISL z then INL (f (OUTL z))
381 else INR (g (OUTR z)) :'c + 'd
382Proof
383 SIMP_TAC (srw_ss()) [FORALL_SUM]
384QED
385
386Theorem SUM_MAP_CASE:
387 !f g (z:'a + 'b).
388 (f ++ g) z = sum_CASE z (INL o f) (INR o g) :'c + 'd
389Proof
390 SIMP_TAC (srw_ss()) [FORALL_SUM]
391QED
392
393Theorem SUM_MAP_I[simp,quotient_simp]:
394 (I ++ I) = (I : 'a + 'b -> 'a + 'b)
395Proof
396 simp[FORALL_SUM, FUN_EQ_THM]
397QED
398
399Theorem SUM_MAP_o:
400 (f ++ g) o (h ++ k) = (f o h) ++ (g o k)
401Proof
402 SIMP_TAC (srw_ss()) [FORALL_SUM, FUN_EQ_THM]
403QED
404
405Theorem cond_sum_expand[simp]:
406 (!x y z. ((if P then INR x else INL y) = INR z) = (P /\ (z = x))) /\
407 (!x y z. ((if P then INR x else INL y) = INL z) = (~P /\ (z = y))) /\
408 (!x y z. ((if P then INL x else INR y) = INL z) = (P /\ (z = x))) /\
409 (!x y z. ((if P then INL x else INR y) = INR z) = (~P /\ (z = y)))
410Proof
411Cases_on `P` THEN FULL_SIMP_TAC(srw_ss())[] THEN SRW_TAC[][EQ_IMP_THM]
412QED
413
414Theorem NOT_ISL_ISR[simp]:
415 !x. ~ISL x = ISR x
416Proof
417 GEN_TAC THEN Q.SPEC_THEN `x` STRUCT_CASES_TAC sum_CASES THEN SRW_TAC[][]
418QED
419
420Theorem NOT_ISR_ISL[simp]:
421 !x. ~ISR x = ISL x
422Proof
423 GEN_TAC THEN Q.SPEC_THEN `x` STRUCT_CASES_TAC sum_CASES THEN SRW_TAC[][]
424QED
425
426(* ----------------------------------------------------------------------
427 SUM_ALL
428 ---------------------------------------------------------------------- *)
429
430val SUM_ALL_def = Prim_rec.new_recursive_definition {
431 def = ``(SUM_ALL (P:'a -> bool) (Q:'b -> bool) (INL x) <=> P x) /\
432 (SUM_ALL (P:'a -> bool) (Q:'b -> bool) (INR y) <=> Q y)``,
433 name = "SUM_ALL_def",
434 rec_axiom = sum_Axiom}
435val _ = export_rewrites ["SUM_ALL_def"]
436
437Theorem SUM_ALL_MONO:
438 (!x:'a. P x ==> P' x) /\ (!y:'b. Q y ==> Q' y) ==>
439 SUM_ALL P Q s ==> SUM_ALL P' Q' s
440Proof
441 Q.SPEC_THEN `s` STRUCT_CASES_TAC sum_CASES THEN
442 REWRITE_TAC [SUM_ALL_def] THEN REPEAT STRIP_TAC THEN RES_TAC
443QED
444val _ = IndDefLib.export_mono "SUM_ALL_MONO"
445
446Theorem SUM_ALL_CONG[defncong]:
447 !(s:'a + 'b) s' P P' Q Q'.
448 (s = s') /\ (!a. (s' = INL a) ==> (P a <=> P' a)) /\
449 (!b. (s' = INR b) ==> (Q b <=> Q' b)) ==>
450 (SUM_ALL P Q s <=> SUM_ALL P' Q' s')
451Proof
452 SIMP_TAC (srw_ss()) [FORALL_SUM]
453QED
454
455(* ----------------------------------------------------------------------
456 SUM_FIN, sums built from particular sets
457 ---------------------------------------------------------------------- *)
458
459val SUM_FIN_def = new_definition(
460 "SUM_FIN_def",
461 “SUM_FIN A B = \ab. sum_CASE ab (\a. a IN A) (\b. b IN B)”);
462
463Theorem IN_SUM_FIN_THM[simp]:
464 (INL a IN SUM_FIN A B <=> a IN A) /\
465 (INR b IN SUM_FIN A B <=> b IN B)
466Proof
467 SIMP_TAC (srw_ss()) [SUM_FIN_def, IN_DEF]
468QED
469
470(* ----------------------------------------------------------------------
471 SUM_REL, the sum "relator"
472 ---------------------------------------------------------------------- *)
473
474val SUM_REL_def = Prim_rec.new_recursive_definition {
475 def = “(SUM_REL R1 R2 (INL x:'a + 'b) ab <=> ISL ab /\ R1 x (OUTL ab)) /\
476 (SUM_REL R1 R2 (INR y) ab <=> ISR ab /\ R2 y (OUTR ab))”,
477 name = "SUM_REL_def",
478 rec_axiom = sum_Axiom};
479
480val _ = set_fixity "+++" (Infixl 480)
481Overload "+++" = “SUM_REL”
482
483Theorem SUM_REL_THM[simp,compute]:
484 (SUM_REL R1 R2 (INL x :'a + 'b) (INL a) <=> R1 x a) /\
485 (SUM_REL R1 R2 (INL x) (INR b) <=> F) /\
486 (SUM_REL R1 R2 (INR y) (INL a) <=> F) /\
487 (SUM_REL R1 R2 (INR y) (INR b) <=> R2 y b)
488Proof
489 SIMP_TAC (srw_ss()) [SUM_REL_def]
490QED
491
492Theorem SUM_REL_EQ[simp,quotient_simp]:
493 SUM_REL $= $= = ($= : 'a + 'b -> 'a + 'b -> bool)
494Proof
495 REWRITE_TAC [FUN_EQ_THM] >> SIMP_TAC (srw_ss()) [FORALL_SUM]
496QED
497
498Theorem SUM_REL_REFL:
499 (!x:'a. R1 x x) /\ (!a:'b. R2 a a) ==>
500 !xy. SUM_REL R1 R2 xy xy
501Proof
502 SIMP_TAC (srw_ss()) [FORALL_SUM]
503QED
504
505Theorem SUM_REL_SYM:
506 (!x y:'a. R1 x y <=> R1 y x) /\ (!a b:'b. R2 a b <=> R2 b a) ==>
507 !xy ab. SUM_REL R1 R2 xy ab <=> SUM_REL R1 R2 ab xy
508Proof
509 SIMP_TAC (srw_ss()) [FORALL_SUM]
510QED
511
512Theorem SUM_REL_TRANS:
513 (!x y z:'a. R1 x y /\ R1 y z ==> R1 x z) /\
514 (!a b c:'b. R2 a b /\ R2 b c ==> R2 a c) ==>
515 !xy ab uv. SUM_REL R1 R2 xy ab /\ SUM_REL R1 R2 ab uv ==>
516 SUM_REL R1 R2 xy uv
517Proof
518 SIMP_TAC (srw_ss()) [FORALL_SUM]
519QED
520
521(* ----------------------------------------------------------------------
522 Set constants
523 ---------------------------------------------------------------------- *)
524
525val setL_def = new_recursive_definition {
526 name = "setL_def[simp,compute]",
527 def = “setL (INL a) = (λx. x = a) ∧
528 setL (INR b) = λx. F”,
529 rec_axiom = sum_Axiom
530 };
531
532val setR_def = new_recursive_definition {
533 name = "setR_def[simp,compute]",
534 def = “setR (INL a) = (λx. F) ∧
535 setR (INR b) = λx. x = b”,
536 rec_axiom = sum_Axiom
537 };
538
539Theorem SUM_MAP_CONG:
540 (!a:'a. a IN setL ab ==> f1 a = f2 a :'c) /\
541 (!b:'b. b IN setR ab ==> g1 b = g2 b :'d) ==>
542 SUM_MAP f1 g1 ab = SUM_MAP f2 g2 ab
543Proof
544 Q.ID_SPEC_TAC ‘ab’ >> SIMP_TAC (srw_ss()) [FORALL_SUM, IN_DEF]
545QED
546
547Theorem SUM_ALL_SET:
548 SUM_ALL P Q ab <=> (!a. a IN setL ab ==> P a) /\ (!b. b IN setR ab ==> Q b)
549Proof
550 Q.ID_SPEC_TAC ‘ab’ >> SIMP_TAC (srw_ss()) [FORALL_SUM, IN_DEF]
551QED
552
553Theorem SUM_MAP_SET[simp]:
554 (setL (SUM_MAP f g ab) = λc. ?a:'a. c:'c = f a /\ a IN setL ab) /\
555 (setR (SUM_MAP f g ab) = λd. ?b:'b. d:'d = g b /\ b IN setR ab)
556Proof
557 Q.ID_SPEC_TAC ‘ab’ >> SIMP_TAC (srw_ss()) [FORALL_SUM, IN_DEF]
558QED
559
560
561val _ = computeLib.add_persistent_funs ["sum_case_def", "INL_11", "INR_11",
562 "sum_distinct", "sum_distinct1",
563 "SUM_ALL_def"]
564
565local
566val ns = ["Data","Sum"]
567fun add x y =
568 OpenTheoryMap.OpenTheory_const_name{const={Thy="sum",Name=x},name=(ns,y)}
569in
570val _ = OpenTheoryMap.OpenTheory_tyop_name{
571 tyop={Thy="sum",Tyop="sum"}, name=(ns,"+")
572}
573val _ = add "INR" "right"
574val _ = add "INL" "left"
575val _ = add "OUTR" "destRight"
576val _ = add "OUTL" "destLeft"
577end
578
579
580Theorem datatype_sum:
581 DATATYPE (sum (INL:'a -> 'a + 'b) (INR:'b -> 'a + 'b))
582Proof
583 REWRITE_TAC[DATATYPE_TAG_THM]
584QED
585
586(* ----------------------------------------------------------------------
587 Theorems to support the quotient package
588 ---------------------------------------------------------------------- *)
589
590Theorem SUM_EQUIV[quotient_equiv]:
591 !(R1:'a -> 'a -> bool) (R2:'b -> 'b -> bool).
592 EQUIV R1 ==> EQUIV R2 ==> EQUIV (R1 +++ R2)
593Proof
594 simp[EQUIV_def, EQUIV_REFL_SYM_TRANS, FORALL_SUM] >> PROVE_TAC[]
595QED
596
597Theorem SUM_QUOTIENT[quotient]:
598 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
599 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
600 QUOTIENT (R1 +++ R2) (abs1 ++ abs2) (rep1 ++ rep2)
601Proof
602 REPEAT STRIP_TAC
603 THEN REWRITE_TAC[QUOTIENT_def]
604 THEN REPEAT CONJ_TAC
605 THENL
606 [ rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >> simp[FORALL_SUM],
607
608 rpt (dxrule_then assume_tac QUOTIENT_REP_REFL) >> simp[FORALL_SUM],
609
610 simp[FORALL_SUM] >>
611 rpt (dxrule_then (fn th => simp[Once th, SimpLHS]) QUOTIENT_REL)
612 ]
613QED
614
615(* sum theory: INL, INR, ISL, ISR, ++ *)
616fun prs_tac ths =
617 rpt (rpt gen_tac >> disch_tac) >>
618 rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
619 simp(FORALL_SUM::ths)
620
621Theorem INL_PRS[quotient_prs]:
622 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
623 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
624 !a. INL a = (abs1 ++ abs2) (INL (rep1 a))
625Proof prs_tac[]
626QED
627
628Theorem INL_RSP[quotient_rsp]:
629 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
630 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
631 !a1 a2.
632 R1 a1 a2 ==>
633 (R1 +++ R2) (INL a1) (INL a2)
634Proof
635 simp[]
636QED
637
638Theorem INR_PRS[quotient_prs]:
639 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
640 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
641 !b. INR b = (abs1 ++ abs2) (INR (rep2 b))
642Proof prs_tac[]
643QED
644
645Theorem INR_RSP[quotient_rsp]:
646 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
647 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
648 !b1 b2.
649 R2 b1 b2 ==>
650 (R1 +++ R2) (INR b1) (INR b2)
651Proof
652 simp[]
653QED
654
655Theorem ISL_PRS[quotient_prs]:
656 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
657 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
658 !a. ISL a = ISL ((rep1 ++ rep2) a)
659Proof prs_tac[]
660QED
661
662Theorem ISL_RSP[quotient_rsp]:
663 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
664 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
665 !a1 a2.
666 (R1 +++ R2) a1 a2 ==>
667 (ISL a1 = ISL a2)
668Proof
669 simp[FORALL_SUM]
670QED
671
672Theorem ISR_PRS[quotient_prs]:
673 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
674 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
675 !a. ISR a = ISR ((rep1 ++ rep2) a)
676Proof prs_tac[]
677QED
678
679Theorem ISR_RSP[quotient_rsp]:
680 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
681 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
682 !a1 a2.
683 (R1 +++ R2) a1 a2 ==>
684 (ISR a1 = ISR a2)
685Proof
686 simp[FORALL_SUM]
687QED
688
689(* OUTL and OUTR are not completely defined, so do not lift. *)
690
691Theorem SUM_MAP_PRS[quotient_prs]:
692 !R1 (abs1:'a -> 'e) rep1. QUOTIENT R1 abs1 rep1 ==>
693 !R2 (abs2:'b -> 'f) rep2. QUOTIENT R2 abs2 rep2 ==>
694 !R3 (abs3:'c -> 'g) rep3. QUOTIENT R3 abs3 rep3 ==>
695 !R4 (abs4:'d -> 'h) rep4. QUOTIENT R4 abs4 rep4 ==>
696 !f g. (f ++ g) =
697 ((rep1 ++ rep3) --> (abs2 ++ abs4))
698 (((abs1 --> rep2) f) ++ ((abs3 --> rep4) g))
699Proof prs_tac[FUN_MAP_THM, FUN_EQ_THM]
700QED
701
702Theorem SUM_MAP_RSP[quotient_rsp]:
703 !R1 (abs1:'a -> 'e) rep1. QUOTIENT R1 abs1 rep1 ==>
704 !R2 (abs2:'b -> 'f) rep2. QUOTIENT R2 abs2 rep2 ==>
705 !R3 (abs3:'c -> 'g) rep3. QUOTIENT R3 abs3 rep3 ==>
706 !R4 (abs4:'d -> 'h) rep4. QUOTIENT R4 abs4 rep4 ==>
707 !f1 f2 g1 g2.
708 (R1 ===> R2) f1 f2 /\ (R3 ===> R4) g1 g2 ==>
709 ((R1 +++ R3) ===> (R2 +++ R4)) (f1 ++ g1) (f2 ++ g2)
710Proof
711 simp[FUN_REL, FORALL_SUM]
712QED
713
714val _ = temp_remove_termtok {term_name = "SUM_MAP", tok = "++"}