1.1 --- a/src/HOL/Cardinals/Wellfounded_More_Base.thy Thu Dec 05 17:52:12 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,194 +0,0 @@
1.4 -(* Title: HOL/Cardinals/Wellfounded_More_Base.thy
1.5 - Author: Andrei Popescu, TU Muenchen
1.6 - Copyright 2012
1.7 -
1.8 -More on well-founded relations (base).
1.9 -*)
1.10 -
1.11 -header {* More on Well-Founded Relations (Base) *}
1.12 -
1.13 -theory Wellfounded_More_Base
1.14 -imports Wellfounded Order_Relation_More_Base "~~/src/HOL/Library/Wfrec"
1.15 -begin
1.16 -
1.17 -
1.18 -text {* This section contains some variations of results in the theory
1.19 -@{text "Wellfounded.thy"}:
1.20 -\begin{itemize}
1.21 -\item means for slightly more direct definitions by well-founded recursion;
1.22 -\item variations of well-founded induction;
1.23 -\item means for proving a linear order to be a well-order.
1.24 -\end{itemize} *}
1.25 -
1.26 -
1.27 -subsection {* Well-founded recursion via genuine fixpoints *}
1.28 -
1.29 -
1.30 -(*2*)lemma wfrec_fixpoint:
1.31 -fixes r :: "('a * 'a) set" and
1.32 - H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
1.33 -assumes WF: "wf r" and ADM: "adm_wf r H"
1.34 -shows "wfrec r H = H (wfrec r H)"
1.35 -proof(rule ext)
1.36 - fix x
1.37 - have "wfrec r H x = H (cut (wfrec r H) r x) x"
1.38 - using wfrec[of r H] WF by simp
1.39 - also
1.40 - {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
1.41 - by (auto simp add: cut_apply)
1.42 - hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
1.43 - using ADM adm_wf_def[of r H] by auto
1.44 - }
1.45 - finally show "wfrec r H x = H (wfrec r H) x" .
1.46 -qed
1.47 -
1.48 -
1.49 -
1.50 -subsection {* Characterizations of well-founded-ness *}
1.51 -
1.52 -
1.53 -text {* A transitive relation is well-founded iff it is ``locally" well-founded,
1.54 -i.e., iff its restriction to the lower bounds of of any element is well-founded. *}
1.55 -
1.56 -(*3*)lemma trans_wf_iff:
1.57 -assumes "trans r"
1.58 -shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
1.59 -proof-
1.60 - obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
1.61 - {assume *: "wf r"
1.62 - {fix a
1.63 - have "wf(R a)"
1.64 - using * R_def wf_subset[of r "R a"] by auto
1.65 - }
1.66 - }
1.67 - (* *)
1.68 - moreover
1.69 - {assume *: "\<forall>a. wf(R a)"
1.70 - have "wf r"
1.71 - proof(unfold wf_def, clarify)
1.72 - fix phi a
1.73 - assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
1.74 - obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
1.75 - with * have "wf (R a)" by auto
1.76 - hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
1.77 - unfolding wf_def by blast
1.78 - moreover
1.79 - have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
1.80 - proof(auto simp add: chi_def R_def)
1.81 - fix b
1.82 - assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
1.83 - hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
1.84 - using assms trans_def[of r] by blast
1.85 - thus "phi b" using ** by blast
1.86 - qed
1.87 - ultimately have "\<forall>b. chi b" by (rule mp)
1.88 - with ** chi_def show "phi a" by blast
1.89 - qed
1.90 - }
1.91 - ultimately show ?thesis using R_def by blast
1.92 -qed
1.93 -
1.94 -
1.95 -text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
1.96 -allowing one to assume the set included in the field. *}
1.97 -
1.98 -(*2*)lemma wf_eq_minimal2:
1.99 -"wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
1.100 -proof-
1.101 - let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
1.102 - have "wf r = (\<forall>A. ?phi A)"
1.103 - by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
1.104 - (rule wfI_min, metis)
1.105 - (* *)
1.106 - also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
1.107 - proof
1.108 - assume "\<forall>A. ?phi A"
1.109 - thus "\<forall>B \<le> Field r. ?phi B" by simp
1.110 - next
1.111 - assume *: "\<forall>B \<le> Field r. ?phi B"
1.112 - show "\<forall>A. ?phi A"
1.113 - proof(clarify)
1.114 - fix A::"'a set" assume **: "A \<noteq> {}"
1.115 - obtain B where B_def: "B = A Int (Field r)" by blast
1.116 - show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
1.117 - proof(cases "B = {}")
1.118 - assume Case1: "B = {}"
1.119 - obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
1.120 - using ** Case1 unfolding B_def by blast
1.121 - hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
1.122 - thus ?thesis using 1 by blast
1.123 - next
1.124 - assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
1.125 - obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
1.126 - using Case2 1 * by blast
1.127 - have "\<forall>a' \<in> A. (a',a) \<notin> r"
1.128 - proof(clarify)
1.129 - fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
1.130 - hence "a' \<in> B" unfolding B_def Field_def by blast
1.131 - thus False using 2 ** by blast
1.132 - qed
1.133 - thus ?thesis using 2 unfolding B_def by blast
1.134 - qed
1.135 - qed
1.136 - qed
1.137 - finally show ?thesis by blast
1.138 -qed
1.139 -
1.140 -subsection {* Characterizations of well-founded-ness *}
1.141 -
1.142 -text {* The next lemma and its corollary enable one to prove that
1.143 -a linear order is a well-order in a way which is more standard than
1.144 -via well-founded-ness of the strict version of the relation. *}
1.145 -
1.146 -(*3*)
1.147 -lemma Linear_order_wf_diff_Id:
1.148 -assumes LI: "Linear_order r"
1.149 -shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
1.150 -proof(cases "r \<le> Id")
1.151 - assume Case1: "r \<le> Id"
1.152 - hence temp: "r - Id = {}" by blast
1.153 - hence "wf(r - Id)" by (simp add: temp)
1.154 - moreover
1.155 - {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
1.156 - obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
1.157 - unfolding order_on_defs using Case1 rel.Total_subset_Id by metis
1.158 - hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
1.159 - hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
1.160 - }
1.161 - ultimately show ?thesis by blast
1.162 -next
1.163 - assume Case2: "\<not> r \<le> Id"
1.164 - hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
1.165 - unfolding order_on_defs by blast
1.166 - show ?thesis
1.167 - proof
1.168 - assume *: "wf(r - Id)"
1.169 - show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
1.170 - proof(clarify)
1.171 - fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
1.172 - hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
1.173 - using 1 * unfolding wf_eq_minimal2 by simp
1.174 - moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
1.175 - using rel.Linear_order_in_diff_Id[of r] ** LI by blast
1.176 - ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
1.177 - qed
1.178 - next
1.179 - assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
1.180 - show "wf(r - Id)"
1.181 - proof(unfold wf_eq_minimal2, clarify)
1.182 - fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
1.183 - hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
1.184 - using 1 * by simp
1.185 - moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
1.186 - using rel.Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
1.187 - ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
1.188 - qed
1.189 - qed
1.190 -qed
1.191 -
1.192 -(*3*)corollary Linear_order_Well_order_iff:
1.193 -assumes "Linear_order r"
1.194 -shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
1.195 -using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
1.196 -
1.197 -end