theory CoCallImplTTreeSafe
imports CoCallImplTTree CoCallAnalysisSpec TTreeAnalysisSpec
begin
hide_const Multiset.single
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!: set_mp[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: set_mp[OF Aexp_edom]
intro!: below_ccTTreeI below_trans[OF _ ccExp_Lam] cc_restr_mono1 set_mp[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] set_mp[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: set_mp[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: set_mp[OF edom_Aheap] set_mp[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!: set_mp[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: set_mp[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!: set_mp[OF edom_Aheap] set_mp[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
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
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
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 set_mp[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