src/HOL/Enum.thy
changeset 55088 57c82e01022b
parent 54890 cb892d835803
child 57247 8191ccf6a1bd
     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 -