formal_lp/more_arith/lin_f.hl

   1 module Linear_function = struct
   2
   3 (********************)
   4 (* Main definitions *)
   5 (********************)
   6
   7 (* A linear function *)
   8 let lin_f = new_definition `lin_f terms =
   9   ITLIST (\tm x. (FST tm) * (SND tm) + x) terms (&0)`;;
  10
  11 (* Example:  let x = `lin_f [&1, x:real; &2, y:real]`;; *)
  12
  13
  14 (**********************)
  15 (* Theorems for lin_f *)
  16 (**********************)
  17
  18 (* Basic properties of lin_f *)
  19 let LIN_F_CONS = prove(`!h t. lin_f (CONS h t) = (FST h * SND h) + lin_f t`,
  20    REWRITE_TAC[lin_f; ITLIST]);;
  21
  22
  23 let LIN_F_EMPTY = prove(`lin_f [] = &0`,
  24                         REWRITE_TAC[lin_f; ITLIST]);;
  25
  26
  27 let LIN_F_APPEND = prove(`!t1 t2. lin_f (APPEND t1 t2) = lin_f t1 + lin_f t2`,
  28    LIST_INDUCT_TAC THEN REWRITE_TAC[APPEND] THENL
  29      [
  30        REWRITE_TAC[LIN_F_EMPTY; REAL_ADD_LID];
  31        ALL_TAC
  32      ] THEN
  33
  34      GEN_TAC THEN
  35      ASM_REWRITE_TAC[LIN_F_CONS; REAL_ADD_ASSOC]);;
  36
  37
  38 (* Sum of two lin_f *)
  39
  40 let LIN_F_SUM_HD = prove(`!v c1 t1 c2 t2 c. c1 + c2 = c ==>
  41     lin_f (CONS (c1,v) t1) + lin_f (CONS (c2,v) t2) = lin_f [c,v] + (lin_f t1 + lin_f t2)`,
  42    REPEAT GEN_TAC THEN REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN
  43      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN REAL_ARITH_TAC);;
  44
  45 let LIN_F_SUM_HD_ZERO = prove(`!v c1 t1 c2 t2. c1 + c2 = &0 ==>
  46     lin_f (CONS (c1,v) t1) + lin_f (CONS (c2,v) t2) = lin_f t1 + lin_f t2`,
  47    REPEAT GEN_TAC THEN DISCH_THEN (MP_TAC o MATCH_MP LIN_F_SUM_HD) THEN
  48      DISCH_THEN (fun th -> REWRITE_TAC[th; LIN_F_CONS; LIN_F_EMPTY]) THEN
  49      REAL_ARITH_TAC);;
  50
  51 let LIN_F_SUM_EMPTY1 = prove(`!x. lin_f [] + lin_f x = lin_f x`,
  52                              REWRITE_TAC[LIN_F_EMPTY; REAL_ADD_LID]);;
  53
  54 let LIN_F_SUM_EMPTY2 = prove(`!x. lin_f x + lin_f [] = lin_f x`,
  55                              REWRITE_TAC[LIN_F_EMPTY; REAL_ADD_RID]);;
  56
  57 let LIN_F_SUM_MOVE1 = prove(`!h t x. lin_f (CONS h t) + lin_f x = lin_f [h] + (lin_f t + lin_f x)`,
  58    REPEAT GEN_TAC THEN REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  59
  60 let LIN_F_SUM_MOVE2 = prove(`!h t x. lin_f x + lin_f (CONS h t) = lin_f [h] + (lin_f x + lin_f t)`,
  61    REPEAT GEN_TAC THEN REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  62
  63
  64 let LIN_F_ADD_SINGLE = prove(`!h t. lin_f [h] + lin_f t = lin_f (CONS h t)`,
  65    REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  66
  67
  68 let LIN_F_ADD_SING_RCANCEL = prove(`!c v t. c * v + lin_f (CONS (--c, v) t)
  69                                        = lin_f t`,
  70    REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  71
  72 let LIN_F_ADD_SING_LCANCEL = prove(`!c v t. --c * v + lin_f (CONS (c, v) t)
  73                                          = lin_f t`,
  74    REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  75
  76
  77 (* Multiplication of lin_f *)
  78
  79 let LIN_F_MUL = prove(`!v t. v * lin_f t = lin_f (MAP (\tm. v * FST tm, SND tm) t)`,
  80    REWRITE_TAC[lin_f] THEN GEN_TAC THEN LIST_INDUCT_TAC THENL
  81      [
  82        REWRITE_TAC[ITLIST; MAP; REAL_MUL_RZERO];
  83        ALL_TAC
  84      ] THEN
  85      REWRITE_TAC[ITLIST; MAP] THEN
  86      ASM_REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_MUL_ASSOC]);;
  87
  88
  89 let LIN_F_MUL_HD = prove(`!x c v t c1. x * c = c1 ==>
  90     x * lin_f (CONS (c,v) t) = lin_f [c1, v] + x * lin_f t`,
  91    REWRITE_TAC[LIN_F_CONS; LIN_F_EMPTY] THEN
  92      REPEAT STRIP_TAC THEN
  93      ASM_REWRITE_TAC[REAL_ARITH `x * (c * v + a) = (x * c) * v + x * a:real`] THEN
  94      REAL_ARITH_TAC);;
  95
  96
  97 let LIN_F_MUL_EMPTY = prove(`!x. x * lin_f [] = lin_f []`,
  98    REWRITE_TAC[LIN_F_EMPTY] THEN REAL_ARITH_TAC);;
  99
 100
 101 (* Theorems for converting sums into lin_f *)
 102 let TO_LIN_F0 = prove(`!x. x = x + lin_f []`, REWRITE_TAC[LIN_F_EMPTY; REAL_ADD_RID]);;
 103
 104 let TO_LIN_F1 = prove(`!a x. a * x = lin_f [a, x]`,
 105    REWRITE_TAC[lin_f; ITLIST; REAL_ADD_RID]);;
 106
 107 let TO_LIN_F = prove(`!c v x t. (c * v + x) + lin_f t = x + lin_f (CONS (c, v) t) /\
 108     c * v + lin_f t = lin_f (CONS (c, v) t)`,
 109    REWRITE_TAC[LIN_F_CONS] THEN REAL_ARITH_TAC);;
 110
 111
 112 end;;