src/HOL/BNF_Greatest_Fixpoint.thy
changeset 61424 c3658c18b7bc
parent 61032 b57df8eecad6
child 61943 7fba644ed827
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -82,13 +82,13 @@
     1.4  lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
     1.5    by blast
     1.6  
     1.7 -lemma in_rel_Collect_split_eq: "in_rel (Collect (case_prod X)) = X"
     1.8 +lemma in_rel_Collect_case_prod_eq: "in_rel (Collect (case_prod X)) = X"
     1.9    unfolding fun_eq_iff by auto
    1.10  
    1.11 -lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
    1.12 +lemma Collect_case_prod_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
    1.13    by auto
    1.14  
    1.15 -lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    1.16 +lemma Collect_case_prod_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    1.17    by force
    1.18  
    1.19  lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"