Theory Logic

section ‹Hyper Hoare Logic›

text ‹This file contains technical results from sections 3 and 5:
- Hyper-assertions (definition 3)
- Hyper-triples (definition 5)
- Core rules of Hyper Hoare Logic (figure 2)
- Soundness of the core rules (theorem 1)
- Completeness of the core rules (theorem 2)
- Ability to disprove hyper-triples (theorem 5)›

theory Logic
  imports Language
begin

text ‹Definition 3›
type_synonym 'a hyperassertion = "('a set ⇒ bool)"

definition entails where
  "entails A B ⟷ (∀S. A S ⟶ B S)"

lemma entails_refl:
  "entails A A"
  by (simp add: entails_def)

lemma entailsI:
  assumes "⋀S. A S ⟹ B S"
  shows "entails A B"
  by (simp add: assms entails_def)

lemma entailsE:
  assumes "entails A B"
      and "A x"
    shows "B x"
  by (meson assms(1) assms(2) entails_def)

lemma bientails_equal:
  assumes "entails A B"
      and "entails B A"
    shows "A = B"
proof (rule ext)
  fix S show "A S = B S"
    by (meson assms(1) assms(2) entailsE)
qed

lemma entails_trans:
  assumes "entails A B"
      and "entails B C"
    shows "entails A C"
  by (metis assms(1) assms(2) entails_def)


definition setify_prop where
  "setify_prop b = { (l, σ) |l σ. b σ}"

lemma sem_assume_setify:
  "sem (Assume b) S = S ∩ setify_prop b" (is "?A = ?B")
proof -
  have "⋀l σ. (l, σ) ∈ ?A ⟷ (l, σ) ∈ ?B"
  proof -
    fix l σ
    have "(l, σ) ∈ ?A ⟷ (l, σ) ∈ S ∧ b σ"
      by (simp add: assume_sem)
    then show "(l, σ) ∈ ?A ⟷ (l, σ) ∈ ?B"
      by (simp add: setify_prop_def)
  qed
  then show ?thesis
    by auto
qed

definition over_approx :: "'a set ⇒ 'a hyperassertion" where
  "over_approx P S ⟷ S ⊆ P"

definition lower_closed :: "'a hyperassertion ⇒ bool" where
  "lower_closed P ⟷ (∀S S'. P S ∧ S' ⊆ S ⟶ P S')"

lemma over_approx_lower_closed:
  "lower_closed (over_approx P)"
  by (metis (full_types) lower_closed_def order_trans over_approx_def)

definition under_approx :: "'a set ⇒ 'a hyperassertion" where
  "under_approx P S ⟷ P ⊆ S"

definition upper_closed :: "'a hyperassertion ⇒ bool" where
  "upper_closed P ⟷ (∀S S'. P S ∧ S ⊆ S' ⟶ P S')"

lemma under_approx_upper_closed:
  "upper_closed (under_approx P)"
  by (metis (no_types, lifting) order.trans under_approx_def upper_closed_def)

definition closed_by_union :: "'a hyperassertion ⇒ bool" where
  "closed_by_union P ⟷ (∀S S'. P S ∧ P S' ⟶ P (S ∪ S'))"

lemma closed_by_unionI:
  assumes "⋀a b. P a ⟹ P b ⟹ P (a ∪ b)"
  shows "closed_by_union P"
  by (simp add: assms closed_by_union_def)

lemma closed_by_union_over:
  "closed_by_union (over_approx P)"
  by (simp add: closed_by_union_def over_approx_def)

lemma closed_by_union_under:
  "closed_by_union (under_approx P)"
  by (simp add: closed_by_union_def sup.coboundedI1 under_approx_def)

definition conj where
  "conj P Q S ⟷ P S ∧ Q S"

lemma entail_conj:
  assumes "entails A B"
  shows "entails A (conj A B)"
  by (metis (full_types) assms conj_def entails_def)

lemma entail_conj_weaken:
  "entails (conj A B) A"
  by (simp add: conj_def entails_def)

definition disj where
  "disj P Q S ⟷ P S ∨ Q S"

definition exists :: "('c ⇒ 'a hyperassertion) ⇒ 'a hyperassertion" where
  "exists P S ⟷ (∃x. P x S)"

definition forall :: "('c ⇒ 'a hyperassertion) ⇒ 'a hyperassertion" where
  "forall P S ⟷ (∀x. P x S)"

lemma over_inter:
  "entails (over_approx (P ∩ Q)) (conj (over_approx P) (over_approx Q))"
  by (simp add: conj_def entails_def over_approx_def)

