1(*---------------------------------------------------------------------------*)
2(* Goedel's encoding : injection from num list to num. See also              *)
3(* numpairTheory in src/num/extra_theories.                                  *)
4(*---------------------------------------------------------------------------*)
5
6(* Interactive
7quietdec := true;
8app load ["primeFactorTheory", "bagTheory"];
9open arithmeticTheory dividesTheory primeFactorTheory bagTheory;
10quietdec := false;
11*)
12
13open HolKernel Parse boolLib bossLib
14     arithmeticTheory dividesTheory primeFactorTheory bagTheory;
15
16val _ = new_theory "goedelCode";
17
18val P_EUCLIDES = gcdTheory.P_EUCLIDES;
19
20(*---------------------------------------------------------------------------*)
21(* Goedel coding                                                             *)
22(*---------------------------------------------------------------------------*)
23
24val GCODE_def =
25 Define
26  `(GCODE i [] = 1) /\
27   (GCODE i (h::t) = (PRIMES(i) ** (h+1)) * GCODE (i+1) t)`;
28
29val ENCODE_def = Define `ENCODE list = GCODE 0 list`;
30
31val GCODE_EMPTY = Q.store_thm
32("GCODE_EMPTY",
33 `!n. GCODE n [] = 1`,
34 GEN_TAC THEN EVAL_TAC);
35
36val ZERO_LT_GCODE = Q.store_thm
37("ZERO_LT_GCODE",
38 `!list n. 0 < GCODE n list`,
39 Induct THEN RW_TAC list_ss [GCODE_EMPTY] THEN
40 Cases_on `h` THEN EVAL_TAC THEN
41 RW_TAC list_ss [ZERO_LT_EXP,ZERO_LESS_MULT] THEN
42 METIS_TAC [INDEX_LESS_PRIMES,primePRIMES,NOT_PRIME_0, DECIDE ``(x=0) \/ 0<x``]);
43
44val ONE_LT_GCODE = Q.store_thm
45("ONE_LT_GCODE",
46 `!h t n. 1 < GCODE n (h::t)`,
47 RW_TAC bool_ss [GCODE_def] THEN
48 MATCH_MP_TAC ONE_LT_MULT_IMP THEN CONJ_TAC THENL
49 [RW_TAC bool_ss [GSYM ADD1,EXP] THEN
50  METIS_TAC [ONE_LT_MULT_IMP,ONE_LT_PRIMES,ZERO_LT_PRIMES,ZERO_LT_EXP],
51  METIS_TAC [ZERO_LT_GCODE]]);
52
53val GCODE_EQ_1 = Q.store_thm
54("GCODE_EQ_1",
55 `!l n. (GCODE n l = 1) = (l=[])`,
56 Cases THEN RW_TAC list_ss [GCODE_EMPTY] THEN
57 MATCH_MP_TAC (DECIDE``b < a ==> a<>b``) THEN
58 RW_TAC arith_ss [GCODE_def] THEN
59 MATCH_MP_TAC ONE_LT_MULT_IMP THEN
60 RW_TAC bool_ss [ZERO_LT_GCODE,GSYM ADD1,EXP] THEN
61 METIS_TAC[ONE_LT_MULT_IMP,ONE_LT_PRIMES,ZERO_LT_PRIMES,ZERO_LT_EXP]);
62
63val lem1 = Q.prove
64(`!p q x. prime p /\ prime q /\ divides p (q ** x) ==> (p=q)`,
65 Induct_on `x` THEN RW_TAC arith_ss [EXP,DIVIDES_ONE] THENL
66 [METIS_TAC[NOT_PRIME_1],
67  METIS_TAC [prime_divides_only_self,P_EUCLIDES]]);
68
69val lem2 = Q.prove
70(`!n l x. BAG_IN x (PRIME_FACTORS (GCODE (n+1) l)) ==> PRIMES n < x`,
71 Induct_on `l` THENL
72 [RW_TAC arith_ss [GCODE_def] THEN
73    METIS_TAC [PRIME_FACTORS_1,NOT_IN_EMPTY_BAG],
74  REPEAT STRIP_TAC THEN
75  `divides x (GCODE (n + 1) (h::l))`
76    by METIS_TAC [PRIME_FACTOR_DIVIDES,ZERO_LT_GCODE] THEN
77  `prime x` by METIS_TAC [PRIME_FACTORS_def,ZERO_LT_GCODE] THEN
78  Q.PAT_X_ASSUM `divides a b` MP_TAC THEN RW_TAC arith_ss [GCODE_def] THEN
79  `divides x (PRIMES (n + 1) ** (h + 1)) \/ divides x (GCODE (n + 2) l)`
80    by METIS_TAC [P_EUCLIDES] THENL
81  [`x = PRIMES(n+1)` by METIS_TAC [lem1,primePRIMES] THEN
82     RW_TAC arith_ss [] THEN METIS_TAC [INFINITE_PRIMES,ADD1],
83   `PRIMES (n+1) < x`
84     by METIS_TAC [DIVISOR_IN_PRIME_FACTORS,DECIDE``n+2 = n+1+1``,ZERO_LT_GCODE]
85    THEN METIS_TAC [LESS_TRANS,INFINITE_PRIMES,ADD1]]]);
86
87val lem3 = Q.prove
88(`!d m x l. BAG_IN x (PRIME_FACTORS (GCODE (m + SUC d) l)) ==> PRIMES m < x`,
89 Induct THEN RW_TAC bool_ss [ADD_CLAUSES] THENL
90 [METIS_TAC [ADD1,lem2],
91  `PRIMES (SUC m) < x` by METIS_TAC [DECIDE``SUC(SUC(m+d)) = SUC m + SUC d``] THEN
92  METIS_TAC [LESS_TRANS,INFINITE_PRIMES,ADD1]]);
93
94val lem4 = Q.prove
95(`!m n l x. m < n /\ BAG_IN x (PRIME_FACTORS (GCODE n l)) ==> PRIMES m < x`,
96 METIS_TAC[lem3,LESS_ADD_1,ADD1]);
97
98val lem5 = Q.prove
99(`!l a. PRIME_FACTORS (GCODE (a + 1) l) (PRIMES a) = 0`,
100 RW_TAC arith_ss [NOT_BAG_IN] THEN STRIP_TAC THEN
101 METIS_TAC [lem4,DECIDE ``~(x < x) /\ a < a+1``]);
102
103val lem6 = Q.prove
104(`PRIME_FACTORS ((PRIMES i ** (h+1)) * GCODE (i+1) t) (PRIMES i) = h+1`,
105 `0 < GCODE (i+1) t` by METIS_TAC [ZERO_LT_GCODE] THEN
106 `0 < PRIMES i ** (h+1)` by RW_TAC arith_ss [ZERO_LT_EXP,ZERO_LT_PRIMES] THEN
107 RW_TAC arith_ss [PRIME_FACTORS_MULT,ZERO_LT_EXP, ZERO_LT_PRIMES,
108       ZERO_LT_GCODE,BAG_UNION,PRIME_FACTORS_EXP,primePRIMES,lem5]);
109
110(*---------------------------------------------------------------------------*)
111(* Injectivity                                                               *)
112(*---------------------------------------------------------------------------*)
113
114val GCODE_11 = Q.store_thm
115("GCODE_11",
116  `!l1 l2 a. (GCODE a l1 = GCODE a l2) ==> (l1=l2)`,
117 Induct THENL
118 [METIS_TAC [GCODE_EQ_1, GCODE_def],
119  GEN_TAC THEN Induct THENL
120  [METIS_TAC [GCODE_EQ_1, GCODE_def],
121   POP_ASSUM (K ALL_TAC) THEN REPEAT GEN_TAC THEN
122   SIMP_TAC list_ss [GCODE_def] THEN STRIP_TAC THEN
123   `0 < PRIMES a ** (h+1) /\ 0 < PRIMES a ** (h'+1) /\
124    0 < GCODE (a+1) l1 /\ 0 < GCODE (a+1) l2`
125      by METIS_TAC [primePRIMES,ZERO_LT_PRIMES,ZERO_LT_EXP,ZERO_LT_GCODE] THEN
126   `PRIME_FACTORS (PRIMES a ** (h + 1) * GCODE (a + 1) l1) =
127    PRIME_FACTORS (PRIMES a ** (h' + 1) * GCODE (a + 1) l2)`
128      by METIS_TAC[] THEN
129   `BAG_UNION (PRIME_FACTORS (PRIMES a ** (h + 1)))
130              (PRIME_FACTORS (GCODE (a + 1) l1))
131      =
132    BAG_UNION (PRIME_FACTORS (PRIMES a ** (h' + 1)))
133              (PRIME_FACTORS (GCODE (a + 1) l2))`
134     by METIS_TAC [PRIME_FACTORS_MULT] THEN
135   `(BAG_UNION (PRIME_FACTORS (PRIMES a ** (h + 1)))
136               (PRIME_FACTORS (GCODE (a + 1) l1))) (PRIMES a) = h+1`
137      by SIMP_TAC arith_ss [BAG_UNION,PRIME_FACTORS_EXP,primePRIMES,lem5] THEN
138   `(BAG_UNION (PRIME_FACTORS (PRIMES a ** (h' + 1)))
139               (PRIME_FACTORS (GCODE (a + 1) l2))) (PRIMES a) = h'+1`
140     by SIMP_TAC arith_ss [BAG_UNION,PRIME_FACTORS_EXP,primePRIMES,lem5] THEN
141   `h = h'` by METIS_TAC [DECIDE ``(a+1 = b+1) = (a=b)``] THEN
142   RW_TAC arith_ss [] THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN
143   `PRIME_FACTORS (GCODE (a + 1) l1) = PRIME_FACTORS (GCODE (a + 1) l2)`
144     by METIS_TAC [BAG_UNION_EQ_LEFT] THEN
145   METIS_TAC [PRIME_FACTORS_def]]]);
146
147val ENCODE_11 = Q.store_thm
148("ENCODE_11",
149  `!l1 l2. (ENCODE l1 = ENCODE l2) ==> (l1=l2)`,
150 METIS_TAC [GCODE_11,ENCODE_def]);
151
152(*---------------------------------------------------------------------------*)
153(* Explicitly give decoder ... similar development as                        *)
154(*                                                                           *)
155(*       src/num/extra_theories/numpairScript.                               *)
156(*---------------------------------------------------------------------------*)
157
158val GDECODE_def =
159 tDefine
160 "GDECODE"
161 `GDECODE i gn =
162   if gn = 0 then NONE else
163   if gn = 1 then SOME [] else
164   case PRIME_FACTORS gn (PRIMES i)
165     of 0 => NONE
166      | SUC n =>
167          case GDECODE (i+1) (gn DIV (PRIMES i ** (n+1)))
168           of NONE => NONE
169            | SOME l => SOME (n::l)`
170(WF_REL_TAC `measure SND` THEN
171 RW_TAC arith_ss [DECIDE ``x <> 0 = 0 < x``] THEN
172 MATCH_MP_TAC DIV_LESS THEN
173 RW_TAC arith_ss [ONE_LT_EXP,ONE_LT_PRIMES,ZERO_LT_EXP]);
174
175val GDECODE_ind = fetch "-" "GDECODE_ind";
176
177val lem7 = Q.prove
178(`(PRIME_FACTORS (GCODE i (h::t)) (PRIMES i) = SUC n) ==> (h=n)`,
179 RW_TAC arith_ss [GCODE_def] THEN FULL_SIMP_TAC arith_ss [lem6]);
180
181val lem8 = Q.prove
182(`GCODE i (h::t) DIV (PRIMES i ** (h+1)) = GCODE (i+1) t`,
183 RW_TAC arith_ss [GCODE_def] THEN
184 RW_TAC bool_ss [Once MULT_SYM] THEN
185 `0 < PRIMES i ** (h+1)` by RW_TAC arith_ss [ZERO_LT_EXP,ZERO_LT_PRIMES] THEN
186 RW_TAC arith_ss [MULT_DIV]);
187
188val lem9 = Q.prove
189(`!i h t. GCODE (i+1) t < GCODE i (h::t)`,
190 RW_TAC arith_ss [GCODE_def,ZERO_LT_GCODE,ONE_LT_EXP,ONE_LT_PRIMES]);
191
192val lem10 = Q.prove
193(`!gn i nl. (gn = GCODE i nl) ==> (GDECODE i gn = SOME nl)`,
194 completeInduct_on `gn` THEN RW_TAC arith_ss [Once GDECODE_def] THENL
195 [
196  FULL_SIMP_TAC list_ss [GCODE_EQ_1],
197  METIS_TAC [ZERO_LT_GCODE,DECIDE ``0 < x = x <> 0``],
198  `?h t. nl = h::t` by METIS_TAC [listTheory.list_CASES,GCODE_EQ_1] THEN
199  Q.PAT_X_ASSUM `a <> b` (K ALL_TAC) THEN POP_ASSUM SUBST_ALL_TAC THEN
200  REPEAT CASE_TAC THENL
201  [POP_ASSUM MP_TAC THEN RW_TAC arith_ss [GCODE_def] THEN
202    `0 < GCODE (i+1) t` by METIS_TAC [ZERO_LT_GCODE] THEN
203     `0 < PRIMES i ** (h + 1)` by RW_TAC arith_ss [ZERO_LT_EXP,ZERO_LT_PRIMES] THEN
204     RW_TAC arith_ss
205           [PRIME_FACTORS_MULT,BAG_UNION,PRIME_FACTORS_EXP,primePRIMES],
206   `h = n` by METIS_TAC [lem7] THEN RW_TAC arith_ss [] THEN
207      FULL_SIMP_TAC arith_ss [lem8] THEN
208      METIS_TAC [lem9,optionTheory.NOT_SOME_NONE],
209   `h = n` by METIS_TAC [lem7] THEN RW_TAC arith_ss [] THEN
210      FULL_SIMP_TAC arith_ss [lem8] THEN
211      METIS_TAC [lem9,optionTheory.SOME_11]]]);
212
213val GDECODE_GCODE = Q.store_thm
214("GDECODE_GCODE",
215 `!nl i. GDECODE i (GCODE i nl) = SOME nl`,
216 METIS_TAC [lem10]);
217
218val DECODE_def = Define `DECODE gn = THE (GDECODE 0 gn)`;
219
220val DECODE_ENCODE = Q.store_thm
221("DECODE_ENCODE",
222 `!nl. DECODE (ENCODE nl) = nl`,
223 RW_TAC arith_ss [DECODE_def, ENCODE_def,GDECODE_GCODE,optionTheory.THE_DEF]);
224
225
226(*---------------------------------------------------------------------------*)
227(* Standard list operators lifted to gnums                                   *)
228(*---------------------------------------------------------------------------*)
229
230val gNIL_def  = Define `gNIL = ENCODE []`;
231val gCONS_def = Define `gCONS n gn = ENCODE (n::DECODE gn)`;
232val gHD_def   = Define `gHD gn = HD (DECODE gn)`;
233val gTL_def   = Define `gTL gn = ENCODE (TL (DECODE gn))`;
234val gLEN_def  = Define `gLEN gn = LENGTH (DECODE gn)`;
235val gAPPEND_def = Define`gAPPEND gn1 gn2 = ENCODE (DECODE gn1 ++ DECODE gn2)`;
236val gMAP_def   = Define `gMAP f gn = ENCODE (MAP f (DECODE gn))`;
237val gFOLDL_def = Define `gFOLDL f a gn = FOLDL f a (DECODE gn)`;
238val gFOLDR_def = Define `gFOLDR f a gn = FOLDR f a (DECODE gn)`;
239
240val gCONS_ENCODE = Q.store_thm
241("gCONS_ENCODE",
242 `!nl. gCONS n (ENCODE nl) = ENCODE (n::nl)`,
243 RW_TAC arith_ss [gCONS_def, DECODE_ENCODE]);
244
245val gLEN_ENCODE = Q.store_thm
246("gLEN_ENCODE",
247 `!nl. gLEN (ENCODE nl) = LENGTH nl`,
248 RW_TAC arith_ss [gLEN_def, DECODE_ENCODE]);
249
250val gAPPEND_ENCODE = Q.store_thm
251("gAPPEND_ENCODE",
252 `!nl1 nl2. gAPPEND (ENCODE nl1) (ENCODE nl2) = ENCODE (APPEND nl1 nl2)`,
253 RW_TAC arith_ss [gAPPEND_def, DECODE_ENCODE]);
254
255val gMAP_ENCODE = Q.store_thm
256("gMAP_ENCODE",
257 `gMAP f (ENCODE nl) = ENCODE (MAP f nl)`,
258 RW_TAC arith_ss [gMAP_def, DECODE_ENCODE]);
259
260val gFOLDL_ENCODE = Q.store_thm
261("gFOLDL_ENCODE",
262 `gFOLDL f a (ENCODE nl) = FOLDL f a nl`,
263 RW_TAC arith_ss [gFOLDL_def, DECODE_ENCODE]);
264
265val gFOLDR_ENCODE = Q.store_thm
266("gFOLDR_ENCODE",
267 `gFOLDR f a (ENCODE nl) = FOLDR f a nl`,
268 RW_TAC arith_ss [gFOLDR_def, DECODE_ENCODE]);
269
270val _ = export_theory();
271