add formalisation of Bourbaki-Witt fixpoint theorem
authorAndreas Lochbihler
Tue Dec 01 12:35:11 2015 +0100 (2015-12-01)
changeset 61766507b39df1a57
parent 61765 13ca8f4f6907
child 61767 f58d75535f66
add formalisation of Bourbaki-Witt fixpoint theorem
CONTRIBUTORS
NEWS
src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
src/HOL/Library/Library.thy
     1.1 --- a/CONTRIBUTORS	Tue Dec 01 12:28:02 2015 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Dec 01 12:35:11 2015 +0100
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* Autumn 2015: Andreas Lochbihler
     1.8 +  Bourbaki-Witt fixpoint theorem for increasing functions on
     1.9 +  chain-complete partial orders.
    1.10 +
    1.11  * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
    1.12    A large number of additional binomial identities.
    1.13  
     2.1 --- a/NEWS	Tue Dec 01 12:28:02 2015 +0100
     2.2 +++ b/NEWS	Tue Dec 01 12:35:11 2015 +0100
     2.3 @@ -581,6 +581,10 @@
     2.4      less_eq_multiset_def
     2.5      INCOMPATIBILITY
     2.6  
     2.7 +* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt
     2.8 +fixpoint theorem for increasing functions in chain-complete partial
     2.9 +orders.
    2.10 +
    2.11  * Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's
    2.12  integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
    2.13  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Dec 01 12:35:11 2015 +0100
     3.3 @@ -0,0 +1,252 @@
     3.4 +(* Title: Bourbaki_Witt_Fixpoint.thy
     3.5 +   Author: Andreas Lochbihler, ETH Zurich *)
     3.6 +
     3.7 +section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
     3.8 +
     3.9 +theory Bourbaki_Witt_Fixpoint imports Main begin
    3.10 +
    3.11 +lemma ChainsI [intro?]:
    3.12 +  "(\<And>a b. \<lbrakk> a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> (a, b) \<in> r \<or> (b, a) \<in> r) \<Longrightarrow> Y \<in> Chains r"
    3.13 +unfolding Chains_def by blast
    3.14 +
    3.15 +lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
    3.16 +by(auto simp add: Chains_def)
    3.17 +
    3.18 +lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
    3.19 +  unfolding Field_def by auto
    3.20 +
    3.21 +lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
    3.22 +by(auto simp add: Chains_def intro: FieldI1 FieldI2)
    3.23 +
    3.24 +lemma partial_order_on_trans:
    3.25 +  "\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r"
    3.26 +by(auto simp add: order_on_defs dest: transD)
    3.27 +
    3.28 +locale bourbaki_witt_fixpoint =
    3.29 +  fixes lub :: "'a set \<Rightarrow> 'a"
    3.30 +  and leq :: "('a \<times> 'a) set"
    3.31 +  and f :: "'a \<Rightarrow> 'a"
    3.32 +  assumes po: "Partial_order leq"
    3.33 +  and lub_least: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> (x, z) \<in> leq \<rbrakk> \<Longrightarrow> (lub M, z) \<in> leq"
    3.34 +  and lub_upper: "\<lbrakk> M \<in> Chains leq; x \<in> M \<rbrakk> \<Longrightarrow> (x, lub M) \<in> leq"
    3.35 +  and lub_in_Field: "\<lbrakk> M \<in> Chains leq; M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> Field leq"
    3.36 +  and increasing: "\<And>x. x \<in> Field leq \<Longrightarrow> (x, f x) \<in> leq"
    3.37 +begin
    3.38 +
    3.39 +lemma leq_trans: "\<lbrakk> (x, y) \<in> leq; (y, z) \<in> leq \<rbrakk> \<Longrightarrow> (x, z) \<in> leq"
    3.40 +by(rule partial_order_on_trans[OF po])
    3.41 +
    3.42 +lemma leq_refl: "x \<in> Field leq \<Longrightarrow> (x, x) \<in> leq"
    3.43 +using po by(simp add: order_on_defs refl_on_def)
    3.44 +
    3.45 +lemma leq_antisym: "\<lbrakk> (x, y) \<in> leq; (y, x) \<in> leq \<rbrakk> \<Longrightarrow> x = y"
    3.46 +using po by(simp add: order_on_defs antisym_def)
    3.47 +
    3.48 +inductive_set iterates_above :: "'a \<Rightarrow> 'a set"
    3.49 +  for a
    3.50 +where
    3.51 +  base: "a \<in> iterates_above a"
    3.52 +| step: "x \<in> iterates_above a \<Longrightarrow> f x \<in> iterates_above a"
    3.53 +| Sup: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above a \<rbrakk> \<Longrightarrow> lub M \<in> iterates_above a"
    3.54 +
    3.55 +definition fixp_above :: "'a \<Rightarrow> 'a"
    3.56 +where "fixp_above a = lub (iterates_above a)"
    3.57 +
    3.58 +context 
    3.59 +  notes leq_refl [intro!, simp]
    3.60 +  and base [intro]
    3.61 +  and step [intro]
    3.62 +  and Sup [intro]
    3.63 +  and leq_trans [trans]
    3.64 +begin
    3.65 +
    3.66 +lemma iterates_above_le_f: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> (x, f x) \<in> leq"
    3.67 +by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+
    3.68 +
    3.69 +lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq"
    3.70 +by(drule (1) iterates_above_le_f)(rule FieldI1)
    3.71 +
    3.72 +lemma iterates_above_ge:
    3.73 +  assumes y: "y \<in> iterates_above a"
    3.74 +  and a: "a \<in> Field leq"
    3.75 +  shows "(a, y) \<in> leq"
    3.76 +using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper])
    3.77 +
    3.78 +lemma iterates_above_lub:
    3.79 +  assumes M: "M \<in> Chains leq"
    3.80 +  and nempty: "M \<noteq> {}"
    3.81 +  and upper: "\<And>y. y \<in> M \<Longrightarrow> \<exists>z \<in> M. (y, z) \<in> leq \<and> z \<in> iterates_above a"
    3.82 +  shows "lub M \<in> iterates_above a"
    3.83 +proof -
    3.84 +  let ?M = "M \<inter> iterates_above a"
    3.85 +  from M have M': "?M \<in> Chains leq" by(rule in_Chains_subset)simp
    3.86 +  have "?M \<noteq> {}" using nempty by(auto dest: upper)
    3.87 +  with M' have "lub ?M \<in> iterates_above a" by(rule Sup) blast
    3.88 +  also have "lub ?M = lub M" using nempty
    3.89 +    by(intro leq_antisym)(blast intro!: lub_least[OF M] lub_least[OF M'] intro: lub_upper[OF M'] lub_upper[OF M] leq_trans dest: upper)+
    3.90 +  finally show ?thesis .
    3.91 +qed
    3.92 +
    3.93 +lemma iterates_above_successor:
    3.94 +  assumes y: "y \<in> iterates_above a"
    3.95 +  and a: "a \<in> Field leq"
    3.96 +  shows "y = a \<or> y \<in> iterates_above (f a)"
    3.97 +using y
    3.98 +proof induction
    3.99 +  case base thus ?case by simp
   3.100 +next
   3.101 +  case (step x) thus ?case by auto
   3.102 +next
   3.103 +  case (Sup M)
   3.104 +  show ?case
   3.105 +  proof(cases "\<exists>x. M \<subseteq> {x}")
   3.106 +    case True
   3.107 +    with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto
   3.108 +    have "lub M = y"
   3.109 +      by(rule leq_antisym)(auto intro!: lub_upper Sup lub_least ChainsI simp add: a M Sup.hyps(3)[of y, THEN iterates_above_Field] dest: iterates_above_Field)
   3.110 +    with Sup.IH[of y] M show ?thesis by simp
   3.111 +  next
   3.112 +    case False
   3.113 +    from Sup(1-2) have "lub M \<in> iterates_above (f a)"
   3.114 +    proof(rule iterates_above_lub)
   3.115 +      fix y
   3.116 +      assume y: "y \<in> M"
   3.117 +      from Sup.IH[OF this] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (f a)"
   3.118 +      proof
   3.119 +        assume "y = a"
   3.120 +        from y False obtain z where z: "z \<in> M" and neq: "y \<noteq> z" by (metis insertI1 subsetI)
   3.121 +        with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
   3.122 +        show ?thesis by(auto dest: iterates_above_ge intro: a)
   3.123 +      next
   3.124 +        assume "y \<in> iterates_above (f a)"
   3.125 +        moreover with increasing[OF a] have "y \<in> Field leq"
   3.126 +          by(auto dest!: iterates_above_Field intro: FieldI2)
   3.127 +        ultimately show ?thesis using y by(auto)
   3.128 +      qed
   3.129 +    qed
   3.130 +    thus ?thesis by simp
   3.131 +  qed
   3.132 +qed
   3.133 +
   3.134 +lemma iterates_above_Sup_aux:
   3.135 +  assumes M: "M \<in> Chains leq" "M \<noteq> {}"
   3.136 +  and M': "M' \<in> Chains leq" "M' \<noteq> {}"
   3.137 +  and comp: "\<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x"
   3.138 +  shows "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
   3.139 +proof(cases "\<exists>x \<in> M. x \<in> iterates_above (lub M')")
   3.140 +  case True
   3.141 +  then obtain x where x: "x \<in> M" "x \<in> iterates_above (lub M')" by blast
   3.142 +  have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field)
   3.143 +  have "lub M \<in> iterates_above (lub M')" using M
   3.144 +  proof(rule iterates_above_lub)
   3.145 +    fix y
   3.146 +    assume y: "y \<in> M"
   3.147 +    from comp[OF y] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (lub M')"
   3.148 +    proof
   3.149 +      assume "y \<in> iterates_above (lub M')"
   3.150 +      from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast
   3.151 +    next
   3.152 +      assume "lub M' \<in> iterates_above y"
   3.153 +      hence "(y, lub M') \<in> leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge)
   3.154 +      also have "(lub M', x) \<in> leq" using x(2) lub_M' by(rule iterates_above_ge)
   3.155 +      finally show ?thesis using x by blast
   3.156 +    qed
   3.157 +  qed
   3.158 +  thus ?thesis ..
   3.159 +next
   3.160 +  case False
   3.161 +  have "(lub M, lub M') \<in> leq" using M
   3.162 +  proof(rule lub_least)
   3.163 +    fix x
   3.164 +    assume x: "x \<in> M"
   3.165 +    from comp[OF x] x False have "lub M' \<in> iterates_above x" by auto
   3.166 +    moreover from M(1) x have "x \<in> Field leq" by(rule Chains_FieldD)
   3.167 +    ultimately show "(x, lub M') \<in> leq" by(rule iterates_above_ge)
   3.168 +  qed
   3.169 +  thus ?thesis ..
   3.170 +qed
   3.171 +
   3.172 +lemma iterates_above_triangle:
   3.173 +  assumes x: "x \<in> iterates_above a"
   3.174 +  and y: "y \<in> iterates_above a"
   3.175 +  and a: "a \<in> Field leq"
   3.176 +  shows "x \<in> iterates_above y \<or> y \<in> iterates_above x"
   3.177 +using x y
   3.178 +proof(induction arbitrary: y)
   3.179 +  case base then show ?case by simp
   3.180 +next
   3.181 +  case (step x) thus ?case using a
   3.182 +    by(auto dest: iterates_above_successor intro: iterates_above_Field)
   3.183 +next
   3.184 +  case x: (Sup M)
   3.185 +  hence lub: "lub M \<in> iterates_above a" by blast
   3.186 +  from \<open>y \<in> iterates_above a\<close> show ?case
   3.187 +  proof(induction)
   3.188 +    case base show ?case using lub by simp
   3.189 +  next
   3.190 +    case (step y) thus ?case using a
   3.191 +      by(auto dest: iterates_above_successor intro: iterates_above_Field)
   3.192 +  next
   3.193 +    case y: (Sup M')
   3.194 +    hence lub': "lub M' \<in> iterates_above a" by blast
   3.195 +    have *: "x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" if "x \<in> M" for x
   3.196 +      using that lub' by(rule x.IH)
   3.197 +    with x(1-2) y(1-2) have "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
   3.198 +      by(rule iterates_above_Sup_aux)
   3.199 +    moreover from y(1-2) x(1-2) have "(lub M', lub M) \<in> leq \<or> lub M' \<in> iterates_above (lub M)"
   3.200 +      by(rule iterates_above_Sup_aux)(blast dest: y.IH)
   3.201 +    ultimately show ?case by(auto 4 3 dest: leq_antisym)
   3.202 +  qed
   3.203 +qed
   3.204 +
   3.205 +lemma chain_iterates_above: 
   3.206 +  assumes a: "a \<in> Field leq"
   3.207 +  shows "iterates_above a \<in> Chains leq" (is "?C \<in> _")
   3.208 +proof (rule ChainsI)
   3.209 +  fix x y
   3.210 +  assume "x \<in> ?C" "y \<in> ?C"
   3.211 +  hence "x \<in> iterates_above y \<or> y \<in> iterates_above x" using a by(rule iterates_above_triangle)
   3.212 +  moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field)
   3.213 +  moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field)
   3.214 +  ultimately show "(x, y) \<in> leq \<or> (y, x) \<in> leq" by(auto dest: iterates_above_ge)
   3.215 +qed
   3.216 +
   3.217 +lemma fixp_iterates_above: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> iterates_above a"
   3.218 +unfolding fixp_above_def by(rule iterates_above.Sup)(blast intro: chain_iterates_above)+
   3.219 +
   3.220 +lemma
   3.221 +  assumes b: "b \<in> iterates_above a"
   3.222 +  and fb: "f b = b"
   3.223 +  and x: "x \<in> iterates_above a"
   3.224 +  and a: "a \<in> Field leq"
   3.225 +  shows "b \<in> iterates_above x"
   3.226 +using x
   3.227 +proof(induction)
   3.228 +  case base show ?case using b by simp
   3.229 +next
   3.230 +  case (step x)
   3.231 +  from step.hyps a have "x \<in> Field leq" by(rule iterates_above_Field)
   3.232 +  from iterates_above_successor[OF step.IH this] fb
   3.233 +  show ?case by(auto)
   3.234 +next
   3.235 +  case (Sup M)
   3.236 +  oops
   3.237 +
   3.238 +lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq"
   3.239 +using fixp_iterates_above by(rule iterates_above_Field)
   3.240 +
   3.241 +lemma fixp_above_unfold:
   3.242 +  assumes a: "a \<in> Field leq"
   3.243 +  shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a")
   3.244 +proof(rule leq_antisym)
   3.245 +  show "(?a, f ?a) \<in> leq" using fixp_above_Field[OF a] by(rule increasing)
   3.246 +  
   3.247 +  have "f ?a \<in> iterates_above a" using fixp_iterates_above[OF a] by(rule iterates_above.step)
   3.248 +  with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq" unfolding fixp_above_def by(rule lub_upper)
   3.249 +qed
   3.250 +
   3.251 +end
   3.252 +
   3.253 +end
   3.254 +
   3.255 +end
   3.256 \ No newline at end of file
     4.1 --- a/src/HOL/Library/Library.thy	Tue Dec 01 12:28:02 2015 +0100
     4.2 +++ b/src/HOL/Library/Library.thy	Tue Dec 01 12:35:11 2015 +0100
     4.3 @@ -6,6 +6,7 @@
     4.4    Bit
     4.5    BNF_Axiomatization
     4.6    Boolean_Algebra
     4.7 +  Bourbaki_Witt_Fixpoint
     4.8    Char_ord
     4.9    Code_Test
    4.10    ContNotDenum