Theory FixTransform

section ‹Fixed point transformations›

theory FixTransform
imports HOLCF
begin

default_sort type

text ‹
In his treatment of the computabily, Shivers gives proofs only for a generic example and leaves it to the reader to apply this to the mutually recursive functions used for the semantics. As we carry this out, we need to transform a fixed point for two functions (implemented in @{theory HOLCF} as a fixed point over a tuple) to a simple fixed point equation. The approach here works as long as both functions in the tuple have the same return type, using the equation
\[
X^A\cdot X^B = X^{A+B}.
\]

Generally, a fixed point can be transformed using any retractable continuous function:
›

lemma fix_transform:
  assumes "⋀x. g⋅(f⋅x)=x"
  shows "fix⋅F = g⋅(fix⋅(f oo F oo g))"
using assms apply -
apply (rule parallel_fix_ind)
apply (rule adm_eq)
apply auto
apply (erule retraction_strict[of g f,rule_format])
done

text ‹
The functions we use here convert a tuple of functions to a function taking a direct sum as parameters and back. We only care about discrete arguments here.
›

definition tup_to_sum :: "('a discr → 'c) × ('b discr → 'c) → ('a + 'b) discr → 'c::cpo"
 where "tup_to_sum = (Λ p s. (λ(f,g).
          case undiscr s of Inl x ⇒ f⋅(Discr x)
                          | Inr x ⇒ g⋅(Discr x)) p)"

definition sum_to_tup :: "(('a + 'b) discr → 'c) → ('a discr → 'c) × ('b discr → 'c::cpo)"
 where "sum_to_tup = (Λ f. (Λ x. f⋅(Discr (Inl (undiscr x))),
                             Λ x. f⋅(Discr (Inr (undiscr x)))))"

text ‹
As so often when working with @{theory HOLCF}, some continuity lemmas are required.
›

lemma cont2cont_case_sum[simp,cont2cont]:
  assumes "cont f" and "cont g"
  shows "cont (λx. case_sum (f x) (g x) s)"
using assms
by (cases s, auto intro:cont2cont_fun)

lemma cont2cont_circ[simp,cont2cont]:
 "cont (λf. f ∘ g)"
apply (rule cont2cont_lambda)
apply (subst comp_def)
apply (rule  cont2cont_fun[of "λx. x", OF "cont_id"])
done

lemma cont2cont_split_pair[cont2cont,simp]:
 assumes f1: "cont f"
     and f2: "⋀ x. cont (f x)"
     and g1: "cont g"
     and g2: "⋀ x. cont (g x)"
 shows "cont (λ(a, b). (f a b, g a b))"
apply (intro cont2cont)
apply (rule cont_apply[OF cont_snd _ cont_const])
apply (rule cont_apply[OF cont_snd f2])
apply (rule cont_apply[OF cont_fst cont2cont_fun[OF f1] cont_const])

apply (rule cont_apply[OF cont_snd _ cont_const])
apply (rule cont_apply[OF cont_snd g2])
apply (rule cont_apply[OF cont_fst cont2cont_fun[OF g1] cont_const])
done

text ‹
Using these continuity lemmas, we can show that our function are actually continuous and thus allow us to apply them to a value.
›

lemma sum_to_tup_app:
 "sum_to_tup⋅f = (Λ x. f⋅(Discr (Inl (undiscr x))), Λ x. f⋅(Discr (Inr (undiscr x))))"
unfolding sum_to_tup_def by simp

lemma tup_to_sum_app:
  "tup_to_sum⋅p = (Λ s. (λ(f,g).
          case undiscr s of Inl x ⇒ f⋅(Discr x)
                          | Inr x ⇒ g⋅(Discr x)) p)"
unfolding tup_to_sum_def by simp

text ‹
Generally, lambda abstractions with discrete domain are continuous and can be resolved immediately.
›

lemma discr_app[simp]:
  "(Λ s. f s)⋅(Discr x) = f (Discr x)"
by simp

text ‹
Our transformation functions are inverse to each other, so we can use them to transform a fixed point.
›

lemma tup_to_sum_to_tup[simp]:
  shows   "sum_to_tup⋅(tup_to_sum⋅F) = F"
unfolding sum_to_tup_app and tup_to_sum_app
by (cases F, auto intro:cfun_eqI)

lemma fix_transform_pair_sum:
  shows "fix⋅F = sum_to_tup⋅(fix⋅(tup_to_sum oo F oo sum_to_tup))"
by (rule fix_transform[OF tup_to_sum_to_tup])

text ‹
After such a transformation, we want to get rid of these helper functions again. This is done by the next two simplification lemmas.
›

lemma tup_sum_oo[simp]:
 assumes f1: "cont F"
     and f2: "⋀ x. cont (F x)"
     and g1: "cont G"
     and g2: "⋀ x. cont (G x)"
shows  "tup_to_sum oo (Λ p. (λ(a, b). (F a b, G a b)) p) oo sum_to_tup
  = (Λ f s. (case undiscr s of
        Inl x ⇒
          F (Λ s. f⋅(Discr (Inl (undiscr s))))
           (Λ s. f⋅(Discr (Inr (undiscr s))))⋅
          (Discr x)
        | Inr x ⇒
            G (Λ s. f⋅(Discr (Inl (undiscr s))))
             (Λ s. f⋅(Discr (Inr (undiscr s))))⋅
            (Discr x)))"
by (rule cfun_eqI, rule cfun_eqI,
    simp add: sum_to_tup_app tup_to_sum_app
       cont2cont_split_pair[OF f1 f2 g1 g2]
       cont2cont_lambda
       cont_apply[OF _ f2 cont2cont_fun[OF cont_compose[OF f1]]]
       cont_apply[OF _ g2 cont2cont_fun[OF cont_compose[OF g1]]])

lemma fst_sum_to_tup[simp]:
  "fst (sum_to_tup⋅x) = (Λ xa. x⋅(Discr (Inl (undiscr xa))))"
by (simp add: sum_to_tup_app)

end