equal
deleted
inserted
replaced
344 apply (subgoal_tac "card {l..<u} = card {..<u-l}") |
344 apply (subgoal_tac "card {l..<u} = card {..<u-l}") |
345 apply (erule ssubst, rule card_lessThan) |
345 apply (erule ssubst, rule card_lessThan) |
346 apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}") |
346 apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}") |
347 apply (erule subst) |
347 apply (erule subst) |
348 apply (rule card_image) |
348 apply (rule card_image) |
349 apply (rule finite_lessThan) |
|
350 apply (simp add: inj_on_def) |
349 apply (simp add: inj_on_def) |
351 apply (auto simp add: image_def atLeastLessThan_def lessThan_def) |
350 apply (auto simp add: image_def atLeastLessThan_def lessThan_def) |
352 apply arith |
351 apply arith |
353 apply (rule_tac x = "x - l" in exI) |
352 apply (rule_tac x = "x - l" in exI) |
354 apply arith |
353 apply arith |
431 apply (subgoal_tac "card {l..<u} = card {0..<u-l}") |
430 apply (subgoal_tac "card {l..<u} = card {0..<u-l}") |
432 apply (erule ssubst, rule card_atLeastZeroLessThan_int) |
431 apply (erule ssubst, rule card_atLeastZeroLessThan_int) |
433 apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
432 apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
434 apply (erule subst) |
433 apply (erule subst) |
435 apply (rule card_image) |
434 apply (rule card_image) |
436 apply (rule finite_atLeastZeroLessThan_int) |
|
437 apply (simp add: inj_on_def) |
435 apply (simp add: inj_on_def) |
438 apply (rule image_atLeastLessThan_int_shift) |
436 apply (rule image_atLeastLessThan_int_shift) |
439 done |
437 done |
440 |
438 |
441 lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)" |
439 lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)" |