Permutation/nummax.ml

   1 (* ========================================================================= *)
   2 (*  Maximum of two nums and of a list of nums.                               *)
   3 (*                                                                           *)
   4 (*  Author: Marco Maggesi                                                    *)
   5 (*          University of Florence, Italy                                    *)
   6 (*          http://www.math.unifi.it/~maggesi/                               *)
   7 (*                                                                           *)
   8 (*          (c) Copyright, Marco Maggesi, 2005-2007                          *)
   9 (* ========================================================================= *)
  10
  11 needs "Permutation/morelist.ml";;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (*  Maximum of two nums.                                                     *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let MAX_LT = prove
  18  (`!m n p. MAX m n < p <=> m < p /\ n < p`,
  19    REWRITE_TAC [MAX] THEN ARITH_TAC);;
  20
  21 let MAX_LE = prove
  22  (`!m n p. MAX m n <= p <=> m <= p /\ n <= p`,
  23    REWRITE_TAC [MAX] THEN ARITH_TAC);;
  24
  25 let LT_MAX = prove
  26  (`!m n p. p < MAX m n <=> p < m \/ p < n`,
  27    REWRITE_TAC [MAX] THEN ARITH_TAC);;
  28
  29 let LE_MAX = prove
  30  (`!m n p. p <= MAX m n <=> p <= m \/ p <= n`,
  31    REWRITE_TAC [MAX] THEN ARITH_TAC);;
  32
  33 let MAX_SYM = prove
  34   (`!m n. MAX n m = MAX m n`,
  35    MATCH_MP_TAC WLOG_LE THEN CONJ_TAC THEN REPEAT GEN_TAC THENL
  36    [EQ_TAC THEN SIMP_TAC []; SIMP_TAC [MAX] THEN ARITH_TAC]);;
  37
  38 let MAX_ASSOC = prove
  39   (`!m n p. MAX (MAX m n) p = MAX m (MAX n p)`,
  40    REPEAT GEN_TAC THEN REWRITE_TAC [MAX] THEN
  41    ASM_CASES_TAC `m <= n` THEN ASM_REWRITE_TAC [] THEN
  42    ASM_CASES_TAC `n <= p` THEN ASM_REWRITE_TAC [] THENL
  43    [SUBGOAL_THEN `m <= p` (fun th -> REWRITE_TAC [th]) THEN
  44     MATCH_MP_TAC LE_TRANS THEN ASM_MESON_TAC [];
  45     SUBGOAL_THEN `~(m <= p)` (fun th -> REWRITE_TAC [th]) THEN
  46     FIRST_X_ASSUM MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC]);;
  47
  48 let MAX_ACI = prove
  49   (`(!m n. MAX n m = MAX m n) /\
  50     (!m n p. MAX (MAX m n) p = MAX m (MAX n p)) /\
  51     (!m n p. MAX m (MAX n p) = MAX n (MAX m p)) /\
  52     (!m. MAX m m = m) /\
  53     (!m n. MAX m (MAX m n) = MAX m n)`,
  54    SUBGOAL_THEN `!n. MAX n n = n` ASSUME_TAC THENL
  55    [REWRITE_TAC [MAX] THEN ARITH_TAC;
  56     ASM_MESON_TAC [MAX_SYM; MAX_ASSOC]]);;
  57
  58 let MAX_0 = prove
  59   (`(!n. MAX n 0 = n) /\ (!n. MAX 0 n = n)`,
  60    REWRITE_TAC [MAX_SYM] THEN REWRITE_TAC [MAX] THEN ARITH_TAC);;
  61
  62 (* ------------------------------------------------------------------------- *)
  63 (*  Maximum of a list of nums.                                               *)
  64 (* ------------------------------------------------------------------------- *)
  65
  66 let MAXL = define
  67   `MAXL [] = 0 /\
  68    (!h t. MAXL (CONS h t) = MAX h (MAXL t))`;;
  69
  70 let MAXL_LE = prove
  71   (`!l n. MAXL l <= n <=> ALL (\m. m <= n) l`,
  72    LIST_INDUCT_TAC THEN REWRITE_TAC [ALL; MAXL; LE_0] THEN
  73    ASM_SIMP_TAC [MAX_LE]);;
  74
  75 let LT_MAXL = prove
  76   (`!l n. n < MAXL l <=> EX (\m. n < m) l`,
  77    LIST_INDUCT_TAC THEN
  78    ASM_SIMP_TAC [EX; MAXL; NOT_LT; LE_0; LT_MAX]);;
  79
  80 let LE_MAXL = prove
  81   (`!n l. MEM n l ==> n <= MAXL l`,
  82    GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; MAXL] THEN
  83    STRIP_TAC THEN ASM_SIMP_TAC [LE_REFL; LE_MAX]);;
  84
  85 let MEM_MAXL = prove
  86   (`!l. ~NULL l ==> MEM (MAXL l) l`,
  87    REWRITE_TAC [NULL_EQ_NIL] THEN LIST_INDUCT_TAC THEN
  88    REWRITE_TAC [MEM; MAXL; NOT_CONS_NIL] THEN
  89    ASM_CASES_TAC `t:num list=[]` THEN ASM_REWRITE_TAC[MAXL; MAX_0] THEN
  90    ASM_MESON_TAC [MAX]);;