ind_typeScript.sml
1Theory ind_type[bare]
2Ancestors
3 num prim_rec arithmetic numpair
4Libs
5 HolKernel boolLib Prim_rec Parse simpLib boolSimps
6 InductiveDefinition mesonLib
7
8val hol_ss = bool_ss ++ numSimps.old_ARITH_ss ++ numSimps.REDUCE_ss
9
10val lhand = rand o rator
11val AND_FORALL_THM = GSYM FORALL_AND_THM;
12val GEN_REWRITE_TAC = fn c => fn thl =>
13 Rewrite.GEN_REWRITE_TAC c Rewrite.empty_rewrites thl
14
15
16(* ------------------------------------------------------------------------- *)
17(* Abstract left inverses for binary injections (we could construct them...) *)
18(* ------------------------------------------------------------------------- *)
19
20Theorem INJ_INVERSE2:
21 !P:'A->'B->'C.
22 (!x1 y1 x2 y2. (P x1 y1 = P x2 y2) <=> (x1 = x2) /\ (y1 = y2)) ==>
23 ?X Y. !x y. (X(P x y) = x) /\ (Y(P x y) = y)
24Proof
25 GEN_TAC THEN DISCH_TAC THEN
26 Q.EXISTS_TAC `\z:'C. @x:'A. ?y:'B. P x y = z` THEN
27 Q.EXISTS_TAC `\z:'C. @y:'B. ?x:'A. P x y = z` THEN
28 REPEAT GEN_TAC THEN ASM_SIMP_TAC hol_ss []
29QED
30
31(* ------------------------------------------------------------------------- *)
32(* Define an injective pairing function on ":num". *)
33(* ------------------------------------------------------------------------- *)
34
35val NUMPAIR_DEST = CONJ (SPEC_ALL nfst_npair) (SPEC_ALL nsnd_npair) |> GEN_ALL
36
37
38(* ------------------------------------------------------------------------- *)
39(* Also, an injective map bool->num->num (even easier!) *)
40(* ------------------------------------------------------------------------- *)
41
42Definition NUMSUM[nocompute]:
43 NUMSUM b x = if b then SUC(2 * x) else 2 * x
44End
45
46Theorem NUMSUM_INJ:
47 !b1 x1 b2 x2. (NUMSUM b1 x1 = NUMSUM b2 x2) <=> (b1 = b2) /\ (x1 = x2)
48Proof
49 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
50 POP_ASSUM(MP_TAC o REWRITE_RULE[NUMSUM]) THEN
51 DISCH_THEN(fn th => MP_TAC th THEN MP_TAC(Q.AP_TERM `EVEN` th)) THEN
52 REPEAT COND_CASES_TAC THEN REWRITE_TAC[EVEN, EVEN_DOUBLE] THEN
53 SIMP_TAC hol_ss [INV_SUC_EQ, EQ_MULT_LCANCEL]
54QED
55
56val NUMSUM_DEST = Rsyntax.new_specification{
57 consts = [{const_name = "NUMLEFT", fixity = NONE},
58 {const_name = "NUMRIGHT", fixity = NONE}],
59 name = "NUMSUM_DEST[notuserdef]",
60 sat_thm = MATCH_MP INJ_INVERSE2 NUMSUM_INJ};
61
62(* ------------------------------------------------------------------------- *)
63(* Injection num->Z, where Z == num->A->bool. *)
64(* ------------------------------------------------------------------------- *)
65
66Definition INJN[nocompute]:
67 INJN (m:num) = \(n:num) (a:'a). n = m
68End
69
70Theorem INJN_INJ:
71 !n1 n2. (INJN n1 :num->'a->bool = INJN n2) = (n1 = n2)
72Proof
73 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
74 POP_ASSUM(MP_TAC o C Q.AP_THM `n1:num` o REWRITE_RULE[INJN]) THEN
75 DISCH_THEN(MP_TAC o C Q.AP_THM `a:'a`) THEN SIMP_TAC bool_ss []
76QED
77
78(* ------------------------------------------------------------------------- *)
79(* Injection A->Z, where Z == num->A->bool. *)
80(* ------------------------------------------------------------------------- *)
81
82Definition INJA[nocompute]:
83 INJA (a:'a) = \(n:num) b. b = a
84End
85
86Theorem INJA_INJ:
87 !a1 a2. (INJA a1 = INJA a2) = (a1:'a = a2)
88Proof
89 REPEAT GEN_TAC THEN SIMP_TAC bool_ss [INJA, FUN_EQ_THM] THEN
90 EQ_TAC THENL [
91 DISCH_THEN(MP_TAC o Q.SPEC `a1:'a`) THEN REWRITE_TAC[],
92 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[]
93 ]
94QED
95
96(* ------------------------------------------------------------------------- *)
97(* Injection (num->Z)->Z, where Z == num->A->bool. *)
98(* ------------------------------------------------------------------------- *)
99
100Definition INJF[nocompute]:
101 INJF (f:num->(num->'a->bool)) = \n. f (nfst n) (nsnd n)
102End
103
104Theorem INJF_INJ:
105 !f1 f2. (INJF f1 :num->'a->bool = INJF f2) = (f1 = f2)
106Proof
107 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
108 REWRITE_TAC[FUN_EQ_THM] THEN
109 MAP_EVERY Q.X_GEN_TAC [`n:num`, `m:num`, `a:'a`] THEN
110 POP_ASSUM(MP_TAC o REWRITE_RULE[INJF]) THEN
111 DISCH_THEN(MP_TAC o C Q.AP_THM `a:'a` o C Q.AP_THM `n *, m`) THEN
112 SIMP_TAC bool_ss [NUMPAIR_DEST]
113QED
114
115(* ------------------------------------------------------------------------- *)
116(* Injection Z->Z->Z, where Z == num->A->bool. *)
117(* ------------------------------------------------------------------------- *)
118
119Definition INJP[nocompute]:
120 INJP f1 f2:num->'a->bool =
121 \n a. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a
122End
123
124Theorem INJP_INJ:
125 !(f1:num->'a->bool) f1' f2 f2'.
126 (INJP f1 f2 = INJP f1' f2') <=> (f1 = f1') /\ (f2 = f2')
127Proof
128 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
129 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
130 SIMP_TAC bool_ss [AND_FORALL_THM] THEN
131 Q.X_GEN_TAC `n:num` THEN POP_ASSUM(MP_TAC o REWRITE_RULE[INJP]) THEN
132 DISCH_THEN(MP_TAC o GEN ``b:bool`` o C Q.AP_THM `NUMSUM b n`) THEN
133 DISCH_THEN(fn th => MP_TAC(Q.SPEC `T` th) THEN MP_TAC(Q.SPEC `F` th)) THEN
134 SIMP_TAC (bool_ss ++ ETA_ss) [NUMSUM_DEST]
135QED
136
137(* ------------------------------------------------------------------------- *)
138(* Now, set up "constructor" and "bottom" element. *)
139(* ------------------------------------------------------------------------- *)
140
141Definition ZCONSTR[nocompute]:
142 ZCONSTR c i r :num->'a->bool =
143 INJP (INJN (SUC c)) (INJP (INJA i) (INJF r))
144End
145
146Definition ZBOT[nocompute]:
147 ZBOT = INJP (INJN 0) (@z:num->'a->bool. T)
148End
149
150Theorem ZCONSTR_ZBOT:
151 !c i r. ~(ZCONSTR c i r :num->'a->bool = ZBOT)
152Proof
153 REWRITE_TAC[ZCONSTR, ZBOT, INJP_INJ, INJN_INJ, NOT_SUC]
154QED
155
156(* ------------------------------------------------------------------------- *)
157(* Carve out an inductively defined set. *)
158(* ------------------------------------------------------------------------- *)
159
160val (ZRECSPACE_RULES,ZRECSPACE_INDUCT,ZRECSPACE_CASES) =
161 IndDefLib.Hol_reln
162 `ZRECSPACE (ZBOT:num->'a->bool) /\
163 (!c i r. (!n. ZRECSPACE (r n)) ==> ZRECSPACE (ZCONSTR c i r))`;
164
165local fun new_basic_type_definition tyname (mkname, destname) thm =
166 let val (pred, witness) = dest_comb(concl thm)
167 val predty = type_of pred
168 val dom_ty = #1 (dom_rng predty)
169 val x = mk_var("x", dom_ty)
170 val witness_exists = EXISTS
171 (mk_exists(x, mk_comb(pred, x)),witness) thm
172 val tyax = new_type_definition(tyname,witness_exists)
173 val (mk_dest, dest_mk) = CONJ_PAIR(define_new_type_bijections
174 {name=(tyname^"_repfns"), ABS=mkname, REP=destname, tyax=tyax})
175 in
176 (SPEC_ALL mk_dest, SPEC_ALL dest_mk)
177 end
178in
179val recspace_tydef =
180 new_basic_type_definition "recspace"
181 ("mk_rec","dest_rec") (CONJUNCT1 ZRECSPACE_RULES)
182end;
183
184(* ------------------------------------------------------------------------- *)
185(* Define lifted constructors. *)
186(* ------------------------------------------------------------------------- *)
187
188Definition BOTTOM[nocompute]:
189 BOTTOM = mk_rec (ZBOT:num->'a->bool)
190End
191
192Definition CONSTR[nocompute]:
193 CONSTR c i r : 'a recspace = mk_rec (ZCONSTR c i (\n. dest_rec(r n)))
194End
195
196(* ------------------------------------------------------------------------- *)
197(* Some lemmas. *)
198(* ------------------------------------------------------------------------- *)
199
200Theorem MK_REC_INJ:
201 !x y. (mk_rec x :'a recspace = mk_rec y)
202 ==> (ZRECSPACE x /\ ZRECSPACE y ==> (x = y))
203Proof
204 REPEAT GEN_TAC THEN DISCH_TAC THEN
205 REWRITE_TAC[snd recspace_tydef] THEN
206 DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM th]) THEN
207 ASM_REWRITE_TAC[]
208QED
209
210Theorem DEST_REC_INJ:
211 !x y. (dest_rec x = dest_rec y) = (x:'a recspace = y)
212Proof
213 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
214 POP_ASSUM(MP_TAC o Q.AP_TERM `mk_rec:(num->'a->bool)->'a recspace`) THEN
215 REWRITE_TAC[fst recspace_tydef]
216QED
217
218(* ------------------------------------------------------------------------- *)
219(* Show that the set is freely inductively generated. *)
220(* ------------------------------------------------------------------------- *)
221
222Theorem CONSTR_BOT:
223 !c i r. ~(CONSTR c i r :'a recspace = BOTTOM)
224Proof
225 REPEAT GEN_TAC THEN REWRITE_TAC[CONSTR, BOTTOM] THEN
226 DISCH_THEN(MP_TAC o MATCH_MP MK_REC_INJ) THEN
227 REWRITE_TAC[ZCONSTR_ZBOT, ZRECSPACE_RULES] THEN
228 MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN
229 SIMP_TAC bool_ss [fst recspace_tydef, snd recspace_tydef]
230QED
231
232Theorem CONSTR_INJ:
233 !c1 i1 r1 c2 i2 r2. (CONSTR c1 i1 r1 :'a recspace = CONSTR c2 i2 r2) <=>
234 (c1 = c2) /\ (i1 = i2) /\ (r1 = r2)
235Proof
236 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
237 POP_ASSUM(MP_TAC o REWRITE_RULE[CONSTR]) THEN
238 DISCH_THEN(MP_TAC o MATCH_MP MK_REC_INJ) THEN
239 W(C SUBGOAL_THEN ASSUME_TAC o funpow 2 lhand o snd) THENL [
240 CONJ_TAC THEN MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN
241 SIMP_TAC bool_ss [fst recspace_tydef, snd recspace_tydef],
242 ASM_REWRITE_TAC[] THEN REWRITE_TAC[ZCONSTR] THEN
243 REWRITE_TAC[INJP_INJ, INJN_INJ, INJF_INJ, INJA_INJ] THEN
244 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN BETA_TAC THEN
245 REWRITE_TAC[INV_SUC_EQ, DEST_REC_INJ]
246 ]
247QED
248
249Theorem CONSTR_IND:
250 !P. P(BOTTOM) /\
251 (!c i r. (!n. P(r n)) ==> P(CONSTR c i r)) ==>
252 !x:'a recspace. P(x)
253Proof
254 REPEAT STRIP_TAC THEN
255 MP_TAC(Q.SPEC `\z:num->'a->bool. ZRECSPACE(z) /\ P(mk_rec z)`
256 ZRECSPACE_INDUCT) THEN
257 BETA_TAC THEN ASM_REWRITE_TAC[ZRECSPACE_RULES, GSYM BOTTOM] THEN
258 W(C SUBGOAL_THEN ASSUME_TAC o funpow 2 lhand o snd) THENL [
259 REPEAT GEN_TAC THEN SIMP_TAC bool_ss [FORALL_AND_THM] THEN
260 REPEAT STRIP_TAC THENL [
261 MATCH_MP_TAC(CONJUNCT2 ZRECSPACE_RULES) THEN ASM_REWRITE_TAC[],
262 FIRST_ASSUM (fn implhs =>
263 FIRST_ASSUM (fn imp => (MP_TAC (HO_MATCH_MP imp implhs)))) THEN
264 REWRITE_TAC[CONSTR] THEN
265 RULE_ASSUM_TAC(REWRITE_RULE[snd recspace_tydef]) THEN
266 ASM_SIMP_TAC (bool_ss ++ ETA_ss) []
267 ],
268 ASM_REWRITE_TAC[] THEN
269 DISCH_THEN(MP_TAC o Q.SPEC `dest_rec (x:'a recspace)`) THEN
270 REWRITE_TAC[fst recspace_tydef] THEN
271 REWRITE_TAC[tautLib.TAUT_PROVE ``(a ==> a /\ b) = (a ==> b)``] THEN
272 DISCH_THEN MATCH_MP_TAC THEN
273 REWRITE_TAC[fst recspace_tydef, snd recspace_tydef]
274 ]
275QED
276
277(* ------------------------------------------------------------------------- *)
278(* Now prove the recursion theorem (this subcase is all we need). *)
279(* ------------------------------------------------------------------------- *)
280
281Theorem CONSTR_REC:
282 !Fn:num->'a->(num->'a recspace)->(num->'b)->'b.
283 ?f. (!c i r. f (CONSTR c i r) = Fn c i r (\n. f (r n)))
284Proof
285 REPEAT STRIP_TAC THEN
286 (MP_TAC o prove_nonschematic_inductive_relations_exist bool_monoset)
287 ``(Z:'a recspace->'b->bool) BOTTOM b /\
288 (!c i r y. (!n. Z (r n) (y n)) ==> Z (CONSTR c i r) (Fn c i r y))`` THEN
289 DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
290 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o GSYM)) THEN
291 Q.SUBGOAL_THEN `!x. ?!y. (Z:'a recspace->'b->bool) x y` MP_TAC THENL [
292 W(MP_TAC o HO_PART_MATCH rand CONSTR_IND o snd) THEN
293 DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THEN REPEAT GEN_TAC THENL [
294 FIRST_ASSUM
295 (fn t => GEN_REWRITE_TAC BINDER_CONV [GSYM t]) THEN
296 REWRITE_TAC[GSYM CONSTR_BOT, EXISTS_UNIQUE_REFL],
297 DISCH_THEN(MP_TAC o SIMP_RULE bool_ss [EXISTS_UNIQUE_THM,FORALL_AND_THM])
298 THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
299 DISCH_THEN(MP_TAC o SIMP_RULE bool_ss [SKOLEM_THM]) THEN
300 DISCH_THEN(Q.X_CHOOSE_THEN `y:num->'b` ASSUME_TAC) THEN
301 REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
302 FIRST_ASSUM(fn th => CHANGED_TAC(ONCE_REWRITE_TAC[GSYM th])) THEN
303 CONJ_TAC THENL [
304 Q.EXISTS_TAC
305 `(Fn:num->'a->(num->'a recspace)->(num->'b)->'b) c i r y` THEN
306 REWRITE_TAC[CONSTR_BOT, CONSTR_INJ, GSYM CONJ_ASSOC] THEN
307 SIMP_TAC hol_ss [RIGHT_EXISTS_AND_THM] THEN
308 Q.EXISTS_TAC `y:num->'b` THEN ASM_REWRITE_TAC[],
309 REWRITE_TAC[CONSTR_BOT, CONSTR_INJ, GSYM CONJ_ASSOC] THEN
310 SIMP_TAC hol_ss [RIGHT_EXISTS_AND_THM] THEN
311 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
312 REPEAT AP_TERM_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
313 Q.X_GEN_TAC `w:num` THEN FIRST_ASSUM MATCH_MP_TAC THEN
314 Q.EXISTS_TAC `w` THEN ASM_REWRITE_TAC[]
315 ]
316 ],
317 REWRITE_TAC[UNIQUE_SKOLEM_ALT] THEN
318 DISCH_THEN(Q.X_CHOOSE_THEN `fn:'a recspace->'b` (ASSUME_TAC o GSYM)) THEN
319 Q.EXISTS_TAC `fn:'a recspace->'b` THEN ASM_REWRITE_TAC[] THEN
320 REPEAT GEN_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN
321 FIRST_ASSUM(fn th => GEN_REWRITE_TAC I [GSYM th]) THEN
322 SIMP_TAC bool_ss []
323 ]
324QED
325
326(* ------------------------------------------------------------------------- *)
327(* The following is useful for coding up functions casewise. *)
328(* ------------------------------------------------------------------------- *)
329
330Definition FCONS[nocompute]:
331 (FCONS (a:'a) f 0 = a) /\
332 (FCONS (a:'a) f (SUC n) = f n)
333End
334
335Theorem FCONS_UNDO[local]:
336 !f:num->'a. f = FCONS (f 0) (f o SUC)
337Proof
338 GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
339 numLib.INDUCT_TAC THEN REWRITE_TAC[FCONS, combinTheory.o_THM]
340QED
341
342Definition FNIL[nocompute]: FNIL (n:num) = (ARB:'a)
343End
344
345(*---------------------------------------------------------------------------*)
346(* Destructor-style FCONS equation *)
347(*---------------------------------------------------------------------------*)
348
349Theorem FCONS_DEST:
350 FCONS a f n = if n = 0 then a else f (n-1)
351Proof
352 BasicProvers.Cases_on `n` THEN ASM_SIMP_TAC numLib.arith_ss [FCONS]
353QED
354
355(* ------------------------------------------------------------------------- *)
356(* Convenient definitions for type isomorphism. *)
357(* ------------------------------------------------------------------------- *)
358
359Definition ISO[nocompute]:
360 ISO (f:'a->'b) (g:'b->'a) <=> (!x. f(g x) = x) /\ (!y. g(f y) = y)
361End
362
363(* ------------------------------------------------------------------------- *)
364(* Composition theorems. *)
365(* ------------------------------------------------------------------------- *)
366
367Theorem ISO_REFL:
368 ISO (\x:'a. x) (\x. x)
369Proof
370 SIMP_TAC bool_ss [ISO]
371QED
372
373Theorem ISO_FUN:
374 ISO (f:'a->'c) f' /\ ISO (g:'b->'d) g' ==>
375 ISO (\h a'. g(h(f' a'))) (\h a. g'(h(f a)))
376Proof
377 REWRITE_TAC [ISO] THEN SIMP_TAC bool_ss [ISO, FUN_EQ_THM]
378QED
379 (* bug in the simplifier requires first rewrite to be performed *)
380
381(* ------------------------------------------------------------------------- *)
382(* The use we make of isomorphism when finished. *)
383(* ------------------------------------------------------------------------- *)
384
385Theorem ISO_USAGE:
386 ISO f g ==>
387 (!P. (!x. P x) = (!x. P(g x))) /\
388 (!P. (?x. P x) = (?x. P(g x))) /\
389 (!a b. (a = g b) = (f a = b))
390Proof
391 SIMP_TAC bool_ss [ISO, FUN_EQ_THM] THEN MESON_TAC[]
392QED
393
394(* ----------------------------------------------------------------------
395 Remove constants from top-level name-space
396 ---------------------------------------------------------------------- *)
397
398val _ = app (fn s => remove_ovl_mapping s {Name = s, Thy = "ind_type"})
399 ["NUMSUM", "INJN", "INJA", "INJF", "INJP",
400 "FCONS", "ZCONSTR", "ZBOT", "BOTTOM", "CONSTR", "FNIL", "ISO"]
401
402local open OpenTheoryMap in
403 val ns = ["HOL4","Datatype"]
404 fun c x = OpenTheory_const_name{const={Thy="ind_type",Name=x},name=(ns,x)}
405 val _ = OpenTheory_tyop_name{tyop={Thy="ind_type",Tyop="recspace"},name=(ns,"recspace")}
406 val _ = c "CONSTR"
407 val _ = c "FCONS"
408 val _ = c "FNIL"
409 val _ = c "BOTTOM"
410end