# HG changeset patch
# User hoelzl
# Date 1409832157 -7200
# Node ID db1381d811abfd89080783f122617ab9c199cf8b
# Parent  285fbec02fb01ef123ae8824cf342381f179567b
cleanup Wfrec; introduce dependent_wf/wellorder_choice

diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Library/Old_Recdef.thy
--- a/src/HOL/Library/Old_Recdef.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Library/Old_Recdef.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -20,6 +20,9 @@
 apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
 done
 
+lemma tfl_cut_def: "cut f r x \<equiv> (\<lambda>y. if (y,x) \<in> r then f y else undefined)"
+  unfolding cut_def .
+
 lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
 apply clarify
 apply (rule cut_apply, assumption)
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -200,7 +200,7 @@
 
   (* case class G x = None *)
 apply (simp (no_asm_simp) add: class_rec_def comp_subcls1
-  wfrec [where r="(subcls1 G)^-1", simplified])
+  wfrec [where R="(subcls1 G)^-1", simplified])
 apply (simp add: comp_class_None)
 
   (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -66,14 +66,8 @@
   assumes wf: "wf ((subcls1 G)^-1)"
     and cls: "class G C = Some (D, fs, ms)"
   shows "class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
-proof -
-  from wf have step: "\<And>H a. wfrec ((subcls1 G)\<inverse>) H a =
-    H (cut (wfrec ((subcls1 G)\<inverse>) H) ((subcls1 G)\<inverse>) a) a"
-    by (rule wfrec)
-  have cut: "\<And>f. C \<noteq> Object \<Longrightarrow> cut f ((subcls1 G)\<inverse>) C D = f D"
-    by (rule cut_apply [where r="(subcls1 G)^-1", simplified, OF subcls1I, OF cls])
-  from cls show ?thesis by (simp add: step cut class_rec_def)
-qed
+  by (subst wfrec_def_adm[OF class_rec_def])
+     (auto simp: assms adm_wf_def fun_eq_iff subcls1I split: option.split)
 
 definition
   "wf_class G = wf ((subcls1 G)^-1)"
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -3734,64 +3734,39 @@
   shows "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
   by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
 
-subsubsection{* Total boundedness *}
+subsubsection{* Totally bounded *}
 
 lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
   unfolding Cauchy_def by metis
 
-fun helper_1 :: "('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a"
-where
-  "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
-declare helper_1.simps[simp del]
-
 lemma seq_compact_imp_totally_bounded:
   assumes "seq_compact s"
-  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
-proof (rule, rule, rule ccontr)
-  fix e::real
-  assume "e > 0"
-  assume assm: "\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
-  def x \<equiv> "helper_1 s e"
-  {
-    fix n
-    have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
-    proof (induct n rule: nat_less_induct)
-      fix n
-      def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
-      assume as: "\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
-      have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
-        using assm
-        apply simp
-        apply (erule_tac x="x ` {0 ..< n}" in allE)
-        using as
-        apply auto
-        done
+  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
+proof -
+  { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
+    let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
+    have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
+    proof (rule dependent_wellorder_choice)
+      fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)"
+      then have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
+        using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
       then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
         unfolding subset_eq by auto
-      have "Q (x n)"
-        unfolding x_def and helper_1.simps[of s e n]
-        apply (rule someI2[where a=z])
-        unfolding x_def[symmetric] and Q_def
-        using z
-        apply auto
-        done
-      then show "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
-        unfolding Q_def by auto
-    qed
-  }
-  then have "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)"
-    by blast+
-  then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
-    using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
-  from this(3) have "Cauchy (x \<circ> r)"
-    using LIMSEQ_imp_Cauchy by auto
-  then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
-    unfolding cauchy_def using `e>0` by auto
-  show False
-    using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
-    using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]]
-    using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]]
-    by auto
+      show "\<exists>r. ?Q x n r"
+        using z by auto
+    qed simp
+    then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
+      by blast
+    then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
+      using assms by (metis seq_compact_def)
+    from this(3) have "Cauchy (x \<circ> r)"
+      using LIMSEQ_imp_Cauchy by auto
+    then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
+      unfolding cauchy_def using `e > 0` by blast
+    then have False
+      using x[of "r N" "r (N+1)"] r by (auto simp: subseq_def) }
+  then show ?thesis
+    by metis
 qed
 
 subsubsection{* Heine-Borel theorem *}
