Theory CoCallImplSafe

theory CoCallImplSafe
imports CoCallAnalysisImpl CoCallAnalysisSpec ArityAnalysisFixProps
begin

locale CoCallImplSafe
begin
sublocale CoCallAnalysisImpl.

lemma ccNeighbors_Int_ccrestr: "(ccNeighbors x G ∩ S) = ccNeighbors x (cc_restr (insert x S) G) ∩ S"
  by transfer auto
  
lemma 
  assumes "x ∉ S" and "y ∉ S"
  shows CCexp_subst: "cc_restr S (CCexp e[y::=x]⋅a) = cc_restr S (CCexp e⋅a)"
    and Aexp_restr_subst: "(Aexp e[y::=x]⋅a) f|` S = (Aexp e⋅a) f|` S"
using assms
proof (nominal_induct e avoiding: x y  arbitrary: a  S rule: exp_strong_induct_rec_set)
  case (Var b v) 
  case 1 show ?case by auto
  case 2 thus ?case by auto
next
  case (App e v)
  case 1
    with App show ?case
    by (auto simp add: Int_insert_left fv_subst_int simp del: join_comm intro: join_mono)
  case 2
    with App show ?case
     by (auto simp add: env_restr_join simp del: fun_meet_simp)
next
  case (Lam v e)
  case 1
    with Lam
    show ?case
      by (auto simp add: CCexp_pre_simps cc_restr_predCC  Diff_Int_distrib2 fv_subst_int env_restr_join env_delete_env_restr_swap[symmetric] simp del: CCexp_simps)
  case 2
    with Lam
    show ?case
      by (auto simp add: env_restr_join env_delete_env_restr_swap[symmetric]  simp del: fun_meet_simp)
