1679 classes. But for the moment we have to live with it. This forces us to setup |
1679 classes. But for the moment we have to live with it. This forces us to setup |
1680 this sublocale dependency simultaneously with the lattice operations on finite |
1680 this sublocale dependency simultaneously with the lattice operations on finite |
1681 sets, to avoid garbage. |
1681 sets, to avoid garbage. |
1682 *} |
1682 *} |
1683 |
1683 |
1684 definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) |
1684 definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
1685 where |
1685 where |
1686 "Inf_fin = semilattice_set.F inf" |
1686 "Inf_fin = semilattice_set.F inf" |
1687 |
1687 |
1688 definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) |
1688 definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) |
1689 where |
1689 where |
1690 "Sup_fin = semilattice_set.F sup" |
1690 "Sup_fin = semilattice_set.F sup" |
1691 |
1691 |
1692 context linorder |
1692 context linorder |
1693 begin |
1693 begin |
1787 *} |
1787 *} |
1788 |
1788 |
1789 context lattice |
1789 context lattice |
1790 begin |
1790 begin |
1791 |
1791 |
1792 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A" |
1792 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" |
1793 apply(subgoal_tac "EX a. a:A") |
1793 apply(subgoal_tac "EX a. a:A") |
1794 prefer 2 apply blast |
1794 prefer 2 apply blast |
1795 apply(erule exE) |
1795 apply(erule exE) |
1796 apply(rule order_trans) |
1796 apply(rule order_trans) |
1797 apply(erule (1) Inf_fin.coboundedI) |
1797 apply(erule (1) Inf_fin.coboundedI) |
1798 apply(erule (1) Sup_fin.coboundedI) |
1798 apply(erule (1) Sup_fin.coboundedI) |
1799 done |
1799 done |
1800 |
1800 |
1801 lemma sup_Inf_absorb [simp]: |
1801 lemma sup_Inf_absorb [simp]: |
1802 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a" |
1802 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a" |
1803 apply(subst sup_commute) |
1803 apply(subst sup_commute) |
1804 apply(simp add: sup_absorb2 Inf_fin.coboundedI) |
1804 apply(simp add: sup_absorb2 Inf_fin.coboundedI) |
1805 done |
1805 done |
1806 |
1806 |
1807 lemma inf_Sup_absorb [simp]: |
1807 lemma inf_Sup_absorb [simp]: |
1808 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a" |
1808 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a" |
1809 by (simp add: inf_absorb1 Sup_fin.coboundedI) |
1809 by (simp add: inf_absorb1 Sup_fin.coboundedI) |
1810 |
1810 |
1811 end |
1811 end |
1812 |
1812 |
1813 context distrib_lattice |
1813 context distrib_lattice |
1814 begin |
1814 begin |
1815 |
1815 |
1816 lemma sup_Inf1_distrib: |
1816 lemma sup_Inf1_distrib: |
1817 assumes "finite A" |
1817 assumes "finite A" |
1818 and "A \<noteq> {}" |
1818 and "A \<noteq> {}" |
1819 shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}" |
1819 shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}" |
1820 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1]) |
1820 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1]) |
1821 (rule arg_cong [where f="Inf_fin"], blast) |
1821 (rule arg_cong [where f="Inf_fin"], blast) |
1822 |
1822 |
1823 lemma sup_Inf2_distrib: |
1823 lemma sup_Inf2_distrib: |
1824 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
1824 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
1825 shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}" |
1825 shows "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B}" |
1826 using A proof (induct rule: finite_ne_induct) |
1826 using A proof (induct rule: finite_ne_induct) |
1827 case singleton then show ?case |
1827 case singleton then show ?case |
1828 by (simp add: sup_Inf1_distrib [OF B]) |
1828 by (simp add: sup_Inf1_distrib [OF B]) |
1829 next |
1829 next |
1830 case (insert x A) |
1830 case (insert x A) |
1835 have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})" |
1835 have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})" |
1836 by blast |
1836 by blast |
1837 thus ?thesis by(simp add: insert(1) B(1)) |
1837 thus ?thesis by(simp add: insert(1) B(1)) |
1838 qed |
1838 qed |
1839 have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
1839 have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
1840 have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)" |
1840 have "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)" |
1841 using insert by simp |
1841 using insert by simp |
1842 also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2) |
1842 also have "\<dots> = inf (sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)) (sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2) |
1843 also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})" |
1843 also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B})" |
1844 using insert by(simp add:sup_Inf1_distrib[OF B]) |
1844 using insert by(simp add:sup_Inf1_distrib[OF B]) |
1845 also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})" |
1845 also have "\<dots> = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})" |
1846 (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M") |
1846 (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M") |
1847 using B insert |
1847 using B insert |
1848 by (simp add: Inf_fin.union [OF finB _ finAB ne]) |
1848 by (simp add: Inf_fin.union [OF finB _ finAB ne]) |
1849 also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}" |
1849 also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}" |
1850 by blast |
1850 by blast |
1851 finally show ?case . |
1851 finally show ?case . |
1852 qed |
1852 qed |
1853 |
1853 |
1854 lemma inf_Sup1_distrib: |
1854 lemma inf_Sup1_distrib: |
1855 assumes "finite A" and "A \<noteq> {}" |
1855 assumes "finite A" and "A \<noteq> {}" |
1856 shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}" |
1856 shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}" |
1857 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1]) |
1857 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1]) |
1858 (rule arg_cong [where f="Sup_fin"], blast) |
1858 (rule arg_cong [where f="Sup_fin"], blast) |
1859 |
1859 |
1860 lemma inf_Sup2_distrib: |
1860 lemma inf_Sup2_distrib: |
1861 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
1861 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
1862 shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}" |
1862 shows "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B}" |
1863 using A proof (induct rule: finite_ne_induct) |
1863 using A proof (induct rule: finite_ne_induct) |
1864 case singleton thus ?case |
1864 case singleton thus ?case |
1865 by(simp add: inf_Sup1_distrib [OF B]) |
1865 by(simp add: inf_Sup1_distrib [OF B]) |
1866 next |
1866 next |
1867 case (insert x A) |
1867 case (insert x A) |
1872 have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})" |
1872 have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})" |
1873 by blast |
1873 by blast |
1874 thus ?thesis by(simp add: insert(1) B(1)) |
1874 thus ?thesis by(simp add: insert(1) B(1)) |
1875 qed |
1875 qed |
1876 have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
1876 have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
1877 have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)" |
1877 have "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)" |
1878 using insert by simp |
1878 using insert by simp |
1879 also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2) |
1879 also have "\<dots> = sup (inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)) (inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2) |
1880 also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})" |
1880 also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B})" |
1881 using insert by(simp add:inf_Sup1_distrib[OF B]) |
1881 using insert by(simp add:inf_Sup1_distrib[OF B]) |
1882 also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})" |
1882 also have "\<dots> = \<Squnion>\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})" |
1883 (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M") |
1883 (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M") |
1884 using B insert |
1884 using B insert |
1885 by (simp add: Sup_fin.union [OF finB _ finAB ne]) |
1885 by (simp add: Sup_fin.union [OF finB _ finAB ne]) |
1886 also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}" |
1886 also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}" |
1887 by blast |
1887 by blast |
1888 finally show ?case . |
1888 finally show ?case . |
1893 context complete_lattice |
1893 context complete_lattice |
1894 begin |
1894 begin |
1895 |
1895 |
1896 lemma Inf_fin_Inf: |
1896 lemma Inf_fin_Inf: |
1897 assumes "finite A" and "A \<noteq> {}" |
1897 assumes "finite A" and "A \<noteq> {}" |
1898 shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A" |
1898 shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A" |
1899 proof - |
1899 proof - |
1900 from assms obtain b B where "A = insert b B" and "finite B" by auto |
1900 from assms obtain b B where "A = insert b B" and "finite B" by auto |
1901 then show ?thesis |
1901 then show ?thesis |
1902 by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b]) |
1902 by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b]) |
1903 qed |
1903 qed |
1904 |
1904 |
1905 lemma Sup_fin_Sup: |
1905 lemma Sup_fin_Sup: |
1906 assumes "finite A" and "A \<noteq> {}" |
1906 assumes "finite A" and "A \<noteq> {}" |
1907 shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A" |
1907 shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A" |
1908 proof - |
1908 proof - |
1909 from assms obtain b B where "A = insert b B" and "finite B" by auto |
1909 from assms obtain b B where "A = insert b B" and "finite B" by auto |
1910 then show ?thesis |
1910 then show ?thesis |
1911 by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b]) |
1911 by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b]) |
1912 qed |
1912 qed |