diff -r 649bf14debe7 -r 3a4348a3d6ff src/HOL/NatDef.ML --- a/src/HOL/NatDef.ML Thu Feb 05 10:38:34 1998 +0100 +++ b/src/HOL/NatDef.ML Thu Feb 05 10:46:31 1998 +0100 @@ -489,6 +489,10 @@ by (Blast_tac 1); qed "not_leE"; +goalw thy [le_def] "(~n<=m) = (m<(n::nat))"; +by (Simp_tac 1); +qed "not_le_iff_less"; + goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n"; by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1); @@ -577,6 +581,32 @@ by (blast_tac (claset() addSDs [le_imp_less_or_eq]) 1); qed "nat_less_le"; +(** max **) + +goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)"; +by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1); +by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); +qed "le_max_iff_disj"; + +goalw thy [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)"; +by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1); +by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); +qed "max_le_iff_conj"; + + +(** min **) + +goalw thy [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)"; +by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1); +by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); +qed "le_min_iff_conj"; + +goalw thy [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)"; +by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1); +by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1); +qed "min_le_iff_disj"; + + (** LEAST -- the least number operator **) goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";