lemma over_union:
  "entails (disj (over_approx P) (over_approx Q)) (over_approx (P ∪ Q))"
  by (metis disj_def entailsI le_supI1 le_supI2 over_approx_def)

lemma under_union:
  "entails (under_approx (P ∪ Q)) (disj (under_approx P) (under_approx Q))"
  by (simp add: disj_def entails_def under_approx_def)

lemma under_inter:
  "entails (conj (under_approx P) (under_approx Q)) (under_approx (P ∩ Q))"
  by (simp add: conj_def entails_def le_infI1 under_approx_def)

text ‹Definition 6: Operator ‹⊗››
definition join :: "'a hyperassertion ⇒ 'a hyperassertion ⇒ 'a hyperassertion" where
  "join A B S ⟷ (∃SA SB. A SA ∧ B SB ∧ S = SA ∪ SB)"

definition general_join :: "('b ⇒ 'a hyperassertion) ⇒ 'a hyperassertion" where
  "general_join f S ⟷ (∃F. S = (⋃x. F x) ∧ (∀x. f x (F x)))"

lemma general_joinI:
  assumes "S = (⋃x. F x)"
      and "⋀x. f x (F x)"
    shows "general_join f S"
  using assms(1) assms(2) general_join_def by blast

lemma join_closed_by_union:
  assumes "closed_by_union Q"
  shows "join Q Q = Q"
proof
  fix S
  show "join Q Q S ⟷ Q S"
    by (metis assms closed_by_union_def join_def sup_idem)
qed

lemma entails_join_entails:
  assumes "entails A1 B1"
      and "entails A2 B2"
    shows "entails (join A1 A2) (join B1 B2)"
proof (rule entailsI)
  fix S assume "join A1 A2 S"
  then obtain S1 S2 where "A1 S1" "A2 S2" "S = S1 ∪ S2"
    by (metis join_def)
  then show "join B1 B2 S"
    by (metis assms(1) assms(2) entailsE join_def)
qed


text ‹Definition 7: Operator ‹⨂› (for ‹x ∈ X›)›
definition natural_partition where
  "natural_partition I S ⟷ (∃F. S = (⋃n. F n) ∧ (∀n. I n (F n)))"

lemma natural_partitionI:
  assumes "S = (⋃n. F n)"
      and "⋀n. I n (F n)"
    shows "natural_partition I S"
  using assms(1) assms(2) natural_partition_def by blast

lemma natural_partitionE:
  assumes "natural_partition I S"
  obtains F where "S = (⋃n. F n)" "⋀n. I n (F n)"
  by (meson assms natural_partition_def)


subsection ‹Rules of the Logic›

text ‹Core rules from figure 2›

inductive syntactic_HHT ::
 "(('lvar, 'lval, 'pvar, 'pval) state hyperassertion) ⇒ ('pvar, 'pval) stmt ⇒ (('lvar, 'lval, 'pvar, 'pval) state hyperassertion) ⇒ bool"
   ("⊢ {_} _ {_}" [51,0,0] 81) where
  RuleSkip: "⊢ {P} Skip {P}"
| RuleCons: "⟦ entails P P' ; entails Q' Q ; ⊢ {P'} C {Q'} ⟧ ⟹ ⊢ {P} C {Q}"
| RuleSeq: "⟦ ⊢ {P} C1 {R} ; ⊢ {R} C2 {Q} ⟧ ⟹ ⊢ {P} (Seq C1 C2) {Q}"
| RuleIf: "⟦ ⊢ {P} C1 {Q1} ; ⊢ {P} C2 {Q2} ⟧ ⟹ ⊢ {P} (If C1 C2) {join Q1 Q2}"
| RuleWhile: "⟦ ⋀n. ⊢ {I n} C {I (Suc n)} ⟧ ⟹ ⊢ {I 0} (While C) {natural_partition I}"
| RuleAssume: "⊢ { (λS. P (Set.filter (b ∘ snd) S)) } (Assume b) {P}"
| RuleAssign: "⊢ { (λS. P { (l, σ(x := e σ)) |l σ. (l, σ) ∈ S }) } (Assign x e) {P}"
| RuleHavoc: "⊢ { (λS. P { (l, σ(x := v)) |l σ v. (l, σ) ∈ S }) } (Havoc x) {P}"
| RuleExistsSet: "⟦⋀x::('lvar, 'lval, 'pvar, 'pval) state set. ⊢ {P x} C {Q x}⟧ ⟹ ⊢ {exists P} C {exists Q}"


subsection ‹Soundness›

