Quelle  Limit.thy

theory Limit
imports LocalLexing
begin

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

lemma setmonotone_funpower: "setmonotone f ==> setmonotone (funpower f n)"
  by (induct n, auto simp add: setmonotone_def)

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

lemma elem_setmonotone: "setmonotone f ==> x ∈ X ==> x ∈ f X"
  by (auto simp add: setmonotone_def)

lemma elem_natUnion: "(∀ n. x ∈ f n) ==> x ∈ natUnion f"
  by (auto simp add: natUnion_def)

lemma subset_natUnion: "(∀ n. X ⊆ f n) ==> X ⊆ natUnion f"
  by (auto simp add: natUnion_def)
  
lemma setmonotone_limit:
  assumes fmono: "setmonotone f"
  shows "setmonotone (limit f)"
proof -
  show "setmonotone (limit f)" 
    apply (auto simp add: setmonotone_def limit_def)
    apply (rule elem_natUnion, auto)
    apply (rule elem_setmonotone[OF setmonotone_funpower])
    by (auto simp add: fmono)
qed

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)

lemma natUnion_decompose[consumes 1, case_names Decompose]:
  assumes p: "p ∈ natUnion S"
  assumes decompose: "∧ n p. p ∈ S n ==> P p" 
  shows "P p" 
proof -
  from p have "∃ n. p ∈ S n" 
    by (auto simp add: natUnion_def)
  then obtain n where "p ∈ S n" by blast
  from decompose[OF this] show ?thesis .
qed

lemma limit_induct[consumes 1, case_names Init Iterate]:
  assumes p: "(p :: 'a) ∈ limit f X"
  assumes init: "∧ p. p ∈ X ==> P p"
  assumes iterate: "∧ p Y. (∧ q . q ∈ Y ==> P q) ==> p ∈ f Y ==> P p"
  shows "P p"
proof -
  from p have p_in_natUnion: "p ∈ natUnion (λ n. funpower f n X)"    
    by (simp add: limit_def)
  {
    fix p :: 'a
    fix n :: nat
    have "p ∈ funpower f n X ==> P p"
    proof (induct n arbitrary: p) 
      case 0 thus ?case using init[OF 0[simplified]] by simp
    next
      case (Suc n) show ?case 
        using iterate[OF Suc(1) Suc(2)[simplified], simplified] by simp
    qed
  }
  with p_in_natUnion show ?thesis
    by (induct rule: natUnion_decompose)
qed

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 continuous_apply:
  "continuous f ==> chain C ==> f (natUnion C) = natUnion (f o C)"
by (simp add: continuous_def)

lemma continuous_imp_mono:
  assumes continuous: "continuous f"
  shows "mono f"
proof -
  { 
    fix A :: "'a set"
    fix B :: "'a set"
    assume sub: "A ⊆ B"
    let ?C = "λ (i::nat). if (i = 0) then A else B"
    have "chain ?C" by (simp add: chain_def sub) 
    then have fC: "chain (f o ?C)" using continuous continuous_def by blast
    then have "f (?C 0) ⊆ f (?C (0 + 1))"
    proof -
      have "∧f n. ¬ chain f ∨ (f n::'b set) ⊆ f (Suc n)"
        by (metis Suc_eq_plus1 chain_def)
      then show ?thesis using fC by fastforce
    qed
    then have "f A ⊆ f B" by auto
  }
  then show "mono f" by (simp add: monoI)
qed 
      
lemma mono_maps_chain_to_chain: 
  assumes f: "mono f"
  assumes C: "chain C"
  shows "chain (f o C)"
by (metis C comp_def f chain_def mono_def)

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 pointwise_simp: 
  assumes f: "pointwise f"
  shows "f X = ∪ { f {x} | x. x ∈ X}"
proof -
  from f have "∀ X. f X = ∪ { f {x} | x. x ∈ X}"
    by (rule iffD1[OF pointwise_def[where f=f]])
  then show ?thesis by blast
qed

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)

lemma limit_step_pointwise:
  assumes x: "x ∈ limit f X"
  assumes f: "pointwise f"
  assumes y: "y ∈ f {x}"
  shows "y ∈ limit f X"
proof - 
  from x have "∃ n. x ∈ funpower f n X" 
    by (simp add: elem_limit_simp)
  then obtain n where n: "x ∈ funpower f n X" by blast
  have "y ∈ funpower f (Suc n) X"
    apply simp 
    apply (subst pointwise_simp[OF f])
    using y n by auto
  then show "y ∈ limit f X" by (meson limit_elem)
qed

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 pointwise_implies_pointbased:
  assumes pointwise: "pointwise f"
  shows "pointbased f"
