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