src/HOL/Hilbert_Choice.thy
 changeset 49948 744934b818c7 parent 49739 13aa6d8268ec child 50105 65d5b18e1626
```     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Oct 20 09:09:37 2012 +0200
1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Oct 20 09:12:16 2012 +0200
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 Plain
1.8 +imports Nat Wellfounded Big_Operators
1.9  keywords "specification" "ax_specification" :: thy_goal
1.10  begin
1.11
1.12 @@ -643,6 +643,144 @@
1.13    done
1.14
1.15
1.16 +subsection {* An aside: bounded accessible part *}
1.17 +
1.18 +text {* Finite monotone eventually stable sequences *}
1.19 +
1.20 +lemma finite_mono_remains_stable_implies_strict_prefix:
1.21 +  fixes f :: "nat \<Rightarrow> 'a::order"
1.22 +  assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
1.23 +  shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
1.24 +  using assms
1.25 +proof -
1.26 +  have "\<exists>n. f n = f (Suc n)"
1.27 +  proof (rule ccontr)
1.28 +    assume "\<not> ?thesis"
1.29 +    then have "\<And>n. f n \<noteq> f (Suc n)" by auto
1.30 +    then have "\<And>n. f n < f (Suc n)"
1.31 +      using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
1.32 +    with lift_Suc_mono_less_iff[of f]
1.33 +    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
1.34 +    then have "inj f"
1.35 +      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
1.36 +    with `finite (range f)` have "finite (UNIV::nat set)"
1.37 +      by (rule finite_imageD)
1.38 +    then show False by simp
1.39 +  qed
1.40 +  then obtain n where n: "f n = f (Suc n)" ..
1.41 +  def N \<equiv> "LEAST n. f n = f (Suc n)"
1.42 +  have N: "f N = f (Suc N)"
1.43 +    unfolding N_def using n by (rule LeastI)
1.44 +  show ?thesis
1.45 +  proof (intro exI[of _ N] conjI allI impI)
1.46 +    fix n assume "N \<le> n"
1.47 +    then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
1.48 +    proof (induct rule: dec_induct)
1.49 +      case (step n) then show ?case
1.50 +        using eq[rule_format, of "n - 1"] N
1.51 +        by (cases n) (auto simp add: le_Suc_eq)
1.52 +    qed simp
1.53 +    from this[of n] `N \<le> n` show "f N = f n" by auto
1.54 +  next
1.55 +    fix n m :: nat assume "m < n" "n \<le> N"
1.56 +    then show "f m < f n"
1.57 +    proof (induct rule: less_Suc_induct[consumes 1])
1.58 +      case (1 i)
1.59 +      then have "i < N" by simp
1.60 +      then have "f i \<noteq> f (Suc i)"
1.61 +        unfolding N_def by (rule not_less_Least)
1.62 +      with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
1.63 +    qed auto
1.64 +  qed
1.65 +qed
1.66 +
1.67 +lemma finite_mono_strict_prefix_implies_finite_fixpoint:
1.68 +  fixes f :: "nat \<Rightarrow> 'a set"
1.69 +  assumes S: "\<And>i. f i \<subseteq> S" "finite S"
1.70 +    and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
1.71 +  shows "f (card S) = (\<Union>n. f n)"
1.72 +proof -
1.73 +  from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
1.74 +
1.75 +  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
1.76 +    proof (induct i)
1.77 +      case 0 then show ?case by simp
1.78 +    next
1.79 +      case (Suc i)
1.80 +      with inj[rule_format, of "Suc i" i]
1.81 +      have "(f i) \<subset> (f (Suc i))" by auto
1.82 +      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
1.83 +      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
1.84 +      with Suc show ?case using inj by auto
1.85 +    qed
1.86 +  }
1.87 +  then have "N \<le> card (f N)" by simp
1.88 +  also have "\<dots> \<le> card S" using S by (intro card_mono)
1.89 +  finally have "f (card S) = f N" using eq by auto
1.90 +  then show ?thesis using eq inj[rule_format, of N]
1.91 +    apply auto
1.92 +    apply (case_tac "n < N")
1.93 +    apply (auto simp: not_less)
1.94 +    done
1.95 +qed
1.96 +
1.97 +primrec bacc :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a set"
1.98 +where
1.99 +  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
1.100 +| "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
1.101 +
1.102 +lemma bacc_subseteq_acc:
1.103 +  "bacc r n \<subseteq> acc r"
1.104 +  by (induct n) (auto intro: acc.intros)
1.105 +
1.106 +lemma bacc_mono:
1.107 +  "n \<le> m \<Longrightarrow> bacc r n \<subseteq> bacc r m"
1.108 +  by (induct rule: dec_induct) auto
1.109 +
1.110 +lemma bacc_upper_bound:
1.111 +  "bacc (r :: ('a \<times> 'a) set)  (card (UNIV :: 'a::finite set)) = (\<Union>n. bacc r n)"
1.112 +proof -
1.113 +  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
1.114 +  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
1.115 +  moreover have "finite (range (bacc r))" by auto
1.116 +  ultimately show ?thesis
1.117 +   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
1.118 +     (auto intro: finite_mono_remains_stable_implies_strict_prefix)
1.119 +qed
1.120 +
1.121 +lemma acc_subseteq_bacc:
1.122 +  assumes "finite r"
1.123 +  shows "acc r \<subseteq> (\<Union>n. bacc r n)"
1.124 +proof
1.125 +  fix x
1.126 +  assume "x : acc r"
1.127 +  then have "\<exists> n. x : bacc r n"
1.128 +  proof (induct x arbitrary: rule: acc.induct)
1.129 +    case (accI x)
1.130 +    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
1.131 +    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
1.132 +    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
1.133 +    proof
1.134 +      fix y assume y: "(y, x) : r"
1.135 +      with n have "y : bacc r (n y)" by auto
1.136 +      moreover have "n y <= Max ((%(y, x). n y) ` r)"
1.137 +        using y `finite r` by (auto intro!: Max_ge)
1.138 +      note bacc_mono[OF this, of r]
1.139 +      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
1.140 +    qed
1.141 +    then show ?case
1.142 +      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
1.143 +  qed
1.144 +  then show "x : (UN n. bacc r n)" by auto
1.145 +qed
1.146 +
1.147 +lemma acc_bacc_eq:
1.148 +  fixes A :: "('a :: finite \<times> 'a) set"
1.149 +  assumes "finite A"
1.150 +  shows "acc A = bacc A (card (UNIV :: 'a set))"
1.151 +  using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
1.152 +
1.153 +
1.154  subsection {* Specification package -- Hilbertized version *}
1.155
1.156  lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
1.157 @@ -651,3 +789,4 @@
1.158  ML_file "Tools/choice_specification.ML"
1.159
1.160  end
1.161 +
```