Theory FullAbstraction
theory FullAbstraction
imports SourceTargetRelation
begin
section ‹Full Abstraction›
text ‹An encoding is fully abstract w.r.t. some source term relation SRel and some target term
relation TRel if two source terms S1 and S2 form a pair (S1, S2) in SRel iff their literal
translations form a pair (enc S1, enc S2) in TRel.›
abbreviation (in encoding) fully_abstract
:: "('procS × 'procS) set ⇒ ('procT × 'procT) set ⇒ bool"
where
"fully_abstract SRel TRel ≡ ∀S1 S2. (S1, S2) ∈ SRel ⟷ (⟦S1⟧, ⟦S2⟧) ∈ TRel"
subsection ‹Trivial Full Abstraction Results›
text ‹We start with some trivial full abstraction results. Each injective encoding is fully
abstract w.r.t. to the identity relation on the source and the identity relation on the
target.›
lemma (in encoding) inj_enc_is_fully_abstract_wrt_identities:
assumes injectivity: "∀S1 S2. ⟦S1⟧ = ⟦S2⟧ ⟶ S1 = S2"
shows "fully_abstract {(S1, S2). S1 = S2} {(T1, T2). T1 = T2}"
by (auto simp add: injectivity)
text ‹Each encoding is fully abstract w.r.t. the empty relation on the source and the target.›
lemma (in encoding) fully_abstract_wrt_empty_relation:
shows "fully_abstract {} {}"
by auto
text ‹Similarly, each encoding is fully abstract w.r.t. the all-relation on the source and the
target.›
lemma (in encoding) fully_abstract_wrt_all_relation:
shows "fully_abstract {(S1, S2). True} {(T1, T2). True}"
by auto
text ‹If the encoding is injective then for each source term relation RelS there exists a target
term relation RelT such that the encoding is fully abstract w.r.t. RelS and RelT.›
lemma (in encoding) fully_abstract_wrt_source_relation:
fixes RelS :: "('procS × 'procS) set"
assumes injectivity: "∀S1 S2. ⟦S1⟧ = ⟦S2⟧ ⟶ S1 = S2"
shows "∃RelT. fully_abstract RelS RelT"
proof -
define RelT where "RelT = {(T1, T2). ∃S1 S2. (S1, S2) ∈ RelS ∧ T1 = ⟦S1⟧ ∧ T2 = ⟦S2⟧}"
with injectivity have "fully_abstract RelS RelT"
by blast
thus "∃RelT. fully_abstract RelS RelT"
by blast
qed
text ‹If all source terms that are translated to the same target term are related by a trans
source term relation RelS, then there exists a target term relation RelT such that the
encoding is fully abstract w.r.t. RelS and RelT.›
lemma (in encoding) fully_abstract_wrt_trans_source_relation:
fixes RelS :: "('procS × 'procS) set"
assumes encRelS: "∀S1 S2. ⟦S1⟧ = ⟦S2⟧ ⟶ (S1, S2) ∈ RelS"
and transS: "trans RelS"
shows "∃RelT. fully_abstract RelS RelT"
proof -
define RelT where "RelT = {(T1, T2). ∃S1 S2. (S1, S2) ∈ RelS ∧ T1 = ⟦S1⟧ ∧ T2 = ⟦S2⟧}"
have "fully_abstract RelS RelT"
proof auto
fix S1 S2
assume "(S1, S2) ∈ RelS"
with RelT_def show "(⟦S1⟧, ⟦S2⟧) ∈ RelT"
by blast
next
fix S1 S2
assume "(⟦S1⟧, ⟦S2⟧) ∈ RelT"
with RelT_def obtain S1' S2' where A1: "(S1', S2') ∈ RelS" and A2: "⟦S1⟧ = ⟦S1'⟧"
and A3: "⟦S2⟧ = ⟦S2'⟧"
by blast
from A2 encRelS have "(S1, S1') ∈ RelS"
by simp
from this A1 transS have "(S1, S2') ∈ RelS"
unfolding trans_def
by blast
moreover from A3 encRelS have "(S2', S2) ∈ RelS"
by simp
ultimately show "(S1, S2) ∈ RelS"
using transS
unfolding trans_def
by blast
qed
thus "∃RelT. fully_abstract RelS RelT"
by blast
qed
lemma (in encoding) fully_abstract_wrt_trans_closure_of_source_relation:
fixes RelS :: "('procS × 'procS) set"
assumes encRelS: "∀S1 S2. ⟦S1⟧ = ⟦S2⟧ ⟶ (S1, S2) ∈ RelS⇧+"
shows "∃RelT. fully_abstract (RelS⇧+) RelT"
using encRelS trans_trancl[of RelS]
fully_abstract_wrt_trans_source_relation[where RelS="RelS⇧+"]
by blast
text ‹For every encoding and every target term relation RelT there exists a source term relation
RelS such that the encoding is fully abstract w.r.t. RelS and RelT.›
lemma (in encoding) fully_abstract_wrt_target_relation:
fixes RelT :: "('procT × 'procT) set"
shows "∃RelS. fully_abstract RelS RelT"
proof -
define RelS where "RelS = {(S1, S2). (⟦S1⟧, ⟦S2⟧) ∈ RelT}"
hence "fully_abstract RelS RelT"
by simp
thus "∃RelS. fully_abstract RelS RelT"
by blast
qed
subsection ‹Fully Abstract Encodings›
text ‹Thus, as long as we can choose one of the two relations, full abstraction is trivial. For
fixed source and target term relations encodings are not trivially fully abstract. For all
encodings and relations SRel and TRel we can construct a relation on the disjunctive union
of source and target terms, whose reduction to source terms is SRel and whose reduction to
target terms is TRel. But full abstraction ensures that each trans relation that
relates source terms and their literal translations in both directions includes SRel iff it
includes TRel restricted to translated source terms.›
lemma (in encoding) full_abstraction_and_trans_relation_contains_SRel_impl_TRel:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
and SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and encR: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and srel: "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
and trans: "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
shows "∀S1 S2. (⟦S1⟧, ⟦S2⟧) ∈ TRel ⟷ (TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
proof auto
fix S1 S2
define Rel' where "Rel' = Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
hence "(TargetTerm (⟦S1⟧), SourceTerm S1) ∈ Rel'"
by simp
moreover assume "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
with fullAbs have "(S1, S2) ∈ SRel"
by simp
with srel Rel'_def have "(SourceTerm S1, SourceTerm S2) ∈ Rel'"
by simp
moreover from encR Rel'_def have "(SourceTerm S2, TargetTerm (⟦S2⟧)) ∈ Rel'"
by simp
ultimately show "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
using trans Rel'_def
unfolding trans_def
by blast
next
fix S1 S2
define Rel' where "Rel' = Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
from encR Rel'_def have "(SourceTerm S1, TargetTerm (⟦S1⟧)) ∈ Rel'"
by simp
moreover assume "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
with Rel'_def have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel'"
by simp
moreover from Rel'_def have "(TargetTerm (⟦S2⟧), SourceTerm S2) ∈ Rel'"
by simp
ultimately have "(SourceTerm S1, SourceTerm S2) ∈ Rel"
using trans Rel'_def
unfolding trans_def
by blast
with srel have "(S1, S2) ∈ SRel"
by simp
with fullAbs show "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
by simp
qed
lemma (in encoding) full_abstraction_and_trans_relation_contains_TRel_impl_SRel:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
and SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and encR: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and trel: "∀S1 S2. (⟦S1⟧, ⟦S2⟧) ∈ TRel ⟷ (TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
and trans: "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
shows "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
proof auto
fix S1 S2
define Rel' where "Rel' = Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
from encR Rel'_def have "(SourceTerm S1, TargetTerm (⟦S1⟧)) ∈ Rel'"
by simp
moreover assume "(S1, S2) ∈ SRel"
with fullAbs have "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
by simp
with trel Rel'_def have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel'"
by simp
moreover from Rel'_def have "(TargetTerm (⟦S2⟧), SourceTerm S2) ∈ Rel'"
by simp
ultimately show "(SourceTerm S1, SourceTerm S2) ∈ Rel"
using trans Rel'_def
unfolding trans_def
by blast
next
fix S1 S2
define Rel' where "Rel' = Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
hence "(TargetTerm (⟦S1⟧), SourceTerm S1) ∈ Rel'"
by simp
moreover assume "(SourceTerm S1, SourceTerm S2) ∈ Rel"
with Rel'_def have "(SourceTerm S1, SourceTerm S2) ∈ Rel'"
by simp
moreover from encR Rel'_def have "(SourceTerm S2, TargetTerm (⟦S2⟧)) ∈ Rel'"
by simp
ultimately have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
using trans Rel'_def
unfolding trans_def
by blast
with trel have "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
by simp
with fullAbs show "(S1, S2) ∈ SRel"
by simp
qed
lemma (in encoding) full_abstraction_impl_trans_relation_contains_SRel_iff_TRel:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
and SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and encR: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and trans: "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
shows "(∀S1 S2. (⟦S1⟧, ⟦S2⟧) ∈ TRel ⟷ (TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel)
⟷ (SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel})"
proof
assume "∀S1 S2. ((⟦S1⟧, ⟦S2⟧) ∈ TRel) = ((TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel)"
thus "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
using assms full_abstraction_and_trans_relation_contains_TRel_impl_SRel[where
SRel="SRel" and TRel="TRel"]
by blast
next
assume "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
thus "∀S1 S2. (⟦S1⟧, ⟦S2⟧) ∈ TRel ⟷ (TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
using assms full_abstraction_and_trans_relation_contains_SRel_impl_TRel[where
SRel="SRel" and TRel="TRel"]
by blast
qed
lemma (in encoding) full_abstraction_impl_trans_relation_contains_SRel_iff_TRel_encRL:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
and SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and encR: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and encL: "∀S. (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
and trans: "trans Rel"
shows "(∀S1 S2. (⟦S1⟧, ⟦S2⟧) ∈ TRel ⟷ (TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel)
⟷ (SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel})"
proof -
from encL have "Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} = Rel"
by auto
with fullAbs encR trans show ?thesis
using full_abstraction_impl_trans_relation_contains_SRel_iff_TRel[where Rel="Rel"
and SRel="SRel" and TRel="TRel"]
by simp
qed
text ‹Full abstraction ensures that SRel and TRel satisfy the same basic properties that can be
defined on their pairs. In particular:
(1) SRel is refl iff TRel reduced to translated source terms is refl
(2) if the encoding is surjective then SRel is refl iff TRel is refl
(3) SRel is sym iff TRel reduced to translated source terms is sym
(4) SRel is trans iff TRel reduced to translated source terms is trans›
lemma (in encoding) full_abstraction_impl_SRel_iff_TRel_is_refl:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
shows "refl SRel ⟷ (∀S. (⟦S⟧, ⟦S⟧) ∈ TRel)"
unfolding refl_on_def
by (simp add: fullAbs)
lemma (in encoding) full_abstraction_and_surjectivity_impl_SRel_iff_TRel_is_refl:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and surj: "∀T. ∃S. T = ⟦S⟧"
shows "refl SRel ⟷ refl TRel"
proof
assume reflS: "refl SRel"
show "refl TRel"
unfolding refl_on_def
proof auto
fix T
from surj obtain S where "T = ⟦S⟧"
by blast
moreover from reflS have "(S, S) ∈ SRel"
unfolding refl_on_def
by simp
with fullAbs have "(⟦S⟧, ⟦S⟧) ∈ TRel"
by simp
ultimately show "(T, T) ∈ TRel"
by simp
qed
next
assume "refl TRel"
with fullAbs show "refl SRel"
unfolding refl_on_def
by simp
qed
lemma (in encoding) full_abstraction_impl_SRel_iff_TRel_is_sym:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
shows "sym SRel ⟷ sym {(T1, T2). ∃S1 S2. T1 = ⟦S1⟧ ∧ T2 = ⟦S2⟧ ∧ (T1, T2) ∈ TRel}"
unfolding sym_def
by (simp add: fullAbs, blast)
lemma (in encoding) full_abstraction_and_surjectivity_impl_SRel_iff_TRel_is_sym:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and surj: "∀T. ∃S. T = ⟦S⟧"
shows "sym SRel ⟷ sym TRel"
using fullAbs surj
full_abstraction_impl_SRel_iff_TRel_is_sym[where SRel="SRel" and TRel="TRel"]
by auto
lemma (in encoding) full_abstraction_impl_SRel_iff_TRel_is_trans:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
shows "trans SRel ⟷ trans {(T1, T2). ∃S1 S2. T1 = ⟦S1⟧ ∧ T2 = ⟦S2⟧ ∧ (T1, T2) ∈ TRel}"
unfolding trans_def
by (simp add: fullAbs, blast)
lemma (in encoding) full_abstraction_and_surjectivity_impl_SRel_iff_TRel_is_trans:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and surj: "∀T. ∃S. T = ⟦S⟧"
shows "trans SRel ⟷ trans TRel"
using fullAbs surj
full_abstraction_impl_SRel_iff_TRel_is_trans[where SRel="SRel" and TRel="TRel"]
by auto
text ‹Similarly, a fully abstract encoding that respects a predicate ensures the this predicate
is preserved, reflected, or respected by SRel iff it is preserved, reflected, or respected
by TRel.›
lemma (in encoding) full_abstraction_and_enc_respects_pred_impl_SRel_iff_TRel_preserve:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and Pred :: "('procS, 'procT) Proc ⇒ bool"
assumes fullAbs: "fully_abstract SRel TRel"
and encP: "enc_respects_pred Pred"
shows "rel_preserves_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred
⟷ rel_preserves_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
proof
assume presS: "rel_preserves_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred"
show "rel_preserves_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
proof clarify
fix SP SQ
assume "Pred (TargetTerm (⟦SP⟧))"
with encP have "Pred (SourceTerm SP)"
by simp
moreover assume "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
with fullAbs have "(SP, SQ) ∈ SRel"
by simp
ultimately have "Pred (SourceTerm SQ)"
using presS
by blast
with encP show "Pred (TargetTerm (⟦SQ⟧))"
by simp
qed
next
assume presT:
"rel_preserves_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
show "rel_preserves_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred"
proof clarify
fix SP SQ
assume "Pred (SourceTerm SP)"
with encP have "Pred (TargetTerm (⟦SP⟧))"
by simp
moreover assume "(SP, SQ) ∈ SRel"
with fullAbs have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by simp
ultimately have "Pred (TargetTerm (⟦SQ⟧))"
using presT
by blast
with encP show "Pred (SourceTerm SQ)"
by simp
qed
qed
lemma (in encoding) full_abstraction_and_enc_respects_binary_pred_impl_SRel_iff_TRel_preserve:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and Pred :: "('procS, 'procT) Proc ⇒ 'b ⇒ bool"
assumes fullAbs: "fully_abstract SRel TRel"
and encP: "enc_respects_binary_pred Pred"
shows "rel_preserves_binary_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred
⟷ rel_preserves_binary_pred
{(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
proof
assume presS:
"rel_preserves_binary_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred"
show "rel_preserves_binary_pred
{(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
proof clarify
fix x SP SQ
assume "Pred (TargetTerm (⟦SP⟧)) x"
with encP have "Pred (SourceTerm SP) x"
by simp
moreover assume "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
with fullAbs have "(SP, SQ) ∈ SRel"
by simp
ultimately have "Pred (SourceTerm SQ) x"
using presS
by blast
with encP show "Pred (TargetTerm (⟦SQ⟧)) x"
by simp
qed
next
assume presT:
"rel_preserves_binary_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
show "rel_preserves_binary_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred"
proof clarify
fix x SP SQ
assume "Pred (SourceTerm SP) x"
with encP have "Pred (TargetTerm (⟦SP⟧)) x"
by simp
moreover assume "(SP, SQ) ∈ SRel"
with fullAbs have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by simp
ultimately have "Pred (TargetTerm (⟦SQ⟧)) x"
using presT
by blast
with encP show "Pred (SourceTerm SQ) x"
by simp
qed
qed
lemma (in encoding) full_abstraction_and_enc_respects_pred_impl_SRel_iff_TRel_reflects:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and Pred :: "('procS, 'procT) Proc ⇒ bool"
assumes fullAbs: "fully_abstract SRel TRel"
and encP: "enc_respects_pred Pred"
shows "rel_reflects_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred
⟷ rel_reflects_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
proof
assume reflS: "rel_reflects_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred"
show "rel_reflects_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
proof clarify
fix SP SQ
assume "Pred (TargetTerm (⟦SQ⟧))"
with encP have "Pred (SourceTerm SQ)"
by simp
moreover assume "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
with fullAbs have "(SP, SQ) ∈ SRel"
by simp
ultimately have "Pred (SourceTerm SP)"
using reflS
by blast
with encP show "Pred (TargetTerm (⟦SP⟧))"
by simp
qed
next
assume reflT:
"rel_reflects_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
show "rel_reflects_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred"
proof clarify
fix SP SQ
assume "Pred (SourceTerm SQ)"
with encP have "Pred (TargetTerm (⟦SQ⟧))"
by simp
moreover assume "(SP, SQ) ∈ SRel"
with fullAbs have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by simp
ultimately have "Pred (TargetTerm (⟦SP⟧))"
using reflT
by blast
with encP show "Pred (SourceTerm SP)"
by simp
qed
qed
lemma (in encoding) full_abstraction_and_enc_respects_binary_pred_impl_SRel_iff_TRel_reflects:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and Pred :: "('procS, 'procT) Proc ⇒ 'b ⇒ bool"
assumes fullAbs: "fully_abstract SRel TRel"
and encP: "enc_respects_binary_pred Pred"
shows "rel_reflects_binary_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred
⟷ rel_reflects_binary_pred
{(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
proof
assume reflS:
"rel_reflects_binary_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred"
show "rel_reflects_binary_pred
{(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
proof clarify
fix x SP SQ
assume "Pred (TargetTerm (⟦SQ⟧)) x"
with encP have "Pred (SourceTerm SQ) x"
by simp
moreover assume "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
with fullAbs have "(SP, SQ) ∈ SRel"
by simp
ultimately have "Pred (SourceTerm SP) x"
using reflS
by blast
with encP show "Pred (TargetTerm (⟦SP⟧)) x"
by simp
qed
next
assume reflT:
"rel_reflects_binary_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
show "rel_reflects_binary_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred"
proof clarify
fix x SP SQ
assume "Pred (SourceTerm SQ) x"
with encP have "Pred (TargetTerm (⟦SQ⟧)) x"
by simp
moreover assume "(SP, SQ) ∈ SRel"
with fullAbs have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by simp
ultimately have "Pred (TargetTerm (⟦SP⟧)) x"
using reflT
by blast
with encP show "Pred (SourceTerm SP) x"
by simp
qed
qed
lemma (in encoding) full_abstraction_and_enc_respects_pred_impl_SRel_iff_TRel_respects:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and Pred :: "('procS, 'procT) Proc ⇒ bool"
assumes fullAbs: "fully_abstract SRel TRel"
and encP: "enc_respects_pred Pred"
shows "rel_respects_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred
⟷ rel_respects_pred {(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
using assms full_abstraction_and_enc_respects_pred_impl_SRel_iff_TRel_preserve[where
SRel="SRel" and TRel="TRel" and Pred="Pred"]
full_abstraction_and_enc_respects_pred_impl_SRel_iff_TRel_reflects[where
SRel="SRel" and TRel="TRel" and Pred="Pred"]
by auto
lemma (in encoding) full_abstraction_and_enc_respects_binary_pred_impl_SRel_iff_TRel_respects:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and Pred :: "('procS, 'procT) Proc ⇒ 'b ⇒ bool"
assumes fullAbs: "fully_abstract SRel TRel"
and encP: "enc_respects_binary_pred Pred"
shows "rel_respects_binary_pred {(P, Q). ∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel} Pred
⟷ rel_respects_binary_pred
{(P, Q). ∃SP SQ. ⟦SP⟧ ∈T P ∧ ⟦SQ⟧ ∈T Q ∧ (⟦SP⟧, ⟦SQ⟧) ∈ TRel} Pred"
using assms full_abstraction_and_enc_respects_binary_pred_impl_SRel_iff_TRel_preserve[where
SRel="SRel" and TRel="TRel" and Pred="Pred"]
full_abstraction_and_enc_respects_binary_pred_impl_SRel_iff_TRel_reflects[where
SRel="SRel" and TRel="TRel" and Pred="Pred"]
by auto
subsection ‹Full Abstraction w.r.t. Preorders›
text ‹If there however exists a trans relation Rel that relates source terms and their
literal translations in both directions, then the encoding is fully abstract with respect
to the reduction of Rel to source terms and the reduction of Rel to target terms.›
lemma (in encoding) trans_source_target_relation_impl_full_abstraction:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
assumes enc: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
and trans: "trans Rel"
shows "fully_abstract {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
{(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
proof auto
fix S1 S2
assume "(SourceTerm S1, SourceTerm S2) ∈ Rel"
with enc trans show "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
unfolding trans_def
by blast
next
fix S1 S2
assume "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
with enc trans show "(SourceTerm S1, SourceTerm S2) ∈ Rel"
unfolding trans_def
by blast
qed
lemma (in encoding) source_target_relation_impl_full_abstraction_wrt_trans_closures:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
assumes enc: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
shows "fully_abstract {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel⇧+}
{(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel⇧+}"
proof auto
fix S1 S2
from enc have "(TargetTerm (⟦S1⟧), SourceTerm S1) ∈ Rel⇧+"
by blast
moreover assume "(SourceTerm S1, SourceTerm S2) ∈ Rel⇧+"
ultimately have "(TargetTerm (⟦S1⟧), SourceTerm S2) ∈ Rel⇧+"
by simp
moreover from enc have "(SourceTerm S2, TargetTerm (⟦S2⟧)) ∈ Rel⇧+"
by blast
ultimately show "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel⇧+"
by simp
next
fix S1 S2
from enc have "(SourceTerm S1, TargetTerm (⟦S1⟧)) ∈ Rel⇧+"
by blast
moreover assume "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel⇧+"
ultimately have "(SourceTerm S1, TargetTerm (⟦S2⟧)) ∈ Rel⇧+"
by simp
moreover from enc have "(TargetTerm (⟦S2⟧), SourceTerm S2) ∈ Rel⇧+"
by blast
ultimately show "(SourceTerm S1, SourceTerm S2) ∈ Rel⇧+"
by simp
qed
lemma (in encoding) quasi_trans_source_target_relation_impl_full_abstraction:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
and SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes enc: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
and srel: "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
and trel: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
and trans: "∀P Q R. (P, Q) ∈ Rel ∧ (Q, R) ∈ Rel ∧ ((P ∈ ProcS ∧ Q ∈ ProcT)
∨ (P ∈ ProcT ∧ Q ∈ ProcS)) ⟶ (P, R) ∈ Rel"
shows "fully_abstract SRel TRel"
proof auto
fix S1 S2
from enc have "(TargetTerm (⟦S1⟧), SourceTerm S1) ∈ Rel"
by simp
moreover assume "(S1, S2) ∈ SRel"
with srel have "(SourceTerm S1, SourceTerm S2) ∈ Rel"
by simp
ultimately have "(TargetTerm (⟦S1⟧), SourceTerm S2) ∈ Rel"
using trans
by blast
moreover from enc have "(SourceTerm S2, TargetTerm (⟦S2⟧)) ∈ Rel"
by simp
ultimately have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
using trans
by blast
with trel show "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
by simp
next
fix S1 S2
from enc have "(SourceTerm S1, TargetTerm (⟦S1⟧)) ∈ Rel"
by simp
moreover assume "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
with trel have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
by simp
ultimately have "(SourceTerm S1, TargetTerm (⟦S2⟧)) ∈ Rel"
using trans
by blast
moreover from enc have "(TargetTerm (⟦S2⟧), SourceTerm S2) ∈ Rel"
by simp
ultimately have "(SourceTerm S1, SourceTerm S2) ∈ Rel"
using trans
by blast
with srel show "(S1, S2) ∈ SRel"
by simp
qed
text ‹If an encoding is fully abstract w.r.t. SRel and TRel, then we can conclude from a pair in
indRelRTPO or indRelSTEQ on a pair in TRel and SRel.›
lemma (in encoding) full_abstraction_impl_indRelRSTPO_to_SRel_and_TRel:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and P Q :: "('procS, 'procT) Proc"
assumes fullAbs: "fully_abstract SRel TRel"
and rel: "P ≲⟦⋅⟧R<SRel,TRel> Q"
shows "∀SP SQ. SP ∈S P ∧ SQ ∈S Q ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel⇧+"
and "∀SP TQ. SP ∈S P ∧ TQ ∈T Q ⟶ (⟦SP⟧, TQ) ∈ TRel⇧*"
proof -
have fullAbsT: "∀S1 S2. (S1, S2) ∈ SRel⇧+ ⟶ (⟦S1⟧, ⟦S2⟧) ∈ TRel⇧+"
proof clarify
fix S1 S2
assume "(S1, S2) ∈ SRel⇧+"
thus "(⟦S1⟧, ⟦S2⟧) ∈ TRel⇧+"
proof induct
fix S2
assume "(S1, S2) ∈ SRel"
with fullAbs show "(⟦S1⟧, ⟦S2⟧) ∈ TRel⇧+"
by simp
next
case (step S2 S3)
assume "(⟦S1⟧, ⟦S2⟧) ∈ TRel⇧+"
moreover assume "(S2, S3) ∈ SRel"
with fullAbs have "(⟦S2⟧, ⟦S3⟧) ∈ TRel⇧+"
by simp
ultimately show "(⟦S1⟧, ⟦S3⟧) ∈ TRel⇧+"
by simp
qed
qed
with rel show "∀SP SQ. SP ∈S P ∧ SQ ∈S Q ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel⇧+"
using indRelRSTPO_to_SRel_and_TRel(1)[where SRel="SRel" and TRel="TRel"]
by simp
show "∀SP TQ. SP ∈S P ∧ TQ ∈T Q ⟶ (⟦SP⟧, TQ) ∈ TRel⇧*"
proof clarify
fix SP TQ
assume "SP ∈S P" and "TQ ∈T Q"
with rel obtain S where A1: "(SP, S) ∈ SRel⇧*"
and A2: "(⟦S⟧, TQ) ∈ TRel⇧*"
using indRelRSTPO_to_SRel_and_TRel(2)[where SRel="SRel" and TRel="TRel"]
by blast
from A1 have "SP = S ∨ (SP, S) ∈ SRel⇧+"
using rtrancl_eq_or_trancl[of SP S SRel]
by blast
with fullAbsT have "(⟦SP⟧, ⟦S⟧) ∈ TRel⇧*"
by fast
from this A2 show "(⟦SP⟧, TQ) ∈ TRel⇧*"
by simp
qed
qed
lemma (in encoding) full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and P Q :: "('procS, 'procT) Proc"
assumes fA: "fully_abstract SRel TRel"
and transT: "trans TRel"
and reflS: "refl SRel"
and rel: "P ∼⟦⋅⟧<SRel,TRel> Q"
shows "∀SP SQ. SP ∈S P ∧ SQ ∈S Q ⟶ (SP, SQ) ∈ SRel"
and "∀SP SQ. SP ∈S P ∧ SQ ∈S Q ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel"
and "∀SP TQ. SP ∈S P ∧ TQ ∈T Q ⟶ (⟦SP⟧, TQ) ∈ TRel"
and "∀TP SQ. TP ∈T P ∧ SQ ∈S Q ⟶ (TP, ⟦SQ⟧) ∈ TRel"
and "∀TP TQ. TP ∈T P ∧ TQ ∈T Q ⟶ (TP, TQ) ∈ TRel"
using rel
proof induct
case (encR S)
show "∀SP SQ. SP ∈S SourceTerm S ∧ SQ ∈S TargetTerm (⟦S⟧) ⟶ (SP, SQ) ∈ SRel"
and "∀SP SQ. SP ∈S SourceTerm S ∧ SQ ∈S TargetTerm (⟦S⟧) ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel"
and "∀TP SQ. TP ∈T SourceTerm S ∧ SQ ∈S TargetTerm (⟦S⟧) ⟶ (TP, ⟦SQ⟧) ∈ TRel"
and "∀TP TQ. TP ∈T SourceTerm S ∧ TQ ∈T TargetTerm (⟦S⟧) ⟶ (TP, TQ) ∈ TRel"
by simp+
from reflS fA show "∀SP TQ. SP ∈S SourceTerm S ∧ TQ ∈T TargetTerm (⟦S⟧) ⟶ (⟦SP⟧, TQ) ∈ TRel"
unfolding refl_on_def
by simp
next
case (encL S)
show "∀SP SQ. SP ∈S TargetTerm (⟦S⟧) ∧ SQ ∈S SourceTerm S ⟶ (SP, SQ) ∈ SRel"
and "∀SP SQ. SP ∈S TargetTerm (⟦S⟧) ∧ SQ ∈S SourceTerm S ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel"
and "∀SP TQ. SP ∈S TargetTerm (⟦S⟧) ∧ TQ ∈T SourceTerm S ⟶ (⟦SP⟧, TQ) ∈ TRel"
and "∀TP TQ. TP ∈T TargetTerm (⟦S⟧) ∧ TQ ∈T SourceTerm S ⟶ (TP, TQ) ∈ TRel"
by simp+
with reflS fA show "∀TP SQ. TP ∈T TargetTerm (⟦S⟧) ∧ SQ ∈S SourceTerm S ⟶ (TP, ⟦SQ⟧) ∈ TRel"
unfolding refl_on_def
by simp
next
case (source S1 S2)
show "∀SP TQ. SP ∈S SourceTerm S1 ∧ TQ ∈T SourceTerm S2 ⟶ (⟦SP⟧, TQ) ∈ TRel"
and "∀TP SQ. TP ∈T SourceTerm S1 ∧ SQ ∈S SourceTerm S2 ⟶ (TP, ⟦SQ⟧) ∈ TRel"
and "∀TP TQ. TP ∈T SourceTerm S1 ∧ TQ ∈T SourceTerm S2 ⟶ (TP, TQ) ∈ TRel"
by simp+
assume "(S1, S2) ∈ SRel"
thus "∀SP SQ. SP ∈S SourceTerm S1 ∧ SQ ∈S SourceTerm S2 ⟶ (SP, SQ) ∈ SRel"
by simp
with fA show "∀SP SQ. SP ∈S SourceTerm S1 ∧ SQ ∈S SourceTerm S2 ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by simp
next
case (target T1 T2)
show "∀SP SQ. SP ∈S TargetTerm T1 ∧ SQ ∈S TargetTerm T2 ⟶ (SP, SQ) ∈ SRel"
and "∀SP SQ. SP ∈S TargetTerm T1 ∧ SQ ∈S TargetTerm T2 ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel"
and "∀SP TQ. SP ∈S TargetTerm T1 ∧ TQ ∈T TargetTerm T2 ⟶ (⟦SP⟧, TQ) ∈ TRel"
and "∀TP SQ. TP ∈T TargetTerm T1 ∧ SQ ∈S TargetTerm T2 ⟶ (TP, ⟦SQ⟧) ∈ TRel"
by simp+
assume "(T1, T2) ∈ TRel"
thus "∀TP TQ. TP ∈T TargetTerm T1 ∧ TQ ∈T TargetTerm T2 ⟶ (TP, TQ) ∈ TRel"
by simp
next
case (trans P Q R)
assume A1: "∀SP SQ. SP ∈S P ∧ SQ ∈S Q ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel"
and A2: "∀SP TQ. SP ∈S P ∧ TQ ∈T Q ⟶ (⟦SP⟧, TQ) ∈ TRel"
and A3: "∀TP SQ. TP ∈T P ∧ SQ ∈S Q ⟶ (TP, ⟦SQ⟧) ∈ TRel"
and A4: "∀TP TQ. TP ∈T P ∧ TQ ∈T Q ⟶ (TP, TQ) ∈ TRel"
and A5: "∀SQ SR. SQ ∈S Q ∧ SR ∈S R ⟶ (⟦SQ⟧, ⟦SR⟧) ∈ TRel"
and A6: "∀SQ TR. SQ ∈S Q ∧ TR ∈T R ⟶ (⟦SQ⟧, TR) ∈ TRel"
and A7: "∀TQ SR. TQ ∈T Q ∧ SR ∈S R ⟶ (TQ, ⟦SR⟧) ∈ TRel"
and A8: "∀TQ TR. TQ ∈T Q ∧ TR ∈T R ⟶ (TQ, TR) ∈ TRel"
show "∀SP SR. SP ∈S P ∧ SR ∈S R ⟶ (⟦SP⟧, ⟦SR⟧) ∈ TRel"
proof clarify
fix SP SR
assume A9: "SP ∈S P" and A10: "SR ∈S R"
show "(⟦SP⟧, ⟦SR⟧) ∈ TRel"
proof (cases Q)
case (SourceTerm SQ)
assume A11: "SQ ∈S Q"
with A1 A9 have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by blast
moreover from A5 A10 A11 have "(⟦SQ⟧, ⟦SR⟧) ∈ TRel"
by blast
ultimately show "(⟦SP⟧, ⟦SR⟧) ∈ TRel"
using transT
unfolding trans_def
by blast
next
case (TargetTerm TQ)
assume A11: "TQ ∈T Q"
with A2 A9 have "(⟦SP⟧, TQ) ∈ TRel"
by blast
moreover from A7 A10 A11 have "(TQ, ⟦SR⟧) ∈ TRel"
by blast
ultimately show "(⟦SP⟧, ⟦SR⟧) ∈ TRel"
using transT
unfolding trans_def
by blast
qed
qed
with fA show "∀SP SR. SP ∈S P ∧ SR ∈S R ⟶ (SP, SR) ∈ SRel"
by simp
show "∀SP TR. SP ∈S P ∧ TR ∈T R ⟶ (⟦SP⟧, TR) ∈ TRel"
proof clarify
fix SP TR
assume A9: "SP ∈S P" and A10: "TR ∈T R"
show "(⟦SP⟧, TR) ∈ TRel"
proof (cases Q)
case (SourceTerm SQ)
assume A11: "SQ ∈S Q"
with A1 A9 have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by blast
moreover from A6 A10 A11 have "(⟦SQ⟧, TR) ∈ TRel"
by blast
ultimately show "(⟦SP⟧, TR) ∈ TRel"
using transT
unfolding trans_def
by blast
next
case (TargetTerm TQ)
assume A11: "TQ ∈T Q"
with A2 A9 have "(⟦SP⟧, TQ) ∈ TRel"
by blast
moreover from A8 A10 A11 have "(TQ, TR) ∈ TRel"
by blast
ultimately show "(⟦SP⟧, TR) ∈ TRel"
using transT
unfolding trans_def
by blast
qed
qed
show "∀TP SR. TP ∈T P ∧ SR ∈S R ⟶ (TP, ⟦SR⟧) ∈ TRel"
proof clarify
fix TP SR
assume A9: "TP ∈T P" and A10: "SR ∈S R"
show "(TP, ⟦SR⟧) ∈ TRel"
proof (cases Q)
case (SourceTerm SQ)
assume A11: "SQ ∈S Q"
with A3 A9 have "(TP, ⟦SQ⟧) ∈ TRel"
by blast
moreover from A5 A10 A11 have "(⟦SQ⟧, ⟦SR⟧) ∈ TRel"
by blast
ultimately show "(TP, ⟦SR⟧) ∈ TRel"
using transT
unfolding trans_def
by blast
next
case (TargetTerm TQ)
assume A11: "TQ ∈T Q"
with A4 A9 have "(TP, TQ) ∈ TRel"
by blast
moreover from A7 A10 A11 have "(TQ, ⟦SR⟧) ∈ TRel"
by blast
ultimately show "(TP, ⟦SR⟧) ∈ TRel"
using transT
unfolding trans_def
by blast
qed
qed
show "∀TP TR. TP ∈T P ∧ TR ∈T R ⟶ (TP, TR) ∈ TRel"
proof clarify
fix TP TR
assume A9: "TP ∈T P" and A10: "TR ∈T R"
show "(TP, TR) ∈ TRel"
proof (cases Q)
case (SourceTerm SQ)
assume A11: "SQ ∈S Q"
with A3 A9 have "(TP, ⟦SQ⟧) ∈ TRel"
by blast
moreover from A6 A10 A11 have "(⟦SQ⟧, TR) ∈ TRel"
by blast
ultimately show "(TP, TR) ∈ TRel"
using transT
unfolding trans_def
by blast
next
case (TargetTerm TQ)
assume A11: "TQ ∈T Q"
with A4 A9 have "(TP, TQ) ∈ TRel"
by blast
moreover from A8 A10 A11 have "(TQ, TR) ∈ TRel"
by blast
ultimately show "(TP, TR) ∈ TRel"
using transT
unfolding trans_def
by blast
qed
qed
qed
text ‹If an encoding is fully abstract w.r.t. a preorder SRel on the source and a trans
relation TRel on the target, then there exists a trans relation, namely indRelSTEQ,
that relates source terms and their literal translations in both direction such that its
reductions to source terms is SRel and its reduction to target terms is TRel.›
lemma (in encoding) full_abstraction_wrt_preorders_impl_trans_source_target_relation:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and reflS: "refl SRel"
and transT: "trans TRel"
shows "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ trans Rel"
proof -
have "∀S. SourceTerm S ∼⟦⋅⟧<SRel,TRel> TargetTerm (⟦S⟧)
∧ TargetTerm (⟦S⟧) ∼⟦⋅⟧<SRel,TRel> SourceTerm S"
using indRelSTEQ.encR[where SRel="SRel" and TRel="TRel"]
indRelSTEQ.encL[where SRel="SRel" and TRel="TRel"]
by blast
moreover have "SRel = {(S1, S2). SourceTerm S1 ∼⟦⋅⟧<SRel,TRel> SourceTerm S2}"
proof auto
fix S1 S2
assume "(S1, S2) ∈ SRel"
thus "SourceTerm S1 ∼⟦⋅⟧<SRel,TRel> SourceTerm S2"
by (rule indRelSTEQ.source[where SRel="SRel" and TRel="TRel"])
next
fix S1 S2
assume "SourceTerm S1 ∼⟦⋅⟧<SRel,TRel> SourceTerm S2"
with fullAbs reflS transT show "(S1, S2) ∈ SRel"
using full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel(1)[where SRel="SRel"
and TRel="TRel"]
by blast
qed
moreover have "TRel = {(T1, T2). TargetTerm T1 ∼⟦⋅⟧<SRel,TRel> TargetTerm T2}"
proof auto
fix T1 T2
assume "(T1, T2) ∈ TRel"
thus "TargetTerm T1 ∼⟦⋅⟧<SRel,TRel> TargetTerm T2"
by (rule indRelSTEQ.target[where SRel="SRel" and TRel="TRel"])
next
fix T1 T2
assume "TargetTerm T1 ∼⟦⋅⟧<SRel,TRel> TargetTerm T2"
with fullAbs reflS transT show "(T1, T2) ∈ TRel"
using full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel(5)[where SRel="SRel"
and TRel="TRel"]
by blast
qed
moreover have "trans (indRelSTEQ SRel TRel)"
using indRelSTEQ.trans[where SRel="SRel" and TRel="TRel"]
unfolding trans_def
by blast
ultimately show ?thesis
by blast
qed
text ‹Thus an encoding is fully abstract w.r.t. a preorder SRel on the source and a trans
relation TRel on the target iff there exists a trans relation that relates source
terms and their literal translations in both directions and whose reduction to
source/target terms is SRel/TRel.›
theorem (in encoding) fully_abstract_wrt_preorders_iff_source_target_relation_is_trans:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
shows "(fully_abstract SRel TRel ∧ refl SRel ∧ trans TRel) =
(∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ trans Rel)"
proof (rule iffI)
assume "fully_abstract SRel TRel ∧ refl SRel ∧ trans TRel"
thus "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ trans Rel"
using full_abstraction_wrt_preorders_impl_trans_source_target_relation[where SRel="SRel"
and TRel="TRel"]
by blast
next
assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ trans Rel"
from this obtain Rel
where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
and A2: "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
and A3: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}" and A4: "trans Rel"
by blast
hence "fully_abstract SRel TRel"
using trans_source_target_relation_impl_full_abstraction[where Rel="Rel"]
by blast
moreover have "refl SRel"
unfolding refl_on_def
proof auto
fix S
from A1 have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
by blast
moreover from A1 have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
by blast
ultimately have "(SourceTerm S, SourceTerm S) ∈ Rel"
using A4
unfolding trans_def
by blast
with A2 show "(S, S) ∈ SRel"
by blast
qed
moreover from A3 A4 have "trans TRel"
unfolding trans_def
by blast
ultimately show "fully_abstract SRel TRel ∧ refl SRel ∧ trans TRel"
by blast
qed
subsection ‹Full Abstraction w.r.t. Equivalences›
text ‹If there exists a relation Rel that relates source terms and their literal translations
and whose sym closure is trans, then the encoding is fully abstract with respect
to the reduction of the sym closure of Rel to source/target terms.›
lemma (in encoding) source_target_relation_with_trans_symcl_impl_full_abstraction:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
assumes enc: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and trans: "trans (symcl Rel)"
shows "fully_abstract {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
{(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}"
proof auto
fix S1 S2
from enc have "(TargetTerm (⟦S1⟧), SourceTerm S1) ∈ symcl Rel"
by (simp add: symcl_def)
moreover assume "(SourceTerm S1, SourceTerm S2) ∈ symcl Rel"
moreover from enc have "(SourceTerm S2, TargetTerm (⟦S2⟧)) ∈ symcl Rel"
by (simp add: symcl_def)
ultimately show "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ symcl Rel"
using trans
unfolding trans_def
by blast
next
fix S1 S2
from enc have "(SourceTerm S1, TargetTerm (⟦S1⟧)) ∈ symcl Rel"
by (simp add: symcl_def)
moreover assume "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ symcl Rel"
moreover from enc have "(TargetTerm (⟦S2⟧), SourceTerm S2) ∈ symcl Rel"
by (simp add: symcl_def)
ultimately show "(SourceTerm S1, SourceTerm S2) ∈ symcl Rel"
using trans
unfolding trans_def
by blast
qed
text ‹If an encoding is fully abstract w.r.t. the equivalences SRel and TRel, then there exists a
preorder, namely indRelRSTPO, that relates source terms and their literal translations such
that its reductions to source terms is SRel and its reduction to target terms is TRel.›
lemma (in encoding) fully_abstract_wrt_equivalences_impl_symcl_source_target_relation_is_preorder:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and reflT: "refl TRel"
and symmT: "sym TRel"
and transT: "trans TRel"
shows "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}
∧ preorder (symcl Rel)"
proof -
from fullAbs reflT have reflS: "refl SRel"
unfolding refl_on_def
by auto
from fullAbs symmT have symmS: "sym SRel"
unfolding sym_def
by auto
from fullAbs transT have transS: "trans SRel"
unfolding trans_def
by blast
have "∀S. SourceTerm S ≲⟦⋅⟧R<SRel,TRel> TargetTerm (⟦S⟧)"
using indRelRSTPO.encR[where SRel="SRel" and TRel="TRel"]
by blast
moreover
have "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl (indRelRSTPO SRel TRel)}"
proof auto
fix S1 S2
assume "(S1, S2) ∈ SRel"
thus "(SourceTerm S1, SourceTerm S2) ∈ symcl (indRelRSTPO SRel TRel)"
by (simp add: symcl_def indRelRSTPO.source[where SRel="SRel" and TRel="TRel"])
next
fix S1 S2
assume "(SourceTerm S1, SourceTerm S2) ∈ symcl (indRelRSTPO SRel TRel)"
moreover from transS
have "SourceTerm S1 ≲⟦⋅⟧R<SRel,TRel> SourceTerm S2 ⟹ (S1, S2) ∈ SRel"
using indRelRSTPO_to_SRel_and_TRel(1)[where SRel="SRel" and TRel="TRel"]
trancl_id[of SRel]
by blast
moreover from symmS transS
have "SourceTerm S2 ≲⟦⋅⟧R<SRel,TRel> SourceTerm S1 ⟹ (S1, S2) ∈ SRel"
using indRelRSTPO_to_SRel_and_TRel(1)[where SRel="SRel" and TRel="TRel"]
trancl_id[of SRel]
unfolding sym_def
by blast
ultimately show "(S1, S2) ∈ SRel"
by (auto simp add: symcl_def)
qed
moreover
have "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl (indRelRSTPO SRel TRel)}"
proof auto
fix T1 T2
assume "(T1, T2) ∈ TRel"
thus "(TargetTerm T1, TargetTerm T2) ∈ symcl (indRelRSTPO SRel TRel)"
by (simp add: symcl_def indRelRSTPO.target[where SRel="SRel" and TRel="TRel"])
next
fix T1 T2
assume "(TargetTerm T1, TargetTerm T2) ∈ symcl (indRelRSTPO SRel TRel)"
moreover from transT
have "TargetTerm T1 ≲⟦⋅⟧R<SRel,TRel> TargetTerm T2 ⟹ (T1, T2) ∈ TRel"
using indRelRSTPO_to_SRel_and_TRel(4)[where SRel="SRel" and TRel="TRel"]
trancl_id[of TRel]
by blast
moreover from symmT transT
have "TargetTerm T2 ≲⟦⋅⟧R<SRel,TRel> TargetTerm T1 ⟹ (T1, T2) ∈ TRel"
using indRelRSTPO_to_SRel_and_TRel(4)[where SRel="SRel" and TRel="TRel"]
trancl_id[of TRel]
unfolding sym_def
by blast
ultimately show "(T1, T2) ∈ TRel"
by (auto simp add: symcl_def)
qed
moreover have "refl (symcl (indRelRSTPO SRel TRel))"
unfolding refl_on_def
proof auto
fix P
show "(P, P) ∈ symcl (indRelRSTPO SRel TRel)"
proof (cases P)
case (SourceTerm SP)
assume "SP ∈S P"
with reflS show "(P, P) ∈ symcl (indRelRSTPO SRel TRel)"
unfolding refl_on_def
by (simp add: symcl_def indRelRSTPO.source)
next
case (TargetTerm TP)
assume "TP ∈T P"
with reflT show "(P, P) ∈ symcl (indRelRSTPO SRel TRel)"
unfolding refl_on_def
by (simp add: symcl_def indRelRSTPO.target)
qed
qed
moreover have "trans (symcl (indRelRSTPO SRel TRel))"
proof -
have "∀P Q R. P ≲⟦⋅⟧R<SRel,TRel> Q ∧ R ≲⟦⋅⟧R<SRel,TRel> Q ∧ (P, R) ∉ (indRelRSTPO SRel TRel)
⟶ Q ≲⟦⋅⟧R<SRel,TRel> P ∨ Q ≲⟦⋅⟧R<SRel,TRel> R"
proof clarify
fix P Q R
assume A1: "P ≲⟦⋅⟧R<SRel,TRel> Q" and A2: "R ≲⟦⋅⟧R<SRel,TRel> Q"
and A3: "(P, R) ∉ (indRelRSTPO SRel TRel)" and A4: "(Q, R) ∉ (indRelRSTPO SRel TRel)"
show "Q ≲⟦⋅⟧R<SRel,TRel> P"
proof (cases P)
case (SourceTerm SP)
assume A5: "SP ∈S P"
show "Q ≲⟦⋅⟧R<SRel,TRel> P"
proof (cases Q)
case (SourceTerm SQ)
assume A6: "SQ ∈S Q"
with transS A1 A5 have "(SP, SQ) ∈ SRel"
using indRelRSTPO_to_SRel_and_TRel(1)[where SRel="SRel" and TRel="TRel"]
trancl_id[of SRel]
by blast
with symmS A5 A6 show "Q ≲⟦⋅⟧R<SRel,TRel> P"
unfolding sym_def
by (simp add: indRelRSTPO.source)
next
case (TargetTerm TQ)
assume A6: "TQ ∈T Q"
show "Q ≲⟦⋅⟧R<SRel,TRel> P"
proof (cases R)
case (SourceTerm SR)
assume A7: "SR ∈S R"
with fullAbs A2 A6 have "(⟦SR⟧, TQ) ∈ TRel⇧*"
using full_abstraction_impl_indRelRSTPO_to_SRel_and_TRel(2)[where SRel="SRel"
and TRel="TRel"] trancl_id[of "TRel⇧="] reflcl_of_refl_rel[of TRel]
trancl_reflcl[of TRel]
unfolding trans_def
by blast
with transT reflT have "(⟦SR⟧, TQ) ∈ TRel"
using trancl_id[of "TRel⇧="] reflcl_of_refl_rel[of TRel] trancl_reflcl[of TRel]
by auto
with symmT have "(TQ, ⟦SR⟧) ∈ TRel"
unfolding sym_def
by simp
moreover from fullAbs A1 A5 A6 have "(⟦SP⟧, TQ) ∈ TRel⇧*"
using full_abstraction_impl_indRelRSTPO_to_SRel_and_TRel(2)[where SRel="SRel"
and TRel="TRel"]
unfolding trans_def
by blast
with transT reflT have "(⟦SP⟧, TQ) ∈ TRel"
using trancl_id[of "TRel⇧="] reflcl_of_refl_rel[of TRel] trancl_reflcl[of TRel]
by auto
ultimately have "(⟦SP⟧, ⟦SR⟧) ∈ TRel"
using transT
unfolding trans_def
by blast
with fullAbs have "(SP, SR) ∈ SRel"
by simp
with A3 A5 A7 show ?thesis
by (simp add: indRelRSTPO.source)
next
case (TargetTerm TR)
assume A7: "TR ∈T R"
with transT A2 A6 have "(TR, TQ) ∈ TRel"
using indRelRSTPO_to_SRel_and_TRel(4)[where SRel="SRel" and TRel="TRel"]
trancl_id[of "TRel"]
by blast
with symmT have "(TQ, TR) ∈ TRel"
unfolding sym_def
by simp
with A4 A6 A7 show ?thesis
by (simp add: indRelRSTPO.target)
qed
qed
next
case (TargetTerm TP)
assume A5: "TP ∈T P"
show "Q ≲⟦⋅⟧R<SRel,TRel> P"
proof (cases Q)
case (SourceTerm SQ)
assume "SQ ∈S Q"
with A1 A5 show ?thesis
using indRelRSTPO_to_SRel_and_TRel(3)[where SRel="SRel" and TRel="TRel"]
by blast
next
case (TargetTerm TQ)
assume A6: "TQ ∈T Q"
with transT A1 A5 have "(TP, TQ) ∈ TRel"
using indRelRSTPO_to_SRel_and_TRel(4)[where SRel="SRel" and TRel="TRel"]
trancl_id[of "TRel"]
by blast
with symmT have "(TQ, TP) ∈ TRel"
unfolding sym_def
by simp
with A5 A6 show "Q ≲⟦⋅⟧R<SRel,TRel> P"
by (simp add: indRelRSTPO.target)
qed
qed
qed
moreover
have "∀P Q R. P ≲⟦⋅⟧R<SRel,TRel> Q ∧ P ≲⟦⋅⟧R<SRel,TRel> R ∧ (Q, R) ∉ (indRelRSTPO SRel TRel)
⟶ Q ≲⟦⋅⟧R<SRel,TRel> P ∨ R ≲⟦⋅⟧R<SRel,TRel> P"
proof clarify
fix P Q R
assume A1: "P ≲⟦⋅⟧R<SRel,TRel> Q" and A2: "P ≲⟦⋅⟧R<SRel,TRel> R"
and A3: "(Q, R) ∉ (indRelRSTPO SRel TRel)" and A4: "(R, P) ∉ (indRelRSTPO SRel TRel)"
show "Q ≲⟦⋅⟧R<SRel,TRel> P"
proof (cases P)
case (SourceTerm SP)
assume A5: "SP ∈S P"
show "Q ≲⟦⋅⟧R<SRel,TRel> P"
proof (cases Q)
case (SourceTerm SQ)
assume A6: "SQ ∈S Q"
with transS A1 A5 have "(SP, SQ) ∈ SRel"
using indRelRSTPO_to_SRel_and_TRel(1)[where SRel="SRel" and TRel="TRel"]
trancl_id[of "SRel"]
by blast
with symmS A5 A6 show "Q ≲⟦⋅⟧R<SRel,TRel> P"
unfolding sym_def
by (simp add: indRelRSTPO.source)
next
case (TargetTerm TQ)
assume A6: "TQ ∈T Q"
show "Q ≲⟦⋅⟧R<SRel,TRel> P"
proof (cases R)
case (SourceTerm SR)
assume A7: "SR ∈S R"
with transS A2 A5 have "(SP, SR) ∈ SRel"
using indRelRSTPO_to_SRel_and_TRel(1)[where SRel="SRel" and TRel="TRel"]
trancl_id[of "SRel"]
by blast
with symmS have "(SR, SP) ∈ SRel"
unfolding sym_def
by simp
with A4 A5 A7 show ?thesis
by (simp add: indRelRSTPO.source)
next
case (TargetTerm TR)
from fullAbs A1 A5 A6 have "(⟦SP⟧, TQ) ∈ TRel⇧*"
using full_abstraction_impl_indRelRSTPO_to_SRel_and_TRel(2)[where SRel="SRel" and
TRel="TRel"]
unfolding trans_def
by blast
with transT reflT have "(⟦SP⟧, TQ) ∈ TRel"
using trancl_id[of "TRel⇧="] reflcl_of_refl_rel[of TRel] trancl_reflcl[of TRel]
by auto
with symmT have "(TQ, ⟦SP⟧) ∈ TRel"
unfolding sym_def
by simp
moreover assume A7: "TR ∈T R"
with fullAbs A2 A5 have "(⟦SP⟧, TR) ∈ TRel⇧*"
using full_abstraction_impl_indRelRSTPO_to_SRel_and_TRel(2)[where SRel="SRel" and
TRel="TRel"]
unfolding trans_def
by blast
with transT reflT have "(⟦SP⟧, TR) ∈ TRel"
using trancl_id[of "TRel⇧="] reflcl_of_refl_rel[of TRel] trancl_reflcl[of TRel]
by auto
ultimately have "(TQ, TR) ∈ TRel"
using transT
unfolding trans_def
by blast
with A3 A6 A7 show ?thesis
by (simp add: indRelRSTPO.target)
qed
qed
next
case (TargetTerm TP)
assume A5: "TP ∈T P"
show "Q ≲⟦⋅⟧R<SRel,TRel> P"
proof (cases Q)
case (SourceTerm SQ)
assume "SQ ∈S Q"
with A1 A5 show ?thesis
using indRelRSTPO_to_SRel_and_TRel(3)[where SRel="SRel" and TRel="TRel"]
by blast
next
case (TargetTerm TQ)
assume A6: "TQ ∈T Q"
with transT A1 A5 have "(TP, TQ) ∈ TRel"
using indRelRSTPO_to_SRel_and_TRel(4)[where SRel="SRel" and TRel="TRel"]
trancl_id[of "TRel"]
by blast
with symmT have "(TQ, TP) ∈ TRel"
unfolding sym_def
by simp
with A5 A6 show "Q ≲⟦⋅⟧R<SRel,TRel> P"
by (simp add: indRelRSTPO.target)
qed
qed
qed
moreover from reflS reflT have "refl (indRelRSTPO SRel TRel)"
using indRelRSTPO_refl[where SRel="SRel" and TRel="TRel"]
by blast
moreover have "trans (indRelRSTPO SRel TRel)"
using indRelRSTPO.trans[where SRel="SRel" and TRel="TRel"]
unfolding trans_def
by blast
ultimately show "trans (symcl (indRelRSTPO SRel TRel))"
using symm_closure_of_preorder_is_trans[where Rel="indRelRSTPO SRel TRel"]
by blast
qed
ultimately show ?thesis
unfolding preorder_on_def
by blast
qed
lemma (in encoding) fully_abstract_impl_symcl_source_target_relation_is_preorder:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract ((symcl (SRel⇧=))⇧+) ((symcl (TRel⇧=))⇧+)"
shows "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ ((symcl (SRel⇧=))⇧+) = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
∧ ((symcl (TRel⇧=))⇧+) = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}
∧ preorder (symcl Rel)"
proof -
have "refl ((symcl (TRel⇧=))⇧+)"
using refl_symm_trans_closure_is_symm_refl_trans_closure[of TRel]
refl_rtrancl[of TRel]
unfolding sym_def refl_on_def
by auto
moreover have "sym ((symcl (TRel⇧=))⇧+)"
using sym_symcl[of "TRel⇧="] sym_trancl[of "symcl (TRel⇧=)"]
by simp
moreover have "trans ((symcl (TRel⇧=))⇧+)"
by simp
ultimately show ?thesis
using fully_abstract_wrt_equivalences_impl_symcl_source_target_relation_is_preorder[where
SRel="(symcl (SRel⇧=))⇧+" and TRel="(symcl (TRel⇧=))⇧+"] fullAbs
refl_symm_closure_is_symm_refl_closure
unfolding preorder_on_def
by blast
qed
lemma (in encoding) fully_abstract_wrt_preorders_impl_source_target_relation_is_trans:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
shows "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ ((refl SRel ∧ trans TRel)
⟷ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}))"
proof -
define Rel where "Rel = (indRelSTEQ SRel TRel) - ({(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}
∪ {(P, Q). ∃S1 S2. S1 ∈S P ∧ S2 ∈S Q ∧ (S1, S2) ∉ SRel}
∪ {(P, Q). ∃T1 T2. T1 ∈T P ∧ T2 ∈T Q ∧ (T1, T2) ∉ TRel})"
from Rel_def have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
by (simp add: indRelSTEQ.encR[where SRel="SRel" and TRel="TRel"])
moreover from Rel_def have "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
proof auto
fix S1 S2
assume "(S1, S2) ∈ SRel"
thus "SourceTerm S1 ∼⟦⋅⟧<SRel,TRel> SourceTerm S2"
by (simp add: indRelSTEQ.source[where SRel="SRel" and TRel="TRel"])
qed
moreover from Rel_def have "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
proof auto
fix T1 T2
assume "(T1, T2) ∈ TRel"
thus "TargetTerm T1 ∼⟦⋅⟧<SRel,TRel> TargetTerm T2"
by (simp add: indRelSTEQ.target[where SRel="SRel" and TRel="TRel"])
qed
moreover
have "(refl SRel ∧ trans TRel) ⟷ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
proof (rule iffI, erule conjE)
assume reflS: "refl SRel" and transT: "trans TRel"
have "Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} = indRelSTEQ SRel TRel"
proof (auto simp add: Rel_def)
fix S
show "TargetTerm (⟦S⟧) ∼⟦⋅⟧<SRel,TRel> SourceTerm S"
by (rule indRelSTEQ.encL)
next
fix S1 S2
assume "SourceTerm S1 ∼⟦⋅⟧<SRel,TRel> SourceTerm S2"
with fullAbs reflS transT have "(S1, S2) ∈ SRel"
using full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel(1)[where
SRel="SRel" and TRel="TRel"]
by blast
moreover assume "(S1, S2) ∉ SRel"
ultimately show False
by simp
next
fix T1 T2
assume "TargetTerm T1 ∼⟦⋅⟧<SRel,TRel> TargetTerm T2"
with fullAbs reflS transT have "(T1, T2) ∈ TRel"
using full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel(5)[where
SRel="SRel" and TRel="TRel"]
by blast
moreover assume "(T1, T2) ∉ TRel"
ultimately show False
by simp
qed
thus "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
using indRelSTEQ_trans[where SRel="SRel" and TRel="TRel"]
unfolding trans_def
by blast
next
assume transR: "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
show "refl SRel ∧ trans TRel"
unfolding trans_def refl_on_def
proof auto
fix S
from Rel_def have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
by (simp add: indRelSTEQ.encR)
moreover have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
by simp
ultimately have "(SourceTerm S, SourceTerm S) ∈ Rel"
using transR
unfolding trans_def
by blast
with Rel_def show "(S, S) ∈ SRel"
by simp
next
fix TP TQ TR
assume "(TP, TQ) ∈ TRel"
with Rel_def have "(TargetTerm TP, TargetTerm TQ) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
by (simp add: indRelSTEQ.target)
moreover assume "(TQ, TR) ∈ TRel"
with Rel_def have "(TargetTerm TQ, TargetTerm TR) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
by (simp add: indRelSTEQ.target)
ultimately have "(TargetTerm TP, TargetTerm TR) ∈ Rel"
using transR
unfolding trans_def
by blast
with Rel_def show "(TP, TR) ∈ TRel"
by simp
qed
qed
ultimately show ?thesis
by blast
qed
lemma (in encoding) fully_abstract_wrt_preorders_impl_source_target_relation_is_trans_B:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes fullAbs: "fully_abstract SRel TRel"
and reflT: "refl TRel"
and transT: "trans TRel"
shows "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
proof -
define Rel where "Rel = (indRelSTEQ SRel TRel) - {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
from fullAbs reflT have reflS: "refl SRel"
unfolding refl_on_def
by auto
from Rel_def have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
by (simp add: indRelSTEQ.encR[where SRel="SRel" and TRel="TRel"])
moreover from Rel_def have "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
proof auto
fix S1 S2
assume "(S1, S2) ∈ SRel"
thus "SourceTerm S1 ∼⟦⋅⟧<SRel,TRel> SourceTerm S2"
by (simp add: indRelSTEQ.source[where SRel="SRel" and TRel="TRel"])
next
fix S1 S2
assume "SourceTerm S1 ∼⟦⋅⟧<SRel,TRel> SourceTerm S2"
with fullAbs transT reflS show "(S1, S2) ∈ SRel"
using full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel(1)[where SRel="SRel"
and TRel="TRel"]
by blast
qed
moreover from Rel_def have "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
proof auto
fix T1 T2
assume "(T1, T2) ∈ TRel"
thus "TargetTerm T1 ∼⟦⋅⟧<SRel,TRel> TargetTerm T2"
by (simp add: indRelSTEQ.target[where SRel="SRel" and TRel="TRel"])
next
fix T1 T2
assume "TargetTerm T1 ∼⟦⋅⟧<SRel,TRel> TargetTerm T2"
with fullAbs transT reflS show "(T1, T2) ∈ TRel"
using full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel(5)[where SRel="SRel"
and TRel="TRel"]
by blast
qed
moreover from Rel_def have "Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} = indRelSTEQ SRel TRel"
by (auto simp add: indRelSTEQ.encL)
hence "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
using indRelSTEQ.trans[where SRel="SRel" and TRel="TRel"]
unfolding trans_def
by auto
ultimately show ?thesis
by blast
qed
text ‹Thus an encoding is fully abstract w.r.t. an equivalence SRel on the source and an
equivalence TRel on the target iff there exists a relation that relates source terms and
their literal translations, whose sym closure is a preorder such that the reduction
of this sym closure to source/target terms is SRel/TRel.›
lemma (in encoding) fully_abstract_wrt_equivalences_iff_symcl_source_target_relation_is_preorder:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
shows "(fully_abstract SRel TRel ∧ equivalence TRel) =
(∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}
∧ preorder (symcl Rel))"
proof (rule iffI)
assume "fully_abstract SRel TRel ∧ equivalence TRel"
thus "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}
∧ preorder (symcl Rel)"
using fully_abstract_wrt_equivalences_impl_symcl_source_target_relation_is_preorder[where
SRel="SRel" and TRel="TRel"]
unfolding equiv_def
by blast
next
assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}
∧ preorder (symcl Rel)"
from this obtain Rel
where "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}"
and A1: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}"
and A2: "preorder (symcl Rel)"
by blast
hence A5: "fully_abstract SRel TRel"
using source_target_relation_with_trans_symcl_impl_full_abstraction[where Rel="Rel"]
unfolding preorder_on_def
by blast
moreover have "equivalence TRel"
unfolding trans_def equiv_def sym_def refl_on_def
proof auto
fix T
from A1 A2 show "(T, T) ∈ TRel"
unfolding preorder_on_def refl_on_def
by blast
next
fix T1 T2
assume "(T1, T2) ∈ TRel"
with A1 show "(T2, T1) ∈ TRel"
by (auto simp add: symcl_def)
next
fix T1 T2 T3
assume "(T1, T2) ∈ TRel" and "(T2, T3) ∈ TRel"
with A1 A2 show "(T1, T3) ∈ TRel"
unfolding trans_def preorder_on_def
by blast
qed
ultimately show "fully_abstract SRel TRel ∧ equivalence TRel"
by blast
qed
lemma (in encoding) fully_abstract_iff_symcl_source_target_relation_is_preorder:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
shows "fully_abstract ((symcl (SRel⇧=))⇧+) ((symcl (TRel⇧=))⇧+) =
(∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ (symcl (SRel⇧=))⇧+ = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
∧ (symcl (TRel⇧=))⇧+ = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}
∧ preorder (symcl Rel))"
proof (rule iffI)
assume "fully_abstract ((symcl (SRel⇧=))⇧+) ((symcl (TRel⇧=))⇧+)"
thus "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ (symcl (SRel⇧=))⇧+ = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
∧ (symcl (TRel⇧=))⇧+ = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}
∧ preorder (symcl Rel)"
using fully_abstract_impl_symcl_source_target_relation_is_preorder[where SRel="SRel" and
TRel="TRel"]
by blast
next
assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ (symcl (SRel⇧=))⇧+ = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}
∧ (symcl (TRel⇧=))⇧+ = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}
∧ preorder (symcl Rel)"
from this obtain Rel
where "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and "(symcl (SRel⇧=))⇧+ = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ symcl Rel}"
and A1: "(symcl (TRel⇧=))⇧+ = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ symcl Rel}"
and A2: "preorder (symcl Rel)"
by blast
thus "fully_abstract ((symcl (SRel⇧=))⇧+) ((symcl (TRel⇧=))⇧+)"
using source_target_relation_with_trans_symcl_impl_full_abstraction[where Rel="Rel"]
unfolding preorder_on_def
by blast
qed
subsection ‹Full Abstraction without Relating Translations to their Source Terms›
text ‹Let Rel be the result of removing from indRelSTEQ all pairs of two source or two target
terms that are not contained in SRel or TRel. Then a fully abstract encoding ensures that
Rel is trans iff SRel is refl and TRel is trans.›
lemma (in encoding) full_abstraction_impl_indRelSTEQ_is_trans:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
and Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
assumes fullAbs: "fully_abstract SRel TRel"
and rel: "Rel = ((indRelSTEQ SRel TRel)
- {(P, Q). (P ∈ ProcS ∧ Q ∈ ProcS) ∨ (P ∈ ProcT ∧ Q ∈ ProcT)})
∪ {(P, Q). (∃SP SQ. SP ∈S P ∧ SQ ∈S Q ∧ (SP, SQ) ∈ SRel)
∨ (∃TP TQ. TP ∈T P ∧ TQ ∈T Q ∧ (TP, TQ) ∈ TRel)}"
shows "(refl SRel ∧ trans TRel) = trans Rel"
unfolding trans_def
proof auto
fix P Q R
assume A1: "refl SRel" and A2: "∀x y. (x, y) ∈ TRel ⟶ (∀z. (y, z) ∈ TRel ⟶ (x, z) ∈ TRel)"
and A3: "(P, Q) ∈ Rel" and A4: "(Q, R) ∈ Rel"
from fullAbs rel have A5: "∀SP SQ. (SourceTerm SP, SourceTerm SQ) ∈ Rel ⟶ (⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by simp
from rel have A6: "∀TP TQ. (TargetTerm TP, TargetTerm TQ) ∈ Rel ⟶ (TP, TQ) ∈ TRel"
by simp
have A7: "∀SP TQ. (SourceTerm SP, TargetTerm TQ) ∈ Rel ⟶ (⟦SP⟧, TQ) ∈ TRel"
proof clarify
fix SP TQ
assume "(SourceTerm SP, TargetTerm TQ) ∈ Rel"
with rel have "SourceTerm SP ∼⟦⋅⟧<SRel,TRel> TargetTerm TQ"
by simp
with A1 A2 fullAbs show "(⟦SP⟧, TQ) ∈ TRel"
using full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel(3)[where
SRel="SRel" and TRel="TRel"]
unfolding trans_def
by blast
qed
have A8: "∀TP SQ. (TargetTerm TP, SourceTerm SQ) ∈ Rel ⟶ (TP, ⟦SQ⟧) ∈ TRel"
proof clarify
fix TP SQ
assume "(TargetTerm TP, SourceTerm SQ) ∈ Rel"
with rel have "TargetTerm TP ∼⟦⋅⟧<SRel,TRel> SourceTerm SQ"
by simp
with A1 A2 fullAbs show "(TP, ⟦SQ⟧) ∈ TRel"
using full_abstraction_wrt_preorders_impl_indRelSTEQ_to_SRel_and_TRel(4)[where
SRel="SRel" and TRel="TRel"]
unfolding trans_def
by blast
qed
show "(P, R) ∈ Rel"
proof (cases P)
case (SourceTerm SP)
assume A9: "SP ∈S P"
show "(P, R) ∈ Rel"
proof (cases Q)
case (SourceTerm SQ)
assume A10: "SQ ∈S Q"
with A3 A5 A9 have A11: "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
by simp
show "(P, R) ∈ Rel"
proof (cases R)
case (SourceTerm SR)
assume A12: "SR ∈S R"
with A4 A5 A10 have "(⟦SQ⟧, ⟦SR⟧) ∈ TRel"
by simp
with A2 A11 have "(⟦SP⟧, ⟦SR⟧) ∈ TRel"
by blast
with fullAbs have "(SP, SR) ∈ SRel"
by simp
with rel A9 A12 show "(P, R) ∈ Rel"
by simp
next
case (TargetTerm TR)
assume A12: "TR ∈T R"
from A9 have "P ∼⟦⋅⟧<SRel,TRel> TargetTerm (⟦SP⟧)"
by (simp add: indRelSTEQ.encR)
moreover from A4 A7 A10 A12 have "(⟦SQ⟧, TR) ∈ TRel"
by simp
with A2 A11 have "(⟦SP⟧, TR) ∈ TRel"
by blast
with A12 have "TargetTerm (⟦SP⟧) ∼⟦⋅⟧<SRel,TRel> R"
by (simp add: indRelSTEQ.target)
ultimately have "P ∼⟦⋅⟧<SRel, TRel> R"
by (rule indRelSTEQ.trans)
with rel A9 A12 show "(P, R) ∈ Rel"
by simp
qed
next
case (TargetTerm TQ)
assume A10: "TQ ∈T Q"
with A3 A7 A9 have A11: "(⟦SP⟧, TQ) ∈ TRel"
by simp
show "(P, R) ∈ Rel"
proof (cases R)
case (SourceTerm SR)
assume A12: "SR ∈S R"
with A4 A8 A10 have "(TQ, ⟦SR⟧) ∈ TRel"
by simp
with A2 A11 have "(⟦SP⟧, ⟦SR⟧) ∈ TRel"
by blast
with fullAbs have "(SP, SR) ∈ SRel"
by simp
with rel A9 A12 show "(P, R) ∈ Rel"
by simp
next
case (TargetTerm TR)
assume A12: "TR ∈T R"
from A9 have "P ∼⟦⋅⟧<SRel,TRel> TargetTerm (⟦SP⟧)"
by (simp add: indRelSTEQ.encR)
moreover from A4 A6 A10 A12 have "(TQ, TR) ∈ TRel"
by simp
with A2 A11 have "(⟦SP⟧, TR) ∈ TRel"
by blast
with A12 have "TargetTerm (⟦SP⟧) ∼⟦⋅⟧<SRel,TRel> R"
by (simp add: indRelSTEQ.target)
ultimately have "P ∼⟦⋅⟧<SRel,TRel> R"
by (rule indRelSTEQ.trans)
with A9 A12 rel show "(P, R) ∈ Rel"
by simp
qed
qed
next
case (TargetTerm TP)
assume A9: "TP ∈T P"
show "(P, R) ∈ Rel"
proof (cases Q)
case (SourceTerm SQ)
assume A10: "SQ ∈S Q"
with A3 A8 A9 have A11: "(TP, ⟦SQ⟧) ∈ TRel"
by simp
show "(P, R) ∈ Rel"
proof (cases R)
case (SourceTerm SR)
assume A12: "SR ∈S R"
with A4 A5 A10 have "(⟦SQ⟧, ⟦SR⟧) ∈ TRel"
by simp
with A2 A11 have "(TP, ⟦SR⟧) ∈ TRel"
by blast
with A9 have "P ∼⟦⋅⟧<SRel,TRel> TargetTerm (⟦SR⟧)"
by (simp add: indRelSTEQ.target)
moreover from A12 have "TargetTerm (⟦SR⟧) ∼⟦⋅⟧<SRel,TRel> R"
by (simp add: indRelSTEQ.encL)
ultimately have "P ∼⟦⋅⟧<SRel,TRel> R"
by (rule indRelSTEQ.trans)
with rel A9 A12 show "(P, R) ∈ Rel"
by simp
next
case (TargetTerm TR)
assume A12: "TR ∈T R"
with A4 A7 A10 have "(⟦SQ⟧, TR) ∈ TRel"
by simp
with A2 A11 have "(TP, TR) ∈ TRel"
by blast
with rel A9 A12 show "(P, R) ∈ Rel"
by simp
qed
next
case (TargetTerm TQ)
assume A10: "TQ ∈T Q"
with A3 A6 A9 have A11: "(TP, TQ) ∈ TRel"
by simp
show "(P, R) ∈ Rel"
proof (cases R)
case (SourceTerm SR)
assume A12: "SR ∈S R"
with A4 A8 A10 have "(TQ, ⟦SR⟧) ∈ TRel"
by simp
with A2 A11 have "(TP, ⟦SR⟧) ∈ TRel"
by blast
with A9 have "P ∼⟦⋅⟧<SRel,TRel> TargetTerm (⟦SR⟧)"
by (simp add: indRelSTEQ.target)
moreover from A12 have "TargetTerm (⟦SR⟧) ∼⟦⋅⟧<SRel,TRel> R"
by (simp add: indRelSTEQ.encL)
ultimately have "P ∼⟦⋅⟧<SRel,TRel> R"
by (rule indRelSTEQ.trans)
with rel A9 A12 show "(P, R) ∈ Rel"
by simp
next
case (TargetTerm TR)
assume A12: "TR ∈T R"
with A4 A6 A10 have "(TQ, TR) ∈ TRel"
by simp
with A2 A11 have "(TP, TR) ∈ TRel"
by blast
with A9 A12 rel show "(P, R) ∈ Rel"
by simp
qed
qed
qed
next
assume B: "∀x y. (x, y) ∈ Rel ⟶ (∀z. (y, z) ∈ Rel ⟶ (x, z) ∈ Rel)"
thus "refl SRel"
unfolding refl_on_def
proof auto
fix S
from rel have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
by (simp add: indRelSTEQ.encR)
moreover from rel have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
by (simp add: indRelSTEQ.encL)
ultimately have "(SourceTerm S, SourceTerm S) ∈ Rel"
using B
by blast
with rel show "(S, S) ∈ SRel"
by simp
qed
next
fix TP TQ TR
assume "∀x y. (x, y) ∈ Rel ⟶ (∀z. (y, z) ∈ Rel ⟶ (x, z) ∈ Rel)"
moreover assume "(TP, TQ) ∈ TRel"
with rel have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
by simp
moreover assume "(TQ, TR) ∈ TRel"
with rel have "(TargetTerm TQ, TargetTerm TR) ∈ Rel"
by simp
ultimately have "(TargetTerm TP, TargetTerm TR) ∈ Rel"
by blast
with rel show "(TP, TR) ∈ TRel"
by simp
qed
text ‹Whenever an encoding induces a trans relation that includes SRel and TRel and relates
source terms to their literal translations in both directions, the encoding is fully
abstract w.r.t. SRel and TRel.›
lemma (in encoding) trans_source_target_relation_impl_fully_abstract:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
and SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes enc: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
and srel: "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
and trel: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
and trans: "trans Rel"
shows "fully_abstract SRel TRel"
proof auto
fix S1 S2
assume "(S1, S2) ∈ SRel"
with srel have "(SourceTerm S1, SourceTerm S2) ∈ Rel"
by simp
with enc trans have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
unfolding trans_def
by blast
with trel show "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
by simp
next
fix S1 S2
assume "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
with trel have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
by simp
with enc trans have "(SourceTerm S1, SourceTerm S2) ∈ Rel"
unfolding trans_def
by blast
with srel show "(S1, S2) ∈ SRel"
by simp
qed
text ‹Assume TRel is a preorder. Then an encoding is fully abstract w.r.t. SRel and TRel iff
there exists a relation that relates add least all source terms to their literal
translations, includes SRel and TRel, and whose union with the relation that relates
exactly all literal translations to their source terms is trans.›
lemma (in encoding) source_target_relation_with_trans_impl_full_abstraction:
fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
assumes enc: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and trans: "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
shows "fully_abstract {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
{(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
proof auto
fix S1 S2
define Rel' where "Rel' = Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
from Rel'_def have "(TargetTerm (⟦S1⟧), SourceTerm S1) ∈ Rel'"
by simp
moreover assume "(SourceTerm S1, SourceTerm S2) ∈ Rel"
with Rel'_def have "(SourceTerm S1, SourceTerm S2) ∈ Rel'"
by simp
moreover from enc Rel'_def have "(SourceTerm S2, TargetTerm (⟦S2⟧)) ∈ Rel'"
by simp
ultimately show "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
using trans Rel'_def
unfolding trans_def
by blast
next
fix S1 S2
define Rel' where "Rel' = Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}"
from enc Rel'_def have "(SourceTerm S1, TargetTerm (⟦S1⟧)) ∈ Rel'"
by simp
moreover assume "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel"
with Rel'_def have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel'"
by simp
moreover from Rel'_def have "(TargetTerm (⟦S2⟧), SourceTerm S2) ∈ Rel'"
by simp
ultimately show "(SourceTerm S1, SourceTerm S2) ∈ Rel"
using trans Rel'_def
unfolding trans_def
by blast
qed
lemma (in encoding) fully_abstract_wrt_preorders_iff_source_target_relation_is_transB:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
assumes preord: "preorder TRel"
shows "fully_abstract SRel TRel =
(∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q}))"
proof (rule iffI)
assume "fully_abstract SRel TRel"
with preord show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
using fully_abstract_wrt_preorders_impl_source_target_relation_is_trans[where SRel="SRel"
and TRel="TRel"]
unfolding preorder_on_def refl_on_def
by auto
next
assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
from this obtain Rel
where "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
and "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
and "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
by blast
thus "fully_abstract SRel TRel"
using source_target_relation_with_trans_impl_full_abstraction[where Rel="Rel"]
by blast
qed
text ‹The same holds if to obtain transitivity the union may contain additional pairs that do
neither relate two source nor two target terms.›
lemma (in encoding) fully_abstract_wrt_preorders_iff_source_target_relation_union_is_trans:
fixes SRel :: "('procS × 'procS) set"
and TRel :: "('procT × 'procT) set"
shows "(fully_abstract SRel TRel ∧ refl SRel ∧ trans TRel) =
(∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ (∃Rel'. (∀(P, Q) ∈ Rel'. P ∈ ProcS ⟷ Q ∈ ProcT)
∧ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel')))"
proof (rule iffI, (erule conjE)+)
assume "fully_abstract SRel TRel" and "refl SRel" and "trans TRel"
from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and A2: "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
and A3: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
and A4: "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
using fully_abstract_wrt_preorders_impl_source_target_relation_is_trans[where SRel="SRel"
and TRel="TRel"]
by blast
have "∀(P, Q) ∈ {}. P ∈ ProcS ⟷ Q ∈ ProcT"
by simp
moreover from A4 have "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ {})"
unfolding trans_def
by blast
ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ (∃Rel'. (∀(P, Q) ∈ Rel'. P ∈ ProcS ⟷ Q ∈ ProcT)
∧ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'))"
using A1 A2 A3
by blast
next
assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
∧ (∃Rel'. (∀(P, Q) ∈ Rel'. P ∈ ProcS ⟷ Q ∈ ProcT)
∧ trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'))"
from this obtain Rel Rel'
where B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
and B2: "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
and B3: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
and B4: "∀(P, Q) ∈ Rel'. P ∈ ProcS ⟷ Q ∈ ProcT"
and B5: "trans (Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel')"
by blast
have "fully_abstract SRel TRel"
proof auto
fix S1 S2
have "(TargetTerm (⟦S1⟧), SourceTerm S1) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'"
by simp
moreover assume "(S1, S2) ∈ SRel"
with B2 have "(SourceTerm S1, SourceTerm S2) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'"
by simp
moreover from B1
have "(SourceTerm S2, TargetTerm (⟦S2⟧)) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'"
by simp
ultimately have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel ∪ Rel'"
using B5
unfolding trans_def
by blast
with B3 B4 show "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
by blast
next
fix S1 S2
from B1
have "(SourceTerm S1, TargetTerm (⟦S1⟧)) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'"
by simp
moreover assume "(⟦S1⟧, ⟦S2⟧) ∈ TRel"
with B3
have "(TargetTerm (⟦S1⟧), TargetTerm (⟦S2⟧)) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'"
by simp
moreover
have "(TargetTerm (⟦S2⟧), SourceTerm S2) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'"
by simp
ultimately have "(SourceTerm S1, SourceTerm S2) ∈ Rel ∪ Rel'"
using B5
unfolding trans_def
by blast
with B2 B4 show "(S1, S2) ∈ SRel"
by blast
qed
moreover have "refl SRel"
unfolding refl_on_def
proof auto
fix S
from B1 have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'"
by simp
moreover
have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} ∪ Rel'"
by simp
ultimately have "(SourceTerm S, SourceTerm S) ∈ Rel ∪ Rel'"
using B5
unfolding trans_def
by blast
with B2 B4 show "(S, S) ∈ SRel"
by blast
qed
moreover have "trans TRel"
unfolding trans_def
proof clarify
fix TP TQ TR
assume "(TP, TQ) ∈ TRel" and "(TQ, TR) ∈ TRel"
with B3 B4 B5 show "(TP, TR) ∈ TRel"
unfolding trans_def
by blast
qed
ultimately show "fully_abstract SRel TRel ∧ refl SRel ∧ trans TRel"
by blast
qed
end