src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
author Andreas Lochbihler
Fri Jul 29 09:49:23 2016 +0200 (2016-07-29)
changeset 63561 fba08009ff3e
parent 63540 f8652d0534fa
child 63562 6f7a9d48a828
permissions -rw-r--r--
add lemmas contributed by Peter Gammie
     1 (*  Title:      HOL/Library/Bourbaki_Witt_Fixpoint.thy
     2     Author:     Andreas Lochbihler, ETH Zurich
     3 
     4   Follows G. Smolka, S. Schäfer and C. Doczkal: Transfinite Constructions in
     5   Classical Type Theory. ITP 2015
     6 *)
     7 
     8 section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
     9 
    10 theory Bourbaki_Witt_Fixpoint
    11   imports While_Combinator
    12 begin
    13 
    14 lemma ChainsI [intro?]:
    15   "(\<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"
    16 unfolding Chains_def by blast
    17 
    18 lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
    19 by(auto simp add: Chains_def)
    20 
    21 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"
    22 unfolding Chains_def by fast
    23 
    24 lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
    25 by(auto simp add: Chains_def intro: FieldI1 FieldI2)
    26 
    27 lemma in_Chains_conv_chain: "M \<in> Chains r \<longleftrightarrow> Complete_Partial_Order.chain (\<lambda>x y. (x, y) \<in> r) M"
    28 by(simp add: Chains_def chain_def)
    29 
    30 lemma partial_order_on_trans:
    31   "\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r"
    32 by(auto simp add: order_on_defs dest: transD)
    33 
    34 locale bourbaki_witt_fixpoint =
    35   fixes lub :: "'a set \<Rightarrow> 'a"
    36   and leq :: "('a \<times> 'a) set"
    37   and f :: "'a \<Rightarrow> 'a"
    38   assumes po: "Partial_order leq"
    39   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"
    40   and lub_upper: "\<lbrakk> M \<in> Chains leq; x \<in> M \<rbrakk> \<Longrightarrow> (x, lub M) \<in> leq"
    41   and lub_in_Field: "\<lbrakk> M \<in> Chains leq; M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> Field leq"
    42   and increasing: "\<And>x. x \<in> Field leq \<Longrightarrow> (x, f x) \<in> leq"
    43 begin
    44 
    45 lemma leq_trans: "\<lbrakk> (x, y) \<in> leq; (y, z) \<in> leq \<rbrakk> \<Longrightarrow> (x, z) \<in> leq"
    46 by(rule partial_order_on_trans[OF po])
    47 
    48 lemma leq_refl: "x \<in> Field leq \<Longrightarrow> (x, x) \<in> leq"
    49 using po by(simp add: order_on_defs refl_on_def)
    50 
    51 lemma leq_antisym: "\<lbrakk> (x, y) \<in> leq; (y, x) \<in> leq \<rbrakk> \<Longrightarrow> x = y"
    52 using po by(simp add: order_on_defs antisym_def)
    53 
    54 inductive_set iterates_above :: "'a \<Rightarrow> 'a set"
    55   for a
    56 where
    57   base: "a \<in> iterates_above a"
    58 | step: "x \<in> iterates_above a \<Longrightarrow> f x \<in> iterates_above a"
    59 | 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"
    60 
    61 definition fixp_above :: "'a \<Rightarrow> 'a"
    62 where "fixp_above a = (if a \<in> Field leq then lub (iterates_above a) else a)"
    63 
    64 lemma fixp_above_outside: "a \<notin> Field leq \<Longrightarrow> fixp_above a = a"
    65 by(simp add: fixp_above_def)
    66 
    67 lemma fixp_above_inside: "a \<in> Field leq \<Longrightarrow> fixp_above a = lub (iterates_above a)"
    68 by(simp add: fixp_above_def)
    69 
    70 context 
    71   notes leq_refl [intro!, simp]
    72   and base [intro]
    73   and step [intro]
    74   and Sup [intro]
    75   and leq_trans [trans]
    76 begin
    77 
    78 lemma iterates_above_le_f: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> (x, f x) \<in> leq"
    79 by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+
    80 
    81 lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq"
    82 by(drule (1) iterates_above_le_f)(rule FieldI1)
    83 
    84 lemma iterates_above_ge:
    85   assumes y: "y \<in> iterates_above a"
    86   and a: "a \<in> Field leq"
    87   shows "(a, y) \<in> leq"
    88 using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper])
    89 
    90 lemma iterates_above_lub:
    91   assumes M: "M \<in> Chains leq"
    92   and nempty: "M \<noteq> {}"
    93   and upper: "\<And>y. y \<in> M \<Longrightarrow> \<exists>z \<in> M. (y, z) \<in> leq \<and> z \<in> iterates_above a"
    94   shows "lub M \<in> iterates_above a"
    95 proof -
    96   let ?M = "M \<inter> iterates_above a"
    97   from M have M': "?M \<in> Chains leq" by(rule in_Chains_subset)simp
    98   have "?M \<noteq> {}" using nempty by(auto dest: upper)
    99   with M' have "lub ?M \<in> iterates_above a" by(rule Sup) blast
   100   also have "lub ?M = lub M" using nempty
   101     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)+
   102   finally show ?thesis .
   103 qed
   104 
   105 lemma iterates_above_successor:
   106   assumes y: "y \<in> iterates_above a"
   107   and a: "a \<in> Field leq"
   108   shows "y = a \<or> y \<in> iterates_above (f a)"
   109 using y
   110 proof induction
   111   case base thus ?case by simp
   112 next
   113   case (step x) thus ?case by auto
   114 next
   115   case (Sup M)
   116   show ?case
   117   proof(cases "\<exists>x. M \<subseteq> {x}")
   118     case True
   119     with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto
   120     have "lub M = y"
   121       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)
   122     with Sup.IH[of y] M show ?thesis by simp
   123   next
   124     case False
   125     from Sup(1-2) have "lub M \<in> iterates_above (f a)"
   126     proof(rule iterates_above_lub)
   127       fix y
   128       assume y: "y \<in> M"
   129       from Sup.IH[OF this] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (f a)"
   130       proof
   131         assume "y = a"
   132         from y False obtain z where z: "z \<in> M" and neq: "y \<noteq> z" by (metis insertI1 subsetI)
   133         with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
   134         show ?thesis by(auto dest: iterates_above_ge intro: a)
   135       next
   136         assume *: "y \<in> iterates_above (f a)"
   137         with increasing[OF a] have "y \<in> Field leq"
   138           by(auto dest!: iterates_above_Field intro: FieldI2)
   139         with * show ?thesis using y by auto
   140       qed
   141     qed
   142     thus ?thesis by simp
   143   qed
   144 qed
   145 
   146 lemma iterates_above_Sup_aux:
   147   assumes M: "M \<in> Chains leq" "M \<noteq> {}"
   148   and M': "M' \<in> Chains leq" "M' \<noteq> {}"
   149   and comp: "\<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x"
   150   shows "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
   151 proof(cases "\<exists>x \<in> M. x \<in> iterates_above (lub M')")
   152   case True
   153   then obtain x where x: "x \<in> M" "x \<in> iterates_above (lub M')" by blast
   154   have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field)
   155   have "lub M \<in> iterates_above (lub M')" using M
   156   proof(rule iterates_above_lub)
   157     fix y
   158     assume y: "y \<in> M"
   159     from comp[OF y] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (lub M')"
   160     proof
   161       assume "y \<in> iterates_above (lub M')"
   162       from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast
   163     next
   164       assume "lub M' \<in> iterates_above y"
   165       hence "(y, lub M') \<in> leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge)
   166       also have "(lub M', x) \<in> leq" using x(2) lub_M' by(rule iterates_above_ge)
   167       finally show ?thesis using x by blast
   168     qed
   169   qed
   170   thus ?thesis ..
   171 next
   172   case False
   173   have "(lub M, lub M') \<in> leq" using M
   174   proof(rule lub_least)
   175     fix x
   176     assume x: "x \<in> M"
   177     from comp[OF x] x False have "lub M' \<in> iterates_above x" by auto
   178     moreover from M(1) x have "x \<in> Field leq" by(rule Chains_FieldD)
   179     ultimately show "(x, lub M') \<in> leq" by(rule iterates_above_ge)
   180   qed
   181   thus ?thesis ..
   182 qed
   183 
   184 lemma iterates_above_triangle:
   185   assumes x: "x \<in> iterates_above a"
   186   and y: "y \<in> iterates_above a"
   187   and a: "a \<in> Field leq"
   188   shows "x \<in> iterates_above y \<or> y \<in> iterates_above x"
   189 using x y
   190 proof(induction arbitrary: y)
   191   case base then show ?case by simp
   192 next
   193   case (step x) thus ?case using a
   194     by(auto dest: iterates_above_successor intro: iterates_above_Field)
   195 next
   196   case x: (Sup M)
   197   hence lub: "lub M \<in> iterates_above a" by blast
   198   from \<open>y \<in> iterates_above a\<close> show ?case
   199   proof(induction)
   200     case base show ?case using lub by simp
   201   next
   202     case (step y) thus ?case using a
   203       by(auto dest: iterates_above_successor intro: iterates_above_Field)
   204   next
   205     case y: (Sup M')
   206     hence lub': "lub M' \<in> iterates_above a" by blast
   207     have *: "x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" if "x \<in> M" for x
   208       using that lub' by(rule x.IH)
   209     with x(1-2) y(1-2) have "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')"
   210       by(rule iterates_above_Sup_aux)
   211     moreover from y(1-2) x(1-2) have "(lub M', lub M) \<in> leq \<or> lub M' \<in> iterates_above (lub M)"
   212       by(rule iterates_above_Sup_aux)(blast dest: y.IH)
   213     ultimately show ?case by(auto 4 3 dest: leq_antisym)
   214   qed
   215 qed
   216 
   217 lemma chain_iterates_above: 
   218   assumes a: "a \<in> Field leq"
   219   shows "iterates_above a \<in> Chains leq" (is "?C \<in> _")
   220 proof (rule ChainsI)
   221   fix x y
   222   assume "x \<in> ?C" "y \<in> ?C"
   223   hence "x \<in> iterates_above y \<or> y \<in> iterates_above x" using a by(rule iterates_above_triangle)
   224   moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field)
   225   moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field)
   226   ultimately show "(x, y) \<in> leq \<or> (y, x) \<in> leq" by(auto dest: iterates_above_ge)
   227 qed
   228 
   229 lemma fixp_iterates_above: "fixp_above a \<in> iterates_above a"
   230 by(auto intro: chain_iterates_above simp add: fixp_above_def)
   231 
   232 lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq"
   233 using fixp_iterates_above by(rule iterates_above_Field)
   234 
   235 lemma fixp_above_unfold:
   236   assumes a: "a \<in> Field leq"
   237   shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a")
   238 proof(rule leq_antisym)
   239   show "(?a, f ?a) \<in> leq" using fixp_above_Field[OF a] by(rule increasing)
   240   
   241   have "f ?a \<in> iterates_above a" using fixp_iterates_above by(rule iterates_above.step)
   242   with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq"
   243     by(simp add: fixp_above_inside assms lub_upper)
   244 qed
   245 
   246 end
   247 
   248 lemma fixp_above_induct [case_names adm base step]:
   249   assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P"
   250   and base: "P a"
   251   and step: "\<And>x. P x \<Longrightarrow> P (f x)"
   252   shows "P (fixp_above a)"
   253 proof(cases "a \<in> Field leq")
   254   case True
   255   from adm chain_iterates_above[OF True]
   256   show ?thesis unfolding fixp_above_inside[OF True] in_Chains_conv_chain
   257   proof(rule ccpo.admissibleD)
   258     have "a \<in> iterates_above a" ..
   259     then show "iterates_above a \<noteq> {}" by(auto)
   260     show "P x" if "x \<in> iterates_above a" for x using that
   261       by induction(auto intro: base step simp add: in_Chains_conv_chain dest: ccpo.admissibleD[OF adm])
   262   qed
   263 qed(simp add: fixp_above_outside base)
   264 
   265 end
   266 
   267 subsection \<open>Connect with the while combinator for executability on chain-finite lattices.\<close>
   268 
   269 context bourbaki_witt_fixpoint begin
   270 
   271 lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}. }\<close>
   272   assumes "M \<in> Chains leq"
   273   and "M \<noteq> {}"
   274   and "finite M"
   275   shows "lub M \<in> M"
   276 using assms(3,1,2)
   277 proof induction
   278   case empty thus ?case by simp
   279 next
   280   case (insert x M)
   281   note chain = \<open>insert x M \<in> Chains leq\<close>
   282   show ?case
   283   proof(cases "M = {}")
   284     case True thus ?thesis
   285       using chain in_ChainsD leq_antisym lub_least lub_upper by fastforce
   286   next
   287     case False
   288     from chain have chain': "M \<in> Chains leq"
   289       using in_Chains_subset subset_insertI by blast
   290     hence "lub M \<in> M" using False by(rule insert.IH)
   291     show ?thesis
   292     proof(cases "(x, lub M) \<in> leq")
   293       case True
   294       have "(lub (insert x M), lub M) \<in> leq" using chain
   295         by (rule lub_least) (auto simp: True intro: lub_upper[OF chain'])
   296       with False have "lub (insert x M) = lub M"
   297         using lub_upper[OF chain] lub_least[OF chain'] by (blast intro: leq_antisym)
   298       with \<open>lub M \<in> M\<close> show ?thesis by simp
   299     next
   300       case False
   301       with in_ChainsD[OF chain, of x "lub M"] \<open>lub M \<in> M\<close>
   302       have "lub (insert x M) = x"
   303         by - (rule leq_antisym, (blast intro: FieldI2 chain chain' insert.prems(2) leq_refl leq_trans lub_least lub_upper)+)
   304       thus ?thesis by simp
   305     qed
   306   qed
   307 qed
   308 
   309 lemma fun_pow_iterates_above: "(f ^^ k) a \<in> iterates_above a"
   310 using iterates_above.base iterates_above.step by (induct k) simp_all
   311 
   312 lemma chfin_iterates_above_fun_pow:
   313   assumes "x \<in> iterates_above a"
   314   assumes "\<forall>M \<in> Chains leq. finite M"
   315   shows "\<exists>j. x = (f ^^ j) a"
   316 using assms(1)
   317 proof induct
   318   case base then show ?case by (simp add: exI[where x=0])
   319 next
   320   case (step x) then obtain j where "x = (f ^^ j) a" by blast
   321   with step(1) show ?case by (simp add: exI[where x="Suc j"])
   322 next
   323   case (Sup M) with in_Chains_finite assms(2) show ?case by blast
   324 qed
   325 
   326 lemma Chain_finite_iterates_above_fun_pow_iff:
   327   assumes "\<forall>M \<in> Chains leq. finite M"
   328   shows "x \<in> iterates_above a \<longleftrightarrow> (\<exists>j. x = (f ^^ j) a)"
   329 using chfin_iterates_above_fun_pow fun_pow_iterates_above assms by blast
   330 
   331 lemma fixp_above_Kleene_iter_ex:
   332   assumes "(\<forall>M \<in> Chains leq. finite M)"
   333   obtains k where "fixp_above a = (f ^^ k) a"
   334 using assms by atomize_elim (simp add: chfin_iterates_above_fun_pow fixp_iterates_above)
   335 
   336 context fixes a assumes a: "a \<in> Field leq" begin
   337 
   338 lemma funpow_Field_leq: "(f ^^ k) a \<in> Field leq"
   339 using a by (induct k) (auto intro: increasing FieldI2)
   340 
   341 lemma funpow_prefix: "j < k \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
   342 proof(induct k)
   343   case (Suc k)
   344   with leq_trans[OF _ increasing[OF funpow_Field_leq]] funpow_Field_leq increasing a
   345   show ?case by simp (metis less_antisym)
   346 qed simp
   347 
   348 lemma funpow_suffix: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ (j + k)) a, (f ^^ k) a) \<in> leq"
   349 using funpow_Field_leq
   350 by (induct j) (simp_all del: funpow.simps add: funpow_Suc_right funpow_add leq_refl)
   351 
   352 lemma funpow_stability: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
   353 using funpow_prefix funpow_suffix[where j="j - k" and k=k] by (cases "j < k") simp_all
   354 
   355 lemma funpow_in_Chains: "{(f ^^ k) a |k. True} \<in> Chains leq"
   356 using chain_iterates_above[OF a] fun_pow_iterates_above
   357 by (blast intro: ChainsI dest: in_ChainsD)
   358 
   359 lemma fixp_above_Kleene_iter:
   360   assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
   361   assumes "(f ^^ Suc k) a = (f ^^ k) a"
   362   shows "fixp_above a = (f ^^ k) a"
   363 proof(rule leq_antisym)
   364   show "(fixp_above a, (f ^^ k) a) \<in> leq" using assms a
   365     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)
   366   show "((f ^^ k) a, fixp_above a) \<in> leq" using a
   367     by(auto simp add: fixp_above_def chain_iterates_above fun_pow_iterates_above intro!: lub_upper)
   368 qed
   369 
   370 context assumes chfin: "\<forall>M \<in> Chains leq. finite M" begin
   371 
   372 lemma Chain_finite_wf: "wf {(f ((f ^^ k) a), (f ^^ k) a) |k. f ((f ^^ k) a) \<noteq> (f ^^ k) a}"
   373 apply(rule wf_measure[where f="\<lambda>b. card {(f ^^ j) a |j. (b, (f ^^ j) a) \<in> leq}", THEN wf_subset])
   374 apply(auto simp: set_eq_iff intro!: psubset_card_mono[OF finite_subset[OF _ bspec[OF chfin funpow_in_Chains]]])
   375 apply(metis funpow_Field_leq increasing leq_antisym leq_trans leq_refl)+
   376 done
   377 
   378 lemma while_option_finite_increasing: "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
   379 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"])
   380   (auto simp: a increasing chfin FieldI2 chfin_iterates_above_fun_pow fun_pow_iterates_above iterates_above.step intro: exI[where x=0])
   381 
   382 lemma fixp_above_the_while_option: "fixp_above a = the (while_option (\<lambda>A. f A \<noteq> A) f a)"
   383 proof -
   384   obtain P where "while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
   385     using while_option_finite_increasing by blast
   386   with while_option_stop2[OF this] fixp_above_Kleene_iter[OF chfin]
   387   show ?thesis by fastforce
   388 qed
   389 
   390 lemma fixp_above_conv_while: "fixp_above a = while (\<lambda>A. f A \<noteq> A) f a"
   391 unfolding while_def by (rule fixp_above_the_while_option)
   392 
   393 end
   394 
   395 end
   396 
   397 end
   398 
   399 lemma bourbaki_witt_fixpoint_complete_latticeI:
   400   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   401   assumes "\<And>x. x \<le> f x"
   402   shows "bourbaki_witt_fixpoint Sup {(x, y). x \<le> y} f"
   403 by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least)
   404 
   405 end