src/HOL/Lattices_Big.thy
changeset 54745 46e441e61ff5
parent 54744 1e7f2d296e19
child 54857 5c05f7c5f8ae
     1.1 --- a/src/HOL/Lattices_Big.thy	Sun Dec 15 15:10:14 2013 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Sun Dec 15 15:10:16 2013 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -locale semilattice_order_set = semilattice_order + semilattice_set
     1.8 +locale semilattice_order_set = binary?: semilattice_order + semilattice_set
     1.9  begin
    1.10  
    1.11  lemma bounded_iff:
    1.12 @@ -251,7 +251,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
    1.17 +locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
    1.18  begin
    1.19  
    1.20  lemma bounded_iff:
    1.21 @@ -425,24 +425,23 @@
    1.22  context lattice
    1.23  begin
    1.24  
    1.25 -lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
    1.26 -apply(subgoal_tac "EX a. a:A")
    1.27 -prefer 2 apply blast
    1.28 -apply(erule exE)
    1.29 -apply(rule order_trans)
    1.30 -apply(erule (1) Inf_fin.coboundedI)
    1.31 -apply(erule (1) Sup_fin.coboundedI)
    1.32 -done
    1.33 +lemma Inf_fin_le_Sup_fin [simp]: 
    1.34 +  assumes "finite A" and "A \<noteq> {}"
    1.35 +  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
    1.36 +proof -
    1.37 +  from `A \<noteq> {}` obtain a where "a \<in> A" by blast
    1.38 +  with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
    1.39 +  moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
    1.40 +  ultimately show ?thesis by (rule order_trans)
    1.41 +qed
    1.42  
    1.43  lemma sup_Inf_absorb [simp]:
    1.44 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
    1.45 -apply(subst sup_commute)
    1.46 -apply(simp add: sup_absorb2 Inf_fin.coboundedI)
    1.47 -done
    1.48 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
    1.49 +  by (rule sup_absorb2) (rule Inf_fin.coboundedI)
    1.50  
    1.51  lemma inf_Sup_absorb [simp]:
    1.52 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
    1.53 -by (simp add: inf_absorb1 Sup_fin.coboundedI)
    1.54 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
    1.55 +  by (rule inf_absorb1) (rule Sup_fin.coboundedI)
    1.56  
    1.57  end
    1.58