avoid misunderstandable names
authorhaftmann
Mon Jul 18 21:34:01 2011 +0200 (2011-07-18)
changeset 4389960ef6abb2f92
parent 43898 935359fd8210
child 43900 7162691e740b
avoid misunderstandable names
NEWS
src/HOL/Complete_Lattice.thy
     1.1 --- a/NEWS	Mon Jul 18 21:15:51 2011 +0200
     1.2 +++ b/NEWS	Mon Jul 18 21:34:01 2011 +0200
     1.3 @@ -71,6 +71,7 @@
     1.4    le_SUPI ~> le_SUP_I
     1.5    le_SUPI2 ~> le_SUP_I2
     1.6    le_INFI ~> le_INF_I
     1.7 +  INF_subset ~> INF_superset_mono
     1.8    INFI_bool_eq ~> INF_bool_eq
     1.9    SUPR_bool_eq ~> SUP_bool_eq
    1.10    INFI_apply ~> INF_apply
     2.1 --- a/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:15:51 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:34:01 2011 +0200
     2.3 @@ -88,6 +88,12 @@
     2.4  lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
     2.5    by (auto intro: Sup_least dest: Sup_upper)
     2.6  
     2.7 +lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
     2.8 +  by (auto intro: Inf_greatest Inf_lower)
     2.9 +
    2.10 +lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
    2.11 +  by (auto intro: Sup_least Sup_upper)
    2.12 +
    2.13  lemma Inf_mono:
    2.14    assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
    2.15    shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
    2.16 @@ -134,10 +140,10 @@
    2.17    ultimately show ?thesis by (rule Sup_upper2)
    2.18  qed
    2.19  
    2.20 -lemma Inf_inter_less_eq: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
    2.21 +lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
    2.22    by (auto intro: Inf_greatest Inf_lower)
    2.23  
    2.24 -lemma Sup_inter_greater_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
    2.25 +lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
    2.26    by (auto intro: Sup_least Sup_upper)
    2.27  
    2.28  lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
    2.29 @@ -177,12 +183,6 @@
    2.30    from dual.Inf_top_conv show ?P and ?Q by simp_all
    2.31  qed
    2.32  
    2.33 -lemma Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
    2.34 -  by (auto intro: Inf_greatest Inf_lower)
    2.35 -
    2.36 -lemma Sup_anti_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
    2.37 -  by (auto intro: Sup_least Sup_upper)
    2.38 -
    2.39  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.40    INF_def: "INFI A f = \<Sqinter> (f ` A)"
    2.41  
    2.42 @@ -285,13 +285,13 @@
    2.43    "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
    2.44    by (force intro!: Sup_mono simp: SUP_def)
    2.45  
    2.46 -lemma INF_subset:
    2.47 -  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
    2.48 -  by (intro INF_mono) auto
    2.49 +lemma INF_superset_mono:
    2.50 +  "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
    2.51 +  by (rule INF_mono) auto
    2.52  
    2.53 -lemma SUP_subset:
    2.54 +lemma SUPO_subset_mono:
    2.55    "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
    2.56 -  by (intro SUP_mono) auto
    2.57 +  by (rule SUP_mono) auto
    2.58  
    2.59  lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
    2.60    by (iprover intro: INF_leI le_INF_I order_trans antisym)
    2.61 @@ -365,13 +365,13 @@
    2.62    "(\<Squnion>b. A b) = A True \<squnion> A False"
    2.63    by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
    2.64  
    2.65 -lemma INF_anti_mono:
    2.66 +lemma INF_mono':
    2.67    "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>B. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
    2.68    -- {* The last inclusion is POSITIVE! *}
    2.69 -  by (blast intro: INF_mono dest: subsetD)
    2.70 +  by (rule INF_mono) auto
    2.71  
    2.72 -lemma SUP_anti_mono:
    2.73 -  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x \<sqsubseteq> f x) \<Longrightarrow> (\<Squnion>x\<in>B. g x) \<sqsubseteq> (\<Squnion>x\<in>B. f x)"
    2.74 +lemma SUP_mono':
    2.75 +  "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>B. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
    2.76    -- {* The last inclusion is POSITIVE! *}
    2.77    by (blast intro: SUP_mono dest: subsetD)
    2.78  
    2.79 @@ -554,7 +554,7 @@
    2.80    by (fact Inf_insert)
    2.81  
    2.82  lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
    2.83 -  by (fact Inf_inter_less_eq)
    2.84 +  by (fact less_eq_Inf_inter)
    2.85  
    2.86  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
    2.87    by (fact Inf_union_distrib)
    2.88 @@ -565,7 +565,7 @@
    2.89    by (fact Inf_top_conv)+
    2.90  
    2.91  lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
    2.92 -  by (fact Inf_anti_mono)
    2.93 +  by (fact Inf_superset_mono)
    2.94  
    2.95  
    2.96  subsection {* Intersections of families *}
    2.97 @@ -682,7 +682,7 @@
    2.98  lemma INT_anti_mono:
    2.99    "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>B. g x)"
   2.100    -- {* The last inclusion is POSITIVE! *}
   2.101 -  by (fact INF_anti_mono)
   2.102 +  by (fact INF_mono')
   2.103  
   2.104  lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
   2.105    by blast
   2.106 @@ -1077,6 +1077,7 @@
   2.107  lemmas (in complete_lattice) le_SUPI = le_SUP_I
   2.108  lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
   2.109  lemmas (in complete_lattice) le_INFI = le_INF_I
   2.110 +lemmas (in complete_lattice) INF_subset = INF_superset_mono 
   2.111  lemmas INFI_apply = INF_apply
   2.112  lemmas SUPR_apply = SUP_apply
   2.113