src/HOL/Zorn.thy
changeset 58184 db1381d811ab
parent 55811 aa1acc25126b
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Zorn.thy	Thu Sep 04 11:53:39 2014 +0200
     1.2 +++ b/src/HOL/Zorn.thy	Thu Sep 04 14:02:37 2014 +0200
     1.3 @@ -720,4 +720,36 @@
     1.4    with 1 show ?thesis by auto
     1.5  qed
     1.6  
     1.7 +(* Move this to Hilbert Choice and wfrec to Wellfounded*)
     1.8 +
     1.9 +lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
    1.10 +  using wfrec_fixpoint by simp
    1.11 +
    1.12 +lemma dependent_wf_choice:
    1.13 +  fixes P :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    1.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"
    1.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"
    1.16 +  shows "\<exists>f. \<forall>x. P f x (f x)"
    1.17 +proof (intro exI allI)
    1.18 +  fix x 
    1.19 +  def f \<equiv> "wfrec R (\<lambda>f x. SOME r. P f x r)"
    1.20 +  from `wf R` show "P f x (f x)"
    1.21 +  proof (induct x)
    1.22 +    fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)"
    1.23 +    show "P f x (f x)"
    1.24 +    proof (subst (2) wfrec_def_adm[OF f_def `wf R`])
    1.25 +      show "adm_wf R (\<lambda>f x. SOME r. P f x r)"
    1.26 +        by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm)
    1.27 +      show "P f x (Eps (P f x))"
    1.28 +        using P by (rule someI_ex) fact
    1.29 +    qed
    1.30 +  qed
    1.31 +qed
    1.32 +
    1.33 +lemma (in wellorder) dependent_wellorder_choice:
    1.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"
    1.35 +  assumes P: "\<And>x f. (\<And>y. y < x \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
    1.36 +  shows "\<exists>f. \<forall>x. P f x (f x)"
    1.37 +  using wf by (rule dependent_wf_choice) (auto intro!: assms)
    1.38 +
    1.39  end