Quelle Bourbaki_Witt_Fixpoint.thy Sprache: Isabelle

(*  Title:      HOL/Library/Bourbaki_Witt_Fixpoint.thy
    Author:     Andreas Lochbihler, ETH Zurich

  Follows G. Smolka, S. Schäfer and C. Doczkal: Transfinite Constructions in
  Classical Type Theory. ITP 2015
*)

section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>

theory Bourbaki_Witt_Fixpoint
  imports While_Combinator
begin

lemma ChainsI [intro?]:
  "(\a b. \ a \ Y; b \ Y \ \ (a, b) \ r \ (b, a) \ r) \ Y \ Chains r"
unfolding Chains_def by blast

lemma in_Chains_subset: "\ M \ Chains r; M' \ M \ \ M' \ Chains r"
by(auto simp add: Chains_def)

lemma in_ChainsD: "\ M \ Chains r; x \ M; y \ M \ \ (x, y) \ r \ (y, x) \ r"
unfolding Chains_def by fast

lemma Chains_FieldD: "\ M \ Chains r; x \ M \ \ x \ Field r"
by(auto simp add: Chains_def intro: FieldI1 FieldI2)

lemma in_Chains_conv_chain: "M \ Chains r \ Complete_Partial_Order.chain (\x y. (x, y) \ r) M"
by(simp add: Chains_def chain_def)

lemma partial_order_on_trans:
  "\ partial_order_on A r; (x, y) \ r; (y, z) \ r \ \ (x, z) \ r"
by(auto simp add: order_on_defs dest: transD)

locale bourbaki_witt_fixpoint =
  fixes lub :: "'a set \ 'a"
  and leq :: "('a \ 'a) set"
  and f :: "'a \ 'a"
  assumes po: "Partial_order leq"
  and lub_least: "\ M \ Chains leq; M \ {}; \x. x \ M \ (x, z) \ leq \ \ (lub M, z) \ leq"
  and lub_upper: "\ M \ Chains leq; x \ M \ \ (x, lub M) \ leq"
  and lub_in_Field: "\ M \ Chains leq; M \ {} \ \ lub M \ Field leq"
  and increasing: "\x. x \ Field leq \ (x, f x) \ leq"
begin

lemma leq_trans: "\ (x, y) \ leq; (y, z) \ leq \ \ (x, z) \ leq"
by(rule partial_order_on_trans[OF po])

lemma leq_refl: "x \ Field leq \ (x, x) \ leq"
using po by(simp add: order_on_defs refl_on_def)

lemma leq_antisym: "\ (x, y) \ leq; (y, x) \ leq \ \ x = y"
using po by(simp add: order_on_defs antisym_def)

inductive_set iterates_above :: "'a \ 'a set"
  for a
where
  base: "a \ iterates_above a"
| step: "x \ iterates_above a \ f x \ iterates_above a"
| Sup: "\ M \ Chains leq; M \ {}; \x. x \ M \ x \ iterates_above a \ \ lub M \ iterates_above a"

definition fixp_above :: "'a \ 'a"
where "fixp_above a = (if a \ Field leq then lub (iterates_above a) else a)"

lemma fixp_above_outside: "a \ Field leq \ fixp_above a = a"
by(simp add: fixp_above_def)

lemma fixp_above_inside: "a \ Field leq \ fixp_above a = lub (iterates_above a)"
by(simp add: fixp_above_def)

context
  notes leq_refl [intro!, simp]
  and base [intro]
  and step [intro]
  and Sup [intro]
  and leq_trans [trans]
begin

lemma iterates_above_le_f: "\ x \ iterates_above a; a \ Field leq \ \ (x, f x) \ leq"
by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+

lemma iterates_above_Field: "\ x \ iterates_above a; a \ Field leq \ \ x \ Field leq"
by(drule (1) iterates_above_le_f)(rule FieldI1)

lemma iterates_above_ge:
  assumes y: "y \ iterates_above a"
  and a: "a \ Field leq"
  shows "(a, y) \ leq"
using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper])

lemma iterates_above_lub:
  assumes M: "M \ Chains leq"
  and nempty: "M \ {}"
  and upper: "\y. y \ M \ \z \ M. (y, z) \ leq \ z \ iterates_above a"
  shows "lub M \ iterates_above a"
