Theory Limit

theory Limit
  imports
    Main
begin

section ‹Slightly adjusted content from AFP/LocalLexing›

fun funpower :: "('a ⇒ 'a) ⇒ nat ⇒ ('a ⇒ 'a)" where
  "funpower f 0 x = x"
| "funpower f (Suc n) x = f (funpower f n x)"

definition natUnion :: "(nat ⇒ 'a set) ⇒ 'a set" where
  "natUnion f = ⋃ { f n | n. True }"

definition limit  :: "('a set ⇒ 'a set) ⇒ 'a set ⇒ 'a set" where
  "limit f x = natUnion (λ n. funpower f n x)"

definition setmonotone :: "('a set ⇒ 'a set) ⇒ bool" where
  "setmonotone f = (∀ X. X ⊆ f X)"

lemma subset_setmonotone: "setmonotone f ⟹ X ⊆ f X"
  by (simp add: setmonotone_def)

lemma[simp]: "funpower id n = id"
  by (rule ext, induct n, simp_all)

lemma[simp]: "limit id = id"
  by (rule ext, auto simp add: limit_def natUnion_def)

definition chain :: "(nat ⇒ 'a set) ⇒ bool"
where
  "chain C = (∀ i. C i ⊆ C (i + 1))"

definition continuous :: "('a set ⇒ 'b set) ⇒ bool"
where
  "continuous f = (∀ C. chain C ⟶ (chain (f o C) ∧ f (natUnion C) = natUnion (f o C)))"

lemma natUnion_upperbound: 
  "(⋀ n. f n ⊆ G) ⟹ (natUnion f) ⊆ G"
by (auto simp add: natUnion_def)

lemma funpower_upperbound:
  "(⋀ I. I ⊆ G ⟹ f I ⊆ G) ⟹ I ⊆ G ⟹ funpower f n I ⊆ G"
proof (induct n)
  case 0 thus ?case by simp
next
  case (Suc n) thus ?case by simp
qed

lemma limit_upperbound:
  "(⋀ I. I ⊆ G ⟹ f I ⊆ G) ⟹ I ⊆ G ⟹ limit f I ⊆ G"
by (simp add: funpower_upperbound limit_def natUnion_upperbound)

lemma elem_limit_simp: "x ∈ limit f X = (∃ n. x ∈ funpower f n X)"
by (auto simp add: limit_def natUnion_def)

definition pointwise :: "('a set ⇒ 'b set) ⇒ bool" where
  "pointwise f = (∀ X. f X = ⋃ { f {x} | x. x ∈ X})" 

lemma natUnion_elem: "x ∈ f n ⟹ x ∈ natUnion f"
using natUnion_def by fastforce
  
lemma limit_elem: "x ∈ funpower f n X ⟹ x ∈ limit f X"
by (simp add: limit_def natUnion_elem)

definition pointbase :: "('a set ⇒ 'b set) ⇒ 'a set ⇒ 'b set" where
  "pointbase F I = ⋃ { F X | X. finite X ∧ X ⊆ I }"

definition pointbased :: "('a set ⇒ 'b set) ⇒ bool" where
  "pointbased f = (∃ F. f = pointbase F)"  

lemma chain_implies_mono: "chain C ⟹ mono C"
by (simp add: chain_def mono_iff_le_Suc)

lemma setmonotone_implies_chain_funpower:
  assumes setmonotone: "setmonotone f"
  shows "chain (λ n. funpower f n I)"
by (simp add: chain_def setmonotone subset_setmonotone)  

lemma natUnion_subset: "(⋀ n. ∃ m. f n ⊆ g m) ⟹ natUnion f ⊆ natUnion g"
  by (meson natUnion_elem natUnion_upperbound subset_iff)

lemma natUnion_eq[case_names Subset Superset]: 
  "(⋀ n. ∃ m. f n ⊆ g m) ⟹ (⋀ n. ∃ m. g n ⊆ f m) ⟹ natUnion f = natUnion g"
by (simp add: natUnion_subset subset_antisym)
  
lemma natUnion_shift[symmetric]: 
  assumes chain: "chain C"
  shows "natUnion C = natUnion (λ n. C (n + m))"
proof (induct rule: natUnion_eq)
  case (Subset n)
    show ?case using chain chain_implies_mono le_add1 mono_def by blast 
next
  case (Superset n)
    show ?case by blast 
qed

definition regular :: "('a set ⇒ 'a set) ⇒ bool"
where
  "regular f = (setmonotone f ∧ continuous f)"

lemma regular_fixpoint:
  assumes regular: "regular f"
  shows "f (limit f I) = limit f I"
proof -
  have setmonotone: "setmonotone f" using regular regular_def by blast
  have continuous: "continuous f" using regular regular_def by blast

  let ?C = "λ n. funpower f n I"
  have chain: "chain ?C"
    by (simp add: setmonotone setmonotone_implies_chain_funpower)
  have "f (limit f I) = f (natUnion ?C)"
    using limit_def by metis
  also have "f (natUnion ?C) = natUnion (f o ?C)"
    by (metis continuous continuous_def chain)
  also have "natUnion (f o ?C) = natUnion (λ n. f(funpower f n I))"
    by (meson comp_apply)
  also have "natUnion (λ n. f(funpower f n I)) = natUnion (λ n. ?C (n + 1))"
    by simp
  also have "natUnion (λ n. ?C(n + 1)) = natUnion ?C"
    apply (subst natUnion_shift)
    using chain by (blast+)
  finally show ?thesis by (simp add: limit_def)
qed  
    
lemma fix_is_fix_of_limit:
  assumes fixpoint: "f I = I"   
  shows "limit f I = I"
proof -
  have funpower: "⋀ n. funpower f n I = I" 
  proof -  
    fix n :: nat
    from fixpoint show "funpower f n I = I"
      by (induct n, auto)
  qed
  show ?thesis by (simp add: limit_def funpower natUnion_def)
qed     

lemma limit_is_idempotent: "regular f ⟹ limit f (limit f I) = limit f I"
by (simp add: fix_is_fix_of_limit regular_fixpoint)

definition mk_regular1 :: "('b ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'a ⇒ 'a) ⇒ 'a set ⇒ 'a set" where
  "mk_regular1 P F I = I ∪ { F q x | q x. x ∈ I ∧ P q x }"

definition mk_regular2 :: "('b ⇒ 'a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'a ⇒ 'a ⇒ 'a) ⇒ 'a set ⇒ 'a set" where
  "mk_regular2 P F I = I ∪ { F q x y | q x y. x ∈ I ∧ y ∈ I ∧ P q x y }"

end