Theory CoCallImplTTreeSafe

theory CoCallImplTTreeSafe
imports CoCallImplTTree CoCallAnalysisSpec TTreeAnalysisSpec
begin

lemma valid_lists_many_calls:
  assumes "¬ one_call_in_path x p"
  assumes "p ∈ valid_lists S G"
  shows "x--x ∈ G"
using assms(2,1)
proof(induction rule:valid_lists.induct[case_names Nil Cons])
  case Nil thus ?case by simp
next
  case (Cons xs x')
  show ?case
  proof(cases "one_call_in_path x xs")
    case False
    from Cons.IH[OF this]
    show ?thesis.
  next
    case True
    with ‹¬ one_call_in_path x (x' # xs)›
    have [simp]: "x' = x" by (auto split: if_splits)

    have "x ∈ set xs"
    proof(rule ccontr)
      assume "x ∉ set xs"
      hence "no_call_in_path x xs" by (metis no_call_in_path_set_conv)
      hence "one_call_in_path x (x # xs)" by simp
      with Cons show False by simp
    qed
    with ‹set xs ⊆ ccNeighbors x' G›
    have "x ∈ ccNeighbors x G" by auto
    thus ?thesis by simp
  qed
qed

context CoCallArityEdom
begin
 lemma carrier_Fexp': "carrier (Texp e⋅a) ⊆ fv e"
    unfolding Texp_simp carrier_ccTTree
    by (rule Aexp_edom)

end


context CoCallAritySafe
begin

lemma carrier_AnalBinds_below:
  "carrier ((Texp.AnalBinds  Δ⋅(Aheap Δ e⋅a)) x) ⊆ edom ((ABinds Δ)⋅(Aheap Δ e⋅a))"
by (auto simp add: Texp.AnalBinds_lookup Texp_def split: option.splits 
         elim!: subsetD[OF edom_mono[OF monofun_cfun_fun[OF ABind_below_ABinds]]])

sublocale TTreeAnalysisCarrier Texp
  apply standard
  unfolding Texp_simp carrier_ccTTree
  apply standard
  done

sublocale TTreeAnalysisSafe Texp
proof
  fix x e a

  from edom_mono[OF Aexp_App]
  have "{x} ∪ edom (Aexp e⋅(inc⋅a)) ⊆ edom (Aexp (App e x)⋅a)" by auto
  moreover
  {
  have "ccApprox (many_calls x ⊗⊗ ccTTree (edom (Aexp e⋅(inc⋅a))) (ccExp e⋅(inc⋅a))) 
    = cc_restr (edom (Aexp e⋅(inc⋅a))) (ccExp e⋅(inc⋅a)) ⊔ ccProd {x} (insert x (edom (Aexp e⋅(inc⋅a))))"
    by (simp add: ccApprox_both ccProd_insert2[where S' = "edom e" for e])
  also
  have "edom (Aexp e⋅(inc⋅a)) ⊆ fv e"
    by (rule Aexp_edom)
  also(below_trans[OF eq_imp_below join_mono[OF below_refl ccProd_mono2[OF insert_mono] ]])
  have "cc_restr (edom (Aexp e⋅(inc⋅a))) (ccExp e⋅(inc⋅a)) ⊑ ccExp e⋅(inc⋅a)"
    by (rule cc_restr_below_arg)
  also
  have "ccExp e⋅(inc⋅a) ⊔ ccProd {x} (insert x (fv e)) ⊑ ccExp (App e x)⋅a" 
    by (rule ccExp_App)
  finally
  have "ccApprox (many_calls x ⊗⊗ ccTTree (edom (Aexp e⋅(inc⋅a))) (ccExp e⋅(inc⋅a))) ⊑ ccExp (App e x)⋅a" by this simp_all
  }
  ultimately
  show "many_calls x ⊗⊗ Texp e⋅(inc⋅a) ⊑ Texp (App e x)⋅a"
    unfolding Texp_simp by (auto intro!: below_ccTTreeI)
next
  fix y e n
  show "without y (Texp e⋅(pred⋅n)) ⊑ Texp (Lam [y]. e)⋅n"
    unfolding Texp_simp
    by (auto dest: subsetD[OF Aexp_edom]
             intro!: below_ccTTreeI  below_trans[OF _ ccExp_Lam] cc_restr_mono1 subsetD[OF edom_mono[OF Aexp_Lam]])
next
  fix e y x a

  from edom_mono[OF Aexp_subst]
  have *: "edom (Aexp e[y::=x]⋅a) ⊆ insert x (edom (Aexp e⋅a) - {y})" by simp

  have "Texp e[y::=x]⋅a = ccTTree (edom (Aexp e[y::=x]⋅a)) (ccExp e[y::=x]⋅a)"
    unfolding Texp_simp..
  also have "… ⊑ ccTTree (insert x (edom (Aexp e⋅a) - {y})) (ccExp e[y::=x]⋅a)"
    by (rule ccTTree_mono1[OF *])
  also have "… ⊑ many_calls x ⊗⊗ without x (…)"
    by (rule paths_many_calls_subset)
  also have "without x (ccTTree (insert x (edom (Aexp e⋅a) - {y})) (ccExp e[y::=x]⋅a))
    = ccTTree (edom (Aexp e⋅a) - {y} - {x}) (ccExp e[y::=x]⋅a)"
    by simp
  also have "… ⊑ ccTTree (edom (Aexp e⋅a) - {y} - {x}) (ccExp e⋅a)"
    by (rule ccTTree_cong_below[OF ccExp_subst]) auto
  also have "… = without y (ccTTree (edom (Aexp e⋅a) - {x}) (ccExp e⋅a))"
    by simp (metis Diff_insert Diff_insert2)
  also have "ccTTree (edom (Aexp e⋅a) - {x}) (ccExp e⋅a) ⊑ ccTTree (edom (Aexp e⋅a)) (ccExp e⋅a)"
    by (rule ccTTree_mono1) auto
  also have "… = Texp e⋅a"
    unfolding Texp_simp..
  finally
  show "Texp e[y::=x]⋅a ⊑ many_calls x ⊗⊗ without y (Texp e⋅a)"
    by this simp_all
next
  fix v a
  have "up⋅a ⊑ (Aexp (Var v)⋅a) v" by (rule Aexp_Var)
  hence "v ∈ edom (Aexp (Var v)⋅a)" by (auto simp add: edom_def)
  thus "single v ⊑ Texp (Var v)⋅a"
    unfolding Texp_simp
    by (auto intro: below_ccTTreeI)
next
  fix scrut e1 a e2
  have "ccTTree (edom (Aexp e1⋅a)) (ccExp e1⋅a) ⊕⊕ ccTTree (edom (Aexp e2⋅a)) (ccExp e2⋅a)
    ⊑ ccTTree (edom (Aexp e1⋅a) ∪ edom (Aexp e2⋅a)) (ccExp e1⋅a ⊔ ccExp e2⋅a)"
      by (rule either_ccTTree)
  note both_mono2'[OF this]
  also
  have "ccTTree (edom (Aexp scrut⋅0)) (ccExp scrut⋅0) ⊗⊗ ccTTree (edom (Aexp e1⋅a) ∪ edom (Aexp e2⋅a)) (ccExp e1⋅a ⊔ ccExp e2⋅a)
    ⊑ ccTTree (edom (Aexp scrut⋅0) ∪ (edom (Aexp e1⋅a) ∪ edom (Aexp e2⋅a))) (ccExp scrut⋅0 ⊔ (ccExp e1⋅a ⊔ ccExp e2⋅a) ⊔ ccProd (edom (Aexp scrut⋅0)) (edom (Aexp e1⋅a) ∪ edom (Aexp e2⋅a)))"
    by (rule interleave_ccTTree)
  also
  have "edom (Aexp scrut⋅0) ∪ (edom (Aexp e1⋅a) ∪ edom (Aexp e2⋅a)) = edom (Aexp scrut⋅0 ⊔ Aexp e1⋅a ⊔ Aexp e2⋅a)" by auto
  also
  have "Aexp scrut⋅0 ⊔ Aexp e1⋅a ⊔ Aexp e2⋅a ⊑ Aexp (scrut ? e1 : e2)⋅a"
    by (rule Aexp_IfThenElse)
  also
  have "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 (rule ccExp_IfThenElse)
  
  show "Texp scrut⋅0 ⊗⊗ (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊑ Texp (scrut ? e1 : e2)⋅a"
    unfolding Texp_simp
    by (auto simp add: ccApprox_both join_below_iff  below_trans[OF _ join_above2]
             intro!: below_ccTTreeI below_trans[OF cc_restr_below_arg]
                     below_trans[OF _ ccExp_IfThenElse]  subsetD[OF edom_mono[OF Aexp_IfThenElse]])
next
  fix e
  assume "isVal e"
  hence [simp]: "ccExp e⋅0 = ccSquare (fv e)" by (rule ccExp_pap)
  thus "repeatable (Texp e⋅0)"
    unfolding Texp_simp by (auto intro: repeatable_ccTTree_ccSquare[OF Aexp_edom])
qed

definition Theap :: "heap ⇒ exp ⇒ Arity → var ttree"
  where "Theap Γ e = (Λ a. if nonrec Γ then ccTTree (edom (Aheap Γ e⋅a)) (ccExp e⋅a) else ttree_restr (edom (Aheap Γ e⋅a)) anything)"

lemma Theap_simp: "Theap Γ e⋅a = (if nonrec Γ then ccTTree (edom (Aheap Γ e⋅a)) (ccExp e⋅a) else ttree_restr (edom (Aheap Γ e⋅a)) anything)"
  unfolding Theap_def by simp

lemma carrier_Fheap':"carrier (Theap Γ e⋅a) = edom (Aheap Γ e⋅a)"
    unfolding Theap_simp carrier_ccTTree by simp

sublocale TTreeAnalysisCardinalityHeap Texp Aexp Aheap Theap
proof
  fix Γ e a
  show "carrier (Theap Γ e⋅a) = edom (Aheap Γ e⋅a)"
    by (rule carrier_Fheap')
next
  fix x Γ p e a
  assume "x ∈ thunks Γ"
  
  assume "¬ one_call_in_path x p"
  hence "x ∈ set p" by (rule more_than_one_setD)
  
  assume "p ∈ paths (Theap Γ e⋅a)" with ‹x ∈ set p›
  have "x ∈ carrier (Theap Γ e⋅a)" by (auto simp add: Union_paths_carrier[symmetric])
  hence "x ∈ edom (Aheap Γ e⋅a)"
    unfolding Theap_simp by (auto split: if_splits)
  
  show "(Aheap Γ e⋅a) x = up⋅0"
  proof(cases "nonrec Γ")
    case False
    from False ‹x ∈ thunks Γ›  ‹x ∈ edom (Aheap Γ e⋅a)›
    show ?thesis  by (rule aHeap_thunks_rec)
  next
    case True
    with ‹p ∈ paths (Theap Γ e⋅a)›
    have "p ∈ valid_lists (edom (Aheap Γ e⋅a)) (ccExp e⋅a)" by (simp add: Theap_simp)

    with ‹¬ one_call_in_path x p›
    have "x--x∈ (ccExp e⋅a)" by (rule valid_lists_many_calls)
  
    from True ‹x ∈ thunks Γ› this
    show ?thesis by (rule aHeap_thunks_nonrec)
  qed
next
  fix Δ e a

  have carrier: "carrier (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊆ edom (Aheap Δ e⋅a) ∪ edom (Aexp (Let Δ e)⋅a)"
  proof(rule carrier_substitute_below)
    from edom_mono[OF Aexp_Let[of Δ e a]]
    show "carrier (Texp e⋅a) ⊆ edom (Aheap Δ e⋅a) ∪ edom (Aexp (Let Δ e)⋅a)"  by (simp add: Texp_def)
  next
    fix x
    assume "x ∈ edom (Aheap Δ e⋅a) ∪ edom (Aexp (Let Δ e)⋅a)"
    hence "x ∈ edom (Aheap Δ e⋅a) ∨ x : (edom (Aexp (Let Δ e)⋅a))" by simp
    thus "carrier ((Texp.AnalBinds  Δ⋅(Aheap Δ e⋅a)) x) ⊆ edom (Aheap Δ e⋅a) ∪ edom (Aexp (Let Δ e)⋅a)"
    proof
      assume "x ∈ edom (Aheap Δ e⋅a)"
      
      have "carrier ((Texp.AnalBinds  Δ⋅(Aheap Δ e⋅a)) x) ⊆ edom (ABinds Δ⋅(Aheap Δ e⋅a))"
        by (rule carrier_AnalBinds_below)
      also have "… ⊆ edom (Aheap Δ e⋅a ⊔ Aexp (Terms.Let Δ e)⋅a)"
        using edom_mono[OF Aexp_Let[of Δ e a]] by simp
      finally show ?thesis by simp
    next
      assume "x ∈ edom (Aexp (Terms.Let Δ e)⋅a)"
      hence "x ∉ domA Δ" by (auto  dest: subsetD[OF Aexp_edom])
      hence "(Texp.AnalBinds  Δ⋅(Aheap Δ e⋅a)) x = ⊥"
        by (rule Texp.AnalBinds_not_there)
      thus ?thesis by simp
    qed
  qed

  show "ttree_restr (- domA Δ) (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊑ Texp (Let Δ e)⋅a"
  proof (rule below_trans[OF _ eq_imp_below[OF Texp_simp[symmetric]]], rule below_ccTTreeI)
    have "carrier (ttree_restr (- domA Δ) (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)))
       = carrier (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) - domA Δ" by auto
    also note carrier
    also have "edom (Aheap Δ e⋅a) ∪ edom (Aexp (Terms.Let Δ e)⋅a) - domA Δ = edom (Aexp (Let Δ e)⋅a)"
      by (auto dest: subsetD[OF edom_Aheap] subsetD[OF Aexp_edom])
    finally
    show "carrier (ttree_restr (- domA Δ) (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ)(Texp e⋅a)))
          ⊆ edom (Aexp (Terms.Let Δ e)⋅a)" by this auto
  next
    let ?x = "ccApprox (ttree_restr (- domA Δ) (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)))"
  
    have "?x = cc_restr (- domA Δ) ?x"  by simp
    also have "… ⊑ cc_restr (- domA Δ) (ccHeap Δ e⋅a)"
    proof(rule cc_restr_mono2[OF wild_recursion_thunked])
      have "ccExp e⋅a ⊑ ccHeap Δ e⋅a" by (rule ccHeap_Exp)
      thus "ccApprox (Texp e⋅a) ⊑ ccHeap Δ e⋅a"
        by (auto simp add: Texp_simp intro: below_trans[OF cc_restr_below_arg])
    next
      fix x
      assume "x ∉ domA Δ"
      thus "(Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) x = empty"
        by (metis Texp.AnalBinds_not_there empty_is_bottom)
    next
      fix x
      assume "x ∈ domA Δ"
      then obtain e' where e': "map_of Δ x = Some e'" by (metis domA_map_of_Some_the)
      
      show "ccApprox ((Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) x) ⊑ ccHeap Δ e⋅a"
      proof(cases "(Aheap Δ e⋅a) x")
        case bottom thus ?thesis using e' by (simp add: Texp.AnalBinds_lookup)
      next
        case (up a')
        with e'
        have "ccExp e'⋅a' ⊑ ccHeap Δ e⋅a" by (rule ccHeap_Heap)
        thus ?thesis using up e'
          by (auto simp add: Texp.AnalBinds_lookup Texp_simp  intro: below_trans[OF cc_restr_below_arg])
      qed

      show "ccProd (ccNeighbors x (ccHeap Δ e⋅a)- {x} ∩ thunks Δ) (carrier ((Texp.AnalBinds  Δ⋅(Aheap Δ e⋅a)) x)) ⊑ ccHeap Δ e⋅a"
      proof(cases "(Aheap Δ e⋅a) x")
        case bottom thus ?thesis using e' by (simp add: Texp.AnalBinds_lookup)
      next
        case (up a')
        have subset: "(carrier (fup⋅(Texp e')⋅((Aheap Δ e⋅a) x))) ⊆ fv e'"
          using up e' by (auto simp add: Texp.AnalBinds_lookup carrier_Fexp dest!: subsetD[OF Aexp_edom])
        
        from e' up
        have "ccProd (fv e') (ccNeighbors x (ccHeap Δ e⋅a) - {x} ∩ thunks Δ) ⊑ ccHeap Δ e⋅a"
          by (rule ccHeap_Extra_Edges)
        then
        show ?thesis using e'
          by (simp add: Texp.AnalBinds_lookup  Texp_simp ccProd_comm  below_trans[OF ccProd_mono2[OF subset]])
      qed
    qed
    also have "… ⊑ ccExp (Let Δ e)⋅a"
      by (rule ccExp_Let)
    finally
    show "ccApprox (ttree_restr (- domA Δ) (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)))
        ⊑ ccExp (Terms.Let Δ e)⋅a" by this simp_all
  qed

  note carrier
  hence "carrier (substitute (ExpAnalysis.AnalBinds Texp Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊆ edom (Aheap Δ e⋅a) ∪ - domA Δ"
    by (rule order_trans) (auto dest: subsetD[OF Aexp_edom])
  hence "ttree_restr (domA Δ)            (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a))
      = ttree_restr (edom (Aheap Δ e⋅a)) (ttree_restr (domA Δ) (substitute (Texp.AnalBinds  Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)))"
    by -(rule ttree_restr_noop[symmetric], auto)
  also
  have "… = ttree_restr (edom (Aheap Δ e⋅a)) (substitute (Texp.AnalBinds  Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a))"
    by (simp add: inf.absorb2[OF edom_Aheap ])
  also
  have "… ⊑ Theap Δ e ⋅a"
  proof(cases "nonrec Δ")
    case False
    have "ttree_restr (edom (Aheap Δ e⋅a)) (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a))
      ⊑ ttree_restr (edom (Aheap Δ e⋅a)) anything"
      by (rule ttree_restr_mono) simp
    also have "… = Theap Δ e⋅a"
      by (simp add: Theap_simp False)
    finally show ?thesis.
  next
    case [simp]: True

    from True
    have "ttree_restr (edom (Aheap Δ e⋅a)) (substitute (Texp.AnalBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a))
       = ttree_restr (edom (Aheap Δ e⋅a)) (Texp e⋅a)"
      by (rule nonrecE) (rule ttree_rest_substitute, auto simp add: carrier_Fexp fv_def fresh_def dest!: subsetD[OF edom_Aheap] subsetD[OF Aexp_edom])
    also have "… = ccTTree (edom (Aexp e⋅a) ∩ edom (Aheap Δ e⋅a)) (ccExp e⋅a)"
      by (simp add: Texp_simp)
    also have "… ⊑ ccTTree (edom (Aexp e⋅a) ∩ domA Δ) (ccExp e⋅a)"
      by (rule ccTTree_mono1[OF Int_mono[OF order_refl edom_Aheap]])
    also have "… ⊑ ccTTree (edom (Aheap Δ e⋅a)) (ccExp e⋅a)"
      by (rule ccTTree_mono1[OF edom_mono[OF Aheap_nonrec[OF True], simplified]])
    also have "… ⊑ Theap Δ e⋅a"
      by (simp add: Theap_simp)
    finally
    show ?thesis by this simp_all
  qed
  finally
  show "ttree_restr (domA Δ) (substitute (ExpAnalysis.AnalBinds Texp Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊑ Theap Δ e⋅a".

qed
end

(* TODO: Unused stuff from here, mostly about singles. Might be useful later. *)


lemma paths_singles: "xs ∈ paths (singles S) ⟷ (∀x ∈ S. one_call_in_path x xs)"
  by transfer (auto simp add: one_call_in_path_filter_conv)

lemma paths_singles': "xs ∈ paths (singles S) ⟷ (∀x ∈ (set xs ∩ S). one_call_in_path x xs)"
  apply transfer
  apply (auto simp add: one_call_in_path_filter_conv)
  apply (erule_tac x = x in ballE)
  apply auto
  by (metis (poly_guards_query) filter_empty_conv le0 length_0_conv)

lemma both_below_singles1:
  assumes "t ⊑ singles S"
  assumes "carrier t' ∩ S = {}"
  shows "t ⊗⊗ t' ⊑ singles S"
proof (rule ttree_belowI)
  fix xs
  assume "xs ∈ paths (t ⊗⊗ t')"
  then obtain ys zs where "ys ∈ paths t" and "zs ∈ paths t'" and "xs ∈ ys ⊗ zs" by (auto simp add: paths_both)
  with assms 
  have "ys ∈ paths (singles S)" and "set zs ∩ S = {}"
    by (metis below_ttree.rep_eq contra_subsetD paths.rep_eq, auto simp add: Union_paths_carrier[symmetric])
  with ‹xs ∈ ys ⊗ zs›
  show "xs ∈ paths (singles S)"
    by (induction) (auto simp add: paths_singles no_call_in_path_set_conv interleave_set dest: more_than_one_setD split: if_splits)
qed


lemma paths_ttree_restr_singles: "xs ∈ paths (ttree_restr S' (singles S)) ⟷ set xs ⊆ S' ∧ (∀x ∈ S. one_call_in_path x xs)"
proof
  show "xs ∈ paths (ttree_restr S' (singles S)) ⟹  set xs ⊆ S' ∧ (∀x ∈ S. one_call_in_path x xs)"
    by (auto simp add: filter_paths_conv_free_restr[symmetric] paths_singles)
next
  assume *: "set xs ⊆ S' ∧ (∀x∈S. one_call_in_path x xs)"
  hence "set xs ⊆ S'" by auto
  hence [simp]: "filter (λ x'. x' ∈ S') xs = xs" by (auto simp add: filter_id_conv)
  
  from *
  have "xs ∈ paths (singles S)"
     by (auto simp add: paths_singles')
  hence "filter (λ x'. x' ∈ S') xs ∈ filter (λx'. x' ∈ S') ` paths (singles S)"
    by (rule imageI)
  thus "xs ∈ paths (ttree_restr S' (singles S))"
    by (auto simp add: filter_paths_conv_free_restr[symmetric] )
qed



(* TODO: unused *)
lemma substitute_not_carrier:
  assumes "x ∉ carrier t"
  assumes "⋀ x'. x ∉ carrier (f x')"
  shows "x ∉  carrier (substitute f T t)"
proof-
  have "ttree_restr ({x}) (substitute f T t) = ttree_restr ({x}) t"
  proof(rule ttree_rest_substitute)
    fix x'
    from ‹x ∉ carrier (f x')›
    show "carrier (f x') ∩ {x} = {}" by auto
  qed
  hence "x ∉ carrier (ttree_restr ({x}) (substitute f T t)) ⟷ x ∉ carrier (ttree_restr ({x}) t)" by metis
  with assms(1)
  show ?thesis by simp
qed

(* TODO: unused *)
lemma substitute_below_singlesI:
  assumes "t ⊑ singles S"
  assumes "⋀ x. carrier (f x) ∩ S = {}"
  shows "substitute f T t ⊑ singles S"
proof(rule ttree_belowI)
  fix xs
  assume "xs ∈ paths (substitute f T t)"
  thus "xs ∈ paths (singles S)"
  using assms
  proof(induction f T t xs arbitrary: S rule: substitute_induct)
    case Nil
    thus ?case by simp
  next
    case (Cons f T t x xs)

    from ‹x#xs ∈ _›
    have xs: "xs ∈ paths (substitute (f_nxt f T x) T (nxt t x ⊗⊗ f x))" by auto
    moreover

    from ‹t ⊑ singles S›
    have "nxt t x ⊑ singles S" 
      by (metis "TTree-HOLCF.nxt_mono" below_trans nxt_singles_below_singles)
    from this ‹carrier (f x) ∩ S = {}›
    have "nxt t x ⊗⊗ f x ⊑ singles S"
      by (rule both_below_singles1)
    moreover
    { fix x'
      from  ‹carrier (f x') ∩ S = {}›
      have "carrier (f_nxt f T x x') ∩ S = {}"
        by (auto simp add: f_nxt_def)
    }
    ultimately
    have IH: "xs ∈ paths (singles S)"
      by (rule Cons.IH) 
  
  show ?case
    proof(cases "x ∈ S")
      case True
      with ‹carrier (f x) ∩ S = {}›
      have "x ∉ carrier (f x)" by auto
      moreover
      from ‹t ⊑ singles S›
      have "nxt t x ⊑ nxt (singles S) x" by (rule nxt_mono)
      hence "carrier (nxt t x) ⊆ carrier (nxt (singles S) x)" by (rule carrier_mono)
      from subsetD[OF this] True
      have "x ∉ carrier (nxt t x)" by auto
      ultimately
      have "x ∉ carrier (nxt t x ⊗⊗ f x)" by simp
      hence "x ∉ carrier (substitute (f_nxt f T x) T (nxt t x ⊗⊗ f x))"
      proof(rule substitute_not_carrier)
        fix x'  
        from ‹carrier (f x') ∩ S = {}› ‹x ∈ S›
        show "x ∉ carrier (f_nxt f T x x')" by (auto simp add: f_nxt_def)
      qed
      with xs
      have "x ∉ set xs" by (auto simp add: Union_paths_carrier[symmetric])
      with IH
      have "xs ∈ paths (without x (singles S))" by (rule paths_withoutI)
      thus ?thesis using True by (simp add: Cons_path)
    next
      case False
      with IH
      show ?thesis by (simp add: Cons_path)
    qed
  qed
qed

end