1open HolKernel Parse boolLib; 2 3val _ = new_theory "normalForms"; 4 5(* ------------------------------------------------------------------------- *) 6(* EXT_POINT *) 7(* If two functions f and g agree on their extension point EXT_POINT f g, *) 8(* then they must agree everywhere (i.e., they are equal). *) 9(* ------------------------------------------------------------------------- *) 10 11val EXT_POINT_EXISTS = 12 let 13 val LAND_CONV = RATOR_CONV o RAND_CONV 14 val f = Term `f : 'a -> 'b` 15 val g = Term `g : 'a -> 'b` 16 val A0 = SPECL [f, g] EQ_EXT 17 val A1 = SPEC (Term `\x. ^f x = ^g x`) LEFT_EXISTS_IMP_THM 18 val A2 = SPEC (Term `^f = ^g`) A1 19 val A3 = CONV_RULE (LAND_CONV (QUANT_CONV (LAND_CONV BETA_CONV))) A2 20 val A4 = CONV_RULE (RAND_CONV (LAND_CONV (QUANT_CONV BETA_CONV))) A3 21 val A5 = EQ_MP (SYM A4) A0 22 val A6 = GEN g A5 23 val A7 = INST_TYPE [alpha |-> (alpha --> beta), beta |-> alpha] SKOLEM_THM 24 val A8 = SPEC (Term `\g x. (^f x = g x) ==> (^f = g)`) A7 25 val A9 = 26 CONV_RULE (LAND_CONV (QUANT_CONV (QUANT_CONV (RATOR_CONV BETA_CONV)))) A8 27 val A10 = CONV_RULE (LAND_CONV (QUANT_CONV (QUANT_CONV BETA_CONV))) A9 28 val A11 = EQ_MP A10 A6 29 val A12 = CONV_RULE (QUANT_CONV (QUANT_CONV (RATOR_CONV BETA_CONV))) A11 30 val A13 = CONV_RULE (QUANT_CONV (QUANT_CONV BETA_CONV)) A12 31 val A14 = GEN f A13 32 val A15 = 33 INST_TYPE 34 [alpha |-> (alpha --> beta), beta |-> ((alpha --> beta) --> alpha)] 35 SKOLEM_THM 36 val A16 = 37 SPEC (Term `\f x. !(g:'a->'b). (f (x g) = g (x g)) ==> (f = g)`) A15 38 val A17 = 39 CONV_RULE (LAND_CONV (QUANT_CONV (QUANT_CONV (RATOR_CONV BETA_CONV)))) A16 40 val A18 = CONV_RULE (LAND_CONV (QUANT_CONV (QUANT_CONV BETA_CONV))) A17 41 val A19 = EQ_MP A18 A14 42 val A20 = CONV_RULE (QUANT_CONV (QUANT_CONV (RATOR_CONV BETA_CONV))) A19 43 val A21 = CONV_RULE (QUANT_CONV (QUANT_CONV BETA_CONV)) A20 44 val A22 = 45 ALPHA (Term `?f. !(x:'a->'b) g. (x (f x g) = g (f x g)) ==> (x = g)`) 46 (Term `?x. !(f:'a->'b) g. (f (x f g) = g (x f g)) ==> (f = g)`) 47 in 48 EQ_MP A22 A21 49 end; 50 51val EXT_POINT_DEF = 52 Definition.new_specification 53 ("EXT_POINT_DEF", ["EXT_POINT"], EXT_POINT_EXISTS); 54 55val _ = add_const "EXT_POINT"; 56 57val EXT_POINT = store_thm 58 ("EXT_POINT", 59 ``!(f : 'a -> 'b) g. (f (EXT_POINT f g) = g (EXT_POINT f g)) = (f = g)``, 60 REPEAT GEN_TAC THEN 61 EQ_TAC THENL 62 [MATCH_ACCEPT_TAC EXT_POINT_DEF, 63 DISCH_THEN (fn th => REWRITE_TAC [th])]); 64 65(* ------------------------------------------------------------------------- *) 66(* UNIV_POINT *) 67(* If a predicate P is true on its UNIV_POINT, it is true everywhere. *) 68(* ------------------------------------------------------------------------- *) 69 70val UNIV_POINT_EXISTS = prove 71 (``?f. !p. p (f p) ==> !x : 'a. p x``, 72 EXISTS_TAC ``\p. @x : 'a. ~p x`` THEN 73 GEN_TAC THEN 74 BETA_TAC THEN 75 DISCH_TAC THEN 76 ONCE_REWRITE_TAC [GSYM (CONJUNCT1 NOT_CLAUSES)] THEN 77 CONV_TAC (RAND_CONV NOT_FORALL_CONV) THEN 78 REWRITE_TAC [EXISTS_DEF] THEN 79 BETA_TAC THEN 80 ASM_REWRITE_TAC []); 81 82val UNIV_POINT_DEF = 83 Definition.new_specification 84 ("UNIV_POINT_DEF", ["UNIV_POINT"], UNIV_POINT_EXISTS); 85 86val _ = add_const "UNIV_POINT"; 87 88val UNIV_POINT = store_thm 89 ("UNIV_POINT", 90 ``!p. p (UNIV_POINT p) = !x : 'a. p x``, 91 GEN_TAC THEN 92 EQ_TAC THENL 93 [MATCH_ACCEPT_TAC UNIV_POINT_DEF, 94 DISCH_THEN MATCH_ACCEPT_TAC]); 95 96val _ = export_theory (); 97