text ‹Definition 5: Hyper-Triples›
definition hyper_hoare_triple ("⊨ {_} _ {_}" [51,0,0] 81) where
  "⊨ {P} C {Q} ⟷ (∀S. P S ⟶ Q (sem C S))"

lemma hyper_hoare_tripleI:
  assumes "⋀S. P S ⟹ Q (sem C S)"
  shows "⊨ {P} C {Q}"
  by (simp add: assms hyper_hoare_triple_def)

lemma hyper_hoare_tripleE:
  assumes "⊨ {P} C {Q}"
      and "P S"
    shows "Q (sem C S)"
  using assms(1) assms(2) hyper_hoare_triple_def
  by metis

lemma consequence_rule:
  assumes "entails P P'"
      and "entails Q' Q"
      and "⊨ {P'} C {Q'}"
    shows "⊨ {P} C {Q}"
  by (metis (no_types, opaque_lifting) assms(1) assms(2) assms(3) entails_def hyper_hoare_triple_def)

lemma skip_rule:
  "⊨ {P} Skip {P}"
  by (simp add: hyper_hoare_triple_def sem_skip)

lemma assume_rule:
  "⊨ { (λS. P (Set.filter (b ∘ snd) S)) } (Assume b) {P}"
proof (rule hyper_hoare_tripleI)
  fix S assume "P (Set.filter (b ∘ snd) S)"
  then show "P (sem (Assume b) S)"
    by (simp add: assume_sem)
qed

lemma seq_rule:
  assumes "⊨ {P} C1 {R}"
    and "⊨ {R} C2 {Q}"
    shows "⊨ {P} Seq C1 C2 {Q}"
  using assms(1) assms(2) hyper_hoare_triple_def sem_seq
  by metis

lemma if_rule:
  assumes "⊨ {P} C1 {Q1}"
      and "⊨ {P} C2 {Q2}"
    shows "⊨ {P} If C1 C2 {join Q1 Q2}"
  by (metis (full_types) assms(1) assms(2) hyper_hoare_triple_def join_def sem_if)

lemma sem_assign:
  "sem (Assign x e) S = {(l, σ(x := e σ)) |l σ. (l, σ) ∈ S}" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix l σ'
    assume "(l, σ') ∈ sem (Assign x e) S"
    then obtain σ where "(l, σ) ∈ S" "single_sem (Assign x e) σ σ'"
      by (metis fst_eqD in_sem snd_conv)
    then show "(l, σ') ∈ {(l, σ(x := e σ)) |l σ. (l, σ) ∈ S}"
      by blast
  qed
  show "?B ⊆ ?A"
  proof (rule subsetPairI)
    fix l σ'
    assume "(l, σ') ∈ ?B"
    then obtain σ where "σ' = σ(x := e σ)" "(l, σ) ∈ S"
      by blast
    then show "(l, σ') ∈ ?A"
      by (metis SemAssign fst_eqD in_sem snd_conv)
  qed
qed

lemma assign_rule:
  "⊨ { (λS. P { (l, σ(x := e σ)) |l σ. (l, σ) ∈ S }) } (Assign x e) {P}"
proof (rule hyper_hoare_tripleI)
  fix S assume "P {(l, σ(x := e σ)) |l σ. (l, σ) ∈ S}"
  then show "P (sem (Assign x e) S)" using sem_assign
    by metis
qed

lemma sem_havoc:
  "sem (Havoc x) S = {(l, σ(x := v)) |l σ v. (l, σ) ∈ S}" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix l σ'
    assume "(l, σ') ∈ sem (Havoc x) S"
    then obtain σ where "(l, σ) ∈ S" "single_sem (Havoc x) σ σ'"
      by (metis fst_eqD in_sem snd_conv)
    then show "(l, σ') ∈ {(l, σ(x := v)) |l σ v. (l, σ) ∈ S}"
      by blast
  qed
  show "?B ⊆ ?A"
  proof (rule subsetPairI)
    fix l σ'
    assume "(l, σ') ∈ ?B"
    then obtain σ v where "σ' = σ(x := v)" "(l, σ) ∈ S"
      by blast
    then show "(l, σ') ∈ ?A"
      by (metis SemHavoc fst_eqD in_sem snd_conv)
  qed
qed

lemma havoc_rule:
  "⊨ { (λS. P { (l, σ(x := v)) |l σ v. (l, σ) ∈ S }) } (Havoc x) {P}"
proof (rule hyper_hoare_tripleI)
  fix S assume "P { (l, σ(x := v)) |l σ v. (l, σ) ∈ S }"
  then show "P (sem (Havoc x) S)" using sem_havoc by metis
qed


text ‹Loops›

