1 (*Define the notion of solution*)
2 let is_solution = define `is_solution xs (cs,b) <=>
3 LENGTH xs = LENGTH cs /\
4 ITLIST2 (\c x s. c * x + s) cs xs (&0) = b`;;
6 (*Useful tactic supporting double list induction -- written by John Harrison*)
8 let list2_INDUCT = prove
9 (`!P:(A)list->(B)list->bool.
11 (!h1 t1 h2 t2. P t1 t2 ==> P (CONS h1 t1) (CONS h2 t2))
12 ==> !l1 l2. LENGTH l1 = LENGTH l2 ==> P l1 l2`,
13 GEN_TAC THEN STRIP_TAC THEN
14 LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN
15 ASM_SIMP_TAC[LENGTH; NOT_SUC; SUC_INJ]) in
16 MATCH_MP_TAC list2_INDUCT THEN
17 CONJ_TAC THENL [ALL_TAC; REPLICATE_TAC 4 GEN_TAC THEN DISCH_TAC];;
19 (*Prove the most basic theorem of multiplying both sides with the same non-zero integer (homogeneity)*)
20 let homogeneity_thm = prove(`!a b xs cs. ( ~(a = &0) ) ==> ( is_solution xs (cs,b) <=> is_solution xs ( MAP (\c. a*c) cs, a*b ) )`,
22 REWRITE_TAC[is_solution; LENGTH_MAP] THEN
23 REWRITE_TAC[TAUT` (a/\b<=>a/\c) = (a ==> (b<=>c))`] THEN
25 UNDISCH_TAC `~(a = &0)` THEN
26 SPEC_TAC (`b:real`, `b:real`) THEN
27 SPEC_TAC (`a:real`, `a:real`) THEN
28 UNDISCH_TAC `LENGTH (xs:real list) = LENGTH (cs:real list)` THEN
29 SPEC_TAC (`cs: real list`,`cs: real list`) THEN
30 SPEC_TAC (`xs: real list`,`xs: real list`) THEN
31 LIST2_INDUCT_TAC THENL [
33 REWRITE_TAC[MAP; ITLIST2] THEN
34 REWRITE_TAC[REAL_FIELD `~(a = &0) ==> (&0 = b <=> &0 = a * b)`];
36 REWRITE_TAC[MAP; ITLIST2] THEN
37 REWRITE_TAC[ARITH_RULE `(a:real)+b=c <=> b=c-a`] THEN
38 REWRITE_TAC[ARITH_RULE `((a:real)* b) * c = a * (b * c)`] THEN
39 REWRITE_TAC[ARITH_RULE `(a:real) * b - a * c = a * (b - c)`] THEN