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
```