@@ -3802,7 +3777,7 @@
   shows "compact s"
 proof -
   from seq_compact_imp_totally_bounded[OF `seq_compact s`]
-  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` f e)"
+  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
     unfolding choice_iff' ..
   def K \<equiv> "(\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
   have "countably_compact s"
@@ -4137,7 +4112,7 @@
 qed
 
 lemma compact_eq_totally_bounded:
-  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
+  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
     (is "_ \<longleftrightarrow> ?rhs")
 proof
   assume assms: "?rhs"
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Order_Relation.thy
--- a/src/HOL/Order_Relation.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Order_Relation.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -319,27 +319,6 @@
 *}
 
 
-subsubsection {* Well-founded recursion via genuine fixpoints *}
-
-lemma wfrec_fixpoint:
-fixes r :: "('a * 'a) set" and
-      H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-assumes WF: "wf r" and ADM: "adm_wf r H"
-shows "wfrec r H = H (wfrec r H)"
-proof(rule ext)
-  fix x
-  have "wfrec r H x = H (cut (wfrec r H) r x) x"
-  using wfrec[of r H] WF by simp
-  also
-  {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
-   by (auto simp add: cut_apply)
-   hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
-   using ADM adm_wf_def[of r H] by auto
-  }
-  finally show "wfrec r H x = H (wfrec r H) x" .
-qed
-
-
 subsubsection {* Characterizations of well-foundedness *}
 
 text {* A transitive relation is well-founded iff it is ``locally'' well-founded,
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -184,70 +184,51 @@
 
       let ?q = "\<lambda>k n y. \<mu>G (?M (J k) (A n) y)"
 
-      have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
-      from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this
-
-      let ?P =
-        "\<lambda>k wk w. w \<in> space (Pi\<^sub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
-          (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
-      def w \<equiv> "rec_nat w0 (\<lambda>k wk. Eps (?P k wk))"
-
-      { fix k have w: "w k \<in> space (Pi\<^sub>M (J k) M) \<and>
-          (\<forall>n. ?a / 2 ^ (k + 1) \<le> ?q k n (w k)) \<and> (k \<noteq> 0 \<longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1))"
-        proof (induct k)
-          case 0 with w0 show ?case
-            unfolding w_def nat.rec(1) by auto
+      let ?P = "\<lambda>w k. w \<in> space (Pi\<^sub>M (J k) M) \<and> (\<forall>n. ?a / 2 ^ (Suc k) \<le> ?q k n w)"
+      have "\<exists>w. \<forall>k. ?P (w k) k \<and> restrict (w (Suc k)) (J k) = w k"
+      proof (rule dependent_nat_choice)
+        have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
+        from Ex_w[OF A(1,2) this J(1-3), of 0] show "\<exists>w. ?P w 0" by auto
+      next
+        fix w k assume Suc: "?P w k"
+        show "\<exists>w'. ?P w' (Suc k) \<and> restrict w' (J k) = w"
+        proof cases
+          assume [simp]: "J k = J (Suc k)"
+          have "?a / 2 ^ (Suc (Suc k)) \<le> ?a / 2 ^ (k + 1)"
+            using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: field_simps)
+          with Suc show ?thesis
+            by (auto intro!: exI[of _ w] simp: extensional_restrict space_PiM intro: order_trans)
         next
-          case (Suc k)
-          then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
-          have "\<exists>w'. ?P k (w k) w'"
-          proof cases
-            assume [simp]: "J k = J (Suc k)"
-            show ?thesis
-            proof (intro exI[of _ "w k"] conjI allI)
-              fix n
-              have "?a / 2 ^ (Suc k + 1) \<le> ?a / 2 ^ (k + 1)"
-                using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: field_simps)
-              also have "\<dots> \<le> ?q k n (w k)" using Suc by auto
-              finally show "?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n (w k)" by simp
-            next
-              show "w k \<in> space (Pi\<^sub>M (J (Suc k)) M)"
-                using Suc by simp
-              then show "restrict (w k) (J k) = w k"
-                by (simp add: extensional_restrict space_PiM)
-            qed
-          next
-            assume "J k \<noteq> J (Suc k)"
-            with J_mono[of k "Suc k"] have "J (Suc k) - J k \<noteq> {}" (is "?D \<noteq> {}") by auto
-            have "range (\<lambda>n. ?M (J k) (A n) (w k)) \<subseteq> ?G"
-              "decseq (\<lambda>n. ?M (J k) (A n) (w k))"
-              "\<forall>n. ?a / 2 ^ (k + 1) \<le> \<mu>G (?M (J k) (A n) (w k))"
-              using `decseq A` fold(4)[OF J(1-3) A_eq(2), of "w k" k] Suc
-              by (auto simp: decseq_def)
-            from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
-            obtain w' where w': "w' \<in> space (Pi\<^sub>M ?D M)"
-              "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) (w k)) w')" by auto
-            let ?w = "merge (J k) ?D (w k, w')"
-            have [simp]: "\<And>x. merge (J k) (I - J k) (w k, merge ?D (I - ?D) (w', x)) =
-              merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
-              using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
-              by (auto intro!: ext split: split_merge)
-            have *: "\<And>n. ?M ?D (?M (J k) (A n) (w k)) w' = ?M (J (Suc k)) (A n) ?w"
-              using w'(1) J(3)[of "Suc k"]
-              by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
-            show ?thesis
-              using w' J_mono[of k "Suc k"] wk unfolding *
-              by (intro exI[of _ ?w])
-                 (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
-          qed
-          then have "?P k (w k) (w (Suc k))"
-            unfolding w_def nat.rec(2) unfolding w_def[symmetric]
-            by (rule someI_ex)
-          then show ?case by auto
+          assume "J k \<noteq> J (Suc k)"
+          with J_mono[of k "Suc k"] have "J (Suc k) - J k \<noteq> {}" (is "?D \<noteq> {}") by auto
+          have "range (\<lambda>n. ?M (J k) (A n) w) \<subseteq> ?G" "decseq (\<lambda>n. ?M (J k) (A n) w)"
+            "\<forall>n. ?a / 2 ^ (k + 1) \<le> \<mu>G (?M (J k) (A n) w)"
+            using `decseq A` fold(4)[OF J(1-3) A_eq(2), of w k] Suc
+            by (auto simp: decseq_def)
+          from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
+          obtain w' where w': "w' \<in> space (Pi\<^sub>M ?D M)"
+            "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) w) w')" by auto
+          let ?w = "merge (J k) ?D (w, w')"
+          have [simp]: "\<And>x. merge (J k) (I - J k) (w, merge ?D (I - ?D) (w', x)) =
+            merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
+            using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
+            by (auto intro!: ext split: split_merge)
+          have *: "\<And>n. ?M ?D (?M (J k) (A n) w) w' = ?M (J (Suc k)) (A n) ?w"
+            using w'(1) J(3)[of "Suc k"]
+            by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
+          show ?thesis
+            using Suc w' J_mono[of k "Suc k"] unfolding *
+            by (intro exI[of _ ?w])
+               (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
         qed
-        moreover
-        from w have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
-        moreover
+      qed
+      then obtain w where w:
+        "\<And>k. w k \<in> space (Pi\<^sub>M (J k) M)"
+        "\<And>k n. ?a / 2 ^ (Suc k) \<le> ?q k n (w k)"
+        "\<And>k. restrict (w (Suc k)) (J k) = w k"
+        by metis
+
+      { fix k
         from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
         then have "?M (J k) (A k) (w k) \<noteq> {}"
           using positive_mu_G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
@@ -256,19 +237,15 @@
         then have "merge (J k) (I - J k) (w k, x) \<in> A k" by auto
         then have "\<exists>x\<in>A k. restrict x (J k) = w k"
           using `w k \<in> space (Pi\<^sub>M (J k) M)`
-          by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM)
-        ultimately have "w k \<in> space (Pi\<^sub>M (J k) M)"
-          "\<exists>x\<in>A k. restrict x (J k) = w k"
-          "k \<noteq> 0 \<Longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1)"
-          by auto }
-      note w = this
+          by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM) }
+      note w_ext = this
 
       { fix k l i assume "k \<le> l" "i \<in> J k"
         { fix l have "w k i = w (k + l) i"
           proof (induct l)
             case (Suc l)
             from `i \<in> J k` J_mono[of k "k + l"] have "i \<in> J (k + l)" by auto
-            with w(3)[of "k + Suc l"]
+            with w(3)[of "k + l"]
             have "w (k + l) i = w (k + Suc l) i"
               by (auto simp: restrict_def fun_eq_iff split: split_if_asm)
             with Suc show ?case by simp
@@ -297,7 +274,8 @@
       { fix n
         have "restrict w' (J n) = w n" using w(1)[of n]
           by (auto simp add: fun_eq_iff space_PiM)
-        with w[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)" by auto
+        with w_ext[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)"
+          by auto
         then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
       then have "w' \<in> (\<Inter>i. A i)" by auto
       with `(\<Inter>i. A i) = {}` show False by auto
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -233,42 +233,34 @@
 proof -
   interpret N: finite_measure N by fact
   let ?d = "\<lambda>A. measure M A - measure N A"
-  let ?P = "\<lambda>A B n. A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
-  let ?r = "\<lambda>S. restricted_space S"
-  { fix S n assume S: "S \<in> sets M"
-    then have "finite_measure (density M (indicator S))" "0 < 1 / real (Suc n)"
-         "finite_measure (density N (indicator S))" "sets (density N (indicator S)) = sets (density M (indicator S))"
+  let ?P = "\<lambda>A n. if n = 0 then A = space M else (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
+  let ?Q = "\<lambda>A B. A \<subseteq> B \<and> ?d B \<le> ?d A"
+
+  have "\<exists>A. \<forall>n. (A n \<in> sets M \<and> ?P (A n) n) \<and> ?Q (A (Suc n)) (A n)"
+  proof (rule dependent_nat_choice)
+    show "\<exists>A. A \<in> sets M \<and> ?P A 0"
+      by auto
+  next
+    fix A n assume "A \<in> sets M \<and> ?P A n"
+    then have A: "A \<in> sets M" by auto
+    then have "finite_measure (density M (indicator A))" "0 < 1 / real (Suc (Suc n))"
+         "finite_measure (density N (indicator A))" "sets (density N (indicator A)) = sets (density M (indicator A))"
       by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
     from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
-    with S have "?P (S \<inter> X) S n"
+    with A have "A \<inter> X \<in> sets M \<and> ?P (A \<inter> X) (Suc n) \<and> ?Q (A \<inter> X) A"
       by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
-    hence "\<exists>A. ?P A S n" .. }
-  note Ex_P = this
-  def A \<equiv> "rec_nat (space M) (\<lambda>n A. SOME B. ?P B A n)"
-  have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
-  have A_0[simp]: "A 0 = space M" unfolding A_def by simp
-  { fix i have "A i \<in> sets M" unfolding A_def
-    proof (induct i)
-      case (Suc i)
-      from Ex_P[OF this, of i] show ?case unfolding nat.rec(2)
-        by (rule someI2_ex) simp
-    qed simp }
-  note A_in_sets = this
-  { fix n have "?P (A (Suc n)) (A n) n"
-      using Ex_P[OF A_in_sets] unfolding A_Suc
-      by (rule someI2_ex) simp }
-  note P_A = this
-  have "range A \<subseteq> sets M" using A_in_sets by auto
-  have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp
-  have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc)
-  have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow> - 1 / real (Suc i) < ?d C"
-      using P_A by auto
+    then show "\<exists>B. (B \<in> sets M \<and> ?P B (Suc n)) \<and> ?Q B A"
+      by blast
+  qed
+  then obtain A where A: "\<And>n. A n \<in> sets M" "\<And>n. ?P (A n) n" "\<And>n. ?Q (A (Suc n)) (A n)"
+    by metis
+  then have mono_dA: "mono (\<lambda>i. ?d (A i))" and A_0[simp]: "A 0 = space M"
+    by (auto simp add: mono_iff_le_Suc)
   show ?thesis
   proof (safe intro!: bexI[of _ "\<Inter>i. A i"])
-    show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto
-    have A: "decseq A" using A_mono by (auto intro!: decseq_SucI)
-    from `range A \<subseteq> sets M`
-      finite_Lim_measure_decseq[OF _ A] N.finite_Lim_measure_decseq[OF _ A]
+    show "(\<Inter>i. A i) \<in> sets M" using `\<And>n. A n \<in> sets M` by auto
+    have "decseq A" using A by (auto intro!: decseq_SucI)
+    from A(1) finite_Lim_measure_decseq[OF _ this] N.finite_Lim_measure_decseq[OF _ this]
     have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: tendsto_diff simp: sets_eq)
     thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
       by (rule_tac LIMSEQ_le_const) auto
@@ -280,10 +272,11 @@
       hence "0 < - ?d B" by auto
       from ex_inverse_of_nat_Suc_less[OF this]
       obtain n where *: "?d B < - 1 / real (Suc n)"
-        by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
-      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
-      from epsilon[OF B(1) this] *
-      show False by auto
+        by (auto simp: real_eq_of_nat field_simps)
+      also have "\<dots> \<le> - 1 / real (Suc (Suc n))"
+        by (auto simp: field_simps)
+      finally show False
+        using * A(2)[of "Suc n"] B by (auto elim!: ballE[of _ _ B])
     qed
   qed
 qed
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Probability/Regularity.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -163,7 +163,7 @@
     by blast
   then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
     \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
-    apply atomize_elim unfolding bchoice_iff .
+    by metis
   hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
     \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
     unfolding Ball_def by blast
@@ -209,8 +209,8 @@
       from nat_approx_posE[OF this] guess n . note n = this
       let ?k = "from_nat_into X ` {0..k e (Suc n)}"
       have "finite ?k" by simp
