computability/turing/turing_machineScript.sml

121   (WF_REL_TAC `$<` >> rw[] >> fs[ODD_EXISTS] >>
139   completeInduct_on `n` >> Cases_on `n` >- EVAL_TAC >> rw[DECODE_def]
140   >- (rw[ENCODE_def]
143       >> `ENCODE (DECODE (n' DIV 2)) = n' DIV 2` by fs[] >> rw[]
148       >> rw[])
149   >> rw[ENCODE_def]
157   Induct_on `n` >- EVAL_TAC >> fs[] >> rw[DECODE_def]  );
248   rpt strip_tac >> rw[UPDATE_ACT_S_TM_def] );
253   rpt strip_tac >> rw[UPDATE_ACT_S_TM_def] );
258   rw[DECODE_def] >> Cases_on `DECODE n` >- `n=0` by fs[DECODE_EMPTY_lem] >>
264   rw[DECODE_def] >> metis_tac[EVEN_AND_ODD] );
268   rpt strip_tac  >> fs[MOD_2] >> `~EVEN n` by metis_tac[EVEN_AND_ODD] >> rw[]);
272   rw[] >> eq_tac >> simp[] >> csimp[fmap_EXT] >>
276   rw[] >>
292   rw[NUM_TO_ACT_def,ACT_TO_NUM_def] >>
294    (ACT_TO_NUM k = 3)` by simp[] >>rw[]>>
312   rw[UPDATE_TAPE_def,UPDATE_ACT_S_TM_def] >>
321   rw[DECODE_TM_TAPE_def])
340 rw[DECODE_TM_TAPE_def] >> `ODD (nsnd (nsnd tmn))` by metis_tac[EVEN_OR_ODD] >>
341   rw[ODD_DIV_2_lem]);
346   rw[DECODE_TM_TAPE_def] >> `ODD (nsnd (t))` by metis_tac[EVEN_OR_ODD] >>
347   rw[ODD_DIV_2_lem]);
352   rw[DECODE_TM_TAPE_def] >> metis_tac[EVEN_AND_ODD]);
357   rw[DECODE_TM_TAPE_def]);
367   rpt strip_tac >> `���j k. j *, k = n` by metis_tac[npair_cases] >> rw[] );
371   strip_tac >> rw[NUM_CELL_def,CELL_NUM_def]);
401   simp[FULL_ENCODE_TM_def,ENCODE_TM_TAPE_def] >> rw[] >> Cases_on `tm.tape_h` >- fs[] >- EVAL_TAC)
414 eq_tac >- (Cases_on ` a` >> Cases_on `b` >> rw[] ) >- (rw[]) )
436 rw[ENCODE_TM_TAPE_def]);
440 rw[DECODE_TM_TAPE_def,ENCODE_TM_TAPE_def] >> fs[EVEN_MULT,EVEN_ADD] >>
445 rw[ENCODE_TM_TAPE_def]);