(*Define the notion of solution*)
let is_solution = define `is_solution xs (cs,b) <=>
         LENGTH xs = LENGTH cs /\
         ITLIST2 (\c x s. c * x + s) cs xs (&0) = b`;;
(*Useful tactic supporting double list induction -- written by John Harrison*) let LIST2_INDUCT_TAC =
let list2_INDUCT = 
prove (`!P:(A)list->(B)list->bool. P [] [] /\ (!h1 t1 h2 t2. P t1 t2 ==> P (CONS h1 t1) (CONS h2 t2)) ==> !l1 l2. LENGTH l1 = LENGTH l2 ==> P l1 l2`,
GEN_TAC THEN STRIP_TAC THEN LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN ASM_SIMP_TAC[LENGTH; NOT_SUC; SUC_INJ]) in MATCH_MP_TAC list2_INDUCT THEN CONJ_TAC THENL [ALL_TAC; REPLICATE_TAC 4 GEN_TAC THEN DISCH_TAC];;
(*Prove the most basic theorem of multiplying both sides with the same non-zero integer (homogeneity)*)
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 ) )`,
REPEAT GEN_TAC THEN REWRITE_TAC[is_solution; LENGTH_MAP] THEN REWRITE_TAC[TAUT` (a/\b<=>a/\c) = (a ==> (b<=>c))`] THEN REPEAT DISCH_TAC THEN UNDISCH_TAC `~(a = &0)` THEN SPEC_TAC (`b:real`, `b:real`) THEN SPEC_TAC (`a:real`, `a:real`) THEN UNDISCH_TAC `LENGTH (xs:real list) = LENGTH (cs:real list)` THEN SPEC_TAC (`cs: real list`,`cs: real list`) THEN SPEC_TAC (`xs: real list`,`xs: real list`) THEN LIST2_INDUCT_TAC THENL [ REPEAT GEN_TAC THEN REWRITE_TAC[MAP; ITLIST2] THEN REWRITE_TAC[REAL_FIELD `~(a = &0) ==> (&0 = b <=> &0 = a * b)`]; REWRITE_TAC[MAP; ITLIST2] THEN REWRITE_TAC[ARITH_RULE `(a:real)+b=c <=> b=c-a`] THEN REWRITE_TAC[ARITH_RULE `((a:real)* b) * c = a * (b * c)`] THEN REWRITE_TAC[ARITH_RULE `(a:real) * b - a * c = a * (b - c)`] THEN ASM_SIMP_TAC[] ] );;