Theory DivergenceReflection

(* Kirstin Peters, TU Berlin, 2015 concerning the reduction semantics and
   Kirstin Peters, University of Augsburg, 2026 for the labelled semantics *)

theory DivergenceReflection
  imports SourceTargetRelation
begin

section ‹Divergence Reflection›

text ‹Divergence reflection forbids for encodings that introduce loops of internal actions. Thus
      they determine the practicability of encodings in particular with respect to implementations.
      An encoding reflects divergence if each loop in a target term result from the translation of
      a divergent source term.›

abbreviation (in encoding) enc_preserves_divergence :: "bool" where
  "enc_preserves_divergence ≡ enc_preserves_pred (λP. P ⟼STω)"

abbreviation (in encodingLS) enc_preserves_divergence :: "bool" where
  "enc_preserves_divergence ≡ enc_preserves_pred (λP. P →STω)"

lemma (in encoding) divergence_preservation_cond:
  shows "enc_preserves_divergence = (∀S. S ⟼(Source)ω ⟶ ⟦S⟧ ⟼(Target)ω)"
  by simp

lemma (in encodingLS) divergence_preservation_cond:
  shows "enc_preserves_divergence = (∀S. S →(Source)ω ⟶ ⟦S⟧ →(Target)ω)"
  by simp

abbreviation (in encoding) enc_reflects_divergence :: "bool" where
  "enc_reflects_divergence ≡ enc_reflects_pred (λP. P ⟼STω)"

abbreviation (in encodingLS) enc_reflects_divergence :: "bool" where
  "enc_reflects_divergence ≡ enc_reflects_pred (λP. P →STω)"

lemma (in encoding) divergence_reflection_cond:
  shows "enc_reflects_divergence = (∀S. ⟦S⟧ ⟼(Target)ω ⟶ S ⟼(Source)ω)"
  by simp

lemma (in encodingLS) divergence_reflection_cond:
  shows "enc_reflects_divergence = (∀S. ⟦S⟧ →(Target)ω ⟶ S →(Source)ω)"
  by simp

abbreviation rel_preserves_divergence :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool"
  where
  "rel_preserves_divergence Rel Cal ≡ rel_preserves_pred Rel (λP. P ⟼(Cal)ω)"

abbreviation rel_preserves_divergenceLS
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "rel_preserves_divergenceLS Rel Cal ≡ rel_preserves_pred Rel (λP. P →(Cal)ω)"

abbreviation rel_reflects_divergence :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool"
  where
  "rel_reflects_divergence Rel Cal ≡ rel_reflects_pred Rel (λP. P ⟼(Cal)ω)"

abbreviation rel_reflects_divergenceLS
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "rel_reflects_divergenceLS Rel Cal ≡ rel_reflects_pred Rel (λP. P →(Cal)ω)"

text ‹Apart from divergence reflection we consider divergence respection. An encoding respects
      divergence if each divergent source term is translated into a divergent target term and each
      divergent target term result from the translation of a divergent source term.›

abbreviation (in encoding) enc_respects_divergence :: "bool" where
  "enc_respects_divergence ≡ enc_respects_pred (λP. P ⟼STω)"

abbreviation (in encodingLS) enc_respects_divergence :: "bool" where
  "enc_respects_divergence ≡ enc_respects_pred (λP. P →STω)"

lemma (in encoding) divergence_respection_cond:
  shows "enc_respects_divergence = (∀S. ⟦S⟧ ⟼(Target)ω ⟷ S ⟼(Source)ω)"
  by auto

lemma (in encodingLS) divergence_respection_cond:
  shows "enc_respects_divergence = (∀S. ⟦S⟧ →(Target)ω ⟷ S →(Source)ω)"
  by auto

abbreviation rel_respects_divergence :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool"
  where
  "rel_respects_divergence Rel Cal ≡ rel_respects_pred Rel (λP. P ⟼(Cal)ω)"

abbreviation rel_respects_divergenceLS
  :: "('proc × 'proc) set ⇒ ('proc, 'lab) labelledProcessCalculus ⇒ bool" where
  "rel_respects_divergenceLS Rel Cal ≡ rel_respects_pred Rel (λP. P →(Cal)ω)"

text ‹An encoding preserves divergence iff
      (1) there exists a relation that relates source terms and their literal translations and
          preserves divergence, or
      (2) there exists a relation that relates literal translations and their source terms and
          reflects divergence.›

lemma (in encoding) divergence_preservation_iff_source_target_rel_preserves_divergence:
  shows "enc_preserves_divergence
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_preserves_divergence Rel (STCal Source Target))"
  using enc_preserves_pred_iff_source_target_rel_preserves_pred(1)[where Pred="λP. P ⟼STω"]
        divergentST_STCal_divergent
  by simp

