equal
deleted
inserted
replaced
791 shows "r <o r'" |
791 shows "r <o r'" |
792 proof- |
792 proof- |
793 {assume "r' \<le>o r" |
793 {assume "r' \<le>o r" |
794 then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r" |
794 then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r" |
795 unfolding ordLeq_def using assms embed_inj_on embed_Field by blast |
795 unfolding ordLeq_def using assms embed_inj_on embed_Field by blast |
796 hence False using finite_imageD finite_subset FIN INF by metis |
796 hence False using finite_imageD finite_subset FIN INF by blast |
797 } |
797 } |
798 thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast |
798 thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast |
799 qed |
799 qed |
800 |
800 |
801 lemma finite_well_order_on_ordIso: |
801 lemma finite_well_order_on_ordIso: |
817 "inj_on f A \<and> f ` A \<le> A" |
817 "inj_on f A \<and> f ` A \<le> A" |
818 unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast |
818 unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast |
819 hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast |
819 hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast |
820 thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto |
820 thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto |
821 qed |
821 qed |
822 ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis |
822 ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast |
823 qed |
823 qed |
824 |
824 |
825 subsection{* @{text "<o"} is well-founded *} |
825 subsection{* @{text "<o"} is well-founded *} |
826 |
826 |
827 text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded |
827 text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded |
985 assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}" |
985 assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}" |
986 obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast |
986 obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast |
987 have "A \<noteq> {} \<and> A \<le> Field r" |
987 have "A \<noteq> {} \<and> A \<le> Field r" |
988 using A_def dir_image_Field[of r f] SUB NE by blast |
988 using A_def dir_image_Field[of r f] SUB NE by blast |
989 then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)" |
989 then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)" |
990 using WF unfolding wf_eq_minimal2 by metis |
990 using WF unfolding wf_eq_minimal2 by blast |
991 have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f" |
991 have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f" |
992 proof(clarify) |
992 proof(clarify) |
993 fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f" |
993 fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f" |
994 obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and |
994 obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and |
995 3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r" |
995 3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r" |
1595 lemma Func_is_emp: |
1595 lemma Func_is_emp: |
1596 "Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R") |
1596 "Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R") |
1597 proof |
1597 proof |
1598 assume L: ?L |
1598 assume L: ?L |
1599 moreover {assume "A = {}" hence False using L Func_empty by auto} |
1599 moreover {assume "A = {}" hence False using L Func_empty by auto} |
1600 moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis} |
1600 moreover {assume "B \<noteq> {}" hence False using L Func_non_emp[of B A] by simp } |
1601 ultimately show ?R by blast |
1601 ultimately show ?R by blast |
1602 next |
1602 next |
1603 assume R: ?R |
1603 assume R: ?R |
1604 moreover |
1604 moreover |
1605 {fix f assume "f \<in> Func A B" |
1605 {fix f assume "f \<in> Func A B" |
1622 show ?thesis |
1622 show ?thesis |
1623 proof safe |
1623 proof safe |
1624 fix h assume h: "h \<in> Func B2 B1" |
1624 fix h assume h: "h \<in> Func B2 B1" |
1625 def j1 \<equiv> "inv_into A1 f1" |
1625 def j1 \<equiv> "inv_into A1 f1" |
1626 have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast |
1626 have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast |
1627 then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis |
1627 then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" |
|
1628 by atomize_elim (rule bchoice) |
1628 {fix b2 assume b2: "b2 \<in> B2" |
1629 {fix b2 assume b2: "b2 \<in> B2" |
1629 hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto |
1630 hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto |
1630 moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto |
1631 moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto |
1631 ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast |
1632 ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast |
1632 } note kk = this |
1633 } note kk = this |