author nipkow Fri Feb 18 11:48:42 2005 +0100 (2005-02-18) changeset 15535 a0cf3a19ee36 parent 15534 fad04f5f822f child 15536 3ce1cb7a24f0
tuning
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 16 19:00:49 2005 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Fri Feb 18 11:48:42 2005 +0100
1.3 @@ -673,6 +673,17 @@
1.5    done
1.6
1.7 +lemma (in ACf) fold_rec:
1.8 +assumes fin: "finite A" and a: "a:A"
1.9 +shows "fold f g z A = f (g a) (fold f g z (A - {a}))"
1.10 +proof-
1.11 +  have A: "A = insert a (A - {a})" using a by blast
1.12 +  hence "fold f g z A = fold f g z (insert a (A - {a}))" by simp
1.13 +  also have "\<dots> = f (g a) (fold f g z (A - {a}))"
1.14 +    by(rule fold_insert) (simp add:fin)+
1.15 +  finally show ?thesis .
1.16 +qed
1.17 +
1.18
1.19  text{* A simplified version for idempotent functions: *}
1.20
1.21 @@ -1064,29 +1075,48 @@
1.22    finally show ?thesis .
1.23  qed
1.24
1.25 -lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
1.26 -  - setsum f A"
1.27 -  by (induct set: Finites, auto)
1.28 +lemma setsum_negf:
1.29 + "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
1.30 +proof (cases "finite A")
1.31 +  case True thus ?thesis by (induct set: Finites, auto)
1.32 +next
1.33 +  case False thus ?thesis by (simp add: setsum_def)
1.34 +qed
1.35
1.36 -lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
1.37 +lemma setsum_subtractf:
1.38 + "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
1.39    setsum f A - setsum g A"
1.41 +proof (cases "finite A")
1.42 +  case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
1.43 +next
1.44 +  case False thus ?thesis by (simp add: setsum_def)
1.45 +qed
1.46
1.47 -lemma setsum_nonneg: "[| finite A;
1.48 -    \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
1.49 -    0 \<le> setsum f A";
1.50 +lemma setsum_nonneg:
1.52 +shows "0 \<le> setsum f A"
1.53 +proof (cases "finite A")
1.54 +  case True thus ?thesis using nn
1.55    apply (induct set: Finites, auto)
1.56    apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
1.58    done
1.59 +next
1.60 +  case False thus ?thesis by (simp add: setsum_def)
1.61 +qed
1.62
1.63 -lemma setsum_nonpos: "[| finite A;
1.64 -    \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
1.65 -    setsum f A \<le> 0";
1.66 +lemma setsum_nonpos:
1.68 +shows "setsum f A \<le> 0"
1.69 +proof (cases "finite A")
1.70 +  case True thus ?thesis using np
1.71    apply (induct set: Finites, auto)
1.72    apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
1.74    done
1.75 +next
1.76 +  case False thus ?thesis by (simp add: setsum_def)
1.77 +qed
1.78
1.79  lemma setsum_mult:
1.80    fixes f :: "'a => ('b::semiring_0_cancel)"
1.81 @@ -1103,27 +1133,35 @@
1.82    case False thus ?thesis by (simp add: setsum_def)
1.83  qed
1.84
1.85 -lemma setsum_abs:
1.86 +lemma setsum_abs[iff]:
1.87    fixes f :: "'a => ('b::lordered_ab_group_abs)"
1.88 -  assumes fin: "finite A"
1.89    shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
1.90 -using fin
1.91 -proof (induct)
1.92 -  case empty thus ?case by simp
1.93 +proof (cases "finite A")
1.94 +  case True
1.95 +  thus ?thesis
1.96 +  proof (induct)
1.97 +    case empty thus ?case by simp
1.98 +  next
1.99 +    case (insert x A)
1.100 +    thus ?case by (auto intro: abs_triangle_ineq order_trans)
1.101 +  qed
1.102  next
1.103 -  case (insert x A)
1.104 -  thus ?case by (auto intro: abs_triangle_ineq order_trans)
1.105 +  case False thus ?thesis by (simp add: setsum_def)
1.106  qed
1.107
1.108 -lemma setsum_abs_ge_zero:
1.109 +lemma setsum_abs_ge_zero[iff]:
1.110    fixes f :: "'a => ('b::lordered_ab_group_abs)"
1.111 -  assumes fin: "finite A"
1.112    shows "0 \<le> setsum (%i. abs(f i)) A"
1.113 -using fin
1.114 -proof (induct)
1.115 -  case empty thus ?case by simp
1.116 +proof (cases "finite A")
1.117 +  case True
1.118 +  thus ?thesis
1.119 +  proof (induct)
1.120 +    case empty thus ?case by simp
1.121 +  next
1.122 +    case (insert x A) thus ?case by (auto intro: order_trans)
1.123 +  qed
1.124  next
1.125 -  case (insert x A) thus ?case by (auto intro: order_trans)
1.126 +  case False thus ?thesis by (simp add: setsum_def)
1.127  qed
1.128
1.129
```
```     2.1 --- a/src/HOL/Set.thy	Wed Feb 16 19:00:49 2005 +0100
2.2 +++ b/src/HOL/Set.thy	Fri Feb 18 11:48:42 2005 +0100
2.3 @@ -56,7 +56,7 @@
2.4    "@Finset"     :: "args => 'a set"                       ("{(_)}")
2.5    "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
2.6    "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
2.7 -
2.8 +  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
2.9    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" 10)
2.10    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" 10)
2.11    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" 10)
2.12 @@ -75,6 +75,7 @@
2.13    "{x, xs}"     == "insert x {xs}"
2.14    "{x}"         == "insert x {}"
2.15    "{x. P}"      == "Collect (%x. P)"
2.16 +  "{x:A. P}"    => "{x. x:A & P}"
2.17    "UN x y. B"   == "UN x. UN y. B"
2.18    "UN x. B"     == "UNION UNIV (%x. B)"
2.19    "UN x. B"     == "UN x:UNIV. B"
2.20 @@ -123,6 +124,7 @@
2.21    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
2.22
2.23  syntax (xsymbols)
2.24 +  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
2.25    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
2.26    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
2.27    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
2.28 @@ -282,8 +284,15 @@
2.29            let val _ \$ idts \$ (_ \$ (_ \$ _ \$ e) \$ Q) = ex_tr' [abs]
2.30            in Syntax.const "@SetCompr" \$ e \$ idts \$ Q end;
2.31      in if check (P, 0) then tr' P
2.32 -       else let val (x,t) = atomic_abs_tr' abs
2.33 -            in Syntax.const "@Coll" \$ x \$ t end
2.34 +       else let val (x as _ \$ Free(xN,_), t) = atomic_abs_tr' abs
2.35 +                val M = Syntax.const "@Coll" \$ x \$ t
2.36 +            in case t of
2.37 +                 Const("op &",_)
2.38 +                   \$ (Const("op :",_) \$ (Const("_bound",_) \$ Free(yN,_)) \$ A)
2.39 +                   \$ P =>
2.40 +                   if xN=yN then Syntax.const "@Collect" \$ x \$ A \$ P else M
2.41 +               | _ => M
2.42 +            end
2.43      end;
2.44    in [("Collect", setcompr_tr')] end;
2.45  *}
```