1%  MICROCODED COMPUTER PROOF : HOL                                      %
2%                                                                       %
3%  'arith.ml'                                                           %
4%                                                                       %
5%  Description                                                          % 
6%                                                                       %
7%     This theory provides some simple arithmetic theorems such as      %
8%  "|- 1 + 2 = 3", which are required by the theory 'proof1'.           %
9%                                                                       %
10%  Author:  Jeff Joyce                                                  %
11%  Date:    August 4, 1985                                              %
12
13new_theory `arith`;;
14
15SPEC "2" (GEN "n" (CONJUNCT1 ADD));;
16let plus_0_2 = save_thm (`plus_0_2`,it);;
17
18REFL "1 + 2";;
19SUBS_OCCS [([2],(num_CONV "1"))] it;;
20PURE_REWRITE_RULE [ADD] it;;
21SUBS [SYM(num_CONV "3")] it;;
22let plus_1_2 = save_thm (`plus_1_2`,it);;
23
24REFL "2 + 2";;
25SUBS_OCCS [([3],(num_CONV "2"))] it;;
26SUBS_OCCS [([1],(num_CONV "1"))] it;;
27PURE_REWRITE_RULE [ADD] it;;
28SUBS [SYM(num_CONV "3")] it;;
29SUBS [SYM(num_CONV "4")] it;;
30let plus_2_2 = save_thm (`plus_2_2`,it);;
31
32REFL "3 + 2";;
33SUBS_OCCS [([2],(num_CONV "3"))] it;;
34SUBS_OCCS [([2],(num_CONV "2"))] it;;
35SUBS_OCCS [([1],(num_CONV "1"))] it;;
36PURE_REWRITE_RULE [ADD] it;;
37SUBS [SYM(num_CONV "3")] it;;
38SUBS [SYM(num_CONV "4")] it;;
39SUBS [SYM(num_CONV "5")] it;;
40let plus_3_2 = save_thm (`plus_3_2`,it);;
41
42SPEC "10" (GEN "n" (CONJUNCT1 ADD));;
43let plus_0_10 = save_thm (`plus_0_10`,it);;
44
45REFL "1 + 10";;
46SUBS_OCCS [([2],(num_CONV "1"))] it;;
47PURE_REWRITE_RULE [ADD] it;;
48SUBS [SYM(num_CONV "11")] it;;
49let plus_1_10 = save_thm (`plus_1_10`,it);;
50
51REFL "2 + 10";;
52SUBS_OCCS [([2],(num_CONV "2"))] it;;
53SUBS [num_CONV "1"] it;;
54PURE_REWRITE_RULE [ADD] it;;
55SUBS [SYM(num_CONV "11")] it;;
56SUBS [SYM(num_CONV "12")] it;;
57let plus_2_10 = save_thm (`plus_2_10`,it);;
58
59REFL "3 + 10";;
60SUBS_OCCS [([2],(num_CONV "3"))] it;;
61SUBS [num_CONV "2"] it;;
62SUBS [num_CONV "1"] it;;
63PURE_REWRITE_RULE [ADD] it;;
64SUBS [SYM(num_CONV "11")] it;;
65SUBS [SYM(num_CONV "12")] it;;
66SUBS [SYM(num_CONV "13")] it;;
67let plus_3_10 = save_thm (`plus_3_10`,it);;
68
69REFL "4 + 10";;
70SUBS_OCCS [([2],(num_CONV "4"))] it;;
71SUBS [num_CONV "3"] it;;
72SUBS [num_CONV "2"] it;;
73SUBS [num_CONV "1"] it;;
74PURE_REWRITE_RULE [ADD] it;;
75SUBS [SYM(num_CONV "11")] it;;
76SUBS [SYM(num_CONV "12")] it;;
77SUBS [SYM(num_CONV "13")] it;;
78SUBS [SYM(num_CONV "14")] it;;
79let plus_4_10 = save_thm (`plus_4_10`,it);;
80
81REFL "5 + 10";;
82SUBS_OCCS [([2],(num_CONV "5"))] it;;
83SUBS [num_CONV "4"] it;;
84SUBS [num_CONV "4"] it;;
85SUBS [num_CONV "3"] it;;
86SUBS [num_CONV "2"] it;;
87SUBS [num_CONV "1"] it;;
88PURE_REWRITE_RULE [ADD] it;;
89SUBS [SYM(num_CONV "11")] it;;
90SUBS [SYM(num_CONV "12")] it;;
91SUBS [SYM(num_CONV "13")] it;;
92SUBS [SYM(num_CONV "14")] it;;
93SUBS [SYM(num_CONV "15")] it;;
94let plus_5_10 = save_thm (`plus_5_10`,it);;
95
96REFL "6 + 10";;
97SUBS_OCCS [([2],(num_CONV "6"))] it;;
98SUBS [num_CONV "5"] it;;
99SUBS [num_CONV "4"] it;;
100SUBS [num_CONV "4"] it;;
101SUBS [num_CONV "3"] it;;
102SUBS [num_CONV "2"] it;;
103SUBS [num_CONV "1"] it;;
104PURE_REWRITE_RULE [ADD] it;;
105SUBS [SYM(num_CONV "11")] it;;
106SUBS [SYM(num_CONV "12")] it;;
107SUBS [SYM(num_CONV "13")] it;;
108SUBS [SYM(num_CONV "14")] it;;
109SUBS [SYM(num_CONV "15")] it;;
110SUBS [SYM(num_CONV "16")] it;;
111let plus_6_10 = save_thm (`plus_6_10`,it);;
112
113REFL "7 + 10";;
114SUBS_OCCS [([2],(num_CONV "7"))] it;;
115SUBS [num_CONV "6"] it;;
116SUBS [num_CONV "5"] it;;
117SUBS [num_CONV "4"] it;;
118SUBS [num_CONV "4"] it;;
119SUBS [num_CONV "3"] it;;
120SUBS [num_CONV "2"] it;;
121SUBS [num_CONV "1"] it;;
122PURE_REWRITE_RULE [ADD] it;;
123SUBS [SYM(num_CONV "11")] it;;
124SUBS [SYM(num_CONV "12")] it;;
125SUBS [SYM(num_CONV "13")] it;;
126SUBS [SYM(num_CONV "14")] it;;
127SUBS [SYM(num_CONV "15")] it;;
128SUBS [SYM(num_CONV "16")] it;;
129SUBS [SYM(num_CONV "17")] it;;
130let plus_7_10 = save_thm (`plus_7_10`,it);;
131
132close_theory ();;
133