lemma indexed_invariant_then_power:
  assumes "⋀n. hyper_hoare_triple (I n) C (I (Suc n))"
      and "I 0 S"
  shows "I n (iterate_sem n C S)"
  using assms
proof (induct n arbitrary: S)
next
  case (Suc n)
  then have "I n (iterate_sem n C S)"
    by blast
  then have "I (Suc n) (sem C (iterate_sem n C S))"
    using Suc.prems(1) hyper_hoare_tripleE by blast
  then show ?case
    by (simp add: Suc.hyps Suc.prems(1))
qed (auto)

lemma indexed_invariant_then_power_bounded:
  assumes "⋀m. m < n ⟹ hyper_hoare_triple (I m) C (I (Suc m))"
      and "I 0 S"
  shows "I n (iterate_sem n C S)"
  using assms
proof (induct n arbitrary: S)
next
  case (Suc n)
  then have "I n (iterate_sem n C S)"
    using less_Suc_eq by presburger
  then have "I (Suc n) (sem C (iterate_sem n C S))"
    using Suc.prems(1) hyper_hoare_tripleE by blast
  then show ?case
    by (simp add: Suc.hyps Suc.prems(1))
qed (auto)

lemma while_rule:
  assumes "⋀n. hyper_hoare_triple (I n) C (I (Suc n))"
  shows "hyper_hoare_triple (I 0) (While C) (natural_partition I)"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "I 0 S"
  show "natural_partition I (sem (While C) S)"
  proof (rule natural_partitionI)
    show "sem (While C) S = ⋃ (range (λn. iterate_sem n C S))"
      by (simp add: sem_while)
    fix n show "I n (iterate_sem n C S)"
      by (simp add: asm0 assms indexed_invariant_then_power)
  qed
qed

lemma rule_exists:
  assumes "⋀x. ⊨ {P x} C {Q x}"
  shows "⊨ {exists P} C {exists Q}"
  by (metis assms exists_def hyper_hoare_triple_def)

text ‹Theorem 1›

theorem soundness:
  assumes "⊢ {A} C {B}"
    shows "⊨ {A} C {B}"
  using assms
proof (induct rule: syntactic_HHT.induct)
  case (RuleSkip P)
  then show ?case
    using skip_rule by auto
next
  case (RuleCons P P' Q' Q C)
  then show ?case
    using consequence_rule by blast
next
  case (RuleExistsSet P C Q)
  then show ?case
    using rule_exists by blast
next
  case (RuleSeq P C1 R C2 Q)
  then show ?case
    using seq_rule by meson
next
  case (RuleIf P C1 Q1 C2 Q2)
  then show ?case
    using if_rule by blast
next
  case (RuleAssume P b)
  then show ?case
    by (simp add: assume_rule)
next
  case (RuleWhile I C)
  then show ?case
    using while_rule by blast
next
  case (RuleAssign x e)
  then show ?case
    by (simp add: assign_rule)
next
  case (RuleHavoc x)
  then show ?case
    using havoc_rule by fastforce
qed



subsection ‹Completeness›

definition complete
  where
  "complete P C Q ⟷ (⊨ {P} C {Q} ⟶ ⊢ {P} C {Q})"

lemma completeI:
  assumes "⊨ {P} C {Q} ⟹ ⊢ {P} C {Q}"
  shows "complete P C Q"
  by (simp add: assms complete_def)

lemma completeE:
  assumes "complete P C Q"
      and "⊨ {P} C {Q}"
    shows "⊢ {P} C {Q}"
  using assms complete_def by auto

lemma complete_if_aux:
  assumes "hyper_hoare_triple A (If C1 C2) B"
  shows "entails (λS'. ∃S. A S ∧ S' = sem C1 S ∪ sem C2 S) B"
proof (rule entailsI)
  fix S' assume "∃S. A S ∧ S' = sem C1 S ∪ sem C2 S"
  then show "B S'"
    by (metis assms hyper_hoare_tripleE sem_if)
qed

lemma complete_if:
  fixes P Q :: "('lvar, 'lval, 'pvar, 'pval) state hyperassertion"
  assumes "⋀P1 Q1 :: ('lvar, 'lval, 'pvar, 'pval) state hyperassertion. complete P1 C1 Q1"
      and "⋀P2 Q2 :: ('lvar, 'lval, 'pvar, 'pval) state hyperassertion. complete P2 C2 Q2"
    shows "complete P (If C1 C2) Q"
