Update from HH
[hl193./.git] / 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]);;