proof -
  let ?F = "λ X. f X"
  {
    fix I :: "'a set"
    fix x :: "'b"
    have lr: "x ∈ pointbase ?F I ==> x ∈ f I"
    proof -
      assume x: "x ∈ pointbase ?F I"
      have "∃ X. x ∈ f X ∧ X ⊆ I"
        proof -
          have "x ∈ ∪{f A |A. finite A ∧ A ⊆ I}"
            by (metis pointbase_def x)
          then show ?thesis
            by blast
        qed
      then obtain X where X:"x ∈ f X ∧ X ⊆ I" by blast
      have "∃ y. y ∈ I ∧ x ∈ f {y}"
        using X apply (simp add: pointwise_simp[OF pointwise, where X=X])
        by blast
      then show "x ∈ f I"
        apply (simp add: pointwise_simp[OF pointwise, where X=I])
        by blast
    qed
    have rl: "x ∈ f I ==> x ∈ pointbase ?F I"
    proof -
      assume x: "x ∈ f I"
      have "∃ y. y ∈ I ∧ x ∈ f {y}"
        using x apply (simp add: pointwise_simp[OF pointwise, where X=I])
        by blast
      then obtain y where "y ∈ I ∧ x ∈ f {y}" by blast
      then have "∃ X. x ∈ f X ∧ finite X ∧ X ⊆ I" by blast
      then show "x ∈ pointbase f I"
        apply (simp add: pointbase_def)
        by blast
    qed
    note lr rl
  }
  then have "∧ I. pointbase f I = f I" by blast
  then have "pointbase f = f" by blast
  then show ?thesis by (metis pointbased_def) 
qed  
   
lemma pointbase_is_mono:
  "mono (pointbase f)"
proof -
  {
    fix A :: "'a set"
    fix B :: "'a set"
    assume subset: "A ⊆ B"
    have "(pointbase f) A ⊆ (pointbase f) B" 
      apply (simp add: pointbase_def)
      using subset by fastforce
  }
  then show ?thesis by (simp add: mono_def)
qed

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

lemma chain_cover_witness: "finite X ==> chain C ==> X ⊆ natUnion C ==> ∃ n. X ⊆ C n"
proof (induct rule: finite.induct)
  case emptyI thus ?case by blast
next
  case (insertI X x) 
  then have "X ⊆ natUnion C" by simp
  with insertI have "∃ n. X ⊆ C n" by blast
  then obtain n where n: "X ⊆ C n" by blast
  have x: "x ∈ natUnion C" using insertI.prems(2) by blast
  then have "∃ m. x ∈ C m"
  proof -
    have "x ∈ ∪{A. ∃n. A = C n}" by (metis x natUnion_def)
    then show ?thesis by blast
  qed
  then obtain m where m: "x ∈ C m" by blast
  have mono_C: "∧ i j. i ≤ j ==> C i ⊆ C j"
    using chain_implies_mono insertI(3) mono_def by blast 
  show ?case
    apply (rule_tac x="max n m" in exI)
    apply auto
    apply (meson contra_subsetD m max.cobounded2 mono_C)
    by (metis max_def mono_C n subsetCE)
qed
    
lemma pointbase_is_continuous:
  "continuous (pointbase f)"
proof -
  {
    fix C :: "nat ==> 'a set"
    assume C: "chain C"
    have mono: "chain ((pointbase f) o C)"
      by (simp add: C mono_maps_chain_to_chain pointbase_is_mono)
    have subset1: "natUnion ((pointbase f) o C) ⊆ (pointbase f) (natUnion C)"
    proof (auto)
      fix y :: "'b"
      assume "y ∈ natUnion ((pointbase f) o C)"
      then show "y ∈ (pointbase f) (natUnion C)"
      proof (induct rule: natUnion_decompose)
        case (Decompose n p)
          thus ?case by (metis comp_apply contra_subsetD mono_def natUnion_elem 
            pointbase_is_mono subsetI) 
      qed
    qed
    have subset2: "(pointbase f) (natUnion C) ⊆ natUnion ((pointbase f) o C)"
    proof (auto)
      fix y :: "'b"
      assume y: "y ∈ (pointbase f) (natUnion C)"
      have "∃ X. finite X ∧ X ⊆ natUnion C ∧ y ∈ f X"
      proof -
        have "y ∈ ∪{f A |A. finite A ∧ A ⊆ natUnion C}"
          by (metis y pointbase_def)
        then show ?thesis by blast
      qed
      then obtain X where X: "finite X ∧ X ⊆ natUnion C ∧ y ∈ f X" by blast
      then have "∃ n. X ⊆ C n" using chain_cover_witness C by blast
      then obtain n where X_sub_C: "X ⊆ C n" by blast
      show "y ∈ natUnion ((pointbase f) o C)" 
        apply (rule_tac natUnion_elem[where n=n])
        proof -
          have "y ∈ ∪{f A |A. finite A ∧ A ⊆ C n}"
          using X X_sub_C by blast
          then show "y ∈ (pointbase f ∘ C) n" by (simp add: pointbase_def)
      qed
    qed
    note mono subset1 subset2
  }  
  then show ?thesis by (simp add: continuous_def subset_antisym)   
