src/HOL/Enum.thy
changeset 46352 73b03235799a
parent 46336 39fe503602fb
child 46357 2795607a1f40
     1.1 --- a/src/HOL/Enum.thy	Sat Jan 28 10:35:52 2012 +0100
     1.2 +++ b/src/HOL/Enum.thy	Sat Jan 28 12:05:26 2012 +0100
     1.3 @@ -742,6 +742,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
     1.8 +
     1.9  subsection {* An executable THE operator on finite types *}
    1.10  
    1.11  definition
    1.12 @@ -785,10 +787,158 @@
    1.13    "Collect P = set (filter P enum)"
    1.14  by (auto simp add: enum_UNIV)
    1.15  
    1.16 -subsection {* Closing up *}
    1.17 +
    1.18 +subsection {* Executable accessible part *}
    1.19 +(* FIXME: should be moved somewhere else !? *)
    1.20 +
    1.21 +subsubsection {* Finite monotone eventually stable sequences *}
    1.22 +
    1.23 +lemma finite_mono_remains_stable_implies_strict_prefix:
    1.24 +  fixes f :: "nat \<Rightarrow> 'a::order"
    1.25 +  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.26 +  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.27 +  using assms
    1.28 +proof -
    1.29 +  have "\<exists>n. f n = f (Suc n)"
    1.30 +  proof (rule ccontr)
    1.31 +    assume "\<not> ?thesis"
    1.32 +    then have "\<And>n. f n \<noteq> f (Suc n)" by auto
    1.33 +    then have "\<And>n. f n < f (Suc n)"
    1.34 +      using  `mono f` by (auto simp: le_less mono_iff_le_Suc)
    1.35 +    with lift_Suc_mono_less_iff[of f]
    1.36 +    have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
    1.37 +    then have "inj f"
    1.38 +      by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
    1.39 +    with `finite (range f)` have "finite (UNIV::nat set)"
    1.40 +      by (rule finite_imageD)
    1.41 +    then show False by simp
    1.42 +  qed
    1.43 +  then guess n .. note n = this
    1.44 +  def N \<equiv> "LEAST n. f n = f (Suc n)"
    1.45 +  have N: "f N = f (Suc N)"
    1.46 +    unfolding N_def using n by (rule LeastI)
    1.47 +  show ?thesis
    1.48 +  proof (intro exI[of _ N] conjI allI impI)
    1.49 +    fix n assume "N \<le> n"
    1.50 +    then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
    1.51 +    proof (induct rule: dec_induct)
    1.52 +      case (step n) then show ?case
    1.53 +        using eq[rule_format, of "n - 1"] N
    1.54 +        by (cases n) (auto simp add: le_Suc_eq)
    1.55 +    qed simp
    1.56 +    from this[of n] `N \<le> n` show "f N = f n" by auto
    1.57 +  next
    1.58 +    fix n m :: nat assume "m < n" "n \<le> N"
    1.59 +    then show "f m < f n"
    1.60 +    proof (induct rule: less_Suc_induct[consumes 1])
    1.61 +      case (1 i)
    1.62 +      then have "i < N" by simp
    1.63 +      then have "f i \<noteq> f (Suc i)"
    1.64 +        unfolding N_def by (rule not_less_Least)
    1.65 +      with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
    1.66 +    qed auto
    1.67 +  qed
    1.68 +qed
    1.69 +
    1.70 +lemma finite_mono_strict_prefix_implies_finite_fixpoint:
    1.71 +  fixes f :: "nat \<Rightarrow> 'a set"
    1.72 +  assumes S: "\<And>i. f i \<subseteq> S" "finite S"
    1.73 +    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.74 +  shows "f (card S) = (\<Union>n. f n)"
    1.75 +proof -
    1.76 +  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.77  
    1.78 -hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
    1.79 +  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
    1.80 +    proof (induct i)
    1.81 +      case 0 then show ?case by simp
    1.82 +    next
    1.83 +      case (Suc i)
    1.84 +      with inj[rule_format, of "Suc i" i]
    1.85 +      have "(f i) \<subset> (f (Suc i))" by auto
    1.86 +      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
    1.87 +      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
    1.88 +      with Suc show ?case using inj by auto
    1.89 +    qed
    1.90 +  }
    1.91 +  then have "N \<le> card (f N)" by simp
    1.92 +  also have "\<dots> \<le> card S" using S by (intro card_mono)
    1.93 +  finally have "f (card S) = f N" using eq by auto
    1.94 +  then show ?thesis using eq inj[rule_format, of N]
    1.95 +    apply auto
    1.96 +    apply (case_tac "n < N")
    1.97 +    apply (auto simp: not_less)
    1.98 +    done
    1.99 +qed
   1.100 +
   1.101 +subsubsection {* Bounded accessible part *}
   1.102 +
   1.103 +fun bacc :: "('a * 'a) set => nat => 'a set" 
   1.104 +where
   1.105 +  "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
   1.106 +| "bacc r (Suc n) = (bacc r n Un {x. \<forall> y. (y, x) : r --> y : bacc r n})"
   1.107 +
   1.108 +lemma bacc_subseteq_acc:
   1.109 +  "bacc r n \<subseteq> acc r"
   1.110 +by (induct n) (auto intro: acc.intros)
   1.111  
   1.112 +lemma bacc_mono:
   1.113 +  "n <= m ==> bacc r n \<subseteq> bacc r m"
   1.114 +by (induct rule: dec_induct) auto
   1.115 +  
   1.116 +lemma bacc_upper_bound:
   1.117 +  "bacc (r :: ('a * 'a) set)  (card (UNIV :: ('a :: enum) set)) = (UN n. bacc r n)"
   1.118 +proof -
   1.119 +  have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
   1.120 +  moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
   1.121 +  moreover have "finite (range (bacc r))" by auto
   1.122 +  ultimately show ?thesis
   1.123 +   by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
   1.124 +     (auto intro: finite_mono_remains_stable_implies_strict_prefix  simp add: enum_UNIV)
   1.125 +qed
   1.126 +
   1.127 +lemma acc_subseteq_bacc:
   1.128 +  assumes "finite r"
   1.129 +  shows "acc r \<subseteq> (UN n. bacc r n)"
   1.130 +proof
   1.131 +  fix x
   1.132 +  assume "x : acc r"
   1.133 +  from this have "\<exists> n. x : bacc r n"
   1.134 +  proof (induct x arbitrary: n rule: acc.induct)
   1.135 +    case (accI x)
   1.136 +    from accI have "\<forall> y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
   1.137 +    from choice[OF this] guess n .. note n = this
   1.138 +    have "\<exists> n. \<forall>y. (y, x) : r --> y : bacc r n"
   1.139 +    proof (safe intro!: exI[of _ "Max ((%(y,x). n y)`r)"])
   1.140 +      fix y assume y: "(y, x) : r"
   1.141 +      with n have "y : bacc r (n y)" by auto
   1.142 +      moreover have "n y <= Max ((%(y, x). n y) ` r)"
   1.143 +        using y `finite r` by (auto intro!: Max_ge)
   1.144 +      note bacc_mono[OF this, of r]
   1.145 +      ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
   1.146 +    qed
   1.147 +    from this guess n ..
   1.148 +    from this show ?case
   1.149 +      by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
   1.150 +  qed
   1.151 +  thus "x : (UN n. bacc r n)" by auto
   1.152 +qed
   1.153 +
   1.154 +lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))"
   1.155 +by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound finite_set order_eq_iff)
   1.156 +
   1.157 +definition 
   1.158 +  [code del]: "card_UNIV = card UNIV"
   1.159 +
   1.160 +lemma [code]:
   1.161 +  "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
   1.162 +unfolding card_UNIV_def enum_UNIV ..
   1.163 +
   1.164 +declare acc_bacc_eq[folded card_UNIV_def, code]
   1.165 +
   1.166 +lemma [code_unfold]: "accp r = (%x. x : acc {(x, y). r x y})"
   1.167 +unfolding acc_def by simp
   1.168 +
   1.169 +subsection {* Closing up *}
   1.170  
   1.171  hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
   1.172  hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl