Theory DivergenceReflection

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ω)"

lemma (in encoding) 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ω)"

lemma (in encoding) 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_reflects_divergence
    :: "('proc × 'proc) set ⇒ 'proc processCalculus ⇒ bool"
  where
  "rel_reflects_divergence 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ω)"

lemma (in encoding) 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)ω)"

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 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

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 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

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

end