Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Complete_Lattice.thy
changeset 44838 610efb6bda1f
parent 44815 b1b436f75070
child 44895 de7642fcbe1e
equal deleted inserted replaced
44825:521de6ab277a 44838:610efb6bda1f 
   474   interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
 
   474   interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
 
   475     by (fact dual_complete_linorder)
 
   475     by (fact dual_complete_linorder)
 
   476   from dual.Sup_eq_top_iff show ?thesis .
 
   476   from dual.Sup_eq_top_iff show ?thesis .
 
   477 qed
 
   477 qed
 
   478 
   478 
       
   479 lemma INF_eq_bot_iff:
 
       
   480   "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
 
       
   481   unfolding INF_def Inf_eq_bot_iff by auto
 
       
   482 
       
   483 lemma SUP_eq_top_iff:
 
       
   484   "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
 
       
   485   unfolding SUP_def Sup_eq_top_iff by auto
 
       
   486 
   479 end
 
   487 end
 
   480 
   488 
   481 
   489 
   482 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
   490 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
   483 
   491 
   927   by (fact SUP_insert)
 
   935   by (fact SUP_insert)
 
   928 
   936 
   929 lemma UN_Un[simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
 
   937 lemma UN_Un[simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
 
   930   by (fact SUP_union)
 
   938   by (fact SUP_union)
 
   931 
   939 
   932 lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)" -- "FIXME generalize"
 
   940 lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
 
   933   by blast
 
   941   by blast
 
   934 
   942 
   935 lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
 
   943 lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
 
   936   by (fact SUP_le_iff)
 
   944   by (fact SUP_le_iff)
 
   937 
   945 
  1065   "\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)"
 
  1073   "\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)"
 
  1066   "\<And>A B C. (\<Inter>z\<in>UNION A B. C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
 
  1074   "\<And>A B C. (\<Inter>z\<in>UNION A B. C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
 
  1067   "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
 
  1075   "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
 
  1068   by auto
 
  1076   by auto
 
  1069 
  1077 
  1070 lemma ball_simps [simp,no_atp]:
 
  1078 lemma UN_ball_bex_simps [simp, no_atp]:
 
  1071   "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
 
       
  1072   "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
 
       
  1073   "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))"
 
       
  1074   "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)"
 
       
  1075   "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True"
 
       
  1076   "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
 
       
  1077   "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))"
 
       
  1078   "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
 
  1079   "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
 
  1079   "\<And>A B P. (\<forall>x\<in> UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
 
  1080   "\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
 
  1080   "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)"
 
       
  1081   "\<And>A P f. (\<forall>x\<in>f`A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))"
 
       
  1082   "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)"
 
       
  1083   by auto
 
       
  1084 
       
  1085 lemma bex_simps [simp,no_atp]:
 
       
  1086   "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)"
 
       
  1087   "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"
 
       
  1088   "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"
 
       
  1089   "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
 
       
  1090   "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))"
 
       
  1091   "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
 
  1081   "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
 
  1092   "\<And>A B P. (\<exists>x\<in>UNION A B. P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
 
  1082   "\<And>A B P. (\<exists>x\<in>UNION A B. P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
 
  1093   "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"
 
       
  1094   "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
 
       
  1095   "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
 
       
  1096   by auto
 
  1083   by auto
 
  1097 
       
  1098 lemma (in complete_linorder) INF_eq_bot_iff:
 
       
  1099   fixes f :: "'b \<Rightarrow> 'a"
 
       
  1100   shows "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
 
       
  1101   unfolding INF_def Inf_eq_bot_iff by auto
 
       
  1102 
       
  1103 lemma (in complete_linorder) SUP_eq_top_iff:
 
       
  1104   fixes f :: "'b \<Rightarrow> 'a"
 
       
  1105   shows "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
 
       
  1106   unfolding SUP_def Sup_eq_top_iff by auto
 
       
  1107 
  1084 
  1108 
  1085 
  1109 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
 
  1086 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
 
  1110 
  1087 
  1111 lemma UN_extend_simps:
 
  1088 lemma UN_extend_simps:
wneuper/isa