Theory Compositionality

section ‹Compositionality Rules›

theory Compositionality
  imports Logic Expressivity Loops
begin

text ‹In this file, we prove the soundness of all compositionality rules presented in Appendix D (figure 11).›

definition in_set where
  "in_set φ S ⟷ φ ∈ S"

subsection ‹Linking rule›

proposition rule_linking:
  assumes "⋀φ1 (φ2 :: ('a, 'b, 'c, 'd) state). fst φ1 = fst φ2 ∧ ( ⊨ { (in_set φ1 :: (('a, 'b, 'c, 'd) state) hyperassertion) } C { in_set φ2 } )
  ⟹ ( ⊨ { (P φ1 :: (('a, 'b, 'c, 'd) state) hyperassertion) } C { Q φ2 } )"
  shows "⊨ { ((λS. ∀φ1 ∈ S. P φ1 S) :: (('a, 'b, 'c, 'd) state) hyperassertion) } C { (λS. ∀φ2 ∈ S. Q φ2 S) }"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "∀φ1∈S. P φ1 S"
  show "∀φ2∈sem C S. Q φ2 (sem C S)"
  proof (clarify)
    fix l σ' assume "(l, σ') ∈ sem C S"
    then obtain σ where "(l, σ) ∈ S" "single_sem C σ σ'"
      by (metis fst_conv in_sem snd_conv)
    then show "Q (l, σ') (sem C S)"
      by (metis (mono_tags, opaque_lifting) asm0 assms fst_eqD hyper_hoare_triple_def in_set_def single_step_then_in_sem)
  qed
qed


lemma rule_linking_alt:
  assumes "⋀l σ σ'. single_sem C σ σ' ⟹ ( ⊨ { P (l, σ) } C { Q (l, σ') } )"
  shows "⊨ { (λS. ∀ω ∈ S. P ω S) } C { (λS. ∀ω' ∈ S. Q ω' S) }"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "∀ω∈S. P ω S"
  show "∀ω'∈sem C S. Q ω' (sem C S)"
  proof (clarify)
    fix l σ' assume "(l, σ') ∈ sem C S"
    then obtain σ where "(l, σ) ∈ S" "single_sem C σ σ'"
      by (metis fst_conv in_sem snd_conv)
    then have "⊨ { P (l, σ) } C { Q (l, σ') }"
      by (simp add: assms)
    then show "Q (l, σ') (sem C S)"
      by (simp add: ‹(l, σ) ∈ S› asm0 hyper_hoare_tripleE)
  qed
qed

subsection ‹Frame rules›

lemma rule_lframe:

  fixes b :: "('a ⇒ ('lvar ⇒ 'lval)) ⇒ bool"
―‹b takes a mapping from keys to logical states (representing the tuple), and returns a boolean›

  shows "⊨ { (λS. ∀φ. (∀k. φ k ∈ S) ⟶ b (fst ∘ φ)) } C { λS. ∀φ. (∀k. φ k ∈ S) ⟶ b (fst ∘ φ) }"

proof (rule hyper_hoare_tripleI)
  fix S :: "('lvar, 'lval, 'b, 'c) state set"
  assume asm0: "∀φ. (∀k. φ k ∈ S) ⟶ b (fst ∘ φ)"
  show "∀φ. (∀k. φ k ∈ sem C S) ⟶ b (fst ∘ φ)"
  proof (clarify)
    fix φ' :: "'a ⇒ ('lvar, 'lval, 'b, 'c) state"
    assume asm1: "∀k. φ' k ∈ sem C S"
    let ?φ = "λk. SOME φk. fst φk = fst (φ' k) ∧ φk ∈ S ∧ single_sem C (snd φk) (snd (φ' k))"
    have r: "⋀k. fst (?φ k) = fst (φ' k) ∧ (?φ k) ∈ S ∧ single_sem C (snd (?φ k)) (snd (φ' k))"
    proof -
      fix k show "fst (?φ k) = fst (φ' k) ∧ (?φ k) ∈ S ∧ single_sem C (snd (?φ k)) (snd (φ' k))"
      proof (rule someI_ex)
        show "∃x. fst x = fst (φ' k) ∧ x ∈ S ∧ ⟨C, snd x⟩ → snd (φ' k)"
          by (metis asm1 fst_conv in_sem snd_conv)
      qed
    qed
    then have "b (fst ∘ ?φ)"
      using asm0 by presburger
    moreover have "fst ∘ ?φ = fst ∘ φ'"
      using ext r by fastforce
    then show "b (fst ∘ φ')"
      using calculation by presburger
  qed
qed

lemma rule_lframe_single:
  "⊨ { (λS. ∀ω ∈ S. P (fst ω)) } C { λS. ∀ω ∈ S. P (fst ω) }"
proof -
  let ?P = "λφ. P (φ ())"
  have "⊨ { (λS. ∀φ. (∀k. φ k ∈ S) ⟶ ?P (fst ∘ φ)) } C { λS. ∀φ. (∀k. φ k ∈ S) ⟶ ?P (fst ∘ φ) }"
    using rule_lframe by fast
  moreover have "(λS. ∀ω ∈ S. P (fst ω)) = (λS. ∀φ. (∀k. φ k ∈ S) ⟶ ?P (fst ∘ φ))"
    using ext by fastforce
  ultimately show ?thesis
    using forw_subst ssubst order_trans_rules(13) prop_subst basic_trans_rules(13)
    by fast
qed

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

lemma differ_only_by_psetI:
  assumes "⋀i. fst (a i) = fst (b i) ∧ differ_only_by_set vars (snd (a i)) (snd (b i))"
  shows "differ_only_by_pset vars a b"
  by (simp add: assms differ_only_by_pset_def)

