# HG changeset patch # User nipkow # Date 1108723722 -3600 # Node ID a0cf3a19ee369fbe95c0473e10c7cc160b0c12a6 # Parent fad04f5f822f6206e3d3ba90616b6faf226a3897 tuning diff -r fad04f5f822f -r a0cf3a19ee36 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Feb 16 19:00:49 2005 +0100 +++ b/src/HOL/Finite_Set.thy Fri Feb 18 11:48:42 2005 +0100 @@ -673,6 +673,17 @@ cong add: conj_cong simp add: fold_def [symmetric] fold_equality) done +lemma (in ACf) fold_rec: +assumes fin: "finite A" and a: "a:A" +shows "fold f g z A = f (g a) (fold f g z (A - {a}))" +proof- + have A: "A = insert a (A - {a})" using a by blast + hence "fold f g z A = fold f g z (insert a (A - {a}))" by simp + also have "\ = f (g a) (fold f g z (A - {a}))" + by(rule fold_insert) (simp add:fin)+ + finally show ?thesis . +qed + text{* A simplified version for idempotent functions: *} @@ -1064,29 +1075,48 @@ finally show ?thesis . qed -lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A = - - setsum f A" - by (induct set: Finites, auto) +lemma setsum_negf: + "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A" +proof (cases "finite A") + case True thus ?thesis by (induct set: Finites, auto) +next + case False thus ?thesis by (simp add: setsum_def) +qed -lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A = +lemma setsum_subtractf: + "setsum (%x. ((f x)::'a::ab_group_add) - g x) A = setsum f A - setsum g A" - by (simp add: diff_minus setsum_addf setsum_negf) +proof (cases "finite A") + case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf) +next + case False thus ?thesis by (simp add: setsum_def) +qed -lemma setsum_nonneg: "[| finite A; - \x \ A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \ f x |] ==> - 0 \ setsum f A"; +lemma setsum_nonneg: +assumes nn: "\x\A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \ f x" +shows "0 \ setsum f A" +proof (cases "finite A") + case True thus ?thesis using nn apply (induct set: Finites, auto) apply (subgoal_tac "0 + 0 \ f x + setsum f F", simp) apply (blast intro: add_mono) done +next + case False thus ?thesis by (simp add: setsum_def) +qed -lemma setsum_nonpos: "[| finite A; - \x \ A. f x \ (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==> - setsum f A \ 0"; +lemma setsum_nonpos: +assumes np: "\x\A. f x \ (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})" +shows "setsum f A \ 0" +proof (cases "finite A") + case True thus ?thesis using np apply (induct set: Finites, auto) apply (subgoal_tac "f x + setsum f F \ 0 + 0", simp) apply (blast intro: add_mono) done +next + case False thus ?thesis by (simp add: setsum_def) +qed lemma setsum_mult: fixes f :: "'a => ('b::semiring_0_cancel)" @@ -1103,27 +1133,35 @@ case False thus ?thesis by (simp add: setsum_def) qed -lemma setsum_abs: +lemma setsum_abs[iff]: fixes f :: "'a => ('b::lordered_ab_group_abs)" - assumes fin: "finite A" shows "abs (setsum f A) \ setsum (%i. abs(f i)) A" -using fin -proof (induct) - case empty thus ?case by simp +proof (cases "finite A") + case True + thus ?thesis + proof (induct) + case empty thus ?case by simp + next + case (insert x A) + thus ?case by (auto intro: abs_triangle_ineq order_trans) + qed next - case (insert x A) - thus ?case by (auto intro: abs_triangle_ineq order_trans) + case False thus ?thesis by (simp add: setsum_def) qed -lemma setsum_abs_ge_zero: +lemma setsum_abs_ge_zero[iff]: fixes f :: "'a => ('b::lordered_ab_group_abs)" - assumes fin: "finite A" shows "0 \ setsum (%i. abs(f i)) A" -using fin -proof (induct) - case empty thus ?case by simp +proof (cases "finite A") + case True + thus ?thesis + proof (induct) + case empty thus ?case by simp + next + case (insert x A) thus ?case by (auto intro: order_trans) + qed next - case (insert x A) thus ?case by (auto intro: order_trans) + case False thus ?thesis by (simp add: setsum_def) qed diff -r fad04f5f822f -r a0cf3a19ee36 src/HOL/Set.thy --- a/src/HOL/Set.thy Wed Feb 16 19:00:49 2005 +0100 +++ b/src/HOL/Set.thy Fri Feb 18 11:48:42 2005 +0100 @@ -56,7 +56,7 @@ "@Finset" :: "args => 'a set" ("{(_)}") "@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") "@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})") - + "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})") "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" 10) "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10) "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10) @@ -75,6 +75,7 @@ "{x, xs}" == "insert x {xs}" "{x}" == "insert x {}" "{x. P}" == "Collect (%x. P)" + "{x:A. P}" => "{x. x:A & P}" "UN x y. B" == "UN x. UN y. B" "UN x. B" == "UNION UNIV (%x. B)" "UN x. B" == "UN x:UNIV. B" @@ -123,6 +124,7 @@ "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10) syntax (xsymbols) + "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \/ _./ _})") "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" 10) "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" 10) "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" 10) @@ -282,8 +284,15 @@ let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs] in Syntax.const "@SetCompr" $ e $ idts $ Q end; in if check (P, 0) then tr' P - else let val (x,t) = atomic_abs_tr' abs - in Syntax.const "@Coll" $ x $ t end + else let val (x as _ $ Free(xN,_), t) = atomic_abs_tr' abs + val M = Syntax.const "@Coll" $ x $ t + in case t of + Const("op &",_) + $ (Const("op :",_) $ (Const("_bound",_) $ Free(yN,_)) $ A) + $ P => + if xN=yN then Syntax.const "@Collect" $ x $ A $ P else M + | _ => M + end end; in [("Collect", setcompr_tr')] end; *}