lemma (in encodingLS) divergence_preservation_iff_source_target_rel_preserves_divergence:
  shows "enc_preserves_divergence
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_preserves_divergenceLS Rel (STLCal Source Target))"
  using enc_preserves_pred_iff_source_target_rel_preserves_pred(1)[where Pred="λP. P →STω"]
        divergentST_STCal_divergent
  by simp

lemma (in encoding) divergence_preservation_iff_source_target_rel_reflects_divergence:
  shows "enc_preserves_divergence
         = (∃Rel. (∀S. (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
            ∧ rel_reflects_divergence Rel (STCal Source Target))"
  using enc_preserves_pred_iff_source_target_rel_reflects_pred(1)[where Pred="λP. P ⟼STω"]
        divergentST_STCal_divergent
  by simp

lemma (in encodingLS) divergence_preservation_iff_source_target_rel_reflects_divergence:
  shows "enc_preserves_divergence
         = (∃Rel. (∀S. (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
            ∧ rel_reflects_divergenceLS Rel (STLCal Source Target))"
  using enc_preserves_pred_iff_source_target_rel_reflects_pred(1)[where Pred="λP. P →STω"]
        divergentST_STCal_divergent
  by simp

text ‹An encoding reflects divergence iff
      (1) there exists a relation that relates source terms and their literal translations and
          reflects divergence, or
      (2) there exists a relation that relates literal translations and their source terms and
          preserves divergence.›

lemma (in encoding) divergence_reflection_iff_source_target_rel_reflects_divergence:
  shows "enc_reflects_divergence
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_reflects_divergence Rel (STCal Source Target))"
  using enc_reflects_pred_iff_source_target_rel_reflects_pred[where Pred="λP. P ⟼STω"]
        divergentST_STCal_divergent
  by simp

lemma (in encodingLS) divergence_reflection_iff_source_target_rel_reflects_divergence:
  shows "enc_reflects_divergence
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_reflects_divergenceLS Rel (STLCal Source Target))"
  using enc_reflects_pred_iff_source_target_rel_reflects_pred[where Pred="λP. P →STω"]
        divergentST_STCal_divergent
  by simp

lemma (in encoding) divergence_reflection_iff_source_target_rel_preserves_divergence:
  shows "enc_reflects_divergence
         = (∃Rel. (∀S. (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
            ∧ rel_preserves_divergence Rel (STCal Source Target))"
  using enc_reflects_pred_iff_source_target_rel_preserves_pred[where Pred="λP. P ⟼STω"]
        divergentST_STCal_divergent
  by simp

lemma (in encodingLS) divergence_reflection_iff_source_target_rel_preserves_divergence:
  shows "enc_reflects_divergence
         = (∃Rel. (∀S. (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
            ∧ rel_preserves_divergenceLS Rel (STLCal Source Target))"
  using enc_reflects_pred_iff_source_target_rel_preserves_pred[where Pred="λP. P →STω"]
        divergentST_STCal_divergent
  by simp

text ‹An encoding respects divergence iff there exists a relation that relates source terms and
      their literal translations in both directions and respects divergence.›

lemma (in encoding) divergence_respection_iff_source_target_rel_respects_divergence:
  shows "enc_respects_divergence = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
         ∧ rel_respects_divergence Rel (STCal Source Target))"
    and "enc_respects_divergence = (∃Rel.
         (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
         ∧ rel_respects_divergence Rel (STCal Source Target))"
proof -
  show "enc_respects_divergence = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
        ∧ rel_respects_divergence Rel (STCal Source Target))"
    using enc_respects_pred_iff_source_target_rel_respects_pred_encR[where Pred="λP. P ⟼STω"]
          divergentST_STCal_divergent
    by simp
next
  show "enc_respects_divergence = (∃Rel.
        (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
        ∧ rel_respects_divergence Rel (STCal Source Target))"
    using enc_respects_pred_iff_source_target_rel_respects_pred_encRL[where Pred="λP. P ⟼STω"]
          divergentST_STCal_divergent
    by simp
qed

lemma (in encodingLS) divergence_respection_iff_source_target_rel_respects_divergence:
  shows "enc_respects_divergence = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
         ∧ rel_respects_divergenceLS Rel (STLCal Source Target))"
    and "enc_respects_divergence = (∃Rel.
         (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
         ∧ rel_respects_divergenceLS Rel (STLCal Source Target))"
proof -
  show "enc_respects_divergence = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
        ∧ rel_respects_divergenceLS Rel (STLCal Source Target))"
    using enc_respects_pred_iff_source_target_rel_respects_pred_encR[where Pred="λP. P →STω"]
          divergentST_STCal_divergent
    by simp
next
  show "enc_respects_divergence = (∃Rel.
        (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
        ∧ rel_respects_divergenceLS Rel (STLCal Source Target))"
    using enc_respects_pred_iff_source_target_rel_respects_pred_encRL[where Pred="λP. P →STω"]
          divergentST_STCal_divergent
    by simp
qed

end