Theory Expressivity

text ‹In this file, we prove most results of section V: hyper-triples subsume many other triples,
as well as example 4.›

theory Expressivity
  imports ProgramHyperproperties
begin


subsection ‹Hoare Logic (HL)~\cite{HoareLogic}›

text ‹Definition 8›
definition HL where
  "HL P C Q ⟷ (∀σ σ' l. (l, σ) ∈ P ∧ (⟨C, σ⟩ → σ') ⟶ (l, σ') ∈ Q)"

lemma HLI:
  assumes "⋀σ σ' l. (l, σ) ∈ P ⟹ ⟨C, σ⟩ → σ' ⟹ (l, σ') ∈ Q"
  shows "HL P C Q"
  using assms HL_def by blast


lemma hoarifyI:
  assumes "⋀σ σ'. (σ, σ') ∈ S ⟹ σ ∈ P ⟹ σ' ∈ Q"
  shows "hoarify P Q S"
  by (metis assms hoarify_def prod.collapse)

definition HL_hyperprop where
  "HL_hyperprop P Q S ⟷ (∀l. ∀p ∈ S. (l, fst p) ∈ P ⟶ (l, snd p) ∈ Q)"

lemma connection_HL:
  "HL P C Q ⟷ HL_hyperprop P Q (set_of_traces C)" (is "?A ⟷ ?B")
proof
  assume ?A
  then show ?B
    by (simp add: HL_def HL_hyperprop_def set_of_traces_def)
next
  assume ?B
  show ?A
  proof (rule HLI)
    fix σ σ' l assume asm0: "(l, σ) ∈ P" "⟨C, σ⟩ → σ'"
    then have "(σ, σ') ∈ set_of_traces C"
      by (simp add: set_of_traces_def)
    then show "(l, σ') ∈ Q"
      using ‹HL_hyperprop P Q (set_of_traces C)› asm0(1) HL_hyperprop_def by fastforce
  qed
qed

text ‹Proposition 1›
theorem HL_expresses_hyperproperties:
  "∃H. (∀C. hypersat C H ⟷ HL P C Q) ∧ k_hypersafety 1 H"
proof -
  let ?H = "HL_hyperprop P Q"
  have "⋀C. hypersat C ?H ⟷ HL P C Q"
    by (simp add: connection_HL hypersat_def)
  moreover have "k_hypersafety 1 ?H"
  proof (rule k_hypersafetyI)
    fix S assume asm0: "¬ HL_hyperprop P Q S"
    then obtain l p where "p ∈ S" "(l, fst p) ∈ P" "(l, snd p) ∉ Q"
      using HL_hyperprop_def by blast
    let ?S = "{p}"
    have "max_k 1 ?S ∧ (∀S''. ?S ⊆ S'' ⟶ ¬ HL_hyperprop P Q S'')"
      by (metis (no_types, lifting) One_nat_def ‹(l, fst p) ∈ P› ‹(l, snd p) ∉ Q› card.empty card.insert
          empty_iff finite.intros(1) finite.intros(2) le_numeral_extra(4) max_k_def HL_hyperprop_def singletonI subsetD)
    then show "∃S'⊆S. max_k 1 S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ HL_hyperprop P Q S'')"
      by (meson ‹p ∈ S› empty_subsetI insert_subsetI)
  qed
  ultimately show ?thesis
    by blast
qed

text ‹Proposition 2›
theorem encoding_HL:
  "HL P C Q ⟷ (hyper_hoare_triple (over_approx P) C (over_approx Q))" (is "?A ⟷ ?B")
proof (rule iffI)
  show "?B ⟹ ?A"
  proof -
    assume asm0: ?B
    show ?A
    proof (rule HLI)
      fix σ σ' l
      assume asm1: "(l, σ) ∈ P" "⟨C, σ⟩ → σ'"
      then have "over_approx P {(l, σ)}"
        by (simp add: over_approx_def)
      then have "(over_approx Q) (sem C {(l, σ)})"
        using asm0 hyper_hoare_tripleE by auto
      then show "(l, σ') ∈ Q"
        by (simp add: asm1(2) in_mono in_sem over_approx_def)
    qed
  qed
next
  assume r: ?A
  show ?B
  proof (rule hyper_hoare_tripleI)
    fix S assume asm0: "over_approx P S"
    then have "S ⊆ P"
      by (simp add: over_approx_def)
    then have "sem C S ⊆ sem C P"
      by (simp add: sem_monotonic)
    then have "sem C S ⊆ Q"
      using r HL_def[of P C Q]
      by (metis (no_types, lifting) fst_conv in_mono in_sem snd_conv subrelI)      
    then show "over_approx Q (sem C S)"
      by (simp add: over_approx_def)
  qed
qed

lemma entailment_order_hoare:
  assumes "P ⊆ P'"
  shows "entails (over_approx P) (over_approx P')"
  by (simp add: assms entails_def over_approx_def subset_trans)


subsection ‹Cartesian Hoare Logic (CHL)~\cite{CHL16}›

text ‹Notation 3›
definition k_sem where
  "k_sem C states states' ⟷ (∀i. (fst (states i) = fst (states' i) ∧ single_sem C (snd (states i)) (snd (states' i))))"

lemma k_semI:
  assumes "⋀i. (fst (states i) = fst (states' i) ∧ single_sem C (snd (states i)) (snd (states' i)))"
  shows "k_sem C states states'"
  by (simp add: assms k_sem_def)

lemma k_semE:
  assumes "k_sem C states states'"
  shows "fst (states i) = fst (states' i) ∧ single_sem C (snd (states i)) (snd (states' i))"
  using assms k_sem_def by fastforce

text ‹Definition 9›
definition CHL where
  "CHL P C Q ⟷ (∀states. states ∈ P ⟶ (∀states'. k_sem C states states' ⟶ states' ∈ Q))"

lemma CHLI:
  assumes "⋀states states'. states ∈ P ⟹ k_sem C states states' ⟹ states' ∈ Q"
  shows "CHL P C Q"
  by (simp add: assms CHL_def)

lemma CHLE:
  assumes "CHL P C Q"
      and "states ∈ P"
      and "k_sem C states states'"
    shows "states' ∈ Q"
  using assms(1) assms(2) assms(3) CHL_def by fast

definition encode_CHL where
  "encode_CHL from_nat x P S ⟷ (∀states. (∀i. states i ∈ S ∧ fst (states i) x = from_nat i) ⟶ states ∈ P)"


lemma encode_CHLI:
  assumes "⋀states. (∀i. states i ∈ S ∧ fst (states i) x = from_nat i) ⟹ states ∈ P"
    shows "encode_CHL from_nat x P S"
  using assms(1) encode_CHL_def by force

lemma encode_CHLE:
  assumes "encode_CHL from_nat x P S"
      and "⋀i. states i ∈ S"
      and "⋀i. fst (states i) x = from_nat i"
    shows "states ∈ P"
  by (metis assms(1) assms(2) assms(3) encode_CHL_def)

lemma equal_change_lvar:
  assumes "fst φ x = y"
  shows "φ = ((fst φ)(x := y), snd φ)"
  using assms by fastforce


text ‹Proposition 3›
theorem encoding_CHL:
  assumes "not_free_var_of P x"
      and "not_free_var_of Q x"
      and "injective from_nat"
  shows "CHL P C Q ⟷ ⊨ {encode_CHL from_nat x P} C {encode_CHL from_nat x Q}" (is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule hyper_hoare_tripleI)
    fix S assume "encode_CHL from_nat x P S"
    then obtain asm0: "⋀states states'. (⋀i. states i ∈ S) ⟹ (⋀i.  fst (states i) x = from_nat i) ⟹ states ∈ P"
      by (simp add: encode_CHLE)

    show "encode_CHL from_nat x Q (sem C S)"
    proof (rule encode_CHLI)
      fix states'
      assume asm1: "∀i. states' i ∈ sem C S ∧ fst (states' i) x = from_nat i"

      let ?states = "λi. (fst (states' i), SOME σ. (fst (states' i), σ) ∈ S ∧ single_sem C σ (snd (states' i)))"

      show "states' ∈ Q"
        using ‹?A›
      proof (rule CHLE)
        show "?states ∈ P"
        proof (rule asm0)
          fix i
          let ?σ = "SOME σ. ((fst (states' i), σ) ∈ S ∧ ⟨C, σ⟩ → snd (states' i))"
          have r: "(fst (states' i), ?σ) ∈ S ∧ ⟨C, ?σ⟩ → snd (states' i)"
            using someI_ex[of "λσ. (fst (states' i), σ) ∈ S ∧ ⟨C, σ⟩ → snd (states' i)"] asm1 in_sem by blast
          then show "?states i ∈ S"
            by blast
          show "fst (?states i) x = from_nat i"
            by (simp add: asm1)
        qed
        show "k_sem C ?states states'"
        proof (rule k_semI)
          fix i
          let ?σ = "SOME σ. ((fst (states' i), σ) ∈ S ∧ ⟨C, σ⟩ → snd (states' i))"
          have r: "(fst (states' i), ?σ) ∈ S ∧ ⟨C, ?σ⟩ → snd (states' i)"
            using someI_ex[of "λσ. (fst (states' i), σ) ∈ S ∧ ⟨C, σ⟩ → snd (states' i)"] asm1 in_sem by blast
          then show "fst (?states i) = fst (states' i) ∧ ⟨C, snd (?states i)⟩ → snd (states' i)"
            by simp
        qed
      qed
    qed
  qed
