Theory Computability
section ‹Generic Computability›
theory Computability
imports HOLCF HOLCFUtils
begin
text ‹
Shivers proves the computability of the abstract semantics functions only by generic and slightly simplified example. This theory contains the abstract treatment in Section 4.4.3. Later, we will work out the details apply this to ‹\<aPR>›.
›
subsection ‹Non-branching case›
text ‹
After the following lemma (which could go into @{theory HOL.Set_Interval}), we show Shivers' Theorem 10. This says that the least fixed point of the equation
\[
f\ x = g\ x \cup f\ (r\ x)
\]
is given by
\[
f\ x = \bigcup_{i\ge 0} g\ (r^i\ x).
\]
The proof follows the standard proof of showing an equality involving a fixed point: First we show that the right hand side fulfills the above equation and then show that our solution is less than any other solution to that equation.
›
lemma insert_greaterThan:
"insert (n::nat) {n<..} = {n..}"
by auto
lemma theorem10:
fixes g :: "'a::cpo → 'b::type set" and r :: "'a → 'a"
shows "fix⋅(Λ f x. g⋅x ∪ f⋅(r⋅x)) = (Λ x. (⋃i. g⋅(r⇗i⇖⋅x)))"
proof(induct rule:fix_eqI[OF cfun_eqI cfun_belowI, case_names fp least])
case (fp x)
have "g⋅x ∪ (⋃i. g⋅(r⇗i⇖⋅(r⋅x))) = g⋅(r⇗0⇖⋅x) ∪ (⋃i. g⋅(r⇗Suc i⇖⋅x))"
by (simp add: iterate_Suc2 del: iterate_Suc)
also have "… = g⋅(r⇗0⇖⋅x) ∪ (⋃i∈{0<..}. g⋅(r⇗i⇖⋅x))"
using less_iff_Suc_add by auto
also have "… = (⋃i∈insert 0 {0<..}. g⋅(r⇗i⇖⋅x))"
by simp
also have "... = (⋃i. g⋅(r⇗i⇖⋅x))"
by (simp only: insert_greaterThan atLeast_0 )
finally
show ?case by auto
next
case (least f x)
hence expand: "⋀x. f⋅x = (g⋅x ∪ f⋅(r⋅x))" by (auto simp:cfun_eq_iff)
{ fix n
have "f⋅x = (⋃i∈{..n}. g⋅(r⇗i⇖⋅x)) ∪ f⋅(r⇗Suc n⇖⋅x)"
proof(induct n)
case 0 thus ?case by (auto simp add:expand[of x])
case (Suc n)
then have "f⋅x = (⋃i∈{..n}. g⋅(r⇗i⇖⋅x)) ∪ f⋅(r⇗Suc n⇖⋅x)" by simp
also have "… = (⋃i∈{..n}. g⋅(r⇗i⇖⋅x))
∪ g⋅(r⇗Suc n⇖⋅x) ∪ f⋅(r⇗Suc (Suc n)⇖⋅x)"
by(subst expand[of "r⇗Suc n⇖⋅x"], auto)
also have "… = (⋃i∈insert (Suc n) {..n}. g⋅(r⇗i⇖⋅x)) ∪ f⋅(r⇗Suc (Suc n)⇖⋅x)"
by auto
also have "… = (⋃i∈{..Suc n}. g⋅(r⇗i⇖⋅x)) ∪ f⋅(r⇗Suc (Suc n)⇖⋅x)"
by (simp add:atMost_Suc)
finally show ?case .
qed
} note fin = this
have "(⋃i. g⋅(r⇗i⇖⋅x)) ⊆ f⋅x"
proof(rule UN_least)
fix i
show "g⋅(r⇗i⇖⋅x) ⊆ f⋅x"
using fin[of i] by auto
qed
thus ?case
apply (subst sqsubset_is_subset) by auto
qed
subsection ‹Branching case›
text ‹
Actually, our functions are more complicated than the one above: The abstract semantics functions recurse with multiple arguments. So we have to handle a recursive equation of the kind
\[
f\ x = g\ x \cup \bigcup_{a \in R\ x} f\ r.
\]
By moving to the power-set relatives of our function, e.g.
\[
{\uline g}Y = \bigcup_{a\in A} g\ a \quad \text{and} {\uline R}Y = \bigcup_{a\in R} R\ a
\]
the equation becomes
\[
{\uline f}Y ={\uline g}Y \cup {\uline f}\ ({\uline R}Y)
\]
(which is shown in Lemma 11) and we can apply Theorem 10 to obtain Theorem 12.
We define the power-set relative for a function together with some properties.
›
definition powerset_lift :: "('a::cpo → 'b::type set) ⇒ 'a set → 'b set" ("\<^ps>")
where "\<^ps>f = (Λ S. (⋃y∈S . f⋅y))"
lemma powerset_lift_singleton[simp]:
"\<^ps>f⋅{x} = f⋅x"
unfolding powerset_lift_def by simp
lemma powerset_lift_union[simp]:
"\<^ps>f⋅(A ∪ B) = \<^ps>f⋅A ∪ \<^ps>f⋅B"
unfolding powerset_lift_def by auto
lemma UNION_commute:"(⋃x∈A. ⋃y∈B . P x y) = (⋃y∈B. ⋃x∈A . P x y)"
by auto
lemma powerset_lift_UNION:
"(⋃x∈S. \<^ps>g⋅(A x)) = \<^ps>g⋅(⋃x∈S. A x)"
unfolding powerset_lift_def by auto
lemma powerset_lift_iterate_UNION:
"(⋃x∈S. (\<^ps>g)⇗i⇖⋅(A x)) = (\<^ps>g)⇗i⇖⋅(⋃x∈S. A x)"
by (induct i, auto simp add:powerset_lift_UNION)
lemmas powerset_distr = powerset_lift_UNION powerset_lift_iterate_UNION
text ‹
Lemma 11 shows that if a function satisfies the relation with the branching $R$, its power-set function satisfies the powerset variant of the equation.
›
lemma lemma11:
fixes f :: "'a → 'b set" and g :: "'a → 'b set" and R :: "'a → 'a set"
assumes "⋀x. f⋅x = g⋅x ∪ (⋃y∈R⋅x. f⋅y)"
shows "\<^ps>f⋅S = \<^ps>g⋅S ∪ \<^ps>f⋅(\<^ps>R⋅S)"
proof-
have "\<^ps>f⋅S = (⋃x∈S . f⋅x)" unfolding powerset_lift_def by auto
also have "… = (⋃x∈S . g⋅x ∪ (⋃y∈R⋅x. f⋅y))" apply (subst assms) by simp
also have "… = \<^ps>g⋅S ∪ \<^ps>f⋅(\<^ps>R⋅S)" by (auto simp add:powerset_lift_def)
finally
show ?thesis .
qed
text ‹
Theorem 10 as it will be used in Theorem 12.
›
lemmas theorem10ps = theorem10[of "\<^ps>g" "\<^ps>r"] for g r
text ‹
Now we can show Lemma 12: If $F$ is the least solution to the recursive power-set equation, then $x \mapsto F\ {x}$ is the least solution to the equation with branching $R$.
We fix the type variable ‹'a› to be a discrete cpo, as otherwise $x \mapsto \{x\}$ is not continuous.
›
lemma theorem12':
fixes g :: "'a::discrete_cpo → 'b::type set" and R :: "'a → 'a set"
assumes F_fix: "F = fix⋅(Λ F x. \<^ps>g⋅x ∪ F⋅(\<^ps>R⋅x))"
shows "fix⋅(Λ f x. g⋅x ∪ (⋃y∈R⋅x. f⋅y)) = (Λ x. F⋅{x})"
proof(induct rule:fix_eqI[OF cfun_eqI cfun_belowI, case_names fp least])
have F_union: "F = (Λ x. ⋃i. \<^ps>g⋅((\<^ps>R)⇗i⇖⋅x))"
using F_fix by(simp)(rule theorem10ps)
case (fp x)
have "g⋅x ∪ (⋃x'∈R⋅x. F⋅{x'}) = \<^ps>g⋅{x} ∪ F⋅(\<^ps>R⋅{x})"
unfolding powerset_lift_singleton
by (auto simp add: powerset_distr UNION_commute F_union)
also have "… = F⋅{x}"
by (subst (2) fix_eq4[OF F_fix], auto)
finally show ?case by simp
next
case (least f' x)
hence expand: "f' = (Λ x. g⋅x ∪ (⋃y∈R⋅x. f'⋅y))" by simp
have "\<^ps>f' = (Λ S. \<^ps>g⋅S ∪ \<^ps>f'⋅(\<^ps>R⋅S))"
by (subst expand, rule cfun_eqI, auto simp add:powerset_lift_def)
hence "(Λ F. Λ x. \<^ps>g⋅x ∪ F⋅(\<^ps>R⋅x))⋅(\<^ps>f') = \<^ps>f'" by simp
from fix_least[OF this] and F_fix
have "F ⊑ \<^ps>f'" by simp
hence "F⋅{x} ⊑ \<^ps>f'⋅{x}"
by (subst (asm)cfun_below_iff, auto simp del:powerset_lift_singleton)
thus ?case by (auto simp add:sqsubset_is_subset)
qed
lemma theorem12:
fixes g :: "'a::discrete_cpo → 'b::type set" and R :: "'a → 'a set"
shows "fix⋅(Λ f x. g⋅x ∪ (⋃y∈R⋅x. f⋅y))⋅x = \<^ps>g⋅(⋃i.((\<^ps>R)⇗i⇖⋅{x}))"
by(subst theorem12'[OF theorem10ps[THEN sym]], auto simp add:powerset_distr)
end