misc tuning and modernization;
authorwenzelm
Sun Jul 31 22:56:18 2016 +0200 (2016-07-31)
changeset 63572c0cbfd2b5a45
parent 63571 aee0d92995b6
child 63573 8976c5bc9e97
misc tuning and modernization;
src/HOL/Order_Relation.thy
src/HOL/Wellfounded.thy
src/HOL/Wfrec.thy
src/HOL/Zorn.thy
     1.1 --- a/src/HOL/Order_Relation.thy	Sun Jul 31 19:09:21 2016 +0200
     1.2 +++ b/src/HOL/Order_Relation.thy	Sun Jul 31 22:56:18 2016 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports Wfrec
     1.5  begin
     1.6  
     1.7 -subsection\<open>Orders on a set\<close>
     1.8 +subsection \<open>Orders on a set\<close>
     1.9  
    1.10  definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
    1.11  
    1.12 @@ -27,51 +27,48 @@
    1.13  
    1.14  
    1.15  lemma preorder_on_empty[simp]: "preorder_on {} {}"
    1.16 -by(simp add:preorder_on_def trans_def)
    1.17 +  by (simp add: preorder_on_def trans_def)
    1.18  
    1.19  lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
    1.20 -by(simp add:partial_order_on_def)
    1.21 +  by (simp add: partial_order_on_def)
    1.22  
    1.23  lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
    1.24 -by(simp add:linear_order_on_def)
    1.25 +  by (simp add: linear_order_on_def)
    1.26  
    1.27  lemma well_order_on_empty[simp]: "well_order_on {} {}"
    1.28 -by(simp add:well_order_on_def)
    1.29 +  by (simp add: well_order_on_def)
    1.30  
    1.31  
    1.32 -lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
    1.33 -by (simp add:preorder_on_def)
    1.34 +lemma preorder_on_converse[simp]: "preorder_on A (r\<inverse>) = preorder_on A r"
    1.35 +  by (simp add: preorder_on_def)
    1.36  
    1.37 -lemma partial_order_on_converse[simp]:
    1.38 -  "partial_order_on A (r^-1) = partial_order_on A r"
    1.39 -by (simp add: partial_order_on_def)
    1.40 +lemma partial_order_on_converse[simp]: "partial_order_on A (r\<inverse>) = partial_order_on A r"
    1.41 +  by (simp add: partial_order_on_def)
    1.42  
    1.43 -lemma linear_order_on_converse[simp]:
    1.44 -  "linear_order_on A (r^-1) = linear_order_on A r"
    1.45 -by (simp add: linear_order_on_def)
    1.46 +lemma linear_order_on_converse[simp]: "linear_order_on A (r\<inverse>) = linear_order_on A r"
    1.47 +  by (simp add: linear_order_on_def)
    1.48  
    1.49  
    1.50 -lemma strict_linear_order_on_diff_Id:
    1.51 -  "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
    1.52 -by(simp add: order_on_defs trans_diff_Id)
    1.53 +lemma strict_linear_order_on_diff_Id: "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r - Id)"
    1.54 +  by (simp add: order_on_defs trans_diff_Id)
    1.55  
    1.56  lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}"
    1.57 -unfolding order_on_defs by simp
    1.58 +  by (simp add: order_on_defs)
    1.59  
    1.60  lemma linear_order_on_acyclic:
    1.61    assumes "linear_order_on A r"
    1.62    shows "acyclic (r - Id)"
    1.63 -using strict_linear_order_on_diff_Id[OF assms] 
    1.64 -by(auto simp add: acyclic_irrefl strict_linear_order_on_def)
    1.65 +  using strict_linear_order_on_diff_Id[OF assms]
    1.66 +  by (auto simp add: acyclic_irrefl strict_linear_order_on_def)
    1.67  
    1.68  lemma linear_order_on_well_order_on:
    1.69    assumes "finite r"
    1.70    shows "linear_order_on A r \<longleftrightarrow> well_order_on A r"
    1.71 -unfolding well_order_on_def
    1.72 -using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast
    1.73 +  unfolding well_order_on_def
    1.74 +  using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast
    1.75  
    1.76  
    1.77 -subsection\<open>Orders on the field\<close>
    1.78 +subsection \<open>Orders on the field\<close>
    1.79  
    1.80  abbreviation "Refl r \<equiv> refl_on (Field r) r"
    1.81  
    1.82 @@ -87,50 +84,57 @@
    1.83  
    1.84  
    1.85  lemma subset_Image_Image_iff:
    1.86 -  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
    1.87 -   r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
    1.88 -unfolding preorder_on_def refl_on_def Image_def
    1.89 -apply (simp add: subset_eq)
    1.90 -unfolding trans_def by fast
    1.91 +  "Preorder r \<Longrightarrow> A \<subseteq> Field r \<Longrightarrow> B \<subseteq> Field r \<Longrightarrow>
    1.92 +    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b, a) \<in> r)"
    1.93 +  apply (simp add: preorder_on_def refl_on_def Image_def subset_eq)
    1.94 +  apply (simp only: trans_def)
    1.95 +  apply fast
    1.96 +  done
    1.97  
    1.98  lemma subset_Image1_Image1_iff:
    1.99 -  "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
   1.100 -by(simp add:subset_Image_Image_iff)
   1.101 +  "Preorder r \<Longrightarrow> a \<in> Field r \<Longrightarrow> b \<in> Field r \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b, a) \<in> r"
   1.102 +  by (simp add: subset_Image_Image_iff)
   1.103  
   1.104  lemma Refl_antisym_eq_Image1_Image1_iff:
   1.105 -  assumes r: "Refl r" and as: "antisym r" and abf: "a \<in> Field r" "b \<in> Field r"
   1.106 +  assumes "Refl r"
   1.107 +    and as: "antisym r"
   1.108 +    and abf: "a \<in> Field r" "b \<in> Field r"
   1.109    shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b"
   1.110 +    (is "?lhs \<longleftrightarrow> ?rhs")
   1.111  proof
   1.112 -  assume "r `` {a} = r `` {b}"
   1.113 -  hence e: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r" by (simp add: set_eq_iff)
   1.114 -  have "(a, a) \<in> r" "(b, b) \<in> r" using r abf by (simp_all add: refl_on_def)
   1.115 -  hence "(a, b) \<in> r" "(b, a) \<in> r" using e[of a] e[of b] by simp_all
   1.116 -  thus "a = b" using as[unfolded antisym_def] by blast
   1.117 -qed fast
   1.118 +  assume ?lhs
   1.119 +  then have *: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r"
   1.120 +    by (simp add: set_eq_iff)
   1.121 +  have "(a, a) \<in> r" "(b, b) \<in> r" using \<open>Refl r\<close> abf by (simp_all add: refl_on_def)
   1.122 +  then have "(a, b) \<in> r" "(b, a) \<in> r" using *[of a] *[of b] by simp_all
   1.123 +  then show ?rhs
   1.124 +    using \<open>antisym r\<close>[unfolded antisym_def] by blast
   1.125 +next
   1.126 +  assume ?rhs
   1.127 +  then show ?lhs by fast
   1.128 +qed
   1.129  
   1.130  lemma Partial_order_eq_Image1_Image1_iff:
   1.131 -  "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   1.132 -by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
   1.133 +  "Partial_order r \<Longrightarrow> a \<in> Field r \<Longrightarrow> b \<in> Field r \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a = b"
   1.134 +  by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff)
   1.135  
   1.136  lemma Total_Id_Field:
   1.137 -assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
   1.138 -shows "Field r = Field(r - Id)"
   1.139 -using mono_Field[of "r - Id" r] Diff_subset[of r Id]
   1.140 -proof(auto)
   1.141 -  have "r \<noteq> {}" using NID by fast
   1.142 -  then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
   1.143 -  hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
   1.144 -
   1.145 +  assumes "Total r"
   1.146 +    and not_Id: "\<not> r \<subseteq> Id"
   1.147 +  shows "Field r = Field (r - Id)"
   1.148 +  using mono_Field[of "r - Id" r] Diff_subset[of r Id]
   1.149 +proof auto
   1.150    fix a assume *: "a \<in> Field r"
   1.151 -  obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
   1.152 -  using * 1 by auto
   1.153 -  hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
   1.154 -  by (simp add: total_on_def)
   1.155 -  thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
   1.156 +  from not_Id have "r \<noteq> {}" by fast
   1.157 +  with not_Id obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" by auto
   1.158 +  then have "b \<noteq> c \<and> {b, c} \<subseteq> Field r" by (auto simp: Field_def)
   1.159 +  with * obtain d where "d \<in> Field r" "d \<noteq> a" by auto
   1.160 +  with * \<open>Total r\<close> have "(a, d) \<in> r \<or> (d, a) \<in> r" by (simp add: total_on_def)
   1.161 +  with \<open>d \<noteq> a\<close> show "a \<in> Field (r - Id)" unfolding Field_def by blast
   1.162  qed
   1.163  
   1.164  
   1.165 -subsection\<open>Orders on a type\<close>
   1.166 +subsection \<open>Orders on a type\<close>
   1.167  
   1.168  abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
   1.169  
   1.170 @@ -141,297 +145,303 @@
   1.171  
   1.172  subsection \<open>Order-like relations\<close>
   1.173  
   1.174 -text\<open>In this subsection, we develop basic concepts and results pertaining
   1.175 -to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
   1.176 -total relations. We also further define upper and lower bounds operators.\<close>
   1.177 +text \<open>
   1.178 +  In this subsection, we develop basic concepts and results pertaining
   1.179 +  to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
   1.180 +  total relations. We also further define upper and lower bounds operators.
   1.181 +\<close>
   1.182  
   1.183  
   1.184  subsubsection \<open>Auxiliaries\<close>
   1.185  
   1.186 -lemma refl_on_domain:
   1.187 -"\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
   1.188 -by(auto simp add: refl_on_def)
   1.189 +lemma refl_on_domain: "refl_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
   1.190 +  by (auto simp add: refl_on_def)
   1.191  
   1.192 -corollary well_order_on_domain:
   1.193 -"\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
   1.194 -by (auto simp add: refl_on_domain order_on_defs)
   1.195 +corollary well_order_on_domain: "well_order_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
   1.196 +  by (auto simp add: refl_on_domain order_on_defs)
   1.197  
   1.198 -lemma well_order_on_Field:
   1.199 -"well_order_on A r \<Longrightarrow> A = Field r"
   1.200 -by(auto simp add: refl_on_def Field_def order_on_defs)
   1.201 +lemma well_order_on_Field: "well_order_on A r \<Longrightarrow> A = Field r"
   1.202 +  by (auto simp add: refl_on_def Field_def order_on_defs)
   1.203  
   1.204 -lemma well_order_on_Well_order:
   1.205 -"well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
   1.206 -using well_order_on_Field by auto
   1.207 +lemma well_order_on_Well_order: "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
   1.208 +  using well_order_on_Field [of A] by auto
   1.209  
   1.210  lemma Total_subset_Id:
   1.211 -assumes TOT: "Total r" and SUB: "r \<le> Id"
   1.212 -shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
   1.213 -proof-
   1.214 -  {assume "r \<noteq> {}"
   1.215 -   then obtain a b where 1: "(a,b) \<in> r" by fast
   1.216 -   hence "a = b" using SUB by blast
   1.217 -   hence 2: "(a,a) \<in> r" using 1 by simp
   1.218 -   {fix c d assume "(c,d) \<in> r"
   1.219 -    hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast
   1.220 -    hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>
   1.221 -           ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"
   1.222 -    using TOT unfolding total_on_def by blast
   1.223 -    hence "a = c \<and> a = d" using SUB by blast
   1.224 -   }
   1.225 -   hence "r \<le> {(a,a)}" by auto
   1.226 -   with 2 have "\<exists>a. r = {(a,a)}" by blast
   1.227 -  }
   1.228 -  thus ?thesis by blast
   1.229 +  assumes "Total r"
   1.230 +    and "r \<subseteq> Id"
   1.231 +  shows "r = {} \<or> (\<exists>a. r = {(a, a)})"
   1.232 +proof -
   1.233 +  have "\<exists>a. r = {(a, a)}" if "r \<noteq> {}"
   1.234 +  proof -
   1.235 +    from that obtain a b where ab: "(a, b) \<in> r" by fast
   1.236 +    with \<open>r \<subseteq> Id\<close> have "a = b" by blast
   1.237 +    with ab have aa: "(a, a) \<in> r" by simp
   1.238 +    have "a = c \<and> a = d" if "(c, d) \<in> r" for c d
   1.239 +    proof -
   1.240 +      from that have "{a, c, d} \<subseteq> Field r"
   1.241 +        using ab unfolding Field_def by blast
   1.242 +      then have "((a, c) \<in> r \<or> (c, a) \<in> r \<or> a = c) \<and> ((a, d) \<in> r \<or> (d, a) \<in> r \<or> a = d)"
   1.243 +        using \<open>Total r\<close> unfolding total_on_def by blast
   1.244 +      with \<open>r \<subseteq> Id\<close> show ?thesis by blast
   1.245 +    qed
   1.246 +    then have "r \<subseteq> {(a, a)}" by auto
   1.247 +    with aa show ?thesis by blast
   1.248 +  qed
   1.249 +  then show ?thesis by blast
   1.250  qed
   1.251  
   1.252  lemma Linear_order_in_diff_Id:
   1.253 -assumes LI: "Linear_order r" and
   1.254 -        IN1: "a \<in> Field r" and IN2: "b \<in> Field r"
   1.255 -shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
   1.256 -using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
   1.257 +  assumes "Linear_order r"
   1.258 +    and "a \<in> Field r"
   1.259 +    and "b \<in> Field r"
   1.260 +  shows "(a, b) \<in> r \<longleftrightarrow> (b, a) \<notin> r - Id"
   1.261 +  using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
   1.262  
   1.263  
   1.264  subsubsection \<open>The upper and lower bounds operators\<close>
   1.265  
   1.266 -text\<open>Here we define upper (``above") and lower (``below") bounds operators.
   1.267 -We think of \<open>r\<close> as a {\em non-strict} relation.  The suffix ``S"
   1.268 -at the names of some operators indicates that the bounds are strict -- e.g.,
   1.269 -\<open>underS a\<close> is the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>).
   1.270 -Capitalization of the first letter in the name reminds that the operator acts on sets, rather
   1.271 -than on individual elements.\<close>
   1.272 +text \<open>
   1.273 +  Here we define upper (``above") and lower (``below") bounds operators. We
   1.274 +  think of \<open>r\<close> as a \<^emph>\<open>non-strict\<close> relation. The suffix \<open>S\<close> at the names of
   1.275 +  some operators indicates that the bounds are strict -- e.g., \<open>underS a\<close> is
   1.276 +  the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>). Capitalization of
   1.277 +  the first letter in the name reminds that the operator acts on sets, rather
   1.278 +  than on individual elements.
   1.279 +\<close>
   1.280  
   1.281 -definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   1.282 -where "under r a \<equiv> {b. (b,a) \<in> r}"
   1.283 +definition under :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   1.284 +  where "under r a \<equiv> {b. (b, a) \<in> r}"
   1.285  
   1.286 -definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   1.287 -where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
   1.288 +definition underS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   1.289 +  where "underS r a \<equiv> {b. b \<noteq> a \<and> (b, a) \<in> r}"
   1.290  
   1.291 -definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.292 -where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
   1.293 +definition Under :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.294 +  where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b, a) \<in> r}"
   1.295  
   1.296 -definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.297 -where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
   1.298 +definition UnderS :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.299 +  where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b, a) \<in> r}"
   1.300  
   1.301 -definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   1.302 -where "above r a \<equiv> {b. (a,b) \<in> r}"
   1.303 +definition above :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   1.304 +  where "above r a \<equiv> {b. (a, b) \<in> r}"
   1.305  
   1.306 -definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   1.307 -where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
   1.308 +definition aboveS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   1.309 +  where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a, b) \<in> r}"
   1.310  
   1.311 -definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.312 -where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
   1.313 +definition Above :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.314 +  where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a, b) \<in> r}"
   1.315  
   1.316 -definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.317 -where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
   1.318 +definition AboveS :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.319 +  where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a, b) \<in> r}"
   1.320  
   1.321  definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
   1.322 -where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
   1.323 +  where "ofilter r A \<equiv> A \<subseteq> Field r \<and> (\<forall>a \<in> A. under r a \<subseteq> A)"
   1.324  
   1.325 -text\<open>Note:  In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>,
   1.326 -  we bounded comprehension by \<open>Field r\<close> in order to properly cover
   1.327 -  the case of \<open>A\<close> being empty.\<close>
   1.328 +text \<open>
   1.329 +  Note: In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>, we bounded
   1.330 +  comprehension by \<open>Field r\<close> in order to properly cover the case of \<open>A\<close> being
   1.331 +  empty.
   1.332 +\<close>
   1.333  
   1.334 -lemma underS_subset_under: "underS r a \<le> under r a"
   1.335 -by(auto simp add: underS_def under_def)
   1.336 +lemma underS_subset_under: "underS r a \<subseteq> under r a"
   1.337 +  by (auto simp add: underS_def under_def)
   1.338  
   1.339  lemma underS_notIn: "a \<notin> underS r a"
   1.340 -by(simp add: underS_def)
   1.341 +  by (simp add: underS_def)
   1.342  
   1.343 -lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
   1.344 -by(simp add: refl_on_def under_def)
   1.345 +lemma Refl_under_in: "Refl r \<Longrightarrow> a \<in> Field r \<Longrightarrow> a \<in> under r a"
   1.346 +  by (simp add: refl_on_def under_def)
   1.347  
   1.348 -lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
   1.349 -by(auto simp add: AboveS_def)
   1.350 +lemma AboveS_disjoint: "A \<inter> (AboveS r A) = {}"
   1.351 +  by (auto simp add: AboveS_def)
   1.352  
   1.353  lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
   1.354 -by(auto simp add: AboveS_def underS_def)
   1.355 +  by (auto simp add: AboveS_def underS_def)
   1.356  
   1.357 -lemma Refl_under_underS:
   1.358 -  assumes "Refl r" "a \<in> Field r"
   1.359 -  shows "under r a = underS r a \<union> {a}"
   1.360 -unfolding under_def underS_def
   1.361 -using assms refl_on_def[of _ r] by fastforce
   1.362 +lemma Refl_under_underS: "Refl r \<Longrightarrow> a \<in> Field r \<Longrightarrow> under r a = underS r a \<union> {a}"
   1.363 +  unfolding under_def underS_def
   1.364 +  using refl_on_def[of _ r] by fastforce
   1.365  
   1.366  lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
   1.367 -by (auto simp: Field_def underS_def)
   1.368 +  by (auto simp: Field_def underS_def)
   1.369  
   1.370 -lemma under_Field: "under r a \<le> Field r"
   1.371 -by(unfold under_def Field_def, auto)
   1.372 +lemma under_Field: "under r a \<subseteq> Field r"
   1.373 +  by (auto simp: under_def Field_def)
   1.374  
   1.375 -lemma underS_Field: "underS r a \<le> Field r"
   1.376 -by(unfold underS_def Field_def, auto)
   1.377 +lemma underS_Field: "underS r a \<subseteq> Field r"
   1.378 +  by (auto simp: underS_def Field_def)
   1.379  
   1.380 -lemma underS_Field2:
   1.381 -"a \<in> Field r \<Longrightarrow> underS r a < Field r"
   1.382 -using underS_notIn underS_Field by fast
   1.383 +lemma underS_Field2: "a \<in> Field r \<Longrightarrow> underS r a \<subset> Field r"
   1.384 +  using underS_notIn underS_Field by fast
   1.385  
   1.386 -lemma underS_Field3:
   1.387 -"Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
   1.388 -by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
   1.389 +lemma underS_Field3: "Field r \<noteq> {} \<Longrightarrow> underS r a \<subset> Field r"
   1.390 +  by (cases "a \<in> Field r") (auto simp: underS_Field2 underS_empty)
   1.391  
   1.392 -lemma AboveS_Field: "AboveS r A \<le> Field r"
   1.393 -by(unfold AboveS_def Field_def, auto)
   1.394 +lemma AboveS_Field: "AboveS r A \<subseteq> Field r"
   1.395 +  by (auto simp: AboveS_def Field_def)
   1.396  
   1.397  lemma under_incr:
   1.398 -  assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
   1.399 -  shows "under r a \<le> under r b"
   1.400 -proof(unfold under_def, auto)
   1.401 -  fix x assume "(x,a) \<in> r"
   1.402 -  with REL TRANS trans_def[of r]
   1.403 -  show "(x,b) \<in> r" by blast
   1.404 +  assumes "trans r"
   1.405 +    and "(a, b) \<in> r"
   1.406 +  shows "under r a \<subseteq> under r b"
   1.407 +  unfolding under_def
   1.408 +proof auto
   1.409 +  fix x assume "(x, a) \<in> r"
   1.410 +  with assms trans_def[of r] show "(x, b) \<in> r" by blast
   1.411  qed
   1.412  
   1.413  lemma underS_incr:
   1.414 -assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   1.415 -        REL: "(a,b) \<in> r"
   1.416 -shows "underS r a \<le> underS r b"
   1.417 -proof(unfold underS_def, auto)
   1.418 -  assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
   1.419 -  with ANTISYM antisym_def[of r] REL
   1.420 -  show False by blast
   1.421 +  assumes "trans r"
   1.422 +    and "antisym r"
   1.423 +    and ab: "(a, b) \<in> r"
   1.424 +  shows "underS r a \<subseteq> underS r b"
   1.425 +  unfolding underS_def
   1.426 +proof auto
   1.427 +  assume *: "b \<noteq> a" and **: "(b, a) \<in> r"
   1.428 +  with \<open>antisym r\<close> antisym_def[of r] ab show False
   1.429 +    by blast
   1.430  next
   1.431 -  fix x assume "x \<noteq> a" "(x,a) \<in> r"
   1.432 -  with REL TRANS trans_def[of r]
   1.433 -  show "(x,b) \<in> r" by blast
   1.434 +  fix x assume "x \<noteq> a" "(x, a) \<in> r"
   1.435 +  with ab \<open>trans r\<close> trans_def[of r] show "(x, b) \<in> r"
   1.436 +    by blast
   1.437  qed
   1.438  
   1.439  lemma underS_incl_iff:
   1.440 -assumes LO: "Linear_order r" and
   1.441 -        INa: "a \<in> Field r" and INb: "b \<in> Field r"
   1.442 -shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
   1.443 +  assumes LO: "Linear_order r"
   1.444 +    and INa: "a \<in> Field r"
   1.445 +    and INb: "b \<in> Field r"
   1.446 +  shows "underS r a \<subseteq> underS r b \<longleftrightarrow> (a, b) \<in> r"
   1.447 +    (is "?lhs \<longleftrightarrow> ?rhs")
   1.448  proof
   1.449 -  assume "(a,b) \<in> r"
   1.450 -  thus "underS r a \<le> underS r b" using LO
   1.451 -  by (simp add: order_on_defs underS_incr)
   1.452 +  assume ?rhs
   1.453 +  with \<open>Linear_order r\<close> show ?lhs
   1.454 +    by (simp add: order_on_defs underS_incr)
   1.455  next
   1.456 -  assume *: "underS r a \<le> underS r b"
   1.457 -  {assume "a = b"
   1.458 -   hence "(a,b) \<in> r" using assms
   1.459 -   by (simp add: order_on_defs refl_on_def)
   1.460 -  }
   1.461 -  moreover
   1.462 -  {assume "a \<noteq> b \<and> (b,a) \<in> r"
   1.463 -   hence "b \<in> underS r a" unfolding underS_def by blast
   1.464 -   hence "b \<in> underS r b" using * by blast
   1.465 -   hence False by (simp add: underS_notIn)
   1.466 -  }
   1.467 -  ultimately
   1.468 -  show "(a,b) \<in> r" using assms
   1.469 -  order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
   1.470 +  assume *: ?lhs
   1.471 +  have "(a, b) \<in> r" if "a = b"
   1.472 +    using assms that by (simp add: order_on_defs refl_on_def)
   1.473 +  moreover have False if "a \<noteq> b" "(b, a) \<in> r"
   1.474 +  proof -
   1.475 +    from that have "b \<in> underS r a" unfolding underS_def by blast
   1.476 +    with * have "b \<in> underS r b" by blast
   1.477 +    then show ?thesis by (simp add: underS_notIn)
   1.478 +  qed
   1.479 +  ultimately show "(a,b) \<in> r"
   1.480 +    using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
   1.481  qed
   1.482  
   1.483  lemma finite_Linear_order_induct[consumes 3, case_names step]:
   1.484    assumes "Linear_order r"
   1.485 -  and "x \<in> Field r"
   1.486 -  and "finite r"
   1.487 -  and step: "\<And>x. \<lbrakk>x \<in> Field r; \<And>y. y \<in> aboveS r x \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> P x"
   1.488 +    and "x \<in> Field r"
   1.489 +    and "finite r"
   1.490 +    and step: "\<And>x. x \<in> Field r \<Longrightarrow> (\<And>y. y \<in> aboveS r x \<Longrightarrow> P y) \<Longrightarrow> P x"
   1.491    shows "P x"
   1.492 -using assms(2)
   1.493 -proof(induct rule: wf_induct[of "r\<inverse> - Id"])
   1.494 +  using assms(2)
   1.495 +proof (induct rule: wf_induct[of "r\<inverse> - Id"])
   1.496 +  case 1
   1.497    from assms(1,3) show "wf (r\<inverse> - Id)"
   1.498      using linear_order_on_well_order_on linear_order_on_converse
   1.499      unfolding well_order_on_def by blast
   1.500  next
   1.501 -  case (2 x) then show ?case
   1.502 -    by - (rule step; auto simp: aboveS_def intro: FieldI2)
   1.503 +  case prems: (2 x)
   1.504 +  show ?case
   1.505 +    by (rule step) (use prems in \<open>auto simp: aboveS_def intro: FieldI2\<close>)
   1.506  qed
   1.507  
   1.508  
   1.509  subsection \<open>Variations on Well-Founded Relations\<close>
   1.510  
   1.511  text \<open>
   1.512 -This subsection contains some variations of the results from @{theory Wellfounded}:
   1.513 -\begin{itemize}
   1.514 -\item means for slightly more direct definitions by well-founded recursion;
   1.515 -\item variations of well-founded induction;
   1.516 -\item means for proving a linear order to be a well-order.
   1.517 -\end{itemize}
   1.518 +  This subsection contains some variations of the results from @{theory Wellfounded}:
   1.519 +    \<^item> means for slightly more direct definitions by well-founded recursion;
   1.520 +    \<^item> variations of well-founded induction;
   1.521 +    \<^item> means for proving a linear order to be a well-order.
   1.522  \<close>
   1.523  
   1.524  
   1.525  subsubsection \<open>Characterizations of well-foundedness\<close>
   1.526  
   1.527 -text \<open>A transitive relation is well-founded iff it is ``locally'' well-founded,
   1.528 -i.e., iff its restriction to the lower bounds of of any element is well-founded.\<close>
   1.529 +text \<open>
   1.530 +  A transitive relation is well-founded iff it is ``locally'' well-founded,
   1.531 +  i.e., iff its restriction to the lower bounds of of any element is
   1.532 +  well-founded.
   1.533 +\<close>
   1.534  
   1.535  lemma trans_wf_iff:
   1.536 -assumes "trans r"
   1.537 -shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
   1.538 -proof-
   1.539 -  obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
   1.540 -  {assume *: "wf r"
   1.541 -   {fix a
   1.542 -    have "wf(R a)"
   1.543 -    using * R_def wf_subset[of r "R a"] by auto
   1.544 -   }
   1.545 -  }
   1.546 -  (*  *)
   1.547 +  assumes "trans r"
   1.548 +  shows "wf r \<longleftrightarrow> (\<forall>a. wf (r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{a})))"
   1.549 +proof -
   1.550 +  define R where "R a = r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{a})" for a
   1.551 +  have "wf (R a)" if "wf r" for a
   1.552 +    using that R_def wf_subset[of r "R a"] by auto
   1.553    moreover
   1.554 -  {assume *: "\<forall>a. wf(R a)"
   1.555 -   have "wf r"
   1.556 -   proof(unfold wf_def, clarify)
   1.557 -     fix phi a
   1.558 -     assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
   1.559 -     obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
   1.560 -     with * have "wf (R a)" by auto
   1.561 -     hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
   1.562 -     unfolding wf_def by blast
   1.563 -     moreover
   1.564 -     have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
   1.565 -     proof(auto simp add: chi_def R_def)
   1.566 -       fix b
   1.567 -       assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
   1.568 -       hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
   1.569 -       using assms trans_def[of r] by blast
   1.570 -       thus "phi b" using ** by blast
   1.571 -     qed
   1.572 -     ultimately have  "\<forall>b. chi b" by (rule mp)
   1.573 -     with ** chi_def show "phi a" by blast
   1.574 -   qed
   1.575 -  }
   1.576 -  ultimately show ?thesis using R_def by blast
   1.577 +  have "wf r" if *: "\<forall>a. wf(R a)"
   1.578 +    unfolding wf_def
   1.579 +  proof clarify
   1.580 +    fix phi a
   1.581 +    assume **: "\<forall>a. (\<forall>b. (b, a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
   1.582 +    define chi where "chi b \<longleftrightarrow> (b, a) \<in> r \<longrightarrow> phi b" for b
   1.583 +    with * have "wf (R a)" by auto
   1.584 +    then have "(\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
   1.585 +      unfolding wf_def by blast
   1.586 +    also have "\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
   1.587 +    proof (auto simp add: chi_def R_def)
   1.588 +      fix b
   1.589 +      assume "(b, a) \<in> r" and "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
   1.590 +      then have "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
   1.591 +        using assms trans_def[of r] by blast
   1.592 +      with ** show "phi b" by blast
   1.593 +    qed
   1.594 +    finally have  "\<forall>b. chi b" .
   1.595 +    with ** chi_def show "phi a" by blast
   1.596 +  qed
   1.597 +  ultimately show ?thesis unfolding R_def by blast
   1.598  qed
   1.599  
   1.600  text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
   1.601 -allowing one to assume the set included in the field.\<close>
   1.602 +  allowing one to assume the set included in the field.\<close>
   1.603  
   1.604 -lemma wf_eq_minimal2:
   1.605 -"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.606 +lemma wf_eq_minimal2: "wf r \<longleftrightarrow> (\<forall>A. A \<subseteq> Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a', a) \<notin> r))"
   1.607  proof-
   1.608 -  let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
   1.609 -  have "wf r = (\<forall>A. ?phi A)"
   1.610 -  by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
   1.611 -     (rule wfI_min, fast)
   1.612 -  (*  *)
   1.613 -  also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
   1.614 +  let ?phi = "\<lambda>A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r)"
   1.615 +  have "wf r \<longleftrightarrow> (\<forall>A. ?phi A)"
   1.616 +    apply (auto simp: ex_in_conv [THEN sym])
   1.617 +     apply (erule wfE_min)
   1.618 +      apply assumption
   1.619 +     apply blast
   1.620 +    apply (rule wfI_min)
   1.621 +    apply fast
   1.622 +    done
   1.623 +  also have "(\<forall>A. ?phi A) \<longleftrightarrow> (\<forall>B \<subseteq> Field r. ?phi B)"
   1.624    proof
   1.625      assume "\<forall>A. ?phi A"
   1.626 -    thus "\<forall>B \<le> Field r. ?phi B" by simp
   1.627 +    then show "\<forall>B \<subseteq> Field r. ?phi B" by simp
   1.628    next
   1.629 -    assume *: "\<forall>B \<le> Field r. ?phi B"
   1.630 +    assume *: "\<forall>B \<subseteq> Field r. ?phi B"
   1.631      show "\<forall>A. ?phi A"
   1.632 -    proof(clarify)
   1.633 -      fix A::"'a set" assume **: "A \<noteq> {}"
   1.634 -      obtain B where B_def: "B = A Int (Field r)" by blast
   1.635 -      show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
   1.636 -      proof(cases "B = {}")
   1.637 -        assume Case1: "B = {}"
   1.638 -        obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
   1.639 -        using ** Case1 unfolding B_def by blast
   1.640 -        hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
   1.641 -        thus ?thesis using 1 by blast
   1.642 +    proof clarify
   1.643 +      fix A :: "'a set"
   1.644 +      assume **: "A \<noteq> {}"
   1.645 +      define B where "B = A \<inter> Field r"
   1.646 +      show "\<exists>a \<in> A. \<forall>a' \<in> A. (a', a) \<notin> r"
   1.647 +      proof (cases "B = {}")
   1.648 +        case True
   1.649 +        with ** obtain a where a: "a \<in> A" "a \<notin> Field r"
   1.650 +          unfolding B_def by blast
   1.651 +        with a have "\<forall>a' \<in> A. (a',a) \<notin> r"
   1.652 +          unfolding Field_def by blast
   1.653 +        with a show ?thesis by blast
   1.654        next
   1.655 -        assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
   1.656 -        obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
   1.657 -        using Case2 1 * by blast
   1.658 -        have "\<forall>a' \<in> A. (a',a) \<notin> r"
   1.659 -        proof(clarify)
   1.660 -          fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
   1.661 -          hence "a' \<in> B" unfolding B_def Field_def by blast
   1.662 -          thus False using 2 ** by blast
   1.663 +        case False
   1.664 +        have "B \<subseteq> Field r" unfolding B_def by blast
   1.665 +        with False * obtain a where a: "a \<in> B" "\<forall>a' \<in> B. (a', a) \<notin> r"
   1.666 +          by blast
   1.667 +        have "(a', a) \<notin> r" if "a' \<in> A" for a'
   1.668 +        proof
   1.669 +          assume a'a: "(a', a) \<in> r"
   1.670 +          with that have "a' \<in> B" unfolding B_def Field_def by blast
   1.671 +          with a a'a show False by blast
   1.672          qed
   1.673 -        thus ?thesis using 2 unfolding B_def by blast
   1.674 +        with a show ?thesis unfolding B_def by blast
   1.675        qed
   1.676      qed
   1.677    qed
   1.678 @@ -441,58 +451,67 @@
   1.679  
   1.680  subsubsection \<open>Characterizations of well-foundedness\<close>
   1.681  
   1.682 -text \<open>The next lemma and its corollary enable one to prove that
   1.683 -a linear order is a well-order in a way which is more standard than
   1.684 -via well-foundedness of the strict version of the relation.\<close>
   1.685 +text \<open>
   1.686 +  The next lemma and its corollary enable one to prove that a linear order is
   1.687 +  a well-order in a way which is more standard than via well-foundedness of
   1.688 +  the strict version of the relation.
   1.689 +\<close>
   1.690  
   1.691  lemma Linear_order_wf_diff_Id:
   1.692 -assumes LI: "Linear_order r"
   1.693 -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.694 -proof(cases "r \<le> Id")
   1.695 -  assume Case1: "r \<le> Id"
   1.696 -  hence temp: "r - Id = {}" by blast
   1.697 -  hence "wf(r - Id)" by (simp add: temp)
   1.698 -  moreover
   1.699 -  {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
   1.700 -   obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
   1.701 -   unfolding order_on_defs using Case1 Total_subset_Id by auto
   1.702 -   hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
   1.703 -   hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
   1.704 -  }
   1.705 +  assumes "Linear_order r"
   1.706 +  shows "wf (r - Id) \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
   1.707 +proof (cases "r \<subseteq> Id")
   1.708 +  case True
   1.709 +  then have *: "r - Id = {}" by blast
   1.710 +  have "wf (r - Id)" by (simp add: *)
   1.711 +  moreover have "\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r"
   1.712 +    if *: "A \<subseteq> Field r" and **: "A \<noteq> {}" for A
   1.713 +  proof -
   1.714 +    from \<open>Linear_order r\<close> True
   1.715 +    obtain a where a: "r = {} \<or> r = {(a, a)}"
   1.716 +      unfolding order_on_defs using Total_subset_Id [of r] by blast
   1.717 +    with * ** have "A = {a} \<and> r = {(a, a)}"
   1.718 +      unfolding Field_def by blast
   1.719 +    with a show ?thesis by blast
   1.720 +  qed
   1.721    ultimately show ?thesis by blast
   1.722  next
   1.723 -  assume Case2: "\<not> r \<le> Id"
   1.724 -  hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
   1.725 -  unfolding order_on_defs by blast
   1.726 +  case False
   1.727 +  with \<open>Linear_order r\<close> have Field: "Field r = Field (r - Id)"
   1.728 +    unfolding order_on_defs using Total_Id_Field [of r] by blast
   1.729    show ?thesis
   1.730    proof
   1.731 -    assume *: "wf(r - Id)"
   1.732 -    show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   1.733 -    proof(clarify)
   1.734 -      fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
   1.735 -      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   1.736 -      using 1 * unfolding wf_eq_minimal2 by simp
   1.737 -      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   1.738 -      using Linear_order_in_diff_Id[of r] ** LI by blast
   1.739 -      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
   1.740 +    assume *: "wf (r - Id)"
   1.741 +    show "\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r)"
   1.742 +    proof clarify
   1.743 +      fix A
   1.744 +      assume **: "A \<subseteq> Field r" and ***: "A \<noteq> {}"
   1.745 +      then have "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   1.746 +        using Field * unfolding wf_eq_minimal2 by simp
   1.747 +      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r \<longleftrightarrow> (a', a) \<notin> r - Id"
   1.748 +        using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** by blast
   1.749 +      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r" by blast
   1.750      qed
   1.751    next
   1.752 -    assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   1.753 -    show "wf(r - Id)"
   1.754 -    proof(unfold wf_eq_minimal2, clarify)
   1.755 -      fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
   1.756 -      hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   1.757 -      using 1 * by simp
   1.758 -      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   1.759 -      using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
   1.760 -      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
   1.761 +    assume *: "\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r)"
   1.762 +    show "wf (r - Id)"
   1.763 +      unfolding wf_eq_minimal2
   1.764 +    proof clarify
   1.765 +      fix A
   1.766 +      assume **: "A \<subseteq> Field(r - Id)" and ***: "A \<noteq> {}"
   1.767 +      then have "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   1.768 +        using Field * by simp
   1.769 +      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r \<longleftrightarrow> (a', a) \<notin> r - Id"
   1.770 +        using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** mono_Field[of "r - Id" r] by blast
   1.771 +      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   1.772 +        by blast
   1.773      qed
   1.774    qed
   1.775  qed
   1.776  
   1.777  corollary Linear_order_Well_order_iff:
   1.778 -assumes "Linear_order r"
   1.779 -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.780 -using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
   1.781 +  "Linear_order r \<Longrightarrow>
   1.782 +    Well_order r \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
   1.783 +  unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
   1.784  
   1.785  end
     2.1 --- a/src/HOL/Wellfounded.thy	Sun Jul 31 19:09:21 2016 +0200
     2.2 +++ b/src/HOL/Wellfounded.thy	Sun Jul 31 22:56:18 2016 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  section \<open>Well-founded Recursion\<close>
     2.5  
     2.6  theory Wellfounded
     2.7 -imports Transitive_Closure
     2.8 +  imports Transitive_Closure
     2.9  begin
    2.10  
    2.11  subsection \<open>Basic Definitions\<close>
    2.12 @@ -59,12 +59,14 @@
    2.13  lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r"
    2.14    by (blast elim: wf_asym)
    2.15  
    2.16 -lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r"
    2.17 +lemma wf_irrefl:
    2.18 +  assumes "wf r"
    2.19 +  obtains "(a, a) \<notin> r"
    2.20    by (drule wf_not_refl[OF assms])
    2.21  
    2.22  lemma wf_wellorderI:
    2.23    assumes wf: "wf {(x::'a::ord, y). x < y}"
    2.24 -  assumes lin: "OFCLASS('a::ord, linorder_class)"
    2.25 +    and lin: "OFCLASS('a::ord, linorder_class)"
    2.26    shows "OFCLASS('a::ord, wellorder_class)"
    2.27    using lin
    2.28    apply (rule wellorder_class.intro)
    2.29 @@ -83,7 +85,7 @@
    2.30  
    2.31  lemma wfE_pf:
    2.32    assumes wf: "wf R"
    2.33 -  assumes a: "A \<subseteq> R `` A"
    2.34 +    and a: "A \<subseteq> R `` A"
    2.35    shows "A = {}"
    2.36  proof -
    2.37    from wf have "x \<notin> A" for x
    2.38 @@ -130,10 +132,13 @@
    2.39  qed
    2.40  
    2.41  lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))"
    2.42 -apply auto
    2.43 -apply (erule wfE_min, assumption, blast)
    2.44 -apply (rule wfI_min, auto)
    2.45 -done
    2.46 +  apply auto
    2.47 +   apply (erule wfE_min)
    2.48 +    apply assumption
    2.49 +   apply blast
    2.50 +  apply (rule wfI_min)
    2.51 +  apply auto
    2.52 +  done
    2.53  
    2.54  lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
    2.55  
    2.56 @@ -200,18 +205,13 @@
    2.57    then show ?thesis by (simp add: bot_fun_def)
    2.58  qed
    2.59  
    2.60 -lemma wf_Int1: "wf r \<Longrightarrow> wf (r Int r')"
    2.61 -  apply (erule wf_subset)
    2.62 -  apply (rule Int_lower1)
    2.63 -  done
    2.64 +lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')"
    2.65 +  by (erule wf_subset) (rule Int_lower1)
    2.66  
    2.67 -lemma wf_Int2: "wf r \<Longrightarrow> wf (r' Int r)"
    2.68 -  apply (erule wf_subset)
    2.69 -  apply (rule Int_lower2)
    2.70 -  done
    2.71 +lemma wf_Int2: "wf r \<Longrightarrow> wf (r' \<inter> r)"
    2.72 +  by (erule wf_subset) (rule Int_lower2)
    2.73  
    2.74 -text \<open>Exponentiation\<close>
    2.75 -
    2.76 +text \<open>Exponentiation.\<close>
    2.77  lemma wf_exp:
    2.78    assumes "wf (R ^^ n)"
    2.79    shows "wf R"
    2.80 @@ -222,38 +222,43 @@
    2.81    show "A = {}" by (rule wfE_pf)
    2.82  qed
    2.83  
    2.84 -text \<open>Well-foundedness of insert\<close>
    2.85 -
    2.86 +text \<open>Well-foundedness of \<open>insert\<close>.\<close>
    2.87  lemma wf_insert [iff]: "wf (insert (y, x) r) \<longleftrightarrow> wf r \<and> (x, y) \<notin> r\<^sup>*"
    2.88 -apply (rule iffI)
    2.89 - apply (blast elim: wf_trancl [THEN wf_irrefl]
    2.90 -              intro: rtrancl_into_trancl1 wf_subset
    2.91 -                     rtrancl_mono [THEN [2] rev_subsetD])
    2.92 -apply (simp add: wf_eq_minimal, safe)
    2.93 -apply (rule allE, assumption, erule impE, blast)
    2.94 -apply (erule bexE)
    2.95 -apply (rename_tac "a", case_tac "a = x")
    2.96 - prefer 2
    2.97 -apply blast
    2.98 -apply (case_tac "y \<in> Q")
    2.99 - prefer 2 apply blast
   2.100 -apply (rule_tac x = "{z. z \<in> Q \<and> (z,y) \<in> r\<^sup>*}" in allE)
   2.101 - apply assumption
   2.102 -apply (erule_tac V = "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> P Q" for P in thin_rl)
   2.103 +  apply (rule iffI)
   2.104 +   apply (blast elim: wf_trancl [THEN wf_irrefl]
   2.105 +      intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN [2] rev_subsetD])
   2.106 +  apply (simp add: wf_eq_minimal)
   2.107 +  apply safe
   2.108 +  apply (rule allE)
   2.109 +   apply assumption
   2.110 +  apply (erule impE)
   2.111 +   apply blast
   2.112 +  apply (erule bexE)
   2.113 +  apply (rename_tac a, case_tac "a = x")
   2.114 +   prefer 2
   2.115 +   apply blast
   2.116 +  apply (case_tac "y \<in> Q")
   2.117 +   prefer 2
   2.118 +   apply blast
   2.119 +  apply (rule_tac x = "{z. z \<in> Q \<and> (z,y) \<in> r\<^sup>*}" in allE)
   2.120 +   apply assumption
   2.121 +  apply (erule_tac V = "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> P Q" for P in thin_rl)
   2.122    (*essential for speed*)
   2.123 -(*blast with new substOccur fails*)
   2.124 -apply (fast intro: converse_rtrancl_into_rtrancl)
   2.125 -done
   2.126 +  (*blast with new substOccur fails*)
   2.127 +  apply (fast intro: converse_rtrancl_into_rtrancl)
   2.128 +  done
   2.129  
   2.130  
   2.131  subsubsection \<open>Well-foundedness of image\<close>
   2.132  
   2.133  lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"
   2.134 -apply (simp only: wf_eq_minimal, clarify)
   2.135 -apply (case_tac "\<exists>p. f p \<in> Q")
   2.136 -apply (erule_tac x = "{p. f p \<in> Q}" in allE)
   2.137 -apply (fast dest: inj_onD, blast)
   2.138 -done
   2.139 +  apply (simp only: wf_eq_minimal)
   2.140 +  apply clarify
   2.141 +  apply (case_tac "\<exists>p. f p \<in> Q")
   2.142 +   apply (erule_tac x = "{p. f p \<in> Q}" in allE)
   2.143 +   apply (fast dest: inj_onD)
   2.144 +apply blast
   2.145 +  done
   2.146  
   2.147  
   2.148  subsection \<open>Well-Foundedness Results for Unions\<close>
   2.149 @@ -270,24 +275,21 @@
   2.150      by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast
   2.151    with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'"
   2.152      by (erule wfE_min)
   2.153 -  {
   2.154 -    fix y assume "(y, z) \<in> S"
   2.155 -    then have "y \<notin> ?Q'" by (rule zmin)
   2.156 -    have "y \<notin> Q"
   2.157 -    proof
   2.158 -      assume "y \<in> Q"
   2.159 -      with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
   2.160 -      from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI)
   2.161 -      with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" ..
   2.162 -      with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast
   2.163 -      with \<open>w \<in> Q\<close> show False by contradiction
   2.164 -    qed
   2.165 -  }
   2.166 +  have "y \<notin> Q" if "(y, z) \<in> S" for y
   2.167 +  proof
   2.168 +    from that have "y \<notin> ?Q'" by (rule zmin)
   2.169 +    assume "y \<in> Q"
   2.170 +    with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
   2.171 +    from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI)
   2.172 +    with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" ..
   2.173 +    with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast
   2.174 +    with \<open>w \<in> Q\<close> show False by contradiction
   2.175 +  qed
   2.176    with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
   2.177  qed
   2.178  
   2.179  
   2.180 -text \<open>Well-foundedness of indexed union with disjoint domains and ranges\<close>
   2.181 +text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close>
   2.182  
   2.183  lemma wf_UN:
   2.184    assumes "\<forall>i\<in>I. wf (r i)"
   2.185 @@ -306,10 +308,9 @@
   2.186    done
   2.187  
   2.188  lemma wfP_SUP:
   2.189 -  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPREMUM UNIV r)"
   2.190 -  apply (rule wf_UN[to_pred])
   2.191 -  apply simp_all
   2.192 -  done
   2.193 +  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow>
   2.194 +    wfP (SUPREMUM UNIV r)"
   2.195 +  by (rule wf_UN[to_pred]) simp_all
   2.196  
   2.197  lemma wf_Union:
   2.198    assumes "\<forall>r\<in>R. wf r"
   2.199 @@ -458,9 +459,7 @@
   2.200  subsection \<open>Acyclic relations\<close>
   2.201  
   2.202  lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r"
   2.203 -apply (simp add: acyclic_def)
   2.204 -apply (blast elim: wf_trancl [THEN wf_irrefl])
   2.205 -done
   2.206 +  by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl])
   2.207  
   2.208  lemmas wfP_acyclicP = wf_acyclic [to_pred]
   2.209  
   2.210 @@ -468,15 +467,15 @@
   2.211  subsubsection \<open>Wellfoundedness of finite acyclic relations\<close>
   2.212  
   2.213  lemma finite_acyclic_wf [rule_format]: "finite r \<Longrightarrow> acyclic r \<longrightarrow> wf r"
   2.214 -apply (erule finite_induct, blast)
   2.215 -apply (simp only: split_tupled_all)
   2.216 -apply simp
   2.217 -done
   2.218 +  apply (erule finite_induct)
   2.219 +   apply blast
   2.220 +  apply (simp add: split_tupled_all)
   2.221 +  done
   2.222  
   2.223  lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)"
   2.224 -apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   2.225 -apply (erule acyclic_converse [THEN iffD2])
   2.226 -done
   2.227 +  apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   2.228 +  apply (erule acyclic_converse [THEN iffD2])
   2.229 +  done
   2.230  
   2.231  text \<open>
   2.232    Observe that the converse of an irreflexive, transitive,
   2.233 @@ -488,12 +487,14 @@
   2.234    shows "wf (r\<inverse>)"
   2.235  proof -
   2.236    have "acyclic r"
   2.237 -    using \<open>irrefl r\<close> and \<open>trans r\<close> by (simp add: irrefl_def acyclic_irrefl)
   2.238 -  with \<open>finite r\<close> show ?thesis by (rule finite_acyclic_wf_converse)
   2.239 +    using \<open>irrefl r\<close> and \<open>trans r\<close>
   2.240 +    by (simp add: irrefl_def acyclic_irrefl)
   2.241 +  with \<open>finite r\<close> show ?thesis
   2.242 +    by (rule finite_acyclic_wf_converse)
   2.243  qed
   2.244  
   2.245  lemma wf_iff_acyclic_if_finite: "finite r \<Longrightarrow> wf r = acyclic r"
   2.246 -by (blast intro: finite_acyclic_wf wf_acyclic)
   2.247 +  by (blast intro: finite_acyclic_wf wf_acyclic)
   2.248  
   2.249  
   2.250  subsection \<open>@{typ nat} is well-founded\<close>
   2.251 @@ -528,8 +529,10 @@
   2.252    unfolding less_eq rtrancl_eq_or_trancl by auto
   2.253  
   2.254  lemma wf_pred_nat: "wf pred_nat"
   2.255 -  apply (unfold wf_def pred_nat_def, clarify)
   2.256 -  apply (induct_tac x, blast+)
   2.257 +  apply (unfold wf_def pred_nat_def)
   2.258 +  apply clarify
   2.259 +  apply (induct_tac x)
   2.260 +   apply blast+
   2.261    done
   2.262  
   2.263  lemma wf_less_than [iff]: "wf less_than"
   2.264 @@ -583,15 +586,13 @@
   2.265  lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]
   2.266  
   2.267  theorem accp_downward: "accp r b \<Longrightarrow> r a b \<Longrightarrow> accp r a"
   2.268 -  apply (erule accp.cases)
   2.269 -  apply fast
   2.270 -  done
   2.271 +  by (cases rule: accp.cases)
   2.272  
   2.273  lemma not_accp_down:
   2.274    assumes na: "\<not> accp R x"
   2.275    obtains z where "R z x" and "\<not> accp R z"
   2.276  proof -
   2.277 -  assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis"
   2.278 +  assume a: "\<And>z. R z x \<Longrightarrow> \<not> accp R z \<Longrightarrow> thesis"
   2.279    show thesis
   2.280    proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")
   2.281      case True
   2.282 @@ -612,12 +613,11 @@
   2.283    done
   2.284  
   2.285  theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b"
   2.286 -  apply (blast dest: accp_downwards_aux)
   2.287 -  done
   2.288 +  by (blast dest: accp_downwards_aux)
   2.289  
   2.290  theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
   2.291    apply (rule wfPUNIVI)
   2.292 -  apply (rule_tac P=P in accp_induct)
   2.293 +  apply (rule_tac P = P in accp_induct)
   2.294     apply blast
   2.295    apply blast
   2.296    done
   2.297 @@ -629,22 +629,22 @@
   2.298    done
   2.299  
   2.300  theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
   2.301 -  apply (blast intro: accp_wfPI dest: accp_wfPD)
   2.302 -  done
   2.303 +  by (blast intro: accp_wfPI dest: accp_wfPD)
   2.304  
   2.305  
   2.306  text \<open>Smaller relations have bigger accessible parts:\<close>
   2.307  
   2.308  lemma accp_subset:
   2.309 -  assumes sub: "R1 \<le> R2"
   2.310 +  assumes "R1 \<le> R2"
   2.311    shows "accp R2 \<le> accp R1"
   2.312  proof (rule predicate1I)
   2.313 -  fix x assume "accp R2 x"
   2.314 +  fix x
   2.315 +  assume "accp R2 x"
   2.316    then show "accp R1 x"
   2.317    proof (induct x)
   2.318      fix x
   2.319 -    assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y"
   2.320 -    with sub show "accp R1 x"
   2.321 +    assume "\<And>y. R2 y x \<Longrightarrow> accp R1 y"
   2.322 +    with assms show "accp R1 x"
   2.323        by (blast intro: accp.accI)
   2.324    qed
   2.325  qed
   2.326 @@ -655,9 +655,9 @@
   2.327  
   2.328  lemma accp_subset_induct:
   2.329    assumes subset: "D \<le> accp R"
   2.330 -    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
   2.331 +    and dcl: "\<And>x z. D x \<Longrightarrow> R z x \<Longrightarrow> D z"
   2.332      and "D x"
   2.333 -    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   2.334 +    and istep: "\<And>x. D x \<Longrightarrow> (\<And>z. R z x \<Longrightarrow> P z) \<Longrightarrow> P x"
   2.335    shows "P x"
   2.336  proof -
   2.337    from subset and \<open>D x\<close>
   2.338 @@ -665,8 +665,7 @@
   2.339    then show "P x" using \<open>D x\<close>
   2.340    proof (induct x)
   2.341      fix x
   2.342 -    assume "D x"
   2.343 -      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
   2.344 +    assume "D x" and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
   2.345      with dcl and istep show "P x" by blast
   2.346    qed
   2.347  qed
   2.348 @@ -691,15 +690,17 @@
   2.349  
   2.350  text \<open>Inverse Image\<close>
   2.351  
   2.352 -lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)" for f :: "'a \<Rightarrow> 'b"
   2.353 -apply (simp add: inv_image_def wf_eq_minimal)
   2.354 -apply clarify
   2.355 -apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}")
   2.356 -prefer 2 apply (blast del: allE)
   2.357 -apply (erule allE)
   2.358 -apply (erule (1) notE impE)
   2.359 -apply blast
   2.360 -done
   2.361 +lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)"
   2.362 + for f :: "'a \<Rightarrow> 'b"
   2.363 +  apply (simp add: inv_image_def wf_eq_minimal)
   2.364 +  apply clarify
   2.365 +  apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}")
   2.366 +   prefer 2
   2.367 +   apply (blast del: allE)
   2.368 +  apply (erule allE)
   2.369 +  apply (erule (1) notE impE)
   2.370 +  apply blast
   2.371 +  done
   2.372  
   2.373  text \<open>Measure functions into @{typ nat}\<close>
   2.374  
   2.375 @@ -710,17 +711,15 @@
   2.376    by (simp add:measure_def)
   2.377  
   2.378  lemma wf_measure [iff]: "wf (measure f)"
   2.379 -apply (unfold measure_def)
   2.380 -apply (rule wf_less_than [THEN wf_inv_image])
   2.381 -done
   2.382 +  unfolding measure_def by (rule wf_less_than [THEN wf_inv_image])
   2.383  
   2.384  lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}"
   2.385    for f :: "'a \<Rightarrow> nat"
   2.386 -apply(insert wf_measure[of f])
   2.387 -apply(simp only: measure_def inv_image_def less_than_def less_eq)
   2.388 -apply(erule wf_subset)
   2.389 -apply auto
   2.390 -done
   2.391 +  apply (insert wf_measure[of f])
   2.392 +  apply (simp only: measure_def inv_image_def less_than_def less_eq)
   2.393 +  apply (erule wf_subset)
   2.394 +  apply auto
   2.395 +  done
   2.396  
   2.397  
   2.398  subsubsection \<open>Lexicographic combinations\<close>
   2.399 @@ -730,13 +729,18 @@
   2.400    where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
   2.401  
   2.402  lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)"
   2.403 -apply (unfold wf_def lex_prod_def)
   2.404 -apply (rule allI, rule impI)
   2.405 -apply (simp only: split_paired_All)
   2.406 -apply (drule spec, erule mp)
   2.407 -apply (rule allI, rule impI)
   2.408 -apply (drule spec, erule mp, blast)
   2.409 -done
   2.410 +  apply (unfold wf_def lex_prod_def)
   2.411 +  apply (rule allI)
   2.412 +  apply (rule impI)
   2.413 +  apply (simp only: split_paired_All)
   2.414 +  apply (drule spec)
   2.415 +  apply (erule mp)
   2.416 +  apply (rule allI)
   2.417 +  apply (rule impI)
   2.418 +  apply (drule spec)
   2.419 +  apply (erule mp)
   2.420 +  apply blast
   2.421 +  done
   2.422  
   2.423  lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
   2.424    by (auto simp:lex_prod_def)
   2.425 @@ -752,19 +756,17 @@
   2.426    where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))"
   2.427  
   2.428  lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
   2.429 -  unfolding mlex_prod_def
   2.430 -  by auto
   2.431 +  by (auto simp: mlex_prod_def)
   2.432  
   2.433  lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   2.434 -  unfolding mlex_prod_def by simp
   2.435 +  by (simp add: mlex_prod_def)
   2.436  
   2.437  lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   2.438 -  unfolding mlex_prod_def by auto
   2.439 +  by (auto simp: mlex_prod_def)
   2.440  
   2.441 -text \<open>proper subset relation on finite sets\<close>
   2.442 -
   2.443 +text \<open>Proper subset relation on finite sets.\<close>
   2.444  definition finite_psubset :: "('a set \<times> 'a set) set"
   2.445 -  where "finite_psubset = {(A,B). A < B \<and> finite B}"
   2.446 +  where "finite_psubset = {(A, B). A \<subset> B \<and> finite B}"
   2.447  
   2.448  lemma wf_finite_psubset[simp]: "wf finite_psubset"
   2.449    apply (unfold finite_psubset_def)
   2.450 @@ -776,15 +778,15 @@
   2.451  lemma trans_finite_psubset: "trans finite_psubset"
   2.452    by (auto simp add: finite_psubset_def less_le trans_def)
   2.453  
   2.454 -lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A < B \<and> finite B"
   2.455 +lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A \<subset> B \<and> finite B"
   2.456    unfolding finite_psubset_def by auto
   2.457  
   2.458  text \<open>max- and min-extension of order to finite sets\<close>
   2.459  
   2.460  inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
   2.461    for R :: "('a \<times> 'a) set"
   2.462 -where
   2.463 -  max_extI[intro]: "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R"
   2.464 +  where max_extI[intro]:
   2.465 +    "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R"
   2.466  
   2.467  lemma max_ext_wf:
   2.468    assumes wf: "wf r"
   2.469 @@ -792,23 +794,24 @@
   2.470  proof (rule acc_wfI, intro allI)
   2.471    fix M
   2.472    show "M \<in> acc (max_ext r)" (is "_ \<in> ?W")
   2.473 -  proof cases
   2.474 -    assume "finite M"
   2.475 +  proof (cases "finite M")
   2.476 +    case True
   2.477      then show ?thesis
   2.478      proof (induct M)
   2.479 -      show "{} \<in> ?W"
   2.480 +      case empty
   2.481 +      show ?case
   2.482          by (rule accI) (auto elim: max_ext.cases)
   2.483      next
   2.484 -      fix M a assume "M \<in> ?W" "finite M"
   2.485 -      with wf show "insert a M \<in> ?W"
   2.486 +      case (insert a M)
   2.487 +      from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W"
   2.488        proof (induct arbitrary: M)
   2.489          fix M a
   2.490 -        assume "M \<in> ?W"  and  [intro]: "finite M"
   2.491 +        assume "M \<in> ?W"
   2.492 +        assume [intro]: "finite M"
   2.493          assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W"
   2.494 -        have add_less: "\<lbrakk>M \<in> ?W ; (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r)\<rbrakk> \<Longrightarrow> N \<union> M \<in> ?W"
   2.495 +        have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W"
   2.496            if "finite N" "finite M" for N M :: "'a set"
   2.497            using that by (induct N arbitrary: M) (auto simp: hyp)
   2.498 -
   2.499          show "insert a M \<in> ?W"
   2.500          proof (rule accI)
   2.501            fix N
   2.502 @@ -823,14 +826,13 @@
   2.503            then have finites: "finite ?N1" "finite ?N2" by auto
   2.504  
   2.505            have "?N2 \<in> ?W"
   2.506 -          proof cases
   2.507 -            assume [simp]: "M = {}"
   2.508 +          proof (cases "M = {}")
   2.509 +            case [simp]: True
   2.510              have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases)
   2.511 -
   2.512              from * have "?N2 = {}" by auto
   2.513              with Mw show "?N2 \<in> ?W" by (simp only:)
   2.514            next
   2.515 -            assume "M \<noteq> {}"
   2.516 +            case False
   2.517              from * finites have N2: "(?N2, M) \<in> max_ext r"
   2.518                by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
   2.519              with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
   2.520 @@ -842,15 +844,13 @@
   2.521        qed
   2.522      qed
   2.523    next
   2.524 -    assume [simp]: "\<not> finite M"
   2.525 +    case [simp]: False
   2.526      show ?thesis
   2.527        by (rule accI) (auto elim: max_ext.cases)
   2.528    qed
   2.529  qed
   2.530  
   2.531 -lemma max_ext_additive:
   2.532 -  "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
   2.533 -    (A \<union> C, B \<union> D) \<in> max_ext R"
   2.534 +lemma max_ext_additive: "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> (A \<union> C, B \<union> D) \<in> max_ext R"
   2.535    by (force elim!: max_ext.cases)
   2.536  
   2.537  
   2.538 @@ -874,13 +874,13 @@
   2.539      obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q"
   2.540        by (erule wfE_min)
   2.541      from z obtain m where "m \<in> Q" "z \<in> m" by auto
   2.542 -    from \<open>m \<in> Q\<close>
   2.543 -    show ?thesis
   2.544 -    proof (rule, intro bexI allI impI)
   2.545 +    from \<open>m \<in> Q\<close> show ?thesis
   2.546 +    proof (intro rev_bexI allI impI)
   2.547        fix n
   2.548        assume smaller: "(n, m) \<in> min_ext r"
   2.549 -      with \<open>z \<in> m\<close> obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def)
   2.550 -      then show "n \<notin> Q" using z(2) by auto
   2.551 +      with \<open>z \<in> m\<close> obtain y where "y \<in> n" "(y, z) \<in> r"
   2.552 +        by (auto simp: min_ext_def)
   2.553 +      with z(2) show "n \<notin> Q" by auto
   2.554      qed
   2.555    qed
   2.556  qed
   2.557 @@ -893,32 +893,33 @@
   2.558      and f :: "'a \<Rightarrow> nat"
   2.559    assumes "\<And>a b. (b, a) \<in> r \<Longrightarrow> ub b \<le> ub a \<and> ub a \<ge> f b \<and> f b > f a"
   2.560    shows "wf r"
   2.561 -  apply (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]])
   2.562 -  apply (auto dest: assms)
   2.563 -  done
   2.564 +  by (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]]) (auto dest: assms)
   2.565  
   2.566  lemma wf_bounded_set:
   2.567    fixes ub :: "'a \<Rightarrow> 'b set"
   2.568      and f :: "'a \<Rightarrow> 'b set"
   2.569    assumes "\<And>a b. (b,a) \<in> r \<Longrightarrow> finite (ub a) \<and> ub b \<subseteq> ub a \<and> ub a \<supseteq> f b \<and> f b \<supset> f a"
   2.570    shows "wf r"
   2.571 -  apply(rule wf_bounded_measure[of r "\<lambda>a. card(ub a)" "\<lambda>a. card(f a)"])
   2.572 -  apply(drule assms)
   2.573 +  apply (rule wf_bounded_measure[of r "\<lambda>a. card (ub a)" "\<lambda>a. card (f a)"])
   2.574 +  apply (drule assms)
   2.575    apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
   2.576    done
   2.577  
   2.578  lemma finite_subset_wf:
   2.579    assumes "finite A"
   2.580 -  shows   "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
   2.581 +  shows "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
   2.582  proof (intro finite_acyclic_wf)
   2.583 -  have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A" by blast
   2.584 +  have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A"
   2.585 +    by blast
   2.586    then show "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
   2.587      by (rule finite_subset) (auto simp: assms finite_cartesian_product)
   2.588  next
   2.589    have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}"
   2.590      by (intro trancl_id transI) blast
   2.591 -  also have " \<forall>x. (x, x) \<notin> \<dots>" by blast
   2.592 -  finally show "acyclic {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" by (rule acyclicI)
   2.593 +  also have " \<forall>x. (x, x) \<notin> \<dots>"
   2.594 +    by blast
   2.595 +  finally show "acyclic {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
   2.596 +    by (rule acyclicI)
   2.597  qed
   2.598  
   2.599  hide_const (open) acc accp
     3.1 --- a/src/HOL/Wfrec.thy	Sun Jul 31 19:09:21 2016 +0200
     3.2 +++ b/src/HOL/Wfrec.thy	Sun Jul 31 22:56:18 2016 +0200
     3.3 @@ -7,20 +7,20 @@
     3.4  section \<open>Well-Founded Recursion Combinator\<close>
     3.5  
     3.6  theory Wfrec
     3.7 -imports Wellfounded
     3.8 +  imports Wellfounded
     3.9  begin
    3.10  
    3.11 -inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F where
    3.12 -  wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
    3.13 +inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F
    3.14 +  where wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
    3.15  
    3.16 -definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b" where
    3.17 -  "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
    3.18 +definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
    3.19 +  where "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
    3.20  
    3.21 -definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool" where
    3.22 -  "adm_wf R F \<longleftrightarrow> (\<forall>f g x. (\<forall>z. (z, x) \<in> R \<longrightarrow> f z = g z) \<longrightarrow> F f x = F g x)"
    3.23 +definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool"
    3.24 +  where "adm_wf R F \<longleftrightarrow> (\<forall>f g x. (\<forall>z. (z, x) \<in> R \<longrightarrow> f z = g z) \<longrightarrow> F f x = F g x)"
    3.25  
    3.26 -definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)" where
    3.27 -  "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
    3.28 +definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)"
    3.29 +  where "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
    3.30  
    3.31  lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
    3.32    by (simp add: fun_eq_iff cut_def)
    3.33 @@ -28,13 +28,17 @@
    3.34  lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
    3.35    by (simp add: cut_def)
    3.36  
    3.37 -text\<open>Inductive characterization of wfrec combinator; for details see:
    3.38 -John Harrison, "Inductive definitions: automation and application"\<close>
    3.39 +text \<open>
    3.40 +  Inductive characterization of \<open>wfrec\<close> combinator; for details see:
    3.41 +  John Harrison, "Inductive definitions: automation and application".
    3.42 +\<close>
    3.43  
    3.44  lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
    3.45    by (auto intro: the_equality[symmetric] theI)
    3.46  
    3.47 -lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
    3.48 +lemma wfrec_unique:
    3.49 +  assumes "adm_wf R F" "wf R"
    3.50 +  shows "\<exists>!y. wfrec_rel R F x y"
    3.51    using \<open>wf R\<close>
    3.52  proof induct
    3.53    define f where "f y = (THE z. wfrec_rel R F y z)" for y
    3.54 @@ -46,44 +50,46 @@
    3.55  qed
    3.56  
    3.57  lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
    3.58 -  by (auto simp add: adm_wf_def
    3.59 -           intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
    3.60 +  by (auto simp: adm_wf_def intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
    3.61  
    3.62  lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
    3.63 -apply (simp add: wfrec_def)
    3.64 -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
    3.65 -apply (rule wfrec_rel.wfrecI)
    3.66 -apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    3.67 -done
    3.68 +  apply (simp add: wfrec_def)
    3.69 +  apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
    3.70 +   apply assumption
    3.71 +  apply (rule wfrec_rel.wfrecI)
    3.72 +  apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
    3.73 +  done
    3.74  
    3.75  
    3.76 -text\<open>* This form avoids giant explosions in proofs.  NOTE USE OF ==\<close>
    3.77 +text \<open>This form avoids giant explosions in proofs.  NOTE USE OF \<open>\<equiv>\<close>.\<close>
    3.78  lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
    3.79 - by (auto intro: wfrec)
    3.80 +  by (auto intro: wfrec)
    3.81  
    3.82  
    3.83  subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>
    3.84  
    3.85  lemma wfrec_fixpoint:
    3.86 -  assumes WF: "wf R" and ADM: "adm_wf R F"
    3.87 +  assumes wf: "wf R"
    3.88 +    and adm: "adm_wf R F"
    3.89    shows "wfrec R F = F (wfrec R F)"
    3.90  proof (rule ext)
    3.91    fix x
    3.92    have "wfrec R F x = F (cut (wfrec R F) R x) x"
    3.93 -    using wfrec[of R F] WF by simp
    3.94 +    using wfrec[of R F] wf by simp
    3.95    also
    3.96 -  { have "\<And> y. (y,x) \<in> R \<Longrightarrow> (cut (wfrec R F) R x) y = (wfrec R F) y"
    3.97 -      by (auto simp add: cut_apply)
    3.98 -    hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
    3.99 -      using ADM adm_wf_def[of R F] by auto }
   3.100 +  have "\<And>y. (y, x) \<in> R \<Longrightarrow> cut (wfrec R F) R x y = wfrec R F y"
   3.101 +    by (auto simp add: cut_apply)
   3.102 +  then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
   3.103 +    using adm adm_wf_def[of R F] by auto
   3.104    finally show "wfrec R F x = F (wfrec R F) x" .
   3.105  qed
   3.106  
   3.107 +
   3.108  subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
   3.109  
   3.110 -definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
   3.111 -  "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
   3.112 -   \<comment>\<open>For @{const wfrec} declarations where the first n parameters
   3.113 +definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
   3.114 +  where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
   3.115 +   \<comment> \<open>For @{const wfrec} declarations where the first n parameters
   3.116         stay unchanged in the recursive call.\<close>
   3.117  
   3.118  lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
   3.119 @@ -92,12 +98,13 @@
   3.120  lemma wf_same_fst:
   3.121    assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
   3.122    shows "wf (same_fst P R)"
   3.123 -apply (simp cong del: imp_cong add: wf_def same_fst_def)
   3.124 -apply (intro strip)
   3.125 -apply (rename_tac a b)
   3.126 -apply (case_tac "wf (R a)")
   3.127 - apply (erule_tac a = b in wf_induct, blast)
   3.128 -apply (blast intro: prem)
   3.129 -done
   3.130 +  apply (simp cong del: imp_cong add: wf_def same_fst_def)
   3.131 +  apply (intro strip)
   3.132 +  apply (rename_tac a b)
   3.133 +  apply (case_tac "wf (R a)")
   3.134 +   apply (erule_tac a = b in wf_induct)
   3.135 +   apply blast
   3.136 +  apply (blast intro: prem)
   3.137 +  done
   3.138  
   3.139  end
     4.1 --- a/src/HOL/Zorn.thy	Sun Jul 31 19:09:21 2016 +0200
     4.2 +++ b/src/HOL/Zorn.thy	Sun Jul 31 22:56:18 2016 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4 -(*  Title:      HOL/Zorn.thy
     4.5 -    Author:     Jacques D. Fleuriot
     4.6 -    Author:     Tobias Nipkow, TUM
     4.7 -    Author:     Christian Sternagel, JAIST
     4.8 +(*  Title:       HOL/Zorn.thy
     4.9 +    Author:      Jacques D. Fleuriot
    4.10 +    Author:      Tobias Nipkow, TUM
    4.11 +    Author:      Christian Sternagel, JAIST
    4.12  
    4.13  Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
    4.14  The well-ordering theorem.
    4.15 @@ -10,7 +10,7 @@
    4.16  section \<open>Zorn's Lemma\<close>
    4.17  
    4.18  theory Zorn
    4.19 -imports Order_Relation Hilbert_Choice
    4.20 +  imports Order_Relation Hilbert_Choice
    4.21  begin
    4.22  
    4.23  subsection \<open>Zorn's Lemma for the Subset Relation\<close>
    4.24 @@ -20,36 +20,38 @@
    4.25  text \<open>Let \<open>P\<close> be a binary predicate on the set \<open>A\<close>.\<close>
    4.26  locale pred_on =
    4.27    fixes A :: "'a set"
    4.28 -    and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
    4.29 +    and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
    4.30  begin
    4.31  
    4.32 -abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) where
    4.33 -  "x \<sqsubseteq> y \<equiv> P\<^sup>=\<^sup>= x y"
    4.34 +abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
    4.35 +  where "x \<sqsubseteq> y \<equiv> P\<^sup>=\<^sup>= x y"
    4.36 +
    4.37 +text \<open>A chain is a totally ordered subset of \<open>A\<close>.\<close>
    4.38 +definition chain :: "'a set \<Rightarrow> bool"
    4.39 +  where "chain C \<longleftrightarrow> C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
    4.40  
    4.41 -text \<open>A chain is a totally ordered subset of @{term A}.\<close>
    4.42 -definition chain :: "'a set \<Rightarrow> bool" where
    4.43 -  "chain C \<longleftrightarrow> C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
    4.44 -
    4.45 -text \<open>We call a chain that is a proper superset of some set @{term X},
    4.46 -but not necessarily a chain itself, a superchain of @{term X}.\<close>
    4.47 -abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "<c" 50) where
    4.48 -  "X <c C \<equiv> chain C \<and> X \<subset> C"
    4.49 +text \<open>
    4.50 +  We call a chain that is a proper superset of some set \<open>X\<close>,
    4.51 +  but not necessarily a chain itself, a superchain of \<open>X\<close>.
    4.52 +\<close>
    4.53 +abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"  (infix "<c" 50)
    4.54 +  where "X <c C \<equiv> chain C \<and> X \<subset> C"
    4.55  
    4.56  text \<open>A maximal chain is a chain that does not have a superchain.\<close>
    4.57 -definition maxchain :: "'a set \<Rightarrow> bool" where
    4.58 -  "maxchain C \<longleftrightarrow> chain C \<and> \<not> (\<exists>S. C <c S)"
    4.59 +definition maxchain :: "'a set \<Rightarrow> bool"
    4.60 +  where "maxchain C \<longleftrightarrow> chain C \<and> (\<nexists>S. C <c S)"
    4.61  
    4.62 -text \<open>We define the successor of a set to be an arbitrary
    4.63 -superchain, if such exists, or the set itself, otherwise.\<close>
    4.64 -definition suc :: "'a set \<Rightarrow> 'a set" where
    4.65 -  "suc C = (if \<not> chain C \<or> maxchain C then C else (SOME D. C <c D))"
    4.66 +text \<open>
    4.67 +  We define the successor of a set to be an arbitrary
    4.68 +  superchain, if such exists, or the set itself, otherwise.
    4.69 +\<close>
    4.70 +definition suc :: "'a set \<Rightarrow> 'a set"
    4.71 +  where "suc C = (if \<not> chain C \<or> maxchain C then C else (SOME D. C <c D))"
    4.72  
    4.73 -lemma chainI [Pure.intro?]:
    4.74 -  "\<lbrakk>C \<subseteq> A; \<And>x y. \<lbrakk>x \<in> C; y \<in> C\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> chain C"
    4.75 +lemma chainI [Pure.intro?]: "C \<subseteq> A \<Longrightarrow> (\<And>x y. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x) \<Longrightarrow> chain C"
    4.76    unfolding chain_def by blast
    4.77  
    4.78 -lemma chain_total:
    4.79 -  "chain C \<Longrightarrow> x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
    4.80 +lemma chain_total: "chain C \<Longrightarrow> x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
    4.81    by (simp add: chain_def)
    4.82  
    4.83  lemma not_chain_suc [simp]: "\<not> chain X \<Longrightarrow> suc X = X"
    4.84 @@ -64,62 +66,67 @@
    4.85  lemma chain_empty [simp]: "chain {}"
    4.86    by (auto simp: chain_def)
    4.87  
    4.88 -lemma not_maxchain_Some:
    4.89 -  "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> C <c (SOME D. C <c D)"
    4.90 +lemma not_maxchain_Some: "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> C <c (SOME D. C <c D)"
    4.91    by (rule someI_ex) (auto simp: maxchain_def)
    4.92  
    4.93 -lemma suc_not_equals:
    4.94 -  "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
    4.95 +lemma suc_not_equals: "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
    4.96    using not_maxchain_Some by (auto simp: suc_def)
    4.97  
    4.98  lemma subset_suc:
    4.99 -  assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y"
   4.100 +  assumes "X \<subseteq> Y"
   4.101 +  shows "X \<subseteq> suc Y"
   4.102    using assms by (rule subset_trans) (rule suc_subset)
   4.103  
   4.104 -text \<open>We build a set @{term \<C>} that is closed under applications
   4.105 -of @{term suc} and contains the union of all its subsets.\<close>
   4.106 -inductive_set suc_Union_closed ("\<C>") where
   4.107 -  suc: "X \<in> \<C> \<Longrightarrow> suc X \<in> \<C>" |
   4.108 -  Union [unfolded Pow_iff]: "X \<in> Pow \<C> \<Longrightarrow> \<Union>X \<in> \<C>"
   4.109 -
   4.110 -text \<open>Since the empty set as well as the set itself is a subset of
   4.111 -every set, @{term \<C>} contains at least @{term "{} \<in> \<C>"} and
   4.112 -@{term "\<Union>\<C> \<in> \<C>"}.\<close>
   4.113 -lemma
   4.114 -  suc_Union_closed_empty: "{} \<in> \<C>" and
   4.115 -  suc_Union_closed_Union: "\<Union>\<C> \<in> \<C>"
   4.116 -  using Union [of "{}"] and Union [of "\<C>"] by simp+
   4.117 -text \<open>Thus closure under @{term suc} will hit a maximal chain
   4.118 -eventually, as is shown below.\<close>
   4.119 +text \<open>
   4.120 +  We build a set @{term \<C>} that is closed under applications
   4.121 +  of @{term suc} and contains the union of all its subsets.
   4.122 +\<close>
   4.123 +inductive_set suc_Union_closed ("\<C>")
   4.124 +  where
   4.125 +    suc: "X \<in> \<C> \<Longrightarrow> suc X \<in> \<C>"
   4.126 +  | Union [unfolded Pow_iff]: "X \<in> Pow \<C> \<Longrightarrow> \<Union>X \<in> \<C>"
   4.127  
   4.128 -lemma suc_Union_closed_induct [consumes 1, case_names suc Union,
   4.129 -  induct pred: suc_Union_closed]:
   4.130 -  assumes "X \<in> \<C>"
   4.131 -    and "\<And>X. \<lbrakk>X \<in> \<C>; Q X\<rbrakk> \<Longrightarrow> Q (suc X)"
   4.132 -    and "\<And>X. \<lbrakk>X \<subseteq> \<C>; \<forall>x\<in>X. Q x\<rbrakk> \<Longrightarrow> Q (\<Union>X)"
   4.133 -  shows "Q X"
   4.134 -  using assms by (induct) blast+
   4.135 +text \<open>
   4.136 +  Since the empty set as well as the set itself is a subset of
   4.137 +  every set, @{term \<C>} contains at least @{term "{} \<in> \<C>"} and
   4.138 +  @{term "\<Union>\<C> \<in> \<C>"}.
   4.139 +\<close>
   4.140 +lemma suc_Union_closed_empty: "{} \<in> \<C>"
   4.141 +  and suc_Union_closed_Union: "\<Union>\<C> \<in> \<C>"
   4.142 +  using Union [of "{}"] and Union [of "\<C>"] by simp_all
   4.143 +
   4.144 +text \<open>Thus closure under @{term suc} will hit a maximal chain
   4.145 +  eventually, as is shown below.\<close>
   4.146  
   4.147 -lemma suc_Union_closed_cases [consumes 1, case_names suc Union,
   4.148 -  cases pred: suc_Union_closed]:
   4.149 +lemma suc_Union_closed_induct [consumes 1, case_names suc Union, induct pred: suc_Union_closed]:
   4.150    assumes "X \<in> \<C>"
   4.151 -    and "\<And>Y. \<lbrakk>X = suc Y; Y \<in> \<C>\<rbrakk> \<Longrightarrow> Q"
   4.152 -    and "\<And>Y. \<lbrakk>X = \<Union>Y; Y \<subseteq> \<C>\<rbrakk> \<Longrightarrow> Q"
   4.153 +    and "\<And>X. X \<in> \<C> \<Longrightarrow> Q X \<Longrightarrow> Q (suc X)"
   4.154 +    and "\<And>X. X \<subseteq> \<C> \<Longrightarrow> \<forall>x\<in>X. Q x \<Longrightarrow> Q (\<Union>X)"
   4.155 +  shows "Q X"
   4.156 +  using assms by induct blast+
   4.157 +
   4.158 +lemma suc_Union_closed_cases [consumes 1, case_names suc Union, cases pred: suc_Union_closed]:
   4.159 +  assumes "X \<in> \<C>"
   4.160 +    and "\<And>Y. X = suc Y \<Longrightarrow> Y \<in> \<C> \<Longrightarrow> Q"
   4.161 +    and "\<And>Y. X = \<Union>Y \<Longrightarrow> Y \<subseteq> \<C> \<Longrightarrow> Q"
   4.162    shows "Q"
   4.163 -  using assms by (cases) simp+
   4.164 +  using assms by cases simp_all
   4.165  
   4.166  text \<open>On chains, @{term suc} yields a chain.\<close>
   4.167  lemma chain_suc:
   4.168 -  assumes "chain X" shows "chain (suc X)"
   4.169 +  assumes "chain X"
   4.170 +  shows "chain (suc X)"
   4.171    using assms
   4.172 -  by (cases "\<not> chain X \<or> maxchain X")
   4.173 -     (force simp: suc_def dest: not_maxchain_Some)+
   4.174 +  by (cases "\<not> chain X \<or> maxchain X") (force simp: suc_def dest: not_maxchain_Some)+
   4.175  
   4.176  lemma chain_sucD:
   4.177 -  assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)"
   4.178 +  assumes "chain X"
   4.179 +  shows "suc X \<subseteq> A \<and> chain (suc X)"
   4.180  proof -
   4.181 -  from \<open>chain X\<close> have *: "chain (suc X)" by (rule chain_suc)
   4.182 -  then have "suc X \<subseteq> A" unfolding chain_def by blast
   4.183 +  from \<open>chain X\<close> have *: "chain (suc X)"
   4.184 +    by (rule chain_suc)
   4.185 +  then have "suc X \<subseteq> A"
   4.186 +    unfolding chain_def by blast
   4.187    with * show ?thesis by blast
   4.188  qed
   4.189  
   4.190 @@ -128,27 +135,31 @@
   4.191      and *: "\<And>Z. Z \<in> \<C> \<Longrightarrow> Z \<subseteq> Y \<Longrightarrow> Z = Y \<or> suc Z \<subseteq> Y"
   4.192    shows "X \<subseteq> Y \<or> suc Y \<subseteq> X"
   4.193    using \<open>X \<in> \<C>\<close>
   4.194 -proof (induct)
   4.195 +proof induct
   4.196    case (suc X)
   4.197    with * show ?case by (blast del: subsetI intro: subset_suc)
   4.198 -qed blast
   4.199 +next
   4.200 +  case Union
   4.201 +  then show ?case by blast
   4.202 +qed
   4.203  
   4.204  lemma suc_Union_closed_subsetD:
   4.205    assumes "Y \<subseteq> X" and "X \<in> \<C>" and "Y \<in> \<C>"
   4.206    shows "X = Y \<or> suc Y \<subseteq> X"
   4.207 -  using assms(2-, 1)
   4.208 +  using assms(2,3,1)
   4.209  proof (induct arbitrary: Y)
   4.210    case (suc X)
   4.211 -  note * = \<open>\<And>Y. \<lbrakk>Y \<in> \<C>; Y \<subseteq> X\<rbrakk> \<Longrightarrow> X = Y \<or> suc Y \<subseteq> X\<close>
   4.212 +  note * = \<open>\<And>Y. Y \<in> \<C> \<Longrightarrow> Y \<subseteq> X \<Longrightarrow> X = Y \<or> suc Y \<subseteq> X\<close>
   4.213    with suc_Union_closed_total' [OF \<open>Y \<in> \<C>\<close> \<open>X \<in> \<C>\<close>]
   4.214 -    have "Y \<subseteq> X \<or> suc X \<subseteq> Y" by blast
   4.215 +  have "Y \<subseteq> X \<or> suc X \<subseteq> Y" by blast
   4.216    then show ?case
   4.217    proof
   4.218      assume "Y \<subseteq> X"
   4.219      with * and \<open>Y \<in> \<C>\<close> have "X = Y \<or> suc Y \<subseteq> X" by blast
   4.220      then show ?thesis
   4.221      proof
   4.222 -      assume "X = Y" then show ?thesis by simp
   4.223 +      assume "X = Y"
   4.224 +      then show ?thesis by simp
   4.225      next
   4.226        assume "suc Y \<subseteq> X"
   4.227        then have "suc Y \<subseteq> suc X" by (rule subset_suc)
   4.228 @@ -164,21 +175,22 @@
   4.229    proof (rule ccontr)
   4.230      assume "\<not> ?thesis"
   4.231      with \<open>Y \<subseteq> \<Union>X\<close> obtain x y z
   4.232 -    where "\<not> suc Y \<subseteq> \<Union>X"
   4.233 -      and "x \<in> X" and "y \<in> x" and "y \<notin> Y"
   4.234 -      and "z \<in> suc Y" and "\<forall>x\<in>X. z \<notin> x" by blast
   4.235 +      where "\<not> suc Y \<subseteq> \<Union>X"
   4.236 +        and "x \<in> X" and "y \<in> x" and "y \<notin> Y"
   4.237 +        and "z \<in> suc Y" and "\<forall>x\<in>X. z \<notin> x" by blast
   4.238      with \<open>X \<subseteq> \<C>\<close> have "x \<in> \<C>" by blast
   4.239 -    from Union and \<open>x \<in> X\<close>
   4.240 -      have *: "\<And>y. \<lbrakk>y \<in> \<C>; y \<subseteq> x\<rbrakk> \<Longrightarrow> x = y \<or> suc y \<subseteq> x" by blast
   4.241 -    with suc_Union_closed_total' [OF \<open>Y \<in> \<C>\<close> \<open>x \<in> \<C>\<close>]
   4.242 -      have "Y \<subseteq> x \<or> suc x \<subseteq> Y" by blast
   4.243 +    from Union and \<open>x \<in> X\<close> have *: "\<And>y. y \<in> \<C> \<Longrightarrow> y \<subseteq> x \<Longrightarrow> x = y \<or> suc y \<subseteq> x"
   4.244 +      by blast
   4.245 +    with suc_Union_closed_total' [OF \<open>Y \<in> \<C>\<close> \<open>x \<in> \<C>\<close>] have "Y \<subseteq> x \<or> suc x \<subseteq> Y"
   4.246 +      by blast
   4.247      then show False
   4.248      proof
   4.249        assume "Y \<subseteq> x"
   4.250        with * [OF \<open>Y \<in> \<C>\<close>] have "x = Y \<or> suc Y \<subseteq> x" by blast
   4.251        then show False
   4.252        proof
   4.253 -        assume "x = Y" with \<open>y \<in> x\<close> and \<open>y \<notin> Y\<close> show False by blast
   4.254 +        assume "x = Y"
   4.255 +        with \<open>y \<in> x\<close> and \<open>y \<notin> Y\<close> show False by blast
   4.256        next
   4.257          assume "suc Y \<subseteq> x"
   4.258          with \<open>x \<in> X\<close> have "suc Y \<subseteq> \<Union>X" by blast
   4.259 @@ -199,75 +211,87 @@
   4.260  proof (cases "\<forall>Z\<in>\<C>. Z \<subseteq> Y \<longrightarrow> Z = Y \<or> suc Z \<subseteq> Y")
   4.261    case True
   4.262    with suc_Union_closed_total' [OF assms]
   4.263 -    have "X \<subseteq> Y \<or> suc Y \<subseteq> X" by blast
   4.264 -  then show ?thesis using suc_subset [of Y] by blast
   4.265 +  have "X \<subseteq> Y \<or> suc Y \<subseteq> X" by blast
   4.266 +  with suc_subset [of Y] show ?thesis by blast
   4.267  next
   4.268    case False
   4.269 -  then obtain Z
   4.270 -    where "Z \<in> \<C>" and "Z \<subseteq> Y" and "Z \<noteq> Y" and "\<not> suc Z \<subseteq> Y" by blast
   4.271 -  with suc_Union_closed_subsetD and \<open>Y \<in> \<C>\<close> show ?thesis by blast
   4.272 +  then obtain Z where "Z \<in> \<C>" and "Z \<subseteq> Y" and "Z \<noteq> Y" and "\<not> suc Z \<subseteq> Y"
   4.273 +    by blast
   4.274 +  with suc_Union_closed_subsetD and \<open>Y \<in> \<C>\<close> show ?thesis
   4.275 +    by blast
   4.276  qed
   4.277  
   4.278  text \<open>Once we hit a fixed point w.r.t. @{term suc}, all other elements
   4.279 -of @{term \<C>} are subsets of this fixed point.\<close>
   4.280 +  of @{term \<C>} are subsets of this fixed point.\<close>
   4.281  lemma suc_Union_closed_suc:
   4.282    assumes "X \<in> \<C>" and "Y \<in> \<C>" and "suc Y = Y"
   4.283    shows "X \<subseteq> Y"
   4.284 -using \<open>X \<in> \<C>\<close>
   4.285 -proof (induct)
   4.286 +  using \<open>X \<in> \<C>\<close>
   4.287 +proof induct
   4.288    case (suc X)
   4.289 -  with \<open>Y \<in> \<C>\<close> and suc_Union_closed_subsetD
   4.290 -    have "X = Y \<or> suc X \<subseteq> Y" by blast
   4.291 -  then show ?case by (auto simp: \<open>suc Y = Y\<close>)
   4.292 -qed blast
   4.293 +  with \<open>Y \<in> \<C>\<close> and suc_Union_closed_subsetD have "X = Y \<or> suc X \<subseteq> Y"
   4.294 +    by blast
   4.295 +  then show ?case
   4.296 +    by (auto simp: \<open>suc Y = Y\<close>)
   4.297 +next
   4.298 +  case Union
   4.299 +  then show ?case by blast
   4.300 +qed
   4.301  
   4.302  lemma eq_suc_Union:
   4.303    assumes "X \<in> \<C>"
   4.304    shows "suc X = X \<longleftrightarrow> X = \<Union>\<C>"
   4.305 +    (is "?lhs \<longleftrightarrow> ?rhs")
   4.306  proof
   4.307 -  assume "suc X = X"
   4.308 -  with suc_Union_closed_suc [OF suc_Union_closed_Union \<open>X \<in> \<C>\<close>]
   4.309 -    have "\<Union>\<C> \<subseteq> X" .
   4.310 -  with \<open>X \<in> \<C>\<close> show "X = \<Union>\<C>" by blast
   4.311 +  assume ?lhs
   4.312 +  then have "\<Union>\<C> \<subseteq> X"
   4.313 +    by (rule suc_Union_closed_suc [OF suc_Union_closed_Union \<open>X \<in> \<C>\<close>])
   4.314 +  with \<open>X \<in> \<C>\<close> show ?rhs
   4.315 +    by blast
   4.316  next
   4.317    from \<open>X \<in> \<C>\<close> have "suc X \<in> \<C>" by (rule suc)
   4.318    then have "suc X \<subseteq> \<Union>\<C>" by blast
   4.319 -  moreover assume "X = \<Union>\<C>"
   4.320 +  moreover assume ?rhs
   4.321    ultimately have "suc X \<subseteq> X" by simp
   4.322    moreover have "X \<subseteq> suc X" by (rule suc_subset)
   4.323 -  ultimately show "suc X = X" ..
   4.324 +  ultimately show ?lhs ..
   4.325  qed
   4.326  
   4.327  lemma suc_in_carrier:
   4.328    assumes "X \<subseteq> A"
   4.329    shows "suc X \<subseteq> A"
   4.330    using assms
   4.331 -  by (cases "\<not> chain X \<or> maxchain X")
   4.332 -     (auto dest: chain_sucD)
   4.333 +  by (cases "\<not> chain X \<or> maxchain X") (auto dest: chain_sucD)
   4.334  
   4.335  lemma suc_Union_closed_in_carrier:
   4.336    assumes "X \<in> \<C>"
   4.337    shows "X \<subseteq> A"
   4.338    using assms
   4.339 -  by (induct) (auto dest: suc_in_carrier)
   4.340 +  by induct (auto dest: suc_in_carrier)
   4.341  
   4.342  text \<open>All elements of @{term \<C>} are chains.\<close>
   4.343  lemma suc_Union_closed_chain:
   4.344    assumes "X \<in> \<C>"
   4.345    shows "chain X"
   4.346 -using assms
   4.347 -proof (induct)
   4.348 -  case (suc X) then show ?case using not_maxchain_Some by (simp add: suc_def)
   4.349 +  using assms
   4.350 +proof induct
   4.351 +  case (suc X)
   4.352 +  then show ?case
   4.353 +    using not_maxchain_Some by (simp add: suc_def)
   4.354  next
   4.355    case (Union X)
   4.356 -  then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier)
   4.357 +  then have "\<Union>X \<subseteq> A"
   4.358 +    by (auto dest: suc_Union_closed_in_carrier)
   4.359    moreover have "\<forall>x\<in>\<Union>X. \<forall>y\<in>\<Union>X. x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   4.360    proof (intro ballI)
   4.361      fix x y
   4.362      assume "x \<in> \<Union>X" and "y \<in> \<Union>X"
   4.363 -    then obtain u v where "x \<in> u" and "u \<in> X" and "y \<in> v" and "v \<in> X" by blast
   4.364 -    with Union have "u \<in> \<C>" and "v \<in> \<C>" and "chain u" and "chain v" by blast+
   4.365 -    with suc_Union_closed_total have "u \<subseteq> v \<or> v \<subseteq> u" by blast
   4.366 +    then obtain u v where "x \<in> u" and "u \<in> X" and "y \<in> v" and "v \<in> X"
   4.367 +      by blast
   4.368 +    with Union have "u \<in> \<C>" and "v \<in> \<C>" and "chain u" and "chain v"
   4.369 +      by blast+
   4.370 +    with suc_Union_closed_total have "u \<subseteq> v \<or> v \<subseteq> u"
   4.371 +      by blast
   4.372      then show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   4.373      proof
   4.374        assume "u \<subseteq> v"
   4.375 @@ -290,18 +314,17 @@
   4.376  
   4.377  subsubsection \<open>Hausdorff's Maximum Principle\<close>
   4.378  
   4.379 -text \<open>There exists a maximal totally ordered subset of @{term A}. (Note that we do not
   4.380 -require @{term A} to be partially ordered.)\<close>
   4.381 +text \<open>There exists a maximal totally ordered subset of \<open>A\<close>. (Note that we do not
   4.382 +  require \<open>A\<close> to be partially ordered.)\<close>
   4.383  
   4.384  theorem Hausdorff: "\<exists>C. maxchain C"
   4.385  proof -
   4.386    let ?M = "\<Union>\<C>"
   4.387    have "maxchain ?M"
   4.388    proof (rule ccontr)
   4.389 -    assume "\<not> maxchain ?M"
   4.390 +    assume "\<not> ?thesis"
   4.391      then have "suc ?M \<noteq> ?M"
   4.392 -      using suc_not_equals and
   4.393 -      suc_Union_closed_chain [OF suc_Union_closed_Union] by simp
   4.394 +      using suc_not_equals and suc_Union_closed_chain [OF suc_Union_closed_Union] by simp
   4.395      moreover have "suc ?M = ?M"
   4.396        using eq_suc_Union [OF suc_Union_closed_Union] by simp
   4.397      ultimately show False by contradiction
   4.398 @@ -310,34 +333,35 @@
   4.399  qed
   4.400  
   4.401  text \<open>Make notation @{term \<C>} available again.\<close>
   4.402 -no_notation suc_Union_closed ("\<C>")
   4.403 +no_notation suc_Union_closed  ("\<C>")
   4.404  
   4.405 -lemma chain_extend:
   4.406 -  "chain C \<Longrightarrow> z \<in> A \<Longrightarrow> \<forall>x\<in>C. x \<sqsubseteq> z \<Longrightarrow> chain ({z} \<union> C)"
   4.407 +lemma chain_extend: "chain C \<Longrightarrow> z \<in> A \<Longrightarrow> \<forall>x\<in>C. x \<sqsubseteq> z \<Longrightarrow> chain ({z} \<union> C)"
   4.408    unfolding chain_def by blast
   4.409  
   4.410 -lemma maxchain_imp_chain:
   4.411 -  "maxchain C \<Longrightarrow> chain C"
   4.412 +lemma maxchain_imp_chain: "maxchain C \<Longrightarrow> chain C"
   4.413    by (simp add: maxchain_def)
   4.414  
   4.415  end
   4.416  
   4.417  text \<open>Hide constant @{const pred_on.suc_Union_closed}, which was just needed
   4.418 -for the proof of Hausforff's maximum principle.\<close>
   4.419 +  for the proof of Hausforff's maximum principle.\<close>
   4.420  hide_const pred_on.suc_Union_closed
   4.421  
   4.422  lemma chain_mono:
   4.423 -  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x y"
   4.424 +  assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   4.425      and "pred_on.chain A P C"
   4.426    shows "pred_on.chain A Q C"
   4.427    using assms unfolding pred_on.chain_def by blast
   4.428  
   4.429 +
   4.430  subsubsection \<open>Results for the proper subset relation\<close>
   4.431  
   4.432  interpretation subset: pred_on "A" "op \<subset>" for A .
   4.433  
   4.434  lemma subset_maxchain_max:
   4.435 -  assumes "subset.maxchain A C" and "X \<in> A" and "\<Union>C \<subseteq> X"
   4.436 +  assumes "subset.maxchain A C"
   4.437 +    and "X \<in> A"
   4.438 +    and "\<Union>C \<subseteq> X"
   4.439    shows "\<Union>C = X"
   4.440  proof (rule ccontr)
   4.441    let ?C = "{X} \<union> C"
   4.442 @@ -352,6 +376,7 @@
   4.443    ultimately show False using * by blast
   4.444  qed
   4.445  
   4.446 +
   4.447  subsubsection \<open>Zorn's lemma\<close>
   4.448  
   4.449  text \<open>If every chain has an upper bound, then there is a maximal set.\<close>
   4.450 @@ -360,19 +385,23 @@
   4.451    shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   4.452  proof -
   4.453    from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
   4.454 -  then have "subset.chain A M" by (rule subset.maxchain_imp_chain)
   4.455 -  with assms obtain Y where "Y \<in> A" and "\<forall>X\<in>M. X \<subseteq> Y" by blast
   4.456 +  then have "subset.chain A M"
   4.457 +    by (rule subset.maxchain_imp_chain)
   4.458 +  with assms obtain Y where "Y \<in> A" and "\<forall>X\<in>M. X \<subseteq> Y"
   4.459 +    by blast
   4.460    moreover have "\<forall>X\<in>A. Y \<subseteq> X \<longrightarrow> Y = X"
   4.461    proof (intro ballI impI)
   4.462      fix X
   4.463      assume "X \<in> A" and "Y \<subseteq> X"
   4.464      show "Y = X"
   4.465      proof (rule ccontr)
   4.466 -      assume "Y \<noteq> X"
   4.467 +      assume "\<not> ?thesis"
   4.468        with \<open>Y \<subseteq> X\<close> have "\<not> X \<subseteq> Y" by blast
   4.469        from subset.chain_extend [OF \<open>subset.chain A M\<close> \<open>X \<in> A\<close>] and \<open>\<forall>X\<in>M. X \<subseteq> Y\<close>
   4.470 -        have "subset.chain A ({X} \<union> M)" using \<open>Y \<subseteq> X\<close> by auto
   4.471 -      moreover have "M \<subset> {X} \<union> M" using \<open>\<forall>X\<in>M. X \<subseteq> Y\<close> and \<open>\<not> X \<subseteq> Y\<close> by auto
   4.472 +      have "subset.chain A ({X} \<union> M)"
   4.473 +        using \<open>Y \<subseteq> X\<close> by auto
   4.474 +      moreover have "M \<subset> {X} \<union> M"
   4.475 +        using \<open>\<forall>X\<in>M. X \<subseteq> Y\<close> and \<open>\<not> X \<subseteq> Y\<close> by auto
   4.476        ultimately show False
   4.477          using \<open>subset.maxchain A M\<close> by (auto simp: subset.maxchain_def)
   4.478      qed
   4.479 @@ -380,13 +409,14 @@
   4.480    ultimately show ?thesis by blast
   4.481  qed
   4.482  
   4.483 -text\<open>Alternative version of Zorn's lemma for the subset relation.\<close>
   4.484 +text \<open>Alternative version of Zorn's lemma for the subset relation.\<close>
   4.485  lemma subset_Zorn':
   4.486    assumes "\<And>C. subset.chain A C \<Longrightarrow> \<Union>C \<in> A"
   4.487    shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   4.488  proof -
   4.489    from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
   4.490 -  then have "subset.chain A M" by (rule subset.maxchain_imp_chain)
   4.491 +  then have "subset.chain A M"
   4.492 +    by (rule subset.maxchain_imp_chain)
   4.493    with assms have "\<Union>M \<in> A" .
   4.494    moreover have "\<forall>Z\<in>A. \<Union>M \<subseteq> Z \<longrightarrow> \<Union>M = Z"
   4.495    proof (intro ballI impI)
   4.496 @@ -403,19 +433,17 @@
   4.497  
   4.498  text \<open>Relate old to new definitions.\<close>
   4.499  
   4.500 -(* Define globally? In Set.thy? *)
   4.501 -definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^sub>\<subseteq>") where
   4.502 -  "chain\<^sub>\<subseteq> C \<longleftrightarrow> (\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A)"
   4.503 +definition chain_subset :: "'a set set \<Rightarrow> bool"  ("chain\<^sub>\<subseteq>")  (* Define globally? In Set.thy? *)
   4.504 +  where "chain\<^sub>\<subseteq> C \<longleftrightarrow> (\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A)"
   4.505  
   4.506 -definition chains :: "'a set set \<Rightarrow> 'a set set set" where
   4.507 -  "chains A = {C. C \<subseteq> A \<and> chain\<^sub>\<subseteq> C}"
   4.508 +definition chains :: "'a set set \<Rightarrow> 'a set set set"
   4.509 +  where "chains A = {C. C \<subseteq> A \<and> chain\<^sub>\<subseteq> C}"
   4.510  
   4.511 -(* Define globally? In Relation.thy? *)
   4.512 -definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set" where
   4.513 -  "Chains r = {C. \<forall>a\<in>C. \<forall>b\<in>C. (a, b) \<in> r \<or> (b, a) \<in> r}"
   4.514 +definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set"  (* Define globally? In Relation.thy? *)
   4.515 +  where "Chains r = {C. \<forall>a\<in>C. \<forall>b\<in>C. (a, b) \<in> r \<or> (b, a) \<in> r}"
   4.516  
   4.517 -lemma chains_extend:
   4.518 -  "[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"
   4.519 +lemma chains_extend: "c \<in> chains S \<Longrightarrow> z \<in> S \<Longrightarrow> \<forall>x \<in> c. x \<subseteq> z \<Longrightarrow> {z} \<union> c \<in> chains S"
   4.520 +  for z :: "'a set"
   4.521    unfolding chains_def chain_subset_def by blast
   4.522  
   4.523  lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
   4.524 @@ -427,8 +455,7 @@
   4.525  lemma chains_alt_def: "chains A = {C. subset.chain A C}"
   4.526    by (simp add: chains_def chain_subset_alt_def subset.chain_def)
   4.527  
   4.528 -lemma Chains_subset:
   4.529 -  "Chains r \<subseteq> {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
   4.530 +lemma Chains_subset: "Chains r \<subseteq> {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
   4.531    by (force simp add: Chains_def pred_on.chain_def)
   4.532  
   4.533  lemma Chains_subset':
   4.534 @@ -442,20 +469,18 @@
   4.535    shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
   4.536    using assms Chains_subset Chains_subset' by blast
   4.537  
   4.538 -lemma Zorn_Lemma:
   4.539 -  "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   4.540 +lemma Zorn_Lemma: "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   4.541    using subset_Zorn' [of A] by (force simp: chains_alt_def)
   4.542  
   4.543 -lemma Zorn_Lemma2:
   4.544 -  "\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   4.545 +lemma Zorn_Lemma2: "\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   4.546    using subset_Zorn [of A] by (auto simp: chains_alt_def)
   4.547  
   4.548 -text\<open>Various other lemmas\<close>
   4.549 +text \<open>Various other lemmas\<close>
   4.550  
   4.551 -lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
   4.552 +lemma chainsD: "c \<in> chains S \<Longrightarrow> x \<in> c \<Longrightarrow> y \<in> c \<Longrightarrow> x \<subseteq> y \<or> y \<subseteq> x"
   4.553    unfolding chains_def chain_subset_def by blast
   4.554  
   4.555 -lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"
   4.556 +lemma chainsD2: "c \<in> chains S \<Longrightarrow> c \<subseteq> S"
   4.557    unfolding chains_def by blast
   4.558  
   4.559  lemma Zorns_po_lemma:
   4.560 @@ -463,42 +488,49 @@
   4.561      and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r"
   4.562    shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
   4.563  proof -
   4.564 -  have "Preorder r" using po by (simp add: partial_order_on_def)
   4.565 -\<comment>\<open>Mirror r in the set of subsets below (wrt r) elements of A\<close>
   4.566 -  let ?B = "%x. r\<inverse> `` {x}" let ?S = "?B ` Field r"
   4.567 -  {
   4.568 -    fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
   4.569 +  have "Preorder r"
   4.570 +    using po by (simp add: partial_order_on_def)
   4.571 +  txt \<open>Mirror \<open>r\<close> in the set of subsets below (wrt \<open>r\<close>) elements of \<open>A\<close>.\<close>
   4.572 +  let ?B = "\<lambda>x. r\<inverse> `` {x}"
   4.573 +  let ?S = "?B ` Field r"
   4.574 +  have "\<exists>u\<in>Field r. \<forall>A\<in>C. A \<subseteq> r\<inverse> `` {u}"  (is "\<exists>u\<in>Field r. ?P u")
   4.575 +    if 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A" for C
   4.576 +  proof -
   4.577      let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}"
   4.578 -    have "C = ?B ` ?A" using 1 by (auto simp: image_def)
   4.579 +    from 1 have "C = ?B ` ?A" by (auto simp: image_def)
   4.580      have "?A \<in> Chains r"
   4.581      proof (simp add: Chains_def, intro allI impI, elim conjE)
   4.582        fix a b
   4.583        assume "a \<in> Field r" and "?B a \<in> C" and "b \<in> Field r" and "?B b \<in> C"
   4.584 -      hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto
   4.585 -      thus "(a, b) \<in> r \<or> (b, a) \<in> r"
   4.586 +      with 2 have "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" by auto
   4.587 +      then show "(a, b) \<in> r \<or> (b, a) \<in> r"
   4.588          using \<open>Preorder r\<close> and \<open>a \<in> Field r\<close> and \<open>b \<in> Field r\<close>
   4.589          by (simp add:subset_Image1_Image1_iff)
   4.590      qed
   4.591 -    then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" using u by auto
   4.592 -    have "\<forall>A\<in>C. A \<subseteq> r\<inverse> `` {u}" (is "?P u")
   4.593 +    with u obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" by auto
   4.594 +    have "?P u"
   4.595      proof auto
   4.596        fix a B assume aB: "B \<in> C" "a \<in> B"
   4.597        with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto
   4.598 -      thus "(a, u) \<in> r" using uA and aB and \<open>Preorder r\<close>
   4.599 +      then show "(a, u) \<in> r"
   4.600 +        using uA and aB and \<open>Preorder r\<close>
   4.601          unfolding preorder_on_def refl_on_def by simp (fast dest: transD)
   4.602      qed
   4.603 -    then have "\<exists>u\<in>Field r. ?P u" using \<open>u \<in> Field r\<close> by blast
   4.604 -  }
   4.605 +    then show ?thesis
   4.606 +      using \<open>u \<in> Field r\<close> by blast
   4.607 +  qed
   4.608    then have "\<forall>C\<in>chains ?S. \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
   4.609      by (auto simp: chains_def chain_subset_def)
   4.610 -  from Zorn_Lemma2 [OF this]
   4.611 -  obtain m B where "m \<in> Field r" and "B = r\<inverse> `` {m}"
   4.612 -    and "\<forall>x\<in>Field r. B \<subseteq> r\<inverse> `` {x} \<longrightarrow> r\<inverse> `` {x} = B"
   4.613 +  from Zorn_Lemma2 [OF this] obtain m B
   4.614 +    where "m \<in> Field r"
   4.615 +      and "B = r\<inverse> `` {m}"
   4.616 +      and "\<forall>x\<in>Field r. B \<subseteq> r\<inverse> `` {x} \<longrightarrow> r\<inverse> `` {x} = B"
   4.617      by auto
   4.618 -  hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
   4.619 +  then have "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
   4.620      using po and \<open>Preorder r\<close> and \<open>m \<in> Field r\<close>
   4.621      by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
   4.622 -  thus ?thesis using \<open>m \<in> Field r\<close> by blast
   4.623 +  then show ?thesis
   4.624 +    using \<open>m \<in> Field r\<close> by blast
   4.625  qed
   4.626  
   4.627  
   4.628 @@ -509,13 +541,12 @@
   4.629     Definition correct/most general?
   4.630     Naming?
   4.631  *)
   4.632 -definition init_seg_of :: "(('a \<times> 'a) set \<times> ('a \<times> 'a) set) set" where
   4.633 -  "init_seg_of = {(r, s). r \<subseteq> s \<and> (\<forall>a b c. (a, b) \<in> s \<and> (b, c) \<in> r \<longrightarrow> (a, b) \<in> r)}"
   4.634 +definition init_seg_of :: "(('a \<times> 'a) set \<times> ('a \<times> 'a) set) set"
   4.635 +  where "init_seg_of = {(r, s). r \<subseteq> s \<and> (\<forall>a b c. (a, b) \<in> s \<and> (b, c) \<in> r \<longrightarrow> (a, b) \<in> r)}"
   4.636  
   4.637 -abbreviation
   4.638 -  initialSegmentOf :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infix "initial'_segment'_of" 55)
   4.639 -where
   4.640 -  "r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of"
   4.641 +abbreviation initial_segment_of_syntax :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
   4.642 +    (infix "initial'_segment'_of" 55)
   4.643 +  where "r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of"
   4.644  
   4.645  lemma refl_on_init_seg_of [simp]: "r initial_segment_of r"
   4.646    by (simp add: init_seg_of_def)
   4.647 @@ -524,85 +555,97 @@
   4.648    "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t"
   4.649    by (simp (no_asm_use) add: init_seg_of_def) blast
   4.650  
   4.651 -lemma antisym_init_seg_of:
   4.652 -  "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s"
   4.653 +lemma antisym_init_seg_of: "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s"
   4.654    unfolding init_seg_of_def by safe
   4.655  
   4.656 -lemma Chains_init_seg_of_Union:
   4.657 -  "R \<in> Chains init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
   4.658 +lemma Chains_init_seg_of_Union: "R \<in> Chains init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
   4.659    by (auto simp: init_seg_of_def Ball_def Chains_def) blast
   4.660  
   4.661  lemma chain_subset_trans_Union:
   4.662    assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. trans r"
   4.663    shows "trans (\<Union>R)"
   4.664  proof (intro transI, elim UnionE)
   4.665 -  fix  S1 S2 :: "'a rel" and x y z :: 'a
   4.666 +  fix S1 S2 :: "'a rel" and x y z :: 'a
   4.667    assume "S1 \<in> R" "S2 \<in> R"
   4.668 -  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1" unfolding chain_subset_def by blast
   4.669 +  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1"
   4.670 +    unfolding chain_subset_def by blast
   4.671    moreover assume "(x, y) \<in> S1" "(y, z) \<in> S2"
   4.672 -  ultimately have "((x, y) \<in> S1 \<and> (y, z) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, z) \<in> S2)" by blast
   4.673 -  with \<open>S1 \<in> R\<close> \<open>S2 \<in> R\<close> assms(2) show "(x, z) \<in> \<Union>R" by (auto elim: transE)
   4.674 +  ultimately have "((x, y) \<in> S1 \<and> (y, z) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, z) \<in> S2)"
   4.675 +    by blast
   4.676 +  with \<open>S1 \<in> R\<close> \<open>S2 \<in> R\<close> assms(2) show "(x, z) \<in> \<Union>R"
   4.677 +    by (auto elim: transE)
   4.678  qed
   4.679  
   4.680  lemma chain_subset_antisym_Union:
   4.681    assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. antisym r"
   4.682    shows "antisym (\<Union>R)"
   4.683  proof (intro antisymI, elim UnionE)
   4.684 -  fix  S1 S2 :: "'a rel" and x y :: 'a
   4.685 +  fix S1 S2 :: "'a rel" and x y :: 'a
   4.686    assume "S1 \<in> R" "S2 \<in> R"
   4.687 -  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1" unfolding chain_subset_def by blast
   4.688 +  with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1"
   4.689 +    unfolding chain_subset_def by blast
   4.690    moreover assume "(x, y) \<in> S1" "(y, x) \<in> S2"
   4.691 -  ultimately have "((x, y) \<in> S1 \<and> (y, x) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, x) \<in> S2)" by blast
   4.692 -  with \<open>S1 \<in> R\<close> \<open>S2 \<in> R\<close> assms(2) show "x = y" unfolding antisym_def by auto
   4.693 +  ultimately have "((x, y) \<in> S1 \<and> (y, x) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, x) \<in> S2)"
   4.694 +    by blast
   4.695 +  with \<open>S1 \<in> R\<close> \<open>S2 \<in> R\<close> assms(2) show "x = y"
   4.696 +    unfolding antisym_def by auto
   4.697  qed
   4.698  
   4.699  lemma chain_subset_Total_Union:
   4.700    assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r"
   4.701    shows "Total (\<Union>R)"
   4.702  proof (simp add: total_on_def Ball_def, auto del: disjCI)
   4.703 -  fix r s a b assume A: "r \<in> R" "s \<in> R" "a \<in> Field r" "b \<in> Field s" "a \<noteq> b"
   4.704 +  fix r s a b
   4.705 +  assume A: "r \<in> R" "s \<in> R" "a \<in> Field r" "b \<in> Field s" "a \<noteq> b"
   4.706    from \<open>chain\<^sub>\<subseteq> R\<close> and \<open>r \<in> R\<close> and \<open>s \<in> R\<close> have "r \<subseteq> s \<or> s \<subseteq> r"
   4.707      by (auto simp add: chain_subset_def)
   4.708 -  thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)"
   4.709 +  then show "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)"
   4.710    proof
   4.711 -    assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A mono_Field[of r s]
   4.712 +    assume "r \<subseteq> s"
   4.713 +    then have "(a, b) \<in> s \<or> (b, a) \<in> s"
   4.714 +      using assms(2) A mono_Field[of r s]
   4.715        by (auto simp add: total_on_def)
   4.716 -    thus ?thesis using \<open>s \<in> R\<close> by blast
   4.717 +    then show ?thesis
   4.718 +      using \<open>s \<in> R\<close> by blast
   4.719    next
   4.720 -    assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A mono_Field[of s r]
   4.721 +    assume "s \<subseteq> r"
   4.722 +    then have "(a, b) \<in> r \<or> (b, a) \<in> r"
   4.723 +      using assms(2) A mono_Field[of s r]
   4.724        by (fastforce simp add: total_on_def)
   4.725 -    thus ?thesis using \<open>r \<in> R\<close> by blast
   4.726 +    then show ?thesis
   4.727 +      using \<open>r \<in> R\<close> by blast
   4.728    qed
   4.729  qed
   4.730  
   4.731  lemma wf_Union_wf_init_segs:
   4.732 -  assumes "R \<in> Chains init_seg_of" and "\<forall>r\<in>R. wf r"
   4.733 +  assumes "R \<in> Chains init_seg_of"
   4.734 +    and "\<forall>r\<in>R. wf r"
   4.735    shows "wf (\<Union>R)"
   4.736 -proof(simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto)
   4.737 -  fix f assume 1: "\<forall>i. \<exists>r\<in>R. (f (Suc i), f i) \<in> r"
   4.738 +proof (simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto)
   4.739 +  fix f
   4.740 +  assume 1: "\<forall>i. \<exists>r\<in>R. (f (Suc i), f i) \<in> r"
   4.741    then obtain r where "r \<in> R" and "(f (Suc 0), f 0) \<in> r" by auto
   4.742 -  { fix i have "(f (Suc i), f i) \<in> r"
   4.743 -    proof (induct i)
   4.744 -      case 0 show ?case by fact
   4.745 -    next
   4.746 -      case (Suc i)
   4.747 -      then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
   4.748 -        using 1 by auto
   4.749 -      then have "s initial_segment_of r \<or> r initial_segment_of s"
   4.750 -        using assms(1) \<open>r \<in> R\<close> by (simp add: Chains_def)
   4.751 -      with Suc s show ?case by (simp add: init_seg_of_def) blast
   4.752 -    qed
   4.753 -  }
   4.754 -  thus False using assms(2) and \<open>r \<in> R\<close>
   4.755 +  have "(f (Suc i), f i) \<in> r" for i
   4.756 +  proof (induct i)
   4.757 +    case 0
   4.758 +    show ?case by fact
   4.759 +  next
   4.760 +    case (Suc i)
   4.761 +    then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
   4.762 +      using 1 by auto
   4.763 +    then have "s initial_segment_of r \<or> r initial_segment_of s"
   4.764 +      using assms(1) \<open>r \<in> R\<close> by (simp add: Chains_def)
   4.765 +    with Suc s show ?case by (simp add: init_seg_of_def) blast
   4.766 +  qed
   4.767 +  then show False
   4.768 +    using assms(2) and \<open>r \<in> R\<close>
   4.769      by (simp add: wf_iff_no_infinite_down_chain) blast
   4.770  qed
   4.771  
   4.772 -lemma initial_segment_of_Diff:
   4.773 -  "p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s"
   4.774 +lemma initial_segment_of_Diff: "p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s"
   4.775    unfolding init_seg_of_def by blast
   4.776  
   4.777 -lemma Chains_inits_DiffI:
   4.778 -  "R \<in> Chains init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chains init_seg_of"
   4.779 +lemma Chains_inits_DiffI: "R \<in> Chains init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chains init_seg_of"
   4.780    unfolding Chains_def by (blast intro: initial_segment_of_Diff)
   4.781  
   4.782  theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV"
   4.783 @@ -610,24 +653,28 @@
   4.784  \<comment> \<open>The initial segment relation on well-orders:\<close>
   4.785    let ?WO = "{r::'a rel. Well_order r}"
   4.786    define I where "I = init_seg_of \<inter> ?WO \<times> ?WO"
   4.787 -  have I_init: "I \<subseteq> init_seg_of" by (auto simp: I_def)
   4.788 -  hence subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"
   4.789 +  then have I_init: "I \<subseteq> init_seg_of" by simp
   4.790 +  then have subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"
   4.791      unfolding init_seg_of_def chain_subset_def Chains_def by blast
   4.792    have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
   4.793      by (simp add: Chains_def I_def) blast
   4.794 -  have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def)
   4.795 -  hence 0: "Partial_order I"
   4.796 +  have FI: "Field I = ?WO"
   4.797 +    by (auto simp add: I_def init_seg_of_def Field_def)
   4.798 +  then have 0: "Partial_order I"
   4.799      by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
   4.800 -      trans_def I_def elim!: trans_init_seg_of)
   4.801 -\<comment> \<open>I-chains have upper bounds in ?WO wrt I: their Union\<close>
   4.802 -  { fix R assume "R \<in> Chains I"
   4.803 -    hence Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast
   4.804 -    have subch: "chain\<^sub>\<subseteq> R" using \<open>R : Chains I\<close> I_init
   4.805 -      by (auto simp: init_seg_of_def chain_subset_def Chains_def)
   4.806 +        trans_def I_def elim!: trans_init_seg_of)
   4.807 +\<comment> \<open>\<open>I\<close>-chains have upper bounds in \<open>?WO\<close> wrt \<open>I\<close>: their Union\<close>
   4.808 +  have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)" if "R \<in> Chains I" for R
   4.809 +  proof -
   4.810 +    from that have Ris: "R \<in> Chains init_seg_of"
   4.811 +      using mono_Chains [OF I_init] by blast
   4.812 +    have subch: "chain\<^sub>\<subseteq> R"
   4.813 +      using \<open>R : Chains I\<close> I_init by (auto simp: init_seg_of_def chain_subset_def Chains_def)
   4.814      have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r"
   4.815        and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)"
   4.816        using Chains_wo [OF \<open>R \<in> Chains I\<close>] by (simp_all add: order_on_defs)
   4.817 -    have "Refl (\<Union>R)" using \<open>\<forall>r\<in>R. Refl r\<close> unfolding refl_on_def by fastforce
   4.818 +    have "Refl (\<Union>R)"
   4.819 +      using \<open>\<forall>r\<in>R. Refl r\<close> unfolding refl_on_def by fastforce
   4.820      moreover have "trans (\<Union>R)"
   4.821        by (rule chain_subset_trans_Union [OF subch \<open>\<forall>r\<in>R. trans r\<close>])
   4.822      moreover have "antisym (\<Union>R)"
   4.823 @@ -640,21 +687,25 @@
   4.824        with \<open>\<forall>r\<in>R. wf (r - Id)\<close> and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
   4.825        show ?thesis by fastforce
   4.826      qed
   4.827 -    ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs)
   4.828 -    moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
   4.829 -      by(simp add: Chains_init_seg_of_Union)
   4.830 -    ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)"
   4.831 +    ultimately have "Well_order (\<Union>R)"
   4.832 +      by (simp add:order_on_defs)
   4.833 +    moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R"
   4.834 +      using Ris by (simp add: Chains_init_seg_of_Union)
   4.835 +    ultimately show ?thesis
   4.836        using mono_Chains [OF I_init] Chains_wo[of R] and \<open>R \<in> Chains I\<close>
   4.837        unfolding I_def by blast
   4.838 -  }
   4.839 -  hence 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
   4.840 -\<comment>\<open>Zorn's Lemma yields a maximal well-order m:\<close>
   4.841 -  then obtain m::"'a rel" where "Well_order m" and
   4.842 -    max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m"
   4.843 +  qed
   4.844 +  then have 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I"
   4.845 +    by (subst FI) blast
   4.846 +\<comment>\<open>Zorn's Lemma yields a maximal well-order \<open>m\<close>:\<close>
   4.847 +  then obtain m :: "'a rel"
   4.848 +    where "Well_order m"
   4.849 +      and max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m"
   4.850      using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce
   4.851 -\<comment>\<open>Now show by contradiction that m covers the whole type:\<close>
   4.852 -  { fix x::'a assume "x \<notin> Field m"
   4.853 -\<comment>\<open>We assume that x is not covered and extend m at the top with x\<close>
   4.854 +\<comment>\<open>Now show by contradiction that \<open>m\<close> covers the whole type:\<close>
   4.855 +  have False if "x \<notin> Field m" for x :: 'a
   4.856 +  proof -
   4.857 +\<comment>\<open>Assuming that \<open>x\<close> is not covered and extend \<open>m\<close> at the top with \<open>x\<close>\<close>
   4.858      have "m \<noteq> {}"
   4.859      proof
   4.860        assume "m = {}"
   4.861 @@ -663,10 +714,10 @@
   4.862        ultimately show False using max
   4.863          by (auto simp: I_def init_seg_of_def simp del: Field_insert)
   4.864      qed
   4.865 -    hence "Field m \<noteq> {}" by(auto simp:Field_def)
   4.866 -    moreover have "wf (m - Id)" using \<open>Well_order m\<close>
   4.867 -      by (simp add: well_order_on_def)
   4.868 -\<comment>\<open>The extension of m by x:\<close>
   4.869 +    then have "Field m \<noteq> {}" by (auto simp: Field_def)
   4.870 +    moreover have "wf (m - Id)"
   4.871 +      using \<open>Well_order m\<close> by (simp add: well_order_on_def)
   4.872 +\<comment>\<open>The extension of \<open>m\<close> by \<open>x\<close>:\<close>
   4.873      let ?s = "{(a, x) | a. a \<in> Field m}"
   4.874      let ?m = "insert (x, x) m \<union> ?s"
   4.875      have Fm: "Field ?m = insert x (Field m)"
   4.876 @@ -674,49 +725,58 @@
   4.877      have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
   4.878        using \<open>Well_order m\<close> by (simp_all add: order_on_defs)
   4.879  \<comment>\<open>We show that the extension is a well-order\<close>
   4.880 -    have "Refl ?m" using \<open>Refl m\<close> Fm unfolding refl_on_def by blast
   4.881 +    have "Refl ?m"
   4.882 +      using \<open>Refl m\<close> Fm unfolding refl_on_def by blast
   4.883      moreover have "trans ?m" using \<open>trans m\<close> and \<open>x \<notin> Field m\<close>
   4.884        unfolding trans_def Field_def by blast
   4.885 -    moreover have "antisym ?m" using \<open>antisym m\<close> and \<open>x \<notin> Field m\<close>
   4.886 -      unfolding antisym_def Field_def by blast
   4.887 -    moreover have "Total ?m" using \<open>Total m\<close> and Fm by (auto simp: total_on_def)
   4.888 +    moreover have "antisym ?m"
   4.889 +      using \<open>antisym m\<close> and \<open>x \<notin> Field m\<close> unfolding antisym_def Field_def by blast
   4.890 +    moreover have "Total ?m"
   4.891 +      using \<open>Total m\<close> and Fm by (auto simp: total_on_def)
   4.892      moreover have "wf (?m - Id)"
   4.893      proof -
   4.894 -      have "wf ?s" using \<open>x \<notin> Field m\<close> 
   4.895 -        by (auto simp: wf_eq_minimal Field_def Bex_def)
   4.896 -      thus ?thesis using \<open>wf (m - Id)\<close> and \<open>x \<notin> Field m\<close>
   4.897 -        wf_subset [OF \<open>wf ?s\<close> Diff_subset]
   4.898 +      have "wf ?s"
   4.899 +        using \<open>x \<notin> Field m\<close> by (auto simp: wf_eq_minimal Field_def Bex_def)
   4.900 +      then show ?thesis
   4.901 +        using \<open>wf (m - Id)\<close> and \<open>x \<notin> Field m\<close> wf_subset [OF \<open>wf ?s\<close> Diff_subset]
   4.902          by (auto simp: Un_Diff Field_def intro: wf_Un)
   4.903      qed
   4.904 -    ultimately have "Well_order ?m" by (simp add: order_on_defs)
   4.905 -\<comment>\<open>We show that the extension is above m\<close>
   4.906 -    moreover have "(m, ?m) \<in> I" using \<open>Well_order ?m\<close> and \<open>Well_order m\<close> and \<open>x \<notin> Field m\<close>
   4.907 +    ultimately have "Well_order ?m"
   4.908 +      by (simp add: order_on_defs)
   4.909 +\<comment>\<open>We show that the extension is above \<open>m\<close>\<close>
   4.910 +    moreover have "(m, ?m) \<in> I"
   4.911 +      using \<open>Well_order ?m\<close> and \<open>Well_order m\<close> and \<open>x \<notin> Field m\<close>
   4.912        by (fastforce simp: I_def init_seg_of_def Field_def)
   4.913      ultimately
   4.914 -\<comment>\<open>This contradicts maximality of m:\<close>
   4.915 -    have False using max and \<open>x \<notin> Field m\<close> unfolding Field_def by blast
   4.916 -  }
   4.917 -  hence "Field m = UNIV" by auto
   4.918 +\<comment>\<open>This contradicts maximality of \<open>m\<close>:\<close>
   4.919 +    show False
   4.920 +      using max and \<open>x \<notin> Field m\<close> unfolding Field_def by blast
   4.921 +  qed
   4.922 +  then have "Field m = UNIV" by auto
   4.923    with \<open>Well_order m\<close> show ?thesis by blast
   4.924  qed
   4.925  
   4.926  corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"
   4.927  proof -
   4.928 -  obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"
   4.929 +  obtain r :: "'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"
   4.930      using well_ordering [where 'a = "'a"] by blast
   4.931    let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
   4.932 -  have 1: "Field ?r = A" using wo univ
   4.933 -    by (fastforce simp: Field_def order_on_defs refl_on_def)
   4.934 -  have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)"
   4.935 -    using \<open>Well_order r\<close> by (simp_all add: order_on_defs)
   4.936 -  have "Refl ?r" using \<open>Refl r\<close> by (auto simp: refl_on_def 1 univ)
   4.937 -  moreover have "trans ?r" using \<open>trans r\<close>
   4.938 +  have 1: "Field ?r = A"
   4.939 +    using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def)
   4.940 +  from \<open>Well_order r\<close> have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
   4.941 +    by (simp_all add: order_on_defs)
   4.942 +  from \<open>Refl r\<close> have "Refl ?r"
   4.943 +    by (auto simp: refl_on_def 1 univ)
   4.944 +  moreover from \<open>trans r\<close> have "trans ?r"
   4.945      unfolding trans_def by blast
   4.946 -  moreover have "antisym ?r" using \<open>antisym r\<close>
   4.947 +  moreover from \<open>antisym r\<close> have "antisym ?r"
   4.948      unfolding antisym_def by blast
   4.949 -  moreover have "Total ?r" using \<open>Total r\<close> by (simp add:total_on_def 1 univ)
   4.950 -  moreover have "wf (?r - Id)" by (rule wf_subset [OF \<open>wf (r - Id)\<close>]) blast
   4.951 -  ultimately have "Well_order ?r" by (simp add: order_on_defs)
   4.952 +  moreover from \<open>Total r\<close> have "Total ?r"
   4.953 +    by (simp add:total_on_def 1 univ)
   4.954 +  moreover have "wf (?r - Id)"
   4.955 +    by (rule wf_subset [OF \<open>wf (r - Id)\<close>]) blast
   4.956 +  ultimately have "Well_order ?r"
   4.957 +    by (simp add: order_on_defs)
   4.958    with 1 show ?thesis by auto
   4.959  qed
   4.960  
   4.961 @@ -727,15 +787,16 @@
   4.962  
   4.963  lemma dependent_wf_choice:
   4.964    fixes P :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   4.965 -  assumes "wf R" and adm: "\<And>f g x r. (\<And>z. (z, x) \<in> R \<Longrightarrow> f z = g z) \<Longrightarrow> P f x r = P g x r"
   4.966 -  assumes P: "\<And>x f. (\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
   4.967 +  assumes "wf R"
   4.968 +    and adm: "\<And>f g x r. (\<And>z. (z, x) \<in> R \<Longrightarrow> f z = g z) \<Longrightarrow> P f x r = P g x r"
   4.969 +    and P: "\<And>x f. (\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
   4.970    shows "\<exists>f. \<forall>x. P f x (f x)"
   4.971  proof (intro exI allI)
   4.972 -  fix x 
   4.973 +  fix x
   4.974    define f where "f \<equiv> wfrec R (\<lambda>f x. SOME r. P f x r)"
   4.975    from \<open>wf R\<close> show "P f x (f x)"
   4.976    proof (induct x)
   4.977 -    fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)"
   4.978 +    case (less x)
   4.979      show "P f x (f x)"
   4.980      proof (subst (2) wfrec_def_adm[OF f_def \<open>wf R\<close>])
   4.981        show "adm_wf R (\<lambda>f x. SOME r. P f x r)"
   4.982 @@ -748,7 +809,7 @@
   4.983  
   4.984  lemma (in wellorder) dependent_wellorder_choice:
   4.985    assumes "\<And>r f g x. (\<And>y. y < x \<Longrightarrow> f y = g y) \<Longrightarrow> P f x r = P g x r"
   4.986 -  assumes P: "\<And>x f. (\<And>y. y < x \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
   4.987 +    and P: "\<And>x f. (\<And>y. y < x \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
   4.988    shows "\<exists>f. \<forall>x. P f x (f x)"
   4.989    using wf by (rule dependent_wf_choice) (auto intro!: assms)
   4.990