Theory Stateful_Typing
section ‹Extending the Typing Result to Stateful Constraints›
theory Stateful_Typing
imports Typing_Result Stateful_Strands
begin
text ‹\label{sec:Stateful-Typing}Locale setup›
locale stateful_typed_model = typed_model arity public Ana Γ
for arity::"'fun ⇒ nat"
and public::"'fun ⇒ bool"
and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
+
fixes Pair::"'fun"
assumes Pair_arity: "arity Pair = 2"
and Ana_subst': "⋀f T δ K M. Ana (Fun f T) = (K,M) ⟹ Ana (Fun f T ⋅ δ) = (K ⋅⇩l⇩i⇩s⇩t δ,M ⋅⇩l⇩i⇩s⇩t δ)"
begin
lemma Ana_invar_subst'[simp]: "Ana_invar_subst 𝒮"
using Ana_subst' unfolding Ana_invar_subst_def by force
definition pair where
"pair d ≡ case d of (t,t') ⇒ Fun Pair [t,t']"
fun tr⇩p⇩a⇩i⇩r⇩s::
"(('fun,'var) term × ('fun,'var) term) list ⇒
('fun,'var) dbstatelist ⇒
(('fun,'var) term × ('fun,'var) term) list list"
where
"tr⇩p⇩a⇩i⇩r⇩s [] D = [[]]"
| "tr⇩p⇩a⇩i⇩r⇩s ((s,t)#F) D =
concat (map (λd. map ((#) (pair (s,t), pair d)) (tr⇩p⇩a⇩i⇩r⇩s F D)) D)"
text ‹
A translation/reduction ‹tr› from stateful constraints to (lists of) "non-stateful" constraints.
The output represents a finite disjunction of constraints whose models constitute exactly the
models of the input constraint. The typing result for "non-stateful" constraints is later lifted
to the stateful setting through this reduction procedure.
›
fun tr::"('fun,'var) stateful_strand ⇒ ('fun,'var) dbstatelist ⇒ ('fun,'var) strand list"
where
"tr [] D = [[]]"
| "tr (send⟨ts⟩#A) D = map ((#) (send⟨ts⟩⇩s⇩t)) (tr A D)"
| "tr (receive⟨ts⟩#A) D = map ((#) (receive⟨ts⟩⇩s⇩t)) (tr A D)"
| "tr (⟨ac: t ≐ t'⟩#A) D = map ((#) (⟨ac: t ≐ t'⟩⇩s⇩t)) (tr A D)"
| "tr (insert⟨t,s⟩#A) D = tr A (List.insert (t,s) D)"
| "tr (delete⟨t,s⟩#A) D =
concat (map (λDi. map (λB. (map (λd. ⟨check: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t) Di)@
(map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩⇩s⇩t) [d←D. d ∉ set Di])@B)
(tr A [d←D. d ∉ set Di]))
(subseqs D))"
| "tr (⟨ac: t ∈ s⟩#A) D =
concat (map (λB. map (λd. ⟨ac: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t#B) D) (tr A D))"
| "tr (∀X⟨∨≠: F ∨∉: F'⟩#A) D =
map ((@) (map (λG. ∀X⟨∨≠: (F@G)⟩⇩s⇩t) (tr⇩p⇩a⇩i⇩r⇩s F' D))) (tr A D)"
text ‹Type-flaw resistance of stateful constraint steps›
fun tfr⇩s⇩s⇩t⇩p where
"tfr⇩s⇩s⇩t⇩p (Equality _ t t') = ((∃δ. Unifier δ t t') ⟶ Γ t = Γ t')"
| "tfr⇩s⇩s⇩t⇩p (NegChecks X F F') = (
(F' = [] ∧ (∀x ∈ fv⇩p⇩a⇩i⇩r⇩s F-set X. ∃a. Γ (Var x) = TAtom a)) ∨
(∀f T. Fun f T ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F ∪ pair ` set F') ⟶
T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X)))"
| "tfr⇩s⇩s⇩t⇩p _ = True"
text ‹Type-flaw resistance of stateful constraints›
definition tfr⇩s⇩s⇩t where "tfr⇩s⇩s⇩t S ≡ tfr⇩s⇩e⇩t (trms⇩s⇩s⇩t S ∪ pair ` setops⇩s⇩s⇩t S) ∧ list_all tfr⇩s⇩s⇩t⇩p S"
subsection ‹Minor Lemmata›
lemma pair_in_pair_image_iff:
"pair (s,t) ∈ pair ` P ⟷ (s,t) ∈ P"
unfolding pair_def by fast
lemma subst_apply_pairs_pair_image_subst:
"pair ` set (F ⋅⇩p⇩a⇩i⇩r⇩s θ) = pair ` set F ⋅⇩s⇩e⇩t θ"
unfolding subst_apply_pairs_def pair_def by (induct F) auto
lemma Ana_subst_subterms_cases:
fixes θ::"('fun,'var) subst"
assumes t: "t ⊑⇩s⇩e⇩t M ⋅⇩s⇩e⇩t θ"
and s: "s ∈ set (snd (Ana t))"
shows "(∃u ∈ subterms⇩s⇩e⇩t M. t = u ⋅ θ ∧ s ∈ set (snd (Ana u)) ⋅⇩s⇩e⇩t θ) ∨ (∃x ∈ fv⇩s⇩e⇩t M. t ⊑ θ x)"
proof (cases "t ∈ subterms⇩s⇩e⇩t M ⋅⇩s⇩e⇩t θ")
case True
then obtain u where u: "u ∈ subterms⇩s⇩e⇩t M" "t = u ⋅ θ" by blast
show ?thesis
proof (cases u)
case (Var x)
hence "x ∈ fv⇩s⇩e⇩t M" using fv_subset_subterms[OF u(1)] by simp
thus ?thesis using u(2) Var by fastforce
next
case (Fun f T)
hence "set (snd (Ana t)) = set (snd (Ana u)) ⋅⇩s⇩e⇩t θ"
using Ana_subst'[of f T _ _ θ] u(2) by (cases "Ana u") auto
thus ?thesis using s u by blast
qed
qed (use s t subterms⇩s⇩e⇩t_subst in blast)
lemma Ana_snd_subst_nth_inv:
fixes θ::"('fun,'var) subst" and f ts
defines "R ≡ snd (Ana (Fun f ts ⋅ θ))"
assumes r: "r = R ! i" "i < length R"
shows "r = snd (Ana (Fun f ts)) ! i ⋅ θ"
proof -
obtain K R where "Ana (Fun f ts) = (K,R)" by (metis surj_pair)
thus ?thesis using Ana_subst'[of f ts K R θ] r unfolding R_def by auto
qed
lemma Ana_snd_subst_inv:
fixes θ::"('fun,'var) subst"
assumes r: "r ∈ set (snd (Ana (Fun f ts ⋅ θ)))"
shows "∃t ∈ set (snd (Ana (Fun f ts))). r = t ⋅ θ"
proof -
obtain K R where "Ana (Fun f ts) = (K,R)" by (metis surj_pair)
thus ?thesis using Ana_subst'[of f ts K R θ] r by auto
qed
lemma fun_pair_eq[dest]: "pair d = pair d' ⟹ d = d'"
proof -
obtain t s t' s' where "d = (t,s)" "d' = (t',s')" by atomize_elim auto
thus "pair d = pair d' ⟹ d = d'" unfolding pair_def by simp
qed
lemma fun_pair_subst: "pair d ⋅ δ = pair (d ⋅⇩p δ)"
using surj_pair[of d] unfolding pair_def by force
lemma fun_pair_subst_set: "pair ` M ⋅⇩s⇩e⇩t δ = pair ` (M ⋅⇩p⇩s⇩e⇩t δ)"
proof
show "pair ` M ⋅⇩s⇩e⇩t δ ⊆ pair ` (M ⋅⇩p⇩s⇩e⇩t δ)"
using fun_pair_subst[of _ δ] by fastforce
show "pair ` (M ⋅⇩p⇩s⇩e⇩t δ) ⊆ pair ` M ⋅⇩s⇩e⇩t δ"
proof
fix t assume t: "t ∈ pair ` (M ⋅⇩p⇩s⇩e⇩t δ)"
then obtain p where p: "p ∈ M" "t = pair (p ⋅⇩p δ)" by blast
thus "t ∈ pair ` M ⋅⇩s⇩e⇩t δ" using fun_pair_subst[of p δ] by force
qed
qed
lemma fun_pair_eq_subst: "pair d ⋅ δ = pair d' ⋅ θ ⟷ d ⋅⇩p δ = d' ⋅⇩p θ"
by (metis fun_pair_subst fun_pair_eq[of "d ⋅⇩p δ" "d' ⋅⇩p θ"])
lemma setops⇩s⇩s⇩t_pair_image_cons[simp]:
"pair ` setops⇩s⇩s⇩t (x#S) = pair ` setops⇩s⇩s⇩t⇩p x ∪ pair ` setops⇩s⇩s⇩t S"
"pair ` setops⇩s⇩s⇩t (send⟨ts⟩#S) = pair ` setops⇩s⇩s⇩t S"
"pair ` setops⇩s⇩s⇩t (receive⟨ts⟩#S) = pair ` setops⇩s⇩s⇩t S"
"pair ` setops⇩s⇩s⇩t (⟨ac: t ≐ t'⟩#S) = pair ` setops⇩s⇩s⇩t S"
"pair ` setops⇩s⇩s⇩t (insert⟨t,s⟩#S) = {pair (t,s)} ∪ pair ` setops⇩s⇩s⇩t S"
"pair ` setops⇩s⇩s⇩t (delete⟨t,s⟩#S) = {pair (t,s)} ∪ pair ` setops⇩s⇩s⇩t S"
"pair ` setops⇩s⇩s⇩t (⟨ac: t ∈ s⟩#S) = {pair (t,s)} ∪ pair ` setops⇩s⇩s⇩t S"
"pair ` setops⇩s⇩s⇩t (∀X⟨∨≠: F ∨∉: G⟩#S) = pair ` set G ∪ pair ` setops⇩s⇩s⇩t S"
unfolding setops⇩s⇩s⇩t_def by auto
lemma setops⇩s⇩s⇩t_pair_image_subst_cons[simp]:
"pair ` setops⇩s⇩s⇩t (x#S ⋅⇩s⇩s⇩t θ) = pair ` setops⇩s⇩s⇩t⇩p (x ⋅⇩s⇩s⇩t⇩p θ) ∪ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
"pair ` setops⇩s⇩s⇩t (send⟨ts⟩#S ⋅⇩s⇩s⇩t θ) = pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
"pair ` setops⇩s⇩s⇩t (receive⟨ts⟩#S ⋅⇩s⇩s⇩t θ) = pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
"pair ` setops⇩s⇩s⇩t (⟨ac: t ≐ t'⟩#S ⋅⇩s⇩s⇩t θ) = pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
"pair ` setops⇩s⇩s⇩t (insert⟨t,s⟩#S ⋅⇩s⇩s⇩t θ) = {pair (t,s) ⋅ θ} ∪ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
"pair ` setops⇩s⇩s⇩t (delete⟨t,s⟩#S ⋅⇩s⇩s⇩t θ) = {pair (t,s) ⋅ θ} ∪ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
"pair ` setops⇩s⇩s⇩t (⟨ac: t ∈ s⟩#S ⋅⇩s⇩s⇩t θ) = {pair (t,s) ⋅ θ} ∪ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
"pair ` setops⇩s⇩s⇩t (∀X⟨∨≠: F ∨∉: G⟩#S ⋅⇩s⇩s⇩t θ) =
pair ` set (G ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) θ) ∪ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
using subst_sst_cons[of _ S θ] unfolding setops⇩s⇩s⇩t_def pair_def by auto
lemma setops⇩s⇩s⇩t_are_pairs: "t ∈ pair ` setops⇩s⇩s⇩t A ⟹ ∃s s'. t = pair (s,s')"
proof (induction A)
case (Cons a A) thus ?case
by (cases a) (auto simp add: setops⇩s⇩s⇩t_def)
qed (simp add: setops⇩s⇩s⇩t_def)
lemma fun_pair_wf⇩t⇩r⇩m: "wf⇩t⇩r⇩m t ⟹ wf⇩t⇩r⇩m t' ⟹ wf⇩t⇩r⇩m (pair (t,t'))"
using Pair_arity unfolding wf⇩t⇩r⇩m_def pair_def by auto
lemma wf⇩t⇩r⇩m⇩s_pairs: "wf⇩t⇩r⇩m⇩s (trms⇩p⇩a⇩i⇩r⇩s F) ⟹ wf⇩t⇩r⇩m⇩s (pair ` set F)"
using fun_pair_wf⇩t⇩r⇩m by blast
lemma wf_fun_pair_ineqs_map:
assumes "wf⇩s⇩t X A"
shows "wf⇩s⇩t X (map (λd. ∀Y⟨∨≠: [(pair (t, s), pair d)]⟩⇩s⇩t) D@A)"
using assms by (induct D) auto
lemma wf_fun_pair_negchecks_map:
assumes "wf⇩s⇩t X A"
shows "wf⇩s⇩t X (map (λG. ∀Y⟨∨≠: (F@G)⟩⇩s⇩t) M@A)"
using assms by (induct M) auto
lemma wf_fun_pair_eqs_ineqs_map:
fixes A::"('fun,'var) strand"
assumes "wf⇩s⇩t X A" "Di ∈ set (subseqs D)" "∀(t,t') ∈ set D. fv t ∪ fv t' ⊆ X"
shows "wf⇩s⇩t X ((map (λd. ⟨check: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t) Di)@
(map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩⇩s⇩t) [d←D. d ∉ set Di])@A)"
proof -
let ?c1 = "map (λd. ⟨check: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t) Di"
let ?c2 = "map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩⇩s⇩t) [d←D. d ∉ set Di]"
have 1: "wf⇩s⇩t X (?c2@A)" using wf_fun_pair_ineqs_map[OF assms(1)] by simp
have 2: "∀(t,t') ∈ set Di. fv t ∪ fv t' ⊆ X"
using assms(2,3) by (meson contra_subsetD subseqs_set_subset(1))
have "wf⇩s⇩t X (?c1@B)" when "wf⇩s⇩t X B" for B::"('fun,'var) strand"
using 2 that by (induct Di) auto
thus ?thesis using 1 by simp
qed
lemma trms⇩s⇩s⇩t_wt_subst_ex:
assumes θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
and t: "t ∈ trms⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
shows "∃s δ. s ∈ trms⇩s⇩s⇩t S ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t = s ⋅ δ"
using t
proof (induction S)
case (Cons s S) thus ?case
proof (cases "t ∈ trms⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)")
case False
hence "t ∈ trms⇩s⇩s⇩t⇩p (s ⋅⇩s⇩s⇩t⇩p θ)"
using Cons.prems trms⇩s⇩s⇩t_subst_cons[of s S θ]
by auto
then obtain u where u: "u ∈ trms⇩s⇩s⇩t⇩p s" "t = u ⋅ rm_vars (set (bvars⇩s⇩s⇩t⇩p s)) θ"
using trms⇩s⇩s⇩t⇩p_subst'' by blast
thus ?thesis
using trms⇩s⇩s⇩t_subst_cons[of s S θ]
wt_subst_rm_vars[OF θ(1), of "set (bvars⇩s⇩s⇩t⇩p s)"]
wf_trms_subst_rm_vars'[OF θ(2), of "set (bvars⇩s⇩s⇩t⇩p s)"]
by fastforce
qed auto
qed simp
lemma setops⇩s⇩s⇩t_wt_subst_ex:
assumes θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
and t: "t ∈ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
shows "∃s δ. s ∈ pair ` setops⇩s⇩s⇩t S ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t = s ⋅ δ"
using t
proof (induction S)
case (Cons x S) thus ?case
proof (cases x)
case (Insert t' s)
hence "t = pair (t',s) ⋅ θ ∨ t ∈ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
using Cons.prems subst_sst_cons[of _ S θ]
unfolding pair_def by (force simp add: setops⇩s⇩s⇩t_def)
thus ?thesis
using Insert Cons.IH θ by (cases "t = pair (t', s) ⋅ θ") (fastforce, auto)
next
case (Delete t' s)
hence "t = pair (t',s) ⋅ θ ∨ t ∈ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
using Cons.prems subst_sst_cons[of _ S θ]
unfolding pair_def by (force simp add: setops⇩s⇩s⇩t_def)
thus ?thesis
using Delete Cons.IH θ by (cases "t = pair (t', s) ⋅ θ") (fastforce, auto)
next
case (InSet ac t' s)
hence "t = pair (t',s) ⋅ θ ∨ t ∈ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
using Cons.prems subst_sst_cons[of _ S θ]
unfolding pair_def by (force simp add: setops⇩s⇩s⇩t_def)
thus ?thesis
using InSet Cons.IH θ by (cases "t = pair (t', s) ⋅ θ") (fastforce, auto)
next
case (NegChecks X F F')
hence "t ∈ pair ` set (F' ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) θ) ∨ t ∈ pair ` setops⇩s⇩s⇩t (S ⋅⇩s⇩s⇩t θ)"
using Cons.prems subst_sst_cons[of _ S θ]
unfolding pair_def by (force simp add: setops⇩s⇩s⇩t_def)
thus ?thesis
proof
assume "t ∈ pair ` set (F' ⋅⇩p⇩a⇩i⇩r⇩s rm_vars (set X) θ)"
then obtain s where s: "t = s ⋅ rm_vars (set X) θ" "s ∈ pair ` set F'"
using subst_apply_pairs_pair_image_subst[of F' "rm_vars (set X) θ"] by auto
thus ?thesis
using NegChecks setops⇩s⇩s⇩t_pair_image_cons(8)[of X F F' S]
wt_subst_rm_vars[OF θ(1), of "set X"]
wf_trms_subst_rm_vars'[OF θ(2), of "set X"]
by fast
qed (use Cons.IH in auto)
qed (auto simp add: setops⇩s⇩s⇩t_def subst_sst_cons[of _ S θ])
qed (simp add: setops⇩s⇩s⇩t_def)
lemma setops⇩s⇩s⇩t_wf⇩t⇩r⇩m⇩s:
"wf⇩t⇩r⇩m⇩s (trms⇩s⇩s⇩t A) ⟹ wf⇩t⇩r⇩m⇩s (pair ` setops⇩s⇩s⇩t A)"
"wf⇩t⇩r⇩m⇩s (trms⇩s⇩s⇩t A) ⟹ wf⇩t⇩r⇩m⇩s (trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A)"
proof -
show "wf⇩t⇩r⇩m⇩s (trms⇩s⇩s⇩t A) ⟹ wf⇩t⇩r⇩m⇩s (pair ` setops⇩s⇩s⇩t A)"
proof (induction A)
case (Cons a A)
hence 0: "wf⇩t⇩r⇩m⇩s (trms⇩s⇩s⇩t⇩p a)" "wf⇩t⇩r⇩m⇩s (pair ` setops⇩s⇩s⇩t A)" by auto
thus ?case
proof (cases a)
case (NegChecks X F F')
hence "wf⇩t⇩r⇩m⇩s (trms⇩p⇩a⇩i⇩r⇩s F')" using 0 by simp
thus ?thesis using NegChecks wf⇩t⇩r⇩m⇩s_pairs[of F'] 0 by (auto simp add: setops⇩s⇩s⇩t_def)
qed (auto simp add: setops⇩s⇩s⇩t_def dest: fun_pair_wf⇩t⇩r⇩m)
qed (auto simp add: setops⇩s⇩s⇩t_def)
thus "wf⇩t⇩r⇩m⇩s (trms⇩s⇩s⇩t A) ⟹ wf⇩t⇩r⇩m⇩s (trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A)" by fast
qed
lemma SMP_MP_split:
assumes "t ∈ SMP M"
and M: "∀m ∈ M. is_Fun m"
shows "(∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t ∈ M ⋅⇩s⇩e⇩t δ) ∨
t ∈ SMP ((subterms⇩s⇩e⇩t M ∪ ⋃((set ∘ fst ∘ Ana) ` M)) - M)"
(is "?P t ∨ ?Q t")
using assms(1)
proof (induction t rule: SMP.induct)
case (MP t)
have "wt⇩s⇩u⇩b⇩s⇩t Var" "wf⇩t⇩r⇩m⇩s (subst_range Var)" "M ⋅⇩s⇩e⇩t Var = M" by simp_all
thus ?case using MP by metis
next
case (Subterm t t')
show ?case using Subterm.IH
proof
assume "?P t"
then obtain s δ where s: "s ∈ M" "t = s ⋅ δ" and δ: "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (subst_range δ)" by auto
then obtain f T where fT: "s = Fun f T" using M by fast
have "(∃s'. s' ⊑ s ∧ t' = s' ⋅ δ) ∨ (∃x ∈ fv s. t' ⊏ δ x)"
using subterm_subst_unfold[OF Subterm.hyps(2)[unfolded s(2)]] by blast
thus ?thesis
proof
assume "∃s'. s' ⊑ s ∧ t' = s' ⋅ δ"
then obtain s' where s': "s' ⊑ s" "t' = s' ⋅ δ" by fast
show ?thesis
proof (cases "s' ∈ M")
case True thus ?thesis using s' δ by blast
next
case False
hence "s' ∈ (subterms⇩s⇩e⇩t M ∪ ⋃((set ∘ fst ∘ Ana) ` M)) - M" using s'(1) s(1) by force
thus ?thesis using SMP.Substitution[OF SMP.MP[of s'] δ] s' by presburger
qed
next
assume "∃x ∈ fv s. t' ⊏ δ x"
then obtain x where x: "x ∈ fv s" "t' ⊏ δ x" by fast
have "Var x ∉ M" using M by blast
hence "Var x ∈ (subterms⇩s⇩e⇩t M ∪ ⋃((set ∘ fst ∘ Ana) ` M)) - M"
using s(1) var_is_subterm[OF x(1)] by blast
hence "δ x ∈ SMP ((subterms⇩s⇩e⇩t M ∪ ⋃((set ∘ fst ∘ Ana) ` M)) - M)"
using SMP.Substitution[OF SMP.MP[of "Var x"] δ] by auto
thus ?thesis using SMP.Subterm x(2) by presburger
qed
qed (metis SMP.Subterm[OF _ Subterm.hyps(2)])
next
case (Substitution t δ)
show ?case using Substitution.IH
proof
assume "?P t"
then obtain θ where "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "t ∈ M ⋅⇩s⇩e⇩t θ" by fast
hence "wt⇩s⇩u⇩b⇩s⇩t (θ ∘⇩s δ)" "wf⇩t⇩r⇩m⇩s (subst_range (θ ∘⇩s δ))" "t ⋅ δ ∈ M ⋅⇩s⇩e⇩t (θ ∘⇩s δ)"
using wt_subst_compose[of θ, OF _ Substitution.hyps(2)]
wf_trm_subst_compose[of θ _ δ, OF _ wf_trm_subst_rangeD[OF Substitution.hyps(3)]]
wf_trm_subst_range_iff
by (argo, blast, auto)
thus ?thesis by blast
next
assume "?Q t" thus ?thesis using SMP.Substitution[OF _ Substitution.hyps(2,3)] by meson
qed
next
case (Ana t K T k)
show ?case using Ana.IH
proof
assume "?P t"
then obtain θ where θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "t ∈ M ⋅⇩s⇩e⇩t θ" by fast
then obtain s where s: "s ∈ M" "t = s ⋅ θ" by auto
then obtain f S where fT: "s = Fun f S" using M by (cases s) auto
obtain K' T' where s_Ana: "Ana s = (K', T')" by (metis surj_pair)
hence "set K = set K' ⋅⇩s⇩e⇩t θ" "set T = set T' ⋅⇩s⇩e⇩t θ"
using Ana_subst'[of f S K' T'] fT Ana.hyps(2) s(2) by auto
then obtain k' where k': "k' ∈ set K'" "k = k' ⋅ θ" using Ana.hyps(3) by fast
show ?thesis
proof (cases "k' ∈ M")
case True thus ?thesis using k' θ(1,2) by blast
next
case False
hence "k' ∈ (subterms⇩s⇩e⇩t M ∪ ⋃((set ∘ fst ∘ Ana) ` M)) - M" using k'(1) s_Ana s(1) by force
thus ?thesis using SMP.Substitution[OF SMP.MP[of k'] θ(1,2)] k'(2) by presburger
qed
next
assume "?Q t" thus ?thesis using SMP.Ana[OF _ Ana.hyps(2,3)] by meson
qed
qed
lemma setops_subterm_trms:
assumes t: "t ∈ pair ` setops⇩s⇩s⇩t S"
and s: "s ⊏ t"
shows "s ∈ subterms⇩s⇩e⇩t (trms⇩s⇩s⇩t S)"
proof -
obtain u u' where u: "pair (u,u') ∈ pair ` setops⇩s⇩s⇩t S" "t = pair (u,u')"
using t setops⇩s⇩s⇩t_are_pairs[of _ S] by blast
hence "s ⊑ u ∨ s ⊑ u'" using s unfolding pair_def by auto
thus ?thesis using u setops⇩s⇩s⇩t_member_iff[of u u' S] unfolding trms⇩s⇩s⇩t_def by force
qed
lemma setops_subterms_cases:
assumes t: "t ∈ subterms⇩s⇩e⇩t (pair ` setops⇩s⇩s⇩t S)"
shows "t ∈ subterms⇩s⇩e⇩t (trms⇩s⇩s⇩t S) ∨ t ∈ pair ` setops⇩s⇩s⇩t S"
proof -
obtain s s' where s: "pair (s,s') ∈ pair ` setops⇩s⇩s⇩t S" "t ⊑ pair (s,s')"
using t setops⇩s⇩s⇩t_are_pairs[of _ S] by blast
hence "t ∈ pair ` setops⇩s⇩s⇩t S ∨ t ⊑ s ∨ t ⊑ s'" unfolding pair_def by auto
thus ?thesis using s setops⇩s⇩s⇩t_member_iff[of s s' S] unfolding trms⇩s⇩s⇩t_def by force
qed
lemma setops_SMP_cases:
assumes "t ∈ SMP (pair ` setops⇩s⇩s⇩t S)"
and "∀p. Ana (pair p) = ([], [])"
shows "(∃δ. wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ t ∈ pair ` setops⇩s⇩s⇩t S ⋅⇩s⇩e⇩t δ) ∨ t ∈ SMP (trms⇩s⇩s⇩t S)"
proof -
have 0: "⋃((set ∘ fst ∘ Ana) ` pair ` setops⇩s⇩s⇩t S) = {}"
proof (induction S)
case (Cons x S) thus ?case
using assms(2) by (cases x) (auto simp add: setops⇩s⇩s⇩t_def)
qed (simp add: setops⇩s⇩s⇩t_def)
have 1: "∀m ∈ pair ` setops⇩s⇩s⇩t S. is_Fun m"
proof (induction S)
case (Cons x S) thus ?case
unfolding pair_def by (cases x) (auto simp add: assms(2) setops⇩s⇩s⇩t_def)
qed (simp add: setops⇩s⇩s⇩t_def)
have 2:
"subterms⇩s⇩e⇩t (pair ` setops⇩s⇩s⇩t S) ∪
⋃((set ∘ fst ∘ Ana) ` (pair ` setops⇩s⇩s⇩t S)) - pair ` setops⇩s⇩s⇩t S
⊆ subterms⇩s⇩e⇩t (trms⇩s⇩s⇩t S)"
using 0 setops_subterms_cases by fast
show ?thesis
using SMP_MP_split[OF assms(1) 1] SMP_mono[OF 2] SMP_subterms_eq[of "trms⇩s⇩s⇩t S"]
by blast
qed
lemma constraint_model_priv_const_in_constr_prefix:
assumes A: "wf⇩s⇩s⇩t A"
and I: "I ⊨⇩s A"
"interpretation⇩s⇩u⇩b⇩s⇩t I"
"wf⇩t⇩r⇩m⇩s (subst_range I)"
"wt⇩s⇩u⇩b⇩s⇩t I"
and c: "¬public c"
"arity c = 0"
"Fun c [] ⊑⇩s⇩e⇩t ik⇩s⇩s⇩t A ⋅⇩s⇩e⇩t I"
shows "Fun c [] ⊑⇩s⇩e⇩t trms⇩s⇩s⇩t A"
using const_subterms_subst_cases[OF c(3)]
proof
assume "Fun c [] ⊑⇩s⇩e⇩t ik⇩s⇩s⇩t A" thus ?thesis using ik⇩s⇩s⇩t_trms⇩s⇩s⇩t_subset by blast
next
assume "∃x ∈ fv⇩s⇩e⇩t (ik⇩s⇩s⇩t A). x ∈ subst_domain I ∧ Fun c [] ⊑ I x"
then obtain x where x: "x ∈ fv⇩s⇩e⇩t (ik⇩s⇩s⇩t A)" "Fun c [] ⊑ I x" by blast
have 0: "wf⇩t⇩r⇩m (I x)" "wf'⇩s⇩s⇩t {} A" "Fun c [] ⋅ I = Fun c []"
using I A by simp_all
have 1: "x ∈ wfrestrictedvars⇩s⇩s⇩t A"
using x(1) in_ik⇩s⇩s⇩t_iff[of _ A] unfolding wfrestrictedvars⇩s⇩s⇩t_def by force
hence 2: "∃v ∈ wfrestrictedvars⇩s⇩s⇩t A. Fun c [] ⋅ I ⊑ I v" using 0(3) x(2) by force
obtain A⇩p⇩r⇩e A⇩s⇩u⇩f where A': "¬(∃w ∈ wfrestrictedvars⇩s⇩s⇩t A⇩p⇩r⇩e. Fun c [] ⊑ I w)"
"(∃ts. A = A⇩p⇩r⇩e@send⟨ts⟩#A⇩s⇩u⇩f ∧ Fun c [] ⊑⇩s⇩e⇩t set ts ⋅⇩s⇩e⇩t I) ∨
(∃s u. A = A⇩p⇩r⇩e@⟨assign: s ≐ u⟩#A⇩s⇩u⇩f ∧ Fun c [] ⊑ s ⋅ I ∧ ¬(Fun c [] ⊑⇩s⇩e⇩t (I ` fv u))) ∨
(∃s u. A = A⇩p⇩r⇩e@⟨assign: s ∈ u⟩#A⇩s⇩u⇩f ∧ (Fun c [] ⊑ s ⋅ I ∨ Fun c [] ⊑ u ⋅ I))"
(is "?X ∨ ?Y ∨ ?Z")
using wf⇩s⇩s⇩t_strand_first_Send_var_split[OF 0(2) 2] by force
show ?thesis using A'(2)
proof (elim disjE)
assume ?X
then obtain ts where ts: "A = A⇩p⇩r⇩e@send⟨ts⟩#A⇩s⇩u⇩f" "Fun c [] ⊑⇩s⇩e⇩t set ts ⋅⇩s⇩e⇩t I" by blast
hence "I ⊨⇩s (A⇩p⇩r⇩e@[send⟨ts⟩])"
using I(1) strand_sem_append_stateful[of "{}" "{}" "A⇩p⇩r⇩e@[send⟨ts⟩]" A⇩s⇩u⇩f I] by auto
hence "(ik⇩s⇩s⇩t A⇩p⇩r⇩e) ⋅⇩s⇩e⇩t I ⊢ t ⋅ I" when "t ∈ set ts" for t
using that strand_sem_append_stateful[of "{}" "{}" A⇩p⇩r⇩e "[send⟨ts⟩]" I]
strand_sem_stateful.simps(2)[of _ _ ts "[]"]
unfolding list_all_iff by force
hence "Fun c [] ⊑⇩s⇩e⇩t ik⇩s⇩s⇩t A⇩p⇩r⇩e ⋅⇩s⇩e⇩t I"
using ts(2) c(1) private_fun_deduct_in_ik by fast
hence "Fun c [] ⊑⇩s⇩e⇩t ik⇩s⇩s⇩t A⇩p⇩r⇩e"
using A'(1) const_subterms_subst_cases[of c I "ik⇩s⇩s⇩t A⇩p⇩r⇩e"]
ik⇩s⇩s⇩t_fv_subset_wfrestrictedvars⇩s⇩s⇩t[of A⇩p⇩r⇩e]
by fast
thus ?thesis
using ik⇩s⇩s⇩t_trms⇩s⇩s⇩t_subset[of "A⇩p⇩r⇩e"] unfolding ts(1) by fastforce
next
assume ?Y
then obtain s u where su:
"A = A⇩p⇩r⇩e@⟨assign: s ≐ u⟩#A⇩s⇩u⇩f" "Fun c [] ⊑ s ⋅ I" "¬(Fun c [] ⊑⇩s⇩e⇩t I ` fv u)"
by fast
hence "s ⋅ I = u ⋅ I"
using I(1) strand_sem_append_stateful[of "{}" "{}" "A⇩p⇩r⇩e@[⟨assign: s ≐ u⟩]" A⇩s⇩u⇩f I]
strand_sem_append_stateful[of _ _ A⇩p⇩r⇩e "[⟨assign: s ≐ u⟩]" I]
by auto
hence "Fun c [] ⊑ u" using su(2,3) const_subterm_subst_var_obtain[of c u I] by auto
thus ?thesis unfolding su(1) by auto
next
assume ?Z
then obtain s u where su:
"A = A⇩p⇩r⇩e@⟨assign: s ∈ u⟩#A⇩s⇩u⇩f" "Fun c [] ⊑ s ⋅ I ∨ Fun c [] ⊑ u ⋅ I"
by fast
hence "(s,u) ⋅⇩p I ∈ dbupd⇩s⇩s⇩t A⇩p⇩r⇩e I {}"
using I(1) strand_sem_append_stateful[of "{}" "{}" "A⇩p⇩r⇩e@[⟨assign: s ∈ u⟩]" A⇩s⇩u⇩f I]
strand_sem_append_stateful[of _ _ A⇩p⇩r⇩e "[⟨assign: s ∈ u⟩]" I]
unfolding db⇩s⇩s⇩t_def by auto
then obtain s' u' where su': "insert⟨s',u'⟩ ∈ set A⇩p⇩r⇩e" "s ⋅ I = s' ⋅ I" "u ⋅ I = u' ⋅ I"
using db⇩s⇩s⇩t_in_cases[of "s ⋅ I" "u ⋅ I" A⇩p⇩r⇩e I "[]"] db⇩s⇩s⇩t_set_is_dbupd⇩s⇩s⇩t[of A⇩p⇩r⇩e I "[]"]
by fastforce
have "fv s' ∪ fv u' ⊆ wfrestrictedvars⇩s⇩s⇩t A⇩p⇩r⇩e"
using su'(1) unfolding wfrestrictedvars⇩s⇩s⇩t_def by force
hence "Fun c [] ⊑ s' ∨ Fun c [] ⊑ u'"
using su(2) A'(1) su'(2,3)
const_subterm_subst_cases[of c s' I]
const_subterm_subst_cases[of c u' I]
by auto
thus ?thesis using su'(1) unfolding su(1) by force
qed
qed
lemma tr⇩p⇩a⇩i⇩r⇩s_empty_case:
assumes "tr⇩p⇩a⇩i⇩r⇩s F D = []"
shows "D = []" "F ≠ []"
proof -
show "F ≠ []" using assms by (auto intro: ccontr)
have "tr⇩p⇩a⇩i⇩r⇩s F (a#A) ≠ []" for a A
by (induct F "a#A" rule: tr⇩p⇩a⇩i⇩r⇩s.induct) fastforce+
thus "D = []" using assms by (cases D) simp_all
qed
lemma tr⇩p⇩a⇩i⇩r⇩s_elem_length_eq:
assumes "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)"
shows "length G = length F"
using assms by (induct F D arbitrary: G rule: tr⇩p⇩a⇩i⇩r⇩s.induct) auto
lemma tr⇩p⇩a⇩i⇩r⇩s_index:
assumes "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)" "i < length F"
shows "∃d ∈ set D. G ! i = (pair (F ! i), pair d)"
using assms
proof (induction F D arbitrary: i G rule: tr⇩p⇩a⇩i⇩r⇩s.induct)
case (2 s t F D)
obtain d G' where G:
"d ∈ set D" "G' ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)"
"G = (pair (s,t), pair d)#G'"
using "2.prems"(1) by atomize_elim auto
show ?case
using "2.IH"[OF G(1,2)] "2.prems"(2) G(1,3)
by (cases i) auto
qed simp
lemma tr⇩p⇩a⇩i⇩r⇩s_cons:
assumes "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)" "d ∈ set D"
shows "(pair (s,t), pair d)#G ∈ set (tr⇩p⇩a⇩i⇩r⇩s ((s,t)#F) D)"
using assms by auto
lemma tr⇩p⇩a⇩i⇩r⇩s_has_pair_lists:
assumes "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)" "g ∈ set G"
shows "∃f ∈ set F. ∃d ∈ set D. g = (pair f, pair d)"
using assms
proof (induction F D arbitrary: G rule: tr⇩p⇩a⇩i⇩r⇩s.induct)
case (2 s t F D)
obtain d G' where G:
"d ∈ set D" "G' ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)"
"G = (pair (s,t), pair d)#G'"
using "2.prems"(1) by atomize_elim auto
show ?case
using "2.IH"[OF G(1,2)] "2.prems"(2) G(1,3)
by (cases "g ∈ set G'") auto
qed simp
lemma tr⇩p⇩a⇩i⇩r⇩s_is_pair_lists:
assumes "f ∈ set F" "d ∈ set D"
shows "∃G ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D). (pair f, pair d) ∈ set G"
(is "?P F D f d")
proof -
have "∀f ∈ set F. ∀d ∈ set D. ?P F D f d"
proof (induction F D rule: tr⇩p⇩a⇩i⇩r⇩s.induct)
case (2 s t F D)
hence IH: "∀f ∈ set F. ∀d ∈ set D. ?P F D f d" by metis
moreover have "∀d ∈ set D. ?P ((s,t)#F) D (s,t) d"
proof
fix d assume d: "d ∈ set D"
then obtain G where G: "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)"
using tr⇩p⇩a⇩i⇩r⇩s_empty_case(1) by force
hence "(pair (s, t), pair d)#G ∈ set (tr⇩p⇩a⇩i⇩r⇩s ((s,t)#F) D)"
using d by auto
thus "?P ((s,t)#F) D (s,t) d" using d G by auto
qed
ultimately show ?case by fastforce
qed simp
thus ?thesis by (metis assms)
qed
lemma tr⇩p⇩a⇩i⇩r⇩s_db_append_subset:
"set (tr⇩p⇩a⇩i⇩r⇩s F D) ⊆ set (tr⇩p⇩a⇩i⇩r⇩s F (D@E))" (is ?A)
"set (tr⇩p⇩a⇩i⇩r⇩s F E) ⊆ set (tr⇩p⇩a⇩i⇩r⇩s F (D@E))" (is ?B)
proof -
show ?A
proof (induction F D rule: tr⇩p⇩a⇩i⇩r⇩s.induct)
case (2 s t F D)
show ?case
proof
fix G assume "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s ((s,t)#F) D)"
then obtain d G' where G':
"d ∈ set D" "G' ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)" "G = (pair (s,t), pair d)#G'"
by atomize_elim auto
have "d ∈ set (D@E)" "G' ∈ set (tr⇩p⇩a⇩i⇩r⇩s F (D@E))" using "2.IH"[OF G'(1)] G'(1,2) by auto
thus "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s ((s,t)#F) (D@E))" using G'(3) by auto
qed
qed simp
show ?B
proof (induction F E rule: tr⇩p⇩a⇩i⇩r⇩s.induct)
case (2 s t F E)
show ?case
proof
fix G assume "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s ((s,t)#F) E)"
then obtain d G' where G':
"d ∈ set E" "G' ∈ set (tr⇩p⇩a⇩i⇩r⇩s F E)" "G = (pair (s,t), pair d)#G'"
by atomize_elim auto
have "d ∈ set (D@E)" "G' ∈ set (tr⇩p⇩a⇩i⇩r⇩s F (D@E))" using "2.IH"[OF G'(1)] G'(1,2) by auto
thus "G ∈ set (tr⇩p⇩a⇩i⇩r⇩s ((s,t)#F) (D@E))" using G'(3) by auto
qed
qed simp
qed
lemma tr⇩p⇩a⇩i⇩r⇩s_trms_subset:
"G ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D) ⟹ trms⇩p⇩a⇩i⇩r⇩s G ⊆ pair ` set F ∪ pair ` set D"
proof (induction F D arbitrary: G rule: tr⇩p⇩a⇩i⇩r⇩s.induct)
case (2 s t F D G)
obtain d G' where G:
"d ∈ set D" "G' ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)" "G = (pair (s,t), pair d)#G'"
using "2.prems"(1) by atomize_elim auto
show ?case using "2.IH"[OF G(1,2)] G(1,3) by auto
qed simp
lemma tr⇩p⇩a⇩i⇩r⇩s_trms_subset':
"⋃(trms⇩p⇩a⇩i⇩r⇩s ` set (tr⇩p⇩a⇩i⇩r⇩s F D)) ⊆ pair ` set F ∪ pair ` set D"
using tr⇩p⇩a⇩i⇩r⇩s_trms_subset by blast
lemma tr⇩p⇩a⇩i⇩r⇩s_vars_subset:
"G ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D) ⟹ fv⇩p⇩a⇩i⇩r⇩s G ⊆ fv⇩p⇩a⇩i⇩r⇩s F ∪ fv⇩p⇩a⇩i⇩r⇩s D"
proof (induction F D arbitrary: G rule: tr⇩p⇩a⇩i⇩r⇩s.induct)
case (2 s t F D G)
obtain d G' where G:
"d ∈ set D" "G' ∈ set (tr⇩p⇩a⇩i⇩r⇩s F D)" "G = (pair (s,t), pair d)#G'"
using "2.prems"(1) by atomize_elim auto
show ?case using "2.IH"[OF G(1,2)] G(1,3) unfolding pair_def by auto
qed simp
lemma tr⇩p⇩a⇩i⇩r⇩s_vars_subset': "⋃(fv⇩p⇩a⇩i⇩r⇩s ` set (tr⇩p⇩a⇩i⇩r⇩s F D)) ⊆ fv⇩p⇩a⇩i⇩r⇩s F ∪ fv⇩p⇩a⇩i⇩r⇩s D"
using tr⇩p⇩a⇩i⇩r⇩s_vars_subset[of _ F D] by blast
lemma tr_trms_subset:
"A' ∈ set (tr A D) ⟹ trms⇩s⇩t A' ⊆ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set D"
proof (induction A D arbitrary: A' rule: tr.induct)
case 1 thus ?case by simp
next
case (2 t A D)
then obtain A'' where A'': "A' = send⟨t⟩⇩s⇩t#A''" "A'' ∈ set (tr A D)" by atomize_elim auto
hence "trms⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set D" by (metis "2.IH")
thus ?case using A'' by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (3 t A D)
then obtain A'' where A'': "A' = receive⟨t⟩⇩s⇩t#A''" "A'' ∈ set (tr A D)" by atomize_elim auto
hence "trms⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set D" by (metis "3.IH")
thus ?case using A'' by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (4 ac t t' A D)
then obtain A'' where A'': "A' = ⟨ac: t ≐ t'⟩⇩s⇩t#A''" "A'' ∈ set (tr A D)" by atomize_elim auto
hence "trms⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set D" by (metis "4.IH")
thus ?case using A'' by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (5 t s A D)
hence "A' ∈ set (tr A (List.insert (t,s) D))" by simp
hence "trms⇩s⇩t A' ⊆ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set (List.insert (t, s) D)"
by (metis "5.IH")
thus ?case by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (6 t s A D)
from 6 obtain Di A'' B C where A'':
"Di ∈ set (subseqs D)" "A'' ∈ set (tr A [d←D. d ∉ set Di])" "A' = (B@C)@A''"
"B = map (λd. ⟨check: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t) Di"
"C = map (λd. Inequality [] [(pair (t,s) , pair d)]) [d←D. d ∉ set Di]"
by atomize_elim auto
hence "trms⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set [d←D. d ∉ set Di]"
by (metis "6.IH")
hence "trms⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t (Delete t s#A) ∪ pair ` setops⇩s⇩s⇩t (Delete t s#A) ∪ pair ` set D"
by (auto simp add: setops⇩s⇩s⇩t_def)
moreover have "trms⇩s⇩t (B@C) ⊆ insert (pair (t,s)) (pair ` set D)"
using A''(4,5) subseqs_set_subset[OF A''(1)] by auto
moreover have "pair (t,s) ∈ pair ` setops⇩s⇩s⇩t (Delete t s#A)" by (simp add: setops⇩s⇩s⇩t_def)
ultimately show ?case using A''(3) trms⇩s⇩t_append[of "B@C" A'] by auto
next
case (7 ac t s A D)
from 7 obtain d A'' where A'':
"d ∈ set D" "A'' ∈ set (tr A D)"
"A' = ⟨ac: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t#A''"
by atomize_elim auto
hence "trms⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set D" by (metis "7.IH")
moreover have "trms⇩s⇩t A' = {pair (t,s), pair d} ∪ trms⇩s⇩t A''"
using A''(1,3) by auto
ultimately show ?case using A''(1) by (auto simp add: setops⇩s⇩s⇩t_def)
next
case (8 X F F' A D)
from 8 obtain A'' where A'':
"A'' ∈ set (tr A D)" "A' = (map (λG. ∀X⟨∨≠: (F@G)⟩⇩s⇩t) (tr⇩p⇩a⇩i⇩r⇩s F' D))@A''"
by atomize_elim auto
define B where "B ≡ ⋃(trms⇩p⇩a⇩i⇩r⇩s ` set (tr⇩p⇩a⇩i⇩r⇩s F' D))"
have "trms⇩s⇩t A'' ⊆ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set D" by (metis A''(1) "8.IH")
hence "trms⇩s⇩t A' ⊆ B ∪ trms⇩p⇩a⇩i⇩r⇩s F ∪ trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A ∪ pair ` set D"
using A'' B_def by auto
moreover have "B ⊆ pair ` set F' ∪ pair ` set D"
using tr⇩p⇩a⇩i⇩r⇩s_trms_subset'[of F' D] B_def by simp
moreover have "pair ` setops⇩s⇩s⇩t (∀X⟨∨≠: F ∨∉: F'⟩#A) = pair ` set F' ∪ pair ` setops⇩s⇩s⇩t A"
by (auto simp add: setops⇩s⇩s⇩t_def)
ultimately show ?case by auto
qed
lemma tr_vars_subset:
assumes "A' ∈ set (tr A D)"
shows "fv⇩s⇩t A' ⊆ fv⇩s⇩s⇩t A ∪ (⋃(t,t') ∈ set D. fv t ∪ fv t')" (is ?P)
and "bvars⇩s⇩t A' ⊆ bvars⇩s⇩s⇩t A" (is ?Q)
proof -
show ?P using assms
proof (induction A arbitrary: A' D rule: strand_sem_stateful_induct)
case (ConsIn A' D ac t s A)
then obtain A'' d where *:
"d ∈ set D" "A' = ⟨ac: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t#A''"
"A'' ∈ set (tr A D)"
by atomize_elim auto
hence "fv⇩s⇩t A'' ⊆ fv⇩s⇩s⇩t A ∪ (⋃(t,t')∈set D. fv t ∪ fv t')" by (metis ConsIn.IH)
thus ?case using * unfolding pair_def by auto
next
case (ConsDel A' D t s A)
define Dfv where "Dfv ≡ λD::('fun,'var) dbstatelist. (⋃(t,t')∈set D. fv t ∪ fv t')"
define fltD where "fltD ≡ λDi. filter (λd. d ∉ set Di) D"
define constr where
"constr ≡ λDi. (map (λd. ⟨check: (pair (t,s)) ≐ (pair d)⟩⇩s⇩t) Di)@
(map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩⇩s⇩t) (fltD Di))"
from ConsDel obtain A'' Di where *:
"Di ∈ set (subseqs D)" "A' = (constr Di)@A''" "A'' ∈ set (tr A (fltD Di))"
unfolding constr_def fltD_def by atomize_elim auto
hence "fv⇩s⇩t A'' ⊆ fv⇩s⇩s⇩t A ∪ Dfv (fltD Di)"
unfolding Dfv_def constr_def fltD_def by (metis ConsDel.IH)
moreover have "Dfv (fltD Di) ⊆ Dfv D" unfolding Dfv_def constr_def fltD_def by auto
moreover have "Dfv Di ⊆ Dfv D"
using subseqs_set_subset(1)[OF *(1)] unfolding Dfv_def constr_def fltD_def by fast
moreover have "fv⇩s⇩t (constr Di) ⊆ fv t ∪ fv s ∪ (Dfv Di ∪ Dfv (fltD Di))"
unfolding Dfv_def constr_def fltD_def pair_def by auto
moreover have "fv⇩s⇩s⇩t (Delete t s#A) = fv t ∪ fv s ∪ fv⇩s⇩s⇩t A" by auto
moreover have "fv⇩s⇩t A' = fv⇩s⇩t (constr Di) ∪ fv⇩s⇩t A''" using * by force
ultimately have "fv⇩s⇩t A' ⊆ fv⇩s⇩s⇩t (Delete t s#A) ∪ Dfv D" by auto
thus ?case unfolding Dfv_def fltD_def constr_def by simp
next
case (ConsNegChecks A' D X F F' A)
then obtain A'' where A'':
"A'' ∈ set (tr A D)" "A' = (map (λG. ∀X⟨∨≠: (F@G)⟩⇩s⇩t) (tr⇩p⇩a⇩i⇩r⇩s F' D))@A''"
by atomize_elim auto
define B where "B ≡ ⋃(fv⇩p⇩a⇩i⇩r⇩s ` set (tr⇩p⇩a⇩i⇩r⇩s F' D))"
have 1: "fv⇩s⇩t (map (λG. ∀X⟨∨≠: (F@G)⟩⇩s⇩t) (tr⇩p⇩a⇩i⇩r⇩s F' D)) ⊆ (B ∪ fv⇩p⇩a⇩i⇩r⇩s F) - set X"
unfolding B_def by auto
have 2: "B ⊆ fv⇩p⇩a⇩i⇩r⇩s F' ∪ fv⇩p⇩a⇩i⇩r⇩s D"
using tr⇩p⇩a⇩i⇩r⇩s_vars_subset'[of F' D]
unfolding B_def by simp
have "fv⇩s⇩t A' ⊆ ((fv⇩p⇩a⇩i⇩r⇩s F' ∪ fv⇩p⇩a⇩i⇩r⇩s D ∪ fv⇩p⇩a⇩i⇩r⇩s F) - set X) ∪ fv⇩s⇩t A''"
using 1 2 A''(2) by fastforce
thus ?case using ConsNegChecks.IH[OF A''(1)] by auto
qed fastforce+
show ?Q using assms by (induct A arbitrary: A' D rule: strand_sem_stateful_induct) fastforce+
qed
lemma tr_vars_disj:
assumes "A' ∈ set (tr A D)" "∀(t,t') ∈ set D. (fv t ∪ fv t') ∩ bvars⇩s⇩s⇩t A = {}"
and "fv⇩s⇩s⇩t A ∩ bvars⇩s⇩s⇩t A = {}"
shows "fv⇩s⇩t A' ∩ bvars⇩s⇩t A' = {}"
using assms tr_vars_subset by fast
lemma tfr⇩s⇩s⇩t⇩p_alt_def:
"list_all tfr⇩s⇩s⇩t⇩p S =
((∀ac t t'. Equality ac t t' ∈ set S ∧ (∃δ. Unifier δ t t') ⟶ Γ t = Γ t') ∧
(∀X F F'. NegChecks X F F' ∈ set S ⟶ (
(F' = [] ∧ (∀x ∈ fv⇩p⇩a⇩i⇩r⇩s F-set X. ∃a. Γ (Var x) = TAtom a)) ∨
(∀f T. Fun f T ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F ∪ pair ` set F') ⟶
T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X)))))"
(is "?P S = ?Q S")
proof
show "?P S ⟹ ?Q S"
proof (induction S)
case (Cons x S) thus ?case by (cases x) auto
qed simp
show "?Q S ⟹ ?P S"
proof (induction S)
case (Cons x S) thus ?case by (cases x) auto
qed simp
qed
lemma tfr⇩s⇩s⇩t_Nil[simp]: "tfr⇩s⇩s⇩t []"
by (simp add: tfr⇩s⇩s⇩t_def setops⇩s⇩s⇩t_def)
lemma tfr⇩s⇩s⇩t_append: "tfr⇩s⇩s⇩t (A@B) ⟹ tfr⇩s⇩s⇩t A"
proof -
assume assms: "tfr⇩s⇩s⇩t (A@B)"
let ?M = "trms⇩s⇩s⇩t A ∪ pair ` setops⇩s⇩s⇩t A"
let ?N = "trms⇩s⇩s⇩t (A@B) ∪ pair ` setops⇩s⇩s⇩t (A@B)"
let ?P = "λt t'. ∀x ∈ fv t ∪ fv t'. ∃a. Γ (Var x) = Var a"
let ?Q = "λX t t'. X = [] ∨ (∀x ∈ (fv t ∪ fv t')-set X. ∃a. Γ (Var x) = Var a)"
have *: "SMP ?M - Var`𝒱 ⊆ SMP ?N - Var`𝒱" "?M ⊆ ?N"
using SMP_mono[of ?M ?N] setops⇩s⇩s⇩t_append[of A B]
by auto
{ fix s t assume **: "tfr⇩s⇩e⇩t ?N" "s ∈ SMP ?M - Var`𝒱" "t ∈ SMP ?M - Var`𝒱" "(∃δ. Unifier δ s t)"
hence "s ∈ SMP ?N - Var`𝒱" "t ∈ SMP ?N - Var`𝒱" using * by auto
hence "Γ s = Γ t" using **(1,4) unfolding tfr⇩s⇩e⇩t_def by blast
} moreover have "∀t ∈ ?N. wf⇩t⇩r⇩m t ⟹ ∀t ∈ ?M. wf⇩t⇩r⇩m t" using * by blast
ultimately have "tfr⇩s⇩e⇩t ?N ⟹ tfr⇩s⇩e⇩t ?M" unfolding tfr⇩s⇩e⇩t_def by blast
hence "tfr⇩s⇩e⇩t ?M" using assms unfolding tfr⇩s⇩s⇩t_def by metis
thus "tfr⇩s⇩s⇩t A" using assms unfolding tfr⇩s⇩s⇩t_def by simp
qed
lemma tfr⇩s⇩s⇩t_append': "tfr⇩s⇩s⇩t (A@B) ⟹ tfr⇩s⇩s⇩t B"
proof -
assume assms: "tfr⇩s⇩s⇩t (A@B)"
let ?M = "trms⇩s⇩s⇩t B ∪ pair ` setops⇩s⇩s⇩t B"
let ?N = "trms⇩s⇩s⇩t (A@B) ∪ pair ` setops⇩s⇩s⇩t (A@B)"
let ?P = "λt t'. ∀x ∈ fv t ∪ fv t'. ∃a. Γ (Var x) = Var a"
let ?Q = "λX t t'. X = [] ∨ (∀x ∈ (fv t ∪ fv t')-set X. ∃a. Γ (Var x) = Var a)"
have *: "SMP ?M - Var`𝒱 ⊆ SMP ?N - Var`𝒱" "?M ⊆ ?N"
using SMP_mono[of ?M ?N] setops⇩s⇩s⇩t_append[of A B]
by auto
{ fix s t assume **: "tfr⇩s⇩e⇩t ?N" "s ∈ SMP ?M - Var`𝒱" "t ∈ SMP ?M - Var`𝒱" "(∃δ. Unifier δ s t)"
hence "s ∈ SMP ?N - Var`𝒱" "t ∈ SMP ?N - Var`𝒱" using * by auto
hence "Γ s = Γ t" using **(1,4) unfolding tfr⇩s⇩e⇩t_def by blast
} moreover have "∀t ∈ ?N. wf⇩t⇩r⇩m t ⟹ ∀t ∈ ?M. wf⇩t⇩r⇩m t" using * by blast
ultimately have "tfr⇩s⇩e⇩t ?N ⟹ tfr⇩s⇩e⇩t ?M" unfolding tfr⇩s⇩e⇩t_def by blast
hence "tfr⇩s⇩e⇩t ?M" using assms unfolding tfr⇩s⇩s⇩t_def by metis
thus "tfr⇩s⇩s⇩t B" using assms unfolding tfr⇩s⇩s⇩t_def by simp
qed
lemma tfr⇩s⇩s⇩t_cons: "tfr⇩s⇩s⇩t (a#A) ⟹ tfr⇩s⇩s⇩t A"
using tfr⇩s⇩s⇩t_append'[of "[a]" A] by simp
lemma tfr⇩s⇩s⇩t⇩p_subst:
assumes s: "tfr⇩s⇩s⇩t⇩p s"
and θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "set (bvars⇩s⇩s⇩t⇩p s) ∩ range_vars θ = {}"
shows "tfr⇩s⇩s⇩t⇩p (s ⋅⇩s⇩s⇩t⇩p θ)"
proof (cases s)
case (Equality a t t')
thus ?thesis
proof (cases "∃δ. Unifier δ (t ⋅ θ) (t' ⋅ θ)")
case True
hence "∃δ. Unifier δ t t'" by (metis subst_subst_compose[of _ θ])
moreover have "Γ t = Γ (t ⋅ θ)" "Γ t' = Γ (t' ⋅ θ)" by (metis wt_subst_trm''[OF assms(2)])+
ultimately have "Γ (t ⋅ θ) = Γ (t' ⋅ θ)" using s Equality by simp
thus ?thesis using Equality True by simp
qed simp
next
case (NegChecks X F G)
let ?P = "λF G. G = [] ∧ (∀x ∈ fv⇩p⇩a⇩i⇩r⇩s F-set X. ∃a. Γ (Var x) = TAtom a)"
let ?Q = "λF G. ∀f T. Fun f T ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F ∪ pair ` set G) ⟶
T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X)"
let ?θ = "rm_vars (set X) θ"
have "?P F G ∨ ?Q F G" using NegChecks assms(1) by simp
hence "?P (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ) (G ⋅⇩p⇩a⇩i⇩r⇩s ?θ) ∨ ?Q (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ) (G ⋅⇩p⇩a⇩i⇩r⇩s ?θ)"
proof
assume *: "?P F G"
have "G ⋅⇩p⇩a⇩i⇩r⇩s ?θ = []" using * by simp
moreover have "∃a. Γ (Var x) = TAtom a" when x: "x ∈ fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ) - set X" for x
proof -
obtain t t' where t: "(t,t') ∈ set (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ)" "x ∈ fv t ∪ fv t' - set X"
using x(1) by auto
then obtain u u' where u: "(u,u') ∈ set F" "u ⋅ ?θ = t" "u' ⋅ ?θ = t'"
unfolding subst_apply_pairs_def by auto
obtain y where y: "y ∈ fv u ∪ fv u' - set X" "x ∈ fv (?θ y)"
using t(2) u(2,3) rm_vars_fv_obtain by fast
hence a: "∃a. Γ (Var y) = TAtom a" using u * by auto
have a': "Γ (Var y) = Γ (?θ y)"
using wt_subst_trm''[OF wt_subst_rm_vars[OF θ(1), of "set X"], of "Var y"]
by simp
have "(∃z. ?θ y = Var z) ∨ (∃c. ?θ y = Fun c [])"
proof (cases "?θ y ∈ subst_range θ")
case True thus ?thesis
using a a' θ(2) const_type_inv_wf
by (cases "?θ y") fastforce+
qed fastforce
hence "?θ y = Var x" using y(2) by fastforce
hence "Γ (Var x) = Γ (Var y)" using a' by simp
thus ?thesis using a by presburger
qed
ultimately show ?thesis by simp
next
assume *: "?Q F G"
have **: "set X ∩ range_vars ?θ = {}"
using θ(3) NegChecks rm_vars_img_fv_subset[of "set X" θ] by auto
have "?Q (F ⋅⇩p⇩a⇩i⇩r⇩s ?θ) (G ⋅⇩p⇩a⇩i⇩r⇩s ?θ)"
using ineq_subterm_inj_cond_subst[OF ** *]
trms⇩p⇩a⇩i⇩r⇩s_subst[of F "rm_vars (set X) θ"]
subst_apply_pairs_pair_image_subst[of G "rm_vars (set X) θ"]
by (metis (no_types, lifting) image_Un)
thus ?thesis by simp
qed
thus ?thesis using NegChecks by simp
qed simp_all
lemma tfr⇩s⇩s⇩t⇩p_all_wt_subst_apply:
assumes S: "list_all tfr⇩s⇩s⇩t⇩p S"
and θ: "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "bvars⇩s⇩s⇩t S ∩ range_vars θ = {}"
shows "list_all tfr⇩s⇩s⇩t⇩p (S ⋅⇩s⇩s⇩t θ)"
proof -
have "set (bvars⇩s⇩s⇩t⇩p s) ∩ range_vars θ = {}" when "s ∈ set S" for s
using that θ(3) unfolding bvars⇩s⇩s⇩t_def range_vars_alt_def by fastforce
thus ?thesis
using tfr⇩s⇩s⇩t⇩p_subst[OF _ θ(1,2)] S
unfolding list_all_iff
by (auto simp add: subst_apply_stateful_strand_def)
qed
lemma tfr_setops_if_tfr_trms:
assumes "Pair ∉ ⋃(funs_term ` SMP (trms⇩s⇩s⇩t S))"
and "∀p. Ana (pair p) = ([], [])"
and "∀s ∈ pair ` setops⇩s⇩s⇩t S. ∀t ∈ pair ` setops⇩s⇩s⇩t S. (∃δ. Unifier δ s t) ⟶ Γ s = Γ t"
and "∀s ∈ pair ` setops⇩s⇩s⇩t S. ∀t ∈ pair ` setops⇩s⇩s⇩t S.
(∃σ θ ρ. wt⇩s⇩u⇩b⇩s⇩t σ ∧ wt⇩s⇩u⇩b⇩s⇩t θ ∧ wf⇩t⇩r⇩m⇩s (subst_range σ) ∧ wf⇩t⇩r⇩m⇩s (subst_range θ) ∧
Unifier ρ (s ⋅ σ) (t ⋅ θ))
⟶ (∃δ. Unifier δ s t)"
and tfr: "tfr⇩s⇩e⇩t (trms⇩s⇩s⇩t S)"
shows "tfr⇩s⇩e⇩t (trms⇩s⇩s⇩t S ∪ pair ` setops⇩s⇩s⇩t S)"
proof -
have 0: "t ∈ SMP (trms⇩s⇩s⇩t S) - range Var ∨ t ∈ SMP (pair ` setops⇩s⇩s⇩t S) - range Var"
when "t ∈ SMP (trms⇩s⇩s⇩t S ∪ pair ` setops⇩s⇩s⇩t S) - range Var" for t
using that SMP_union by blast
have 1: "s ∈ SMP (trms⇩s⇩s⇩t S) - range Var"
when st: "s ∈ SMP (pair ` setops⇩s⇩s⇩t S) - range Var"
"t ∈ SMP (trms⇩s⇩s⇩t S) - range Var"
"∃δ. Unifier δ s t"
for s t
proof -
have "(∃δ. s ∈ pair ` setops⇩s⇩s⇩t S ⋅⇩s⇩e⇩t δ) ∨ s ∈ SMP (trms⇩s⇩s⇩t S) - range Var"
using st setops_SMP_cases[of s S] assms(2) by blast
moreover {
fix δ assume δ: "s ∈ pair ` setops⇩s⇩s⇩t S ⋅⇩s⇩e⇩t δ"
then obtain s' where s': "s' ∈ pair ` setops⇩s⇩s⇩t S" "s = s' ⋅ δ" by blast
then obtain u u' where u: "s' = Fun Pair [u,u']"
using setops⇩s⇩s⇩t_are_pairs[of s'] unfolding pair_def by fast
hence *: "s = Fun Pair [u ⋅ δ, u' ⋅ δ]" using δ s' by simp
obtain f T where fT: "t = Fun f T" using st(2) by (cases t) auto
hence "f ≠ Pair" using st(2) assms(1) by auto
hence False using st(3) * fT s' u by fast
} ultimately show ?thesis by meson
qed
have 2: "Γ s = Γ t"
when "s ∈ SMP (trms⇩s⇩s⇩t S) - range Var"
"t ∈ SMP (trms⇩s⇩s⇩t S) - range Var"
"∃δ. Unifier δ s t"
for s t
using that tfr unfolding tfr⇩s⇩e⇩t_def by blast
have 3: "Γ s = Γ t"
when st: "s ∈ SMP (pair ` setops⇩s⇩s⇩t S) - range Var"
"t ∈ SMP (pair ` setops⇩s⇩s⇩t S) - range Var"
"∃δ. Unifier δ s