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