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