cleanup Wfrec; introduce dependent_wf/wellorder_choice
authorhoelzl
Thu Sep 04 14:02:37 2014 +0200 (2014-09-04)
changeset 58184db1381d811ab
parent 58183 285fbec02fb0
child 58185 e6e3b20340be
cleanup Wfrec; introduce dependent_wf/wellorder_choice
src/HOL/Library/Old_Recdef.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Order_Relation.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Regularity.thy
src/HOL/Tools/TFL/thms.ML
src/HOL/Wfrec.thy
src/HOL/Zorn.thy
     1.1 --- a/src/HOL/Library/Old_Recdef.thy	Thu Sep 04 11:53:39 2014 +0200
     1.2 +++ b/src/HOL/Library/Old_Recdef.thy	Thu Sep 04 14:02:37 2014 +0200
     1.3 @@ -20,6 +20,9 @@
     1.4  apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
     1.5  done
     1.6  
     1.7 +lemma tfl_cut_def: "cut f r x \<equiv> (\<lambda>y. if (y,x) \<in> r then f y else undefined)"
     1.8 +  unfolding cut_def .
     1.9 +
    1.10  lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
    1.11  apply clarify
    1.12  apply (rule cut_apply, assumption)
     2.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Sep 04 11:53:39 2014 +0200
     2.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Sep 04 14:02:37 2014 +0200
     2.3 @@ -200,7 +200,7 @@
     2.4  
     2.5    (* case class G x = None *)
     2.6  apply (simp (no_asm_simp) add: class_rec_def comp_subcls1
     2.7 -  wfrec [where r="(subcls1 G)^-1", simplified])
     2.8 +  wfrec [where R="(subcls1 G)^-1", simplified])
     2.9  apply (simp add: comp_class_None)
    2.10  
    2.11    (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
     3.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Sep 04 11:53:39 2014 +0200
     3.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Sep 04 14:02:37 2014 +0200
     3.3 @@ -66,14 +66,8 @@
     3.4    assumes wf: "wf ((subcls1 G)^-1)"
     3.5      and cls: "class G C = Some (D, fs, ms)"
     3.6    shows "class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
     3.7 -proof -
     3.8 -  from wf have step: "\<And>H a. wfrec ((subcls1 G)\<inverse>) H a =
     3.9 -    H (cut (wfrec ((subcls1 G)\<inverse>) H) ((subcls1 G)\<inverse>) a) a"
    3.10 -    by (rule wfrec)
    3.11 -  have cut: "\<And>f. C \<noteq> Object \<Longrightarrow> cut f ((subcls1 G)\<inverse>) C D = f D"
    3.12 -    by (rule cut_apply [where r="(subcls1 G)^-1", simplified, OF subcls1I, OF cls])
    3.13 -  from cls show ?thesis by (simp add: step cut class_rec_def)
    3.14 -qed
    3.15 +  by (subst wfrec_def_adm[OF class_rec_def])
    3.16 +     (auto simp: assms adm_wf_def fun_eq_iff subcls1I split: option.split)
    3.17  
    3.18  definition
    3.19    "wf_class G = wf ((subcls1 G)^-1)"
     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 04 11:53:39 2014 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 04 14:02:37 2014 +0200
     4.3 @@ -3734,64 +3734,39 @@
     4.4    shows "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
     4.5    by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
     4.6  
     4.7 -subsubsection{* Total boundedness *}
     4.8 +subsubsection{* Totally bounded *}
     4.9  
    4.10  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)"
    4.11    unfolding Cauchy_def by metis
    4.12  
    4.13 -fun helper_1 :: "('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a"
    4.14 -where
    4.15 -  "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
    4.16 -declare helper_1.simps[simp del]
    4.17 -
    4.18  lemma seq_compact_imp_totally_bounded:
    4.19    assumes "seq_compact s"
    4.20 -  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
    4.21 -proof (rule, rule, rule ccontr)
    4.22 -  fix e::real
    4.23 -  assume "e > 0"
    4.24 -  assume assm: "\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
    4.25 -  def x \<equiv> "helper_1 s e"
    4.26 -  {
    4.27 -    fix n
    4.28 -    have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
    4.29 -    proof (induct n rule: nat_less_induct)
    4.30 -      fix n
    4.31 -      def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
    4.32 -      assume as: "\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
    4.33 -      have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
    4.34 -        using assm
    4.35 -        apply simp
    4.36 -        apply (erule_tac x="x ` {0 ..< n}" in allE)
    4.37 -        using as
    4.38 -        apply auto
    4.39 -        done
    4.40 +  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
    4.41 +proof -
    4.42 +  { 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)"
    4.43 +    let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
    4.44 +    have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
    4.45 +    proof (rule dependent_wellorder_choice)
    4.46 +      fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)"
    4.47 +      then have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
    4.48 +        using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
    4.49        then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
    4.50          unfolding subset_eq by auto
    4.51 -      have "Q (x n)"
    4.52 -        unfolding x_def and helper_1.simps[of s e n]
    4.53 -        apply (rule someI2[where a=z])
    4.54 -        unfolding x_def[symmetric] and Q_def
    4.55 -        using z
    4.56 -        apply auto
    4.57 -        done
    4.58 -      then show "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
    4.59 -        unfolding Q_def by auto
    4.60 -    qed
    4.61 -  }
    4.62 -  then have "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)"
    4.63 -    by blast+
    4.64 -  then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
    4.65 -    using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
    4.66 -  from this(3) have "Cauchy (x \<circ> r)"
    4.67 -    using LIMSEQ_imp_Cauchy by auto
    4.68 -  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"
    4.69 -    unfolding cauchy_def using `e>0` by auto
    4.70 -  show False
    4.71 -    using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
    4.72 -    using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]]
    4.73 -    using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]]
    4.74 -    by auto
    4.75 +      show "\<exists>r. ?Q x n r"
    4.76 +        using z by auto
    4.77 +    qed simp
    4.78 +    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)"
    4.79 +      by blast
    4.80 +    then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
    4.81 +      using assms by (metis seq_compact_def)
    4.82 +    from this(3) have "Cauchy (x \<circ> r)"
    4.83 +      using LIMSEQ_imp_Cauchy by auto
    4.84 +    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"
    4.85 +      unfolding cauchy_def using `e > 0` by blast
    4.86 +    then have False
    4.87 +      using x[of "r N" "r (N+1)"] r by (auto simp: subseq_def) }
    4.88 +  then show ?thesis
    4.89 +    by metis
    4.90  qed
    4.91  
    4.92  subsubsection{* Heine-Borel theorem *}
    4.93 @@ -3802,7 +3777,7 @@
    4.94    shows "compact s"
    4.95  proof -
    4.96    from seq_compact_imp_totally_bounded[OF `seq_compact s`]
    4.97 -  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)"
    4.98 +  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)"
    4.99      unfolding choice_iff' ..
   4.100    def K \<equiv> "(\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
   4.101    have "countably_compact s"
   4.102 @@ -4137,7 +4112,7 @@
   4.103  qed
   4.104  
   4.105  lemma compact_eq_totally_bounded:
   4.106 -  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
   4.107 +  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
   4.108      (is "_ \<longleftrightarrow> ?rhs")
   4.109  proof
   4.110    assume assms: "?rhs"
     5.1 --- a/src/HOL/Order_Relation.thy	Thu Sep 04 11:53:39 2014 +0200
     5.2 +++ b/src/HOL/Order_Relation.thy	Thu Sep 04 14:02:37 2014 +0200
     5.3 @@ -319,27 +319,6 @@
     5.4  *}
     5.5  
     5.6  
     5.7 -subsubsection {* Well-founded recursion via genuine fixpoints *}
     5.8 -
     5.9 -lemma wfrec_fixpoint:
    5.10 -fixes r :: "('a * 'a) set" and
    5.11 -      H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    5.12 -assumes WF: "wf r" and ADM: "adm_wf r H"
    5.13 -shows "wfrec r H = H (wfrec r H)"
    5.14 -proof(rule ext)
    5.15 -  fix x
    5.16 -  have "wfrec r H x = H (cut (wfrec r H) r x) x"
    5.17 -  using wfrec[of r H] WF by simp
    5.18 -  also
    5.19 -  {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
    5.20 -   by (auto simp add: cut_apply)
    5.21 -   hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
    5.22 -   using ADM adm_wf_def[of r H] by auto
    5.23 -  }
    5.24 -  finally show "wfrec r H x = H (wfrec r H) x" .
    5.25 -qed
    5.26 -
    5.27 -
    5.28  subsubsection {* Characterizations of well-foundedness *}
    5.29  
    5.30  text {* A transitive relation is well-founded iff it is ``locally'' well-founded,
     6.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Sep 04 11:53:39 2014 +0200
     6.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Sep 04 14:02:37 2014 +0200
     6.3 @@ -184,70 +184,51 @@
     6.4  
     6.5        let ?q = "\<lambda>k n y. \<mu>G (?M (J k) (A n) y)"
     6.6  
     6.7 -      have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
     6.8 -      from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this
     6.9 -
    6.10 -      let ?P =
    6.11 -        "\<lambda>k wk w. w \<in> space (Pi\<^sub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
    6.12 -          (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
    6.13 -      def w \<equiv> "rec_nat w0 (\<lambda>k wk. Eps (?P k wk))"
    6.14 -
    6.15 -      { fix k have w: "w k \<in> space (Pi\<^sub>M (J k) M) \<and>
    6.16 -          (\<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))"
    6.17 -        proof (induct k)
    6.18 -          case 0 with w0 show ?case
    6.19 -            unfolding w_def nat.rec(1) by auto
    6.20 +      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)"
    6.21 +      have "\<exists>w. \<forall>k. ?P (w k) k \<and> restrict (w (Suc k)) (J k) = w k"
    6.22 +      proof (rule dependent_nat_choice)
    6.23 +        have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
    6.24 +        from Ex_w[OF A(1,2) this J(1-3), of 0] show "\<exists>w. ?P w 0" by auto
    6.25 +      next
    6.26 +        fix w k assume Suc: "?P w k"
    6.27 +        show "\<exists>w'. ?P w' (Suc k) \<and> restrict w' (J k) = w"
    6.28 +        proof cases
    6.29 +          assume [simp]: "J k = J (Suc k)"
    6.30 +          have "?a / 2 ^ (Suc (Suc k)) \<le> ?a / 2 ^ (k + 1)"
    6.31 +            using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: field_simps)
    6.32 +          with Suc show ?thesis
    6.33 +            by (auto intro!: exI[of _ w] simp: extensional_restrict space_PiM intro: order_trans)
    6.34          next
    6.35 -          case (Suc k)
    6.36 -          then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
    6.37 -          have "\<exists>w'. ?P k (w k) w'"
    6.38 -          proof cases
    6.39 -            assume [simp]: "J k = J (Suc k)"
    6.40 -            show ?thesis
    6.41 -            proof (intro exI[of _ "w k"] conjI allI)
    6.42 -              fix n
    6.43 -              have "?a / 2 ^ (Suc k + 1) \<le> ?a / 2 ^ (k + 1)"
    6.44 -                using `0 < ?a` `?a \<le> 1` by (cases ?a) (auto simp: field_simps)
    6.45 -              also have "\<dots> \<le> ?q k n (w k)" using Suc by auto
    6.46 -              finally show "?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n (w k)" by simp
    6.47 -            next
    6.48 -              show "w k \<in> space (Pi\<^sub>M (J (Suc k)) M)"
    6.49 -                using Suc by simp
    6.50 -              then show "restrict (w k) (J k) = w k"
    6.51 -                by (simp add: extensional_restrict space_PiM)
    6.52 -            qed
    6.53 -          next
    6.54 -            assume "J k \<noteq> J (Suc k)"
    6.55 -            with J_mono[of k "Suc k"] have "J (Suc k) - J k \<noteq> {}" (is "?D \<noteq> {}") by auto
    6.56 -            have "range (\<lambda>n. ?M (J k) (A n) (w k)) \<subseteq> ?G"
    6.57 -              "decseq (\<lambda>n. ?M (J k) (A n) (w k))"
    6.58 -              "\<forall>n. ?a / 2 ^ (k + 1) \<le> \<mu>G (?M (J k) (A n) (w k))"
    6.59 -              using `decseq A` fold(4)[OF J(1-3) A_eq(2), of "w k" k] Suc
    6.60 -              by (auto simp: decseq_def)
    6.61 -            from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
    6.62 -            obtain w' where w': "w' \<in> space (Pi\<^sub>M ?D M)"
    6.63 -              "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) (w k)) w')" by auto
    6.64 -            let ?w = "merge (J k) ?D (w k, w')"
    6.65 -            have [simp]: "\<And>x. merge (J k) (I - J k) (w k, merge ?D (I - ?D) (w', x)) =
    6.66 -              merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
    6.67 -              using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
    6.68 -              by (auto intro!: ext split: split_merge)
    6.69 -            have *: "\<And>n. ?M ?D (?M (J k) (A n) (w k)) w' = ?M (J (Suc k)) (A n) ?w"
    6.70 -              using w'(1) J(3)[of "Suc k"]
    6.71 -              by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
    6.72 -            show ?thesis
    6.73 -              using w' J_mono[of k "Suc k"] wk unfolding *
    6.74 -              by (intro exI[of _ ?w])
    6.75 -                 (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
    6.76 -          qed
    6.77 -          then have "?P k (w k) (w (Suc k))"
    6.78 -            unfolding w_def nat.rec(2) unfolding w_def[symmetric]
    6.79 -            by (rule someI_ex)
    6.80 -          then show ?case by auto
    6.81 +          assume "J k \<noteq> J (Suc k)"
    6.82 +          with J_mono[of k "Suc k"] have "J (Suc k) - J k \<noteq> {}" (is "?D \<noteq> {}") by auto
    6.83 +          have "range (\<lambda>n. ?M (J k) (A n) w) \<subseteq> ?G" "decseq (\<lambda>n. ?M (J k) (A n) w)"
    6.84 +            "\<forall>n. ?a / 2 ^ (k + 1) \<le> \<mu>G (?M (J k) (A n) w)"
    6.85 +            using `decseq A` fold(4)[OF J(1-3) A_eq(2), of w k] Suc
    6.86 +            by (auto simp: decseq_def)
    6.87 +          from Ex_w[OF this `?D \<noteq> {}`] J[of "Suc k"]
    6.88 +          obtain w' where w': "w' \<in> space (Pi\<^sub>M ?D M)"
    6.89 +            "\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> \<mu>G (?M ?D (?M (J k) (A n) w) w')" by auto
    6.90 +          let ?w = "merge (J k) ?D (w, w')"
    6.91 +          have [simp]: "\<And>x. merge (J k) (I - J k) (w, merge ?D (I - ?D) (w', x)) =
    6.92 +            merge (J (Suc k)) (I - (J (Suc k))) (?w, x)"
    6.93 +            using J(3)[of "Suc k"] J(3)[of k] J_mono[of k "Suc k"]
    6.94 +            by (auto intro!: ext split: split_merge)
    6.95 +          have *: "\<And>n. ?M ?D (?M (J k) (A n) w) w' = ?M (J (Suc k)) (A n) ?w"
    6.96 +            using w'(1) J(3)[of "Suc k"]
    6.97 +            by (auto simp: space_PiM split: split_merge intro!: extensional_merge_sub) force+
    6.98 +          show ?thesis
    6.99 +            using Suc w' J_mono[of k "Suc k"] unfolding *
   6.100 +            by (intro exI[of _ ?w])
   6.101 +               (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
   6.102          qed
   6.103 -        moreover
   6.104 -        from w have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
   6.105 -        moreover
   6.106 +      qed
   6.107 +      then obtain w where w:
   6.108 +        "\<And>k. w k \<in> space (Pi\<^sub>M (J k) M)"
   6.109 +        "\<And>k n. ?a / 2 ^ (Suc k) \<le> ?q k n (w k)"
   6.110 +        "\<And>k. restrict (w (Suc k)) (J k) = w k"
   6.111 +        by metis
   6.112 +
   6.113 +      { fix k
   6.114          from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
   6.115          then have "?M (J k) (A k) (w k) \<noteq> {}"
   6.116            using positive_mu_G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
   6.117 @@ -256,19 +237,15 @@
   6.118          then have "merge (J k) (I - J k) (w k, x) \<in> A k" by auto
   6.119          then have "\<exists>x\<in>A k. restrict x (J k) = w k"
   6.120            using `w k \<in> space (Pi\<^sub>M (J k) M)`
   6.121 -          by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM)
   6.122 -        ultimately have "w k \<in> space (Pi\<^sub>M (J k) M)"
   6.123 -          "\<exists>x\<in>A k. restrict x (J k) = w k"
   6.124 -          "k \<noteq> 0 \<Longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1)"
   6.125 -          by auto }
   6.126 -      note w = this
   6.127 +          by (intro rev_bexI) (auto intro!: ext simp: extensional_def space_PiM) }
   6.128 +      note w_ext = this
   6.129  
   6.130        { fix k l i assume "k \<le> l" "i \<in> J k"
   6.131          { fix l have "w k i = w (k + l) i"
   6.132            proof (induct l)
   6.133              case (Suc l)
   6.134              from `i \<in> J k` J_mono[of k "k + l"] have "i \<in> J (k + l)" by auto
   6.135 -            with w(3)[of "k + Suc l"]
   6.136 +            with w(3)[of "k + l"]
   6.137              have "w (k + l) i = w (k + Suc l) i"
   6.138                by (auto simp: restrict_def fun_eq_iff split: split_if_asm)
   6.139              with Suc show ?case by simp
   6.140 @@ -297,7 +274,8 @@
   6.141        { fix n
   6.142          have "restrict w' (J n) = w n" using w(1)[of n]
   6.143            by (auto simp add: fun_eq_iff space_PiM)
   6.144 -        with w[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)" by auto
   6.145 +        with w_ext[of n] obtain x where "x \<in> A n" "restrict x (J n) = restrict w' (J n)"
   6.146 +          by auto
   6.147          then have "w' \<in> A n" unfolding A_eq using w' by (auto simp: prod_emb_def space_PiM) }
   6.148        then have "w' \<in> (\<Inter>i. A i)" by auto
   6.149        with `(\<Inter>i. A i) = {}` show False by auto
     7.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Sep 04 11:53:39 2014 +0200
     7.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Thu Sep 04 14:02:37 2014 +0200
     7.3 @@ -233,42 +233,34 @@
     7.4  proof -
     7.5    interpret N: finite_measure N by fact
     7.6    let ?d = "\<lambda>A. measure M A - measure N A"
     7.7 -  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)"
     7.8 -  let ?r = "\<lambda>S. restricted_space S"
     7.9 -  { fix S n assume S: "S \<in> sets M"
    7.10 -    then have "finite_measure (density M (indicator S))" "0 < 1 / real (Suc n)"
    7.11 -         "finite_measure (density N (indicator S))" "sets (density N (indicator S)) = sets (density M (indicator S))"
    7.12 +  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)"
    7.13 +  let ?Q = "\<lambda>A B. A \<subseteq> B \<and> ?d B \<le> ?d A"
    7.14 +
    7.15 +  have "\<exists>A. \<forall>n. (A n \<in> sets M \<and> ?P (A n) n) \<and> ?Q (A (Suc n)) (A n)"
    7.16 +  proof (rule dependent_nat_choice)
    7.17 +    show "\<exists>A. A \<in> sets M \<and> ?P A 0"
    7.18 +      by auto
    7.19 +  next
    7.20 +    fix A n assume "A \<in> sets M \<and> ?P A n"
    7.21 +    then have A: "A \<in> sets M" by auto
    7.22 +    then have "finite_measure (density M (indicator A))" "0 < 1 / real (Suc (Suc n))"
    7.23 +         "finite_measure (density N (indicator A))" "sets (density N (indicator A)) = sets (density M (indicator A))"
    7.24        by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
    7.25      from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
    7.26 -    with S have "?P (S \<inter> X) S n"
    7.27 +    with A have "A \<inter> X \<in> sets M \<and> ?P (A \<inter> X) (Suc n) \<and> ?Q (A \<inter> X) A"
    7.28        by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
    7.29 -    hence "\<exists>A. ?P A S n" .. }
    7.30 -  note Ex_P = this
    7.31 -  def A \<equiv> "rec_nat (space M) (\<lambda>n A. SOME B. ?P B A n)"
    7.32 -  have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
    7.33 -  have A_0[simp]: "A 0 = space M" unfolding A_def by simp
    7.34 -  { fix i have "A i \<in> sets M" unfolding A_def
    7.35 -    proof (induct i)
    7.36 -      case (Suc i)
    7.37 -      from Ex_P[OF this, of i] show ?case unfolding nat.rec(2)
    7.38 -        by (rule someI2_ex) simp
    7.39 -    qed simp }
    7.40 -  note A_in_sets = this
    7.41 -  { fix n have "?P (A (Suc n)) (A n) n"
    7.42 -      using Ex_P[OF A_in_sets] unfolding A_Suc
    7.43 -      by (rule someI2_ex) simp }
    7.44 -  note P_A = this
    7.45 -  have "range A \<subseteq> sets M" using A_in_sets by auto
    7.46 -  have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp
    7.47 -  have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc)
    7.48 -  have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow> - 1 / real (Suc i) < ?d C"
    7.49 -      using P_A by auto
    7.50 +    then show "\<exists>B. (B \<in> sets M \<and> ?P B (Suc n)) \<and> ?Q B A"
    7.51 +      by blast
    7.52 +  qed
    7.53 +  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)"
    7.54 +    by metis
    7.55 +  then have mono_dA: "mono (\<lambda>i. ?d (A i))" and A_0[simp]: "A 0 = space M"
    7.56 +    by (auto simp add: mono_iff_le_Suc)
    7.57    show ?thesis
    7.58    proof (safe intro!: bexI[of _ "\<Inter>i. A i"])
    7.59 -    show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto
    7.60 -    have A: "decseq A" using A_mono by (auto intro!: decseq_SucI)
    7.61 -    from `range A \<subseteq> sets M`
    7.62 -      finite_Lim_measure_decseq[OF _ A] N.finite_Lim_measure_decseq[OF _ A]
    7.63 +    show "(\<Inter>i. A i) \<in> sets M" using `\<And>n. A n \<in> sets M` by auto
    7.64 +    have "decseq A" using A by (auto intro!: decseq_SucI)
    7.65 +    from A(1) finite_Lim_measure_decseq[OF _ this] N.finite_Lim_measure_decseq[OF _ this]
    7.66      have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: tendsto_diff simp: sets_eq)
    7.67      thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
    7.68        by (rule_tac LIMSEQ_le_const) auto
    7.69 @@ -280,10 +272,11 @@
    7.70        hence "0 < - ?d B" by auto
    7.71        from ex_inverse_of_nat_Suc_less[OF this]
    7.72        obtain n where *: "?d B < - 1 / real (Suc n)"
    7.73 -        by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
    7.74 -      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
    7.75 -      from epsilon[OF B(1) this] *
    7.76 -      show False by auto
    7.77 +        by (auto simp: real_eq_of_nat field_simps)
    7.78 +      also have "\<dots> \<le> - 1 / real (Suc (Suc n))"
    7.79 +        by (auto simp: field_simps)
    7.80 +      finally show False
    7.81 +        using * A(2)[of "Suc n"] B by (auto elim!: ballE[of _ _ B])
    7.82      qed
    7.83    qed
    7.84  qed
     8.1 --- a/src/HOL/Probability/Regularity.thy	Thu Sep 04 11:53:39 2014 +0200
     8.2 +++ b/src/HOL/Probability/Regularity.thy	Thu Sep 04 14:02:37 2014 +0200
     8.3 @@ -163,7 +163,7 @@
     8.4      by blast
     8.5    then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
     8.6      \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
     8.7 -    apply atomize_elim unfolding bchoice_iff .
     8.8 +    by metis
     8.9    hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
    8.10      \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
    8.11      unfolding Ball_def by blast
    8.12 @@ -209,8 +209,8 @@
    8.13        from nat_approx_posE[OF this] guess n . note n = this
    8.14        let ?k = "from_nat_into X ` {0..k e (Suc n)}"
    8.15        have "finite ?k" by simp
    8.16 -      moreover have "K \<subseteq> \<Union>((\<lambda>x. ball x e') ` ?k)" unfolding K_def B_def using n by force
    8.17 -      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>((\<lambda>x. ball x e') ` k)" by blast
    8.18 +      moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force
    8.19 +      ultimately show "\<exists>k. finite k \<and> K \<subseteq> (\<Union>x\<in>k. ball x e')" by blast
    8.20      qed
    8.21      ultimately
    8.22      show "?thesis e " by (auto simp: sU)
     9.1 --- a/src/HOL/Tools/TFL/thms.ML	Thu Sep 04 11:53:39 2014 +0200
     9.2 +++ b/src/HOL/Tools/TFL/thms.ML	Thu Sep 04 14:02:37 2014 +0200
     9.3 @@ -7,7 +7,7 @@
     9.4  struct
     9.5    val WFREC_COROLLARY = @{thm tfl_wfrec};
     9.6    val WF_INDUCTION_THM = @{thm tfl_wf_induct};
     9.7 -  val CUT_DEF = @{thm cut_def};
     9.8 +  val CUT_DEF = @{thm tfl_cut_def};
     9.9    val eqT = @{thm tfl_eq_True};
    9.10    val rev_eq_mp = @{thm tfl_rev_eq_mp};
    9.11    val simp_thm = @{thm tfl_simp_thm};
    10.1 --- a/src/HOL/Wfrec.thy	Thu Sep 04 11:53:39 2014 +0200
    10.2 +++ b/src/HOL/Wfrec.thy	Thu Sep 04 14:02:37 2014 +0200
    10.3 @@ -10,86 +10,88 @@
    10.4  imports Wellfounded
    10.5  begin
    10.6  
    10.7 -inductive
    10.8 -  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
    10.9 -  for R :: "('a * 'a) set"
   10.10 -  and F :: "('a => 'b) => 'a => 'b"
   10.11 -where
   10.12 -  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
   10.13 -            wfrec_rel R F x (F g x)"
   10.14 +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
   10.15 +  wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
   10.16  
   10.17 -definition
   10.18 -  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" where
   10.19 -  "cut f r x == (%y. if (y,x):r then f y else undefined)"
   10.20 +definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b" where
   10.21 +  "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
   10.22 +
   10.23 +definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool" where
   10.24 +  "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)"
   10.25  
   10.26 -definition
   10.27 -  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" where
   10.28 -  "adm_wf R F == ALL f g x.
   10.29 -     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
   10.30 +definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)" where
   10.31 +  "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
   10.32  
   10.33 -definition
   10.34 -  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
   10.35 -  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
   10.36 +lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
   10.37 +  by (simp add: fun_eq_iff cut_def)
   10.38  
   10.39 -lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
   10.40 -by (simp add: fun_eq_iff cut_def)
   10.41 -
   10.42 -lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
   10.43 -by (simp add: cut_def)
   10.44 +lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
   10.45 +  by (simp add: cut_def)
   10.46  
   10.47  text{*Inductive characterization of wfrec combinator; for details see:
   10.48  John Harrison, "Inductive definitions: automation and application"*}
   10.49  
   10.50 -lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
   10.51 -apply (simp add: adm_wf_def)
   10.52 -apply (erule_tac a=x in wf_induct)
   10.53 -apply (rule ex1I)
   10.54 -apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
   10.55 -apply (fast dest!: theI')
   10.56 -apply (erule wfrec_rel.cases, simp)
   10.57 -apply (erule allE, erule allE, erule allE, erule mp)
   10.58 -apply (blast intro: the_equality [symmetric])
   10.59 -done
   10.60 +lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
   10.61 +  by (auto intro: the_equality[symmetric] theI)
   10.62  
   10.63 -lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
   10.64 -apply (simp add: adm_wf_def)
   10.65 -apply (intro strip)
   10.66 -apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
   10.67 -apply (rule refl)
   10.68 -done
   10.69 +lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
   10.70 +  using `wf R`
   10.71 +proof induct
   10.72 +  def f \<equiv> "\<lambda>y. THE z. wfrec_rel R F y z"
   10.73 +  case (less x)
   10.74 +  then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
   10.75 +    unfolding f_def by (rule theI_unique)
   10.76 +  with `adm_wf R F` show ?case
   10.77 +    by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
   10.78 +qed
   10.79  
   10.80 -lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
   10.81 +lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
   10.82 +  by (auto simp add: adm_wf_def
   10.83 +           intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
   10.84 +
   10.85 +lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
   10.86  apply (simp add: wfrec_def)
   10.87  apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
   10.88  apply (rule wfrec_rel.wfrecI)
   10.89 -apply (intro strip)
   10.90  apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
   10.91  done
   10.92  
   10.93  
   10.94  text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
   10.95 -lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
   10.96 -apply auto
   10.97 -apply (blast intro: wfrec)
   10.98 -done
   10.99 +lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
  10.100 + by (auto intro: wfrec)
  10.101 +
  10.102 +
  10.103 +subsubsection {* Well-founded recursion via genuine fixpoints *}
  10.104  
  10.105 +lemma wfrec_fixpoint:
  10.106 +  assumes WF: "wf R" and ADM: "adm_wf R F"
  10.107 +  shows "wfrec R F = F (wfrec R F)"
  10.108 +proof (rule ext)
  10.109 +  fix x
  10.110 +  have "wfrec R F x = F (cut (wfrec R F) R x) x"
  10.111 +    using wfrec[of R F] WF by simp
  10.112 +  also
  10.113 +  { have "\<And> y. (y,x) \<in> R \<Longrightarrow> (cut (wfrec R F) R x) y = (wfrec R F) y"
  10.114 +      by (auto simp add: cut_apply)
  10.115 +    hence "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
  10.116 +      using ADM adm_wf_def[of R F] by auto }
  10.117 +  finally show "wfrec R F x = F (wfrec R F) x" .
  10.118 +qed
  10.119  
  10.120  subsection {* Wellfoundedness of @{text same_fst} *}
  10.121  
  10.122 -definition
  10.123 - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
  10.124 -where
  10.125 -    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
  10.126 -   --{*For @{text rec_def} declarations where the first n parameters
  10.127 +definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
  10.128 +  "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
  10.129 +   --{*For @{const wfrec} declarations where the first n parameters
  10.130         stay unchanged in the recursive call. *}
  10.131  
  10.132 -lemma same_fstI [intro!]:
  10.133 -     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
  10.134 -by (simp add: same_fst_def)
  10.135 +lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
  10.136 +  by (simp add: same_fst_def)
  10.137  
  10.138  lemma wf_same_fst:
  10.139 -  assumes prem: "(!!x. P x ==> wf(R x))"
  10.140 -  shows "wf(same_fst P R)"
  10.141 +  assumes prem: "\<And>x. P x \<Longrightarrow> wf (R x)"
  10.142 +  shows "wf (same_fst P R)"
  10.143  apply (simp cong del: imp_cong add: wf_def same_fst_def)
  10.144  apply (intro strip)
  10.145  apply (rename_tac a b)
    11.1 --- a/src/HOL/Zorn.thy	Thu Sep 04 11:53:39 2014 +0200
    11.2 +++ b/src/HOL/Zorn.thy	Thu Sep 04 14:02:37 2014 +0200
    11.3 @@ -720,4 +720,36 @@
    11.4    with 1 show ?thesis by auto
    11.5  qed
    11.6  
    11.7 +(* Move this to Hilbert Choice and wfrec to Wellfounded*)
    11.8 +
    11.9 +lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
   11.10 +  using wfrec_fixpoint by simp
   11.11 +
   11.12 +lemma dependent_wf_choice:
   11.13 +  fixes P :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   11.14 +  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"
   11.15 +  assumes P: "\<And>x f. (\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
   11.16 +  shows "\<exists>f. \<forall>x. P f x (f x)"
   11.17 +proof (intro exI allI)
   11.18 +  fix x 
   11.19 +  def f \<equiv> "wfrec R (\<lambda>f x. SOME r. P f x r)"
   11.20 +  from `wf R` show "P f x (f x)"
   11.21 +  proof (induct x)
   11.22 +    fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)"
   11.23 +    show "P f x (f x)"
   11.24 +    proof (subst (2) wfrec_def_adm[OF f_def `wf R`])
   11.25 +      show "adm_wf R (\<lambda>f x. SOME r. P f x r)"
   11.26 +        by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm)
   11.27 +      show "P f x (Eps (P f x))"
   11.28 +        using P by (rule someI_ex) fact
   11.29 +    qed
   11.30 +  qed
   11.31 +qed
   11.32 +
   11.33 +lemma (in wellorder) dependent_wellorder_choice:
   11.34 +  assumes "\<And>r f g x. (\<And>y. y < x \<Longrightarrow> f y = g y) \<Longrightarrow> P f x r = P g x r"
   11.35 +  assumes P: "\<And>x f. (\<And>y. y < x \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
   11.36 +  shows "\<exists>f. \<forall>x. P f x (f x)"
   11.37 +  using wf by (rule dependent_wf_choice) (auto intro!: assms)
   11.38 +
   11.39  end