theory "Value"
imports HOLCF
begin
subsubsection {* The semantic domain for values and environments *}
domain Value = Fn (lazy "Value \ Value")
fixrec Fn_project :: "Value \ Value \ Value"
where "Fn_project\(Fn\f) = f"
abbreviation Fn_project_abbr (infix "\Fn" 55)
where "f \Fn v \ Fn_project\f\v"
lemma [simp]: "\ \Fn x = \"
by (fixrec_simp)
text {*
A chain in the domain @{typ Value} is either always bottom, or eventually @{term "Fn"} of another
chain
*}
lemma Value_chainE:
assumes "chain Y"
obtains "Y = (\ _ . \)" |
n Y' where "Y = (\ m. (if m < n then \ else Fn\(Y' (m-n))))" "chain Y'"
proof(cases "Y = (\ _ . \)")
case True
thus ?thesis by (rule that(1))
next
case False
hence "\ i. Y i \ \" by auto
hence "\ n. Y n \ \ \ (\m. Y m \ \ \ m \ n)"
by (rule exE)(rule ex_has_least_nat)
then obtain n where "Y n \ \" and "\m. m < n \ Y m = \" by fastforce
then obtain f where "Y n = Fn \ f" by (metis Value.exhaust)
{
fix i
from `chain Y` have "Y n \ Y (i+n)" by (metis chain_mono le_add2)
with `Y n = _`
have "\ g. (Y (i+n) = Fn \ g)" by (metis (full_types) Value.exhaust minimal po_eq_conv)
}
then obtain Y' where Y': "\ i. Y (i + n) = Fn \ (Y' i)" by metis
have "Y = (\m. if m < n then \ else Fn\(Y' (m - n)))"
using `\m. _` Y' by (metis add_diff_inverse add.commute)
moreover
have"chain Y'" using `chain Y`
by (auto intro!:chainI elim: chainE simp add: Value.inverts[symmetric] Y'[symmetric] simp del: Value.inverts)
ultimately
show ?thesis by (rule that(2))
qed
end