proof -
  let ?M = "M \ iterates_above a"
  from M have M': "?M \ Chains leq" by(rule in_Chains_subset)simp
  have "?M \ {}" using nempty by(auto dest: upper)
  with M' have "lub ?M \ iterates_above a" by(rule Sup) blast
  also have "lub ?M = lub M" using nempty
    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)+
  finally show ?thesis .
qed

lemma iterates_above_successor:
  assumes y: "y \ iterates_above a"
  and a: "a \ Field leq"
  shows "y = a \ y \ iterates_above (f a)"
using y
proof induction
  case base thus ?case by simp
next
  case (step x) thus ?case by auto
next
  case (Sup M)
  show ?case
  proof(cases "\x. M \ {x}")
    case True
    with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto
    have "lub M = y"
      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)
    with Sup.IH[of y] M show ?thesis by simp
  next
    case False
    from Sup(1-2) have "lub M \ iterates_above (f a)"
    proof(rule iterates_above_lub)
      fix y
      assume y: "y \ M"
      from Sup.IH[OF this] show "\z\M. (y, z) \ leq \ z \ iterates_above (f a)"
      proof
        assume "y = a"
        from y False obtain z where z: "z \ M" and neq: "y \ z" by (metis insertI1 subsetI)
        with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
        show ?thesis by(auto dest: iterates_above_ge intro: a)
      next
        assume *: "y \ iterates_above (f a)"
        with increasing[OF a] have "y \ Field leq"
          by(auto dest!: iterates_above_Field intro: FieldI2)
        with * show ?thesis using y by auto
      qed
    qed
    thus ?thesis by simp
  qed
qed

lemma iterates_above_Sup_aux:
  assumes M: "M \ Chains leq" "M \ {}"
  and M': "M' \<in> Chains leq" "M' \<noteq> {}"
  and comp: "\x. x \ M \ x \ iterates_above (lub M') \ lub M' \ iterates_above x"
  shows "(lub M, lub M') \ leq \ lub M \ iterates_above (lub M')"
proof(cases "\x \ M. x \ iterates_above (lub M')")
  case True
  then obtain x where x: "x \ M" "x \ iterates_above (lub M')" by blast
  have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field)
  have "lub M \ iterates_above (lub M')" using M
  proof(rule iterates_above_lub)
    fix y
    assume y: "y \ M"
    from comp[OF y] show "\z\M. (y, z) \ leq \ z \ iterates_above (lub M')"
    proof
      assume "y \ iterates_above (lub M')"
      from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast
    next
      assume "lub M' \ iterates_above y"
      hence "(y, lub M') \ leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge)
      also have "(lub M', x) \ leq" using x(2) lub_M' by(rule iterates_above_ge)
      finally show ?thesis using x by blast
    qed
  qed
  thus ?thesis ..
next
  case False
  have "(lub M, lub M') \ leq" using M
  proof(rule lub_least)
    fix x
    assume x: "x \ M"
    from comp[OF x] x False have "lub M' \ iterates_above x" by auto
    moreover from M(1) x have "x \ Field leq" by(rule Chains_FieldD)
    ultimately show "(x, lub M') \ leq" by(rule iterates_above_ge)
  qed
  thus ?thesis ..
qed

lemma iterates_above_triangle:
  assumes x: "x \ iterates_above a"
  and y: "y \ iterates_above a"
  and a: "a \ Field leq"
  shows "x \ iterates_above y \ y \ iterates_above x"
using x y
proof(induction arbitrary: y)
  case base then show ?case by simp
next
  case (step x) thus ?case using a
    by(auto dest: iterates_above_successor intro: iterates_above_Field)
next
  case x: (Sup M)
  hence lub: "lub M \ iterates_above a" by blast
  from \<open>y \<in> iterates_above a\<close> show ?case
  proof(induction)
    case base show ?case using lub by simp
  next
    case (step y) thus ?case using a
      by(auto dest: iterates_above_successor intro: iterates_above_Field)
  next
    case y: (Sup M')
    hence lub': "lub M' \<in> iterates_above a" by blast
    have *: "x \ iterates_above (lub M') \ lub M' \ iterates_above x" if "x \ M" for x
      using that lub' by(rule x.IH)
    with x(1-2) y(1-2) have "(lub M, lub M') \ leq \ lub M \ iterates_above (lub M')"
      by(rule iterates_above_Sup_aux)
    moreover from y(1-2) x(1-2) have "(lub M', lub M) \ leq \ lub M' \ iterates_above (lub M)"
      by(rule iterates_above_Sup_aux)(blast dest: y.IH)
    ultimately show ?case by(auto 4 3 dest: leq_antisym)
  qed
qed

lemma chain_iterates_above:
  assumes a: "a \ Field leq"
  shows "iterates_above a \ Chains leq" (is "?C \ _")
proof (rule ChainsI)
  fix x y
  assume "x \ ?C" "y \ ?C"
  hence "x \ iterates_above y \ y \ iterates_above x" using a by(rule iterates_above_triangle)
  moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field)
  moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field)
  ultimately show "(x, y) \ leq \ (y, x) \ leq" by(auto dest: iterates_above_ge)
