--- a/src/HOL/Auth/ZhouGollmann.thy Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy Thu Jul 15 15:32:32 2004 +0200
@@ -198,15 +198,17 @@
text{*Holds also for @{term "A = Spy"}!*}
theorem NRO_authenticity:
- "[|Says A' B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
+ "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
A \<notin> broken; evs \<in> zg |]
==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+apply (drule Gets_imp_Says, assumption)
apply clarify
apply (frule NRO_sender, auto)
-txt{*We are left with the case where @{term "A' = Spy"} and @{term "A' \<noteq> A"},
- i.e. @{term "A \<notin> bad"}, when we can apply @{text NRO_authenticity_good}.*}
- apply (blast dest: NRO_authenticity_good [OF refl])
+txt{*We are left with the case where the sender is @{term Spy} and not
+ equal to @{term A}, because @{term "A \<notin> bad"}.
+ Thus theorem @{text NRO_authenticity_good} applies.*}
+apply (blast dest: NRO_authenticity_good [OF refl])
done
@@ -276,15 +278,17 @@
text{*Holds also for @{term "A = Spy"}!*}
theorem sub_K_authenticity:
- "[|Says A' TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
+ "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
A \<notin> broken; evs \<in> zg |]
==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+apply (drule Gets_imp_Says, assumption)
apply clarify
apply (frule sub_K_sender, auto)
-txt{*We are left with the case where @{term "A' = Spy"} and @{term "A' \<noteq> A"},
- i.e. @{term "A \<notin> bad"}, when we can apply @{text sub_K_authenticity_good}.*}
- apply (blast dest: sub_K_authenticity_good [OF refl])
+txt{*We are left with the case where the sender is @{term Spy} and not
+ equal to @{term A}, because @{term "A \<notin> bad"}.
+ Thus theorem @{text sub_K_authenticity_good} applies.*}
+apply (blast dest: sub_K_authenticity_good [OF refl])
done
@@ -326,7 +330,7 @@
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
txt{*ZG4*}
-apply (clarify dest!: Gets_imp_Says)
+apply clarify
apply (rule sub_K_authenticity, auto)
done
--- a/src/HOL/Finite_Set.thy Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Finite_Set.thy Thu Jul 15 15:32:32 2004 +0200
@@ -798,17 +798,14 @@
end
*}
-text{* As Jeremy Avigad notes: ultimately the analogous
- thing should be done for setprod as well \dots *}
-
+text{* As Jeremy Avigad notes, setprod needs the same treatment \dots *}
lemma setsum_empty [simp]: "setsum f {} = 0"
by (simp add: setsum_def)
lemma setsum_insert [simp]:
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
- by (simp add: setsum_def
- LC.fold_insert [OF LC.intro] add_left_commute)
+ by (simp add: setsum_def LC.fold_insert [OF LC.intro] add_left_commute)
lemma setsum_reindex [rule_format]:
"finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
@@ -938,9 +935,10 @@
"finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
by (induct set: Finites) auto
-lemma setsum_constant_nat [simp]:
+lemma setsum_constant_nat:
"finite A ==> (\<Sum>x: A. y) = (card A) * y"
- -- {* Later generalized to any @{text comm_semiring_1_cancel}. *}
+ -- {* Generalized to any @{text comm_semiring_1_cancel} in
+ @{text IntDef} as @{text setsum_constant}. *}
by (erule finite_induct, auto)
lemma setsum_Un: "finite A ==> finite B ==>
@@ -978,6 +976,41 @@
apply (blast intro: add_mono)
done
+lemma setsum_mult:
+ fixes f :: "'a => ('b::semiring_0_cancel)"
+ assumes fin: "finite A"
+ shows "r * setsum f A = setsum (%n. r * f n) A"
+using fin
+proof (induct)
+ case empty thus ?case by simp
+next
+ case (insert A x)
+ thus ?case by (simp add: right_distrib)
+qed
+
+lemma setsum_abs:
+ fixes f :: "'a => ('b::lordered_ab_group_abs)"
+ assumes fin: "finite A"
+ shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
+using fin
+proof (induct)
+ case empty thus ?case by simp
+next
+ case (insert A x)
+ thus ?case by (auto intro: abs_triangle_ineq order_trans)
+qed
+
+lemma setsum_abs_ge_zero:
+ fixes f :: "'a => ('b::lordered_ab_group_abs)"
+ assumes fin: "finite A"
+ shows "0 \<le> setsum (%i. abs(f i)) A"
+using fin
+proof (induct)
+ case empty thus ?case by simp
+next
+ case (insert A x) thus ?case by (auto intro: order_trans)
+qed
+
subsubsection {* Cardinality of unions and Sigma sets *}
lemma card_UN_disjoint:
@@ -986,12 +1019,10 @@
card (UNION I A) = setsum (%i. card (A i)) I"
apply (subst card_eq_setsum)
apply (subst finite_UN, assumption+)
- apply (subgoal_tac "setsum (%i. card (A i)) I =
- setsum (%i. (setsum (%x. 1) (A i))) I")
- apply (erule ssubst)
- apply (erule setsum_UN_disjoint, assumption+)
- apply (rule setsum_cong)
- apply simp+
+ apply (subgoal_tac
+ "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
+ apply (simp add: setsum_UN_disjoint)
+ apply (simp add: setsum_constant_nat cong: setsum_cong)
done
lemma card_Union_disjoint:
@@ -1023,9 +1054,10 @@
apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
done
-lemma card_cartesian_product: "[| finite A; finite B |] ==>
- card (A <*> B) = card(A) * card(B)"
- by simp
+lemma card_cartesian_product:
+ "[| finite A; finite B |] ==> card (A <*> B) = card(A) * card(B)"
+ by (simp add: setsum_constant_nat)
+
subsection {* Generalized product over a set *}
--- a/src/HOL/Hyperreal/HSeries.thy Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy Thu Jul 15 15:32:32 2004 +0200
@@ -102,17 +102,11 @@
apply (simp add: sumhr hypnat_of_nat_eq)
done
-lemma sumhr_const: "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r"
-apply (cases n)
-apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat hypreal_mult)
-done
-
-lemma sumhr_add_mult_const:
- "sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) =
- sumhr(0,n,%i. f i + -r)"
+lemma sumhr_const:
+ "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
apply (cases n)
apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat
- hypreal_mult hypreal_add hypreal_minus sumr_add [symmetric])
+ hypreal_mult real_of_nat_def)
done
lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
@@ -139,11 +133,12 @@
(such as @{term whn})*}
lemma sumhr_hypreal_of_hypnat_omega:
"sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
-by (simp add: hypnat_omega_def hypnat_zero_def sumhr hypreal_of_hypnat)
+by (simp add: hypnat_omega_def hypnat_zero_def sumhr hypreal_of_hypnat
+ real_of_nat_def)
lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
by (simp add: hypnat_omega_def hypnat_zero_def omega_def hypreal_one_def
- sumhr hypreal_diff real_of_nat_Suc)
+ sumhr hypreal_diff real_of_nat_def)
lemma sumhr_minus_one_realpow_zero [simp]:
"sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
@@ -254,8 +249,6 @@
val sumhr_split_diff = thm "sumhr_split_diff";
val sumhr_hrabs = thm "sumhr_hrabs";
val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq";
-val sumhr_const = thm "sumhr_const";
-val sumhr_add_mult_const = thm "sumhr_add_mult_const";
val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero";
val sumhr_minus = thm "sumhr_minus";
val sumhr_shift_bounds = thm "sumhr_shift_bounds";
--- a/src/HOL/Hyperreal/MacLaurin_lemmas.ML Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin_lemmas.ML Thu Jul 15 15:32:32 2004 +0200
@@ -110,7 +110,7 @@
by (asm_simp_tac (simpset() addsimps
[CLAIM "Suc m = ma + d + 1 ==> m - ma = d"]
delsimps [sumr_Suc]) 2);
-by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])
+by (asm_simp_tac (simpset() addsimps [(simplify (simpset() delsimps [sumr_Suc])
(read_instantiate [("k","1")] sumr_offset4))]
delsimps [sumr_Suc,fact_Suc,realpow_Suc]) 2);
by (rtac lemma_DERIV_subst 2);
--- a/src/HOL/Hyperreal/Series.thy Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy Thu Jul 15 15:32:32 2004 +0200
@@ -9,10 +9,9 @@
theory Series = SEQ + Lim:
-consts sumr :: "[nat,nat,(nat=>real)] => real"
-primrec
- sumr_0: "sumr m 0 f = 0"
- sumr_Suc: "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
+syntax sumr :: "[nat,nat,(nat=>real)] => real"
+translations
+ "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)"
constdefs
sums :: "[nat=>real,real] => bool" (infixr "sums" 80)
@@ -25,83 +24,52 @@
"suminf f == (@s. f sums s)"
-lemma sumr_Suc_zero [simp]: "sumr (Suc n) n f = 0"
-by (induct_tac "n", auto)
-
-lemma sumr_eq_bounds [simp]: "sumr m m f = 0"
-by (induct_tac "m", auto)
+text{*This simprule replaces @{text "sumr 0 n"} by a term involving
+ @{term lessThan}, making other simprules inapplicable.*}
+declare atLeast0LessThan [simp del]
-lemma sumr_Suc_eq [simp]: "sumr m (Suc m) f = f(m)"
-by auto
-
-lemma sumr_add_lbound_zero [simp]: "sumr (m+k) k f = 0"
-by (induct_tac "k", auto)
+lemma sumr_Suc [simp]:
+ "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
+by (simp add: atLeastLessThanSuc)
lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
-apply (induct_tac "n")
-apply (simp_all add: add_ac)
-done
+by (simp add: setsum_addf)
-lemma sumr_mult: "r * sumr m n f = sumr m n (%n. r * f n)"
-apply (induct_tac "n")
-apply (simp_all add: right_distrib)
-done
+lemma sumr_mult: "r * sumr m n (f::nat=>real) = sumr m n (%n. r * f n)"
+by (simp add: setsum_mult)
lemma sumr_split_add [rule_format]:
- "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f"
+ "n < p --> sumr 0 n f + sumr n p f = sumr 0 p (f::nat=>real)"
apply (induct_tac "p", auto)
apply (rename_tac k)
apply (subgoal_tac "n=k", auto)
done
-lemma sumr_split_add_minus: "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p f"
+lemma sumr_split_add_minus:
+ "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p (f::nat=>real)"
apply (drule_tac f1 = f in sumr_split_add [symmetric])
apply (simp add: add_ac)
done
-lemma sumr_split_add2 [rule_format]:
- "0 < n --> n < p --> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"
-apply (induct_tac "p", auto)
-apply (rename_tac k)
-apply (subgoal_tac "n=k", auto)
-done
-
-lemma sumr_split_add3:
- "[| 0<n; n \<le> p |] ==> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"
-apply (drule le_imp_less_or_eq, auto)
-apply (blast intro: sumr_split_add2)
-done
+lemma sumr_rabs: "abs(sumr m n (f::nat=>real)) \<le> sumr m n (%i. abs(f i))"
+by (simp add: setsum_abs)
-lemma sumr_rabs: "abs(sumr m n f) \<le> sumr m n (%i. abs(f i))"
-apply (induct_tac "n")
-apply (auto intro: abs_triangle_ineq [THEN order_trans] add_right_mono)
-done
-
-lemma sumr_fun_eq [rule_format (no_asm)]:
- "(\<forall>r. m \<le> r & r < n --> f r = g r) --> sumr m n f = sumr m n g"
-by (induct_tac "n", auto)
+lemma sumr_rabs_ge_zero [iff]: "0 \<le> sumr m n (%n. abs (f n))"
+by (simp add: setsum_abs_ge_zero)
-lemma sumr_const [simp]: "sumr 0 n (%i. r) = real n * r"
-apply (induct_tac "n")
-apply (simp_all add: left_distrib real_of_nat_zero real_of_nat_Suc)
-done
-
-lemma sumr_add_mult_const:
- "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"
-by (simp only: sumr_add [symmetric] minus_mult_right, simp)
+text{*Just a congruence rule*}
+lemma sumr_fun_eq:
+ "(\<forall>r. m \<le> r & r < n --> f r = g r) ==> sumr m n f = sumr m n g"
+by (auto intro: setsum_cong)
lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
-by (simp add: real_diff_def sumr_add_mult_const)
+by (simp add: diff_minus setsum_addf real_of_nat_def)
-lemma sumr_less_bounds_zero [rule_format, simp]: "n < m --> sumr m n f = 0"
-apply (induct_tac "n")
-apply (auto dest: less_imp_le)
-done
+lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0"
+by (simp add: atLeastLessThan_empty)
lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
-apply (induct_tac "n")
-apply (case_tac [2] "Suc n \<le> m", simp_all)
-done
+by (simp add: Finite_Set.setsum_negf)
lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
by (induct_tac "n", auto)
@@ -109,15 +77,12 @@
lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"
by (induct_tac "n", auto)
-lemma Suc_diff_n: "m < Suc n ==> Suc n - m = Suc (n - m)"
-by (drule less_imp_Suc_add, auto)
-
lemma sumr_interval_const [rule_format (no_asm)]:
"(\<forall>n. m \<le> Suc n --> f n = r) --> m \<le> k --> sumr m k f = (real(k-m) * r)"
apply (induct_tac "k", auto)
apply (drule_tac x = n in spec)
apply (auto dest!: le_imp_less_or_eq)
-apply (simp (no_asm_simp) add: left_distrib Suc_diff_n real_of_nat_Suc)
+apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
done
lemma sumr_interval_const2 [rule_format (no_asm)]:
@@ -126,16 +91,17 @@
apply (induct_tac "k", auto)
apply (drule_tac x = n in spec)
apply (auto dest!: le_imp_less_or_eq)
-apply (simp (no_asm_simp) add: Suc_diff_n left_distrib real_of_nat_Suc)
+apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
done
+
lemma sumr_le [rule_format (no_asm)]:
"(\<forall>n. m \<le> n --> 0 \<le> f n) --> m < k --> sumr 0 m f \<le> sumr 0 k f"
apply (induct_tac "k")
apply (auto simp add: less_Suc_eq_le)
apply (drule_tac [!] x = n in spec, safe)
apply (drule le_imp_less_or_eq, safe)
-apply (drule_tac [2] a = "sumr 0 m f" in add_mono)
+apply (arith)
apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
done
@@ -156,9 +122,6 @@
apply (drule_tac x = n in spec, arith)
done
-lemma sumr_rabs_ge_zero [iff]: "0 \<le> sumr m n (%n. abs (f n))"
-by (induct_tac "n", auto, arith)
-
lemma rabs_sumr_rabs_cancel [simp]:
"abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"
apply (induct_tac "n")
@@ -198,7 +161,7 @@
"(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))
--> (sumr 0 n f \<le> (real n * K))"
apply (induct_tac "n")
-apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
+apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute)
done
lemma sumr_group [simp]:
@@ -523,35 +486,18 @@
ML
{*
-val sumr_0 = thm"sumr_0";
val sumr_Suc = thm"sumr_Suc";
val sums_def = thm"sums_def";
val summable_def = thm"summable_def";
val suminf_def = thm"suminf_def";
-val sumr_Suc_zero = thm "sumr_Suc_zero";
-val sumr_eq_bounds = thm "sumr_eq_bounds";
-val sumr_Suc_eq = thm "sumr_Suc_eq";
-val sumr_add_lbound_zero = thm "sumr_add_lbound_zero";
val sumr_add = thm "sumr_add";
val sumr_mult = thm "sumr_mult";
val sumr_split_add = thm "sumr_split_add";
-val sumr_split_add_minus = thm "sumr_split_add_minus";
-val sumr_split_add2 = thm "sumr_split_add2";
-val sumr_split_add3 = thm "sumr_split_add3";
val sumr_rabs = thm "sumr_rabs";
val sumr_fun_eq = thm "sumr_fun_eq";
-val sumr_const = thm "sumr_const";
-val sumr_add_mult_const = thm "sumr_add_mult_const";
val sumr_diff_mult_const = thm "sumr_diff_mult_const";
-val sumr_less_bounds_zero = thm "sumr_less_bounds_zero";
-val sumr_minus = thm "sumr_minus";
-val sumr_shift_bounds = thm "sumr_shift_bounds";
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
-val Suc_diff_n = thm "Suc_diff_n";
-val sumr_interval_const = thm "sumr_interval_const";
-val sumr_interval_const2 = thm "sumr_interval_const2";
-val sumr_le = thm "sumr_le";
val sumr_le2 = thm "sumr_le2";
val sumr_ge_zero = thm "sumr_ge_zero";
val sumr_ge_zero2 = thm "sumr_ge_zero2";
--- a/src/HOL/Hyperreal/Transcendental.ML Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.ML Thu Jul 15 15:32:32 2004 +0200
@@ -394,6 +394,8 @@
(* Properties of power series *)
(*--------------------------------------------------------------------------*)
+Delsimps [thm"atLeast0LessThan"];
+
Goal "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) = \
\ y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))";
by (auto_tac (claset(),simpset() addsimps [sumr_mult] delsimps [sumr_Suc]));
@@ -406,6 +408,7 @@
Goal "x ^ (Suc n) - y ^ (Suc n) = \
\ (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))";
by (induct_tac "n" 1);
+by (Asm_full_simp_tac 1);
by (auto_tac (claset(),simpset() delsimps [sumr_Suc]));
by (stac sumr_Suc 1);
by (dtac sym 1);
--- a/src/HOL/Integ/IntDef.thy Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy Thu Jul 15 15:32:32 2004 +0200
@@ -869,7 +869,7 @@
lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
by (subst int_eq_of_nat, rule setprod_of_nat)
-lemma setsum_constant: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
+lemma setsum_constant [simp]: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
apply (erule finite_induct)
apply (auto simp add: ring_distrib add_ac)
done
--- a/src/HOL/NumberTheory/Euler.thy Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/NumberTheory/Euler.thy Thu Jul 15 15:32:32 2004 +0200
@@ -138,7 +138,7 @@
also have "... = int(setsum (%x.2) (SetS a p))";
apply (insert prems)
apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
- card_setsum_aux simp del: setsum_constant_nat)
+ card_setsum_aux simp del: setsum_constant)
done
also have "... = 2 * int(card( SetS a p))";
by (auto simp add: prems SetS_finite setsum_const2)
--- a/src/HOL/NumberTheory/Finite2.thy Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy Thu Jul 15 15:32:32 2004 +0200
@@ -76,7 +76,8 @@
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)";
apply (induct set: Finites)
-by (auto simp add: zadd_zmult_distrib2)
+ apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
+ done
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
int(c) * int(card X)";
--- a/src/HOL/SetInterval.thy Thu Jul 15 13:24:45 2004 +0200
+++ b/src/HOL/SetInterval.thy Thu Jul 15 15:32:32 2004 +0200
@@ -192,6 +192,8 @@
subsection {* Intervals of natural numbers *}
+subsubsection {* The Constant @{term lessThan} *}
+
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
by (simp add: lessThan_def)
@@ -204,6 +206,8 @@
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
by blast
+subsubsection {* The Constant @{term greaterThan} *}
+
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
apply (simp add: greaterThan_def)
apply (blast dest: gr0_conv_Suc [THEN iffD1])
@@ -217,6 +221,8 @@
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
by blast
+subsubsection {* The Constant @{term atLeast} *}
+
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
by (unfold atLeast_def UNIV_def, simp)
@@ -232,6 +238,8 @@
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
by blast
+subsubsection {* The Constant @{term atMost} *}
+
lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
by (simp add: atMost_def)
@@ -243,10 +251,37 @@
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
by blast
-lemma atLeast0LessThan [simp]: "{0::nat..<n} = {..<n}"
+subsubsection {* The Constant @{term atLeastLessThan} *}
+
+text{*But not a simprule because some concepts are better left in terms
+ of @{term atLeastLessThan}*}
+lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
by(simp add:lessThan_def atLeastLessThan_def)
-text {* Intervals of nats with @{text Suc} *}
+lemma atLeastLessThan0 [simp]: "{m..<0::nat} = {}"
+by (simp add: atLeastLessThan_def)
+
+lemma atLeastLessThan_self [simp]: "{n::'a::order..<n} = {}"
+by (auto simp add: atLeastLessThan_def)
+
+lemma atLeastLessThan_empty: "n \<le> m ==> {m..<n::'a::order} = {}"
+by (auto simp add: atLeastLessThan_def)
+
+subsubsection {* Intervals of nats with @{term Suc} *}
+
+text{*Not a simprule because the RHS is too messy.*}
+lemma atLeastLessThanSuc:
+ "{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})"
+by (auto simp add: atLeastLessThan_def)
+
+lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
+by (auto simp add: atLeastLessThan_def)
+
+lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
+by (induct k, simp_all add: atLeastLessThanSuc)
+
+lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
+by (auto simp add: atLeastLessThan_def)
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
@@ -312,7 +347,7 @@
apply arith
done
-lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
+lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"