8 assume mk_num (IND_SUC (dest_num m)) =
9 mk_num (IND_SUC (dest_num n)) [3];
12 NUM_REP (dest_num p) [5]
13 by REWRITE_TAC[fst num_tydef; snd num_tydef] ;
14 thus NUM_REP (IND_SUC (dest_num p))
15 by MATCH_MP_TAC (CONJUNCT2 NUM_REP_RULES) from 5;
17 !p. NUM_REP (IND_SUC (dest_num p)) [6] by GEN_TAC from 4;
19 assume !p. dest_num (mk_num (IND_SUC (dest_num p))) =
20 IND_SUC (dest_num p) [8];
21 mk_num (dest_num m) = mk_num (dest_num n) ==> m = n [9]
22 by REWRITE_TAC[fst num_tydef];
23 dest_num m = dest_num n ==> m = n [10]
24 by DISCH_THEN(MP_TAC o AP_TERM (parse_term "mk_num")) from 9;
25 thus dest_num (mk_num (IND_SUC (dest_num m))) =
26 dest_num (mk_num (IND_SUC (dest_num n)))
27 ==> m = n by ASM_REWRITE_TAC[IND_SUC_INJ],8 from 10;
29 (!p. dest_num (mk_num (IND_SUC (dest_num p))) =
31 ==> dest_num (mk_num (IND_SUC (dest_num m))) =
32 dest_num (mk_num (IND_SUC (dest_num n)))
33 ==> m = n [11] by DISCH_TAC from 7;
34 (!p. NUM_REP (IND_SUC (dest_num p)))
35 ==> dest_num (mk_num (IND_SUC (dest_num m))) =
36 dest_num (mk_num (IND_SUC (dest_num n)))
37 ==> m = n [12] by REWRITE_TAC[fst num_tydef; snd num_tydef] from 11;
38 dest_num (mk_num (IND_SUC (dest_num m))) =
39 dest_num (mk_num (IND_SUC (dest_num n)))
41 by SUBGOAL_THEN (parse_term "!p. NUM_REP (IND_SUC (dest_num p))")
44 by POP_ASSUM(MP_TAC o AP_TERM (parse_term "dest_num")),3 from 13;
46 mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n))
47 ==> m = n [14] by DISCH_TAC from 2;
50 thus mk_num (IND_SUC (dest_num m)) =
51 mk_num (IND_SUC (dest_num n)) by ASM_REWRITE_TAC[],16;
54 ==> mk_num (IND_SUC (dest_num m)) =
55 mk_num (IND_SUC (dest_num n)) [17] by DISCH_TAC from 15;
56 mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) <=>
57 m = n [18] by EQ_TAC from 14,17;
58 thus SUC m = SUC n <=> m = n by REWRITE_TAC[SUC_DEF] from 18;
60 thus !m n. SUC m = SUC n <=> m = n by REPEAT GEN_TAC from 1;
64 let SUC_INJ_2 = thm `;
65 !m n. SUC m = SUC n <=> m = n [1]
68 mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n))
71 assume mk_num (IND_SUC (dest_num m)) =
72 mk_num (IND_SUC (dest_num n)) [3];
73 !p. NUM_REP (IND_SUC (dest_num p)) [4]
76 NUM_REP (dest_num p) [5]
77 by REWRITE_TAC[fst num_tydef; snd num_tydef];
78 qed by MATCH_MP_TAC (CONJUNCT2 NUM_REP_RULES) from 5;
79 (!p. dest_num (mk_num (IND_SUC (dest_num p))) =
81 ==> dest_num (mk_num (IND_SUC (dest_num m))) =
82 dest_num (mk_num (IND_SUC (dest_num n)))
85 assume !p. dest_num (mk_num (IND_SUC (dest_num p))) =
86 IND_SUC (dest_num p) [7];
87 mk_num (dest_num m) = mk_num (dest_num n) ==> m = n [8]
88 by REWRITE_TAC[fst num_tydef];
89 dest_num m = dest_num n ==> m = n [9]
90 by DISCH_THEN(MP_TAC o AP_TERM (parse_term "mk_num")) from 8;
91 qed by ASM_REWRITE_TAC[IND_SUC_INJ],* from 9;
92 (!p. NUM_REP (IND_SUC (dest_num p)))
93 ==> dest_num (mk_num (IND_SUC (dest_num m))) =
94 dest_num (mk_num (IND_SUC (dest_num n)))
95 ==> m = n [10] by REWRITE_TAC[fst num_tydef; snd num_tydef] from 6;
96 dest_num (mk_num (IND_SUC (dest_num m))) =
97 dest_num (mk_num (IND_SUC (dest_num n)))
99 by SUBGOAL_THEN (parse_term "!p. NUM_REP (IND_SUC (dest_num p))")
102 qed by POP_ASSUM(MP_TAC o AP_TERM (parse_term "dest_num")),3 from 11;
104 ==> mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) [12]
107 qed by ASM_REWRITE_TAC[],*;
108 mk_num (IND_SUC (dest_num m)) = mk_num (IND_SUC (dest_num n)) <=>
109 m = n [14] by EQ_TAC from 2,12;
110 qed by REWRITE_TAC[SUC_DEF] from 14;`;;
112 let num_INDUCTION_ = thm `;
117 assume !n. P n ==> P (SUC n);
122 NUM_REP i [3] by ASM_REWRITE_TAC[],*;
123 thus NUM_REP (IND_SUC i)
124 by MATCH_MP_TAC(CONJUNCT2 NUM_REP_RULES) from 3;
130 NUM_REP i [5] by FIRST_ASSUM MATCH_ACCEPT_TAC,*;
131 dest_num (mk_num i) = i [6] by REWRITE_TAC[GSYM(snd num_tydef)] from 5;
132 i = dest_num (mk_num i) [7] by CONV_TAC SYM_CONV from 6;
133 mk_num (IND_SUC i) = mk_num (IND_SUC (dest_num (mk_num i))) [8]
134 by REPEAT AP_TERM_TAC from 7;
135 mk_num (IND_SUC i) = SUC (mk_num i) [9] by REWRITE_TAC[SUC_DEF] from 8;
136 P (mk_num i) [10] by FIRST_ASSUM MATCH_ACCEPT_TAC,*;
137 P (SUC (mk_num i)) [11] by FIRST_ASSUM MATCH_MP_TAC,* from 10;
138 thus P (mk_num (IND_SUC i))
139 by SUBGOAL_THEN (parse_term "mk_num(IND_SUC i) = SUC(mk_num i)")
143 !i. NUM_REP i /\ P (mk_num i)
144 ==> NUM_REP (IND_SUC i) /\ P (mk_num (IND_SUC i)) [12]
145 by REPEAT STRIP_TAC from 2,4;
146 (NUM_REP (dest_num n)
147 ==> NUM_REP (dest_num n) /\ P (mk_num (dest_num n)))
148 ==> P n [13] by REWRITE_TAC[fst num_tydef; snd num_tydef];
149 (!a. NUM_REP a ==> NUM_REP a /\ P (mk_num a)) ==> P n [14]
150 by DISCH_THEN(MP_TAC o SPEC (parse_term "dest_num n")) from 13;
151 ((!i. NUM_REP i /\ P (mk_num i)
152 ==> NUM_REP (IND_SUC i) /\ P (mk_num (IND_SUC i)))
153 ==> (!a. NUM_REP a ==> NUM_REP a /\ P (mk_num a)))
155 by W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd)
157 ((\i. NUM_REP i /\ P (mk_num i)) IND_0 /\
158 (!i. (\i. NUM_REP i /\ P (mk_num i)) i
159 ==> (\i. NUM_REP i /\ P (mk_num i)) (IND_SUC i))
160 ==> (!a. NUM_REP a ==> (\i. NUM_REP i /\ P (mk_num i)) a))
161 ==> P n [16] by ASM_REWRITE_TAC[GSYM ZERO_DEF; NUM_REP_RULES],* from 15;
162 thus P n by MP_TAC (SPEC (parse_term
163 "\\i. NUM_REP i /\\ P(mk_num i):bool") NUM_REP_INDUCT) from 16;
165 thus !P. P(_0) /\ (!n. P(n) ==> P(SUC n)) ==> !n. P n
166 by REPEAT STRIP_TAC from 1;
169 let num_RECURSION_STD = thm `;
170 !e:Z f. ?fn. (fn 0 = e) /\ (!n. fn (SUC n) = f n (fn n))
172 !e:Z f. ?fn. fn 0 = e /\ (!n. fn (SUC n) = f n (fn n)) [1]
176 (?fn. fn 0 = e /\ (!n. fn (SUC n) = (\z n. f n z) (fn n) n))
177 ==> (?fn. fn 0 = e /\ (!n. fn (SUC n) = f n (fn n))) [2]
179 qed by MP_TAC(ISPECL [(parse_term "e:Z");
180 (parse_term "(\\z n. (f:num->Z->Z) n z)")] num_RECURSION) from 2;
181 qed by REPEAT GEN_TAC from 1;