-      moreover have "K \<subseteq> \<Union>((\<lambda>x. ball x e') ` ?k)" unfolding K_def B_def using n by force
-      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>((\<lambda>x. ball x e') ` k)" by blast
+      moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force
+      ultimately show "\<exists>k. finite k \<and> K \<subseteq> (\<Union>x\<in>k. ball x e')" by blast
     qed
     ultimately
     show "?thesis e " by (auto simp: sU)
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Tools/TFL/thms.ML
--- a/src/HOL/Tools/TFL/thms.ML	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Tools/TFL/thms.ML	Thu Sep 04 14:02:37 2014 +0200
@@ -7,7 +7,7 @@
 struct
   val WFREC_COROLLARY = @{thm tfl_wfrec};
   val WF_INDUCTION_THM = @{thm tfl_wf_induct};
-  val CUT_DEF = @{thm cut_def};
+  val CUT_DEF = @{thm tfl_cut_def};
   val eqT = @{thm tfl_eq_True};
   val rev_eq_mp = @{thm tfl_rev_eq_mp};
   val simp_thm = @{thm tfl_simp_thm};
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Wfrec.thy
--- a/src/HOL/Wfrec.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Wfrec.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -10,86 +10,88 @@
 imports Wellfounded
 begin
 
-inductive
-  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
-  for R :: "('a * 'a) set"
-  and F :: "('a => 'b) => 'a => 'b"
-where
-  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
-            wfrec_rel R F x (F g x)"
+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
+  wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
 
-definition
-  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
-  "cut f r x == (%y. if (y,x):r then f y else undefined)"
+definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b" where
+  "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
+
+definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool" 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)"
 
-definition
-  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
-  "adm_wf R F == ALL f g x.
-     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
+definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)" where
+  "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
 
-definition
-  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
-  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
+  by (simp add: fun_eq_iff cut_def)
 
-lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
-by (simp add: fun_eq_iff cut_def)
-
-lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
-by (simp add: cut_def)
+lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
+  by (simp add: cut_def)
 
 text{*Inductive characterization of wfrec combinator; for details see:
 John Harrison, "Inductive definitions: automation and application"*}
 
-lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
-apply (simp add: adm_wf_def)
-apply (erule_tac a=x in wf_induct)
-apply (rule ex1I)
-apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
-apply (fast dest!: theI')
-apply (erule wfrec_rel.cases, simp)
-apply (erule allE, erule allE, erule allE, erule mp)
-apply (blast intro: the_equality [symmetric])
-done
+lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
+  by (auto intro: the_equality[symmetric] theI)
 
-lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
-apply (simp add: adm_wf_def)
-apply (intro strip)
-apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
-apply (rule refl)
-done
+lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
+  using `wf R`
+proof induct
+  def f \<equiv> "\<lambda>y. THE z. wfrec_rel R F y z"
+  case (less x)
+  then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
+    unfolding f_def by (rule theI_unique)
+  with `adm_wf R F` show ?case
+    by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
+qed
 
-lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
+lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
+  by (auto simp add: adm_wf_def
+           intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
+
+lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
 apply (simp add: wfrec_def)
 apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
 apply (rule wfrec_rel.wfrecI)
-apply (intro strip)
 apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
 done
 
 
 text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
-lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
-apply auto
-apply (blast intro: wfrec)
-done
+lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
+ by (auto intro: wfrec)
+
+
+subsubsection {* Well-founded recursion via genuine fixpoints *}
 
+lemma wfrec_fixpoint:
+  assumes WF: "wf R" and ADM: "adm_wf R F"
+  shows "wfrec R F = F (wfrec R F)"
+proof (rule ext)
+  fix x
+  have "wfrec R F x = F (cut (wfrec R F) R x) x"
+    using wfrec[of R F] WF by simp
+  also
+  { have "\<And> y. (y,x) \<in> R \<Longrightarrow> (cut (wfrec R F) R x) y = (wfrec R F) y"
+      by (auto simp add: cut_apply)
+    hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
+      using ADM adm_wf_def[of R F] by auto }
+  finally show "wfrec R F x = F (wfrec R F) x" .
+qed
 
 subsection {* Wellfoundedness of @{text same_fst} *}
 
-definition
- same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
-where
-    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
-   --{*For @{text rec_def} declarations where the first n parameters
+definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
+  "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
+   --{*For @{const wfrec} declarations where the first n parameters
        stay unchanged in the recursive call. *}
 
-lemma same_fstI [intro!]:
-     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
-by (simp add: same_fst_def)
+lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
+  by (simp add: same_fst_def)
 
 lemma wf_same_fst:
-  assumes prem: "(!!x. P x ==> wf(R x))"
-  shows "wf(same_fst P R)"
+  assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
+  shows "wf (same_fst P R)"
 apply (simp cong del: imp_cong add: wf_def same_fst_def)
 apply (intro strip)
 apply (rename_tac a b)
diff -r 285fbec02fb0 -r db1381d811ab src/HOL/Zorn.thy
--- a/src/HOL/Zorn.thy	Thu Sep 04 11:53:39 2014 +0200
+++ b/src/HOL/Zorn.thy	Thu Sep 04 14:02:37 2014 +0200
@@ -720,4 +720,36 @@
   with 1 show ?thesis by auto
 qed
 
+(* Move this to Hilbert Choice and wfrec to Wellfounded*)
+
+lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
+  using wfrec_fixpoint by simp
+
+lemma dependent_wf_choice:
+  fixes P :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+  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"
+  assumes P: "\<And>x f. (\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
+  shows "\<exists>f. \<forall>x. P f x (f x)"
+proof (intro exI allI)
+  fix x 
+  def f \<equiv> "wfrec R (\<lambda>f x. SOME r. P f x r)"
+  from `wf R` show "P f x (f x)"
+  proof (induct x)
+    fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)"
+    show "P f x (f x)"
+    proof (subst (2) wfrec_def_adm[OF f_def `wf R`])
+      show "adm_wf R (\<lambda>f x. SOME r. P f x r)"
+        by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm)
+      show "P f x (Eps (P f x))"
+        using P by (rule someI_ex) fact
+    qed
+  qed
+qed
+
+lemma (in wellorder) dependent_wellorder_choice:
+  assumes "\<And>r f g x. (\<And>y. y < x \<Longrightarrow> f y = g y) \<Longrightarrow> P f x r = P g x r"
+  assumes P: "\<And>x f. (\<And>y. y < x \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
+  shows "\<exists>f. \<forall>x. P f x (f x)"
+  using wf by (rule dependent_wf_choice) (auto intro!: assms)
+
 end