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