moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
authorblanchet
Mon Jan 20 23:07:23 2014 +0100 (2014-01-20)
changeset 5508857c82e01022b
parent 55087 252c7fec4119
child 55089 181751ad852f
moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
src/HOL/Enum.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Enum.thy	Mon Jan 20 22:24:48 2014 +0100
     1.2 +++ b/src/HOL/Enum.thy	Mon Jan 20 23:07:23 2014 +0100
     1.3 @@ -176,6 +176,65 @@
     1.4    "f <*mlex*> R = {(x, y). f x < f y \<or> (f x \<le> f y \<and> (x, y) \<in> R)}"
     1.5    by (auto simp add: mlex_prod_def)
     1.6  
     1.7 +
     1.8 +subsubsection {* Bounded accessible part *}
     1.9 +
    1.10 +primrec bacc :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a set" 
    1.11 +where
    1.12 +  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
    1.13 +| "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
    1.14 +
    1.15 +lemma bacc_subseteq_acc:
    1.16 +  "bacc r n \<subseteq> Wellfounded.acc r"
    1.17 +  by (induct n) (auto intro: acc.intros)
    1.18 +
    1.19 +lemma bacc_mono:
    1.20 +  "n \<le> m \<Longrightarrow> bacc r n \<subseteq> bacc r m"
    1.21 +  by (induct rule: dec_induct) auto
    1.22 +  
    1.23 +lemma bacc_upper_bound:
    1.24 +  "bacc (r :: ('a \<times> 'a) set)  (card (UNIV :: 'a::finite set)) = (\<Union>n. bacc r n)"
    1.25 +proof -
    1.26 +  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
    1.27 +  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
    1.28 +  moreover have "finite (range (bacc r))" by auto
    1.29 +  ultimately show ?thesis
    1.30 +   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
    1.31 +     (auto intro: finite_mono_remains_stable_implies_strict_prefix)
    1.32 +qed
    1.33 +
    1.34 +lemma acc_subseteq_bacc:
    1.35 +  assumes "finite r"
    1.36 +  shows "Wellfounded.acc r \<subseteq> (\<Union>n. bacc r n)"
    1.37 +proof
    1.38 +  fix x
    1.39 +  assume "x : Wellfounded.acc r"
    1.40 +  then have "\<exists> n. x : bacc r n"
    1.41 +  proof (induct x arbitrary: rule: acc.induct)
    1.42 +    case (accI x)
    1.43 +    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
    1.44 +    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
    1.45 +    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
    1.46 +    proof
    1.47 +      fix y assume y: "(y, x) : r"
    1.48 +      with n have "y : bacc r (n y)" by auto
    1.49 +      moreover have "n y <= Max ((%(y, x). n y) ` r)"
    1.50 +        using y `finite r` by (auto intro!: Max_ge)
    1.51 +      note bacc_mono[OF this, of r]
    1.52 +      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
    1.53 +    qed
    1.54 +    then show ?case
    1.55 +      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
    1.56 +  qed
    1.57 +  then show "x : (UN n. bacc r n)" by auto
    1.58 +qed
    1.59 +
    1.60 +lemma acc_bacc_eq:
    1.61 +  fixes A :: "('a :: finite \<times> 'a) set"
    1.62 +  assumes "finite A"
    1.63 +  shows "Wellfounded.acc A = bacc A (card (UNIV :: 'a set))"
    1.64 +  using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
    1.65 +
    1.66  lemma [code]:
    1.67    fixes xs :: "('a::finite \<times> 'a) list"
    1.68    shows "Wellfounded.acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
    1.69 @@ -641,4 +700,3 @@
    1.70  hide_const (open) enum enum_all enum_ex all_n_lists ex_n_lists ntrancl
    1.71  
    1.72  end
    1.73 -
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Jan 20 22:24:48 2014 +0100
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Jan 20 23:07:23 2014 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
     2.5  
     2.6  theory Hilbert_Choice
     2.7 -imports Nat Wellfounded Lattices_Big Metis
     2.8 +imports Nat Wellfounded Metis
     2.9  keywords "specification" "ax_specification" :: thy_goal
    2.10  begin
    2.11  
    2.12 @@ -770,62 +770,6 @@
    2.13      done
    2.14  qed
    2.15  
    2.16 -primrec bacc :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a set" 
    2.17 -where
    2.18 -  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
    2.19 -| "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
    2.20 -
    2.21 -lemma bacc_subseteq_acc:
    2.22 -  "bacc r n \<subseteq> Wellfounded.acc r"
    2.23 -  by (induct n) (auto intro: acc.intros)
    2.24 -
    2.25 -lemma bacc_mono:
    2.26 -  "n \<le> m \<Longrightarrow> bacc r n \<subseteq> bacc r m"
    2.27 -  by (induct rule: dec_induct) auto
    2.28 -  
    2.29 -lemma bacc_upper_bound:
    2.30 -  "bacc (r :: ('a \<times> 'a) set)  (card (UNIV :: 'a::finite set)) = (\<Union>n. bacc r n)"
    2.31 -proof -
    2.32 -  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
    2.33 -  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
    2.34 -  moreover have "finite (range (bacc r))" by auto
    2.35 -  ultimately show ?thesis
    2.36 -   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
    2.37 -     (auto intro: finite_mono_remains_stable_implies_strict_prefix)
    2.38 -qed
    2.39 -
    2.40 -lemma acc_subseteq_bacc:
    2.41 -  assumes "finite r"
    2.42 -  shows "Wellfounded.acc r \<subseteq> (\<Union>n. bacc r n)"
    2.43 -proof
    2.44 -  fix x
    2.45 -  assume "x : Wellfounded.acc r"
    2.46 -  then have "\<exists> n. x : bacc r n"
    2.47 -  proof (induct x arbitrary: rule: acc.induct)
    2.48 -    case (accI x)
    2.49 -    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
    2.50 -    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
    2.51 -    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
    2.52 -    proof
    2.53 -      fix y assume y: "(y, x) : r"
    2.54 -      with n have "y : bacc r (n y)" by auto
    2.55 -      moreover have "n y <= Max ((%(y, x). n y) ` r)"
    2.56 -        using y `finite r` by (auto intro!: Max_ge)
    2.57 -      note bacc_mono[OF this, of r]
    2.58 -      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
    2.59 -    qed
    2.60 -    then show ?case
    2.61 -      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
    2.62 -  qed
    2.63 -  then show "x : (UN n. bacc r n)" by auto
    2.64 -qed
    2.65 -
    2.66 -lemma acc_bacc_eq:
    2.67 -  fixes A :: "('a :: finite \<times> 'a) set"
    2.68 -  assumes "finite A"
    2.69 -  shows "Wellfounded.acc A = bacc A (card (UNIV :: 'a set))"
    2.70 -  using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
    2.71 -
    2.72  
    2.73  subsection {* More on injections, bijections, and inverses *}
    2.74  
     3.1 --- a/src/HOL/Set_Interval.thy	Mon Jan 20 22:24:48 2014 +0100
     3.2 +++ b/src/HOL/Set_Interval.thy	Mon Jan 20 23:07:23 2014 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4  header {* Set intervals *}
     3.5  
     3.6  theory Set_Interval
     3.7 -imports Nat_Transfer
     3.8 +imports Lattices_Big Nat_Transfer
     3.9  begin
    3.10  
    3.11  context ord