normalFormsScript.sml

1Theory normalForms[bare]
2Libs
3  HolKernel Parse boolLib
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
57Theorem EXT_POINT:
58     !(f : 'a -> 'b) g. (f (EXT_POINT f g) = g (EXT_POINT f g)) = (f = g)
59Proof
60   REPEAT GEN_TAC THEN
61   EQ_TAC THENL
62   [MATCH_ACCEPT_TAC EXT_POINT_DEF,
63    DISCH_THEN (fn th => REWRITE_TAC [th])]
64QED
65
66(* ------------------------------------------------------------------------- *)
67(* UNIV_POINT                                                                *)
68(* If a predicate P is true on its UNIV_POINT, it is true everywhere.        *)
69(* ------------------------------------------------------------------------- *)
70
71Theorem UNIV_POINT_EXISTS[local]:
72     ?f. !p. p (f p) ==> !x : 'a. p x
73Proof
74   EXISTS_TAC ``\p. @x : 'a. ~p x`` THEN
75   GEN_TAC THEN
76   BETA_TAC THEN
77   DISCH_TAC THEN
78   ONCE_REWRITE_TAC [GSYM (CONJUNCT1 NOT_CLAUSES)] THEN
79   CONV_TAC (RAND_CONV NOT_FORALL_CONV) THEN
80   REWRITE_TAC [EXISTS_DEF] THEN
81   BETA_TAC THEN
82   ASM_REWRITE_TAC []
83QED
84
85val UNIV_POINT_DEF =
86  Definition.new_specification
87  ("UNIV_POINT_DEF", ["UNIV_POINT"], UNIV_POINT_EXISTS);
88
89val _ = add_const "UNIV_POINT";
90
91Theorem UNIV_POINT:
92     !p. p (UNIV_POINT p) = !x : 'a. p x
93Proof
94   GEN_TAC THEN
95   EQ_TAC THENL
96   [MATCH_ACCEPT_TAC UNIV_POINT_DEF,
97    DISCH_THEN MATCH_ACCEPT_TAC]
98QED
99