proof (rule completeI)
  assume asm0: "⊨ {P} If C1 C2 {Q}"

  show "⊢ {P} stmt.If C1 C2 {Q}"
  proof (rule RuleCons)
    show "⊢ {exists (λV S. P S ∧ S = V)} stmt.If C1 C2 {exists (λV. join (λS. S = sem C1 V ∧ P V) (λS. S = sem C2 V))}"
    proof (rule RuleExistsSet)
      fix V
      show "⊢ {(λS. P S ∧ S = V)} stmt.If C1 C2 {join (λS. S = sem C1 V ∧ P V) (λS. S = sem C2 V)}"
      proof (rule RuleIf)
        show "⊢ {(λS. P S ∧ S = V)} C1 {λS. S = sem C1 V ∧ P V}"
          by (simp add: assms(1) completeE hyper_hoare_triple_def)
        show "⊢ {(λS. P S ∧ S = V)} C2 {λS. S = sem C2 V}"
          by (simp add: assms(2) completeE hyper_hoare_triple_def)
      qed
    qed
    show "entails P (exists (λV S. P S ∧ S = V))"
      by (simp add: entailsI exists_def)
    show "entails (exists (λV. join (λS. S = sem C1 V ∧ P V) (λS. S = sem C2 V))) Q"
    proof (rule entailsI)
      fix S assume "exists (λV. join (λS. S = sem C1 V ∧ P V) (λS. S = sem C2 V)) S"
      then obtain V where "join (λS. S = sem C1 V ∧ P V) (λS. S = sem C2 V) S"
        by (meson exists_def)
      then obtain S1 S2 where "S = S1 ∪ S2" "S1 = sem C1 V ∧ P V" "S2 = sem C2 V"
        by (simp add: join_def)
      then show "Q S"
        by (metis asm0 hyper_hoare_tripleE sem_if)
    qed
  qed
qed

lemma complete_seq_aux:
  assumes "hyper_hoare_triple A (Seq C1 C2) B"
  shows "∃R. hyper_hoare_triple A C1 R ∧ hyper_hoare_triple R C2 B"
proof -
  let ?R = "λS. ∃S'. A S' ∧ S = sem C1 S'"
  have "hyper_hoare_triple A C1 ?R"
    using hyper_hoare_triple_def by blast
  moreover have "hyper_hoare_triple ?R C2 B"
  proof (rule hyper_hoare_tripleI)
    fix S assume "∃S'. A S' ∧ S = sem C1 S'"
    then obtain S' where asm0: "A S'" "S = sem C1 S'"
      by blast
    then show "B (sem C2 S)"
      by (metis assms hyper_hoare_tripleE sem_seq)
  qed
  ultimately show ?thesis by blast
qed


lemma complete_assume:
  "complete P (Assume b) Q"
proof (rule completeI)
  assume asm0: "⊨ {P} Assume b {Q}"
  show "⊢ {P} Assume b {Q}"
  proof (rule RuleCons)
    show "⊢ { (λS. Q (Set.filter (b ∘ snd) S)) } (Assume b) {Q}"
      by (simp add: RuleAssume)
    show "entails P (λS. Q (Set.filter (b ∘ snd) S))"
      by (metis (mono_tags, lifting) asm0 assume_sem entails_def hyper_hoare_tripleE)
    show "entails Q Q"      
      by (simp add: entailsI)
  qed
qed

lemma complete_skip:
  "complete P Skip Q"
  using completeI RuleSkip
  by (metis (mono_tags, lifting) entails_def hyper_hoare_triple_def sem_skip RuleCons)

lemma complete_assign:
  "complete P (Assign x e) Q"
proof (rule completeI)
  assume asm0: "⊨ {P} Assign x e {Q}"
  show "⊢ {P} Assign x e {Q}"
  proof (rule RuleCons)
    show "⊢ {(λS. Q {(l, σ(x := e σ)) |l σ. (l, σ) ∈ S})} Assign x e {Q}"
      by (simp add: RuleAssign)
    show "entails P (λS. Q {(l, σ(x := e σ)) |l σ. (l, σ) ∈ S})"
    proof (rule entailsI)
      fix S assume "P S"
      then show "Q {(l, σ(x := e σ)) |l σ. (l, σ) ∈ S}"
        by (metis asm0 hyper_hoare_triple_def sem_assign)
    qed
    show "entails Q Q"
      by (simp add: entailsI)
  qed
qed

lemma complete_havoc:
  "complete P (Havoc x) Q"
