Theory SuccessSensitiveness

theory SuccessSensitiveness
  imports SourceTargetRelation
begin

section ‹Success Sensitiveness and Barbs›

text ‹To compare the abstract behavior of two terms, often some notion of success or successful
        termination is used. Daniele Gorla assumes a constant process (similar to the empty
        process) that represents successful termination in order to compare the behavior of source
        terms with their literal translations. Then an encoding is success sensitive if, for all
        source terms S, S reaches success iff the translation of S reaches success. Successful
        termination can be considered as some special kind of barb. Accordingly we generalize
        successful termination to the respection of an arbitrary subset of barbs. An encoding
        respects a set of barbs if, for every source term S and all considered barbs a, S reaches a
        iff the translation of S reaches a.›

abbreviation (in encoding_wrt_barbs) enc_weakly_preserves_barb_set :: "'barbs set ⇒ bool" where
  "enc_weakly_preserves_barb_set Barbs ≡ enc_preserves_binary_pred (λP a. a ∈ Barbs ∧ P⇓.a)"

abbreviation (in encoding_wrt_barbs) enc_weakly_preserves_barbs :: "bool" where
  "enc_weakly_preserves_barbs ≡ enc_preserves_binary_pred (λP a. P⇓.a)"

lemma (in encoding_wrt_barbs) enc_weakly_preserves_barbs_and_barb_set:
  shows "enc_weakly_preserves_barbs = (∀Barbs. enc_weakly_preserves_barb_set Barbs)"
    by blast

abbreviation (in encoding_wrt_barbs) enc_weakly_reflects_barb_set :: "'barbs set ⇒ bool" where
  "enc_weakly_reflects_barb_set Barbs ≡ enc_reflects_binary_pred (λP a. a ∈ Barbs ∧ P⇓.a)"

abbreviation (in encoding_wrt_barbs) enc_weakly_reflects_barbs :: "bool" where
  "enc_weakly_reflects_barbs ≡ enc_reflects_binary_pred (λP a. P⇓.a)"

lemma (in encoding_wrt_barbs) enc_weakly_reflects_barbs_and_barb_set:
  shows "enc_weakly_reflects_barbs = (∀Barbs. enc_weakly_reflects_barb_set Barbs)"
    by blast

abbreviation (in encoding_wrt_barbs) enc_weakly_respects_barb_set :: "'barbs set ⇒ bool" where
  "enc_weakly_respects_barb_set Barbs ≡
   enc_weakly_preserves_barb_set Barbs ∧ enc_weakly_reflects_barb_set Barbs"

abbreviation (in encoding_wrt_barbs) enc_weakly_respects_barbs :: "bool" where
  "enc_weakly_respects_barbs ≡ enc_weakly_preserves_barbs ∧ enc_weakly_reflects_barbs"

lemma (in encoding_wrt_barbs) enc_weakly_respects_barbs_and_barb_set:
  shows "enc_weakly_respects_barbs = (∀Barbs. enc_weakly_respects_barb_set Barbs)"
proof -
  have "(∀Barbs. enc_weakly_respects_barb_set Barbs)
        = (∀Barbs. (∀S x. x ∈ Barbs ∧ S⇓<SWB>x ⟶ ⟦S⟧⇓<TWB>x)
          ∧ (∀S x. x ∈ Barbs ∧ ⟦S⟧⇓<TWB>x ⟶ S⇓<SWB>x))"
    by simp
  hence "(∀Barbs. enc_weakly_respects_barb_set Barbs)
        = ((∀Barbs. enc_weakly_preserves_barb_set Barbs)
            ∧ (∀Barbs. enc_weakly_reflects_barb_set Barbs))"
    apply simp by fast
  thus ?thesis
    apply simp by blast
qed

text ‹An encoding strongly respects some set of barbs if, for every source term S and all
        considered barbs a, S has a iff the translation of S has a.›

abbreviation (in encoding_wrt_barbs) enc_preserves_barb_set :: "'barbs set ⇒ bool" where
  "enc_preserves_barb_set Barbs ≡ enc_preserves_binary_pred (λP a. a ∈ Barbs ∧ P↓.a)"

abbreviation (in encoding_wrt_barbs) enc_preserves_barbs :: "bool" where
  "enc_preserves_barbs ≡ enc_preserves_binary_pred (λP a. P↓.a)"

