1781 qed |
1781 qed |
1782 |
1782 |
1783 |
1783 |
1784 subsection {* Others *} |
1784 subsection {* Others *} |
1785 |
1785 |
1786 (* function space *) |
|
1787 definition Func where |
|
1788 "Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}" |
|
1789 |
|
1790 lemma Func_empty: |
|
1791 "Func {} B = {\<lambda>x. undefined}" |
|
1792 unfolding Func_def by auto |
|
1793 |
|
1794 lemma Func_elim: |
|
1795 assumes "g \<in> Func A B" and "a \<in> A" |
|
1796 shows "\<exists> b. b \<in> B \<and> g a = b" |
|
1797 using assms unfolding Func_def by (cases "g a = undefined") auto |
|
1798 |
|
1799 definition curr where |
|
1800 "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined" |
|
1801 |
|
1802 lemma curr_in: |
|
1803 assumes f: "f \<in> Func (A <*> B) C" |
|
1804 shows "curr A f \<in> Func A (Func B C)" |
|
1805 using assms unfolding curr_def Func_def by auto |
|
1806 |
|
1807 lemma curr_inj: |
|
1808 assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C" |
|
1809 shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2" |
|
1810 proof safe |
|
1811 assume c: "curr A f1 = curr A f2" |
|
1812 show "f1 = f2" |
|
1813 proof (rule ext, clarify) |
|
1814 fix a b show "f1 (a, b) = f2 (a, b)" |
|
1815 proof (cases "(a,b) \<in> A <*> B") |
|
1816 case False |
|
1817 thus ?thesis using assms unfolding Func_def by auto |
|
1818 next |
|
1819 case True hence a: "a \<in> A" and b: "b \<in> B" by auto |
|
1820 thus ?thesis |
|
1821 using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp |
|
1822 qed |
|
1823 qed |
|
1824 qed |
|
1825 |
|
1826 lemma curr_surj: |
|
1827 assumes "g \<in> Func A (Func B C)" |
|
1828 shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g" |
|
1829 proof |
|
1830 let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined" |
|
1831 show "curr A ?f = g" |
|
1832 proof (rule ext) |
|
1833 fix a show "curr A ?f a = g a" |
|
1834 proof (cases "a \<in> A") |
|
1835 case False |
|
1836 hence "g a = undefined" using assms unfolding Func_def by auto |
|
1837 thus ?thesis unfolding curr_def using False by simp |
|
1838 next |
|
1839 case True |
|
1840 obtain g1 where "g1 \<in> Func B C" and "g a = g1" |
|
1841 using assms using Func_elim[OF assms True] by blast |
|
1842 thus ?thesis using True unfolding Func_def curr_def by auto |
|
1843 qed |
|
1844 qed |
|
1845 show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto |
|
1846 qed |
|
1847 |
|
1848 lemma bij_betw_curr: |
|
1849 "bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))" |
|
1850 unfolding bij_betw_def inj_on_def image_def |
|
1851 apply (intro impI conjI ballI) |
|
1852 apply (erule curr_inj[THEN iffD1], assumption+) |
|
1853 apply auto |
|
1854 apply (erule curr_in) |
|
1855 using curr_surj by blast |
|
1856 |
|
1857 lemma card_of_Func_Times: |
1786 lemma card_of_Func_Times: |
1858 "|Func (A <*> B) C| =o |Func A (Func B C)|" |
1787 "|Func (A <*> B) C| =o |Func A (Func B C)|" |
1859 unfolding card_of_ordIso[symmetric] |
1788 unfolding card_of_ordIso[symmetric] |
1860 using bij_betw_curr by blast |
1789 using bij_betw_curr by blast |
1861 |
|
1862 definition Func_map where |
|
1863 "Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined" |
|
1864 |
|
1865 lemma Func_map: |
|
1866 assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2" |
|
1867 shows "Func_map B2 f1 f2 g \<in> Func B2 B1" |
|
1868 using assms unfolding Func_def Func_map_def mem_Collect_eq by auto |
|
1869 |
|
1870 lemma Func_non_emp: |
|
1871 assumes "B \<noteq> {}" |
|
1872 shows "Func A B \<noteq> {}" |
|
1873 proof- |
|
1874 obtain b where b: "b \<in> B" using assms by auto |
|
1875 hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto |
|
1876 thus ?thesis by blast |
|
1877 qed |
|
1878 |
|
1879 lemma Func_is_emp: |
|
1880 "Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R") |
|
1881 proof |
|
1882 assume L: ?L |
|
1883 moreover {assume "A = {}" hence False using L Func_empty by auto} |
|
1884 moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis} |
|
1885 ultimately show ?R by blast |
|
1886 next |
|
1887 assume R: ?R |
|
1888 moreover |
|
1889 {fix f assume "f \<in> Func A B" |
|
1890 moreover obtain a where "a \<in> A" using R by blast |
|
1891 ultimately obtain b where "b \<in> B" unfolding Func_def by blast |
|
1892 with R have False by blast |
|
1893 } |
|
1894 thus ?L by blast |
|
1895 qed |
|
1896 |
|
1897 lemma Func_map_surj: |
|
1898 assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2" |
|
1899 and B2A2: "B2 = {} \<Longrightarrow> A2 = {}" |
|
1900 shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1" |
|
1901 proof(cases "B2 = {}") |
|
1902 case True |
|
1903 thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def) |
|
1904 next |
|
1905 case False note B2 = False |
|
1906 show ?thesis |
|
1907 proof safe |
|
1908 fix h assume h: "h \<in> Func B2 B1" |
|
1909 def j1 \<equiv> "inv_into A1 f1" |
|
1910 have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast |
|
1911 then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis |
|
1912 {fix b2 assume b2: "b2 \<in> B2" |
|
1913 hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto |
|
1914 moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto |
|
1915 ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast |
|
1916 } note kk = this |
|
1917 obtain b22 where b22: "b22 \<in> B2" using B2 by auto |
|
1918 def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22" |
|
1919 have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto |
|
1920 have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2" |
|
1921 using kk unfolding j2_def by auto |
|
1922 def g \<equiv> "Func_map A2 j1 j2 h" |
|
1923 have "Func_map B2 f1 f2 g = h" |
|
1924 proof (rule ext) |
|
1925 fix b2 show "Func_map B2 f1 f2 g b2 = h b2" |
|
1926 proof(cases "b2 \<in> B2") |
|
1927 case True |
|
1928 show ?thesis |
|
1929 proof (cases "h b2 = undefined") |
|
1930 case True |
|
1931 hence b1: "h b2 \<in> f1 ` A1" using h `b2 \<in> B2` unfolding B1 Func_def by auto |
|
1932 show ?thesis using A2 f_inv_into_f[OF b1] |
|
1933 unfolding True g_def Func_map_def j1_def j2[OF `b2 \<in> B2`] by auto |
|
1934 qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def, |
|
1935 auto intro: f_inv_into_f) |
|
1936 qed(insert h, unfold Func_def Func_map_def, auto) |
|
1937 qed |
|
1938 moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h]) |
|
1939 using inv_into_into j2A2 B1 A2 inv_into_into |
|
1940 unfolding j1_def image_def by fast+ |
|
1941 ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1" |
|
1942 unfolding Func_map_def[abs_def] unfolding image_def by auto |
|
1943 qed(insert B1 Func_map[OF _ _ A2(2)], auto) |
|
1944 qed |
|
1945 |
1790 |
1946 lemma card_of_Pow_Func: |
1791 lemma card_of_Pow_Func: |
1947 "|Pow A| =o |Func A (UNIV::bool set)|" |
1792 "|Pow A| =o |Func A (UNIV::bool set)|" |
1948 proof- |
1793 proof- |
1949 def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then True else False) |
1794 def F \<equiv> "\<lambda> A' a. if a \<in> A then (if a \<in> A' then True else False) |