tuning
authornipkow
Fri Feb 18 11:48:42 2005 +0100 (2005-02-18)
changeset 15535a0cf3a19ee36
parent 15534 fad04f5f822f
child 15536 3ce1cb7a24f0
tuning
src/HOL/Finite_Set.thy
src/HOL/Set.thy
     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.4      cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
     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.40 -  by (simp add: diff_minus setsum_addf setsum_negf)
    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.51 +assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
    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.57    apply (blast intro: add_mono)
    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.67 +assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
    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.73    apply (blast intro: add_mono)
    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  *}