src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
changeset 63561 fba08009ff3e
parent 63540 f8652d0534fa
child 63562 6f7a9d48a828
     1.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Thu Jul 28 20:39:51 2016 +0200
     1.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 29 09:49:23 2016 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
     1.5  
     1.6  theory Bourbaki_Witt_Fixpoint
     1.7 -  imports Main
     1.8 +  imports While_Combinator
     1.9  begin
    1.10  
    1.11  lemma ChainsI [intro?]:
    1.12 @@ -18,8 +18,8 @@
    1.13  lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
    1.14  by(auto simp add: Chains_def)
    1.15  
    1.16 -lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
    1.17 -  unfolding Field_def by auto
    1.18 +lemma in_ChainsD: "\<lbrakk> M \<in> Chains r; x \<in> M; y \<in> M \<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r"
    1.19 +unfolding Chains_def by fast
    1.20  
    1.21  lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
    1.22  by(auto simp add: Chains_def intro: FieldI1 FieldI2)
    1.23 @@ -245,7 +245,7 @@
    1.24  
    1.25  end
    1.26  
    1.27 -lemma fixp_induct [case_names adm base step]:
    1.28 +lemma fixp_above_induct [case_names adm base step]:
    1.29    assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P"
    1.30    and base: "P a"
    1.31    and step: "\<And>x. P x \<Longrightarrow> P (f x)"
    1.32 @@ -264,4 +264,142 @@
    1.33  
    1.34  end
    1.35  
    1.36 +subsection \<open>Connect with the while combinator for executability on chain-finite lattices.\<close>
    1.37 +
    1.38 +context bourbaki_witt_fixpoint begin
    1.39 +
    1.40 +lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}. }\<close>
    1.41 +  assumes "M \<in> Chains leq"
    1.42 +  and "M \<noteq> {}"
    1.43 +  and "finite M"
    1.44 +  shows "lub M \<in> M"
    1.45 +using assms(3,1,2)
    1.46 +proof induction
    1.47 +  case empty thus ?case by simp
    1.48 +next
    1.49 +  case (insert x M)
    1.50 +  note chain = \<open>insert x M \<in> Chains leq\<close>
    1.51 +  show ?case
    1.52 +  proof(cases "M = {}")
    1.53 +    case True thus ?thesis
    1.54 +      using chain in_ChainsD leq_antisym lub_least lub_upper by fastforce
    1.55 +  next
    1.56 +    case False
    1.57 +    from chain have chain': "M \<in> Chains leq"
    1.58 +      using in_Chains_subset subset_insertI by blast
    1.59 +    hence "lub M \<in> M" using False by(rule insert.IH)
    1.60 +    show ?thesis
    1.61 +    proof(cases "(x, lub M) \<in> leq")
    1.62 +      case True
    1.63 +      have "(lub (insert x M), lub M) \<in> leq" using chain
    1.64 +        by (rule lub_least) (auto simp: True intro: lub_upper[OF chain'])
    1.65 +      with False have "lub (insert x M) = lub M"
    1.66 +        using lub_upper[OF chain] lub_least[OF chain'] by (blast intro: leq_antisym)
    1.67 +      with \<open>lub M \<in> M\<close> show ?thesis by simp
    1.68 +    next
    1.69 +      case False
    1.70 +      with in_ChainsD[OF chain, of x "lub M"] \<open>lub M \<in> M\<close>
    1.71 +      have "lub (insert x M) = x"
    1.72 +        by - (rule leq_antisym, (blast intro: FieldI2 chain chain' insert.prems(2) leq_refl leq_trans lub_least lub_upper)+)
    1.73 +      thus ?thesis by simp
    1.74 +    qed
    1.75 +  qed
    1.76 +qed
    1.77 +
    1.78 +lemma fun_pow_iterates_above: "(f ^^ k) a \<in> iterates_above a"
    1.79 +using iterates_above.base iterates_above.step by (induct k) simp_all
    1.80 +
    1.81 +lemma chfin_iterates_above_fun_pow:
    1.82 +  assumes "x \<in> iterates_above a"
    1.83 +  assumes "\<forall>M \<in> Chains leq. finite M"
    1.84 +  shows "\<exists>j. x = (f ^^ j) a"
    1.85 +using assms(1)
    1.86 +proof induct
    1.87 +  case base then show ?case by (simp add: exI[where x=0])
    1.88 +next
    1.89 +  case (step x) then obtain j where "x = (f ^^ j) a" by blast
    1.90 +  with step(1) show ?case by (simp add: exI[where x="Suc j"])
    1.91 +next
    1.92 +  case (Sup M) with in_Chains_finite assms(2) show ?case by blast
    1.93 +qed
    1.94 +
    1.95 +lemma Chain_finite_iterates_above_fun_pow_iff:
    1.96 +  assumes "\<forall>M \<in> Chains leq. finite M"
    1.97 +  shows "x \<in> iterates_above a \<longleftrightarrow> (\<exists>j. x = (f ^^ j) a)"
    1.98 +using chfin_iterates_above_fun_pow fun_pow_iterates_above assms by blast
    1.99 +
   1.100 +lemma fixp_above_Kleene_iter_ex:
   1.101 +  assumes "(\<forall>M \<in> Chains leq. finite M)"
   1.102 +  obtains k where "fixp_above a = (f ^^ k) a"
   1.103 +using assms by atomize_elim (simp add: chfin_iterates_above_fun_pow fixp_iterates_above)
   1.104 +
   1.105 +context fixes a assumes a: "a \<in> Field leq" begin
   1.106 +
   1.107 +lemma funpow_Field_leq: "(f ^^ k) a \<in> Field leq"
   1.108 +using a by (induct k) (auto intro: increasing FieldI2)
   1.109 +
   1.110 +lemma funpow_prefix: "j < k \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
   1.111 +proof(induct k)
   1.112 +  case (Suc k)
   1.113 +  with leq_trans[OF _ increasing[OF funpow_Field_leq]] funpow_Field_leq increasing a
   1.114 +  show ?case by simp (metis less_antisym)
   1.115 +qed simp
   1.116 +
   1.117 +lemma funpow_suffix: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ (j + k)) a, (f ^^ k) a) \<in> leq"
   1.118 +using funpow_Field_leq
   1.119 +by (induct j) (simp_all del: funpow.simps add: funpow_Suc_right funpow_add leq_refl)
   1.120 +
   1.121 +lemma funpow_stability: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
   1.122 +using funpow_prefix funpow_suffix[where j="j - k" and k=k] by (cases "j < k") simp_all
   1.123 +
   1.124 +lemma funpow_in_Chains: "{(f ^^ k) a |k. True} \<in> Chains leq"
   1.125 +using chain_iterates_above[OF a] fun_pow_iterates_above
   1.126 +by (blast intro: ChainsI dest: in_ChainsD)
   1.127 +
   1.128 +lemma fixp_above_Kleene_iter:
   1.129 +  assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
   1.130 +  assumes "(f ^^ Suc k) a = (f ^^ k) a"
   1.131 +  shows "fixp_above a = (f ^^ k) a"
   1.132 +proof(rule leq_antisym)
   1.133 +  show "(fixp_above a, (f ^^ k) a) \<in> leq" using assms a
   1.134 +    by(auto simp add: fixp_above_def chain_iterates_above Chain_finite_iterates_above_fun_pow_iff funpow_stability[OF assms(2)] intro!: lub_least intro: iterates_above.base)
   1.135 +  show "((f ^^ k) a, fixp_above a) \<in> leq" using a
   1.136 +    by(auto simp add: fixp_above_def chain_iterates_above fun_pow_iterates_above intro!: lub_upper)
   1.137 +qed
   1.138 +
   1.139 +context assumes chfin: "\<forall>M \<in> Chains leq. finite M" begin
   1.140 +
   1.141 +lemma Chain_finite_wf: "wf {(f ((f ^^ k) a), (f ^^ k) a) |k. f ((f ^^ k) a) \<noteq> (f ^^ k) a}"
   1.142 +apply(rule wf_measure[where f="\<lambda>b. card {(f ^^ j) a |j. (b, (f ^^ j) a) \<in> leq}", THEN wf_subset])
   1.143 +apply(auto simp: set_eq_iff intro!: psubset_card_mono[OF finite_subset[OF _ bspec[OF chfin funpow_in_Chains]]])
   1.144 +apply(metis funpow_Field_leq increasing leq_antisym leq_trans leq_refl)+
   1.145 +done
   1.146 +
   1.147 +lemma while_option_finite_increasing: "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
   1.148 +by(rule wf_rel_while_option_Some[OF Chain_finite_wf, where P="\<lambda>A. (\<exists>k. A = (f ^^ k) a) \<and> (A, f A) \<in> leq" and s="a"])
   1.149 +  (auto simp: a increasing chfin FieldI2 chfin_iterates_above_fun_pow fun_pow_iterates_above iterates_above.step intro: exI[where x=0])
   1.150 +
   1.151 +lemma fixp_above_the_while_option: "fixp_above a = the (while_option (\<lambda>A. f A \<noteq> A) f a)"
   1.152 +proof -
   1.153 +  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
   1.154 +    using while_option_finite_increasing by blast
   1.155 +  with while_option_stop2[OF this] fixp_above_Kleene_iter[OF chfin]
   1.156 +  show ?thesis by fastforce
   1.157 +qed
   1.158 +
   1.159 +lemma fixp_above_conv_while: "fixp_above a = while (\<lambda>A. f A \<noteq> A) f a"
   1.160 +unfolding while_def by (rule fixp_above_the_while_option)
   1.161 +
   1.162  end
   1.163 +
   1.164 +end
   1.165 +
   1.166 +end
   1.167 +
   1.168 +lemma bourbaki_witt_fixpoint_complete_latticeI:
   1.169 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   1.170 +  assumes "\<And>x. x \<le> f x"
   1.171 +  shows "bourbaki_witt_fixpoint Sup {(x, y). x \<le> y} f"
   1.172 +by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least)
   1.173 +
   1.174 +end
   1.175 \ No newline at end of file