next
  assume asm0: "⊨ {encode_CHL from_nat x P} C {encode_CHL from_nat x Q}"

  show "CHL P C Q"
  proof (rule CHLI)
    fix states states'
    assume asm1: "states ∈ P" "k_sem C states states'"

    let ?states = "λi. ((fst (states i))(x := from_nat i), snd (states i))"
    let ?states' = "λi. ((fst (states i))(x := from_nat i), snd (states' i))"
    let ?S = "range ?states"

    have "encode_CHL from_nat x Q (sem C ?S)"
      using asm0
    proof (rule hyper_hoare_tripleE)
      show "encode_CHL from_nat x P ?S"
      proof (rule encode_CHLI)
        fix f assume asm2: "∀i. f i ∈ ?S ∧ fst (f i) x = from_nat i"
        have "f = ?states"
        proof (rule ext)
          fix i
          obtain j where j_def: "f i = ((fst (states j))(x := from_nat j), snd (states j))"
            using asm2 by fastforce
          then have "from_nat j = from_nat i"
            by (metis asm2 fst_conv fun_upd_same)
          then show "f i = ((fst (states i))(x := from_nat i), snd (states i))"
            by (metis j_def assms(3) injective_def)
        qed
        moreover have "?states ∈ P"
          using assms(1)
        proof (rule not_free_var_ofE)
          show "states ∈ P"
            using asm1(1) by simp
          fix i
          show "differ_only_by (fst (states i)) (fst ((fst (states i))(x := from_nat i), snd (states i))) x"
            by (simp add: differ_only_by_def)
          show "snd (states i) = snd ((fst (states i))(x := from_nat i), snd (states i))"
            by simp
        qed
        ultimately show "f ∈ P"
          by meson
      qed
    qed
    then have "?states' ∈ Q"
    proof (rule encode_CHLE)
      fix i
      show "fst ((fst (states i))(x := from_nat i), snd (states' i)) x = from_nat i"
        by simp
      moreover have "single_sem C (snd (?states i)) (snd (?states' i))"
        using asm1(2) k_sem_def by fastforce
      ultimately show "((fst (states i))(x := from_nat i), snd (states' i)) ∈ sem C ?S"
        using in_sem by fastforce
    qed
    show "states' ∈ Q"
      using assms(2) 
    proof (rule not_free_var_ofE[of Q x])
      show "?states' ∈ Q"
        by (simp add: ‹(λi. ((fst (states i))(x := from_nat i), snd (states' i))) ∈ Q›)
      fix i show "differ_only_by (fst ((fst (states i))(x := from_nat i), snd (states' i))) (fst (states' i)) x"
        by (metis asm1(2) diff_by_update fst_conv k_sem_def)
    qed (auto)
  qed
qed

definition CHL_hyperprop where
  "CHL_hyperprop P Q S ⟷ (∀l p. (∀i. p i ∈ S) ∧ (λi. (l i, fst (p i))) ∈ P ⟶ (λi. (l i, snd (p i))) ∈ Q)"

lemma CHL_hyperpropI:
  assumes "⋀l p. (∀i. p i ∈ S) ∧ (λi. (l i, fst (p i))) ∈ P ⟹ (λi. (l i, snd (p i))) ∈ Q"
  shows "CHL_hyperprop P Q S"
  by (simp add: assms CHL_hyperprop_def)

lemma CHL_hyperpropE:
  assumes "CHL_hyperprop P Q S"
      and "⋀i. p i ∈ S"
      and "(λi. (l i, fst (p i))) ∈ P"
    shows "(λi. (l i, snd (p i))) ∈ Q"
  using assms(1) assms(2) assms(3) CHL_hyperprop_def by blast

text ‹Proposition 10›
theorem CHL_hyperproperty:
  "hypersat C (CHL_hyperprop P Q) ⟷ CHL P C Q" (is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule CHLI)
    fix states states'
    assume asm0: "states ∈ P" "k_sem C states states'"
    let ?p = "λi. (snd (states i), snd (states' i))"
    let ?l = "λi. fst (states i)"

    have "range ?p ⊆ set_of_traces C"
    proof (rule subsetI)
      fix x assume "x ∈ range ?p"
      then obtain i where "x = (snd (states i), snd (states' i))"
        by blast
      then show "x ∈ set_of_traces C"
        by (metis (mono_tags, lifting) CollectI asm0(2) k_sem_def set_of_traces_def)
    qed
    have "(λi. (?l i, snd (?p i))) ∈ Q"
    proof (rule CHL_hyperpropE)
      show "CHL_hyperprop P Q (range ?p)"
      proof (rule CHL_hyperpropI)
        fix l p assume asm1: "(∀i. p i ∈ range (λi. (snd (states i), snd (states' i)))) ∧ (λi. (l i, fst (p i))) ∈ P"
        then show "(λi. (l i, snd (p i))) ∈ Q"
          using CHL_hyperprop_def[of P Q "set_of_traces C"] ‹hypersat C (CHL_hyperprop P Q)›
            ‹range (λi. (snd (states i), snd (states' i))) ⊆ set_of_traces C› hypersat_def subset_iff
          by blast
      qed          
      show "(λi. (fst (states i), fst (snd (states i), snd (states' i)))) ∈ P"
        by (simp add: asm0(1))
      fix i show "(snd (states i), snd (states' i)) ∈ range (λi. (snd (states i), snd (states' i)))"
        by blast
    qed
    moreover have "states' = (λi. (?l i, snd (?p i)))"
    proof (rule ext)
      fix i show "states' i = (fst (states i), snd (snd (states i), snd (states' i)))"
        by (metis asm0(2) k_sem_def prod.exhaust_sel sndI)
    qed
    ultimately show "states' ∈ Q"
      by auto
  qed
next
  assume asm0: "CHL P C Q"
  have "CHL_hyperprop P Q (set_of_traces C)"
  proof (rule CHL_hyperpropI)
    fix l p assume asm1: "(∀i. p i ∈ set_of_traces C) ∧ (λi. (l i, fst (p i))) ∈ P"

    show "(λi. (l i, snd (p i))) ∈ Q"
      using asm0
    proof (rule CHLE)
      show "(λi. (l i, fst (p i))) ∈ P"
        by (simp add: asm1)
      show "k_sem C (λi. (l i, fst (p i))) (λi. (l i, snd (p i)))"
      proof (rule k_semI)
        fix i show "fst (l i, fst (p i)) = fst (l i, snd (p i)) ∧ ⟨C, snd (l i, fst (p i))⟩ → snd (l i, snd (p i))"
          using asm1 in_set_of_traces by fastforce
      qed
    qed
  qed
  then show "hypersat C (CHL_hyperprop P Q)"
    by (simp add: hypersat_def)
qed



theorem k_hypersafety_HL_hyperprop:
  fixes P :: "('i ⇒ ('lvar, 'lval, 'pvar, 'pval) state) set"
  assumes "finite (UNIV :: 'i set)"
      and "card (UNIV :: 'i set) = k"
    shows "k_hypersafety k (CHL_hyperprop P Q)"
proof (rule k_hypersafetyI)
  fix S
  assume "¬ CHL_hyperprop P Q S"
  then obtain l p where asm0: "∀i. p i ∈ S" "(λi. (l i, fst (p i))) ∈ P"
    "(λi. (l i, snd (p i))) ∉ Q"
    using CHL_hyperprop_def by blast
  let ?S = "range p"
  have "max_k k ?S"
    by (metis assms(1) assms(2) card_image_le finite_imageI max_k_def)
  moreover have "⋀S''. ?S ⊆ S'' ⟹ ¬ CHL_hyperprop P Q S''"
    by (meson asm0(2) asm0(3) CHL_hyperprop_def range_subsetD)
  ultimately show "∃S'⊆S. max_k k S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ CHL_hyperprop P Q S'')"
    by (meson asm0(1) image_subsetI)
qed



subsection ‹Incorrectness Logic~\cite{IncorrectnessLogic} or Reverse Hoare Logic~\cite{ReverseHL} (IL))›

text ‹Definition 11›

definition IL where
  "IL P C Q ⟷ Q ⊆ sem C P"

lemma equiv_def_incorrectness:
  "IL P C Q ⟷ (∀l σ'. (l, σ') ∈ Q ⟶ (∃σ. (l, σ) ∈ P ∧ ⟨C, σ⟩ → σ'))"
  by (simp add: in_sem IL_def subset_iff)

definition IL_hyperprop where
  "IL_hyperprop P Q S ⟷ (∀l σ'. (l, σ') ∈ Q ⟶ (∃σ. (l, σ) ∈ P ∧ (σ, σ') ∈ S))"


lemma IL_hyperpropI:
  assumes "⋀l σ'. (l, σ') ∈ Q ⟹ (∃σ. (l, σ) ∈ P ∧ (σ, σ') ∈ S)"
  shows "IL_hyperprop P Q S"
  by (simp add: assms IL_hyperprop_def)

text ‹Proposition 11›
lemma IL_expresses_hyperproperties:
  "IL P C Q ⟷ IL_hyperprop P Q (set_of_traces C)" (is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule IL_hyperpropI)
    fix l σ' assume asm0: "(l, σ') ∈ Q"
    then obtain σ where "(l, σ) ∈ P" "single_sem C σ σ'"
      using ‹IL P C Q› equiv_def_incorrectness by blast
    then show "∃σ. (l, σ) ∈ P ∧ (σ, σ') ∈ set_of_traces C"
      using set_of_traces_def by auto
  qed
next
  assume ?B
  have "Q ⊆ sem C P"
  proof (rule subsetPairI)
    fix l σ' assume "(l, σ') ∈ Q"
    then obtain σ where "(σ, σ') ∈ set_of_traces C" "(l, σ) ∈ P"
      by (meson ‹IL_hyperprop P Q (set_of_traces C)› IL_hyperprop_def)
    then show "(l, σ') ∈ sem C P"
      using in_set_of_traces_then_in_sem by blast
  qed
  then show ?A
    by (simp add: IL_def)
qed


lemma IL_consequence:
  assumes "IL P C Q"
      and "(l, σ') ∈ Q"
    shows "∃σ. (l, σ) ∈ P ∧ single_sem C σ σ'"
  using assms(1) assms(2) equiv_def_incorrectness by blast

text ‹Proposition 4›
theorem encoding_IL:
  "IL P C Q ⟷ (hyper_hoare_triple (under_approx P) C (under_approx Q))" (is "?A ⟷ ?B")
proof (rule iffI)
  show "?B ⟹ ?A"
  proof -
    assume ?B
    then have "under_approx Q (sem C P)"
      by (simp add: hyper_hoare_triple_def under_approx_def)
    then show ?A
      by (simp add: IL_def under_approx_def)
  qed
  assume ?A
  then show ?B
    by (simp add: hyper_hoare_triple_def sem_monotonic IL_def under_approx_def subset_trans)
qed

lemma entailment_order_reverse_hoare:
  assumes "P ⊆ P'"
  shows "entails (under_approx P') (under_approx P)"
  by (simp add: assms dual_order.trans entails_def under_approx_def)

definition incorrectify where
  "incorrectify p = under_approx { σ |σ. p σ}"

lemma incorrectifyI:
  assumes "⋀σ. p σ ⟹ σ ∈ S"
  shows "incorrectify p S"
  by (metis assms incorrectify_def mem_Collect_eq subsetI under_approx_def)

lemma incorrectifyE:
  assumes "incorrectify p S"
      and "p σ"
    shows "σ ∈ S"
  by (metis CollectI assms(1) assms(2) in_mono incorrectify_def under_approx_def)

lemma simple_while_incorrectness:
  assumes "⋀n. hyper_hoare_triple (incorrectify (p n)) C (incorrectify (p (Suc n)))"
  shows "hyper_hoare_triple (incorrectify (p 0)) (While C) (incorrectify (λσ. ∃n. p n σ))" 
proof (rule consequence_rule)
  show "entails (incorrectify (p 0)) (incorrectify (p 0))"
    by (simp add: entailsI)
  show "hyper_hoare_triple (incorrectify (p 0)) (While C) (natural_partition (λn. incorrectify (p n)))"
    by (meson assms while_rule)

  have "entails (incorrectify (λσ. ∃n. p n σ)) (natural_partition (λn. incorrectify (p n)))"
  proof (rule entailsI)
    fix S assume asm0: "incorrectify (λσ. ∃n. p n σ) S"
    then have "under_approx { σ |σ n. p n σ} S"
      by (metis incorrectify_def)
    let ?F = "λn. S"
    show "natural_partition (λn. incorrectify (p n)) S"
    proof (rule natural_partitionI)
      show "⋀n. incorrectify (p n) (?F n)"
        by (metis asm0 incorrectifyE incorrectifyI)
      show "S = ⋃ (range ?F)"
        by simp
    qed
  qed


  show "entails (natural_partition (λn. incorrectify (p n))) (incorrectify (λσ. ∃n. p n σ))"
  proof (rule entailsI)
    fix S assume asm0: "natural_partition (λn. incorrectify (p n)) S"
    then obtain F where "S = (⋃n. F n)" "⋀n. incorrectify (p n) (F n)"
      using natural_partitionE by blast
    show "incorrectify (λσ. ∃n. p n σ) S"
    proof (rule incorrectifyI)
      fix σ assume "∃n. p n σ"
      then obtain n where "p n σ"
        by blast
      then have "σ ∈ F n"
        by (meson ‹⋀n. incorrectify (p n) (F n)› incorrectifyE)
      then show "σ ∈ S"
        using ‹S = ⋃ (range F)› by blast
    qed
  qed
qed

definition sat_for_l where
  "sat_for_l l P ⟷ (∃σ. (l, σ) ∈ P)"

theorem incorrectness_hyperliveness:
  assumes "⋀l. sat_for_l l Q ⟹ sat_for_l l P"
  shows "hyperliveness (IL_hyperprop P Q)"
proof (rule hyperlivenessI)
  fix S
  let ?S = "S ∪ {(σ, σ') |σ σ' l. (l, σ') ∈ Q ∧ (l, σ) ∈ P }"
  have "IL_hyperprop P Q ?S"
  proof (rule IL_hyperpropI)
    fix l σ'
    assume asm0: "(l, σ') ∈ Q"
    then obtain σ where "(l, σ) ∈ P"
      by (meson assms sat_for_l_def)
    then show "∃σ. (l, σ) ∈ P ∧ (σ, σ') ∈ ?S"
      using asm0 by auto
  qed
  then show "∃S'. S ⊆ S' ∧ IL_hyperprop P Q S'"
    by auto
qed


subsection ‹Relational Incorrectness Logic~\cite{InsecurityLogic} (RIL)›

text ‹Definition 11›
definition RIL where
  "RIL P C Q ⟷ (∀states' ∈ Q. ∃states ∈ P. k_sem C states states')"

lemma RILI:
  assumes "⋀states'. states' ∈ Q ⟹ (∃states ∈ P. k_sem C states states')"
  shows "RIL P C Q"
  by (simp add: assms RIL_def)

lemma RILE:
  assumes "RIL P C Q"
      and "states' ∈ Q"
    shows "∃states ∈ P. k_sem C states states'"
  using assms(1) assms(2) RIL_def by blast


definition RIL_hyperprop where
  "RIL_hyperprop P Q S ⟷ (∀l states'. (λi. (l i, states' i)) ∈ Q
         ⟶ (∃states. (λi. (l i, states i)) ∈ P ∧ (∀i. (states i, states' i) ∈ S)))"

lemma RIL_hyperpropI:
  assumes "⋀l states'. (λi. (l i, states' i)) ∈ Q ⟹ (∃states. (λi. (l i, states i)) ∈ P ∧ (∀i. (states i, states' i) ∈ S))"
  shows "RIL_hyperprop P Q S"
  by (simp add: assms RIL_hyperprop_def)


lemma RIL_hyperpropE:
  assumes "RIL_hyperprop P Q S"
      and "(λi. (l i, states' i)) ∈ Q"
    shows "∃states. (λi. (l i, states i)) ∈ P ∧ (∀i. (states i, states' i) ∈ S)"
  using assms(1) assms(2) RIL_hyperprop_def by blast

lemma useful:
  "states' = (λi. ((fst ∘ states') i, (snd ∘ states') i))"
proof (rule ext)
  fix i show "states' i = ((fst ∘ states') i, (snd ∘ states') i)"
    by auto
qed

text ‹Proposition 12›
theorem RIL_expresses_hyperproperties:
  "hypersat C (RIL_hyperprop P Q) ⟷ RIL P C Q" (is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule RILI)
    fix states' assume asm0: "states' ∈ Q"
    then obtain states where asm0: "(λi. ((fst ∘ states') i, states i)) ∈ P ∧ (∀i. (states i, (snd ∘ states') i) ∈ set_of_traces C)"
      using RIL_hyperpropE[of P Q "set_of_traces C" "fst ∘ states'" "snd ∘ states'"] ‹?A›
      using hypersat_def by auto

    moreover have "k_sem C (λi. ((fst ∘ states') i, states i)) states'"
    proof (rule k_semI)
      fix i 
      have "⟨C, snd ((fst ∘ states') i, states i)⟩ → snd (states' i)"
        using calculation set_of_traces_def by auto
      then show "fst ((fst ∘ states') i, states i) = fst (states' i) ∧ ⟨C, snd ((fst ∘ states') i, states i)⟩ → snd (states' i)"
        by simp
    qed
    ultimately show "∃states∈P. k_sem C states states'"
      by fast
  qed
next
  assume ?B
  have "RIL_hyperprop P Q (set_of_traces C)"
  proof (rule RIL_hyperpropI)
    fix l states'
    assume asm0: "(λi. (l i, states' i)) ∈ Q"
    then obtain states where "states ∈ P" "k_sem C states (λi. (l i, states' i))"
      using ‹RIL P C Q› RILE by blast
    moreover have "(λi. (l i, (snd ∘ states) i)) = states"
    proof (rule ext)
      fix i show "(l i, (snd ∘ states) i) = states i"
        by (metis calculation(2) comp_apply fst_conv k_sem_def surjective_pairing)
    qed
    moreover have "⋀i. ((snd ∘ states) i, states' i) ∈ set_of_traces C"
      by (metis (mono_tags, lifting) calculation(2) comp_apply in_set_of_traces k_sem_def snd_conv)
    ultimately show "∃states. (λi. (l i, states i)) ∈ P ∧ (∀i. (states i, states' i) ∈ set_of_traces C)"
      by force
  qed
  then show ?A
    using hypersat_def by blast
qed

definition k_sat_for_l where
  "k_sat_for_l l P ⟷ (∃σ. (λi. (l i, σ i)) ∈ P)"

theorem RIL_hyperprop_hyperlive:
  assumes "⋀l. k_sat_for_l l Q ⟹ k_sat_for_l l P"
  shows "hyperliveness (RIL_hyperprop P Q)"
proof (rule hyperlivenessI)
  fix S
  have "RIL_hyperprop P Q UNIV"
    by (meson assms RIL_hyperpropI iso_tuple_UNIV_I k_sat_for_l_def)
  then show "∃S'. S ⊆ S' ∧ RIL_hyperprop P Q S'"
    by blast
qed


definition strong_pre_insec where
  "strong_pre_insec from_nat x c P S ⟷ (∀states ∈ P.
(∀i. fst (states i) x = from_nat i) ⟶ (∃r. ∀i. ((fst (states i))(c := r), snd (states i)) ∈ S)) ∧
(∀states. (∀i. states i ∈ S) ∧ (∀i. fst (states i) x = from_nat i) ∧
(∀i j. fst (states i) c = fst (states j) c) ⟶ states ∈ P)"

lemma strong_pre_insecI:
  assumes "⋀states. states ∈ P ⟹ (∀i. fst (states i) x = from_nat i)
  ⟹ (∃r. ∀i. ((fst (states i))(c := r), snd (states i)) ∈ S)"
      and "⋀states. (∀i. states i ∈ S) ⟹ (∀i. fst (states i) x = from_nat i) ⟹ (∀i j. fst (states i) c = fst (states j) c) ⟹ states ∈ P"
    shows "strong_pre_insec from_nat x c P S"
  by (simp add: assms(1) assms(2) strong_pre_insec_def)

lemma strong_pre_insecE:
  assumes "strong_pre_insec from_nat x c P S"
      and "⋀i. states i ∈ S"
      and "⋀i. fst (states i) x = from_nat i"
      and "⋀i j. fst (states i) c = fst (states j) c"
    shows "states ∈ P"
  by (meson assms(1) assms(2) assms(3) assms(4) strong_pre_insec_def)


definition pre_insec where
  "pre_insec from_nat x c P S ⟷ (∀states ∈ P.
(∀i. fst (states i) x = from_nat i)
  ⟶ (∃r. ∀i. ((fst (states i))(c := r), snd (states i)) ∈ S))"

lemma pre_insecI:
  assumes "⋀states. states ∈ P ⟹ (∀i. fst (states i) x = from_nat i)
  ⟹ (∃r. ∀i. ((fst (states i))(c := r), snd (states i)) ∈ S)"
    shows "pre_insec from_nat x c P S"
  by (simp add: assms(1) pre_insec_def)

lemma strong_pre_implies_pre:
  assumes "strong_pre_insec from_nat x c P S"
  shows "pre_insec from_nat x c P S"
  by (meson assms pre_insecI strong_pre_insec_def)

lemma pre_insecE:
  assumes "pre_insec from_nat x c P S"
      and "states ∈ P"
      and "⋀i. fst (states i) x = from_nat i"
    shows "∃r. ∀i. ((fst (states i))(c := r), snd (states i)) ∈ S"
  by (meson assms(1) assms(2) assms(3) pre_insec_def)




definition post_insec where
  "post_insec from_nat x c Q S ⟷ (∀states ∈ Q. (∀i. fst (states i) x = from_nat i)
  ⟶ (∃r. (∀i. ((fst (states i))(c := r), snd (states i)) ∈ S)))"

lemma post_insecE:
  assumes "post_insec from_nat x c Q S"
      and "states ∈ Q"
      and "⋀i. fst (states i) x = from_nat i"
    shows "∃r. (∀i. ((fst (states i))(c := r), snd (states i)) ∈ S)"
  by (meson assms(1) assms(2) assms(3) post_insec_def)

lemma post_insecI:
  assumes "⋀states. states ∈ Q ⟹ (∀i. fst (states i) x = from_nat i)
  ⟹ (∃r. (∀i. ((fst (states i))(c := r), snd (states i)) ∈ S))"
  shows "post_insec from_nat x c Q S"
  by (simp add: assms post_insec_def)

lemma same_pre_post:
  "pre_insec from_nat x c Q S ⟷ post_insec from_nat x c Q S"
  by (simp add: post_insec_def pre_insec_def)

theorem can_be_sat:
  fixes x :: "'lvar"
  assumes "⋀l l' σ. (λi. (l i, σ i)) ∈ P ⟷ (λi. (l' i, σ i)) ∈ P"  (* P does not depend on logical variables *)
      and "injective (indexify :: (('a ⇒ ('pvar ⇒ 'pval)) ⇒ 'lval))" (* |lval| ≥ |PStates^k| *)
      and "x ≠ c"
      and "injective from_nat"
    shows "sat (strong_pre_insec from_nat x c (P :: ('a ⇒ ('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set))"
proof -

  let ?S = "⋃states∈P. { (((fst (states i))(x := from_nat i))(c := indexify (λi. snd (states i))), snd (states i)) |i. True}"

  have "strong_pre_insec from_nat x c P ?S"
  proof (rule strong_pre_insecI)
    fix states
    assume asm0: "states ∈ P" "∀i. fst (states i) x = from_nat i"
    define r where "r = indexify (λi. snd (states i))"
    have "⋀i. ((fst (states i))(c := r), snd (states i)) ∈ { (((fst (states i))(x := from_nat i))(c := indexify (λi. snd (states i))), snd (states i)) |i. True}"
    proof -
      fix i
      show "((fst (states i))(c := r), snd (states i)) ∈ { (((fst (states i))(x := from_nat i))(c := indexify (λi. snd (states i))), snd (states i)) |i. True}"
        using asm0(2) r_def by fastforce
    qed
    then show "∃r. ∀i. ((fst (states i))(c := r), snd (states i)) ∈ ?S"
      by (meson UN_I asm0(1))
  next
    fix states
    
    assume asm0: "∀i. states i ∈ ?S" "∀i. fst (states i) x = from_nat i" "∀i j. fst (states i) c = fst (states j) c"

    let ?P = "λi states'. states' ∈ P ∧ states i ∈ { (((fst (states' i))(x := from_nat i))(c := indexify (λi. snd (states' i))), snd (states' i)) |i. True}"

    let ?states = "λi. SOME states'. ?P i states'"
    have r: "⋀i. ?P i (?states i)"
    proof -
      fix i 
      show "?P i (?states i)"
      proof (rule someI_ex[of "?P i"])
        show "∃states'. states' ∈ P ∧ states i ∈ { (((fst (states' i))(x := from_nat i))(c := indexify (λi. snd (states' i))), snd (states' i)) |i. True}"
          using asm0(1) by fastforce
      qed
    qed
    moreover have rr: "⋀i. fst (states i) c = indexify (λj. snd (?states i j)) ∧ snd (?states i i) = snd (states i)"
    proof -
      fix i
      obtain j where j_def: "states i = (((fst ((?states i) j))(x := from_nat j))(c := indexify (λk. snd ((?states i) k))), snd ((?states i) j))"
        using r[of i] by blast
      then have r1: "snd (?states i j) = snd (states i)"
        by (metis (no_types, lifting) snd_conv)
      then have "from_nat i = from_nat j"
        by (metis (no_types, lifting) j_def asm0(2) assms(3) fst_conv fun_upd_same fun_upd_twist)
      then have "i = j"
        by (meson assms(4) injective_def)
      show "fst (states i) c = indexify (λj. snd (?states i j)) ∧ snd (?states i i) = snd (states i)"
      proof
        show "fst (states i) c = indexify (λj. snd (?states i j))"
          by (metis (no_types, lifting) j_def fst_conv fun_upd_same)
        show "snd (?states i i) = snd (states i)"
          using ‹i = j› r1 by blast
      qed
    qed
    moreover have r0: "⋀i j. (λn. snd (?states i n)) = (λn. snd (?states j n))"
    proof -
      fix i j
      have "indexify (λn. snd (?states i n)) = indexify (λn. snd (?states j n))"
        using asm0(3) rr by fastforce
      then show "(λn. snd (?states i n)) = (λn. snd (?states j n))"
        by (meson assms(2) injective_def)
    qed
    obtain k :: 'a where "True" by blast
    then have "?states k ∈ P"
      using UN_iff[of _ "λstates. {((fst (states i))(x := from_nat i, c := indexify (λi. snd (states i))), snd (states i)) |i. True}" P]
        asm0(1) someI_ex[of "λy. y ∈ P ∧ states k ∈ {((fst (y i))(x := from_nat i, c := indexify (λi. snd (y i))), snd (y i)) |i. True}"]
      by fast
    moreover have "⋀i. snd (?states k i) = snd (states i)"
    proof -
      fix i 
      have "snd (?states i i) = snd (states i)"
        using rr by blast
      moreover have "(λn. snd (?states i n)) i = (λn. snd (?states k n)) i"
        by (metis r0)
      ultimately show "snd (?states k i) = snd (states i)"
        by auto
    qed
    moreover have "(λi. ((λi. fst (?states k i)) i, (λi. snd (states i)) i)) ∈ P ⟷ (λi. ((λi. fst (states i)) i, (λi. snd (states i)) i)) ∈ P" 
      using assms(1) by fast
    moreover have "(λi. ((λi. fst (states i)) i, (λi. snd (states i)) i)) = states"
    proof (rule ext)
      fix i show "(fst (states i), snd (states i)) = states i"
        by simp
    qed
    moreover have "(λi. ((λi. fst (?states k i)) i, (λi. snd (states i)) i)) = ?states k"
    proof (rule ext)
      fix i show "(λi. ((λi. fst (?states k i)) i, (λi. snd (states i)) i)) i = ?states k i"
        by (metis (no_types, lifting) calculation(4) prod.exhaust_sel)
    qed
    ultimately show "states ∈ P" by argo
  qed
  then show "sat (strong_pre_insec from_nat x c P)"
    by (meson sat_def)
qed

theorem encode_insec:
  assumes "injective from_nat"
      and "sat (strong_pre_insec from_nat x c (P :: ('a ⇒ ('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set))"
      and "not_free_var_of P x ∧ not_free_var_of P c"
      and "not_free_var_of Q x ∧ not_free_var_of Q c"
      and "c ≠ x"

    shows "RIL P C Q ⟷ ⊨ {pre_insec from_nat x c P} C {post_insec from_nat x c Q}" (is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule hyper_hoare_tripleI)
    fix S assume asm0: "pre_insec from_nat x c P S"

    show "post_insec from_nat x c Q (sem C S)"
    proof (rule post_insecI)
      fix states' assume asm1: "states' ∈ Q" "∀i. fst (states' i) x = from_nat i"
      then obtain states where "states ∈ P" "k_sem C states states'"
        using ‹RIL P C Q› RILE by blast
      then obtain r where asm2: "⋀i. ((fst (states i))(c := r), snd (states i)) ∈ S"
        using pre_insecE[of from_nat x c P S states]
        by (metis asm0 asm1(2) k_sem_def)
      then show "∃r. ∀i. ((fst (states' i))(c := r), snd (states' i)) ∈ sem C S"
        by (metis (mono_tags, opaque_lifting) ‹k_sem C states states'› k_sem_def single_step_then_in_sem)
    qed
  qed
next
  assume asm0: ?B
  show ?A
  proof (rule RILI)
    fix states' assume asm1: "states' ∈ Q"
    obtain S where asm2: "strong_pre_insec from_nat x c P S"
      by (meson assms(2) sat_def)
    then have asm3: "post_insec from_nat x c Q (sem C S)"
      by (meson asm0 hyper_hoare_tripleE strong_pre_implies_pre)

    let ?states' = "λi. ((fst (states' i))(x := from_nat i), snd (states' i))"
    have "?states' ∈ Q"
      by (metis (no_types, lifting) asm1 assms(4) diff_by_update fstI not_free_var_of_def snd_conv)
    then obtain r where r_def: "⋀i. ((fst (?states' i))(c := r), snd (?states' i)) ∈ sem C S"
      using asm3 post_insecE[of from_nat x c Q] by fastforce

    let ?states = "λi. SOME σ. ((fst (?states' i))(c := r), σ) ∈ S ∧ single_sem C σ (snd (?states' i))"

    have asm4: "⋀i. ((fst (?states' i))(c := r), (?states i)) ∈ S ∧ single_sem C (?states i) (snd (?states' i))"
    proof -
      fix i 
      have "∃σ. ((fst (?states' i))(c := r), σ) ∈ S ∧ single_sem C σ (snd (?states' i))"
        by (metis r_def fst_conv in_sem snd_conv)
      then show "((fst (?states' i))(c := r), (?states i)) ∈ S ∧ single_sem C (?states i) (snd (?states' i))"
        using someI_ex[of "λσ. ((fst (?states' i))(c := r), σ) ∈ S ∧ single_sem C σ (snd (?states' i))"]
        by blast
    qed
    moreover have r0: "(λi. ((fst (?states' i))(c := r), (?states i))) ∈ P"
      using asm2
    proof (rule strong_pre_insecE)
      fix i
      show "(λi. ((fst (?states' i))(c := r), (?states i))) i ∈ S"
        using calculation by blast
      show "fst ((λi. ((fst (?states' i))(c := r), (?states i))) i) x = from_nat i"
        using assms(5) by auto
      fix j
      show "fst ((λi. ((fst (?states' i))(c := r), (?states i))) i) c = fst ((λi. ((fst (?states' i))(c := r), (?states i))) j) c"
        by fastforce
    qed
    have r1: "(λi. (((fst (?states' i))(c := r))(x := fst (states' i) x), (?states i))) ∈ P"
    proof (rule not_free_var_ofE[of P x])
      show "(λi. ((fst (?states' i))(c := r), (?states i))) ∈ P"
        using r0 by fastforce
      show "not_free_var_of P x"
        by (simp add: assms(3))
      fix i
      show "differ_only_by
          (fst ((fst ((fst (states' i))(x := from_nat i), snd (states' i)))(c := r), ?states i))
          (fst ((fst ((fst (states' i))(x := from_nat i), snd (states' i)))(c := r, x := fst (states' i) x), ?states i)) x"
        by (metis (mono_tags, lifting) diff_by_comm diff_by_update fst_conv)
    qed (auto)
    have "(λi. ((((fst (?states' i))(c := r))(x := fst (states' i) x))(c := fst (states' i) c), (?states i))) ∈ P"
    proof (rule not_free_var_ofE)
      show "(λi. (((fst (?states' i))(c := r))(x := fst (states' i) x), (?states i))) ∈ P"
        using r1 by fastforce
      show "not_free_var_of P c"
        by (simp add: assms(3))
      fix i show "differ_only_by
          (fst ((fst ((fst (states' i))(x := from_nat i), snd (states' i)))(c := r, x := fst (states' i) x), ?states i))
          (fst ((fst ((fst (states' i))(x := from_nat i), snd (states' i)))(c := r, x := fst (states' i) x, c := fst (states' i) c), ?states i))
          c"
        by (metis (mono_tags, lifting) diff_by_comm diff_by_update fst_conv)
    qed (auto)
    moreover have "(λi. ((((fst (?states' i))(c := r))(x := fst (states' i) x))(c := fst (states' i) c), (?states i)))
      = (λi. (fst (states' i), (?states i)))"
    proof (rule ext)
      fix i show "(λi. ((((fst (?states' i))(c := r))(x := fst (states' i) x))(c := fst (states' i) c), (?states i))) i
      = (λi. (fst (states' i), (?states i))) i"
        by force
    qed
    moreover have "k_sem C (λi. (fst (states' i), (?states i))) states'"
    proof (rule k_semI)
      fix i
      show "(fst ((λi. (fst (states' i), (?states i))) i) = fst (states' i) ∧
      single_sem C (snd ((λi. (fst (states' i), (?states i))) i)) (snd (states' i)))"
        using asm4 by auto
    qed
    ultimately show "∃states∈P. k_sem C states states'"
      by auto
  qed
qed


text ‹Proposition 5›

theorem encoding_RIL:
  fixes x :: "'lvar"
  assumes "⋀l l' σ. (λi. (l i, σ i)) ∈ P ⟷ (λi. (l' i, σ i)) ∈ P"  (* P does not depend on logical variables *)
      and "injective (indexify :: (('a ⇒ ('pvar ⇒ 'pval)) ⇒ 'lval))" (* |lval| ≥ |PStates^k| *)
      and "c ≠ x"
      and "injective from_nat"
      and "not_free_var_of (P :: ('a ⇒ ('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set) x ∧ not_free_var_of P c"
      and "not_free_var_of Q x ∧ not_free_var_of Q c"
    shows "RIL P C Q ⟷ ⊨ {pre_insec from_nat x c P} C {post_insec from_nat x c Q}" (is "?A ⟷ ?B")
proof (rule encode_insec)
  show "sat (strong_pre_insec from_nat x c (P :: ('a ⇒ ('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set))"
  proof (rule can_be_sat)
    show "injective (indexify :: (('a ⇒ ('pvar ⇒ 'pval)) ⇒ 'lval))"
      by (simp add: assms(2))
    show "x ≠ c"
      using assms(3) by auto
  qed (auto simp add: assms)
qed (auto simp add: assms)


subsection ‹Forward Underapproximation (FU)›

text ‹As employed by Outcome Logic~\cite{OutcomeLogic}›

text ‹Definition 12›
definition FU where
  "FU P C Q ⟷ (∀l. ∀σ. (l, σ) ∈ P ⟶ (∃σ'. single_sem C σ σ' ∧ (l, σ') ∈ Q))"

lemma FUI:
  assumes "⋀σ l. (l, σ) ∈ P ⟹ (∃σ'. single_sem C σ σ' ∧ (l, σ') ∈ Q)"
  shows "FU P C Q"
  by (simp add: assms FU_def)

definition encode_FU where
  "encode_FU P S ⟷ P ∩ S ≠ {}"

text ‹Proposition 6›
theorem encoding_FU:
  "FU P C Q ⟷ ⊨ {encode_FU P} C {encode_FU Q}" (is "?A ⟷ ?B")
proof
  show "?B ⟹ ?A"
  proof -
    assume ?B
    show ?A
    proof (rule FUI)
      fix σ l
      assume asm: "(l, σ) ∈ P"
      then have "encode_FU P {(l, σ)}"
        by (simp add: encode_FU_def)
      then have "Q ∩ sem C {(l, σ)} ≠ {}"
        using ‹⊨ {encode_FU P} C {encode_FU Q}› hyper_hoare_tripleE encode_FU_def by blast
      then obtain φ' where "φ' ∈ Q" "φ' ∈ sem C {(l, σ)}"
        by blast
      then show "∃σ'. single_sem C σ σ' ∧ (l, σ') ∈ Q"
        by (metis fst_conv in_sem prod.collapse singletonD snd_conv)
    qed
  qed
  assume ?A
  show ?B
  proof (rule hyper_hoare_tripleI)
    fix S assume "encode_FU P S"
    then obtain l σ where "(l, σ) ∈ P ∩ S"
      by (metis Expressivity.encode_FU_def ex_in_conv surj_pair)
    then obtain σ' where "single_sem C σ σ' ∧ (l, σ') ∈ Q"
      by (meson IntD1 ‹FU P C Q› FU_def)
    then show "encode_FU Q (sem C S)"
      using Expressivity.encode_FU_def ‹(l, σ) ∈ P ∩ S› sem_def by fastforce
  qed
qed

definition hyperprop_FU where
  "hyperprop_FU P Q S ⟷ (∀l σ. (l, σ) ∈ P ⟶ (∃σ'. (l, σ') ∈ Q ∧ (σ, σ') ∈ S))"

lemma hyperprop_FUI:
  assumes "⋀l σ. (l, σ) ∈ P ⟹ (∃σ'. (l, σ') ∈ Q ∧ (σ, σ') ∈ S)"
  shows "hyperprop_FU P Q S"
  by (simp add: hyperprop_FU_def assms)

lemma hyperprop_FUE:
  assumes "hyperprop_FU P Q S"
      and "(l, σ) ∈ P"
    shows "∃σ'. (l, σ') ∈ Q ∧ (σ, σ') ∈ S"
  using hyperprop_FU_def assms(1) assms(2) by fastforce

theorem FU_expresses_hyperproperties:
  "hypersat C (hyperprop_FU P Q) ⟷ FU P C Q" (is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule FUI)
    fix σ l assume "(l, σ) ∈ P"
    then obtain σ' where asm0: "(l, σ') ∈ Q ∧ (σ, σ') ∈ set_of_traces C"
      by (meson ‹hypersat C (hyperprop_FU P Q)› hyperprop_FUE hypersat_def)
    then show "∃σ'. (⟨C, σ⟩ → σ') ∧ (l, σ') ∈ Q"
      using in_set_of_traces by blast
  qed
next
  assume ?B
  have "hyperprop_FU P Q (set_of_traces C)"
  proof (rule hyperprop_FUI)
    fix l σ
    assume asm0: "(l, σ) ∈ P"
    then show "∃σ'. (l, σ') ∈ Q ∧ (σ, σ') ∈ set_of_traces C"
      by (metis (mono_tags, lifting) CollectI ‹FU P C Q› FU_def set_of_traces_def)
  qed
  then show ?A
    by (simp add: hypersat_def)
qed

theorem hyperliveness_hyperprop_FU:
  assumes "⋀l. sat_for_l l P ⟹ sat_for_l l Q"
  shows "hyperliveness (hyperprop_FU P Q)"
proof (rule hyperlivenessI)
  fix S show "∃S'. S ⊆ S' ∧ hyperprop_FU P Q S'"
    by (meson UNIV_I hyperprop_FU_def assms sat_for_l_def subsetI)
qed


text ‹No relationship between incorrectness and forward underapproximation›

lemma incorrectness_does_not_imply_FU:
  assumes "injective from_nat"
  assumes "P = {(l, σ) |σ l. σ x = from_nat (0 :: nat) ∨ σ x = from_nat 1}"
      and "Q = {(l, σ) |σ l. σ x = from_nat 1}"
      and "C = Assume (λσ. σ x = from_nat 1)"
  shows "IL P C Q"
    and "¬ FU P C Q"
proof -
  have "Q ⊆ sem C P"
  proof (rule subsetPairI)
    fix l σ assume "(l, σ) ∈ Q"
    then have "σ x = from_nat 1"
      using assms(3) by blast
    then have "(l, σ) ∈ P"
      by (simp add: assms(2))
    then show "(l, σ) ∈ sem C P"
      by (simp add: ‹σ x = from_nat 1› assms(4) sem_assume)
  qed
  then show "IL P C Q"
    by (simp add: IL_def)
  show "¬ FU P C Q"
  proof (rule ccontr)
    assume "¬ ¬ FU P C Q"
    then have "FU P C Q"
      by blast
    obtain σ where "σ x = from_nat 0"
      by simp
    then obtain l where "(l, σ) ∈ P"
      using assms(2) by blast
    then obtain σ' where "single_sem C σ σ'" "(l, σ') ∈ Q"
      by (meson ‹FU P C Q› FU_def)
    then have "σ' x = from_nat 0"
      using ‹σ x = from_nat 0› assms(4) by blast
    then have "from_nat 0 = from_nat 1"
      using ‹⟨C, σ⟩ → σ'› assms(4) by force
    then show False
      using assms(1) injective_def[of from_nat] by auto
  qed
qed

lemma FU_does_not_imply_incorrectness:
  assumes "P = {(l, σ) |σ l. σ x = from_nat (0 :: nat) ∨ σ x = from_nat 1}"
      and "Q = {(l, σ) |σ l. σ x = from_nat 1}"
  assumes "injective from_nat"
  shows "¬ IL Q Skip P"
    and "FU Q Skip P"
proof -
  show "FU Q Skip P"
  proof (rule FUI)
    fix σ l
    assume "(l, σ) ∈ Q"
    then show "∃σ'. (⟨Skip, σ⟩ → σ') ∧ (l, σ') ∈ P"
      using SemSkip assms(1) assms(2) by fastforce
  qed
  obtain σ where "σ x = from_nat 0"
    by simp
  then obtain l where "(l, σ) ∈ P"
    using assms(1) by blast
  moreover have "σ x ≠ from_nat 1"
    by (metis ‹σ x = from_nat 0› assms(3) injective_def one_neq_zero)
  then have "(l, σ) ∉ Q"
    using assms(2) by blast
  ultimately show "¬ IL Q Skip P"
    using IL_consequence by blast
qed


subsection ‹Relational Forward Underapproximate logic›

text ‹Definition 13›
definition RFU where
  "RFU P C Q ⟷ (∀states ∈ P. ∃states' ∈ Q. k_sem C states states')"

lemma RFUI:
  assumes "⋀states. states ∈ P ⟹ (∃states' ∈ Q. k_sem C states states')"
  shows "RFU P C Q"
  by (simp add: assms RFU_def)

lemma RFUE:
  assumes "RFU P C Q"
      and "states ∈ P"
    shows "∃states' ∈ Q. k_sem C states states'"
  using assms(1) assms(2) RFU_def by blast

definition encode_RFU where
  "encode_RFU from_nat x P S ⟷ (∃states ∈ P. (∀i. states i ∈ S ∧ fst (states i) x = from_nat i))"

text ‹Proposition 7›
theorem encode_RFU:
  assumes "not_free_var_of P x"
      and "not_free_var_of Q x"
      and "injective from_nat"
    shows "RFU P C Q ⟷ ⊨ {encode_RFU from_nat x P} C {encode_RFU from_nat x Q}"
(is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule hyper_hoare_tripleI)
    fix S assume "encode_RFU from_nat x P S"
    then obtain states where asm0: "states ∈ P" "⋀i. states i ∈ S ∧ fst (states i) x = from_nat i"
      by (meson encode_RFU_def)
    then obtain states' where "states' ∈ Q" "k_sem C states states'"
      using ‹RFU P C Q› RFUE by blast
    then have "⋀i. states' i ∈ sem C S ∧ fst (states' i) x = from_nat i"
      by (metis (mono_tags, lifting) asm0(2) in_sem k_sem_def prod.collapse)
    then show "encode_RFU from_nat x Q (sem C S)"
      by (meson ‹states' ∈ Q› encode_RFU_def)
  qed
next
  assume ?B
  show ?A
  proof (rule RFUI)
    fix states assume asm0: "states ∈ P"
    let ?states = "λi. ((fst (states i))(x := from_nat i), snd (states i))"

    have "?states ∈ P"
      using assms(1)
    proof (rule not_free_var_ofE)
      show "states ∈ P" using asm0 by simp
      fix i show "differ_only_by (fst (states i)) (fst ((fst (states i))(x := from_nat i), snd (states i))) x"
        using diff_by_comm diff_by_update by fastforce
    qed (auto)
    then have "encode_RFU from_nat x P (range ?states)"
      using encode_RFU_def by fastforce
    then have "encode_RFU from_nat x Q (sem C (range ?states))"
      using ‹⊨ {encode_RFU from_nat x P} C {encode_RFU from_nat x Q}› hyper_hoare_tripleE by blast
    then obtain states' where states'_def: "states' ∈ Q" "⋀i. states' i ∈ sem C (range ?states) ∧ fst (states' i) x = from_nat i"
      by (meson encode_RFU_def)

    let ?states' = "λi. ((fst (states' i))(x := fst (states i) x), snd (states' i))"

    have "?states' ∈ Q"
      using assms(2)
    proof (rule not_free_var_ofE)
      show "states' ∈ Q" using ‹states' ∈ Q› by simp
      fix i show "differ_only_by (fst (states' i)) (fst ((fst (states' i))(x := fst (states i) x), snd (states' i))) x"
        using diff_by_comm diff_by_update by fastforce
    qed (auto)
    moreover obtain to_pvar where to_pvar_def: "⋀i. to_pvar (from_nat i) = i"
      using assms(3) injective_then_exists_inverse by blast
    then have inj: "⋀i j. from_nat i = from_nat j ⟹ i = j"
      by metis

    moreover have "k_sem C states ?states'"
    proof (rule k_semI)
      fix i 
      obtain σ where "(fst (states' i), σ) ∈ range (λi. ((fst (states i))(x := from_nat i), snd (states i))) ∧ ⟨C, σ⟩ → snd (states' i)"
        using states'_def(2) in_sem by blast
      moreover have "fst (states' i) x = from_nat i"
        by (simp add: states'_def)
      then have r: "((fst (states (inv ?states (fst (states' i), σ))))
      (x := from_nat (inv ?states (fst (states' i), σ))), snd (states (inv ?states (fst (states' i), σ))))
        = (fst (states' i), σ)"
        by (metis (mono_tags, lifting) calculation f_inv_into_f)
      then have "single_sem C (snd (states i)) (snd (states' i))"
        using ‹fst (states' i) x = from_nat i› calculation inj by fastforce
      moreover have "fst (?states i) = fst (states' i)"
        by (metis (mono_tags, lifting)r ‹fst (states' i) x = from_nat i› fst_conv fun_upd_same inj)
      ultimately show "fst (states i) = fst ((fst (states' i))(x := fst (states i) x), snd (states' i)) ∧
         ⟨C, snd (states i)⟩ → snd ((fst (states' i))(x := fst (states i) x), snd (states' i))"
        by (metis (mono_tags, lifting) fst_conv fun_upd_triv fun_upd_upd snd_conv)
    qed
    ultimately show "∃states'∈Q. k_sem C states states'" by blast
  qed
qed

definition RFU_hyperprop where
  "RFU_hyperprop P Q S ⟷ (∀l states. (λi. (l i, states i)) ∈ P
         ⟶ (∃states'. (λi. (l i, states' i)) ∈ Q ∧ (∀i. (states i, states' i) ∈ S)))"

lemma RFU_hyperpropI:
  assumes "⋀l states. (λi. (l i, states i)) ∈ P ⟹ (∃states'. (λi. (l i, states' i)) ∈ Q ∧ (∀i. (states i, states' i) ∈ S))"
  shows "RFU_hyperprop P Q S"
  by (simp add: assms RFU_hyperprop_def)

lemma RFU_hyperpropE:
  assumes "RFU_hyperprop P Q S"
      and "(λi. (l i, states i)) ∈ P"
    shows "∃states'. (λi. (l i, states' i)) ∈ Q ∧ (∀i. (states i, states' i) ∈ S)"
  using assms(1) assms(2) RFU_hyperprop_def by blast

text ‹Proposition 13›
theorem RFU_captures_hyperproperties:
  "hypersat C (RFU_hyperprop P Q) ⟷ RFU P C Q" (is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule RFUI)
    fix states assume "states ∈ P"
    moreover have "(λi. ((fst ∘ states) i, (snd ∘ states) i)) = states" by simp
    ultimately obtain states' where asm0: "(λi. ((fst ∘ states) i, states' i)) ∈ Q" "⋀i. ((snd ∘ states) i, states' i) ∈ set_of_traces C"
      using RFU_hyperpropE[of P Q "set_of_traces C" "fst ∘ states" "snd ∘ states"]
      using ‹hypersat C (RFU_hyperprop P Q)› hypersat_def by auto

    moreover have "k_sem C states (λi. ((fst ∘ states) i, states' i))"
    proof (rule k_semI)
      fix i 
      have "⟨C, snd (states i)⟩ → states' i"
        using calculation(2) in_set_of_traces by fastforce
      then show "fst (states i) = fst ((fst ∘ states) i, states' i) ∧ ⟨C, snd (states i)⟩ → snd ((fst ∘ states) i, states' i)"
        by simp
    qed
    ultimately show "∃states'∈Q. k_sem C states states'"
      by fast
  qed
next
  assume ?B
  have "RFU_hyperprop P Q (set_of_traces C)"
  proof (rule RFU_hyperpropI)
    fix l states
    assume "(λi. (l i, states i)) ∈ P"
    then obtain states' where asm0: "states' ∈ Q" "k_sem C (λi. (l i, states i)) states'"
      using ‹RFU P C Q› RFUE by blast
    then have "⋀i. fst (states' i) = l i"
      by (simp add: k_sem_def)
    moreover have "(λi. (l i, (snd ∘ states') i)) = states'"
    proof (rule ext)
      fix i show "(l i, (snd ∘ states') i) = states' i"
        by (metis calculation comp_apply surjective_pairing)
    qed
    moreover have "⋀i. (states i, (snd ∘ states') i) ∈ set_of_traces C"
    proof -
      fix i show "(states i, (snd ∘ states') i) ∈ set_of_traces C"
        using asm0(2) comp_apply[of snd states'] in_set_of_traces k_sem_def[of C "λi. (l i, states i)" states'] snd_conv
        by fastforce
    qed
    ultimately show "∃states'. (λi. (l i, states' i)) ∈ Q ∧ (∀i. (states i, states' i) ∈ set_of_traces C)"
      using asm0(1) by force
  qed
  then show ?A
    by (simp add: hypersat_def)
qed

theorem hyperliveness_encode_RFU:
  assumes "⋀l. k_sat_for_l l P ⟹ k_sat_for_l l Q"
  shows "hyperliveness (RFU_hyperprop P Q)"
proof (rule hyperlivenessI)
  fix S 
  have "RFU_hyperprop P Q UNIV"
  proof (rule RFU_hyperpropI)
    fix l states assume asm0: "(λi. (l i, states i)) ∈ P"
    then obtain states' where "(λi. (l i, states' i)) ∈ Q"
      by (metis assms k_sat_for_l_def)
    then show "∃states'. (λi. (l i, states' i)) ∈ Q ∧ (∀i. (states i, states' i) ∈ UNIV)"
      by blast
  qed
  then show "∃S'. S ⊆ S' ∧ RFU_hyperprop P Q S'"
    by blast
qed


subsection ‹Relational Universal Existential (RUE)~\cite{RHLE}›

text ‹Definition 14›

definition RUE where
  "RUE P C Q ⟷ (∀(σ1, σ2) ∈ P. ∀σ1'. k_sem C σ1 σ1' ⟶ (∃σ2'. k_sem C σ2 σ2' ∧ (σ1', σ2') ∈ Q))"

lemma RUE_I:
  assumes "⋀σ1 σ2 σ1'. (σ1, σ2) ∈ P ⟹ k_sem C σ1 σ1' ⟹ (∃σ2'. k_sem C σ2 σ2' ∧ (σ1', σ2') ∈ Q)"
  shows "RUE P C Q"
  using assms RUE_def by fastforce

lemma RUE_E:
  assumes "RUE P C Q"
      and "(σ1, σ2) ∈ P"
      and "k_sem C σ1 σ1'"
    shows "∃σ2'. k_sem C σ2 σ2' ∧ (σ1', σ2') ∈ Q"
  using RUE_def assms(1) assms(2) assms(3) by blast

text ‹Hyperproperty›

definition hyperprop_RUE where
  "hyperprop_RUE P Q S ⟷ (∀l1 l2 σ1 σ2 σ1'. (λi. (l1 i, σ1 i), λk. (l2 k, σ2 k)) ∈ P ∧
  (∀i. (σ1 i, σ1' i) ∈ S) ⟶ (∃σ2'. (∀k. (σ2 k, σ2' k) ∈ S) ∧ (λi. (l1 i, σ1' i), λk. (l2 k, σ2' k)) ∈ Q))"

lemma hyperprop_RUE_I:
  assumes "⋀l1 l2 σ1 σ2 σ1'. (λi. (l1 i, σ1 i), λk. (l2 k, σ2 k)) ∈ P ⟹
  (∀i. (σ1 i, σ1' i) ∈ S) ⟹ (∃σ2'. (∀k. (σ2 k, σ2' k) ∈ S) ∧ (λi. (l1 i, σ1' i), λk. (l2 k, σ2' k)) ∈ Q)"
  shows "hyperprop_RUE P Q S"
  using assms hyperprop_RUE_def[of P Q S]
  by force

lemma hyperprop_RUE_E:
  assumes "hyperprop_RUE P Q S"
      and "(λi. (l1 i, σ1 i), λk. (l2 k, σ2 k)) ∈ P"
      and "⋀i. (σ1 i, σ1' i) ∈ S"
    shows "∃σ2'. (∀k. (σ2 k, σ2' k) ∈ S) ∧ (λi. (l1 i, σ1' i), λk. (l2 k, σ2' k)) ∈ Q"
  using assms(1) assms(2) assms(3) hyperprop_RUE_def by blast


text ‹Proposition 14›
theorem RUE_express_hyperproperties:
  "RUE P C Q ⟷ hypersat C (hyperprop_RUE P Q)" (is "?A ⟷ ?B")
proof
  assume asm0: ?A
  have "hyperprop_RUE P Q (set_of_traces C)"
  proof (rule hyperprop_RUE_I)
    fix l1 l2 σ1 σ2 σ1'
    assume asm1: "(λi. (l1 i, σ1 i), λk. (l2 k, σ2 k)) ∈ P" "∀i. (σ1 i, σ1' i) ∈ set_of_traces C"

    let ?x1 = "λi. (l1 i, σ1 i)"
    let ?x2 = "λk. (l2 k, σ2 k)"

    let ?x1' = "λi. (l1 i, σ1' i)"

    have "∃σ2'. k_sem C (λk. (l2 k, σ2 k)) σ2' ∧ (?x1', σ2') ∈ Q"
      using asm0 asm1(1)
    proof (rule RUE_E)
      show "k_sem C (λi. (l1 i, σ1 i)) (λi. (l1 i, σ1' i))"
      proof (rule k_semI)
        fix i 
        have "single_sem C (σ1 i) (σ1' i)" using asm1(2)
          by (simp add: set_of_traces_def)
        then show "fst (l1 i, σ1 i) = fst (l1 i, σ1' i) ∧ ⟨C, snd (l1 i, σ1 i)⟩ → snd (l1 i, σ1' i)"
          by simp
      qed
    qed
    then obtain σ2' where asm2: "k_sem C (λk. (l2 k, σ2 k)) σ2'" "(?x1', σ2') ∈ Q"
      by blast
    let ?σ2' = "λk. snd (σ2' k)"

    have "⋀k. (σ2 k, ?σ2' k) ∈ set_of_traces C"
      by (metis (mono_tags, lifting) asm2(1) in_set_of_traces k_sem_def snd_conv)
    moreover have "(λk. (l2 k, ?σ2' k)) = σ2'"
    proof (rule ext)
      fix k show "(l2 k, snd (σ2' k)) = σ2' k"
        by (metis (mono_tags, lifting) asm2(1) fst_eqD k_sem_def surjective_pairing)
    qed
    ultimately show "∃σ2'. (∀k. (σ2 k, σ2' k) ∈ set_of_traces C) ∧ (λi. (l1 i, σ1' i), λk. (l2 k, σ2' k)) ∈ Q"
      using asm2(2) by fastforce
  qed
  then show ?B
    by (simp add: hypersat_def)
next
  assume ?B then have asm0: "hyperprop_RUE P Q (set_of_traces C)"
    by (simp add: hypersat_def)
  show ?A
  proof (rule RUE_I)
    fix σ1 σ2 σ1'
    assume asm1: "(σ1, σ2) ∈ P" "k_sem C σ1 σ1'"
    then have "⋀i. fst (σ1 i) = fst (σ1' i)"
      by (simp add: k_sem_def)
    have "∃σ2'. (∀k. (snd (σ2 k), σ2' k) ∈ set_of_traces C) ∧ (λi. (fst (σ1 i), snd (σ1' i)), λk. (fst (σ2 k), σ2' k)) ∈ Q"
      using asm0
    proof (rule hyperprop_RUE_E[of P Q "set_of_traces C" "λi. fst (σ1 i)" "λi. snd (σ1 i)" "λk. fst (σ2 k)" "λk. snd (σ2 k)" "λi. snd (σ1' i)"])
      show "(λi. (fst (σ1 i), snd (σ1 i)), λk. (fst (σ2 k), snd (σ2 k))) ∈ P"        
        by (simp add: asm1(1))
      fix i show "(snd (σ1 i), snd (σ1' i)) ∈ set_of_traces C"
        by (metis (mono_tags, lifting) CollectI asm1(2) k_sem_def set_of_traces_def)
    qed
    then obtain σ2' where asm2: "⋀k. (snd (σ2 k), σ2' k) ∈ set_of_traces C" "(λi. (fst (σ1 i), snd (σ1' i)), λk. (fst (σ2 k), σ2' k)) ∈ Q"
      by blast
    moreover have "k_sem C σ2 (λk. (fst (σ2 k), σ2' k))"
    proof (rule k_semI)
      fix i show "fst (σ2 i) = fst (fst (σ2 i), σ2' i) ∧ ⟨C, snd (σ2 i)⟩ → snd (fst (σ2 i), σ2' i)"
        using calculation(1) in_set_of_traces by auto
    qed
    ultimately show "∃σ2'. k_sem C σ2 σ2' ∧ (σ1', σ2') ∈ Q"
      using ‹⋀i. fst (σ1 i) = fst (σ1' i)› by auto
  qed
qed

definition is_type where
  "is_type type fn x t S σ ⟷ (∀i. σ i ∈ S ∧ fst (σ i) t = type ∧ fst (σ i) x = fn i)"

lemma is_typeI:
  assumes "⋀i. σ i ∈ S"
      and "⋀i. fst (σ i) t = type"
      and "⋀i. fst (σ i) x = fn i"
    shows "is_type type fn x t S σ"
  by (simp add: assms(1) assms(2) assms(3) is_type_def)

lemma is_type_E:
  assumes "is_type type fn x t S σ"
  shows "σ i ∈ S ∧ fst (σ i) t = type ∧ fst (σ i) x = fn i"
  by (meson assms is_type_def)


definition encode_RUE_1 where
  "encode_RUE_1 fn fn1 fn2 x t P S ⟷ (∀k. ∃σ ∈ S. fst σ x = fn2 k ∧ fst σ t = fn 2)
  ∧ (∀σ σ'. is_type (fn 1) fn1 x t S σ ∧ is_type (fn 2) fn2 x t S σ'
  ⟶ (σ, σ') ∈ P)"

lemma encode_RUE_1_I:
  assumes "⋀k. ∃σ ∈ S. fst σ x = fn2 k ∧ fst σ t = fn 2"
      and "⋀σ σ'. is_type (fn 1) fn1 x t S σ ∧ is_type (fn 2) fn2 x t S σ'
  ⟹ (σ, σ') ∈ P"
    shows "encode_RUE_1 fn fn1 fn2 x t P S"
  by (simp add: assms(1) assms(2) encode_RUE_1_def)

lemma encode_RUE_1_E1:
  assumes "encode_RUE_1 fn fn1 fn2 x t P S"
  shows "∃σ ∈ S. fst σ x = fn2 k ∧ fst σ t = fn 2"
  by (meson assms encode_RUE_1_def)

lemma encode_RUE_1_E2:
  assumes "encode_RUE_1 fn fn1 fn2 x t P S"
      and "is_type (fn 1) fn1 x t S σ"
      and "is_type (fn 2) fn2 x t S σ'"
    shows "(σ, σ') ∈ P"
  by (meson assms encode_RUE_1_def)


definition encode_RUE_2 where
  "encode_RUE_2 fn fn1 fn2 x t Q S ⟷ (∀σ. is_type (fn 1) fn1 x t S σ ⟶ (∃σ'. is_type (fn 2) fn2 x t S σ' ∧ (σ, σ') ∈ Q))"

lemma encode_RUE_2I:
  assumes "⋀σ. is_type (fn 1) fn1 x t S σ ⟹ (∃σ'. is_type (fn 2) fn2 x t S σ' ∧ (σ, σ') ∈ Q)"
  shows "encode_RUE_2 fn fn1 fn2 x t Q S"
  by (simp add: assms encode_RUE_2_def)

lemma encode_RUE_2_E:
  assumes "encode_RUE_2 fn fn1 fn2 x t Q S"
      and "is_type (fn 1) fn1 x t S σ"
    shows "∃σ'. is_type (fn 2) fn2 x t S σ' ∧ (σ, σ') ∈ Q"
  by (meson assms(1) assms(2) encode_RUE_2_def)

definition differ_only_by_set where
  "differ_only_by_set vars a b ⟷ (∀x. x ∉ vars ⟶ a x = b x)"

definition differ_only_by_lset where
  "differ_only_by_lset vars a b ⟷ (∀i. snd (a i) = snd (b i) ∧ differ_only_by_set vars (fst (a i)) (fst (b i)))"

lemma differ_only_by_lsetI:
  assumes "⋀i. snd (a i) = snd (b i)"
      and "⋀i. differ_only_by_set vars (fst (a i)) (fst (b i))"
    shows "differ_only_by_lset vars a b"
  using assms(1) assms(2) differ_only_by_lset_def by blast

definition not_in_free_vars_double where
  "not_in_free_vars_double vars P ⟷ (∀σ σ'. differ_only_by_lset vars (fst σ) (fst σ') ∧
  differ_only_by_lset vars (snd σ) (snd σ') ⟶ (σ ∈ P ⟷ σ' ∈ P))"

lemma not_in_free_vars_doubleE:
  assumes "not_in_free_vars_double vars P"
      and "differ_only_by_lset vars (fst σ) (fst σ')"
      and "differ_only_by_lset vars (snd σ) (snd σ')"
      and "σ ∈ P"
    shows "σ' ∈ P"
  by (meson assms not_in_free_vars_double_def)


text ‹Proposition 8›

theorem encoding_RUE:
  assumes "injective fn ∧ injective fn1 ∧ injective fn2"
      and "t ≠ x"

    and "injective (fn :: nat ⇒ 'a)"
    and "injective fn1"
    and "injective fn2"

    and "not_in_free_vars_double {x, t} P"
    and "not_in_free_vars_double {x, t} Q"

    shows "RUE P C Q ⟷ ⊨ {encode_RUE_1 fn fn1 fn2 x t P} C {encode_RUE_2 fn fn1 fn2 x t Q}"
(is "?A ⟷ ?B")
proof
  assume asm0: ?A
  show ?B
  proof (rule hyper_hoare_tripleI)
    fix S assume asm1: "encode_RUE_1 fn fn1 fn2 x t P S"

    show "encode_RUE_2 fn fn1 fn2 x t Q (sem C S)"
    proof (rule encode_RUE_2I)
      fix σ1' assume asm2: "is_type (fn 1) fn1 x t (sem C S) σ1'"

      let ?σ2 = "λk. SOME σ'. σ'∈S ∧ fst σ' x = fn2 k ∧ fst σ' t = fn 2"
      have r2: "⋀k. ?σ2 k ∈S ∧ fst (?σ2 k) x = fn2 k ∧ fst (?σ2 k) t = fn 2"
      proof -
        fix k
        show "?σ2 k ∈S ∧ fst (?σ2 k) x = fn2 k ∧ fst (?σ2 k) t = fn 2"
        proof (rule someI_ex)
          show "∃xa. xa ∈ S ∧ fst xa x = fn2 k ∧ fst xa t = fn 2"
            by (meson asm1 encode_RUE_1_E1)
        qed
      qed
      let ?σ1 = "λi. SOME σ. (fst (σ1' i), σ) ∈ S ∧ single_sem C σ (snd (σ1' i))"
      have r1: "⋀i. (fst (σ1' i), ?σ1 i) ∈ S ∧ single_sem C (?σ1 i) (snd (σ1' i))"
      proof -
        fix i
        show "(fst (σ1' i), ?σ1 i) ∈ S ∧ single_sem C (?σ1 i) (snd (σ1' i))"
        proof (rule someI_ex[of "λσ. (fst (σ1' i), σ) ∈ S ∧ single_sem C σ (snd (σ1' i))"])
          show "∃σ. (fst (σ1' i), σ) ∈ S ∧ ⟨C, σ⟩ → snd (σ1' i)"
            by (meson asm2 in_sem is_type_def)
        qed
      qed
      have "(λi. (fst (σ1' i), ?σ1 i), ?σ2) ∈ P"
        using asm1
      proof (rule encode_RUE_1_E2)
        show "is_type (fn 1) fn1 x t S (λi. (fst (σ1' i), ?σ1 i))"
          using asm2 fst_conv is_type_def[of "fn 1" fn1 x t S] is_type_def[of "fn 1" fn1 x t "sem C S"] r1
          by force
        show "is_type (fn 2) fn2 x t S ?σ2"
          by (simp add: is_type_def r2)
      qed
      moreover have "∃σ2'. k_sem C ?σ2 σ2' ∧ (σ1', σ2') ∈ Q"
        using asm0
      proof (rule RUE_E)
        show "(λi. (fst (σ1' i), ?σ1 i), ?σ2) ∈ P"
          using calculation by auto
        show "k_sem C (λi. (fst (σ1' i), SOME σ. (fst (σ1' i), σ) ∈ S ∧ ⟨C, σ⟩ → snd (σ1' i))) σ1'"
          by (simp add: k_sem_def r1)
      qed
      then obtain σ2' where σ2'_def: "k_sem C ?σ2 σ2' ∧ (σ1', σ2') ∈ Q" by blast
      then have "is_type (fn 2) fn2 x t (sem C S) σ2'"
        using in_sem[of _ C S] k_semE[of C ?σ2 σ2']
          prod.collapse r2 is_type_def[of "fn 2" fn2 x t S] is_type_def[of "fn 2" fn2 x t "sem C S"]
        by (metis (no_types, lifting))
      then show "∃σ2'. is_type (fn 2) fn2 x t (sem C S) σ2' ∧ (σ1', σ2') ∈ Q"
        using σ2'_def by blast
    qed
  qed
next
  assume asm0: "⊨ {encode_RUE_1 fn fn1 fn2 x t P} C {encode_RUE_2 fn fn1 fn2 x t Q}"
  show ?A
  proof (rule RUE_I)
    fix σ1 σ2 σ1'
    assume asm1: "(σ1, σ2) ∈ P" "k_sem C σ1 σ1'"

    let ?σ1 = "λi. ((((fst (σ1 i))(t := fn 1))(x := fn1 i)), snd (σ1 i))"
    let ?σ2 = "λk. ((((fst (σ2 k))(t := fn 2))(x := fn2 k)), snd (σ2 k))"

    let ?S1 = "{ ?σ1 i |i. True }"
    let ?S2 = "{ ?σ2 k |k. True }"
    let ?S = "?S1 ∪ ?S2"

    let ?σ1' = "λi. ((((fst (σ1' i))(t := fn 1))(x := fn1 i)), snd (σ1' i))"

    have "encode_RUE_2 fn fn1 fn2 x t Q (sem C ?S)"
      using asm0       
    proof (rule hyper_hoare_tripleE)
      show "encode_RUE_1 fn fn1 fn2 x t P ?S"
      proof (rule encode_RUE_1_I)
        fix k
        let ?σ = "((((fst (σ2 k))(t := fn 2))(x := fn2 k)), snd (σ2 k))"
        have "?σ ∈ ?S2"
          by auto
        moreover have "fst ?σ x = fn2 k"
          by simp
        moreover have "fst ?σ t = fn 2"
          by (simp add: assms(2))
        ultimately show "∃σ∈?S1 ∪ ?S2. fst σ x = fn2 k ∧ fst σ t = fn 2"
          by blast
      next
        fix σ σ'
        assume asm2: "is_type (fn (1 :: nat)) fn1 x t (?S1 ∪ ?S2) σ ∧ is_type (fn 2) fn2 x t (?S1 ∪ ?S2) σ'"
        moreover have r1: "⋀i. σ i = ((fst (σ1 i))(t := fn 1, x := fn1 i), snd (σ1 i))"
        proof -
          fix i
          have "fst (σ i) t = fn 1"
            by (meson calculation is_type_def)
          moreover have "σ i ∈ ?S1"
          proof (rule ccontr)
            assume "¬ σ i ∈ ?S1"
            moreover have "σ i ∈ ?S1 ∪ ?S2"
              using asm2 is_type_def[of "fn 1" fn1 x t]
              by (metis (no_types, lifting))
            ultimately have "σ i ∈ ?S2" by simp
            then have "fst (σ i) t = fn 2"
              using assms(2) by auto
            then show False
              by (metis Suc_1 Suc_eq_numeral ‹fst (σ i) t = fn 1› assms(3) injective_def numeral_One one_neq_zero pred_numeral_simps(1))
          qed
          then obtain j where "σ i = ((fst (σ1 j))(t := fn 1, x := fn1 j), snd (σ1 j))"
            by blast
          moreover have "i = j"
            by (metis (mono_tags, lifting) asm2 assms(4) calculation(2) fst_conv fun_upd_same injective_def is_type_def)
          ultimately show "σ i = ((fst (σ1 i))(t := fn 1, x := fn1 i), snd (σ1 i))"
            by blast
        qed
        moreover have "⋀i. σ' i = ((fst (σ2 i))(t := fn 2, x := fn2 i), snd (σ2 i))"
        proof -
          fix i
          have "fst (σ' i) t = fn 2"
            by (meson calculation is_type_def)
          moreover have "σ' i ∈ ?S2"
          proof (rule ccontr)
            assume "¬ σ' i ∈ ?S2"
            moreover have "σ' i ∈ ?S1 ∪ ?S2"
              using asm2 is_type_def[of "fn 2" fn2 x t]
              by (metis (no_types, lifting))
            ultimately have "σ' i ∈ ?S1" by simp
            then have "fst (σ' i) t = fn 1"
              using assms(2) by auto
            then show False
              by (metis Suc_1 Suc_eq_numeral ‹fst (σ' i) t = fn 2› assms(3) injective_def numeral_One one_neq_zero pred_numeral_simps(1))
          qed
          then obtain j where "σ' i = ((fst (σ2 j))(t := fn 2, x := fn2 j), snd (σ2 j))"
            by blast
          moreover have "i = j"
            by (metis (mono_tags, lifting) asm2 assms(5) calculation(2) fst_conv fun_upd_same injective_def is_type_def)
          ultimately show "σ' i = ((fst (σ2 i))(t := fn 2, x := fn2 i), snd (σ2 i))"
            by blast
        qed
        moreover have "(?σ1, ?σ2) ∈ P"
          using assms(6)
        proof (rule not_in_free_vars_doubleE)
          show "(σ1, σ2) ∈ P"
            by (simp add: asm1(1))
          show "differ_only_by_lset {x, t} (fst (σ1, σ2)) (fst (?σ1, ?σ2))"
            by (rule differ_only_by_lsetI) (simp_all add: differ_only_by_set_def)
          show "differ_only_by_lset {x, t} (snd (σ1, σ2)) (snd (?σ1, ?σ2))"
            by (rule differ_only_by_lsetI) (simp_all add: differ_only_by_set_def)
        qed
        ultimately show "(σ, σ') ∈ P"
          by presburger
      qed
    qed
    then have "∃σ'. is_type (fn 2) fn2 x t (sem C ?S) σ' ∧ (?σ1', σ') ∈ Q"
    proof (rule encode_RUE_2_E)
      show "is_type (fn 1) fn1 x t (sem C ?S) ?σ1'"
      proof (rule is_typeI)
        fix i show "fst ((fst (σ1' i))(t := fn 1, x := fn1 i), snd (σ1' i)) t = fn 1"
          by (simp add: assms(2))
        show " ((fst (σ1' i))(t := fn 1, x := fn1 i), snd (σ1' i)) ∈ sem C ?S"
          using UnI1[of _ ?S1 ?S2]
            asm1(2) k_semE[of C σ1 σ1' i]
            single_step_then_in_sem[of C "snd (σ1 i)" "snd (σ1' i)" _ ?S]
          by force
      qed (auto)
    qed
    then obtain σ2' where r: "is_type (fn 2) fn2 x t (sem C ?S) σ2' ∧ (?σ1', σ2') ∈ Q"
      by blast
    let ?σ2' = "λk. ((fst (σ2' k))(x := fst (σ2 k) x, t := fst (σ2 k) t), snd (σ2' k))"
    have "(σ1', ?σ2') ∈ Q"
      using assms(7)
    proof (rule not_in_free_vars_doubleE)
      show "(?σ1', σ2') ∈ Q"
        using r by blast
      show "differ_only_by_lset {x, t} (fst (?σ1', σ2')) (fst (σ1', ?σ2'))"
        by (rule differ_only_by_lsetI) (simp_all add: differ_only_by_set_def)
      show "differ_only_by_lset {x, t} (snd (?σ1', σ2')) (snd (σ1', ?σ2'))"
        by (rule differ_only_by_lsetI) (simp_all add: differ_only_by_set_def)
    qed
    moreover have "k_sem C σ2 ?σ2'"
    proof (rule k_semI)
      fix i
      obtain y where y_def: "y ∈ ?S" "fst y = fst (σ2' i)" "single_sem C (snd y) (snd (σ2' i))"
        using r in_sem[of "σ2' i" C ?S]
          is_type_E[of "fn 2" fn2 x t "sem C ?S" σ2' i]
        by (metis (no_types, lifting) fst_conv snd_conv)
      then have "fst y t = fn 2"
        by (metis (no_types, lifting) is_type_def r)
      moreover have "fn 1 ≠ fn 2"
        by (metis Suc_1 assms(3) injective_def n_not_Suc_n)
      then have "y ∉ ?S1"
        using assms(2) calculation by fastforce
      then have "y ∈ ?S2"
        using y_def(1) by blast
      show "fst (σ2 i) = fst ((fst (σ2' i))(x := fst (σ2 i) x, t := fst (σ2 i) t), snd (σ2' i)) ∧
         ⟨C, snd (σ2 i)⟩ → snd ((fst (σ2' i))(x := fst (σ2 i) x, t := fst (σ2 i) t), snd (σ2' i))"
      proof
        have r1: "σ2' i ∈ sem C ?S ∧ fst (σ2' i) t = fn 2 ∧ fst (σ2' i) x = fn2 i"
        proof (rule is_type_E[of "fn 2" fn2 x t "sem C ?S" σ2' i])
          show "is_type (fn 2) fn2 x t (sem C ?S) σ2'"
            using r by blast
        qed
        then obtain σ where "(fst (σ2' i), σ) ∈ ?S" "single_sem C σ (snd (σ2' i))"
          by (meson in_sem)
        then have "(fst (σ2' i), σ) ∈ ?S2"
          using r1 ‹fn 1 ≠ fn 2› assms(2) by fastforce
        then obtain k where "fst (σ2' i) = (fst (σ2 k))(t := fn 2, x := fn2 k)" and "σ = snd (σ2 k)"
          by blast
        then have "k = i"
          by (metis r1 assms(5) fun_upd_same injective_def)
        then show "⟨C, snd (σ2 i)⟩ → snd ((fst (σ2' i))(x := fst (σ2 i) x, t := fst (σ2 i) t), snd (σ2' i))"
          using ‹⟨C, σ⟩ → snd (σ2' i)› ‹σ = snd (σ2 k)› by auto
        show "fst (σ2 i) = fst ((fst (σ2' i))(x := fst (σ2 i) x, t := fst (σ2 i) t), snd (σ2' i))"
          by (simp add: ‹fst (σ2' i) = (fst (σ2 k))(t := fn 2, x := fn2 k)› ‹k = i›)
      qed
    qed
    ultimately show "∃σ2'. k_sem C σ2 σ2' ∧ (σ1', σ2') ∈ Q"
      by blast
  qed
qed

subsection ‹Program Refinement›

lemma sem_assign_single:
  "sem (Assign x e) {(l, σ)} = {(l, σ(x := e σ))}" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix la σ'
    assume "(la, σ') ∈ sem (Assign x e) {(l, σ)}"
    then show "(la, σ') ∈ {(l, σ(x := e σ))}"
      by (metis (mono_tags, lifting) in_sem prod.sel(1) prod.sel(2) single_sem_Assign_elim singleton_iff)
  qed
  show "?B ⊆ ?A"
    by (simp add: SemAssign in_sem)
qed

definition refinement where
  "refinement C1 C2 ⟷ (set_of_traces C1 ⊆ set_of_traces C2)"

definition not_free_var_stmt where
  "not_free_var_stmt x C ⟷ (∀σ σ' v. (σ, σ') ∈ set_of_traces C ⟶ (σ(x := v), σ'(x := v)) ∈ set_of_traces C)
∧ (∀σ σ'. single_sem C σ σ' ⟶ σ x = σ' x)"

lemma not_free_var_stmtE_1:
  assumes "not_free_var_stmt x C"
      and "(σ, σ') ∈ set_of_traces C"
    shows "(σ(x := v), σ'(x := v)) ∈ set_of_traces C"
  using assms(1) assms(2) not_free_var_stmt_def by force

lemma not_free_in_sem_same_val:
  assumes "not_free_var_stmt x C"
      and "single_sem C σ σ'"
    shows "σ x = σ' x"
  using assms(1) assms(2) not_free_var_stmt_def by fastforce

lemma not_free_in_sem_equiv:
  assumes "not_free_var_stmt x C"
      and "single_sem C σ σ'"
    shows "single_sem C (σ(x := v)) (σ'(x := v))"
  by (meson assms(1) assms(2) in_set_of_traces not_free_var_stmtE_1)
      

text ‹Example 4›
theorem encoding_refinement:
  fixes P :: "(('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set ⇒ bool"
  assumes "(a :: 'pval) ≠ b"
    (* and x free var *)
      and "P = (λS. card S = 1)"
      and "Q = (λS.
  ∀φ∈S. snd φ x = a ⟶ (fst φ, (snd φ)(x := b)) ∈ S)"
      and "not_free_var_stmt x C1"
      and "not_free_var_stmt x C2"
  shows "refinement C1 C2 ⟷
  ⊨ { P } If (Seq (Assign (x :: 'pvar) (λ_. a)) C1) (Seq (Assign x (λ_. b)) C2) { Q }"
(is "?A ⟷ ?B")
proof
  assume ?A
  show ?B
  proof (rule hyper_hoare_tripleI)
    fix S assume "P (S :: (('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set)"

    then obtain σ l where asm0: "S = {(l, σ)}"
      by (metis assms(2) card_1_singletonE surj_pair)

    let ?C = "If (Seq (Assign x (λ_. a)) C1) (Seq (Assign x (λ_. b)) C2)"
    let ?a = "(l, σ(x := a))"
    let ?b = "(l, σ(x := b))"

    have if_sem: "sem ?C S = sem C1 {?a} ∪ sem C2 {?b}"
      by (simp add: asm0 sem_assign_single sem_if sem_seq)
    then have "⋀φ. φ ∈ sem ?C S ⟹ snd φ x = a ⟹ (fst φ, (snd φ)(x := b)) ∈ sem ?C S"
    proof -
      fix φ assume asm1: "φ ∈ sem ?C S" "snd φ x = a"
      have "φ ∈ sem C1 {?a}"
      proof (rule ccontr)
        assume "φ ∉ sem C1 {(l, σ(x := a))}"
        then have "φ ∈ sem C2 {(l, σ(x := b))}"
          using if_sem asm1(1) by force
        then have "snd φ x = b"
          using assms(5) fun_upd_same in_sem not_free_in_sem_same_val[of x C2 "σ(x := b)" "snd φ"] singletonD snd_conv
          by metis
        then show False
          using asm1(2) assms(1) by blast
      qed
      then have "(σ(x := a), snd φ) ∈ set_of_traces C1"
        by (simp add: in_sem set_of_traces_def)
      then have "(σ(x := a), snd φ) ∈ set_of_traces C2"
        using ‹refinement C1 C2› refinement_def by fastforce
      then have "((σ(x := a))(x := b), (snd φ)(x := b)) ∈ set_of_traces C2"
        by (meson assms(5) not_free_var_stmtE_1)
      then have "single_sem C2 (σ(x := b)) ((snd φ)(x := b))"
        by (simp add: set_of_traces_def)
      then have "(fst φ, (snd φ)(x := b)) ∈ sem C2 {?b}"
        by (metis ‹φ ∈ sem C1 {(l, σ(x := a))}› fst_eqD in_sem singleton_iff snd_eqD)
      then show "(fst φ, (snd φ)(x := b)) ∈ sem ?C S"
        by (simp add: if_sem)
    qed
    then show "Q (sem ?C S)"
      using assms(3) by blast
  qed
next
  assume asm0: ?B

  have "set_of_traces C1 ⊆ set_of_traces C2"
  proof (rule subsetPairI)
    fix σ σ' assume asm1: "(σ, σ') ∈ set_of_traces C1"
    obtain l S where "(S :: (('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set) = { (l, σ) }"      
      by simp

    let ?a = "(l, σ(x := a))"
    let ?b = "(l, σ(x := b))"

    let ?C = "If (Seq (Assign (x :: 'pvar) (λ_. a)) C1) (Seq (Assign x (λ_. b)) C2)"
    have "Q (sem ?C S)"
    proof (rule hyper_hoare_tripleE)
      show "P S"
        by (simp add: ‹S = {(l, σ)}› assms(2))
      show ?B using asm0 by simp
    qed
    moreover have "(l, σ'(x := a)) ∈ sem ?C S"
    proof -
      have "single_sem (Seq (Assign x (λ_. a)) C1) σ (σ'(x := a))"
        by (meson SemAssign SemSeq asm1 assms(4) in_set_of_traces not_free_in_sem_equiv)
      then show ?thesis
        by (simp add: SemIf1 ‹S = {(l, σ)}› in_sem)
    qed
    then have "(l, σ'(x := b)) ∈ sem ?C S"
      using assms(3) calculation by fastforce
    moreover have "(l, σ'(x := b)) ∈ sem (Seq (Assign x (λ_. b)) C2) S"
    proof (rule ccontr)
      assume "¬ (l, σ'(x := b)) ∈ sem (Seq (Assign x (λ_. b)) C2) S"
      then have "(l, σ'(x := b)) ∈ sem (Seq (Assign x (λ_. a)) C1) S"
        using calculation(2) sem_if by auto
      then have "(l, σ'(x := b)) ∈ sem C1 {?a}"
        by (simp add: ‹S = {(l, σ)}› sem_assign_single sem_seq)
      then show False
        using assms(1) assms(4) fun_upd_same in_sem not_free_in_sem_same_val[of x C1  "σ(x := a)" "σ'(x := b)"] singletonD snd_conv
        by metis
    qed
    then have "single_sem (Seq (Assign x (λ_. b)) C2) σ (σ'(x := b))"
      by (simp add: ‹S = {(l, σ)}› in_sem)
    then have "single_sem C2 (σ(x := b)) (σ'(x := b))"
      by blast
    then have "(σ(x := b), σ'(x := b)) ∈ set_of_traces C2"
      by (simp add: set_of_traces_def)
    then have "((σ(x := b))(x := σ x), (σ'(x := b))(x := σ x)) ∈ set_of_traces C2"
      by (meson assms(5) not_free_var_stmtE_1)
    then show "(σ, σ') ∈ set_of_traces C2"
      by (metis asm1 assms(4) fun_upd_triv fun_upd_upd in_set_of_traces not_free_in_sem_same_val)
  qed
  then show ?A
    by (simp add: refinement_def)
qed

end