Theory Iterative

theory Iterative
imports "Env-HOLCF"
begin

text ‹
A setup for defining a fixed point of mutual recursive environments iteratively
›

locale iterative =
  fixes ρ :: "'a::type ⇒ 'b::pcpo"
   and e1 :: "('a ⇒ 'b) → ('a ⇒ 'b)"
   and e2 :: "('a ⇒ 'b) → 'b"
   and S :: "'a set" and x :: 'a
  assumes ne:"x ∉ S"
begin
  abbreviation "L == (Λ ρ'. (ρ ++⇘S⇙ e1 ⋅ ρ')(x := e2 ⋅ ρ'))"
  abbreviation "H == (λ ρ'. Λ ρ''. ρ' ++⇘S⇙ e1 ⋅ ρ'')"
  abbreviation "R == (Λ ρ'. (ρ ++⇘S⇙ (fix ⋅ (H ρ')))(x := e2 ⋅ ρ'))"
  abbreviation "R' == (Λ ρ'. (ρ ++⇘S⇙ (fix ⋅ (H ρ')))(x := e2 ⋅ (fix ⋅ (H ρ'))))"

  lemma split_x:
    fixes y
    obtains "y = x" and "y ∉ S" | "y ∈ S" and "y ≠ x" | "y ∉ S" and "y ≠ x" using ne by blast
  lemmas below = fun_belowI[OF split_x, where y1 = "λx. x"]
  lemmas eq = ext[OF split_x, where y1 = "λx. x"]

  lemma lookup_fix[simp]:
    fixes y and F :: "('a ⇒ 'b) → ('a ⇒ 'b)"
    shows "(fix ⋅ F) y = (F ⋅ (fix ⋅ F)) y"
    by (subst fix_eq, rule)

  lemma R_S: "⋀ y. y ∈ S ⟹ (fix ⋅ R) y = (e1 ⋅ (fix ⋅ (H (fix ⋅ R)))) y"
    by (case_tac y rule: split_x) simp_all

  lemma R'_S: "⋀ y. y ∈ S ⟹ (fix ⋅ R') y = (e1 ⋅ (fix ⋅ (H (fix ⋅ R')))) y"
    by (case_tac y rule: split_x) simp_all

  lemma HR_is_R[simp]: "fix⋅(H (fix ⋅ R)) = fix ⋅ R"
    by (rule eq) simp_all

  lemma HR'_is_R'[simp]: "fix ⋅ (H (fix ⋅ R')) = fix ⋅ R'"
    by (rule eq) simp_all

  lemma H_noop:
    fixes ρ' ρ''
    assumes "⋀ y. y ∈ S ⟹ y ≠ x ⟹ (e1 ⋅ ρ'') y ⊑ ρ' y"
    shows "H ρ' ⋅ ρ'' ⊑ ρ'"
      using assms
      by -(rule below, simp_all)

  lemma HL_is_L[simp]: "fix ⋅ (H (fix ⋅ L)) = fix ⋅ L"
  proof (rule below_antisym)
    show "fix ⋅ (H (fix ⋅ L)) ⊑ fix ⋅ L"
      by (rule fix_least_below[OF H_noop]) simp
    hence *: "e2 ⋅ (fix ⋅ (H (fix ⋅ L))) ⊑ e2 ⋅ (fix ⋅ L)" by (rule monofun_cfun_arg)

    show "fix ⋅ L ⊑ fix ⋅ (H (fix ⋅ L))"
      by (rule fix_least_below[OF below]) (simp_all add: ne *)
  qed
  
  lemma iterative_override_on:
    shows "fix ⋅ L = fix ⋅ R"
  proof(rule below_antisym)
    show "fix ⋅ R ⊑ fix ⋅ L"
      by (rule fix_least_below[OF below]) simp_all

    show "fix ⋅ L ⊑ fix ⋅ R"
      apply (rule fix_least_below[OF below])
      apply simp
      apply (simp del: lookup_fix add: R_S)
      apply simp
      done
  qed

  lemma iterative_override_on':
    shows "fix ⋅ L = fix ⋅  R'"
  proof(rule below_antisym)
    show "fix ⋅ R' ⊑ fix ⋅ L"
      by (rule fix_least_below[OF below]) simp_all
  
    show "fix ⋅ L ⊑ fix ⋅ R'"
      apply (rule fix_least_below[OF below])
      apply simp
      apply (simp del: lookup_fix add: R'_S)
      apply simp
      done
  qed
end

end