definition not_in_free_pvars_prop where
  "not_in_free_pvars_prop vars b ⟷ (∀φ1 φ2. differ_only_by_pset vars φ1 φ2 ⟶ (b φ1 ⟷ b φ2))"

proposition rule_frame:

  fixes b :: "('a ⇒ ('lvar, 'lval, 'pvar, 'pval) state) ⇒ bool"
―‹b takes a mapping from keys to extended states (representing the tuple), and returns a boolean›

  assumes "not_in_free_pvars_prop (written_vars C) b"

  shows "⊨ { (λS. ∀φ. (∀k. φ k ∈ S) ⟶ b φ) } C { λS. ∀φ. (∀k. φ k ∈ S) ⟶ b φ }"

proof (rule hyper_hoare_tripleI)
  fix S :: "('lvar, 'lval, 'pvar, 'pval) state set"
  assume asm0: "∀φ. (∀k. φ k ∈ S) ⟶ b φ"
  show "∀φ. (∀k. φ k ∈ sem C S) ⟶ b φ"
  proof (clarify)
    fix φ' :: "'a ⇒ ('lvar, 'lval, 'pvar, 'pval) state"
    assume asm1: "∀k. φ' k ∈ sem C S"
    let ?φ = "λk. SOME φk. fst φk = fst (φ' k) ∧ φk ∈ S ∧ single_sem C (snd φk) (snd (φ' k))"
    have r: "⋀k. fst (?φ k) = fst (φ' k) ∧ (?φ k) ∈ S ∧ single_sem C (snd (?φ k)) (snd (φ' k))"
    proof -
      fix k show "fst (?φ k) = fst (φ' k) ∧ (?φ k) ∈ S ∧ single_sem C (snd (?φ k)) (snd (φ' k))"
      proof (rule someI_ex)
        show "∃x. fst x = fst (φ' k) ∧ x ∈ S ∧ ⟨C, snd x⟩ → snd (φ' k)"
          by (metis asm1 fst_conv in_sem snd_conv)
      qed
    qed
    then have "b ?φ"
      using asm0 by presburger
    moreover have "differ_only_by_pset (written_vars C) ?φ φ'"
    proof (rule differ_only_by_psetI)
      fix i show "fst (SOME φk. fst φk = fst (φ' i) ∧ φk ∈ S ∧ ⟨C, snd φk⟩ → snd (φ' i)) = fst (φ' i) ∧
       differ_only_by_set (written_vars C) (snd (SOME φk. fst φk = fst (φ' i) ∧ φk ∈ S ∧ ⟨C, snd φk⟩ → snd (φ' i))) (snd (φ' i))"
        by (metis (mono_tags, lifting) differ_only_by_set_def r written_vars_not_modified)
    qed
    ultimately show "b φ'"
      using assms not_in_free_pvars_prop_def by blast
  qed
qed


subsection ‹Logical Updates›

definition equal_outside_set where
  "equal_outside_set vars l1 l2 ⟷ (∀x. x ∉ vars ⟶ l1 x = l2 x)"

lemma equal_outside_setI:
  assumes "⋀x. x ∉ vars ⟹ l1 x = l2 x"
  shows "equal_outside_set vars l1 l2"
  using assms equal_outside_set_def by auto

lemma equal_outside_setE:
  assumes "equal_outside_set vars l1 l2"
      and "x ∉ vars"
    shows "l1 x = l2 x"
  using assms equal_outside_set_def by meson

lemma equal_outside_sym:
  "equal_outside_set vars l l' ⟷ equal_outside_set vars l' l"
  by (metis equal_outside_set_def)

definition subset_mod_updates where
  "subset_mod_updates vars S S' ⟷ (∀ω ∈ S. ∃ω' ∈ S'. snd ω = snd ω' ∧ equal_outside_set vars (fst ω) (fst ω'))"

lemma subset_mod_updatesI:
  assumes "⋀ω. ω ∈ S ⟹ (∃ω' ∈ S'. snd ω = snd ω' ∧ equal_outside_set vars (fst ω) (fst ω'))"
  shows "subset_mod_updates vars S S'"
  by (simp add: assms subset_mod_updates_def)

lemma subset_mod_updatesE:
  assumes "subset_mod_updates vars S S'"
      and "ω ∈ S"
    shows "∃ω' ∈ S'. snd ω = snd ω' ∧ equal_outside_set vars (fst ω) (fst ω')"
  using assms(1) assms(2) subset_mod_updates_def by blast


definition same_mod_updates where
  "same_mod_updates vars S S' ⟷ subset_mod_updates vars S S' ∧ subset_mod_updates vars S' S"

lemma same_mod_updatesI:
  assumes "⋀ω. ω ∈ S ⟹ (∃ω' ∈ S'. snd ω = snd ω' ∧ equal_outside_set vars (fst ω) (fst ω'))"
      and "⋀ω'. ω' ∈ S' ⟹ (∃ω ∈ S. snd ω = snd ω' ∧ equal_outside_set vars (fst ω') (fst ω))"
    shows "same_mod_updates vars S S'"
  by (metis assms(1) assms(2) same_mod_updates_def subset_mod_updates_def)

lemma same_mod_updates_sym:
  "same_mod_updates vars S S' ⟷ same_mod_updates vars S' S"
  using same_mod_updates_def by blast

lemma same_mod_updates_refl:
  "same_mod_updates vars S S"
  by (metis equal_outside_set_def same_mod_updates_def subset_mod_updates_def)

lemma equal_outside_set_trans:
  assumes "equal_outside_set vars a b"
      and "equal_outside_set vars b c"
    shows "equal_outside_set vars a c"
  using equal_outside_set_def[of vars a b] equal_outside_set_def[of vars b c] equal_outside_set_def[of vars a c] assms
  by presburger

lemma subset_mod_updates_trans:
  assumes "subset_mod_updates vars S1 S2"
      and "subset_mod_updates vars S2 S3"
    shows "subset_mod_updates vars S1 S3"
proof (rule subset_mod_updatesI)
  fix ω1 assume "ω1 ∈ S1"
  then obtain ω2 where "ω2 ∈ S2" "snd ω1 = snd ω2 ∧ equal_outside_set vars (fst ω1) (fst ω2)"
    using assms(1) same_mod_updates_def subset_mod_updatesE by blast
  then show "∃ω'∈S3. snd ω1 = snd ω' ∧ equal_outside_set vars (fst ω1) (fst ω')"
    by (metis (no_types, lifting) assms(2) equal_outside_set_trans subset_mod_updatesE)
qed

lemma same_mod_updates_trans:
  assumes "same_mod_updates vars S1 S2"
      and "same_mod_updates vars S2 S3"
    shows "same_mod_updates vars S1 S3"
  by (meson assms(1) assms(2) same_mod_updates_def subset_mod_updates_trans)


lemma sem_update_commute_aux:
  assumes "subset_mod_updates vars S1 S2"
  shows "subset_mod_updates vars (sem C S1) (sem C S2)"
proof (rule subset_mod_updatesI)
  fix ω1 assume asm0: "ω1 ∈ sem C S1"
  then obtain l1 σ where "(l1, σ) ∈ S1" "single_sem C σ (snd ω1)" "fst ω1 = l1"
    by (metis in_sem)
  then obtain l2 where "(l2, σ) ∈ S2" "equal_outside_set vars l1 l2"
    using assms subset_mod_updatesE by fastforce
  then show "∃ω'∈sem C S2. snd ω1 = snd ω' ∧ equal_outside_set vars (fst ω1) (fst ω')"
    by (metis ‹⟨C, σ⟩ → snd ω1› ‹fst ω1 = l1› fst_conv in_sem snd_conv)
qed


lemma sem_update_commute:
  assumes "same_mod_updates (vars :: 'a set) S1 S2"
  shows "same_mod_updates vars (sem C S1) (sem C S2)"
  using assms same_mod_updates_def sem_update_commute_aux by blast



type_synonym ('a, 'b, 'c, 'd) chyperassertion = "(('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool"

definition invariant_on_updates :: "'a set ⇒ ('a, 'b, 'c, 'd) chyperassertion ⇒ bool" where
  "invariant_on_updates vars P ⟷ (∀S S'. same_mod_updates vars S S' ⟶ (P S ⟷ P S'))"

lemma invariant_on_updatesI:
  assumes "⋀S S'. same_mod_updates vars S S' ⟹ P S ⟹ P S'"
  shows "invariant_on_updates vars P"
  using assms invariant_on_updates_def same_mod_updates_sym by blast

definition entails_with_updates :: "'a set ⇒ ('a, 'b, 'c, 'd) chyperassertion ⇒ ('a, 'b, 'c, 'd) chyperassertion ⇒ bool"
  where
  "entails_with_updates vars P Q ⟷ (∀S. P S ⟶ (∃S'. same_mod_updates vars S S' ∧ Q S'))"

lemma entails_with_updatesI:
  assumes "⋀S. P S ⟹ (∃S'. same_mod_updates vars S S' ∧ Q S')"
  shows "entails_with_updates vars P Q"
  by (simp add: assms entails_with_updates_def)


lemma entails_with_updatesE:
  assumes "entails_with_updates vars P Q"
      and "P S"
    shows "∃S'. same_mod_updates vars S S' ∧ Q S'"
  by (meson assms(1) assms(2) entails_with_updates_def)


proposition rule_LUpdate:
  assumes "⊨ {P'} C {Q}"
      and "entails_with_updates vars P P'"
      and "invariant_on_updates vars Q"
    shows "⊨ {P} C {Q}"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "P S"
  then obtain S' where "same_mod_updates vars S S' ∧ P' S'"
    using assms(2) entails_with_updatesE by blast
  then have "same_mod_updates vars (sem C S) (sem C S')"
    using sem_update_commute by blast
  moreover have "Q (sem C S')"
    using ‹same_mod_updates vars S S' ∧ P' S'› assms(1) hyper_hoare_tripleE by auto
  ultimately show "Q (sem C S)"
    using assms(3) invariant_on_updates_def by blast
qed




subsection ‹Filters›

lemma filter_prop_commute_aux:
  assumes "⋀ω ω'. fst ω = fst ω' ⟹ (f ω ⟷ f ω')"
  shows "Set.filter f (sem C S) = sem C (Set.filter f S)" (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix ω' assume "ω' ∈ ?A"
    then obtain ω where "ω ∈ S" "single_sem C (snd ω) (snd ω')" "fst ω' = fst ω" "f ω'"
      by (auto simp add: in_sem)
    then show "ω' ∈ ?B"
      using assms [OF ‹fst ω' = fst ω›] by (auto simp add: in_sem intro: exI [of _ ‹snd ω›])
  qed
  show "?B ⊆ ?A"
  proof
    fix x assume "x ∈ sem C (Set.filter f S)"
    then show "x ∈ Set.filter f (sem C S)"
      by simp (metis (mono_tags, lifting) assms fst_conv in_sem mem_Collect_eq)
  qed
qed

definition commute_with_sem where
  "commute_with_sem f ⟷ (∀S C. f (sem C S) = sem C (f S))"

lemma commute_with_semI:
  assumes "⋀(S :: (('a ⇒ 'b) × ('c ⇒ 'd)) set) C. f (sem C S) = sem C (f S)"
  shows "commute_with_sem f"
  by (simp add: assms commute_with_sem_def)

lemma filter_prop_commute:
  assumes "⋀ω ω'. fst ω = fst ω' ⟹ (f ω ⟷ f ω')"
  shows "commute_with_sem (Set.filter f)"
  using assms commute_with_sem_def filter_prop_commute_aux by blast

lemma rule_apply:
  assumes "⊨ {P} C {Q}"
      and "commute_with_sem f"
    shows "⊨ {P ∘ f} C {Q ∘ f}"
proof (rule hyper_hoare_tripleI)
  fix S assume "(P ∘ f) S"
  then show "(Q ∘ f) (sem C S)"
    by (metis assms(1) assms(2) commute_with_sem_def comp_apply hyper_hoare_tripleE)
qed

definition apply_filter where
  "apply_filter b P S ⟷ P (Set.filter b S)"

proposition rule_LFilter:
  assumes "⊨ {P} C {Q}"
  shows "⊨ { P ∘ (Set.filter (b ∘ fst)) } C { Q ∘ (Set.filter (b ∘ fst)) }"
  by (simp add: assms filter_prop_commute rule_apply)


definition differ_only_by_pset_single where
  "differ_only_by_pset_single vars a b ⟷ (fst a = fst b ∧ differ_only_by_set vars (snd a) (snd b))"

definition not_in_free_pvars_pexp where
  "not_in_free_pvars_pexp vars b ⟷ (∀φ1 φ2. differ_only_by_set vars φ1 φ2 ⟶ (b φ1 ⟷ b φ2))"

lemma single_sem_differ_by_written_vars:
  assumes "single_sem C φ φ'"
  shows "differ_only_by_set (written_vars C) φ φ'"
  by (meson assms differ_only_by_set_def written_vars_not_modified)

lemma single_sem_not_free_vars:
  assumes "not_in_free_pvars_pexp (written_vars C) b"
      and "single_sem C φ φ'"
    shows "b φ ⟷ b φ'"
  using assms(1) assms(2) not_in_free_pvars_pexp_def single_sem_differ_by_written_vars by blast


proposition rule_PFilter:
  assumes "⊨ {P} C {Q}"
      and "not_in_free_pvars_pexp (written_vars C) b"
  shows "⊨ { P ∘ (Set.filter (b ∘ snd)) } C { Q ∘ (Set.filter (b ∘ snd)) }"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "(P ∘ Set.filter (b ∘ snd)) S"
  let ?S = "Set.filter (b ∘ snd) S"
  have "Q (sem C ?S)"
    using asm0 assms(1) hyper_hoare_tripleE by auto
  moreover have "sem C ?S = Set.filter (b ∘ snd) (sem C S)" (is "?A = ?B")
  proof
    show "?B ⊆ ?A"
    proof
      fix φ' assume "φ' ∈ Set.filter (b ∘ snd) (sem C S)"
      then obtain φ where "φ ∈ S" "fst φ = fst φ'" "single_sem C (snd φ) (snd φ')" "b (snd φ')"
        by (auto simp add: in_sem)
      then have "b (snd φ)"
        using single_sem_not_free_vars[of C b "snd φ" "snd φ'"] assms(2)
        by simp
      then show "φ' ∈ ?A"
        using ‹⟨C, snd φ⟩ → snd φ'› ‹φ ∈ S› ‹fst φ = fst φ'› [symmetric]
        by (auto simp add: in_sem intro: exI [of _ ‹snd φ›])
    qed
    show "?A ⊆ ?B"
    proof
      fix φ' assume "φ' ∈ sem C (Set.filter (b ∘ snd) S)"
      then obtain φ where "φ ∈ S" "fst φ = fst φ'" "single_sem C (snd φ) (snd φ')" "b (snd φ)"
        by (auto simp add: in_sem)
      then have "b (snd φ')"
        using assms(2) single_sem_not_free_vars by blast
      then show "φ' ∈ ?B"
        using ‹⟨C, snd φ⟩ → snd φ'› ‹φ ∈ S› ‹fst φ = fst φ'› [symmetric]
        by (auto simp add: in_sem intro: exI [of _ ‹snd φ›])
    qed
  qed
  ultimately show "(Q ∘ Set.filter (b ∘ snd)) (sem C S)"
    by auto
qed




subsection ‹Other Compositionality Rules›

proposition rule_False:
  "hyper_hoare_triple (λ_. False) C Q"
  by (simp add: hyper_hoare_triple_def)

proposition rule_True:
  "hyper_hoare_triple P C (λ_. True)"
  by (simp add: hyper_hoare_triple_def)


(* Other direction does not hold! *)
lemma sem_inter:
  "sem C (S1 ∩ S2) ⊆ sem C S1 ∩ sem C S2"
  by (simp add: sem_monotonic)


proposition rule_Union:
  assumes "⊨ {P} C {Q}"
      and "hyper_hoare_triple P' C Q'"
    shows "hyper_hoare_triple (join P P') C (join Q Q')"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "join P P' S"
  then obtain S1 S2 where "S = S1 ∪ S2" "P S1" "P' S2"
    by (metis join_def)
  then have "sem C S = sem C S1 ∪ sem C S2"
    using sem_union by auto
  then show "join Q Q' (sem C S)"
    by (metis ‹P S1› ‹P' S2› assms(1) assms(2) hyper_hoare_tripleE join_def)
qed

proposition rule_IndexedUnion:
  assumes "⋀x. ⊨ {P x} C {Q x}"
  shows "hyper_hoare_triple (general_join P) C (general_join Q)"
proof (rule hyper_hoare_tripleI)
  fix S assume "general_join P S"
  then obtain F where asm0: "S = (⋃x. F x)" "⋀x. P x (F x)"
    by (meson general_join_def)
  have "sem C S = (⋃x. sem C (F x))"
    by (simp add: asm0(1) sem_split_general)
  moreover have "⋀x. Q x (sem C (F x))"
    using asm0(2) assms hyper_hoare_tripleE by blast
  ultimately show "general_join Q (sem C S)"
    by (metis general_join_def)
qed

proposition rule_And:
  assumes "⊨ {P} C {Q}"
      and "hyper_hoare_triple P' C Q'"
    shows "hyper_hoare_triple (conj P P') C (conj Q Q')"
proof (rule hyper_hoare_tripleI)
  fix S assume "Logic.conj P P' S"
  then show "Logic.conj Q Q' (sem C S)"
    by (metis assms(1) assms(2) conj_def hyper_hoare_tripleE)
qed

lemma rule_Forall:
  assumes "⋀x. ⊨ {P x} C {Q x}"
  shows "hyper_hoare_triple (forall P) C (forall Q)"
  by (metis assms forall_def hyper_hoare_triple_def)

lemma rule_Or:
  assumes "⊨ {P} C {Q}"
      and "⊨ {P'} C {Q'}"
    shows "hyper_hoare_triple (disj P P') C (disj Q Q')"
  by (metis assms(1) assms(2) disj_def hyper_hoare_triple_def)

corollary variant_if_rule:
  assumes "hyper_hoare_triple P C1 Q"
      and "hyper_hoare_triple P C2 Q"
      and "closed_by_union Q"
    shows "hyper_hoare_triple P (If C1 C2) Q"
  by (metis assms(1) assms(2) assms(3) if_rule join_closed_by_union)


text ‹Simplifying the rule›

definition stable_by_infinite_union :: "'a hyperassertion ⇒ bool" where
  "stable_by_infinite_union I ⟷ (∀F. (∀S ∈ F. I S) ⟶ I (⋃S ∈ F. S))"

lemma stable_by_infinite_unionE:
  assumes "stable_by_infinite_union I"
      and "⋀S. S ∈ F ⟹ I S"
    shows "I (⋃S ∈ F. S)"
  using assms(1) assms(2) stable_by_infinite_union_def by blast

lemma stable_by_union_and_constant_then_I:
  assumes "⋀n. I n = I'"
      and "stable_by_infinite_union I'"
    shows "natural_partition I = I'"
proof (rule ext)
  fix S show "natural_partition I S = I' S"
  proof
    show "I' S ⟹ natural_partition I S"
    proof -
      assume "I' S"
      show "natural_partition I S"
      proof (rule natural_partitionI)
        show "S = ⋃ (range (λn. S))"
          by simp
        fix n show "I n S"
          by (simp add: ‹I' S› assms(1))
      qed
    qed
    assume asm0: "natural_partition I S"
    then obtain F where "S = (⋃n. F n)" "⋀n. I n (F n)"
      using natural_partitionE by blast
    let ?F = "{F n |n. True}"
    have "I' (⋃S∈?F. S)"
      using assms(2)
    proof (rule stable_by_infinite_unionE[of I'])
      fix S assume "S ∈ {F n |n. True}"
      then show "I' S"
        using ‹⋀n. I n (F n)› assms(1) by force
    qed
    moreover have "(⋃S∈?F. S) = S"
      using ‹S = (⋃n. F n)› by auto
    ultimately show "I' S" by blast
  qed
qed

corollary simpler_rule_while:
  assumes "hyper_hoare_triple I C I"
    and "stable_by_infinite_union I"
  shows "hyper_hoare_triple I (While C) I"
proof -
  let ?I = "λn. I"
  have "hyper_hoare_triple (?I 0) (While C) (natural_partition ?I)"
    using while_rule[of ?I C]
    by (simp add: assms(1) assms(2) stable_by_union_and_constant_then_I)
  then show ?thesis
    by (simp add: assms(2) stable_by_union_and_constant_then_I)
qed


lemma rule_and3:
  assumes "⊨ {P1} C {Q1}"
      and "⊨ {P2} C {Q2}"
      and "⊨ {P3} C {Q3}"
    shows "⊨ { conj P1 (conj P2 P3) } C { conj Q1 (conj Q2 Q3) }"
  by (simp add: assms(1) assms(2) assms(3) rule_And)

definition not_empty where
  "not_empty S ⟷ S ≠ {}"

definition finite_not_empty where
  "finite_not_empty S ⟷ S ≠ {} ∧ finite S"

definition update_logical where
  "update_logical ω i v = ((fst ω)(i := v), snd ω)"


lemma single_sem_prop:
  assumes "single_sem C (snd ω) (snd ω')"
      and "fst ω = fst ω'"
  shows "⊨ { (λS. ω ∈ S) } C { (λS. ω' ∈ S) }"
  by (metis assms(1) assms(2) hyper_hoare_tripleI in_sem prod.collapse)

lemma weaker_linking_rule:
  assumes "⋀l σ σ'. ⊨ { (λS. (l, σ) ∈ S) } C { (λS. (l, σ') ∈ S) } ⟹ ( ⊨ { P (l, σ) } C { Q (l, σ') } )"
  shows "⊨ { (λS. ∀ω ∈ S. P ω S) } C { (λS. ∀ω' ∈ S. Q ω' S) }"
  by (simp add: assms rule_linking_alt single_sem_prop)


definition general_union :: "'a hyperassertion ⇒ 'a hyperassertion" where
  "general_union P S ⟷ (∃F. S = Union F ∧ (∀S' ∈ F. P S'))"

lemma general_unionI:
  assumes "S = Union F"
      and "⋀S'. S' ∈ F ⟹ P S'"
    shows "general_union P S"
  using assms(1) assms(2) general_union_def by blast

lemma general_unionE:
  assumes "general_union P S"
  obtains F where "S = Union F" "⋀S'. S' ∈ F ⟹ P S'"
  by (metis assms general_union_def)


(* Derived *)
proposition rule_BigUnion:
  fixes P :: "((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool)"
  assumes "⊨ {P} C {Q}"
  shows "⊨ {general_union P} C {general_union Q}"
proof (rule consequence_rule)
  define PP :: "(('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ (('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool" where
  "PP = (λ_. P)"
  let ?P = "disj (general_join PP) (λS. S = {})"
  show "entails (general_union P) ?P"
  proof (rule entailsI)
    fix S assume "general_union P S"
    then obtain F where "S = Union F" "⋀S'. S' ∈ F ⟹ P S'"
      by (metis general_union_def)
    have "general_join PP S ∨ S = {}"
    proof (cases "S = {}")
      case True
      then show ?thesis
        by simp
    next
      case False
      then obtain S' where "S' ∈ F"
        using ‹S = ⋃ F› by blast
      let ?F = "λSS. if SS ∈ F then SS else S'"
      have "general_join PP S"
      proof (rule general_joinI)
        fix x show "PP x (?F x)"
          by (simp add: PP_def ‹S' ∈ F› ‹⋀S'. S' ∈ F ⟹ P S'›)
      next
        show "S = (⋃x. if x ∈ F then x else S')"
          using ‹S = ⋃ F› ‹S' ∈ F› by force
      qed
      then show ?thesis by simp
    qed
    then show "disj (general_join PP) (λS. S = {}) S"
      by (simp add: disj_def)
  qed

  define QQ :: "(('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ (('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool" where
  "QQ = (λ_. Q)"
  let ?Q = "disj (general_join QQ) (λS. S = {})"

  show "⊨ {Logic.disj (general_join PP) (λS. S = {})} C {?Q}"
  proof (rule rule_Or)
    show "⊨ {(λS. S = {})} C {λS. S = {}}"
      by (metis (mono_tags, lifting) empty_iff equals0I hyper_hoare_triple_def in_sem)
        (* TODO: Prove this rule *)
    show "⊨ {general_join PP} C {general_join QQ}"
    proof (rule rule_IndexedUnion)
      fix x show "⊨ {PP x} C {QQ x}"
        by (simp add: PP_def QQ_def assms)
    qed
  qed
  show "entails (Logic.disj (general_join QQ) (λS. S = {})) (general_union Q)"
  proof (rule entailsI)
    fix S assume "Logic.disj (general_join QQ) (λS. S = {}) S"
    then show "general_union Q S"
    proof (cases "S = {}")
      case True
      then show ?thesis
        using general_union_def by auto
    next
      case False
      then obtain F where "⋀x. QQ x (F x)" "S = ⋃ (range F)"
        by (metis (mono_tags, lifting) ‹Logic.disj (general_join QQ) (λS. S = {}) S› disj_def general_join_def)
      then show ?thesis
        by (metis QQ_def general_unionI rangeE)
    qed
  qed
qed



proposition rule_Empty:
  "⊨ { (λS. S = {}) } C { (λS. S = {}) }"
proof (rule consequence_rule)
  let ?P = "general_union (λ_. False)"
  show "entails (λS. S = {}) ?P"
    by (metis (full_types) Union_empty empty_iff entailsI general_unionI)
  show "entails ?P (λS. S = {})"
    using entailsI[of ?P "λS. S = {}"] general_union_def Sup_bot_conv(2) by metis
  show "⊨ {general_union (λ_. False)} C {general_union (λ_. False)}"
  proof (rule rule_BigUnion)
    show "⊨ {(λ_. False)} C {λ_. False}"
      using rule_False by auto
  qed
qed

definition has_subset where
  "has_subset P S ⟷ (∃S'. S' ⊆ S ∧ P S')"

lemma has_subset_join_same:
  "entails (has_subset P) (join P (λ_. True))"
  "entails (join P (λ_. True)) (has_subset P)"
  using entailsI[of "has_subset P" "join P (λ_. True)"] has_subset_def join_def sup.absorb_iff2
   apply metis
  using UnCI entails_def[of "join P (λ_. True)" "has_subset P"] has_subset_def join_def subset_eq
  by metis


(* derived from join *)
proposition rule_AtLeast:
  assumes "⊨ {P} C {Q}"
  shows "⊨ {has_subset P} C {has_subset Q}"
proof (rule consequence_rule)
  let ?P = "join P (λ_. True)"
  let ?Q = "join Q (λ_. True)"
  show "⊨ {?P} C {?Q}"
    by (simp add: assms rule_True rule_Union)
qed (auto simp add: has_subset_join_same)

definition has_superset where
  "has_superset P S ⟷ (∃S'. S ⊆ S' ∧ P S')"

proposition rule_AtMost:
  assumes "⊨ {P} C {Q}"
  shows "⊨ {has_superset P} C {has_superset Q}"
proof (rule hyper_hoare_tripleI)
  fix S :: "(('a ⇒ 'b) × ('c ⇒ 'd)) set"
  assume "has_superset P S"
  then obtain S' where "S ⊆ S'" "P S'"
    by (meson has_superset_def)
  then have "Q (sem C S')"
    using assms hyper_hoare_tripleE by blast
  then show "has_superset Q (sem C S)"
    by (meson ‹S ⊆ S'› has_superset_def sem_monotonic)
qed




subsection ‹Synchronous Reasoning (Proposition 14, Appendix H).›

theorem if_sync_rule:
  assumes "⊨ {P} C1 {P1}"
      and "⊨ {P} C2 {P2}"
      and "⊨ {combine from_nat x P1 P2} C {combine from_nat x R1 R2}"
      and "⊨ {R1} C1' {Q1}"
      and "⊨ {R2} C2' {Q2}"

      and "not_free_var_hyper x P1"
      and "not_free_var_hyper x P2"
      and "from_nat 1 ≠ from_nat 2"

      and "not_free_var_hyper x R1"
      and "not_free_var_hyper x R2"

    shows "⊨ {P} If (Seq C1 (Seq C C1')) (Seq C2 (Seq C C2')) {join Q1 Q2}"
proof (rule hyper_hoare_tripleI)
  fix S assume asm0: "P S"
  have r0: "sem (stmt.If (Seq C1 (Seq C C1')) (Seq C2 (Seq C C2'))) S
  = sem C1' (sem C (sem C1 S)) ∪ sem C2' (sem C (sem C2 S))"
    by (simp add: sem_if sem_seq)
  moreover have "P1 (sem C1 S) ∧ P2 (sem C2 S)"
    using asm0 assms(1) assms(2) hyper_hoare_tripleE by blast

  let ?S1 = "(modify_lvar_to x (from_nat 1)) ` (sem C1 S)"
  let ?S2 = "(modify_lvar_to x (from_nat 2)) ` (sem C2 S)"
  let ?f1 = "Set.filter (λφ. fst φ x = from_nat 1)"
  let ?f2 = "Set.filter (λφ. fst φ x = from_nat 2)"

  have "P1 ?S1 ∧ P2 ?S2"
    by (meson ‹P1 (sem C1 S) ∧ P2 (sem C2 S)› assms(6) assms(7) not_free_var_hyper_def)
  moreover have rr1: "Set.filter (λφ. fst φ x = from_nat 1) (?S1 ∪ ?S2) = ?S1"
    using injective_then_ok[of "from_nat 1" "from_nat 2" ?S1 x]
    by (metis (no_types, lifting) assms(8))
  moreover have rr2: "Set.filter (λφ. fst φ x = from_nat 2) (?S1 ∪ ?S2) = ?S2"
    using injective_then_ok[of "from_nat 2" "from_nat 1" ?S2 x]
    by (metis (no_types, lifting) assms(8) sup_commute)
  ultimately have "combine from_nat x P1 P2 (?S1 ∪ ?S2)"
    by (metis combineI)
  then have "combine from_nat x R1 R2 (sem C (?S1 ∪ ?S2))"
    using assms(3) hyper_hoare_tripleE by blast
  moreover have "?f1 (sem C (?S1 ∪ ?S2)) = sem C ?S1"
    using recover_after_sem[of "from_nat 1" "from_nat 2" ?S1 x ?S2] assms(8) rr1 rr2
    by simp blast
  then have "R1 (sem C ?S1)"
    by (metis (mono_tags) calculation combine_def)
  then have "R1 (sem C (sem C1 S))"
    by (metis assms(9) not_free_var_hyper_def sem_of_modify_lvar)
  moreover have "?f2 (sem C (?S1 ∪ ?S2)) = sem C ?S2"
    using recover_after_sem[of "from_nat 2" "from_nat 1" ?S2 x ?S1] assms(8) rr1 rr2
    by (simp add: ac_simps) blast

  then have "R2 (sem C ?S2)"
    by (metis (mono_tags) calculation(1) combine_def)
  then have "R2 (sem C (sem C2 S))"
    by (metis assms(10) not_free_var_hyper_def sem_of_modify_lvar)

  then show "join Q1 Q2 (sem (stmt.If (Seq C1 (Seq C C1')) (Seq C2 (Seq C C2'))) S)"
    by (metis (full_types) r0 assms(4) assms(5) calculation(2) hyper_hoare_tripleE join_def)
qed


definition update_lvar_set where
  "update_lvar_set u e S = { ((fst φ')(u := e φ'), snd φ') |φ'. φ' ∈ S}"

lemma equal_outside_set_helper:
  "equal_outside_set {u} (fst φ) (fst ((fst φ)(u := x), snd φ))"
  by (simp add: equal_outside_set_def)

lemma same_update_lvar_set:
  "same_mod_updates {u} S (update_lvar_set u e S)"
proof (rule same_mod_updatesI)
  show "⋀ω'. ω' ∈ update_lvar_set u e S ⟹ ∃ω∈S. snd ω = snd ω' ∧ equal_outside_set {u} (fst ω') (fst ω)"
  proof -
    fix ω' assume "ω' ∈ update_lvar_set u e S"
    then obtain φ' where "ω' = ((fst φ')(u := e φ'), snd φ')" "φ' ∈ S"
      using mem_Collect_eq update_lvar_set_def[of u e S] by auto
    then show "∃ω∈S. snd ω = snd ω' ∧ equal_outside_set {u} (fst ω') (fst ω)"
      by (meson equal_outside_set_helper equal_outside_sym snd_eqD)
  qed
  show "⋀ω. ω ∈ S ⟹ ∃ω'∈update_lvar_set u e S. snd ω = snd ω' ∧ equal_outside_set {u} (fst ω) (fst ω')"
    by (metis (mono_tags, lifting) equal_outside_set_helper mem_Collect_eq snd_conv update_lvar_set_def)
qed


lemma same_mod_updates_empty:
  assumes "same_mod_updates vars {} S'"
  shows "S' = {}"
  by (meson assms equals0D equals0I same_mod_updates_def subset_mod_updatesE)

definition not_fv_hyper where
  "not_fv_hyper t A ⟷ (∀S S'. same_mod_updates {t} S S' ∧ A S ⟶ A S')"

lemma not_fv_hyperE:
  assumes "not_fv_hyper e I"
      and "same_mod_updates {e} S S'"
      and "I S"
    shows "I S'"
  by (meson assms(1) assms(2) assms(3) not_fv_hyper_def)

definition assign_exp_to_lvar where
  "assign_exp_to_lvar e l φ = ((fst φ)(l := e (snd φ)), snd φ)"

definition assign_exp_to_lvar_set where
  "assign_exp_to_lvar_set e l S = assign_exp_to_lvar e l ` S"

lemma same_outside_set_lvar_assign_exp:
  "snd φ = snd (assign_exp_to_lvar e l φ) ∧ equal_outside_set {l} (fst φ) (fst (assign_exp_to_lvar e l φ))"
  by (simp add: assign_exp_to_lvar_def equal_outside_set_def)


lemma assign_exp_to_lvar_set_same_mod_updates:
  "same_mod_updates {l} S (assign_exp_to_lvar_set e l S)"
proof (rule same_mod_updatesI)
  show "⋀ω. ω ∈ S ⟹ ∃ω'∈assign_exp_to_lvar_set e l S. snd ω = snd ω' ∧ equal_outside_set {l} (fst ω) (fst ω')"
    by (metis assign_exp_to_lvar_set_def rev_image_eqI same_outside_set_lvar_assign_exp)
  show "⋀ω'. ω' ∈ assign_exp_to_lvar_set e l S ⟹ ∃ω∈S. snd ω = snd ω' ∧ equal_outside_set {l} (fst ω') (fst ω)"
    by (metis (mono_tags, opaque_lifting) assign_exp_to_lvar_set_def equal_outside_sym imageE same_outside_set_lvar_assign_exp)
qed


lemma holds_forall_same_mod_updates:
  assumes "same_mod_updates vars S S'"
      and "holds_forall b S"
    shows "holds_forall b S'"
proof (rule holds_forallI)
  fix φ' assume asm0: "φ' ∈ S'"
  then obtain φ where "φ ∈ S" "snd φ = snd φ'"
    by (metis assms(1) same_mod_updates_def subset_mod_updatesE)
  then show "b (snd φ')"
    by (metis assms(2) holds_forall_def)
qed

lemma not_fv_hyper_assign_exp:
  assumes "not_fv_hyper t A"
  shows "A S ⟷ A (assign_exp_to_lvar_set e t S)"
  by (metis assign_exp_to_lvar_set_same_mod_updates assms not_fv_hyper_def same_mod_updates_sym)

lemma holds_forall_same_assign_lvar:
  "holds_forall b S ⟷ holds_forall b (assign_exp_to_lvar_set e l S)" (is "?A ⟷ ?B")
proof
  show "?A ⟹ ?B"
    by (simp add: assign_exp_to_lvar_def assign_exp_to_lvar_set_def holds_forall_def)
  show "?B ⟹ ?A"
    by (simp add: assign_exp_to_lvar_def assign_exp_to_lvar_set_def holds_forall_def)
qed

definition e_recorded_in_t where
  "e_recorded_in_t e t S ⟷ (∀φ∈S. fst φ t = e (snd φ))"

lemma e_recorded_in_tI:
  assumes "⋀φ. φ∈S ⟹ fst φ t = e (snd φ)"
  shows "e_recorded_in_t e t S"
  by (simp add: assms e_recorded_in_t_def)

definition e_smaller_than_t where
  "e_smaller_than_t e t lt S ⟷ (∀φ∈S. lt (e (snd φ)) (fst φ t))"


lemma low_expI:
  assumes "⋀φ φ'. φ ∈ S ∧ φ' ∈ S ⟹ (e (snd φ) = e (snd φ'))"
  shows "low_exp e S"
  using low_exp_def assms by blast

lemma low_exp_forall_same_mod_updates:
  assumes "same_mod_updates vars S S'"
      and "low_exp b S"
    shows "low_exp b S'"
proof (rule low_expI)
  fix φ' φ'' assume asm0: "φ' ∈ S' ∧ φ'' ∈ S'"
  then obtain φ where "φ ∈ S" "snd φ = snd φ'"
    by (metis assms(1) same_mod_updates_def subset_mod_updatesE)
  then show "b (snd φ') = b (snd φ'')"
    using asm0 assms(1) assms(2) low_exp_def[of b S] same_mod_updates_def[of vars S S'] subset_mod_updatesE
    by metis
qed

lemma e_recorded_in_t_if_assigned:
  "e_recorded_in_t e t (assign_exp_to_lvar_set e t S)"
  by (simp add: assign_exp_to_lvar_def assign_exp_to_lvar_set_def e_recorded_in_t_def)

lemma low_exp_commute_assign_lvar:
  "low_exp b (assign_exp_to_lvar_set e t S) ⟷ low_exp b S" (is "?A ⟷ ?B")
proof
  assume ?A
  then show ?B
    by (meson assign_exp_to_lvar_set_same_mod_updates low_exp_forall_same_mod_updates same_mod_updates_sym)
next
  assume ?B
  then show ?A
    by (meson assign_exp_to_lvar_set_same_mod_updates low_exp_forall_same_mod_updates)
qed

end