Lines Matching refs:MIN
2920 val MIN = new_definition("MIN_DEF", ���MIN m n = if m < n then m else n���);
2930 ���!m n. MIN m n = MIN n m���,
2931 ARW [MIN] THEN FULL_SIMP_TAC bool_ss [NOT_LESS] THEN
2940 ���!m n p. MIN m (MIN n p) = MIN (MIN m n) p���,
2941 SIMP_TAC bool_ss [MIN] THEN
2945 ���!m n. (MIN m n = MAX m n) = (m = n)���,
2946 SIMP_TAC bool_ss [MAX, MIN] THEN
2950 ���!m n. (MIN m n < MAX m n) = ~(m = n)���,
2951 SIMP_TAC bool_ss [MAX, MIN] THEN
2955 ���!m n. MIN m n <= MAX m n���,
2956 SIMP_TAC bool_ss [MAX, MIN] THEN
2960 ���!P m n. P m /\ P n ==> P (MIN m n) /\ P (MAX m n)���,
2961 PROVE_TAC [MIN, MAX]);
2964 ���!n m p. (MIN m n < p = m < p \/ n < p) /\
2965 (p < MIN m n = p < m /\ p < n)���,
2966 SIMP_TAC bool_ss [MIN] THEN
2976 ���!n m p. (MIN m n <= p = m <= p \/ n <= p) /\
2977 (p <= MIN m n = p <= m /\ p <= n)���,
2978 SIMP_TAC bool_ss [MIN] THEN
2988 ���!n. (MIN n 0 = 0) /\ (MIN 0 n = 0)���,
2989 REWRITE_TAC [MIN] THEN
3005 ���(MIN m n = 0) <=> (m = 0) \/ (n = 0)���,
3006 SRW_TAC[][MIN,EQ_IMP_THM] THEN
3010 ���!n. MIN n n = n���,
3011 PROVE_TAC [MIN]);