qed

lemma fixp_iterates_above: "fixp_above a \ iterates_above a"
by(auto intro: chain_iterates_above simp add: fixp_above_def)

lemma fixp_above_Field: "a \ Field leq \ fixp_above a \ Field leq"
using fixp_iterates_above by(rule iterates_above_Field)

lemma fixp_above_unfold:
  assumes a: "a \ Field leq"
  shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a")
proof(rule leq_antisym)
  show "(?a, f ?a) \ leq" using fixp_above_Field[OF a] by(rule increasing)

  have "f ?a \ iterates_above a" using fixp_iterates_above by(rule iterates_above.step)
  with chain_iterates_above[OF a] show "(f ?a, ?a) \ leq"
    by(simp add: fixp_above_inside assms lub_upper)
qed

end

lemma fixp_above_induct [case_names adm base step]:
  assumes adm: "ccpo.admissible lub (\x y. (x, y) \ leq) P"
  and base: "P a"
  and step: "\x. P x \ P (f x)"
  shows "P (fixp_above a)"
proof(cases "a \ Field leq")
  case True
  from adm chain_iterates_above[OF True]
  show ?thesis unfolding fixp_above_inside[OF True] in_Chains_conv_chain
  proof(rule ccpo.admissibleD)
    have "a \ iterates_above a" ..
    then show "iterates_above a \ {}" by(auto)
    show "P x" if "x \ iterates_above a" for x using that
      by induction(auto intro: base step simp add: in_Chains_conv_chain dest: ccpo.admissibleD[OF adm])
  qed
qed(simp add: fixp_above_outside base)

end

subsection \<open>Connect with the while combinator for executability on chain-finite lattices.\<close>

context bourbaki_witt_fixpoint begin

lemma in_Chains_finite: \<comment> \<open>Translation from @{thm in_chain_finite}.\<close>
  assumes "M \ Chains leq"
  and "M \ {}"
  and "finite M"
  shows "lub M \ M"
using assms(3,1,2)
proof induction
  case empty thus ?case by simp
