src/HOL/BNF_Constructions_on_Wellorders.thy
changeset 55811 aa1acc25126b
parent 55603 48596c45bf7f
child 56077 d397030fb27e
equal deleted inserted replaced
55810:63d63d854fae 55811:aa1acc25126b
   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