src/HOL/Library/Product_Order.thy
changeset 56166 9a241bc276cd
parent 56154 f0a927235162
child 56212 3253aaf73a01
     1.1 --- a/src/HOL/Library/Product_Order.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -178,7 +178,7 @@
     1.4  instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
     1.5      conditionally_complete_lattice
     1.6    by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
     1.7 -    INF_def SUP_def intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
     1.8 +    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
     1.9  
    1.10  instance prod :: (complete_lattice, complete_lattice) complete_lattice
    1.11    by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
    1.12 @@ -197,46 +197,46 @@
    1.13    unfolding Inf_prod_def by simp
    1.14  
    1.15  lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
    1.16 -  by (simp add: SUP_def fst_Sup image_image)
    1.17 +  using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
    1.18  
    1.19  lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
    1.20 -  by (simp add: SUP_def snd_Sup image_image)
    1.21 +  using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
    1.22  
    1.23  lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
    1.24 -  by (simp add: INF_def fst_Inf image_image)
    1.25 +  using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
    1.26  
    1.27  lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
    1.28 -  by (simp add: INF_def snd_Inf image_image)
    1.29 +  using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
    1.30  
    1.31  lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
    1.32 -  by (simp add: SUP_def Sup_prod_def image_image)
    1.33 +  unfolding SUP_def Sup_prod_def by (simp add: comp_def)
    1.34  
    1.35  lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
    1.36 -  by (simp add: INF_def Inf_prod_def image_image)
    1.37 +  unfolding INF_def Inf_prod_def by (simp add: comp_def)
    1.38  
    1.39  
    1.40  text {* Alternative formulations for set infima and suprema over the product
    1.41  of two complete lattices: *}
    1.42  
    1.43  lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
    1.44 -by (auto simp: Inf_prod_def INF_def)
    1.45 +by (auto simp: Inf_prod_def)
    1.46  
    1.47  lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
    1.48 -by (auto simp: Sup_prod_def SUP_def)
    1.49 +by (auto simp: Sup_prod_def)
    1.50  
    1.51  lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
    1.52 -by (auto simp: INF_def Inf_prod_def image_comp)
    1.53 +  unfolding INF_def Inf_prod_def by simp
    1.54  
    1.55  lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
    1.56 -by (auto simp: SUP_def Sup_prod_def image_comp)
    1.57 +  unfolding SUP_def Sup_prod_def by simp
    1.58  
    1.59  lemma INF_prod_alt_def:
    1.60    "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
    1.61 -by (metis fst_INF snd_INF surjective_pairing)
    1.62 +  by (simp add: INFI_prod_alt_def comp_def)
    1.63  
    1.64  lemma SUP_prod_alt_def:
    1.65    "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
    1.66 -by (metis fst_SUP snd_SUP surjective_pairing)
    1.67 +  by (simp add: SUPR_prod_alt_def comp_def)
    1.68  
    1.69  
    1.70  subsection {* Complete distributive lattices *}