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