equal
deleted
inserted
replaced
829 (number_of n <= natfloor x) = (number_of n <= x)" |
829 (number_of n <= natfloor x) = (number_of n <= x)" |
830 apply (subst le_natfloor_eq, assumption) |
830 apply (subst le_natfloor_eq, assumption) |
831 apply simp |
831 apply simp |
832 done |
832 done |
833 |
833 |
834 lemma le_natfloor_one_eq [simp]: "(1 <= natfloor x) = (1 <= x)" |
834 lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" |
835 apply (case_tac "0 <= x") |
835 apply (case_tac "0 <= x") |
836 apply (subst le_natfloor_eq, assumption, simp) |
836 apply (subst le_natfloor_eq, assumption, simp) |
837 apply (rule iffI) |
837 apply (rule iffI) |
838 apply (subgoal_tac "natfloor x <= natfloor 0") |
838 apply (subgoal_tac "natfloor x <= natfloor 0") |
839 apply simp |
839 apply simp |
969 apply (subst real_of_nat_le_iff) |
969 apply (subst real_of_nat_le_iff) |
970 apply assumption |
970 apply assumption |
971 apply (erule natceiling_le) |
971 apply (erule natceiling_le) |
972 done |
972 done |
973 |
973 |
974 lemma natceiling_le_eq2 [simp]: "~ neg((number_of n)::int) ==> 0 <= x ==> |
974 lemma natceiling_le_eq_number_of [simp]: |
975 (natceiling x <= number_of n) = (x <= number_of n)" |
975 "~ neg((number_of n)::int) ==> 0 <= x ==> |
|
976 (natceiling x <= number_of n) = (x <= number_of n)" |
976 apply (subst natceiling_le_eq, assumption) |
977 apply (subst natceiling_le_eq, assumption) |
977 apply simp |
978 apply simp |
978 done |
979 done |
979 |
980 |
980 lemma natceiling_one_le_eq: "(natceiling x <= 1) = (x <= 1)" |
981 lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" |
981 apply (case_tac "0 <= x") |
982 apply (case_tac "0 <= x") |
982 apply (subst natceiling_le_eq) |
983 apply (subst natceiling_le_eq) |
983 apply assumption |
984 apply assumption |
984 apply simp |
985 apply simp |
985 apply (subst natceiling_neg) |
986 apply (subst natceiling_neg) |
1015 apply (erule ssubst) |
1016 apply (erule ssubst) |
1016 apply (erule ceiling_mono2) |
1017 apply (erule ceiling_mono2) |
1017 apply simp_all |
1018 apply simp_all |
1018 done |
1019 done |
1019 |
1020 |
1020 lemma natceiling_add2 [simp]: "~ neg ((number_of n)::int) ==> 0 <= x ==> |
1021 lemma natceiling_add_number_of [simp]: |
1021 natceiling (x + number_of n) = natceiling x + number_of n" |
1022 "~ neg ((number_of n)::int) ==> 0 <= x ==> |
|
1023 natceiling (x + number_of n) = natceiling x + number_of n" |
1022 apply (subst natceiling_add [THEN sym]) |
1024 apply (subst natceiling_add [THEN sym]) |
1023 apply simp_all |
1025 apply simp_all |
1024 done |
1026 done |
1025 |
1027 |
1026 lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1" |
1028 lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1" |