proof (rule completeI)
  assume asm0: "⊨ {P} Havoc x {Q}"
  show "⊢ {P} Havoc x {Q}"
  proof (rule RuleCons)
    show "⊢ { (λS. Q { (l, σ(x := v)) |l σ v. (l, σ) ∈ S }) } (Havoc x) {Q}"
      using RuleHavoc by fast
    show "entails P (λS. Q {(l, σ(x := v)) |l σ v. (l, σ) ∈ S})"
    proof (rule entailsI)
      fix S assume "P S"
      then show "Q {(l, σ(x := v)) |l σ v. (l, σ) ∈ S}"
        by (metis asm0 hyper_hoare_triple_def sem_havoc)
    qed
    show "entails Q Q"
      by (simp add: entailsI)
  qed
qed

lemma complete_seq:
  assumes "⋀R. complete P C1 R"
      and "⋀R. complete R C2 Q"
    shows "complete P (Seq C1 C2) Q"
  by (meson RuleSeq assms(1) assms(2) completeE completeI complete_seq_aux)



fun construct_inv
  where
  "construct_inv P C 0 = P"
| "construct_inv P C (Suc n) = (λS. (∃S'. S = sem C S' ∧ construct_inv P C n S'))"

lemma iterate_sem_ind:
  assumes "construct_inv P C n S'"
  shows "∃S. P S ∧ S' = iterate_sem n C S"
  using assms
by (induct n arbitrary: S') (auto)


lemma complete_while_aux:
  assumes "hyper_hoare_triple (λS. P S ∧ S = V) (While C) Q"
  shows "entails (natural_partition (construct_inv (λS. P S ∧ S = V) C)) Q"
proof (rule entailsI)
  fix S assume "natural_partition (construct_inv (λS. P S ∧ S = V) C) S"

  then obtain F where asm0: "S = (⋃n. F n)" "⋀n. construct_inv (λS. P S ∧ S = V) C n (F n)"
    using natural_partitionE by blast
  then have "P (F 0) ∧ F 0 = V"
    by (metis (mono_tags, lifting) construct_inv.simps(1))
  then have "Q (⋃n. iterate_sem n C (F 0))"
    using assms hyper_hoare_triple_def[of "λS. P S ∧ S = V" "While C" Q] sem_while
    by metis
  moreover have "⋀n. F n = iterate_sem n C V"
  proof -
    fix n
    obtain S' where "P S' ∧ S' = V" "F n = iterate_sem n C S'"
      using asm0(2) iterate_sem_ind by blast
    then show "F n = iterate_sem n C V"
      by simp
  qed
  ultimately show "Q S"
    using asm0(1) by auto
qed

lemma complete_while:
  fixes P Q :: "('lvar, 'lval, 'pvar, 'pval) state hyperassertion"
  assumes "⋀P' Q' :: ('lvar, 'lval, 'pvar, 'pval) state hyperassertion. complete P' C Q'"
    shows "complete P (While C) Q"
proof (rule completeI)
  assume asm0: "hyper_hoare_triple P (While C) Q"

  let ?I = "λV. construct_inv (λS. P S ∧ S = V) C"

  have r: "⋀V. syntactic_HHT (?I V 0) (While C) (natural_partition (?I V))"
  proof (rule RuleWhile)
    fix V n show "syntactic_HHT (construct_inv (λS. P S ∧ S = V) C n) C (construct_inv (λS. P S ∧ S = V) C (Suc n))"
      by (meson assms completeE construct_inv.simps(2) hyper_hoare_tripleI)
  qed

  show "syntactic_HHT P (While C) Q"
  proof (rule RuleCons)
    show "syntactic_HHT (exists (λV. ?I V 0)) (While C) (exists (λV. ((natural_partition (?I V)))))"
      using r by (rule RuleExistsSet)
    show "entails P (exists (λV. construct_inv (λS. P S ∧ S = V) C 0))"
      by (simp add: entailsI exists_def)
    show "entails (exists (λV. natural_partition (construct_inv (λS. P S ∧ S = V) C))) Q"
    proof (rule entailsI)
      fix S' assume "exists (λV. natural_partition (construct_inv (λS. P S ∧ S = V) C)) S'"
      then obtain V where "natural_partition (construct_inv (λS. P S ∧ S = V) C) S'"
        by (meson exists_def)
      moreover have "entails (natural_partition (construct_inv (λS. P S ∧ S = V) C)) Q"
      proof (rule complete_while_aux)
        show "hyper_hoare_triple (λS. P S ∧ S = V) (While C) Q"
          using asm0 hyper_hoare_triple_def[of "λS. P S ∧ S = V"]
          hyper_hoare_triple_def[of P "While C" Q] by auto
      qed
      ultimately show "Q S'"
        by (simp add: entails_def)
    qed
  qed
qed


text ‹Theorem 2›

theorem completeness:
  fixes P Q :: "('lvar, 'lval, 'pvar, 'pval) state hyperassertion"
  assumes "⊨ {P} C {Q}"
  shows "⊢ {P} C {Q}"
  using assms
proof (induct C arbitrary: P Q)
  case (Assign x1 x2)
  then show ?case
    using completeE complete_assign by fast
next
  case (Seq C1 C2)
  then show ?case
    using complete_def complete_seq by meson
next
  case (If C1 C2)
  then show ?case
    using complete_def complete_if by meson
next
  case Skip
  then show ?case
    using complete_def complete_skip by meson
next
  case (Havoc x)
  then show ?case
    by (simp add: completeE complete_havoc)
next
  case (Assume b)
  then show ?case
    by (simp add: completeE complete_assume)
next
  case (While C)
  then show ?case
    using complete_def complete_while by blast
qed




subsection ‹Disproving Hyper-Triples›

definition sat where "sat P ⟷ (∃S. P S)"

text ‹Theorem 5›

theorem disproving_triple:
  "¬ ⊨ {P} C {Q} ⟷ (∃P'. sat P' ∧ entails P' P ∧ ⊨ {P'} C {λS. ¬ Q S})" (is "?A ⟷ ?B")
proof
  assume "¬ ⊨ {P} C {Q}"
  then obtain S where asm0: "P S" "¬ Q (sem C S)"
    using hyper_hoare_triple_def by blast
  let ?P = "λS'. S = S'"
  have "entails ?P P"
    by (simp add: asm0(1) entails_def)
  moreover have "⊨ {?P} C {λS. ¬ Q S}"
    by (simp add: asm0(2) hyper_hoare_triple_def)
  moreover have "sat ?P"
    by (simp add: sat_def)
  ultimately show ?B by blast
next
  assume "∃P'. sat P' ∧ entails P' P ∧ ⊨ {P'} C {λS. ¬ Q S}"
  then obtain P' where asm0: "sat P'" "entails P' P" "⊨ {P'} C {λS. ¬ Q S}"
    by blast
  then obtain S where "P' S"
    by (meson sat_def)
  then show ?A
    using asm0(2) asm0(3) entailsE hyper_hoare_tripleE
    by (metis (no_types, lifting))
