disambiguation of interpretation prefixes
authorhaftmann
Sun Dec 15 15:10:16 2013 +0100 (2013-12-15)
changeset 5474546e441e61ff5
parent 54744 1e7f2d296e19
child 54749 2fe1fe193f38
disambiguation of interpretation prefixes
NEWS
src/HOL/Groups_Big.thy
src/HOL/Lattices_Big.thy
     1.1 --- a/NEWS	Sun Dec 15 15:10:14 2013 +0100
     1.2 +++ b/NEWS	Sun Dec 15 15:10:16 2013 +0100
     1.3 @@ -28,6 +28,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin.
     1.8 +INCOMPATBILITY.
     1.9 +
    1.10  * Code generations are provided for make, fields, extend and truncate
    1.11  operations on records.
    1.12  
     2.1 --- a/src/HOL/Groups_Big.thy	Sun Dec 15 15:10:14 2013 +0100
     2.2 +++ b/src/HOL/Groups_Big.thy	Sun Dec 15 15:10:16 2013 +0100
     2.3 @@ -20,8 +20,8 @@
     2.4  interpretation comp_fun_commute f
     2.5    by default (simp add: fun_eq_iff left_commute)
     2.6  
     2.7 -interpretation comp_fun_commute "f \<circ> g"
     2.8 -  by (rule comp_comp_fun_commute)
     2.9 +interpretation comp?: comp_fun_commute "f \<circ> g"
    2.10 +  by (fact comp_comp_fun_commute)
    2.11  
    2.12  definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    2.13  where
     3.1 --- a/src/HOL/Lattices_Big.thy	Sun Dec 15 15:10:14 2013 +0100
     3.2 +++ b/src/HOL/Lattices_Big.thy	Sun Dec 15 15:10:16 2013 +0100
     3.3 @@ -127,7 +127,7 @@
     3.4  
     3.5  end
     3.6  
     3.7 -locale semilattice_order_set = semilattice_order + semilattice_set
     3.8 +locale semilattice_order_set = binary?: semilattice_order + semilattice_set
     3.9  begin
    3.10  
    3.11  lemma bounded_iff:
    3.12 @@ -251,7 +251,7 @@
    3.13  
    3.14  end
    3.15  
    3.16 -locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
    3.17 +locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
    3.18  begin
    3.19  
    3.20  lemma bounded_iff:
    3.21 @@ -425,24 +425,23 @@
    3.22  context lattice
    3.23  begin
    3.24  
    3.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"
    3.26 -apply(subgoal_tac "EX a. a:A")
    3.27 -prefer 2 apply blast
    3.28 -apply(erule exE)
    3.29 -apply(rule order_trans)
    3.30 -apply(erule (1) Inf_fin.coboundedI)
    3.31 -apply(erule (1) Sup_fin.coboundedI)
    3.32 -done
    3.33 +lemma Inf_fin_le_Sup_fin [simp]: 
    3.34 +  assumes "finite A" and "A \<noteq> {}"
    3.35 +  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
    3.36 +proof -
    3.37 +  from `A \<noteq> {}` obtain a where "a \<in> A" by blast
    3.38 +  with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
    3.39 +  moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
    3.40 +  ultimately show ?thesis by (rule order_trans)
    3.41 +qed
    3.42  
    3.43  lemma sup_Inf_absorb [simp]:
    3.44 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
    3.45 -apply(subst sup_commute)
    3.46 -apply(simp add: sup_absorb2 Inf_fin.coboundedI)
    3.47 -done
    3.48 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
    3.49 +  by (rule sup_absorb2) (rule Inf_fin.coboundedI)
    3.50  
    3.51  lemma inf_Sup_absorb [simp]:
    3.52 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
    3.53 -by (simp add: inf_absorb1 Sup_fin.coboundedI)
    3.54 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
    3.55 +  by (rule inf_absorb1) (rule Sup_fin.coboundedI)
    3.56  
    3.57  end
    3.58