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