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