1(* proof of linearization of cosinus *) 2load "holyHammer"; open holyHammer; 3load "transcTheory"; open realTheory transcTheory; 4 5val thm1 = holyhammer ``cos (2 * x) = cos (x + x)``; 6val thm2 = TAC_PROOF (([], 7 ``cos (x + x) = cos x * cos x - sin x * sin x``), hh); 8 9val thm3_l0 = holyhammer ``cos x * cos x + sin x * sin x = 1``; 10val thm3_l1 = holyhammer ``(a + b = 1) ==> (b = 1 - a)``; 11val thm3 = METIS_PROVE [thm3_l0,thm3_l1] 12 ``cos x * cos x - sin x * sin x = 13 cos x * cos x - (1 - cos x * cos x)``; 14 15val thm4_l1 = holyhammer ``a - (1 - a) = a + a - 1``; 16val thm4_l2 = holyhammer ``a - (1 - a) = 2 * a - 1``; 17val thm4 = holyhammer 18 ``cos x * cos x - (1 - cos x * cos x) = 19 2 * (cos x * cos x) - 1``; 20 21val thm5 = holyhammer ``cos (2 * x) = 2 * (cos x * cos x) - 1``; 22val thm6_l1 = holyhammer ``a = b - 1 ==> a + 1 = b``; 23val thm6_l2 = holyhammer ``a = 2 * b ==> b = a / 2``; 24val thm6 = METIS_PROVE [thm5,thm6_l1,thm6_l2] 25 ``cos x * cos x = (cos (2 * x) + 1) / 2``; 26