1open HolKernel boolLib bossLib Parse 2 3open normal_orderTheory 4open reductionEval 5 6fun Store_thm (trip as (n,t,tac)) = store_thm trip before export_rewrites [n] 7 8val _ = new_theory "steps" 9 10val steps_def = Define` 11 (steps 0 t = t) ��� 12 (steps (SUC n) t = if bnf t then t else steps n (THE (noreduct t))) 13`; 14val _ = export_rewrites ["steps_def"] 15 16val bnf_steps = store_thm( 17 "bnf_steps", 18 ``(bnf_of t = SOME u) ��� ���n. (steps n t = u) ��� bnf u``, 19 SRW_TAC [][EQ_IMP_THM] THENL [ 20 IMP_RES_TAC bnf_of_SOME THEN SRW_TAC [][] THEN 21 Q.PAT_ASSUM `t -n->* u` MP_TAC THEN 22 MAP_EVERY Q.ID_SPEC_TAC [`u`, `t`] THEN 23 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN1 24 (Q.EXISTS_TAC `0` THEN SRW_TAC[][]) THEN 25 Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][] THEN1 26 (METIS_TAC [normorder_bnf]) THEN 27 FULL_SIMP_TAC (srw_ss()) [noreduct_characterisation], 28 29 POP_ASSUM MP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`t`,`n`] THEN 30 Induct THEN SRW_TAC [][] THENL [ 31 MATCH_MP_TAC nstar_bnf_of_SOME_I THEN SRW_TAC [][], 32 MATCH_MP_TAC nstar_bnf_of_SOME_I THEN SRW_TAC [][], 33 SRW_TAC [][Once bnf_of_thm] 34 ] 35 ]); 36 37val RTC_L1_I = CONJUNCT2 (SPEC_ALL relationTheory.RTC_RULES) 38 39val steps_nstar = store_thm( 40 "steps_nstar", 41 ``���n t. t -n->* steps n t``, 42 Induct THEN SRW_TAC [][] THEN MATCH_MP_TAC RTC_L1_I THEN 43 Q.EXISTS_TAC `THE (noreduct t)` THEN SRW_TAC [][] THEN 44 `���u. t -n-> u` by METIS_TAC [normorder_bnf] THEN 45 `noreduct t = SOME u` by METIS_TAC [noreduct_characterisation] THEN 46 SRW_TAC [][]); 47 48val bnf_steps_upwards_closed = store_thm( 49 "bnf_steps_upwards_closed", 50 ``���n m t. bnf (steps n t) ��� n < m ��� (steps m t = steps n t)``, 51 Induct_on `n` THEN SRW_TAC [][] THENL [ 52 Cases_on `m` THEN SRW_TAC [][], 53 Cases_on `m` THEN SRW_TAC [][], 54 Cases_on `m` THEN FULL_SIMP_TAC (srw_ss()) [] 55 ]); 56 57val nstar_steps = store_thm( 58 "nstar_steps", 59 ``���M N. M -n->* N ��� ���n. N = steps n M``, 60 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN1 61 (Q.EXISTS_TAC `0` THEN SRW_TAC [][]) THEN 62 FULL_SIMP_TAC (srw_ss()) [noreduct_characterisation] THEN 63 Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][] THEN 64 FULL_SIMP_TAC (srw_ss()) [SYM noreduct_bnf]); 65 66val steps_noreduct = store_thm( 67 "steps_noreduct", 68 ``���t. ��bnf (steps n t) ��� 69 (steps n (THE (noreduct t)) = THE (noreduct (steps n t)))``, 70 Induct_on `n` THEN SRW_TAC [][] THEN 71 POP_ASSUM MP_TAC THEN Cases_on `n` THEN SRW_TAC [][]); 72 73val steps_plus = store_thm( 74 "steps_plus", 75 ``���t. steps (m + n) t = steps m (steps n t)``, 76 Induct_on `m` THEN SRW_TAC [][arithmeticTheory.ADD_CLAUSES] THENL [ 77 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [], 78 POP_ASSUM MP_TAC THEN Cases_on `n` THEN SRW_TAC [][], 79 `steps n (THE (noreduct t)) = steps n t` 80 by METIS_TAC [bnf_steps_upwards_closed, steps_def, 81 DECIDE ``n < SUC n``] THEN 82 Cases_on `m` THEN SRW_TAC [][], 83 SRW_TAC [][steps_noreduct] 84 ]); 85 86val bnf_steps_fixpoint = store_thm( 87 "bnf_steps_fixpoint", 88 ``bnf M ��� (steps n M = M)``, 89 METIS_TAC [bnf_steps_upwards_closed, DECIDE ``0 < n ��� (n = 0)``, steps_def]); 90 91val _ = export_theory () 92