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 31 32open HolKernel Parse boolLib BasicProvers; 33 34(* done to keep Holmake happy - satTheory is an ancestor of BasicProvers *) 35local open satTheory in end 36 37local open DefnBase in end 38val _ = new_theory "sum"; 39 40val o_DEF = combinTheory.o_DEF 41and o_THM = combinTheory.o_THM; 42 43(* ---------------------------------------------------------------------*) 44(* Introduce the new type. *) 45(* *) 46(* The sum of types `:'a` and `:'b` will be represented by a certain *) 47(* subset of type `:bool->'a->'b->bool`. A left injection of value *) 48(* `p:'a` will be represented by: `\b x y. x=p /\ b`. A right injection*) 49(* of value `q:'b` will be represented by: `\b x y. x=q /\ ~b`. *) 50(* The predicate IS_SUM_REP is true of just those objects of the type *) 51(* `:bool->'a->'b->bool` which are representations of some injection. *) 52(* ---------------------------------------------------------------------*) 53 54 55val IS_SUM_REP = 56 new_definition 57 ("IS_SUM_REP", 58 ���IS_SUM_REP (f:bool->'a->'b->bool) = 59 ?v1 v2. (f = \b x y.(x=v1) /\ b) \/ 60 (f = \b x y.(y=v2) /\ ~b)���); 61 62(* Prove that there exists some object in the representing type that *) 63(* lies in the subset of legal representations. *) 64 65val EXISTS_SUM_REP = 66 TAC_PROOF(([], ���?f:bool -> 'a -> 'b -> bool. IS_SUM_REP f���), 67 EXISTS_TAC ���\b x (y:'b). (x = @(x:'a).T) /\ b��� THEN 68 PURE_ONCE_REWRITE_TAC [IS_SUM_REP] THEN 69 EXISTS_TAC ���@(x:'a).T��� THEN 70 REWRITE_TAC []); 71 72(* ---------------------------------------------------------------------*) 73(* Use the type definition mechanism to introduce the new type. *) 74(* The theorem returned is: |- ?rep. TYPE_DEFINITION IS_SUM_REP rep *) 75(* ---------------------------------------------------------------------*) 76 77val sum_TY_DEF = new_type_definition ("sum", EXISTS_SUM_REP); 78val _ = add_infix_type {Prec = 60, ParseName = SOME "+", Name = "sum", 79 Assoc = HOLgrammars.RIGHT} 80 81 82(*---------------------------------------------------------------------------*) 83(* Define a representation function, REP_sum, from the type ('a,'b)sum to *) 84(* the representing type bool->'a->'b->bool, and the inverse abstraction *) 85(* function ABS_sum, and prove some trivial lemmas about them. *) 86(*---------------------------------------------------------------------------*) 87 88val sum_ISO_DEF = define_new_type_bijections 89 {name = "sum_ISO_DEF", 90 ABS = "ABS_sum", 91 REP = "REP_sum", 92 tyax = sum_TY_DEF}; 93 94 95val R_A = GEN_ALL (SYM (SPEC_ALL (CONJUNCT2 sum_ISO_DEF))) 96and R_11 = SYM(SPEC_ALL (prove_rep_fn_one_one sum_ISO_DEF)) 97and A_ONTO = REWRITE_RULE [IS_SUM_REP] (prove_abs_fn_onto sum_ISO_DEF); 98 99(* --------------------------------------------------------------------- *) 100(* The definitions of the constants INL and INR follow: *) 101(* --------------------------------------------------------------------- *) 102 103(* Define the injection function INL:'a->('a,'b)sum *) 104val INL_DEF = new_definition("INL_DEF", 105 ���!e.(INL:'a->(('a,'b)sum)) e = ABS_sum(\b x (y:'b). (x = e) /\ b)���); 106 107(* Define the injection function INR:'b->( 'a,'b )sum *) 108val INR_DEF = new_definition("INR_DEF", 109 ���!e.(INR:'b->(('a,'b)sum)) e = ABS_sum(\b (x:'a) y. (y = e) /\ ~b)���); 110 111(* --------------------------------------------------------------------- *) 112(* The proof of the `axiom` for sum types follows. *) 113(* --------------------------------------------------------------------- *) 114 115val SIMP = REWRITE_RULE []; 116fun REWRITE1_TAC th = REWRITE_TAC [th]; 117 118(* Prove that REP_sum(INL v) gives the representation of INL v. *) 119val REP_INL = TAC_PROOF(([], 120 ���REP_sum (INL v) = \b x (y:'b). ((x:'a) = v) /\ b���), 121 PURE_REWRITE_TAC [INL_DEF,R_A,IS_SUM_REP] THEN 122 EXISTS_TAC ���v:'a��� THEN 123 REWRITE_TAC[]); 124 125 126(* Prove that REP_sum(INR v) gives the representation of INR v. *) 127val REP_INR = TAC_PROOF(([], 128 ���REP_sum (INR v) = \b (x:'a) y. ((y:'b) = v) /\ ~b���), 129 PURE_REWRITE_TAC [INR_DEF,R_A,IS_SUM_REP] THEN 130 MAP_EVERY EXISTS_TAC [���v:'a���,���v:'b���] THEN 131 DISJ2_TAC THEN 132 REFL_TAC); 133 134(* Prove that INL is one-to-one *) 135val INL_11 = store_thm( 136 "INL_11", 137 ``(INL x = ((INL y):('a,'b)sum)) = (x = y)``, 138 EQ_TAC THENL 139 [PURE_REWRITE_TAC [R_11,REP_INL] THEN 140 CONV_TAC (REDEPTH_CONV (FUN_EQ_CONV ORELSEC BETA_CONV)) THEN 141 DISCH_THEN (ACCEPT_TAC o SIMP o SPECL [���T���,���x:'a���,���y:'b���]), 142 DISCH_THEN SUBST1_TAC THEN REFL_TAC]); 143 144(* Prove that INR is one-to-one *) 145val INR_11 = store_thm( 146 "INR_11", 147 ``(INR x = (INR y:('a,'b)sum)) = (x = y)``, 148 EQ_TAC THENL 149 [PURE_REWRITE_TAC [R_11,REP_INR] THEN 150 CONV_TAC (REDEPTH_CONV (FUN_EQ_CONV ORELSEC BETA_CONV)) THEN 151 DISCH_THEN (ACCEPT_TAC o SYM o SIMP o SPECL[���F���,���x:'a���,���y:'b���]), 152 DISCH_THEN SUBST1_TAC THEN REFL_TAC]); 153 154val INR_INL_11 = save_thm("INR_INL_11", 155 CONJ (GEN_ALL INL_11) (GEN_ALL INR_11)); 156val _ = export_rewrites ["INR_INL_11"] 157 158(* Prove that left injections and right injections are not equal. *) 159val INR_neq_INL = store_thm("INR_neq_INL", 160 ���!v1 v2. ~(INR v2 :('a,'b)sum = INL v1)���, 161 PURE_REWRITE_TAC [R_11,REP_INL,REP_INR] THEN 162 REPEAT GEN_TAC THEN 163 CONV_TAC (REDEPTH_CONV (FUN_EQ_CONV ORELSEC BETA_CONV)) THEN 164 DISCH_THEN (CONTR_TAC o SIMP o SPECL [���T���,���v1:'a���,���v2:'b���])); 165 166(*----------------------------------------------------------------------*) 167(* The abstract `axiomatization` of the sum type consists of the single *) 168(* theorem given below: *) 169(* *) 170(* sum_axiom |- !f g. ?!h. (h o INL = f) /\ (h o INR = g) *) 171(* *) 172(* The definitions of the usual operators ISL, OUTL, etc. follow from *) 173(* this axiom. *) 174(*----------------------------------------------------------------------*) 175 176val sum_axiom = store_thm("sum_axiom", 177 ���!(f:'a->'c). 178 !(g:'b->'c). 179 ?!h. ((h o INL) = f) /\ ((h o INR) = g)���, 180PURE_REWRITE_TAC [boolTheory.EXISTS_UNIQUE_DEF,o_DEF] THEN 181CONV_TAC (REDEPTH_CONV (BETA_CONV ORELSEC FUN_EQ_CONV)) THEN 182REPEAT (FILTER_STRIP_TAC ���x:('a,'b)sum->'c���) THENL 183[EXISTS_TAC (���\(x:('a,'b)sum). if (?v1. x = INL v1) 184 then f(@v1.x = INL v1) 185 else g(@v2.x = INR v2):'c���) THEN 186 simpLib.SIMP_TAC boolSimps.bool_ss [ 187 INL_11,INR_11,INR_neq_INL,SELECT_REFL_2 188 ], 189 REPEAT GEN_TAC THEN DISCH_THEN (CONJUNCTS_THEN2 MP_TAC 190 (REWRITE1_TAC o (CONV_RULE (ONCE_DEPTH_CONV SYM_CONV)))) THEN 191 REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC (SPEC ���s:('a,'b)sum��� A_ONTO) THEN 192 ASM_REWRITE_TAC (map (SYM o SPEC_ALL) [INL_DEF,INR_DEF])]); 193 194 195(* ---------------------------------------------------------------------*) 196(* We also prove a version of sum_axiom which is in a form suitable for *) 197(* use with the recursive type definition tools. *) 198(* ---------------------------------------------------------------------*) 199 200val sum_Axiom0 = prove( 201 ���!f:'a->'c. 202 !g:'b->'c. 203 ?!h. (!x. h(INL x) = f x) /\ 204 (!y. h(INR y) = g y)���, 205 let val cnv = CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) sum_axiom 206 val rew = SPEC_ALL (REWRITE_RULE [o_THM] cnv) 207 in 208 MATCH_ACCEPT_TAC rew 209 end); 210 211val sum_INDUCT = save_thm("sum_INDUCT", 212 Prim_rec.prove_induction_thm sum_Axiom0); 213 214Theorem FORALL_SUM: 215 (!s. P s) <=> (!x. P (INL x)) /\ (!y. P (INR y)) 216Proof 217 EQ_TAC THENL [DISCH_TAC THEN ASM_REWRITE_TAC [], 218 MATCH_ACCEPT_TAC sum_INDUCT] 219QED 220 221open simpLib 222 223(* !P. (?s. P s) <=> (?x. P (INL x)) \/ (?y. P (INR y)) *) 224val EXISTS_SUM = save_thm( 225 "EXISTS_SUM", 226 FORALL_SUM |> Q.INST [`P` |-> `\x. ~P x`] |> AP_TERM ``$~`` 227 |> CONV_RULE (BINOP_CONV (SIMP_CONV bool_ss [])) 228 |> Q.GEN `P`) 229 230val sum_Axiom = store_thm( 231 "sum_Axiom", 232 Term`!(f:'a -> 'c) (g:'b -> 'c). 233 ?h. (!x. h (INL x) = f x) /\ (!y. h (INR y) = g y)`, 234 REPEAT GEN_TAC THEN 235 STRIP_ASSUME_TAC 236 ((SPECL [Term`f:'a -> 'c`, Term`g:'b -> 'c`] o 237 Ho_Rewrite.REWRITE_RULE [EXISTS_UNIQUE_THM]) sum_Axiom0) THEN 238 EXISTS_TAC (Term`h:'a + 'b -> 'c`) THEN 239 ASM_REWRITE_TAC []); 240 241val sum_CASES = save_thm("sum_CASES", 242 hd (Prim_rec.prove_cases_thm sum_INDUCT)); 243 244val sum_distinct = store_thm("sum_distinct", 245 Term`!x:'a y:'b. ~(INL x = INR y)`, 246 REPEAT STRIP_TAC THEN 247 STRIP_ASSUME_TAC ((BETA_RULE o REWRITE_RULE [EXISTS_UNIQUE_DEF] o 248 Q.ISPECL [`\x:'a. T`, `\y:'b. F`]) sum_Axiom) THEN 249 FIRST_X_ASSUM (MP_TAC o AP_TERM (Term`h:'a + 'b -> bool`)) THEN 250 ASM_REWRITE_TAC []); 251val _ = export_rewrites ["sum_distinct"] 252 253val sum_distinct_rev = save_thm("sum_distinct1", GSYM sum_distinct); 254 255(* ---------------------------------------------------------------------*) 256(* The definitions of ISL, ISR, OUTL, OUTR follow. *) 257(* ---------------------------------------------------------------------*) 258 259 260(* Derive the defining property for ISL. *) 261val ISL_DEF = TAC_PROOF( 262 ([], ���?ISL. (!x:'a. ISL(INL x)) /\ (!y:'b. ~ISL(INR y))���), 263 let val inst = INST_TYPE [Type.gamma |-> Type.bool] sum_axiom 264 val spec = SPECL [���\x:'a.T���, ���\y:'b.F���] inst 265 val exth = CONJUNCT1 (CONV_RULE EXISTS_UNIQUE_CONV spec) 266 val conv = CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) exth 267 in 268 STRIP_ASSUME_TAC (REWRITE_RULE [o_THM] conv) THEN 269 EXISTS_TAC ���h:'a+'b->bool��� THEN ASM_REWRITE_TAC [] 270 end); 271 272(* Then define ISL with a constant specification. *) 273val ISL = new_specification("ISL",["ISL"], ISL_DEF); 274val _ = export_rewrites ["ISL"] 275 276(* Derive the defining property for ISR. *) 277val ISR_DEF = TAC_PROOF( 278 ([], ���?ISR. (!x:'b. ISR(INR x)) /\ (!y:'a. ~ISR(INL y))���), 279 let val inst = INST_TYPE [Type.gamma |-> Type.bool] sum_axiom 280 val spec = SPECL [���\x:'a.F���, ���\y:'b.T���] inst 281 val exth = CONJUNCT1 (CONV_RULE EXISTS_UNIQUE_CONV spec) 282 val conv = CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) exth 283 in 284 STRIP_ASSUME_TAC (REWRITE_RULE [o_THM] conv) THEN 285 EXISTS_TAC ���h:'a+'b->bool��� THEN ASM_REWRITE_TAC [] 286 end); 287 288(* Then define ISR with a constant specification. *) 289val ISR = new_specification("ISR",["ISR"], ISR_DEF); 290val _ = export_rewrites ["ISR"] 291 292(* Derive the defining property of OUTL. *) 293val OUTL_DEF = TAC_PROOF(([], 294���?OUTL. !x. OUTL(INL x:('a,'b)sum) = x���), 295 let val inst = INST_TYPE [Type.gamma |-> Type.alpha] sum_axiom 296 val spec = SPECL [���\x:'a.x���, ���\y:'b.@x:'a.F���] inst 297 val exth = CONJUNCT1 (CONV_RULE EXISTS_UNIQUE_CONV spec) 298 val conv = CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) exth 299 in 300 STRIP_ASSUME_TAC (REWRITE_RULE [o_THM] (BETA_RULE conv)) THEN 301 EXISTS_TAC ���h:'a+'b->'a��� THEN ASM_REWRITE_TAC [] 302 end); 303 304(* Then define OUTL with a constant specification. *) 305val OUTL = new_specification("OUTL",["OUTL"], OUTL_DEF) 306val _ = export_rewrites ["OUTL"] 307 308(* Derive the defining property of OUTR. *) 309val OUTR_DEF = TAC_PROOF( 310 ([], ���?OUTR. !x. OUTR(INR x:'a+'b) = x���), 311 let val inst = INST_TYPE [Type.gamma |-> Type.beta] sum_axiom 312 val spec = SPECL [���\x:'a.@y:'b.F���, ���\y:'b.y���] inst 313 val exth = CONJUNCT1 (CONV_RULE EXISTS_UNIQUE_CONV spec) 314 val conv = CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) exth 315 in 316 STRIP_ASSUME_TAC (REWRITE_RULE [o_THM] (BETA_RULE conv)) THEN 317 EXISTS_TAC ���h:'a+'b->'b��� THEN ASM_REWRITE_TAC [] 318 end); 319 320(* Then define OUTR with a constant specification. *) 321val OUTR = new_specification("OUTR", ["OUTR"], OUTR_DEF); 322val _ = export_rewrites ["OUTR"] 323 324 325 326(* ---------------------------------------------------------------------*) 327(* Prove the following standard theorems about the sum type. *) 328(* *) 329(* |- ISL(s) ==> INL (OUTL s)=s *) 330(* |- ISR(s) ==> INR (OUTR s)=s *) 331(* |- !s. ISL s \/ ISR s *) 332(* *) 333(* ---------------------------------------------------------------------*) 334(* First, get the existence and uniqueness parts of sum_axiom. *) 335(* *) 336(* sum_EXISTS: *) 337(* |- !f g. ?h. (!x. h(INL x) = f x) /\ (!x. h(INR x) = g x) *) 338(* *) 339(* sum_UNIQUE: *) 340(* |- !f g x y. *) 341(* ((!x. x(INL x) = f x) /\ (!x. x(INR x) = g x)) /\ *) 342(* ((!x. y(INL x) = f x) /\ (!x. y(INR x) = g x)) ==> *) 343(* (!s. x s = y s) *) 344(* ---------------------------------------------------------------------*) 345 346(* GEN_ALL gives problems, so changed to be more precise. kls. *) 347val [sum_EXISTS,sum_UNIQUE] = 348 let val cnv = CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) sum_axiom 349 val rew = SPEC_ALL (REWRITE_RULE [o_THM] cnv) 350 val [a,b] = CONJUNCTS (CONV_RULE EXISTS_UNIQUE_CONV rew) 351 in 352 map (GENL [���f :'a -> 'c���, ���g :'b -> 'c���]) 353 [ a, BETA_RULE (CONV_RULE (ONCE_DEPTH_CONV FUN_EQ_CONV) b) ] 354 end; 355 356(* Prove that: !x. ISL(x) \/ ISR(x) *) 357val ISL_OR_ISR = store_thm("ISL_OR_ISR", 358 ���!x:('a,'b)sum. ISL(x) \/ ISR(x)���, 359 STRIP_TAC THEN 360 STRIP_ASSUME_TAC (SPEC ���x:('a,'b)sum��� sum_CASES) THEN 361 ASM_REWRITE_TAC [ISL,ISR]); 362 363(* Prove that: |- !x. ISL(x) ==> INL (OUTL x) = x *) 364val INL = store_thm("INL", 365 ���!x:('a,'b)sum. ISL(x) ==> (INL (OUTL x) = x)���, 366 STRIP_TAC THEN 367 STRIP_ASSUME_TAC (SPEC ���x:('a,'b)sum��� sum_CASES) THEN 368 ASM_REWRITE_TAC [ISL,OUTL]); 369val _ = export_rewrites ["INL"] 370 371(* Prove that: |- !x. ISR(x) ==> INR (OUTR x) = x *) 372val INR = store_thm("INR", 373 ���!x:('a,'b)sum. ISR(x) ==> (INR (OUTR x) = x)���, 374 STRIP_TAC THEN 375 STRIP_ASSUME_TAC (SPEC ���x:('a,'b)sum��� sum_CASES) THEN 376 ASM_REWRITE_TAC [ISR,OUTR]); 377val _ = export_rewrites ["INR"] 378 379val [sum_case_def] = Prim_rec.define_case_constant sum_Axiom 380val _ = export_rewrites ["sum_case_def"] 381val _ = overload_on("case", ``sum_CASE``) 382 383val sum_case_cong = save_thm("sum_case_cong", 384 Prim_rec.case_cong_thm sum_CASES sum_case_def); 385 386 387(* ---------------------------------------------------------------------- 388 SUM_MAP 389 ---------------------------------------------------------------------- *) 390 391val SUM_MAP_def = Prim_rec.new_recursive_definition{ 392 name = "SUM_MAP_def", 393 def = ``(SUM_MAP f g (INL (a:'a)) = INL (f a:'c)) /\ 394 (SUM_MAP f g (INR (b:'b)) = INR (g b:'d))``, 395 rec_axiom = sum_Axiom}; 396val _ = export_rewrites ["SUM_MAP_def"] 397val _ = temp_set_mapped_fixity{tok = "++", term_name = "SUM_MAP", 398 fixity = Infixl 480} 399 400val SUM_MAP = store_thm ( 401 "SUM_MAP", 402 ``!f g (z:'a + 'b). 403 (f ++ g) z = if ISL z then INL (f (OUTL z)) 404 else INR (g (OUTR z)) :'c + 'd``, 405 SIMP_TAC (srw_ss()) [FORALL_SUM]); 406 407val SUM_MAP_CASE = store_thm ( 408 "SUM_MAP_CASE", 409 ``!f g (z:'a + 'b). 410 (f ++ g) z = sum_CASE z (INL o f) (INR o g) :'c + 'd``, 411 SIMP_TAC (srw_ss()) [FORALL_SUM]); 412 413val SUM_MAP_I = store_thm ( 414 "SUM_MAP_I", 415 ``(I ++ I) = (I : 'a + 'b -> 'a + 'b)``, 416 SIMP_TAC (srw_ss()) [FORALL_SUM, FUN_EQ_THM]); 417 418Theorem SUM_MAP_o: 419 (f ++ g) o (h ++ k) = (f o h) ++ (g o k) 420Proof 421 SIMP_TAC (srw_ss()) [FORALL_SUM, FUN_EQ_THM] 422QED 423 424val cond_sum_expand = store_thm("cond_sum_expand", 425``(!x y z. ((if P then INR x else INL y) = INR z) = (P /\ (z = x))) /\ 426 (!x y z. ((if P then INR x else INL y) = INL z) = (~P /\ (z = y))) /\ 427 (!x y z. ((if P then INL x else INR y) = INL z) = (P /\ (z = x))) /\ 428 (!x y z. ((if P then INL x else INR y) = INR z) = (~P /\ (z = y)))``, 429Cases_on `P` THEN FULL_SIMP_TAC(srw_ss())[] THEN SRW_TAC[][EQ_IMP_THM]) 430val _ = export_rewrites["cond_sum_expand"] 431 432val NOT_ISL_ISR = store_thm("NOT_ISL_ISR", 433 ``!x. ~ISL x = ISR x``, 434 GEN_TAC THEN Q.SPEC_THEN `x` STRUCT_CASES_TAC sum_CASES THEN SRW_TAC[][]) 435val _ = export_rewrites["NOT_ISL_ISR"] 436 437val NOT_ISR_ISL = store_thm("NOT_ISR_ISL", 438 ``!x. ~ISR x = ISL x``, 439 GEN_TAC THEN Q.SPEC_THEN `x` STRUCT_CASES_TAC sum_CASES THEN SRW_TAC[][]) 440val _ = export_rewrites["NOT_ISR_ISL"] 441 442(* ---------------------------------------------------------------------- 443 SUM_ALL 444 ---------------------------------------------------------------------- *) 445 446val SUM_ALL_def = Prim_rec.new_recursive_definition { 447 def = ``(SUM_ALL (P:'a -> bool) (Q:'b -> bool) (INL x) <=> P x) /\ 448 (SUM_ALL (P:'a -> bool) (Q:'b -> bool) (INR y) <=> Q y)``, 449 name = "SUM_ALL_def", 450 rec_axiom = sum_Axiom} 451val _ = export_rewrites ["SUM_ALL_def"] 452 453val SUM_ALL_MONO = store_thm( 454 "SUM_ALL_MONO", 455 ``(!x:'a. P x ==> P' x) /\ (!y:'b. Q y ==> Q' y) ==> 456 SUM_ALL P Q s ==> SUM_ALL P' Q' s``, 457 Q.SPEC_THEN `s` STRUCT_CASES_TAC sum_CASES THEN 458 REWRITE_TAC [SUM_ALL_def] THEN REPEAT STRIP_TAC THEN RES_TAC); 459val _ = IndDefLib.export_mono "SUM_ALL_MONO" 460 461val SUM_ALL_CONG = store_thm( 462 "SUM_ALL_CONG[defncong]", 463 ``!(s:'a + 'b) s' P P' Q Q'. 464 (s = s') /\ (!a. (s' = INL a) ==> (P a <=> P' a)) /\ 465 (!b. (s' = INR b) ==> (Q b <=> Q' b)) ==> 466 (SUM_ALL P Q s <=> SUM_ALL P' Q' s')``, 467 SIMP_TAC (srw_ss()) [FORALL_SUM]); 468 469val _ = computeLib.add_persistent_funs ["sum_case_def", "INL_11", "INR_11", 470 "sum_distinct", "sum_distinct1", 471 "SUM_ALL_def", "SUM_MAP_def", 472 "OUTL", "OUTR", "ISL", "ISR"] 473 474local open OpenTheoryMap 475val ns = ["Data","Sum"] 476fun add x y = OpenTheory_const_name{const={Thy="sum",Name=x},name=(ns,y)} in 477val _ = OpenTheory_tyop_name{tyop={Thy="sum",Tyop="sum"},name=(ns,"+")} 478val _ = add "INR" "right" 479val _ = add "INL" "left" 480val _ = add "OUTR" "destRight" 481val _ = add "OUTL" "destLeft" 482end 483 484val _ = TypeBase.export 485 [TypeBasePure.mk_datatype_info_no_simpls 486 {ax=TypeBasePure.ORIG sum_Axiom, 487 case_def=sum_case_def, 488 case_cong=sum_case_cong, 489 case_eq = Prim_rec.prove_case_eq_thm {case_def = sum_case_def, 490 nchotomy = sum_CASES}, 491 induction=TypeBasePure.ORIG sum_INDUCT, 492 nchotomy=sum_CASES, 493 size=NONE, 494 encode=NONE, 495 fields=[], accessors=[], updates=[], 496 recognizers = [ISL,ISR], 497 destructors = [OUTL,OUTR], 498 lift=SOME(mk_var("sumSyntax.lift_sum", 499 ���:'type -> ('a -> 'term) -> 500 ('b -> 'term) -> ('a,'b)sum -> 'term���)), 501 one_one=SOME INR_INL_11, 502 distinct=SOME sum_distinct}]; 503 504val datatype_sum = store_thm( 505 "datatype_sum", 506 ``DATATYPE (sum (INL:'a -> 'a + 'b) (INR:'b -> 'a + 'b))``, 507 REWRITE_TAC[DATATYPE_TAG_THM]); 508 509val _ = temp_remove_termtok {term_name = "SUM_MAP", tok = "++"} 510 511val _ = export_theory(); 512