Theory Encodings

theory Encodings
  imports ProcessCalculi
begin

section ‹Encodings›

text ‹In the simplest case an encoding from a source into a target language is a mapping from
        source into target terms. Encodability criteria describe properties on such mappings. To
        analyse encodability criteria we map them on conditions on relations between source and
        target terms. More precisely, we consider relations on pairs of the disjoint union of
        source and target terms. We denote this disjoint union of source and target terms by Proc.
›

datatype ('procS, 'procT) Proc =
  SourceTerm 'procS |
  TargetTerm 'procT

definition STCal
    :: "'procS processCalculus ⇒ 'procT processCalculus
        ⇒ (('procS, 'procT) Proc) processCalculus"
  where
  "STCal Source Target ≡
   ⦇Reductions = λP P'.
   (∃SP SP'. P = SourceTerm SP ∧ P' = SourceTerm SP' ∧ Reductions Source SP SP') ∨
   (∃TP TP'. P = TargetTerm TP ∧ P' = TargetTerm TP' ∧ Reductions Target TP TP')⦈"

definition STCalWB
    :: "('procS, 'barbs) calculusWithBarbs ⇒ ('procT, 'barbs) calculusWithBarbs
        ⇒ (('procS, 'procT) Proc, 'barbs) calculusWithBarbs"
  where
  "STCalWB Source Target ≡
   ⦇Calculus = STCal (calculusWithBarbs.Calculus Source) (calculusWithBarbs.Calculus Target),
   HasBarb   = λP a. (∃SP. P = SourceTerm SP ∧ (calculusWithBarbs.HasBarb Source) SP a) ∨
                     (∃TP. P = TargetTerm TP ∧ (calculusWithBarbs.HasBarb Target) TP a)⦈"

text ‹An encoding consists of a source language, a target language, and a mapping from source
        into target terms.›

locale encoding =
  fixes Source :: "'procS processCalculus"
    and Target :: "'procT processCalculus"
    and Enc    :: "'procS ⇒ 'procT"
begin

abbreviation enc :: "'procS ⇒ 'procT" ("⟦_⟧" [65] 70) where
  "⟦S⟧ ≡ Enc S"

abbreviation isSource :: "('procS, 'procT) Proc ⇒ bool" ("_ ∈ ProcS" [70] 80) where
  "P ∈ ProcS ≡ (∃S. P = SourceTerm S)"

abbreviation isTarget :: "('procS, 'procT) Proc ⇒ bool" ("_ ∈ ProcT" [70] 80) where
  "P ∈ ProcT ≡ (∃T. P = TargetTerm T)"

abbreviation getSource
    :: "'procS ⇒ ('procS, 'procT) Proc ⇒ bool" ("_ ∈S _" [70, 70] 80)
  where
  "S ∈S P ≡ (P = SourceTerm S)"

abbreviation getTarget
    :: "'procT ⇒ ('procS, 'procT) Proc ⇒ bool" ("_ ∈T _" [70, 70] 80)
  where
  "T ∈T P ≡ (P = TargetTerm T)"

text ‹A step of a term in Proc is either a source term step or a target term step.›

abbreviation stepST
    :: "('procS, 'procT) Proc ⇒ ('procS, 'procT) Proc ⇒ bool" ("_ ⟼ST _" [70, 70] 80)
  where
  "P ⟼ST P' ≡
   (∃S S'. S ∈S P ∧ S' ∈S P' ∧ S ⟼Source S') ∨ (∃T T'. T ∈T P ∧ T' ∈T P' ∧ T ⟼Target T')"

lemma stepST_STCal_step:
  fixes P P' :: "('procS, 'procT) Proc"
  shows "P ⟼(STCal Source Target) P' = P ⟼ST P'"
    by (simp add: STCal_def)

lemma STStep_step:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ⟼ST P' = (∃S'. S' ∈S P' ∧ S ⟼Source S')"
    and "TargetTerm T ⟼ST P' = (∃T'. T' ∈T P' ∧ T ⟼Target T')"
    by blast+

lemma STCal_step:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ⟼(STCal Source Target) P' = (∃S'. S' ∈S P' ∧ S ⟼Source S')"
    and "TargetTerm T ⟼(STCal Source Target) P' = (∃T'. T' ∈T P' ∧ T ⟼Target T')"
    by (simp add: STCal_def)+

text ‹A sequence of steps of a term in Proc is either a sequence of source term steps or a
        sequence of target term steps.›

abbreviation stepsST
    :: "('procS, 'procT) Proc ⇒ ('procS, 'procT) Proc ⇒ bool" ("_ ⟼ST* _" [70, 70] 80)
  where
  "P ⟼ST* P' ≡
   (∃S S'. S ∈S P ∧ S' ∈S P' ∧ S ⟼Source* S') ∨ (∃T T'. T ∈T P ∧ T' ∈T P' ∧ T ⟼Target* T')"

lemma STSteps_steps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ⟼ST* P' = (∃S'. S' ∈S P' ∧ S ⟼Source* S')"
    and "TargetTerm T ⟼ST* P' = (∃T'. T' ∈T P' ∧ T ⟼Target* T')"
    by blast+

lemma STCal_steps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ⟼(STCal Source Target)* P' = (∃S'. S' ∈S P' ∧ S ⟼Source* S')"
    and "TargetTerm T ⟼(STCal Source Target)* P' = (∃T'. T' ∈T P' ∧ T ⟼Target* T')"
proof auto
  assume "SourceTerm S ⟼(STCal Source Target)* P'"
  from this obtain n where "SourceTerm S ⟼(STCal Source Target)⇗n⇖ P'"
    by (auto simp add: steps_def)
  thus "∃S'. S' ∈S P' ∧ S ⟼Source* S'"
  proof (induct n arbitrary: P')
    case 0
    assume "SourceTerm S ⟼(STCal Source Target)⇗0⇖ P'"
    hence "S ∈S P'"
      by simp
    moreover have "S ⟼Source* S"
      by (rule steps_refl)
    ultimately show "∃S'. S' ∈S P' ∧ S ⟼Source* S'"
      by blast
  next
    case (Suc n P'')
    assume "SourceTerm S ⟼(STCal Source Target)⇗Suc n⇖ P''"
    from this obtain P' where A1: "SourceTerm S ⟼(STCal Source Target)⇗n⇖ P'"
                          and A2: "P' ⟼(STCal Source Target) P''"
      by auto
    assume "⋀P'. SourceTerm S ⟼(STCal Source Target)⇗n⇖ P' ⟹ ∃S'. S' ∈S P' ∧ S ⟼Source* S'"
    with A1 obtain S' where A3: "S' ∈S P'" and A4: "S ⟼Source* S'"
      by blast
    from A2 A3 obtain S'' where A5: "S'' ∈S P''" and A6: "S' ⟼Source S''"
        using STCal_step(1)[where S="S'" and P'="P''"]
      by blast
    from A4 A6 have "S ⟼Source* S''"
        using step_to_steps[where Cal="Source" and P="S'" and P'="S''"]
      by (simp add: steps_add[where Cal="Source" and P="S" and Q="S'" and R="S''"])
    with A5 show "∃S''. S'' ∈S P'' ∧ S ⟼Source* S''"
      by blast
  qed
next
  fix S'
  assume "S ⟼Source* S'"
  from this obtain n where "S ⟼Source⇗n⇖ S'"
    by (auto simp add: steps_def)
  thus "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
  proof (induct n arbitrary: S')
    case 0
    assume "S ⟼Source⇗0⇖ S'"
    hence "S = S'"
      by auto
    thus "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
      by (simp add: steps_refl)
  next
    case (Suc n S'')
    assume "S ⟼Source⇗Suc n⇖ S''"
    from this obtain S' where B1: "S ⟼Source⇗n⇖ S'" and B2: "S' ⟼Source S''"
      by auto
    assume "⋀S'. S ⟼Source⇗n⇖ S' ⟹ SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
    with B1 have "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
      by blast
    moreover from B2 have "SourceTerm S' ⟼(STCal Source Target)* (SourceTerm S'')"
        using step_to_steps[where Cal="STCal Source Target" and P="SourceTerm S'"]
      by (simp add: STCal_def)
    ultimately show "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S'')"
      by (rule steps_add)
  qed
next
  assume "TargetTerm T ⟼(STCal Source Target)* P'"
  from this obtain n where "TargetTerm T ⟼(STCal Source Target)⇗n⇖ P'"
    by (auto simp add: steps_def)
  thus "∃T'. T' ∈T P' ∧ T ⟼Target* T'"
  proof (induct n arbitrary: P')
    case 0
    assume "TargetTerm T ⟼(STCal Source Target)⇗0⇖ P'"
    hence "T ∈T P'"
      by simp
    moreover have "T ⟼Target* T"
      by (rule steps_refl)
    ultimately show "∃T'. T' ∈T P' ∧ T ⟼Target* T'"
      by blast
  next
    case (Suc n P'')
    assume "TargetTerm T ⟼(STCal Source Target)⇗Suc n⇖ P''"
    from this obtain P' where A1: "TargetTerm T ⟼(STCal Source Target)⇗n⇖ P'"
                          and A2: "P' ⟼(STCal Source Target) P''"
      by auto
    assume "⋀P'. TargetTerm T ⟼(STCal Source Target)⇗n⇖ P' ⟹ ∃T'. T' ∈T P' ∧ T ⟼Target* T'"
    with A1 obtain T' where A3: "T' ∈T P'" and A4: "T ⟼Target* T'"
      by blast
    from A2 A3 obtain T'' where A5: "T'' ∈T P''" and A6: "T' ⟼Target T''"
        using STCal_step(2)[where T="T'" and P'="P''"]
      by blast
    from A4 A6 have "T ⟼Target* T''"
        using step_to_steps[where Cal="Target" and P="T'" and P'="T''"]
      by (simp add: steps_add[where Cal="Target" and P="T" and Q="T'" and R="T''"])
    with A5 show "∃T''. T'' ∈T P'' ∧ T ⟼Target* T''"
      by blast
  qed
next
  fix T'
  assume "T ⟼Target* T'"
  from this obtain n where "T ⟼Target⇗n⇖ T'"
    by (auto simp add: steps_def)
  thus "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
  proof (induct n arbitrary: T')
    case 0
    assume "T ⟼Target⇗0⇖ T'"
    hence "T = T'"
      by auto
    thus "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
      by (simp add: steps_refl)
  next
    case (Suc n T'')
    assume "T ⟼Target⇗Suc n⇖ T''"
    from this obtain T' where B1: "T ⟼Target⇗n⇖ T'" and B2: "T' ⟼Target T''"
      by auto
    assume "⋀T'. T ⟼Target⇗n⇖ T' ⟹ TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
    with B1 have "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
      by blast
    moreover from B2 have "TargetTerm T' ⟼(STCal Source Target)* (TargetTerm T'')"
        using step_to_steps[where Cal="STCal Source Target" and P="TargetTerm T'"]
      by (simp add: STCal_def)
    ultimately show "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T'')"
      by (rule steps_add)
  qed
qed

lemma stepsST_STCal_steps:
  fixes P P' :: "('procS, 'procT) Proc"
  shows "P ⟼(STCal Source Target)* P' = P ⟼ST* P'"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P ⟼(STCal Source Target)* P' = P ⟼ST* P'"
      using STCal_steps(1)[where S="SP" and P'="P'"] STSteps_steps(1)[where S="SP" and P'="P'"]
    by blast
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P ⟼(STCal Source Target)* P' = P ⟼ST* P'"
      using STCal_steps(2)[where T="TP" and P'="P'"] STSteps_steps(2)[where T="TP" and P'="P'"]
    by blast
qed

lemma stepsST_refl:
  fixes P :: "('procS, 'procT) Proc"
  shows "P ⟼ST* P"
    by (cases P, simp_all add: steps_refl)

lemma stepsST_add:
  fixes P Q R :: "('procS, 'procT) Proc"
  assumes A1: "P ⟼ST* Q"
      and A2: "Q ⟼ST* R"
  shows "P ⟼ST* R"
proof -
  from A1 have "P ⟼(STCal Source Target)* Q"
    by (simp add: stepsST_STCal_steps)
  moreover from A2 have "Q ⟼(STCal Source Target)* R"
    by (simp add: stepsST_STCal_steps)
  ultimately have "P ⟼(STCal Source Target)* R"
    by (rule steps_add)
  thus "P ⟼ST* R"
    by (simp add: stepsST_STCal_steps)
qed

text ‹A divergent term of Proc is either a divergent source term or a divergent target term.›

abbreviation divergentST
    :: "('procS, 'procT) Proc ⇒ bool" ("_ ⟼STω" [70] 80)
  where
  "P ⟼STω ≡ (∃S. S ∈S P ∧ S ⟼(Source)ω) ∨ (∃T. T ∈T P ∧ T ⟼(Target)ω)"

lemma STCal_divergent:
  fixes S  :: "'procS"
    and T  :: "'procT"
  shows "SourceTerm S ⟼(STCal Source Target)ω = S ⟼(Source)ω"
    and "TargetTerm T ⟼(STCal Source Target)ω = T ⟼(Target)ω"
      using STCal_steps
    by (auto simp add: STCal_def divergent_def)

lemma divergentST_STCal_divergent:
  fixes P :: "('procS, 'procT) Proc"
  shows "P ⟼(STCal Source Target)ω = P ⟼STω"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P ⟼(STCal Source Target)ω = P ⟼STω"
      using STCal_divergent(1)
    by simp
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P ⟼(STCal Source Target)ω = P ⟼STω"
      using STCal_divergent(2)
    by simp
qed

text ‹Similar to relations we define what it means for an encoding to preserve, reflect, or
        respect a predicate. An encoding preserves some predicate P if P(S) implies P(enc S) for
        all source terms S.›

abbreviation enc_preserves_pred :: "(('procS, 'procT) Proc ⇒ bool) ⇒ bool" where
  "enc_preserves_pred Pred ≡ ∀S. Pred (SourceTerm S) ⟶ Pred (TargetTerm (⟦S⟧))"

abbreviation enc_preserves_binary_pred
    :: "(('procS, 'procT) Proc ⇒ 'b ⇒ bool) ⇒ bool"
  where
  "enc_preserves_binary_pred Pred ≡ ∀S x. Pred (SourceTerm S) x ⟶ Pred (TargetTerm (⟦S⟧)) x"

text ‹An encoding reflects some predicate P if P(S) implies P(enc S) for all source terms S.›

abbreviation enc_reflects_pred :: "(('procS, 'procT) Proc ⇒ bool) ⇒ bool" where
  "enc_reflects_pred Pred ≡ ∀S. Pred (TargetTerm (⟦S⟧)) ⟶ Pred (SourceTerm S)"

abbreviation enc_reflects_binary_pred
    :: "(('procS, 'procT) Proc ⇒ 'b ⇒ bool) ⇒ bool"
  where
  "enc_reflects_binary_pred Pred ≡ ∀S x. Pred (TargetTerm (⟦S⟧)) x ⟶ Pred (SourceTerm S) x"

text ‹An encoding respects a predicate if it preserves and reflects it.›

abbreviation enc_respects_pred :: "(('procS, 'procT) Proc ⇒ bool) ⇒ bool" where
  "enc_respects_pred Pred ≡ enc_preserves_pred Pred ∧ enc_reflects_pred Pred"

abbreviation enc_respects_binary_pred
    :: "(('procS, 'procT) Proc ⇒ 'b ⇒ bool) ⇒ bool"
  where
  "enc_respects_binary_pred Pred ≡
   enc_preserves_binary_pred Pred ∧ enc_reflects_binary_pred Pred"

end

text ‹To compare source terms and target terms w.r.t. their barbs or observables we assume that
        each languages defines its own predicate for the existence of barbs.›

locale encoding_wrt_barbs =
  encoding Source Target Enc
  for Source :: "'procS processCalculus"
  and Target :: "'procT processCalculus"
  and Enc    :: "'procS ⇒ 'procT" +
  fixes SWB :: "('procS, 'barbs) calculusWithBarbs"
    and TWB :: "('procT, 'barbs) calculusWithBarbs"
  assumes calS: "calculusWithBarbs.Calculus SWB = Source"
      and calT: "calculusWithBarbs.Calculus TWB = Target"
begin

lemma STCalWB_STCal:
  shows "Calculus (STCalWB SWB TWB) = STCal Source Target"
      unfolding STCalWB_def using calS calT
    by auto

text ‹We say a term P of Proc has some barbs a if either P is a source term that has barb a or P
        is a target term that has the barb b. For simplicity we assume that the sets of barbs is
        large enough to contain all barbs of the source terms, the target terms, and all barbs they
        might have in common.›

abbreviation hasBarbST
    :: "('procS, 'procT) Proc ⇒ 'barbs ⇒ bool" ("_↓._" [70, 70] 80)
  where
  "P↓.a ≡ (∃S. S ∈S P ∧ S↓<SWB>a) ∨ (∃T. T ∈T P ∧ T↓<TWB>a)"

lemma STCalWB_hasBarbST:
  fixes P :: "('procS, 'procT) Proc"
    and a :: "'barbs"
  shows "P↓<STCalWB SWB TWB>a = P↓.a"
    by (simp add: STCalWB_def)

lemma preservation_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes preservation: "rel_preserves_barbs Rel (STCalWB SWB TWB)"
      and rel:          "(P, Q) ∈ Rel"
      and barb:         "P↓.a"
  shows "Q↓.a"
      using preservation rel barb
    by (simp add: STCalWB_def)

lemma reflection_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes reflection: "rel_reflects_barbs Rel (STCalWB SWB TWB)"
      and rel:        "(P, Q) ∈ Rel"
      and barb:       "Q↓.a"
  shows "P↓.a"
      using reflection rel barb
    by (simp add: STCalWB_def)

lemma respection_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes respection: "rel_respects_barbs Rel (STCalWB SWB TWB)"
      and rel:        "(P, Q) ∈ Rel"
  shows "P↓.a = Q↓.a"
      using preservation_of_barbs_in_barbed_encoding[where Rel="Rel" and P="P" and Q="Q" and a="a"]
            reflection_of_barbs_in_barbed_encoding[where Rel="Rel" and P="P" and Q="Q" and a="a"]
            respection rel
    by blast

text ‹A term P of Proc reaches a barb a if either P is a source term that reaches a or P is a
        target term that reaches a.›

abbreviation reachesBarbST
    :: "('procS, 'procT) Proc ⇒ 'barbs ⇒ bool" ("_⇓._" [70, 70] 80)
  where
  "P⇓.a ≡ (∃S. S ∈S P ∧ S⇓<SWB>a) ∨ (∃T. T ∈T P ∧ T⇓<TWB>a)"

lemma STCalWB_reachesBarbST:
  fixes P :: "('procS, 'procT) Proc"
    and a :: "'barbs"
  shows "P⇓<STCalWB SWB TWB>a = P⇓.a"
proof -
  have "∀S. SourceTerm S⇓<STCalWB SWB TWB>a = SourceTerm S⇓.a"
      using STCal_steps(1)
    by (auto simp add: STCalWB_def calS calT)
  moreover have "∀T. TargetTerm T⇓<STCalWB SWB TWB>a = TargetTerm T⇓.a"
      using STCal_steps(2)
    by (auto simp add: STCalWB_def calS calT)
  ultimately show "P⇓<STCalWB SWB TWB>a = P⇓.a"
    by (cases P, simp+)
qed

lemma weak_preservation_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes preservation: "rel_weakly_preserves_barbs Rel (STCalWB SWB TWB)"
      and rel:          "(P, Q) ∈ Rel"
      and barb:         "P⇓.a"
  shows "Q⇓.a"
proof -
  from barb have "P⇓<STCalWB SWB TWB>a"
    by (simp add: STCalWB_reachesBarbST)
  with preservation rel have "Q⇓<STCalWB SWB TWB>a"
    by blast
  thus "Q⇓.a"
    by (simp add: STCalWB_reachesBarbST)
qed

lemma weak_reflection_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes reflection: "rel_weakly_reflects_barbs Rel (STCalWB SWB TWB)"
      and rel:        "(P, Q) ∈ Rel"
      and barb:       "Q⇓.a"
  shows "P⇓.a"
proof -
  from barb have "Q⇓<STCalWB SWB TWB>a"
    by (simp add: STCalWB_reachesBarbST)
  with reflection rel have "P⇓<STCalWB SWB TWB>a"
    by blast
  thus "P⇓.a"
    by (simp add: STCalWB_reachesBarbST)
qed

lemma weak_respection_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes respection: "rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
      and rel:        "(P, Q) ∈ Rel"
  shows "P⇓.a = Q⇓.a"
proof (rule iffI)
  assume "P⇓.a"
  with respection rel show "Q⇓.a"
      using weak_preservation_of_barbs_in_barbed_encoding[where Rel="Rel"]
    by blast
next
  assume "Q⇓.a"
  with respection rel show "P⇓.a"
      using weak_reflection_of_barbs_in_barbed_encoding[where Rel="Rel"]
    by blast
qed

end

end