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