src/HOL/Relation.thy
changeset 55414 eab03e9cee8a
parent 55096 916b2ac758f4
child 56085 3d11892ea537
     1.1 --- a/src/HOL/Relation.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Relation.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4  lemma lfp_induct2: -- {* Version of @{thm [source] lfp_induct} for binary relations *}
     1.5    "(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow>
     1.6      (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
     1.7 -  using lfp_induct_set [of "(a, b)" f "prod_case P"] by auto
     1.8 +  using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto
     1.9  
    1.10  
    1.11  subsubsection {* Conversions between set and predicate relations *}
    1.12 @@ -113,7 +113,7 @@
    1.13  lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
    1.14    by (simp add: fun_eq_iff)
    1.15  
    1.16 -lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
    1.17 +lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (case_prod ` S) Collect)"
    1.18    by (simp add: fun_eq_iff)
    1.19  
    1.20  lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
    1.21 @@ -125,7 +125,7 @@
    1.22  lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
    1.23    by (simp add: fun_eq_iff)
    1.24  
    1.25 -lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
    1.26 +lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (case_prod ` S) Collect)"
    1.27    by (simp add: fun_eq_iff)
    1.28  
    1.29  lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"