Theory Expressivity

text ‹In this file, we prove most results of Appendix C:
  hyper-triples subsume many other triples, as well as example 3.›

theory Expressivity
  imports ProgramHyperproperties
begin


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

paragraph ‹Definition 16›
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

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

paragraph ‹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}›

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

paragraph ‹Definition 17›
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


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

paragraph ‹Proposition 3›
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))›

paragraph ‹Definition 18›

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)

paragraph ‹Proposition 5›
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

paragraph ‹Proposition 6›
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 ‹k-Incorrectness Logic~\cite{InsecurityLogic} (k-IL)›

text ‹RIL is the old name of k-IL.›

paragraph ‹Definition 19›
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

paragraph ‹Proposition 17›
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 "statesP. 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 = "statesP. { (((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 "statesP. k_sem C states states'"
      by auto
  qed
qed


paragraph ‹Proposition 8›

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

paragraph ‹Definition 20›
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  {}"

paragraph ‹Proposition 9›
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


paragraph ‹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 ‹k-Forward Underapproximate logic›

text ‹RFU is the old name of k-FU.›

paragraph ‹Definition 21›
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))"

paragraph ‹Proposition 11›
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

paragraph ‹Proposition 10›
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 ‹k-Universal Existential (RUE)~\cite{RHLE}›

text ‹RUE is the old name of k-UE.›

paragraph ‹Definition 22›

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

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


paragraph ‹Proposition 12›
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)


paragraph ‹Proposition 13›

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)
      

paragraph ‹Example 3›

lemma rewrite_if_commute:
  assumes " { P } If C1 C2 {Q}"
  shows " { P } If C2 C1 {Q}"
  by (metis assms hyper_hoare_triple_def sem_if sup_commute)

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

paragraph ‹Necessary Preconditions›

definition NC where
  "NC P C Q  (σ σ' l. (l, σ')  Q  (C, σ  σ')  (l, σ)  P)"

lemma NC_I:
  assumes "σ σ' l. (l, σ')  Q  (C, σ  σ')  (l, σ)  P"
  shows "NC P C Q"
  by (simp add: NC_def assms)

definition backwards_sem where
  "backwards_sem C S'  = { (l, σ) |l σ σ'. (l, σ')  S'  C, σ  σ'}"

lemma equiv_def_NC:
  "NC P C Q  backwards_sem C Q  P" (is "?A  ?B")
proof
  assume ?A
  then show ?B
    using CollectD NC_def backwards_sem_def[of C Q] subsetI[of "backwards_sem C Q" P] by fastforce
next
  assume ?B
  then show ?A 
    using NC_def backwards_sem_def by fastforce
qed

lemma equiv_def_FU:
  "FU P C Q  P  backwards_sem C Q" (is "?A  ?B")
proof
  show "?A  ?B"
    using FU_def[of P C Q] backwards_sem_def[of C Q]
    by fastforce
  show "?B  ?A"
    using FU_def[of P C Q] backwards_sem_def[of C Q] by auto
qed

lemma encoding_NC_in_HL_1:
  "NC P C Q   { (λS. S = -P) } C { (λS. S  Q = {} ) }" (is "?A  ?B")
proof
  assume ?A
  show ?B
  proof (rule hyper_hoare_tripleI)
    fix S assume asm0: "S = - P"
    then show "sem C S  Q = {}"
      by (metis (no_types, lifting) ComplD NC_def NC P C Q disjoint_iff in_sem prod.collapse)
  qed
next
  assume ?B
  show ?A
  proof (rule NC_I)
    fix σ σ' l
    assume asm0: "(l, σ')  Q  C, σ  σ'"
    then have "(l, σ')  sem C (-P)"
      using  {(λS. S = - P)} C {λS. S  Q = {}} hyper_hoare_tripleE by fastforce
    then have "(l, σ)  -P"
      by (meson asm0 single_step_then_in_sem)
    then show "(l, σ)  P"
      by simp
  qed
qed


end