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