dropped lemmas (Inf|Sup)_(singleton|binary)
authorhaftmann
Mon Aug 08 19:21:11 2011 +0200 (2011-08-08)
changeset 4408281e55342cb86
parent 44063 4588597ba37e
child 44083 9f8790f8e589
dropped lemmas (Inf|Sup)_(singleton|binary)
NEWS
src/HOL/Complete_Lattice.thy
src/HOL/Import/HOLLight/hollight.imp
     1.1 --- a/NEWS	Mon Aug 08 08:55:49 2011 -0700
     1.2 +++ b/NEWS	Mon Aug 08 19:21:11 2011 +0200
     1.3 @@ -68,6 +68,8 @@
     1.4  boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
     1.5  less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
     1.6  Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
     1.7 +Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary and Sup_binary have
     1.8 +been discarded.
     1.9  More consistent and less misunderstandable names:
    1.10    INFI_def ~> INF_def
    1.11    SUPR_def ~> SUP_def
     2.1 --- a/src/HOL/Complete_Lattice.thy	Mon Aug 08 08:55:49 2011 -0700
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Aug 08 19:21:11 2011 +0200
     2.3 @@ -129,13 +129,13 @@
     2.4  lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     2.5    by (auto intro: Inf_greatest dest: Inf_lower)
     2.6  
     2.7 -lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
     2.8 +lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
     2.9    by (auto simp add: INF_def le_Inf_iff)
    2.10  
    2.11  lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    2.12    by (auto intro: Sup_least dest: Sup_upper)
    2.13  
    2.14 -lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
    2.15 +lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
    2.16    by (auto simp add: SUP_def Sup_le_iff)
    2.17  
    2.18  lemma Inf_empty [simp]:
    2.19 @@ -160,13 +160,13 @@
    2.20    "\<Squnion>UNIV = \<top>"
    2.21    by (auto intro!: antisym Sup_upper)
    2.22  
    2.23 -lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    2.24 +lemma Inf_insert (*[simp]*): "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    2.25    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
    2.26  
    2.27  lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
    2.28    by (simp add: INF_def Inf_insert)
    2.29  
    2.30 -lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    2.31 +lemma Sup_insert (*[simp]*): "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    2.32    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
    2.33  
    2.34  lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
    2.35 @@ -178,22 +178,6 @@
    2.36  lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
    2.37    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
    2.38  
    2.39 -lemma Inf_singleton [simp]:
    2.40 -  "\<Sqinter>{a} = a"
    2.41 -  by (auto intro: antisym Inf_lower Inf_greatest)
    2.42 -
    2.43 -lemma Sup_singleton [simp]:
    2.44 -  "\<Squnion>{a} = a"
    2.45 -  by (auto intro: antisym Sup_upper Sup_least)
    2.46 -
    2.47 -lemma Inf_binary:
    2.48 -  "\<Sqinter>{a, b} = a \<sqinter> b"
    2.49 -  by (simp add: Inf_insert)
    2.50 -
    2.51 -lemma Sup_binary:
    2.52 -  "\<Squnion>{a, b} = a \<squnion> b"
    2.53 -  by (simp add: Sup_insert)
    2.54 -
    2.55  lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
    2.56    by (auto intro: Inf_greatest Inf_lower)
    2.57  
    2.58 @@ -444,7 +428,7 @@
    2.59    and prove @{text inf_Sup} and @{text sup_Inf} from that? *}
    2.60    fix a b c
    2.61    from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
    2.62 -  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)
    2.63 +  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
    2.64  qed
    2.65  
    2.66  lemma Inf_sup:
    2.67 @@ -698,7 +682,7 @@
    2.68    by (fact Inf_greatest)
    2.69  
    2.70  lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
    2.71 -  by (fact Inf_binary [symmetric])
    2.72 +  by (simp add: Inf_insert)
    2.73  
    2.74  lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
    2.75    by (fact Inf_empty)
    2.76 @@ -1206,6 +1190,22 @@
    2.77  
    2.78  text {* Legacy names *}
    2.79  
    2.80 +lemma Inf_singleton [simp]:
    2.81 +  "\<Sqinter>{a} = a"
    2.82 +  by (auto intro: antisym Inf_lower Inf_greatest)
    2.83 +
    2.84 +lemma Sup_singleton [simp]:
    2.85 +  "\<Squnion>{a} = a"
    2.86 +  by (auto intro: antisym Sup_upper Sup_least)
    2.87 +
    2.88 +lemma Inf_binary:
    2.89 +  "\<Sqinter>{a, b} = a \<sqinter> b"
    2.90 +  by (simp add: Inf_insert)
    2.91 +
    2.92 +lemma Sup_binary:
    2.93 +  "\<Squnion>{a, b} = a \<squnion> b"
    2.94 +  by (simp add: Sup_insert)
    2.95 +
    2.96  lemmas (in complete_lattice) INFI_def = INF_def
    2.97  lemmas (in complete_lattice) SUPR_def = SUP_def
    2.98  lemmas (in complete_lattice) le_SUPI = le_SUP_I
     3.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Mon Aug 08 08:55:49 2011 -0700
     3.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Mon Aug 08 19:21:11 2011 +0200
     3.3 @@ -591,7 +591,6 @@
     3.4    "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
     3.5    "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
     3.6    "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
     3.7 -  "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
     3.8    "UNIONS_0" > "Complete_Lattice.Union_empty"
     3.9    "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
    3.10    "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
    3.11 @@ -1598,7 +1597,6 @@
    3.12    "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
    3.13    "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
    3.14    "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
    3.15 -  "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
    3.16    "INTERS_0" > "Complete_Lattice.Inter_empty"
    3.17    "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
    3.18    "INSERT_UNION_EQ" > "Set.Un_insert_left"