next
  case (Let Γ e x y)
  hence [simp]: "x ∉ domA Γ " "y ∉ domA Γ"
    by (metis (erased, opaque_lifting) bn_subst domA_not_fresh fresh_def fresh_star_at_base fresh_star_def obtain_fresh subst_is_fresh(2))+

  note Let(1,2)[simp]

  from Let(3)
  have "¬ nonrec (Γ[y::h=x])"  by (simp add: nonrec_subst)

  case [simp]: 1
  have "cc_restr (S ∪ domA Γ) (CCfix Γ[y::h=x]⋅(Afix Γ[y::h=x]⋅(Aexp e[y::=x]⋅a ⊔ (λ_. up⋅0) f|` thunks Γ), CCexp e[y::=x]⋅a)) =
        cc_restr (S ∪ domA Γ) (CCfix Γ⋅        (Afix Γ⋅        (Aexp e⋅       a ⊔ (λ_. up⋅0) f|` thunks Γ), CCexp e⋅       a))"
    apply (subst CCfix_restr_subst')
      apply (erule Let(4))
      apply auto[5]
    apply (subst CCfix_restr) back
      apply simp
    apply (subst Afix_restr_subst')
      apply (erule Let(5))
      apply auto[5]
    apply (subst Afix_restr) back
      apply simp
    apply (simp only: env_restr_join)
    apply (subst Let(7))
      apply auto[2]
    apply (subst Let(6))
      apply auto[2]
    apply rule
    done
  thus ?case using Let(1,2) ‹¬ nonrec Γ› ‹¬ nonrec (Γ[y::h=x])›
    by (auto simp add: fresh_star_Pair  elim: cc_restr_eq_subset[rotated] )

  case [simp]: 2
  have "Afix Γ[y::h=x]⋅(Aexp e[y::=x]⋅a ⊔ (λ_. up⋅0) f|` (thunks Γ)) f|` (S ∪ domA Γ) = Afix Γ⋅(Aexp e⋅a ⊔ (λ_. up⋅0) f|` (thunks Γ)) f|` (S ∪ domA Γ)"
    apply (subst Afix_restr_subst')
      apply (erule Let(5))
      apply auto[5]
    apply (subst Afix_restr) back
      apply auto[1]
    apply (simp only: env_restr_join)
    apply (subst Let(7))
      apply auto[2]
    apply rule
    done
  thus ?case using Let(1,2)
    using ‹¬ nonrec Γ› ‹¬ nonrec (Γ[y::h=x])›
    by (auto simp add: fresh_star_Pair elim:env_restr_eq_subset[rotated])
next
  case (Let_nonrec x' e exp x y)

  from Let_nonrec(1,2)
  have  "x ≠ x'" "y ≠ x'" by (simp_all add: fresh_at_base)

  note Let_nonrec(1,2)[simp]
  
  from ‹x' ∉ fv e› ‹y ≠ x'› ‹x ≠ x'›
  have [simp]: "x' ∉ fv (e[y::=x])"
    by (auto simp add: fv_subst_eq)

  note ‹x' ∉ fv e›[simp] ‹y ≠ x'› [simp]‹x ≠ x'›  [simp]

  case [simp]: 1

  have "⋀ a. cc_restr {x'} (CCexp exp[y::=x]⋅a) = cc_restr {x'} (CCexp exp⋅a)"
   by (rule Let_nonrec(6)) auto
  from arg_cong[where f = "λx.  x'--x'∈x", OF this]
  have [simp]: "x'--x'∈CCexp  exp[y::=x]⋅a ⟷ x'--x'∈CCexp exp⋅a" by auto

  have [simp]: "⋀ a. Aexp e[y::=x]⋅a f|` S = Aexp e⋅a f|` S"
    by (rule Let_nonrec(5)) auto

  have [simp]: "⋀ a. fup⋅(Aexp e[y::=x])⋅a f|` S = fup⋅(Aexp e)⋅a f|` S"
    by (case_tac a) auto

  have [simp]: "Aexp  exp[y::=x]⋅a f|` S = Aexp exp⋅a f|` S"
    by (rule Let_nonrec(7)) auto

  have "Aexp exp[y::=x]⋅a f|` {x'} = Aexp exp⋅a f|` {x'}"
    by (rule Let_nonrec(7)) auto
  from fun_cong[OF this, where x = x']
  have [simp]: "(Aexp exp[y::=x]⋅a) x' = (Aexp exp⋅a) x'" by auto

  have [simp]:  "⋀ a. cc_restr S (CCexp exp[y::=x]⋅a) = cc_restr S (CCexp exp⋅a)"
    by (rule Let_nonrec(6)) auto

  have [simp]:  "⋀ a. cc_restr S (CCexp e[y::=x]⋅a) = cc_restr S (CCexp e⋅a)"
    by (rule Let_nonrec(4)) auto

  have [simp]: "⋀ a. cc_restr S (fup⋅(CCexp e[y::=x])⋅a) = cc_restr S (fup⋅(CCexp e)⋅a)"
    by (rule fup_ccExp_restr_subst') simp

  have [simp]: "fv e[y::=x] ∩ S = fv e ∩ S"
    by (auto simp add: fv_subst_eq)

  have [simp]:
    "ccNeighbors x' (CCexp exp[y::=x]⋅a) ∩ - {x'} ∩ S = ccNeighbors x' (CCexp exp⋅a)  ∩ - {x'} ∩ S"
    apply (simp only: Int_assoc)
    apply (subst (1 2) ccNeighbors_Int_ccrestr)
    apply (subst Let_nonrec(6))
      apply auto[2]
    apply rule
    done

  have [simp]:
    "ccNeighbors x' (CCexp exp[y::=x]⋅a) ∩ S = ccNeighbors x' (CCexp exp⋅a) ∩ S"
    apply (subst (1 2) ccNeighbors_Int_ccrestr)
    apply (subst Let_nonrec(6))
      apply auto[2]
    apply rule
    done

  show "cc_restr S (CCexp (let x' be e in exp )[y::=x]⋅a) = cc_restr S (CCexp (let x' be e in exp )⋅a)"
    apply (subst subst_let_be)
      apply auto[2]
    apply (subst (1 2) CCexp_simps(6))
      apply fact+
    apply (simp only: cc_restr_cc_delete_twist)
    apply (rule arg_cong) back
    apply (simp add:  Diff_eq ccBind_eq ABind_nonrec_eq)
    done

  show "Aexp (let x' be e in exp )[y::=x]⋅a f|` S = Aexp (let x' be e in exp )⋅a f|` S"
    by (simp add: env_restr_join env_delete_env_restr_swap[symmetric] ABind_nonrec_eq)
next
  case (IfThenElse scrut e1 e2)
  case [simp]: 2
    from IfThenElse
    show "cc_restr S (CCexp (scrut ? e1 : e2)[y::=x]⋅a) = cc_restr S (CCexp (scrut ? e1 : e2)⋅a)"
      by (auto simp del: edom_env env_restr_empty env_restr_empty_iff simp  add: edom_env[symmetric])

    from IfThenElse(2,4,6)
    show "Aexp (scrut ? e1 : e2)[y::=x]⋅a f|` S = Aexp (scrut ? e1 : e2)⋅a f|` S"
       by (auto simp add: env_restr_join simp del: fun_meet_simp)
qed auto
   
sublocale ArityAnalysisSafe Aexp
  by standard (simp_all add:Aexp_restr_subst)


sublocale ArityAnalysisLetSafe Aexp Aheap
proof
  fix Γ e a
  show "edom (Aheap Γ e⋅a) ⊆ domA Γ"
    by (cases "nonrec Γ")
       (auto simp add: Aheap_nonrec_simp dest: subsetD[OF edom_esing_subset] elim!: nonrecE)
next
  fix x y :: var and Γ :: heap and e :: exp
  assume assms: "x ∉ domA Γ"  "y ∉ domA Γ"

  from Aexp_restr_subst[OF assms(2,1)]
  have **: "⋀ a. Aexp e[x::=y]⋅a f|` domA Γ = Aexp e⋅a f|` domA Γ".

  show "Aheap Γ[x::h=y] e[x::=y] = Aheap Γ e"
  proof(cases "nonrec Γ")
    case [simp]: False

    from assms
    have "atom ` domA Γ ♯* x" and "atom ` domA Γ ♯* y"
      by (auto simp add: fresh_star_at_base image_iff)
    hence [simp]: "¬ nonrec (Γ[x::h=y])"
      by (simp add: nonrec_subst)

    show ?thesis
    apply (rule cfun_eqI)
    apply simp
    apply (subst Afix_restr_subst[OF assms subset_refl])
    apply (subst Afix_restr[OF  subset_refl]) back
    apply (simp add: env_restr_join)
    apply (subst **)
    apply simp
    done
  next
    case True
    
    from assms
    have "atom ` domA Γ ♯* x" and "atom ` domA Γ ♯* y"
      by (auto simp add: fresh_star_at_base image_iff)
    with True
    have *: "nonrec (Γ[x::h=y])" by (simp add: nonrec_subst)

    from True
    obtain x' e' where [simp]: "Γ = [(x',e')]" "x' ∉ fv e'" by (auto elim: nonrecE)

    from * have [simp]: "x' ∉ fv (e'[x::=y])"
      by (auto simp add: nonrec_def)

    from fun_cong[OF **, where x = x']
    have [simp]: "⋀ a. (Aexp e[x::=y]⋅a) x' = (Aexp e⋅a) x'" by simp

    from CCexp_subst[OF assms(2,1)]
    have "⋀ a.  cc_restr {x'} (CCexp e[x::=y]⋅a) = cc_restr {x'} (CCexp e⋅a)" by simp
    from arg_cong[where f = "λx.  x'--x'∈x", OF this]
    have [simp]: "⋀ a. x'--x'∈(CCexp e[x::=y]⋅a) ⟷ x'--x'∈(CCexp e⋅a)" by simp
    
    show ?thesis
      apply -
      apply (rule cfun_eqI)
      apply (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq)
      done
  qed
next
  fix Γ e a
  show "ABinds Γ⋅(Aheap Γ e⋅a) ⊔ Aexp e⋅a ⊑ Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a"
  proof(cases "nonrec Γ")
    case False
    thus ?thesis
      by (auto simp add: Aheap_def join_below_iff env_restr_join2 Compl_partition intro:  below_trans[OF _ Afix_above_arg])
  next
    case True
    then obtain x e' where [simp]: "Γ = [(x,e')]" "x ∉ fv e'" by (auto elim: nonrecE)

    hence "⋀ a. x ∉ edom (fup⋅(Aexp e')⋅a)"
      by (auto dest:subsetD[OF fup_Aexp_edom])
    hence [simp]: "⋀ a. (fup⋅(Aexp e')⋅a) x = ⊥" by (simp add: edomIff)

    show ?thesis
      apply (rule env_restr_below_split[where S = "{x}"])
      apply (rule env_restr_belowI2)
      apply (auto simp add:  Aheap_nonrec_simp  join_below_iff env_restr_join env_delete_restr)
      apply (rule ABind_nonrec_above_arg)
      apply (rule below_trans[OF _ join_above2])
      apply (rule below_trans[OF _ join_above2])
      apply (rule below_refl)
      done
  qed
qed

definition ccHeap_nonrec
  where "ccHeap_nonrec x e exp = (Λ n. CCfix_nonrec x e⋅(Aexp exp⋅n, CCexp exp⋅n))"

lemma ccHeap_nonrec_eq:
   "ccHeap_nonrec x e exp⋅n = CCfix_nonrec x e⋅(Aexp exp⋅n, CCexp exp⋅n)"
unfolding ccHeap_nonrec_def by (rule beta_cfun) (intro cont2cont)

definition ccHeap_rec :: "heap ⇒ exp ⇒ Arity → CoCalls"
  where "ccHeap_rec Γ e  = (Λ a. CCfix Γ⋅(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0) f|` (thunks Γ)), CCexp e⋅a))"

lemma ccHeap_rec_eq:
  "ccHeap_rec Γ e⋅a = CCfix Γ⋅(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0) f|` (thunks Γ)), CCexp e⋅a)"
unfolding ccHeap_rec_def by simp

definition ccHeap :: "heap ⇒ exp ⇒ Arity → CoCalls"
  where "ccHeap Γ  = (if nonrec Γ then case_prod ccHeap_nonrec (hd Γ) else ccHeap_rec Γ)"

lemma ccHeap_simp1:
  "¬ nonrec Γ ⟹ ccHeap Γ e⋅a = CCfix Γ⋅(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0) f|` (thunks Γ)), CCexp e⋅a)"
  by (simp add: ccHeap_def ccHeap_rec_eq)

lemma ccHeap_simp2:
  "x ∉ fv e ⟹ ccHeap [(x,e)] exp⋅n = CCfix_nonrec x e⋅(Aexp exp⋅n, CCexp exp⋅n)"
  by (simp add: ccHeap_def ccHeap_nonrec_eq nonrec_def)


sublocale CoCallAritySafe CCexp Aexp ccHeap Aheap
proof
  fix e a x
  show "CCexp e⋅(inc⋅a) ⊔ ccProd {x} (insert x (fv e)) ⊑ CCexp (App e x)⋅a"
    by simp
next
  fix y e n
  show "cc_restr (fv (Lam [y]. e)) (CCexp e⋅(pred⋅n)) ⊑ CCexp (Lam [y]. e)⋅n"
    by (auto simp add: CCexp_pre_simps predCC_eq dest!: subsetD[OF ccField_cc_restr] simp del: CCexp_simps)
next
  fix x y :: var and S e a
  assume "x ∉ S"  and "y ∉ S"
  thus "cc_restr S (CCexp e[y::=x]⋅a) ⊑ cc_restr S (CCexp e⋅a)"
    by (rule eq_imp_below[OF CCexp_subst])
next
  fix e
  assume "isVal e"
  thus "CCexp e⋅0 = ccSquare (fv e)"
    by (induction e rule: isVal.induct) (auto simp add: predCC_eq)
next
  fix Γ e a
  show "cc_restr (- domA Γ) (ccHeap Γ e⋅a) ⊑ CCexp (Let Γ e)⋅a"
  proof(cases "nonrec Γ")
    case False
    thus "cc_restr (- domA Γ) (ccHeap Γ e⋅a) ⊑ CCexp (Let Γ e)⋅a"
      by (simp add: ccHeap_simp1[OF False, symmetric] del: cc_restr_join)
  next
    case True
    thus ?thesis
      by (auto simp add: ccHeap_simp2 Diff_eq elim!: nonrecE simp del: cc_restr_join)
  qed
next
  fix Δ :: heap and e a

  show "CCexp e⋅a ⊑ ccHeap Δ e⋅a"
    by (cases "nonrec Δ")
       (auto simp add: ccHeap_simp1 ccHeap_simp2 arg_cong[OF CCfix_unroll, where f = "(⊑) x" for x ] elim!: nonrecE)

  fix x e' a'
  assume "map_of Δ x = Some e'"
  hence [simp]: "x ∈ domA Δ" by (metis domI dom_map_of_conv_domA) 
  assume "(Aheap Δ e⋅a) x = up⋅a'"
  show "CCexp e'⋅a' ⊑ ccHeap Δ e⋅a"
  proof(cases "nonrec Δ")
    case False

    from ‹(Aheap Δ e⋅a) x = up⋅a'› False
    have "(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ))) x = up⋅a'" 
      by (simp add: Aheap_def)
    hence "CCexp e'⋅a' ⊑ ccBind x e'⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), CCfix Δ⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), CCexp e⋅a))"
      by (auto simp add: ccBind_eq dest: subsetD[OF ccField_CCexp])
    also
    have "ccBind x e'⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), CCfix Δ⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), CCexp e⋅a)) ⊑  ccHeap Δ e⋅a"
      using ‹map_of Δ x = Some e'› False
      by (fastforce simp add: ccHeap_simp1 ccHeap_rec_eq ccBindsExtra_simp  ccBinds_eq  arg_cong[OF CCfix_unroll, where f = "(⊑) x" for x ]
                  intro: below_trans[OF _ join_above2])
    finally
    show "CCexp e'⋅a' ⊑ ccHeap Δ e⋅a" by this simp_all
  next
    case True
    with ‹map_of Δ x = Some e'›
    have [simp]: "Δ = [(x,e')]" "x ∉ fv e'" by (auto elim!: nonrecE split: if_splits)

    show ?thesis
    proof(cases "x--x∉CCexp e⋅a ∨ isVal e'")
      case True
      with ‹(Aheap Δ e⋅a) x = up⋅a'›
      have [simp]: "(CoCallArityAnalysis.Aexp cCCexp e⋅a) x = up⋅a'"
        by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq split: if_splits)

      have "CCexp e'⋅a' ⊑ ccSquare (fv e')"
        unfolding below_ccSquare
        by (rule ccField_CCexp)
      then
      show ?thesis using True
        by (auto simp add: ccHeap_simp2 ccBind_eq Aheap_nonrec_simp ABind_nonrec_eq below_trans[OF _ join_above2] simp del: below_ccSquare )
    next
      case False

      from ‹(Aheap Δ e⋅a) x = up⋅a'›
      have [simp]: "a' = 0" using  False
        by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq split: if_splits)

      show ?thesis using False
        by (auto simp add: ccHeap_simp2 ccBind_eq Aheap_nonrec_simp ABind_nonrec_eq simp del: below_ccSquare )
    qed
  qed

  show "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ) ⊑ ccHeap Δ e⋅a" 
  proof (cases "nonrec Δ")
    case [simp]: False

    have "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ) ⊑ ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a))"
      by (rule ccProd_mono2) auto
    also have "… ⊑ (⨆x↦e'∈map_of Δ. ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a)))" 
      using ‹map_of Δ x = Some e'› by (rule below_lubmapI)
    also have "… ⊑ ccBindsExtra Δ⋅(Afix Δ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Δ)), ccHeap Δ e⋅a)"
      by (simp add: ccBindsExtra_simp  below_trans[OF _ join_above2])
    also have "… ⊑ ccHeap Δ e⋅a"
      by (simp add: ccHeap_simp1  arg_cong[OF CCfix_unroll, where f = "(⊑) x" for x])
    finally
    show ?thesis by this simp_all
  next
    case True
    with ‹map_of Δ x = Some e'›
    have [simp]: "Δ = [(x,e')]" "x ∉ fv e'" by (auto elim!: nonrecE split: if_splits)

    have [simp]: "(ccNeighbors x (ccBind x e'⋅(Aexp e⋅a, CCexp e⋅a))) = {}"
     by (auto simp add: ccBind_eq dest!: subsetD[OF ccField_cc_restr] subsetD[OF ccField_fup_CCexp])

    show ?thesis
    proof(cases "isVal e' ∧ x--x∈CCexp e⋅a")
    case True

    have "ccNeighbors x (ccHeap Δ e⋅a) =
        ccNeighbors x (ccBind x e'⋅(Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a), CCexp e⋅a)) ∪
        ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - (if isVal e' then {} else {x}))) ∪
        ccNeighbors x (CCexp e⋅a)" by (auto simp add: ccHeap_simp2 )
    also have "ccNeighbors x (ccBind  x e'⋅(Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a), CCexp e⋅a)) = {}"
       by (auto simp add: ccBind_eq dest!: subsetD[OF ccField_cc_restr] subsetD[OF ccField_fup_CCexp])
    also have "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - (if isVal e' then {} else {x})))
      ⊆ ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a)))" by (simp add: ccNeighbors_ccProd)
    also have "… ⊆ fv e'" by (simp add: ccNeighbors_ccProd)
    finally
    have "ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ ⊆ ccNeighbors x (CCexp e⋅a) ∪ fv e'" by auto
    hence "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ) ⊑ ccProd (fv e') (ccNeighbors x (CCexp e⋅a) ∪ fv e')" by (rule ccProd_mono2)
    also have "… ⊑ ccProd (fv e') (ccNeighbors x (CCexp e⋅a)) ⊔ ccProd (fv e') (fv e')" by simp
    also have "ccProd (fv e') (ccNeighbors x (CCexp e⋅a)) ⊑ ccHeap Δ e⋅a"
      using ‹map_of Δ x = Some e'› ‹(Aheap Δ e⋅a) x = up⋅a'› True
      by (auto simp add: ccHeap_simp2  below_trans[OF _ join_above2])
    also have "ccProd (fv e') (fv e') = ccSquare (fv e')" by (simp add: ccSquare_def)
    also have "… ⊑ ccHeap Δ e⋅a"
      using ‹map_of Δ x = Some e'› ‹(Aheap Δ e⋅a) x = up⋅a'› True
      by (auto simp add: ccHeap_simp2  ccBind_eq below_trans[OF _ join_above2])
    also note join_self
    finally show ?thesis by this simp_all
  next
    case False
    have "ccNeighbors x (ccHeap Δ e⋅a) =
        ccNeighbors x (ccBind x e'⋅(Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a), CCexp e⋅a)) ∪
        ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - (if isVal e' then {} else {x}))) ∪
        ccNeighbors x (CCexp e⋅a)" by (auto simp add: ccHeap_simp2 )
    also have "ccNeighbors x (ccBind  x e'⋅(Aheap_nonrec x e'⋅(Aexp e⋅a, CCexp e⋅a), CCexp e⋅a)) = {}"
       by (auto simp add: ccBind_eq dest!: subsetD[OF ccField_cc_restr] subsetD[OF ccField_fup_CCexp])
    also have  "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e⋅a) - (if isVal e' then {} else {x}) )) 
      = {}" using False by (auto simp add: ccNeighbors_ccProd)
    finally
    have "ccNeighbors x (ccHeap Δ e⋅a) ⊆ ccNeighbors x (CCexp e⋅a)" by auto
    hence"ccNeighbors x (ccHeap Δ e⋅a)  - {x} ∩ thunks Δ ⊆ ccNeighbors x (CCexp e⋅a)   - {x} ∩ thunks Δ" by auto
    hence "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ ) ⊑ ccProd (fv e') (ccNeighbors x (CCexp e⋅a)  - {x} ∩ thunks Δ )" by (rule ccProd_mono2)
    also have "… ⊑ ccHeap Δ e⋅a"
      using ‹map_of Δ x = Some e'› ‹(Aheap Δ e⋅a) x = up⋅a'› False
      by (auto simp add: ccHeap_simp2  thunks_Cons below_trans[OF _ join_above2])
    finally show ?thesis by this simp_all
   qed
  qed

next
  fix x Γ e a
  assume [simp]: "¬ nonrec Γ"
  assume "x ∈ thunks Γ"
  hence [simp]: "x ∈ domA Γ" by (rule subsetD[OF thunks_domA])
  assume "x ∈ edom (Aheap Γ e⋅a)"

  from ‹x ∈ thunks Γ›
  have "(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Γ))) x = up⋅0" 
    by (subst Afix_unroll) simp

  thus "(Aheap Γ e⋅a) x = up⋅0" by simp
next
  fix x Γ e a
  assume "nonrec Γ"
  then obtain x' e' where [simp]: "Γ = [(x',e')]" "x' ∉ fv e'" by (auto elim: nonrecE)
  assume "x ∈ thunks Γ"
  hence [simp]: "x = x'" "¬ isVal e'" by (auto simp add: thunks_Cons split: if_splits)

  assume "x--x ∈ CCexp e⋅a"
  hence [simp]: "x'--x'∈ CCexp  e⋅a" by simp

  from ‹x ∈ thunks Γ›
  have "(Afix Γ⋅(Aexp e⋅a ⊔ (λ_.up⋅0)f|` (thunks Γ))) x = up⋅0" 
    by (subst Afix_unroll) simp

  show "(Aheap Γ e⋅a) x = up⋅0" by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq)
next
  fix scrut e1 a e2
  show "CCexp scrut⋅0 ⊔ (CCexp e1⋅a ⊔ CCexp e2⋅a) ⊔ ccProd (edom (Aexp scrut⋅0)) (edom (Aexp e1⋅a) ∪ edom (Aexp e2⋅a)) ⊑ CCexp (scrut ? e1 : e2)⋅a"
    by simp
qed
end

end