qed

definition differ_only_by where
  "differ_only_by a b x ⟷ (∀y. y ≠ x ⟶ a y = b y)"

lemma differ_only_byI:
  assumes "⋀y. y ≠ x ⟹ a y = b y"
  shows "differ_only_by a b x"
  by (simp add: assms differ_only_by_def)

lemma diff_by_update:
  "differ_only_by (a(x := v)) a x"
  by (simp add: differ_only_by_def)

lemma diff_by_comm:
  "differ_only_by a b x ⟷ differ_only_by b a x"
  by (metis (mono_tags, lifting) differ_only_by_def)

lemma diff_by_trans:
  assumes "differ_only_by a b x"
      and "differ_only_by b c x"
    shows "differ_only_by a c x"
  by (metis assms(1) assms(2) differ_only_by_def)


definition not_free_var_of where
  "not_free_var_of P x ⟷ (∀states states'.
  (∀i. differ_only_by (fst (states i)) (fst (states' i)) x ∧ snd (states i) = snd (states' i))
  ⟶ (states ∈ P ⟷ states' ∈ P))"


lemma not_free_var_ofE:
  assumes "not_free_var_of P x"
      and "⋀i. differ_only_by (fst (states i)) (fst (states' i)) x"
      and "⋀i. snd (states i) = snd (states' i)"
      and "states ∈ P"
    shows "states' ∈ P"
  using not_free_var_of_def[of P x] assms by blast


subsection ‹Synchronized Rule for Branching›

definition combine where
  "combine from_nat x P1 P2 S ⟷ P1 (Set.filter (λφ. fst φ x = from_nat 1) S) ∧ P2 (Set.filter (λφ. fst φ x = from_nat 2) S)"

lemma combineI:
  assumes "P1 (Set.filter (λφ. fst φ x = from_nat 1) S) ∧ P2 (Set.filter (λφ. fst φ x = from_nat 2) S)"
  shows "combine from_nat x P1 P2 S"
  by (simp add: assms combine_def)

definition modify_lvar_to where
  "modify_lvar_to x v φ = ((fst φ)(x := v), snd φ)"

lemma logical_var_in_sem_same:
  assumes "⋀φ. φ ∈ S ⟹ fst φ x = a"
      and "φ' ∈ sem C S"
    shows "fst φ' x = a"
  by (metis assms(1) assms(2) fst_conv in_sem)

lemma recover_after_sem:
  assumes "a ≠ b"
      and "⋀φ. φ ∈ S1 ⟹ fst φ x = a"
      and "⋀φ. φ ∈ S2 ⟹ fst φ x = b"
    shows "sem C S1 = Set.filter (λφ. fst φ x = a) (sem C (S1 ∪ S2))" (is "?A = ?B")
proof
  have r: "sem C (S1 ∪ S2) = sem C S1 ∪ sem C S2"
    by (simp add: sem_union)
  moreover have r1: "⋀φ'. φ' ∈ sem C S1 ⟹ fst φ' x = a"
    by (metis assms(2) fst_conv in_sem)
  moreover have r2: "⋀φ'. φ' ∈ sem C S2 ⟹ fst φ' x = b"
    by (metis assms(3) fst_conv in_sem)
  show "?B ⊆ ?A"
  proof (rule subsetPairI)
    fix l σ
    assume "(l, σ) ∈ Set.filter (λφ. fst φ x = a) (sem C (S1 ∪ S2))"
    then show "(l, σ) ∈ sem C S1"
      using assms(1) r r2 by auto
  qed
  show "?A ⊆ ?B"
    by (simp add: r r1 subsetI)
qed

lemma injective_then_ok:
  assumes "a ≠ b"
      and "S1' = (modify_lvar_to x a) ` S1"
      and "S2' = (modify_lvar_to x b) ` S2"
    shows "Set.filter (λφ. fst φ x = a) (S1' ∪ S2') = S1'" (is "?A = ?B")
proof
  show "?B ⊆ ?A"
  proof (rule subsetI)
    fix y assume "y ∈ S1'"
    then have "fst y x = a" using modify_lvar_to_def assms(2)
      by (metis (mono_tags, lifting) fst_conv fun_upd_same image_iff)
    then show "y ∈ Set.filter (λφ. fst φ x = a) (S1' ∪ S2')"
      by (simp add: ‹y ∈ S1'›)
  qed
  show "?A ⊆ ?B"
  proof
    fix y assume "y ∈ ?A"
    then have "y ∉ S2'"
      by (metis (mono_tags, lifting) assms(1) assms(3) fun_upd_same image_iff member_filter modify_lvar_to_def prod.sel(1))
    then show "y ∈ ?B"
      using ‹y ∈ Set.filter (λφ. fst φ x = a) (S1' ∪ S2')› by auto
  qed
qed

definition not_free_var_hyper where
  "not_free_var_hyper x P ⟷ (∀S v. P S ⟷ P ((modify_lvar_to x v) ` S))"

definition injective where
  "injective f ⟷ (∀a b. a ≠ b ⟶ f a ≠ f b)"

lemma sem_of_modify_lvar:
  "sem C ((modify_lvar_to r v) ` S) = (modify_lvar_to r v) ` (sem C S)" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetI)
    fix y assume asm0: "y ∈ ?A"
    then obtain x where "x ∈ (modify_lvar_to r v) ` S" "single_sem C (snd x) (snd y)" "fst x = fst y"
      by (metis fst_conv in_sem snd_conv)
    then obtain xx where "xx ∈ S" "x = modify_lvar_to r v xx"
      by blast
    then have "(fst xx, snd y) ∈ sem C S"
      by (metis ‹⟨C, snd x⟩ → snd y› fst_conv in_sem modify_lvar_to_def prod.collapse snd_conv)
    then show "y ∈ ?B"
      by (metis ‹fst x = fst y› ‹x = modify_lvar_to r v xx› fst_eqD modify_lvar_to_def prod.exhaust_sel rev_image_eqI snd_eqD)
  qed
  show "?B ⊆ ?A"
  proof (rule subsetI)
    fix y assume "y ∈ modify_lvar_to r v ` sem C S"
    then obtain yy where "y = modify_lvar_to r v yy" "yy ∈ sem C S"
      by blast
    then obtain x where "x ∈ S" "fst x = fst yy" "single_sem C (snd x) (snd yy)"
      by (metis fst_conv in_sem snd_conv)
    then have "fst (modify_lvar_to r v x) = fst y"
      by (simp add: ‹y = modify_lvar_to r v yy› modify_lvar_to_def)
    then show "y ∈ sem C (modify_lvar_to r v ` S)"
      by (metis (mono_tags, lifting) ‹⟨C, snd x⟩ → snd yy› ‹x ∈ S› ‹y = modify_lvar_to r v yy› fst_conv
          image_eqI in_sem modify_lvar_to_def snd_conv)
  qed
qed

end