1open HolKernel boolLib bossLib Parse 2 3open pure_dBTheory normal_orderTheory 4 5fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n] 6 7val _ = new_theory "dnoreduct" 8 9val dest_dabs_def = Define` 10 (dest_dabs (dABS t) = t) 11`; 12val _ = export_rewrites ["dest_dabs_def"] 13 14val dnoreduct_def = Define` 15 (dnoreduct (dV i) = NONE) ��� 16 (dnoreduct (dAPP t u) = 17 if is_dABS t then SOME (nsub u 0 (dest_dabs t)) 18 else if dbnf t then OPTION_MAP (dAPP t) (dnoreduct u) 19 else SOME (dAPP (THE (dnoreduct t)) u)) ��� 20 (dnoreduct (dABS t) = OPTION_MAP dABS (dnoreduct t)) 21`; 22val _ = export_rewrites ["dnoreduct_def"] 23 24val notbnf_noreduct = prove( 25 ``��bnf t ��� ���u. noreduct t = SOME u``, 26 Cases_on `noreduct t` THEN1 FULL_SIMP_TAC (srw_ss()) [noreduct_bnf] THEN 27 SRW_TAC [][]); 28 29val notbnf_dnoreduct = store_thm( 30 "notbnf_dnoreduct", 31 ``��dbnf t ��� ���u. dnoreduct t = SOME u``, 32 Induct_on `t` THEN SRW_TAC [][]); 33 34val dnoreduct_dbeta = store_thm( 35 "dnoreduct_dbeta", 36 ``���t u. (dnoreduct t = SOME u) ��� dbeta t u``, 37 Induct_on `t` THEN SRW_TAC [][] THENL [ 38 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 39 METIS_TAC [dbeta_rules], 40 METIS_TAC [dbeta_rules], 41 IMP_RES_TAC notbnf_dnoreduct THEN SRW_TAC [][] THEN 42 METIS_TAC [dbeta_rules], 43 METIS_TAC [dbeta_rules] 44 ]); 45 46val dnoreduct_FV = store_thm( 47 "dnoreduct_FV", 48 ``(dnoreduct t = SOME u) ��� v ��� dFV u ��� v ��� dFV t``, 49 STRIP_TAC THEN IMP_RES_TAC dnoreduct_dbeta THEN 50 FULL_SIMP_TAC (srw_ss()) [dbeta_dbeta'_eqn] THEN 51 `���tt uu. (t = fromTerm tt) ��� (u = fromTerm uu)` 52 by METIS_TAC [fromTerm_onto] THEN 53 FULL_SIMP_TAC (srw_ss()) [IN_dFV, dbeta'_eq_ccbeta] THEN 54 METIS_TAC [chap3Theory.cc_beta_FV_SUBSET, pred_setTheory.SUBSET_DEF]); 55 56val dpm_is_dABS = Store_thm( 57 "dpm_is_dABS", 58 ``is_dABS (dpm �� t) = is_dABS t``, 59 Cases_on `t` THEN SRW_TAC [][]); 60 61val dpm_dbnf = Store_thm( 62 "dpm_dbnf", 63 ``�����. dbnf (dpm �� t) = dbnf t``, 64 Induct_on `t` THEN SRW_TAC [][]); 65 66val dest_dabs_dpm = store_thm( 67 "dest_dabs_dpm", 68 ``is_dABS d ��� (dest_dabs (dpm �� d) = dpm (inc_pm 0 ��) (dest_dabs d))``, 69 Cases_on `d` THEN SRW_TAC [][]); 70 71val dnoreduct_dpm = store_thm( 72 "dnoreduct_dpm", 73 ``���d ��. dnoreduct (dpm �� d) = OPTION_MAP (dpm ��) (dnoreduct d)``, 74 Induct_on `d` THEN 75 SRW_TAC [][dpm_nsub, optionTheory.OPTION_MAP_COMPOSE, combinTheory.o_DEF, 76 dest_dabs_dpm] THEN 77 IMP_RES_TAC notbnf_dnoreduct THEN SRW_TAC [][]); 78 79val dnoreduct_dLAM = Store_thm( 80 "dnoreduct_dLAM", 81 ``dnoreduct (dLAM i t) = OPTION_MAP (dLAM i) (dnoreduct t)``, 82 SRW_TAC [][dLAM_def] THEN 83 `dLAM i = ��t. dLAM i t` by SRW_TAC [][FUN_EQ_THM] THEN 84 POP_ASSUM SUBST1_TAC THEN SRW_TAC [][dLAM_def] THEN 85 Q.ABBREV_TAC `MX = if dFV t = {} then 0 else MAX_SET (dFV t)` THEN 86 `���i. i ��� dFV t ��� i ��� MX` 87 by SRW_TAC [][Abbr`MX`, pred_setTheory.MAX_SET_DEF] THEN 88 Q.ABBREV_TAC `�� = lifting_pm 0 MX` THEN 89 `lift t 0 = dpm �� t` 90 by SRW_TAC [][lifts_are_specific_dpms, Abbr`��`] THEN 91 `0 ��� dFV (lift t 0)` by SRW_TAC [][] THEN 92 `sub (dV 0) (i + 1) (lift t 0) = dpm [(n2s 0, n2s (i + 1))] (lift t 0)` 93 by SRW_TAC [][fresh_dpm_sub] THEN 94 SRW_TAC [][dnoreduct_dpm, optionTheory.OPTION_MAP_COMPOSE] THEN 95 `(dnoreduct t = NONE) ��� ���u. dnoreduct t = SOME u` 96 by (Cases_on `dnoreduct t` THEN SRW_TAC [][]) THEN 97 SRW_TAC [][] THEN 98 `���i. i ��� dFV u ��� i ��� MX` by METIS_TAC [dnoreduct_FV] THEN 99 `lift u 0 = dpm �� u` 100 by SRW_TAC [][lifts_are_specific_dpms, Abbr`��`] THEN 101 `0 ��� dFV (lift u 0)` by SRW_TAC [][] THEN 102 `sub (dV 0) (i + 1) (lift u 0) = dpm [(n2s 0, n2s (i + 1))] (lift u 0)` 103 by SRW_TAC [][fresh_dpm_sub] THEN 104 SRW_TAC [][]); 105 106val dnoreduct_correct = store_thm( 107 "dnoreduct_correct", 108 ``���t. noreduct t = OPTION_MAP toTerm (dnoreduct (fromTerm t))``, 109 HO_MATCH_MP_TAC termTheory.simple_induction THEN 110 SRW_TAC [][noreduct_thm, optionTheory.OPTION_MAP_COMPOSE, 111 combinTheory.o_DEF] 112 THENL [ 113 `���v t0. t = LAM v t0` 114 by (Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC termTheory.term_CASES THEN 115 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []) THEN 116 ASM_SIMP_TAC (srw_ss()) [noreduct_thm, dLAM_def, GSYM sub_nsub, 117 GSYM fromTerm_subst], 118 119 `��dbnf (fromTerm t)` by SRW_TAC [][] THEN 120 IMP_RES_TAC notbnf_dnoreduct THEN SRW_TAC [][] 121 ]); 122 123val omap_lemma = prove(``OPTION_MAP (��x. x) y = y``, 124 Cases_on `y` THEN SRW_TAC [][]) 125 126val dnoreduct_thm = Store_thm( 127 "dnoreduct_thm", 128 ``(dnoreduct (fromTerm t) = OPTION_MAP fromTerm (noreduct t)) ��� 129 (noreduct (toTerm d) = OPTION_MAP toTerm (dnoreduct d))``, 130 SRW_TAC [][dnoreduct_correct, optionTheory.OPTION_MAP_COMPOSE, 131 combinTheory.o_DEF, omap_lemma]); 132 133val _ = export_theory() 134