lemma (in encoding_wrt_barbs) enc_preserves_barbs_and_barb_set:
  shows "enc_preserves_barbs = (∀Barbs. enc_preserves_barb_set Barbs)"
    by blast

abbreviation (in encoding_wrt_barbs) enc_reflects_barb_set :: "'barbs set ⇒ bool" where
  "enc_reflects_barb_set Barbs ≡ enc_reflects_binary_pred (λP a. a ∈ Barbs ∧ P↓.a)"

abbreviation (in encoding_wrt_barbs) enc_reflects_barbs :: "bool" where
  "enc_reflects_barbs ≡ enc_reflects_binary_pred (λP a. P↓.a)"

lemma (in encoding_wrt_barbs) enc_reflects_barbs_and_barb_set:
  shows "enc_reflects_barbs = (∀Barbs. enc_reflects_barb_set Barbs)"
    by blast

abbreviation (in encoding_wrt_barbs) enc_respects_barb_set :: "'barbs set ⇒ bool" where
  "enc_respects_barb_set Barbs ≡ enc_preserves_barb_set Barbs ∧ enc_reflects_barb_set Barbs"

abbreviation (in encoding_wrt_barbs) enc_respects_barbs :: "bool" where
  "enc_respects_barbs ≡ enc_preserves_barbs ∧ enc_reflects_barbs"

lemma (in encoding_wrt_barbs) enc_respects_barbs_and_barb_set:
  shows "enc_respects_barbs = (∀Barbs. enc_respects_barb_set Barbs)"
proof -
  have "(∀Barbs. enc_respects_barb_set Barbs)
        = ((∀Barbs. enc_preserves_barb_set Barbs)
            ∧ (∀Barbs. enc_reflects_barb_set Barbs))"
    apply simp by fast
  thus ?thesis
    apply simp by blast
qed

text ‹An encoding (weakly) preserves barbs iff
        (1) there exists a relation, like indRelR, that relates source terms and their literal
            translations and preserves (reachability/)existence of barbs, or
        (2) there exists a relation, like indRelL, that relates literal translations and their
            source terms and reflects (reachability/)existence of barbs.›

lemma (in encoding_wrt_barbs) enc_weakly_preserves_barb_set_iff_source_target_rel:
  fixes Barbs :: "'barbs set"
    and TRel  :: "('procT × 'procT) set"
  shows "enc_weakly_preserves_barb_set Barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_weakly_preserves_barb_set Rel (STCalWB SWB TWB) Barbs)"
      using enc_preserves_binary_pred_iff_source_target_rel_preserves_binary_pred[where
             Pred="λP a. a ∈ Barbs ∧ P⇓<STCalWB SWB TWB>a"] STCalWB_reachesBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_weakly_preserves_barbs_iff_source_target_rel:
  shows "enc_weakly_preserves_barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_weakly_preserves_barbs Rel (STCalWB SWB TWB))"
      using enc_preserves_binary_pred_iff_source_target_rel_preserves_binary_pred[where
             Pred="λP a. P⇓<STCalWB SWB TWB>a"] STCalWB_reachesBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_preserves_barb_set_iff_source_target_rel:
  fixes Barbs :: "'barbs set"
  shows "enc_preserves_barb_set Barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_preserves_barb_set Rel (STCalWB SWB TWB) Barbs)"
      using enc_preserves_binary_pred_iff_source_target_rel_preserves_binary_pred[where
             Pred="λP a. a ∈ Barbs ∧ P↓<STCalWB SWB TWB>a"] STCalWB_hasBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_preserves_barbs_iff_source_target_rel:
  shows "enc_preserves_barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_preserves_barbs Rel (STCalWB SWB TWB))"
      using enc_preserves_binary_pred_iff_source_target_rel_preserves_binary_pred[where
             Pred="λP a. P↓<STCalWB SWB TWB>a"] STCalWB_hasBarbST
    by simp

text ‹An encoding (weakly) reflects barbs iff
        (1) there exists a relation, like indRelR, that relates source terms and their literal
            translations and reflects (reachability/)existence of barbs, or
        (2) there exists a relation, like indRelL, that relates literal translations and their
            source terms and preserves (reachability/)existence of barbs.›

