1timer true;; 2 3new_theory `MULT_FUN`;; 4 5new_parent `MULT_FUN_CURRY`;; 6 7% 8 |- !i1 i2 m n t. 9 MULT_FUN((i1,i2),m,n,t) = 10 (t => 11 (m,n,t) | 12 MULT_FUN((i1,i2),((i1=0)=>m|i2+m),n-1,((((n-1)-1)=0) \/ (i2=0)))) 13% 14 15let MULT_FUN_DEF = theorem `MULT_FUN_CURRY` `MULT_FUN_DEF`;; 16 17let MULT_FUN_T = 18 prove_thm 19 (`MULT_FUN_T`, 20 "!i1 i2 m n. 21 MULT_FUN((i1,i2),m,n,T) = (m,n,T)", 22 REPEAT GEN_TAC 23 THEN ASM_CASES_TAC "t" 24 THEN REWRITE_TAC[INST["T","t:bool"](SPEC_ALL MULT_FUN_DEF)]);; 25 26let MULT_FUN_F = 27 prove_thm 28 (`MULT_FUN_F`, 29 "!i1 i2 m n. 30 MULT_FUN((i1,i2),m,n,F) = 31 MULT_FUN((i1,i2),((i1=0)=>m|i2+m),n-1,((((n-1)-1)=0) \/ (i2=0)))", 32 REPEAT GEN_TAC 33 THEN ASM_CASES_TAC "t:bool" 34 THEN REWRITE_TAC[INST["F","t:bool"](SPEC_ALL MULT_FUN_DEF)]);; 35 36let LESS_EQ_0 = 37 prove_thm 38 (`LESS_EQ_0`, 39 "!m. 0 <= m", 40 INDUCT_TAC 41 THEN ASM_REWRITE_TAC[LESS_OR_EQ;LESS_0]);; 42 43let LESS_EQ_SUC_1 = 44 prove_thm 45 (`LESS_EQ_SUC_1`, 46 "!m. 1 <= SUC m", 47 INDUCT_TAC 48 THEN ASM_REWRITE_TAC[num_CONV "1";LESS_OR_EQ;LESS_MONO_EQ;LESS_0]);; 49 50let SUB_LEMMA1 = 51 prove_thm 52 (`SUB_LEMMA1`, 53 "!m.~(m=0) ==> (m-1=0) ==> (m=1)", 54 INDUCT_TAC 55 THEN REWRITE_TAC 56 [SYM 57 (SUBS 58 [SPECL["0";"(SUC m)-1"](INST_TYPE[":num",":*"]EQ_SYM_EQ)] 59 (MP 60 (SPECL 61 ["0";"1";"SUC m"]ADD_EQ_SUB)(SPEC "m:num" LESS_EQ_SUC_1))); 62 ADD_CLAUSES] 63 THEN REPEAT STRIP_TAC 64 THEN ASM_REWRITE_TAC[]);; 65 66let SUB_LEMMA2 = 67 prove_thm 68 (`SUB_LEMMA2`, 69 "!m.(m=0) ==> ~(m-1=0) ==> F", 70 GEN_TAC 71 THEN DISCH_TAC 72 THEN ASM_REWRITE_TAC[SUB_0]);; 73 74let MULT_NOT_0_LESS = 75 prove_thm 76 (`MULT_NOT_0_LESS`, 77 "!m n. ~(m = 0) ==> n <= (m * n)", 78 INDUCT_TAC 79 THEN GEN_TAC 80 THEN REWRITE_TAC 81 [MULT_CLAUSES;SUBS[SPEC_ALL ADD_SYM](SPEC_ALL LESS_EQ_ADD)]);; 82 83let MULT_ADD_LEMMA1 = 84 prove_thm 85 (`MULT_ADD_LEMMA1`, 86 "!m. ~(m=0) ==> !n p. (((m-1)*n)+(n+p) = (m*n)+p)", 87 REPEAT STRIP_TAC 88 THEN REWRITE_TAC[ADD_ASSOC;RIGHT_SUB_DISTRIB;MULT_CLAUSES] 89 THEN IMP_RES_TAC MULT_NOT_0_LESS 90 THEN IMP_RES_TAC SUB_ADD 91 THEN ASM_REWRITE_TAC[]);; 92 93let MULT_FUN_THM = 94 prove_thm 95 (`MULT_FUN_THM`, 96 "!n i1 i2 m t. 97 MULT_FUN((i1,i2),m,n,t) = 98 (t => 99 (m,n,t) | 100 (((n-1)=0)\/(i2=0)) => 101 (((i1=0)=>m|i2+m),n-1,T) | 102 (((i1=0)=>m|((n-1)*i2)+m),1,T))", 103 INDUCT_TAC 104 THEN REPEAT GEN_TAC 105 THEN ASM_CASES_TAC "t:bool" 106 THEN ASM_REWRITE_TAC[MULT_FUN_T;MULT_FUN_F;SUC_SUB1;SUB_0] 107 THEN ASM_CASES_TAC "i1=0" 108 THEN ASM_CASES_TAC "i2=0" 109 THEN ASM_CASES_TAC "n=0" 110 THEN ASM_CASES_TAC "(n-1)=0" 111 THEN ASM_REWRITE_TAC[MULT_FUN_T;MULT_FUN_F;SUC_SUB1;SUB_0] 112 THEN IMP_RES_TAC SUB_LEMMA1 113 THEN IMP_RES_TAC SUB_LEMMA2 114 THEN IMP_RES_TAC MULT_ADD_LEMMA1 115 THEN ASM_REWRITE_TAC[MULT_CLAUSES]);; 116 117let MULT_ADD_LEMMA2 = 118 prove_thm 119 (`MULT_ADD_LEMMA2`, 120 "!m. ~(m=0) ==> !n. ((m-1)*n)+n = m*n", 121 REPEAT STRIP_TAC 122 THEN REWRITE_TAC[RIGHT_SUB_DISTRIB;MULT_CLAUSES] 123 THEN IMP_RES_TAC MULT_NOT_0_LESS 124 THEN IMP_RES_TAC SUB_ADD 125 THEN ASM_REWRITE_TAC[]);; 126 127let MULT_FUN_LEMMA = 128 prove_thm 129 (`MULT_FUN_LEMMA`, 130 "!i1 i2. 131 MULT_FUN((i1,i2),((i1=0)=>0|i2),i1,(((i1-1)=0)\/(i2=0))) = 132 (i1*i2, ((((i1-1)=0)\/(i2=0))=>i1|1), T)", 133 REPEAT GEN_TAC 134 THEN ASM_CASES_TAC "i1=0" 135 THEN ASM_CASES_TAC "i2=0" 136 THEN ASM_REWRITE_TAC[MULT_FUN_THM;MULT_CLAUSES;SUB_0] 137 THEN ASM_CASES_TAC "i1-1=0" 138 THEN IMP_RES_TAC SUB_LEMMA1 139 THEN IMP_RES_TAC MULT_ADD_LEMMA2 140 THEN ASM_REWRITE_TAC[MULT_CLAUSES]);; 141