src/HOL/Hilbert_Choice.thy
changeset 55088 57c82e01022b
parent 55020 96b05fd2aee4
child 55415 05f5fdb8d093
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Jan 20 22:24:48 2014 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Jan 20 23:07:23 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
     1.5  
     1.6  theory Hilbert_Choice
     1.7 -imports Nat Wellfounded Lattices_Big Metis
     1.8 +imports Nat Wellfounded Metis
     1.9  keywords "specification" "ax_specification" :: thy_goal
    1.10  begin
    1.11  
    1.12 @@ -770,62 +770,6 @@
    1.13      done
    1.14  qed
    1.15  
    1.16 -primrec bacc :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a set" 
    1.17 -where
    1.18 -  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
    1.19 -| "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
    1.20 -
    1.21 -lemma bacc_subseteq_acc:
    1.22 -  "bacc r n \<subseteq> Wellfounded.acc r"
    1.23 -  by (induct n) (auto intro: acc.intros)
    1.24 -
    1.25 -lemma bacc_mono:
    1.26 -  "n \<le> m \<Longrightarrow> bacc r n \<subseteq> bacc r m"
    1.27 -  by (induct rule: dec_induct) auto
    1.28 -  
    1.29 -lemma bacc_upper_bound:
    1.30 -  "bacc (r :: ('a \<times> 'a) set)  (card (UNIV :: 'a::finite set)) = (\<Union>n. bacc r n)"
    1.31 -proof -
    1.32 -  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
    1.33 -  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
    1.34 -  moreover have "finite (range (bacc r))" by auto
    1.35 -  ultimately show ?thesis
    1.36 -   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
    1.37 -     (auto intro: finite_mono_remains_stable_implies_strict_prefix)
    1.38 -qed
    1.39 -
    1.40 -lemma acc_subseteq_bacc:
    1.41 -  assumes "finite r"
    1.42 -  shows "Wellfounded.acc r \<subseteq> (\<Union>n. bacc r n)"
    1.43 -proof
    1.44 -  fix x
    1.45 -  assume "x : Wellfounded.acc r"
    1.46 -  then have "\<exists> n. x : bacc r n"
    1.47 -  proof (induct x arbitrary: rule: acc.induct)
    1.48 -    case (accI x)
    1.49 -    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
    1.50 -    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
    1.51 -    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
    1.52 -    proof
    1.53 -      fix y assume y: "(y, x) : r"
    1.54 -      with n have "y : bacc r (n y)" by auto
    1.55 -      moreover have "n y <= Max ((%(y, x). n y) ` r)"
    1.56 -        using y `finite r` by (auto intro!: Max_ge)
    1.57 -      note bacc_mono[OF this, of r]
    1.58 -      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
    1.59 -    qed
    1.60 -    then show ?case
    1.61 -      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
    1.62 -  qed
    1.63 -  then show "x : (UN n. bacc r n)" by auto
    1.64 -qed
    1.65 -
    1.66 -lemma acc_bacc_eq:
    1.67 -  fixes A :: "('a :: finite \<times> 'a) set"
    1.68 -  assumes "finite A"
    1.69 -  shows "Wellfounded.acc A = bacc A (card (UNIV :: 'a set))"
    1.70 -  using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
    1.71 -
    1.72  
    1.73  subsection {* More on injections, bijections, and inverses *}
    1.74