qed
 
lemma pointbased_implies_continuous:
  "pointbased f ==> continuous f"
  using pointbase_is_continuous pointbased_def by force

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 }"

lemma setmonotone_mk_regular1: "setmonotone (mk_regular1 P F)"
by (simp add: mk_regular1_def setmonotone_def)

lemma setmonotone_mk_regular2: "setmonotone (mk_regular2 P F)"
by (simp add: mk_regular2_def setmonotone_def)

lemma pointbased_mk_regular1: "pointbased (mk_regular1 P F)"
proof -
  let ?f = "λ X. X ∪ { F q x | q x. x ∈ X ∧ P q x }"
  {
    fix I :: "'a set"
    have 1: "pointbase ?f I ⊆ mk_regular1 P F I"
      by (auto simp add: pointbase_def mk_regular1_def)
    have 2: "mk_regular1 P F I ⊆ pointbase ?f I"
      apply (simp add: pointbase_def mk_regular1_def)
      apply blast
      done
    from 1 2 have "pointbase ?f I = mk_regular1 P F I" by blast
  }
  then show ?thesis
    apply (subst pointbased_def)
    apply (rule_tac x="?f" in exI)
    by blast
qed

lemma pointbased_mk_regular2: "pointbased (mk_regular2 P F)"
proof -
  let ?f = "λ X. X ∪ { F q x y | q x y. x ∈ X ∧ y ∈ X ∧ P q x y }"
  {
    fix I :: "'a set"
    have 1: "pointbase ?f I ⊆ mk_regular2 P F I"
      by (auto simp add: pointbase_def mk_regular2_def)
    have 2: "mk_regular2 P F I ⊆ pointbase ?f I"
      apply (auto simp add: pointbase_def mk_regular2_def)
      apply blast
      proof -
        fix q x y
        assume x: "x ∈ I"
        assume y: "y ∈ I"
        assume P: "P q x y"
        let ?X = "{x, y}"
        let ?A = "?X ∪ {F q x y |q x y. x ∈ ?X ∧ y ∈ ?X ∧ P q x y}"
        show "∃A. (∃X. A = X ∪ {F q x y |q x y. x ∈ X ∧ y ∈ X ∧ P q x y} ∧
          finite X ∧ X ⊆ I) ∧ F q x y ∈ A"
          apply (rule_tac x="?A" in exI)
          apply (rule conjI)
          apply (rule_tac x="?X" in exI)
          apply (auto simp add: x y)[1]
          using x y P by blast
      qed  
    from 1 2 have "pointbase ?f I = mk_regular2 P F I" by blast
  }
  then show ?thesis
    apply (subst pointbased_def)
    apply (rule_tac x="?f" in exI)
    by blast
qed

lemma regular1:"regular (mk_regular1 P F)"
by (simp add: pointbased_implies_continuous pointbased_mk_regular1 regular_def 
  setmonotone_mk_regular1)
  
lemma regular2: "regular (mk_regular2 P F)"
by (simp add: pointbased_implies_continuous pointbased_mk_regular2 regular_def 
  setmonotone_mk_regular2)

lemma continuous_comp: 
  assumes f: "continuous f"
  assumes g: "continuous g"
  shows "continuous (g o f)"
by (metis (no_types, lifting) comp_assoc comp_def continuous_def f g)

lemma setmonotone_comp:
  assumes f: "setmonotone f"
  assumes g: "setmonotone g"
  shows "setmonotone (g o f)"
by (metis (mono_tags, lifting) comp_def f g rev_subsetD setmonotone_def subsetI)

lemma regular_comp:
  assumes f: "regular f"
  assumes g: "regular g"
  shows "regular (g o f)"
using continuous_comp f g regular_def setmonotone_comp by blast

lemma setmonotone_id[simp]: "setmonotone id"
  by (simp add: id_def setmonotone_def)

lemma continuous_id[simp]: "continuous id"
  by (simp add: continuous_def)

lemma regular_id[simp]: "regular id"
  by (simp add: regular_def)

lemma regular_funpower: "regular f ==> regular (funpower f n)"
proof (induct n)
  case 0 thus ?case by (simp add: id_def[symmetric])
next
  case (Suc n) 
  have funpower: "funpower f (Suc n) = f o (funpower f n)"
    apply (rule ext)
    by simp
  with Suc show ?case
    by (auto simp only: funpower regular_comp)
qed

lemma mono_id[simp]: "mono id"
  by (simp add: mono_def id_def)

lemma mono_funpower:
  assumes mono: "mono f"
  shows "mono (funpower f n)"
