(* ========================================================================= *)
(*  Maximum of two nums and of a list of nums.                               *)
(*                                                                           *)
(*  Author: Marco Maggesi                                                    *)
(*          University of Florence, Italy                                    *)
(*          http://www.math.unifi.it/~maggesi/                               *)
(*                                                                           *)
(*          (c) Copyright, Marco Maggesi, 2005-2007                          *)
(* ========================================================================= *)

needs "Permutation/morelist.ml";;

(* ------------------------------------------------------------------------- *)
(*  Maximum of two nums.                                                     *)
(* ------------------------------------------------------------------------- *)

let MAX_LT = prove
 (`!m n p. MAX m n < p <=> m < p /\ n < p`,
   REWRITE_TAC [MAX] THEN ARITH_TAC);;

let MAX_LE = prove
 (`!m n p. MAX m n <= p <=> m <= p /\ n <= p`,
   REWRITE_TAC [MAX] THEN ARITH_TAC);;

let LT_MAX = prove
 (`!m n p. p < MAX m n <=> p < m \/ p < n`,
   REWRITE_TAC [MAX] THEN ARITH_TAC);;

let LE_MAX = prove
 (`!m n p. p <= MAX m n <=> p <= m \/ p <= n`,
   REWRITE_TAC [MAX] THEN ARITH_TAC);;

let MAX_SYM = prove
  (`!m n. MAX n m = MAX m n`,
   MATCH_MP_TAC WLOG_LE THEN CONJ_TAC THEN REPEAT GEN_TAC THENL
   [EQ_TAC THEN SIMP_TAC []; SIMP_TAC [MAX] THEN ARITH_TAC]);;

let MAX_ASSOC = prove
  (`!m n p. MAX (MAX m n) p = MAX m (MAX n p)`,
   REPEAT GEN_TAC THEN REWRITE_TAC [MAX] THEN
   ASM_CASES_TAC `m <= n` THEN ASM_REWRITE_TAC [] THEN
   ASM_CASES_TAC `n <= p` THEN ASM_REWRITE_TAC [] THENL
   [SUBGOAL_THEN `m <= p` (fun th -> REWRITE_TAC [th]) THEN
    MATCH_MP_TAC LE_TRANS THEN ASM_MESON_TAC [];
    SUBGOAL_THEN `~(m <= p)` (fun th -> REWRITE_TAC [th]) THEN
    FIRST_X_ASSUM MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC]);;

let MAX_ACI = prove
  (`(!m n. MAX n m = MAX m n) /\
    (!m n p. MAX (MAX m n) p = MAX m (MAX n p)) /\
    (!m n p. MAX m (MAX n p) = MAX n (MAX m p)) /\
    (!m. MAX m m = m) /\
    (!m n. MAX m (MAX m n) = MAX m n)`,
   SUBGOAL_THEN `!n. MAX n n = n` ASSUME_TAC THENL
   [REWRITE_TAC [MAX] THEN ARITH_TAC;
    ASM_MESON_TAC [MAX_SYM; MAX_ASSOC]]);;

let MAX_0 = prove
  (`(!n. MAX n 0 = n) /\ (!n. MAX 0 n = n)`,
   REWRITE_TAC [MAX_SYM] THEN REWRITE_TAC [MAX] THEN ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(*  Maximum of a list of nums.                                               *)
(* ------------------------------------------------------------------------- *)

let MAXL = define
  `MAXL [] = 0 /\
   (!h t. MAXL (CONS h t) = MAX h (MAXL t))`;;

let MAXL_LE = prove
  (`!l n. MAXL l <= n <=> ALL (\m. m <= n) l`,
   LIST_INDUCT_TAC THEN REWRITE_TAC [ALL; MAXL; LE_0] THEN
   ASM_SIMP_TAC [MAX_LE]);;

let LT_MAXL = prove
  (`!l n. n < MAXL l <=> EX (\m. n < m) l`,
   LIST_INDUCT_TAC THEN
   ASM_SIMP_TAC [EX; MAXL; NOT_LT; LE_0; LT_MAX]);;

let LE_MAXL = prove
  (`!n l. MEM n l ==> n <= MAXL l`,
   GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; MAXL] THEN
   STRIP_TAC THEN ASM_SIMP_TAC [LE_REFL; LE_MAX]);;

let MEM_MAXL = prove
  (`!l. ~NULL l ==> MEM (MAXL l) l`,
   REWRITE_TAC [NULL_EQ_NIL] THEN LIST_INDUCT_TAC THEN
   REWRITE_TAC [MEM; MAXL; NOT_CONS_NIL] THEN
   ASM_CASES_TAC `t:num list=[]` THEN ASM_REWRITE_TAC[MAXL; MAX_0] THEN
   ASM_MESON_TAC [MAX]);;