1.1 --- a/src/HOL/Predicate.thy	Sat Mar 10 16:13:08 2007 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Sat Mar 10 16:23:28 2007 +0100
     1.3 @@ -286,28 +286,61 @@
     1.4  subsubsection {* Unions of families *}
     1.5  
     1.6  lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)"
     1.7 -  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
     1.8 +  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
     1.9  
    1.10  lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)"
    1.11 -  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
    1.12 +  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
    1.13  
    1.14 -lemma SUP1_iff [simp]: "((SUP x. B x) b) = (EX x. B x b)"
    1.15 -  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast
    1.16 +lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
    1.17 +  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
    1.18 +
    1.19 +lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
    1.20 +  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
    1.21  
    1.22 -lemma SUP2_iff [simp]: "((SUP x. B x) b c) = (EX x. B x b c)"
    1.23 -  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast
    1.24 +lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
    1.25 +  by auto
    1.26  
    1.27 -lemma SUP1_I [intro]: "B a b ==> (SUP x. B x) b"
    1.28 +lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
    1.29 +  by auto
    1.30 +
    1.31 +lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
    1.32 +  by auto
    1.33 +
    1.34 +lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
    1.35    by auto
    1.36  
    1.37 -lemma SUP2_I [intro]: "B a b c ==> (SUP x. B x) b c"
    1.38 +
    1.39 +subsubsection {* Intersections of families *}
    1.40 +
    1.41 +lemma member_INF: "(INF i. member (r i)) = member (INT i. r i)"
    1.42 +  by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast
    1.43 +
    1.44 +lemma member2_INF: "(INF i. member2 (r i)) = member2 (INT i. r i)"
    1.45 +  by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast
    1.46 +
    1.47 +lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
    1.48 +  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
    1.49 +
    1.50 +lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
    1.51 +  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
    1.52 +
    1.53 +lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
    1.54    by auto
    1.55  
    1.56 -lemma SUP1_E [elim!]: "(SUP x. B x) b ==> (!!x. B x b ==> R) ==> R"
    1.57 -  by simp iprover
    1.58 +lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
    1.59 +  by auto
    1.60 +
    1.61 +lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
    1.62 +  by auto
    1.63  
    1.64 -lemma SUP2_E [elim!]: "(SUP x. B x) b c ==> (!!x. B x b c ==> R) ==> R"
    1.65 -  by simp iprover
    1.66 +lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
    1.67 +  by auto
    1.68 +
    1.69 +lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
    1.70 +  by auto
    1.71 +
    1.72 +lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
    1.73 +  by auto
    1.74  
    1.75  
    1.76  subsection {* Composition of two relations *}