proof (induct n)
  case 0 thus ?case by (simp add: id_def[symmetric])
next
  case (Suc n) 
  show ?case by (simp add: Suc.hyps mono monoD monoI)
qed    

lemma mono_limit:
  assumes mono: "mono f"
  shows "mono (limit f)"
proof(auto simp add: mono_def limit_def)
  fix A :: "'a set" 
  fix B :: "'a set"
  fix x
  assume subset: "A ⊆ B"
  assume "x ∈ natUnion (λn. funpower f n A)"
  then have "∃ n. x ∈ funpower f n A" using elem_limit_simp limit_def by fastforce 
  then obtain n where n: "x ∈ funpower f n A" by blast
  then have mono: "mono (funpower f n)" by (simp add: mono mono_funpower)
  then have "x ∈ funpower f n B" by (meson contra_subsetD monoD n subset)  
  then show "x ∈ natUnion (λn. funpower f n B)" by (simp add: natUnion_elem) 
qed

lemma continuous_funpower:
  assumes continuous: "continuous f"
  shows "continuous (funpower f n)"
proof (induct n)
  case 0 thus ?case by (simp add: id_def[symmetric])
next
  case (Suc n)
  have mono: "mono (funpower f (Suc n))" 
    by (simp add: continuous continuous_imp_mono mono_funpower) 
  have chain: "∀ C. chain C ⟶ chain ((funpower f (Suc n)) o C)"
    by (simp del: funpower.simps add: mono mono_maps_chain_to_chain) 
  have limit: "∧ C. chain C ==> (funpower f (Suc n)) (natUnion C) =
      natUnion ((funpower f (Suc n)) o C)"
      apply simp
      apply (subst continuous_apply[OF Suc])
      apply simp
      apply (subst continuous_apply[OF continuous])
      apply (simp add: Suc.hyps continuous_imp_mono mono_maps_chain_to_chain)
      apply (rule arg_cong[where f="natUnion"])
      apply (rule ext)
      by simp
  from chain limit show ?case using continuous_def by blast
qed      

lemma natUnion_swap:
  "natUnion (λ i. natUnion (λ j. f i j)) = natUnion (λ j. natUnion (λ i. f i j))"
by (metis (no_types, lifting) natUnion_elem natUnion_upperbound subsetI subset_antisym)
      
lemma continuous_limit:
  assumes continuous: "continuous f"
  shows "continuous (limit f)"
proof -
  have mono: "mono (limit f)"
    by (simp add: continuous continuous_imp_mono mono_limit) 
  have chain: "∧ C. chain C ==> chain ((limit f) o C)"
    by (simp add: mono mono_maps_chain_to_chain)
  have "∧ C. chain C ==> (limit f) (natUnion C) = natUnion ((limit f) o C)"
  proof -
    fix C :: "nat ==> 'a set"
    assume chain_C: "chain C"
    have contpower: "∧ n. continuous (funpower f n)"
      by (simp add: continuous continuous_funpower) 
    have comp: "∧ n F. F o C = (λ i. F (C i))"
      by auto    
    have "(limit f) (natUnion C) = natUnion (λ n. funpower f n (natUnion C))"
      by (simp add: limit_def)
    also have "natUnion (λ n. funpower f n (natUnion C)) =
          natUnion (λ n. natUnion ((funpower f n) o C))"
      apply (subst continuous_apply[OF contpower])
      apply (simp add: chain_C)+
      done
    also have "natUnion (λ n. natUnion ((funpower f n) o C)) =
      natUnion (λ n. natUnion (λ i. funpower f n (C i)))" 
      apply (subst comp)
      apply blast
      done
    also have "natUnion (λ n. natUnion (λ i. funpower f n (C i))) =
      natUnion (λ i. natUnion (λ n. funpower f n (C i)))"
      apply (subst natUnion_swap)
      apply blast
      done
    also have "natUnion (λ i. natUnion (λ n. funpower f n (C i))) =
      (natUnion (λ i. limit f (C i)))"
      apply (simp add: limit_def)
      done
    also have "natUnion (λ i. limit f (C i)) = natUnion ((limit f) o C)"
      apply (subst comp)
      apply simp
      done
    finally show "(limit f) (natUnion C) = natUnion ((limit f) o C)" by blast
  qed
  with chain show ?thesis by (simp add: continuous_def)
qed   
      
lemma regular_limit: "regular f ==> regular (limit f)"
by (simp add: continuous_limit regular_def setmonotone_limit)

lemma regular_implies_mono: "regular f ==> mono f"
by (simp add: continuous_imp_mono regular_def)

lemma regular_implies_setmonotone: "regular f ==> setmonotone f"
by (simp add: regular_def)
  
lemma regular_implies_continuous: "regular f ==> continuous f"
by (simp add: regular_def)

end