1 (* ========================================================================= *)
2 (* Trivial odds and ends. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Combinators. We don't bother with S and K, which seem of little use. *)
14 (* ------------------------------------------------------------------------- *)
16 parse_as_infix ("o",(26,"right"));;
18 let o_DEF = new_definition
19 `(o) (f:B->C) g = \x:A. f(g(x))`;;
21 let I_DEF = new_definition
25 (`!f:B->C. !g:A->B. !x:A. (f o g) x = f(g(x))`,
26 PURE_REWRITE_TAC [o_DEF] THEN
27 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
28 REPEAT GEN_TAC THEN REFL_TAC);;
31 (`!f:C->D. !g:B->C. !h:A->B. f o (g o h) = (f o g) o h`,
32 REPEAT GEN_TAC THEN REWRITE_TAC [o_DEF] THEN
33 CONV_TAC (REDEPTH_CONV BETA_CONV) THEN
38 REWRITE_TAC [I_DEF]);;
41 (`!f:A->B. (I o f = f) /\ (f o I = f)`,
43 REWRITE_TAC[FUN_EQ_THM; o_DEF; I_THM]);;
45 (* ------------------------------------------------------------------------- *)
46 (* The theory "1" (a 1-element type). *)
47 (* ------------------------------------------------------------------------- *)
49 let EXISTS_ONE_REP = prove
52 BETA_TAC THEN ACCEPT_TAC TRUTH);;
55 new_type_definition "1" ("one_ABS","one_REP") EXISTS_ONE_REP;;
57 let one_DEF = new_definition
62 MP_TAC(GEN_ALL (SPEC `one_REP a` (CONJUNCT2 one_tydef))) THEN
63 REWRITE_TAC[CONJUNCT1 one_tydef] THEN DISCH_TAC THEN
64 ONCE_REWRITE_TAC[GSYM (CONJUNCT1 one_tydef)] THEN
68 (`!f g. f = (g:A->1)`,
69 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
70 GEN_TAC THEN ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
72 let one_INDUCT = prove
73 (`!P. P one ==> !x. P x`,
74 ONCE_REWRITE_TAC[one] THEN REWRITE_TAC[]);;
76 let one_RECURSION = prove
77 (`!e:A. ?fn. fn one = e`,
78 GEN_TAC THEN EXISTS_TAC `\x:1. e:A` THEN BETA_TAC THEN REFL_TAC);;
81 (`!e:A. ?!fn. fn one = e`,
82 GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM; one_RECURSION] THEN
83 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
84 ONCE_REWRITE_TAC [one] THEN ASM_REWRITE_TAC[]);;
86 (* ------------------------------------------------------------------------- *)
87 (* Add the type "1" to the inductive type store. *)
88 (* ------------------------------------------------------------------------- *)
90 inductive_type_store :=
91 ("1",(1,one_INDUCT,one_RECURSION))::(!inductive_type_store);;