next
  case (insert x M)
  note chain = \<open>insert x M \<in> Chains leq\<close>
  show ?case
  proof(cases "M = {}")
    case True thus ?thesis
      using chain in_ChainsD leq_antisym lub_least lub_upper by fastforce
  next
    case False
    from chain have chain': "M \ Chains leq"
      using in_Chains_subset subset_insertI by blast
    hence "lub M \ M" using False by(rule insert.IH)
    show ?thesis
    proof(cases "(x, lub M) \ leq")
      case True
      have "(lub (insert x M), lub M) \ leq" using chain
        by (rule lub_least) (auto simp: True intro: lub_upper[OF chain'])
      with False have "lub (insert x M) = lub M"
        using lub_upper[OF chain] lub_least[OF chain'] by (blast intro: leq_antisym)
      with \<open>lub M \<in> M\<close> show ?thesis by simp
    next
      case False
      with in_ChainsD[OF chain, of x "lub M"] \<open>lub M \<in> M\<close>
      have "lub (insert x M) = x"
        by - (rule leq_antisym, (blast intro: FieldI2 chain chain' insert.prems(2) leq_refl leq_trans lub_least lub_upper)+)
      thus ?thesis by simp
    qed
  qed
qed

lemma fun_pow_iterates_above: "(f ^^ k) a \ iterates_above a"
using iterates_above.base iterates_above.step by (induct k) simp_all

lemma chfin_iterates_above_fun_pow:
  assumes "x \ iterates_above a"
  assumes "\M \ Chains leq. finite M"
  shows "\j. x = (f ^^ j) a"
using assms(1)
proof induct
  case base then show ?case by (simp add: exI[where x=0])
next
  case (step x) then obtain j where "x = (f ^^ j) a" by blast
  with step(1) show ?case by (simp add: exI[where x="Suc j"])
next
  case (Sup M) with in_Chains_finite assms(2) show ?case by blast
qed

lemma Chain_finite_iterates_above_fun_pow_iff:
  assumes "\M \ Chains leq. finite M"
  shows "x \ iterates_above a \ (\j. x = (f ^^ j) a)"
using chfin_iterates_above_fun_pow fun_pow_iterates_above assms by blast

lemma fixp_above_Kleene_iter_ex:
  assumes "(\M \ Chains leq. finite M)"
  obtains k where "fixp_above a = (f ^^ k) a"
using assms by atomize_elim (simp add: chfin_iterates_above_fun_pow fixp_iterates_above)

context fixes a assumes a: "a \ Field leq" begin

lemma funpow_Field_leq: "(f ^^ k) a \ Field leq"
using a by (induct k) (auto intro: increasing FieldI2)

lemma funpow_prefix: "j < k \ ((f ^^ j) a, (f ^^ k) a) \ leq"
proof(induct k)
  case (Suc k)
  with leq_trans[OF _ increasing[OF funpow_Field_leq]] funpow_Field_leq increasing a
  show ?case by simp (metis less_antisym)
qed simp

lemma funpow_suffix: "(f ^^ Suc k) a = (f ^^ k) a \ ((f ^^ (j + k)) a, (f ^^ k) a) \ leq"
using funpow_Field_leq
by (induct j) (simp_all del: funpow.simps add: funpow_Suc_right funpow_add leq_refl)

lemma funpow_stability: "(f ^^ Suc k) a = (f ^^ k) a \ ((f ^^ j) a, (f ^^ k) a) \ leq"
using funpow_prefix funpow_suffix[where j="j - k" and k=k] by (cases "j < k") simp_all

lemma funpow_in_Chains: "{(f ^^ k) a |k. True} \ Chains leq"
using chain_iterates_above[OF a] fun_pow_iterates_above
by (blast intro: ChainsI dest: in_ChainsD)

lemma fixp_above_Kleene_iter:
  assumes "\M \ Chains leq. finite M" \ \convenient but surely not necessary\
  assumes "(f ^^ Suc k) a = (f ^^ k) a"
  shows "fixp_above a = (f ^^ k) a"
proof(rule leq_antisym)
  show "(fixp_above a, (f ^^ k) a) \ leq" using assms a
    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)
  show "((f ^^ k) a, fixp_above a) \ leq" using a
    by(auto simp add: fixp_above_def chain_iterates_above fun_pow_iterates_above intro!: lub_upper)
qed

context assumes chfin: "\M \ Chains leq. finite M" begin

lemma Chain_finite_wf: "wf {(f ((f ^^ k) a), (f ^^ k) a) |k. f ((f ^^ k) a) \ (f ^^ k) a}"
apply(rule wf_measure[where f="\b. card {(f ^^ j) a |j. (b, (f ^^ j) a) \ leq}", THEN wf_subset])
apply(auto simp: set_eq_iff intro!: psubset_card_mono[OF finite_subset[OF _ bspec[OF chfin funpow_in_Chains]]])
apply(metis funpow_Field_leq increasing leq_antisym leq_trans leq_refl)+
done

lemma while_option_finite_increasing: "\P. while_option (\A. f A \ A) f a = Some P"
by(rule wf_rel_while_option_Some[OF Chain_finite_wf, where P="\A. (\k. A = (f ^^ k) a) \ (A, f A) \ leq" and s="a"])
  (auto simp: a increasing chfin FieldI2 chfin_iterates_above_fun_pow fun_pow_iterates_above iterates_above.step intro: exI[where x=0])

lemma fixp_above_the_while_option: "fixp_above a = the (while_option (\A. f A \ A) f a)"
proof -
  obtain P where "while_option (\A. f A \ A) f a = Some P"
    using while_option_finite_increasing by blast
  with while_option_stop2[OF this] fixp_above_Kleene_iter[OF chfin]
  show ?thesis by fastforce
qed

lemma fixp_above_conv_while: "fixp_above a = while (\A. f A \ A) f a"
unfolding while_def by (rule fixp_above_the_while_option)

end

end

end

lemma bourbaki_witt_fixpoint_complete_latticeI:
  fixes f :: "'a::complete_lattice \ 'a"
  assumes "\x. x \ f x"
  shows "bourbaki_witt_fixpoint Sup {(x, y). x \ y} f"
by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least)

end

quality99%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.