Theory HOL-Library.Bourbaki_Witt_Fixpoint

(*  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 ‹The Bourbaki-Witt tower construction for transfinite iteration›

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 ‹M ≠ {}› 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] ‹y = a› 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' ∈ Chains leq" "M' ≠ {}"
  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' ∈ 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 ‹y ∈ iterates_above a› 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' ∈ 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 ‹x ∈ ?C› a have "x ∈ Field leq" by(rule iterates_above_Field)
  moreover from ‹y ∈ ?C› a have "y ∈ 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 ‹Connect with the while combinator for executability on chain-finite lattices.›

context bourbaki_witt_fixpoint begin

lemma in_Chains_finite: ― ‹Translation from @{thm in_chain_finite}.›
  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 = ‹insert x M ∈ Chains leq›
  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 ‹lub M ∈ M› show ?thesis by simp
    next
      case False
      with in_ChainsD[OF chain, of x "lub M"] ‹lub M ∈ M›
      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