theory "Correctness-Counterexample"
imports "Denotational" Launchbury
begin
text {* In this theory we show that Theorem 2 in Launchbury's original paper \cite{launchbury} does not hold if one
takes @{text "\"} to mean the least upper bound, by giving a counter example. *}
(* TODO: State using HSem, not USemUpd *)
theorem counterexample:
assumes correct: "
\ \ e L \ z \.
\ \ : e \\<^bsub>L\<^esub> \ : z;
distinctVars \;
fdom \ - heapVars \ \ set L
\ \
\e\\<^bsub>\\\\\<^esub> = \z\\<^bsub>\\\\\<^esub>"
shows False
proof-
txt {* We need several variables; for two of them we require that they are different from each other. *}
obtain x :: var where True by metis
obtain a :: var where True by metis
obtain b :: var where "atom b \ a" by (rule obtain_fresh)
hence [simp]:"b \ a" by (simp add: fresh_at_base)
txt {* Two distinct, but compatible elements of type @{typ Value}. *}
def id \ "Fn\(\ x. x)"
def const \ "\ y. Fn\(\ x. y)"
have "const id \Fn id \ const \ \Fn id"
by (simp only: const_def id_def Fn_project.simps beta_cfun cont2cont Value.con_rews not_False_eq_True)
hence "const id \ const \" by auto
have [simp]:"compatible (const id) (const \)"
by (auto intro: compatibleI[where z = "const id"] simp add: const_def id_def)
txt {* This is how we instantiate the theorem. *}
def e \ "Var x"
def z \ "Lam [a]. let b be Var b in Var b"
def \ \ "[(x, z)]"
def \ \ "[(x, z)]"
def \ \ "fempty( x f\ const id )"
txt {* Establish the denotation of our terms (this involves picking fresh variables). *}
have [simp]: "\ \. \let b be Var b in Var b\\<^bsub>\\<^esub> = \"
proof-
fix \ :: Env
obtain b' :: var where fresh: "atom b' \ (b,\)" by (rule obtain_fresh)
hence "b' \ b" "atom b' \ \" and [simp]: "b' \ fdom \"
by (auto simp add: fresh_Pair fresh_at_base fresh_fmap_pure)
have "let b be Var b in Var b = let b' be Var b' in Var b'"
apply simp
apply (subst Abs_swap2[where a = "atom b" and b = "atom b'"])
apply (auto simp add: exp_assn.bn_defs exp_assn.supp supp_Pair supp_at_base)
done
also
have "\\\\<^bsub>\\<^esub> = \Var b'\\<^bsub>\[(b', Var b')]\\\<^esub>"
using `atom b' \ \`
by (auto simp add: fresh_star_def exp_assn.bn_defs)
also have "\ = \[(b', Var b')]\\ f!\<^sub>\ b'" by simp
also have "\ = \"
apply (rule HSem_ind)
apply (rule adm_is_adm_on)
apply auto[1]
apply (simp add: to_bot_fmap_def)
apply (subst fmap_lookup_bot_join[OF rho_F_compat_fjc], assumption)
apply simp_all
done
finally
show "\let b be Var b in Var b\\<^bsub>\\<^esub> = \".
qed
have [simp]: "\ \. \z\\<^bsub>\\<^esub> = const \"
proof-
fix \ :: Env
obtain a' :: var where fresh: "atom a' \ (b,\)" by (rule obtain_fresh)
hence [simp]:"b \ a'" "atom a' \ \"
by (auto simp add: fresh_Pair fresh_at_base sharp_Env)
have "z = Lam [a]. let b be Var b in Var b" unfolding z_def..
also have "\ = Lam [a']. let b be Var b in Var b"
apply (simp add: fresh_Pair)
by (metis `b \ a'` `b \ a` flip_at_base_simps(3) not_self_fresh)
also have "\\\\<^bsub>\\<^esub> = const \"
by (simp add: const_def)
finally show "\z\\<^bsub>\\<^esub> = const \".
qed
txt {* Establish that all joins occuring in the proof are well-defined. *}
have cond: "HSem_cond'' \ \"
apply (intro fix_join_condI cont_compose[OF fmap_expand_cont cont2cont_heapToEnv] ESem_cont)
apply (rule compatible_fmapI)
apply (auto simp add: \_def \_def)
done
txt {* On the one hand, we have an equality according to theorem 2. *}
have "\ : e \\<^bsub>[]\<^esub> \ : z"
unfolding \_def \_def e_def z_def
by (auto intro!: reds.intros)
moreover
have "distinctVars \" by (simp add: \_def)
moreover
have "fdom \ - heapVars \ \ set []" by (simp add: \_def \_def)
ultimately
have "\e\\<^bsub>\\\\\<^esub> = \z\\<^bsub>\\\\\<^esub>"
by (rule correct)
moreover
txt {* On the other hand, we have an inequality between the same terms. *}
{
have "\e\\<^bsub>\\\\\<^esub> = \\\\ f!\<^sub>\ x"
by (simp add: e_def)
also have "\ = (\ f! x) \ (\z\\<^bsub>\\\\\<^esub>)"
by (simp add: \_def \_def the_lookup_HSem_both[OF cond, unfolded \_def \_def])
also have "\ = const id \ const \"
by (simp add: \_def)
also have "\ = const id"
by (auto intro: larger_is_join1 simp add: const_def)
also have "\ \ const \"
by fact
also have "const \ = \z\\<^bsub>\\\\\<^esub>" by simp
finally
have "\e\\<^bsub>\\\\\<^esub> \ \z\\<^bsub>\\\\\<^esub>".
}
ultimately
txt {* So clearly, this is a contradiction. *}
show False by metis
qed
oops
end