1 (* ========================================================================= *)
2 (* Maximum of two nums and of a list of nums. *)
4 (* Author: Marco Maggesi *)
5 (* University of Florence, Italy *)
6 (* http://www.math.unifi.it/~maggesi/ *)
8 (* (c) Copyright, Marco Maggesi, 2005-2007 *)
9 (* ========================================================================= *)
11 needs "Permutation/morelist.ml";;
13 (* ------------------------------------------------------------------------- *)
14 (* Maximum of two nums. *)
15 (* ------------------------------------------------------------------------- *)
18 (`!m n p. MAX m n < p <=> m < p /\ n < p`,
19 REWRITE_TAC [MAX] THEN ARITH_TAC);;
22 (`!m n p. MAX m n <= p <=> m <= p /\ n <= p`,
23 REWRITE_TAC [MAX] THEN ARITH_TAC);;
26 (`!m n p. p < MAX m n <=> p < m \/ p < n`,
27 REWRITE_TAC [MAX] THEN ARITH_TAC);;
30 (`!m n p. p <= MAX m n <=> p <= m \/ p <= n`,
31 REWRITE_TAC [MAX] THEN ARITH_TAC);;
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]);;
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]);;
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)) /\
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]]);;
59 (`(!n. MAX n 0 = n) /\ (!n. MAX 0 n = n)`,
60 REWRITE_TAC [MAX_SYM] THEN REWRITE_TAC [MAX] THEN ARITH_TAC);;
62 (* ------------------------------------------------------------------------- *)
63 (* Maximum of a list of nums. *)
64 (* ------------------------------------------------------------------------- *)
68 (!h t. MAXL (CONS h t) = MAX h (MAXL t))`;;
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]);;
76 (`!l n. n < MAXL l <=> EX (\m. n < m) l`,
78 ASM_SIMP_TAC [EX; MAXL; NOT_LT; LE_0; LT_MAX]);;
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]);;
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]);;