lemma (in encoding_wrt_barbs) enc_weakly_reflects_barb_set_iff_source_target_rel:
  fixes Barbs :: "'barbs set"
  shows "enc_weakly_reflects_barb_set Barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_weakly_reflects_barb_set Rel (STCalWB SWB TWB) Barbs)"
      using enc_reflects_binary_pred_iff_source_target_rel_reflects_binary_pred[where
             Pred="λP a. a ∈ Barbs ∧ P⇓<STCalWB SWB TWB>a"] STCalWB_reachesBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_weakly_reflects_barbs_iff_source_target_rel:
  shows "enc_weakly_reflects_barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_weakly_reflects_barbs Rel (STCalWB SWB TWB))"
      using enc_reflects_binary_pred_iff_source_target_rel_reflects_binary_pred[where
             Pred="λP a. P⇓<STCalWB SWB TWB>a"] STCalWB_reachesBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_reflects_barb_set_iff_source_target_rel:
  fixes Barbs :: "'barbs set"
  shows "enc_reflects_barb_set Barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_reflects_barb_set Rel (STCalWB SWB TWB) Barbs)"
      using enc_reflects_binary_pred_iff_source_target_rel_reflects_binary_pred[where
             Pred="λP a. a ∈ Barbs ∧ P↓<STCalWB SWB TWB>a"] STCalWB_hasBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_reflects_barbs_iff_source_target_rel:
  shows "enc_reflects_barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_reflects_barbs Rel (STCalWB SWB TWB))"
      using enc_reflects_binary_pred_iff_source_target_rel_reflects_binary_pred[where
             Pred="λP a. P↓<STCalWB SWB TWB>a"] STCalWB_hasBarbST
    by simp

text ‹An encoding (weakly) respects barbs iff
        (1) there exists a relation, like indRelR, that relates source terms and their literal
            translations and respects (reachability/)existence of barbs, or
        (2) there exists a relation, like indRelL, that relates literal translations and their
            source terms and respects (reachability/)existence of barbs, or
        (3) there exists a relation, like indRel, that relates source terms and their literal
            translations in both directions and respects (reachability/)existence of barbs.›

lemma (in encoding_wrt_barbs) enc_weakly_respects_barb_set_iff_source_target_rel:
  fixes Barbs :: "'barbs set"
  shows "enc_weakly_respects_barb_set Barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) Barbs)"
      using enc_respects_binary_pred_iff_source_target_rel_respects_binary_pred_encR[where
             Pred="λP a. a ∈ Barbs ∧ P⇓<STCalWB SWB TWB>a"] STCalWB_reachesBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_weakly_respects_barbs_iff_source_target_rel:
  shows "enc_weakly_respects_barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB))"
      using enc_respects_binary_pred_iff_source_target_rel_respects_binary_pred_encR[where
             Pred="λP a. P⇓<STCalWB SWB TWB>a"] STCalWB_reachesBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_respects_barb_set_iff_source_target_rel:
  fixes Barbs :: "'barbs set"
  shows "enc_respects_barb_set Barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) Barbs)"
      using enc_respects_binary_pred_iff_source_target_rel_respects_binary_pred_encR[where
             Pred="λP a. a ∈ Barbs ∧ P↓<STCalWB SWB TWB>a"] STCalWB_hasBarbST
    by simp

lemma (in encoding_wrt_barbs) enc_respects_barbs_iff_source_target_rel:
  shows "enc_respects_barbs
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_respects_barbs Rel (STCalWB SWB TWB))"
      using enc_respects_binary_pred_iff_source_target_rel_respects_binary_pred_encR[where
             Pred="λP a. P↓<STCalWB SWB TWB>a"] STCalWB_hasBarbST
    by simp

text ‹Accordingly an encoding is success sensitive iff there exists such a relation between
        source and target terms that weakly respects the barb success.›

lemma (in encoding_wrt_barbs) success_sensitive_cond:
  fixes success :: "'barbs"
  shows "enc_weakly_respects_barb_set {success} = (∀S. S⇓<SWB>success ⟷ ⟦S⟧⇓<TWB>success)"
    by auto

lemma (in encoding_wrt_barbs) success_sensitive_iff_source_target_rel_weakly_respects_success:
  fixes success :: "'barbs"
  shows "enc_weakly_respects_barb_set {success}
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success})"
    by (rule enc_weakly_respects_barb_set_iff_source_target_rel[where Barbs="{success}"])+

lemma (in encoding_wrt_barbs) success_sensitive_iff_source_target_rel_respects_success:
  fixes success :: "'barbs"
  shows "enc_respects_barb_set {success}
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success})"
    by (rule enc_respects_barb_set_iff_source_target_rel[where Barbs="{success}"])

end