folded 'Wellfounded_More_FP' into 'Wellfounded'
authorblanchet
Fri Jan 17 10:02:50 2014 +0100 (2014-01-17)
changeset 55027a74ea6d75571
parent 55026 258fa7b5a621
child 55028 00e849f5b397
folded 'Wellfounded_More_FP' into 'Wellfounded'
src/HOL/Cardinals/Order_Union.thy
src/HOL/Cardinals/README.txt
src/HOL/Cardinals/Wellfounded_More.thy
src/HOL/Cardinals/Wellfounded_More_FP.thy
src/HOL/Cardinals/Wellorder_Relation_FP.thy
src/HOL/Order_Relation.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Cardinals/Order_Union.thy	Fri Jan 17 10:02:49 2014 +0100
     1.2 +++ b/src/HOL/Cardinals/Order_Union.thy	Fri Jan 17 10:02:50 2014 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Order Union *}
     1.5  
     1.6  theory Order_Union
     1.7 -imports Wellfounded_More_FP
     1.8 +imports Order_Relation
     1.9  begin
    1.10  
    1.11  definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where
     2.1 --- a/src/HOL/Cardinals/README.txt	Fri Jan 17 10:02:49 2014 +0100
     2.2 +++ b/src/HOL/Cardinals/README.txt	Fri Jan 17 10:02:50 2014 +0100
     2.3 @@ -188,7 +188,7 @@
     2.4    Should we define all constants from "wo_rel" in "rel" instead, 
     2.5    so that their outside definition not be conditional in "wo_rel r"? 
     2.6  
     2.7 -Theory Wellfounded_More (and Wellfounded_More_FP):
     2.8 +Theory Wellfounded_More:
     2.9    Recall the lemmas "wfrec" and "wf_induct". 
    2.10  
    2.11  Theory Wellorder_Embedding (and Wellorder_Embedding_FP):
     3.1 --- a/src/HOL/Cardinals/Wellfounded_More.thy	Fri Jan 17 10:02:49 2014 +0100
     3.2 +++ b/src/HOL/Cardinals/Wellfounded_More.thy	Fri Jan 17 10:02:50 2014 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  header {* More on Well-Founded Relations *}
     3.5  
     3.6  theory Wellfounded_More
     3.7 -imports Wellfounded_More_FP Order_Relation_More
     3.8 +imports Wellfounded Order_Relation_More
     3.9  begin
    3.10  
    3.11  
     4.1 --- a/src/HOL/Cardinals/Wellfounded_More_FP.thy	Fri Jan 17 10:02:49 2014 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,194 +0,0 @@
     4.4 -(*  Title:      HOL/Cardinals/Wellfounded_More_FP.thy
     4.5 -    Author:     Andrei Popescu, TU Muenchen
     4.6 -    Copyright   2012
     4.7 -
     4.8 -More on well-founded relations (FP).
     4.9 -*)
    4.10 -
    4.11 -header {* More on Well-Founded Relations (FP) *}
    4.12 -
    4.13 -theory Wellfounded_More_FP
    4.14 -imports Wfrec Order_Relation
    4.15 -begin
    4.16 -
    4.17 -
    4.18 -text {* This section contains some variations of results in the theory
    4.19 -@{text "Wellfounded.thy"}:
    4.20 -\begin{itemize}
    4.21 -\item means for slightly more direct definitions by well-founded recursion;
    4.22 -\item variations of well-founded induction;
    4.23 -\item means for proving a linear order to be a well-order.
    4.24 -\end{itemize} *}
    4.25 -
    4.26 -
    4.27 -subsection {* Well-founded recursion via genuine fixpoints *}
    4.28 -
    4.29 -
    4.30 -(*2*)lemma wfrec_fixpoint:
    4.31 -fixes r :: "('a * 'a) set" and
    4.32 -      H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    4.33 -assumes WF: "wf r" and ADM: "adm_wf r H"
    4.34 -shows "wfrec r H = H (wfrec r H)"
    4.35 -proof(rule ext)
    4.36 -  fix x
    4.37 -  have "wfrec r H x = H (cut (wfrec r H) r x) x"
    4.38 -  using wfrec[of r H] WF by simp
    4.39 -  also
    4.40 -  {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
    4.41 -   by (auto simp add: cut_apply)
    4.42 -   hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
    4.43 -   using ADM adm_wf_def[of r H] by auto
    4.44 -  }
    4.45 -  finally show "wfrec r H x = H (wfrec r H) x" .
    4.46 -qed
    4.47 -
    4.48 -
    4.49 -
    4.50 -subsection {* Characterizations of well-founded-ness *}
    4.51 -
    4.52 -
    4.53 -text {* A transitive relation is well-founded iff it is ``locally" well-founded,
    4.54 -i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}
    4.55 -
    4.56 -(*3*)lemma trans_wf_iff:
    4.57 -assumes "trans r"
    4.58 -shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
    4.59 -proof-
    4.60 -  obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
    4.61 -  {assume *: "wf r"
    4.62 -   {fix a
    4.63 -    have "wf(R a)"
    4.64 -    using * R_def wf_subset[of r "R a"] by auto
    4.65 -   }
    4.66 -  }
    4.67 -  (*  *)
    4.68 -  moreover
    4.69 -  {assume *: "\<forall>a. wf(R a)"
    4.70 -   have "wf r"
    4.71 -   proof(unfold wf_def, clarify)
    4.72 -     fix phi a
    4.73 -     assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
    4.74 -     obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
    4.75 -     with * have "wf (R a)" by auto
    4.76 -     hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
    4.77 -     unfolding wf_def by blast
    4.78 -     moreover
    4.79 -     have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
    4.80 -     proof(auto simp add: chi_def R_def)
    4.81 -       fix b
    4.82 -       assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
    4.83 -       hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
    4.84 -       using assms trans_def[of r] by blast
    4.85 -       thus "phi b" using ** by blast
    4.86 -     qed
    4.87 -     ultimately have  "\<forall>b. chi b" by (rule mp)
    4.88 -     with ** chi_def show "phi a" by blast
    4.89 -   qed
    4.90 -  }
    4.91 -  ultimately show ?thesis using R_def by blast
    4.92 -qed
    4.93 -
    4.94 -
    4.95 -text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
    4.96 -allowing one to assume the set included in the field.  *}
    4.97 -
    4.98 -(*2*)lemma wf_eq_minimal2:
    4.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))"
   4.100 -proof-
   4.101 -  let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
   4.102 -  have "wf r = (\<forall>A. ?phi A)"
   4.103 -  by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
   4.104 -     (rule wfI_min, fast)
   4.105 -  (*  *)
   4.106 -  also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
   4.107 -  proof
   4.108 -    assume "\<forall>A. ?phi A"
   4.109 -    thus "\<forall>B \<le> Field r. ?phi B" by simp
   4.110 -  next
   4.111 -    assume *: "\<forall>B \<le> Field r. ?phi B"
   4.112 -    show "\<forall>A. ?phi A"
   4.113 -    proof(clarify)
   4.114 -      fix A::"'a set" assume **: "A \<noteq> {}"
   4.115 -      obtain B where B_def: "B = A Int (Field r)" by blast
   4.116 -      show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
   4.117 -      proof(cases "B = {}")
   4.118 -        assume Case1: "B = {}"
   4.119 -        obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
   4.120 -        using ** Case1 unfolding B_def by blast
   4.121 -        hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
   4.122 -        thus ?thesis using 1 by blast
   4.123 -      next
   4.124 -        assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
   4.125 -        obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
   4.126 -        using Case2 1 * by blast
   4.127 -        have "\<forall>a' \<in> A. (a',a) \<notin> r"
   4.128 -        proof(clarify)
   4.129 -          fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
   4.130 -          hence "a' \<in> B" unfolding B_def Field_def by blast
   4.131 -          thus False using 2 ** by blast
   4.132 -        qed
   4.133 -        thus ?thesis using 2 unfolding B_def by blast
   4.134 -      qed
   4.135 -    qed
   4.136 -  qed
   4.137 -  finally show ?thesis by blast
   4.138 -qed
   4.139 -
   4.140 -subsection {* Characterizations of well-founded-ness *}
   4.141 -
   4.142 -text {* The next lemma and its corollary enable one to prove that
   4.143 -a linear order is a well-order in a way which is more standard than
   4.144 -via well-founded-ness of the strict version of the relation.  *}
   4.145 -
   4.146 -(*3*)
   4.147 -lemma Linear_order_wf_diff_Id:
   4.148 -assumes LI: "Linear_order r"
   4.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))"
   4.150 -proof(cases "r \<le> Id")
   4.151 -  assume Case1: "r \<le> Id"
   4.152 -  hence temp: "r - Id = {}" by blast
   4.153 -  hence "wf(r - Id)" by (simp add: temp)
   4.154 -  moreover
   4.155 -  {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
   4.156 -   obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
   4.157 -   unfolding order_on_defs using Case1 Total_subset_Id by auto
   4.158 -   hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
   4.159 -   hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
   4.160 -  }
   4.161 -  ultimately show ?thesis by blast
   4.162 -next
   4.163 -  assume Case2: "\<not> r \<le> Id"
   4.164 -  hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
   4.165 -  unfolding order_on_defs by blast
   4.166 -  show ?thesis
   4.167 -  proof
   4.168 -    assume *: "wf(r - Id)"
   4.169 -    show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   4.170 -    proof(clarify)
   4.171 -      fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
   4.172 -      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   4.173 -      using 1 * unfolding wf_eq_minimal2 by simp
   4.174 -      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   4.175 -      using Linear_order_in_diff_Id[of r] ** LI by blast
   4.176 -      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
   4.177 -    qed
   4.178 -  next
   4.179 -    assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   4.180 -    show "wf(r - Id)"
   4.181 -    proof(unfold wf_eq_minimal2, clarify)
   4.182 -      fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
   4.183 -      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   4.184 -      using 1 * by simp
   4.185 -      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   4.186 -      using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
   4.187 -      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
   4.188 -    qed
   4.189 -  qed
   4.190 -qed
   4.191 -
   4.192 -(*3*)corollary Linear_order_Well_order_iff:
   4.193 -assumes "Linear_order r"
   4.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))"
   4.195 -using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
   4.196 -
   4.197 -end
     5.1 --- a/src/HOL/Cardinals/Wellorder_Relation_FP.thy	Fri Jan 17 10:02:49 2014 +0100
     5.2 +++ b/src/HOL/Cardinals/Wellorder_Relation_FP.thy	Fri Jan 17 10:02:50 2014 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  header {* Well-Order Relations (FP) *}
     5.5  
     5.6  theory Wellorder_Relation_FP
     5.7 -imports Wellfounded_More_FP
     5.8 +imports Order_Relation
     5.9  begin
    5.10  
    5.11  
     6.1 --- a/src/HOL/Order_Relation.thy	Fri Jan 17 10:02:49 2014 +0100
     6.2 +++ b/src/HOL/Order_Relation.thy	Fri Jan 17 10:02:50 2014 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* Orders as Relations *}
     6.5  
     6.6  theory Order_Relation
     6.7 -imports Wellfounded
     6.8 +imports Wfrec
     6.9  begin
    6.10  
    6.11  subsection{* Orders on a set *}
    6.12 @@ -303,4 +303,183 @@
    6.13    order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
    6.14  qed
    6.15  
    6.16 +
    6.17 +subsection {* Variations on Well-Founded Relations  *}
    6.18 +
    6.19 +text {*
    6.20 +This subsection contains some variations of the results from @{theory Wellfounded}:
    6.21 +\begin{itemize}
    6.22 +\item means for slightly more direct definitions by well-founded recursion;
    6.23 +\item variations of well-founded induction;
    6.24 +\item means for proving a linear order to be a well-order.
    6.25 +\end{itemize}
    6.26 +*}
    6.27 +
    6.28 +
    6.29 +subsubsection {* Well-founded recursion via genuine fixpoints *}
    6.30 +
    6.31 +lemma wfrec_fixpoint:
    6.32 +fixes r :: "('a * 'a) set" and
    6.33 +      H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    6.34 +assumes WF: "wf r" and ADM: "adm_wf r H"
    6.35 +shows "wfrec r H = H (wfrec r H)"
    6.36 +proof(rule ext)
    6.37 +  fix x
    6.38 +  have "wfrec r H x = H (cut (wfrec r H) r x) x"
    6.39 +  using wfrec[of r H] WF by simp
    6.40 +  also
    6.41 +  {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
    6.42 +   by (auto simp add: cut_apply)
    6.43 +   hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
    6.44 +   using ADM adm_wf_def[of r H] by auto
    6.45 +  }
    6.46 +  finally show "wfrec r H x = H (wfrec r H) x" .
    6.47 +qed
    6.48 +
    6.49 +
    6.50 +subsubsection {* Characterizations of well-foundedness *}
    6.51 +
    6.52 +text {* A transitive relation is well-founded iff it is ``locally'' well-founded,
    6.53 +i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}
    6.54 +
    6.55 +lemma trans_wf_iff:
    6.56 +assumes "trans r"
    6.57 +shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
    6.58 +proof-
    6.59 +  obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
    6.60 +  {assume *: "wf r"
    6.61 +   {fix a
    6.62 +    have "wf(R a)"
    6.63 +    using * R_def wf_subset[of r "R a"] by auto
    6.64 +   }
    6.65 +  }
    6.66 +  (*  *)
    6.67 +  moreover
    6.68 +  {assume *: "\<forall>a. wf(R a)"
    6.69 +   have "wf r"
    6.70 +   proof(unfold wf_def, clarify)
    6.71 +     fix phi a
    6.72 +     assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
    6.73 +     obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
    6.74 +     with * have "wf (R a)" by auto
    6.75 +     hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
    6.76 +     unfolding wf_def by blast
    6.77 +     moreover
    6.78 +     have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
    6.79 +     proof(auto simp add: chi_def R_def)
    6.80 +       fix b
    6.81 +       assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
    6.82 +       hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
    6.83 +       using assms trans_def[of r] by blast
    6.84 +       thus "phi b" using ** by blast
    6.85 +     qed
    6.86 +     ultimately have  "\<forall>b. chi b" by (rule mp)
    6.87 +     with ** chi_def show "phi a" by blast
    6.88 +   qed
    6.89 +  }
    6.90 +  ultimately show ?thesis using R_def by blast
    6.91 +qed
    6.92 +
    6.93 +text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
    6.94 +allowing one to assume the set included in the field.  *}
    6.95 +
    6.96 +lemma wf_eq_minimal2:
    6.97 +"wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
    6.98 +proof-
    6.99 +  let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
   6.100 +  have "wf r = (\<forall>A. ?phi A)"
   6.101 +  by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
   6.102 +     (rule wfI_min, fast)
   6.103 +  (*  *)
   6.104 +  also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
   6.105 +  proof
   6.106 +    assume "\<forall>A. ?phi A"
   6.107 +    thus "\<forall>B \<le> Field r. ?phi B" by simp
   6.108 +  next
   6.109 +    assume *: "\<forall>B \<le> Field r. ?phi B"
   6.110 +    show "\<forall>A. ?phi A"
   6.111 +    proof(clarify)
   6.112 +      fix A::"'a set" assume **: "A \<noteq> {}"
   6.113 +      obtain B where B_def: "B = A Int (Field r)" by blast
   6.114 +      show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
   6.115 +      proof(cases "B = {}")
   6.116 +        assume Case1: "B = {}"
   6.117 +        obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
   6.118 +        using ** Case1 unfolding B_def by blast
   6.119 +        hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
   6.120 +        thus ?thesis using 1 by blast
   6.121 +      next
   6.122 +        assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
   6.123 +        obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
   6.124 +        using Case2 1 * by blast
   6.125 +        have "\<forall>a' \<in> A. (a',a) \<notin> r"
   6.126 +        proof(clarify)
   6.127 +          fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
   6.128 +          hence "a' \<in> B" unfolding B_def Field_def by blast
   6.129 +          thus False using 2 ** by blast
   6.130 +        qed
   6.131 +        thus ?thesis using 2 unfolding B_def by blast
   6.132 +      qed
   6.133 +    qed
   6.134 +  qed
   6.135 +  finally show ?thesis by blast
   6.136 +qed
   6.137 +
   6.138 +
   6.139 +subsubsection {* Characterizations of well-foundedness *}
   6.140 +
   6.141 +text {* The next lemma and its corollary enable one to prove that
   6.142 +a linear order is a well-order in a way which is more standard than
   6.143 +via well-foundedness of the strict version of the relation.  *}
   6.144 +
   6.145 +lemma Linear_order_wf_diff_Id:
   6.146 +assumes LI: "Linear_order r"
   6.147 +shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
   6.148 +proof(cases "r \<le> Id")
   6.149 +  assume Case1: "r \<le> Id"
   6.150 +  hence temp: "r - Id = {}" by blast
   6.151 +  hence "wf(r - Id)" by (simp add: temp)
   6.152 +  moreover
   6.153 +  {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
   6.154 +   obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
   6.155 +   unfolding order_on_defs using Case1 Total_subset_Id by auto
   6.156 +   hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
   6.157 +   hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
   6.158 +  }
   6.159 +  ultimately show ?thesis by blast
   6.160 +next
   6.161 +  assume Case2: "\<not> r \<le> Id"
   6.162 +  hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
   6.163 +  unfolding order_on_defs by blast
   6.164 +  show ?thesis
   6.165 +  proof
   6.166 +    assume *: "wf(r - Id)"
   6.167 +    show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   6.168 +    proof(clarify)
   6.169 +      fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
   6.170 +      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   6.171 +      using 1 * unfolding wf_eq_minimal2 by simp
   6.172 +      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   6.173 +      using Linear_order_in_diff_Id[of r] ** LI by blast
   6.174 +      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
   6.175 +    qed
   6.176 +  next
   6.177 +    assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   6.178 +    show "wf(r - Id)"
   6.179 +    proof(unfold wf_eq_minimal2, clarify)
   6.180 +      fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
   6.181 +      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   6.182 +      using 1 * by simp
   6.183 +      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   6.184 +      using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
   6.185 +      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
   6.186 +    qed
   6.187 +  qed
   6.188 +qed
   6.189 +
   6.190 +corollary Linear_order_Well_order_iff:
   6.191 +assumes "Linear_order r"
   6.192 +shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
   6.193 +using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
   6.194 +
   6.195  end
     7.1 --- a/src/HOL/Wellfounded.thy	Fri Jan 17 10:02:49 2014 +0100
     7.2 +++ b/src/HOL/Wellfounded.thy	Fri Jan 17 10:02:50 2014 +0100
     7.3 @@ -3,6 +3,7 @@
     7.4      Author:     Lawrence C Paulson
     7.5      Author:     Konrad Slind
     7.6      Author:     Alexander Krauss
     7.7 +    Author:     Andrei Popescu, TU Muenchen
     7.8  *)
     7.9  
    7.10  header {*Well-founded Recursion*}