Theory ExamplesCompositionality

section ‹Examples›

text ‹In this file, we prove the correctness of the two compositionality
proofs presented in Appendix D.2.›

theory ExamplesCompositionality
  imports Logic Compositionality
begin

definition low where
  "low l S ⟷ (∀φ1 φ2. φ1 ∈ S ∧ φ2 ∈ S ⟶ snd φ1 l = snd φ2 l)"

subsection ‹Examples using the core rules.›

definition GNI where
  "GNI l h S ⟷ (∀φ1 φ2. φ1 ∈ S ∧ φ2 ∈ S
  ⟶ (∃φ ∈ S. snd φ h = snd φ1 h ∧ snd φ l = snd φ2 l))"

lemma GNI_I:
  assumes "⋀φ1 φ2. φ1 ∈ S ∧ φ2 ∈ S
  ⟹ (∃φ ∈ S. snd φ h = snd φ1 h ∧ snd φ l = snd φ2 l)"
  shows "GNI l h S"
  by (simp add: GNI_def assms)

subsection ‹Examples using the compositionality rules›



definition has_minimum :: "'c ⇒ ('d ⇒ 'd ⇒ bool) ⇒ ('a, 'b, 'c, 'd) chyperassertion" where
  "has_minimum x leq S ⟷ (∃ω∈S. ∀ω'∈S. leq (snd ω x) (snd ω' x))"

lemma has_minimumI:
  assumes "ω ∈ S"
      and "⋀ω'. ω' ∈ S ⟹ leq (snd ω x) (snd ω' x)"
    shows "has_minimum x leq S"
  by (metis assms(1) assms(2) has_minimum_def)

definition is_monotonic where
  "is_monotonic i x one two leq S ⟷ (∀ω∈S. ∀ω'∈S. fst ω i = one ∧ fst ω' i = two ⟶ leq (snd ω x) (snd ω' x))"

lemma is_monotonicI:
  assumes "⋀ω ω'. ω ∈ S ⟹ ω' ∈ S ⟹ fst ω i = one ∧ fst ω' i = two ⟹ leq (snd ω x) (snd ω' x)"
  shows "is_monotonic i x one two leq S"
  by (simp add: assms is_monotonic_def)



lemma update_logical_equal_outside:
  "equal_outside_set {i} (snd ω) (snd (update_logical ω i v))"
  by (simp add: equal_outside_set_def update_logical_def)

lemma update_logical_read:
  "fst (update_logical ω i v) i = v"
  by (simp add: update_logical_def)

lemma snd_update_logical_same:
  "snd (update_logical ω i v) = snd ω"
  by (simp add: update_logical_def)

text ‹Figure 12›
proposition composing_monotonicity_and_minimum:
  fixes P :: "((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool)"
  fixes i :: 'a
  fixes x :: 'c
  fixes y :: 'c
  fixes leq :: "'d ⇒ 'd ⇒ bool"
  fixes one :: 'b
  fixes two :: 'b

  assumes "⊨ { P } C1 { has_minimum x leq }"
      and "⊨ { is_monotonic i x one two leq } C2 { is_monotonic i y one two leq }"
      and "⊨ { (is_singleton :: ((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool)) } C2 { is_singleton }"
      and "one ≠ two"

      and "⋀x. leq x x" ―‹reflexivity›

    shows "⊨ { P } C1 ;; C2 { has_minimum y leq }"
  using assms(1)
proof (rule seq_rule)

  let ?P1 = "is_singleton ∘ (Set.filter (λω. fst ω i = one))"
  let ?P2 = "is_monotonic i x one two leq"
  let ?P3 = "λS. ∀ω∈S. fst ω i = one ∨ fst ω i = two"

  let ?P = "conj ?P1 (conj ?P2 ?P3)"

  let ?Q1 = "is_singleton ∘ (Set.filter (λω. fst ω i = one))"
  let ?Q2 = "is_monotonic i y one two leq"
  let ?Q3 = "λS. ∀ω∈S. fst ω i = one ∨ fst ω i = two"

  let ?Q = "conj ?Q1 (conj ?Q2 ?Q3)"


  show "⊨ { (has_minimum x leq :: ((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool)) } C2 { has_minimum y leq }"
  proof (rule rule_LUpdate)

    show "entails_with_updates {i} (has_minimum x leq) ?P"
    proof (rule entails_with_updatesI)
      fix S :: "(('a ⇒ 'b) × ('c ⇒ 'd)) set"
      assume asm0: "has_minimum x leq S"
      then obtain ω where minimum: "ω ∈ S" "⋀ω'. ω' ∈ S ⟹ leq (snd ω x) (snd ω' x)"
        by (metis has_minimum_def)
      let ?ω = "update_logical ω i one"
      let ?S = "{ update_logical ω' i two |ω'. ω' ∈ S } ∪ {?ω}"
      have "same_mod_updates {i} S ?S"
      proof (rule same_mod_updatesI)
        fix ω' assume asm1: "ω' ∈ S"
        then have "update_logical ω' i two ∈ ?S"
          by blast
        moreover have "snd ω' = snd (update_logical ω' i two) ∧ equal_outside_set {i} (fst ω') (fst (update_logical ω' i two))"
          by (metis equal_outside_setI fst_eqD fun_upd_other singletonI snd_update_logical_same update_logical_def)
        ultimately show "∃ω''∈?S. snd ω' = snd ω'' ∧ equal_outside_set {i} (fst ω') (fst ω'')"
          by blast
      next
        fix ω'
        assume asm1: "ω' ∈ {update_logical ω' i two |ω'. ω' ∈ S} ∪ {update_logical ω i one}"
        show "∃ω∈S. snd ω = snd ω' ∧ equal_outside_set {i} (fst ω') (fst ω)"
        proof (cases "ω' ∈ {update_logical ω' i two |ω'. ω' ∈ S}")
          case True
          then obtain ω'' where "ω' = update_logical ω'' i two" "ω'' ∈ S"
            by blast
          then show ?thesis
            by (metis (mono_tags, lifting) equal_outside_set_def fst_conv fun_upd_other insertCI snd_update_logical_same update_logical_def)
        next
          case False
          then show ?thesis
            by (metis (mono_tags, lifting) UnE asm1 equal_outside_setI fst_eqD fun_upd_other minimum(1) singletonD singletonI snd_update_logical_same update_logical_def)
        qed
      qed
      moreover have "is_singleton (Set.filter (λω. fst ω i = one) ?S)"
      proof -
        have "Set.filter (λω. fst ω i = one) ?S ⊆ {?ω}"
        proof
          fix ω assume "ω ∈ Set.filter (λω. fst ω i = one) ?S"
          then have "ω ∈ ?S ∧ fst ω i = one"
            by simp
          then show "ω ∈ {?ω}"
            using assms(4) update_logical_read by force
        qed
        moreover have "{?ω} ⊆ Set.filter (λω. fst ω i = one) ?S"
          by (simp add: update_logical_read)
        ultimately show ?thesis
          by (simp add: is_singleton_def order_antisym_conv)
      qed
      moreover have "is_monotonic i x one two leq ?S"
      proof (rule is_monotonicI)
        fix ω' ω'' assume asm1: "ω' ∈ ?S" "ω'' ∈ ?S" "fst ω' i = one ∧ fst ω'' i = two"
        then have " ω' ∈ {update_logical ω i one} ∧ ω'' ∈ {update_logical ω' i two |ω'. ω' ∈ S}"
          using assms(4) update_logical_read by fastforce
        then show "leq (snd ω' x) (snd ω'' x)"
          by (metis (no_types, lifting) asm1(2) calculation(1) minimum(2) same_mod_updates_def singletonD snd_update_logical_same subset_mod_updatesE)
      qed
      moreover have "⋀ω'. ω' ∈ ?S ⟹ fst ω' i = one ∨ fst ω' i = two"
        using update_logical_read by fastforce
      ultimately have "same_mod_updates {i} S ?S ∧ ?P ?S"
        using comp_eq_dest_lhs[of is_singleton "Set.filter (λω. fst ω i = one)"] conj_def[of ?P1 "conj ?P2 ?P3"] conj_def[of ?P2 ?P3]
        by simp
      then show "∃S'. same_mod_updates {i} S S' ∧ ?P S'"
        by blast
    qed

    show "invariant_on_updates {i} (has_minimum y leq :: ((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool))"
    proof (rule invariant_on_updatesI)
      fix S :: "(('a ⇒ 'b) × ('c ⇒ 'd)) set"
      fix S'
      assume asm0: "same_mod_updates {i} S S'" "has_minimum y leq S"
      then show "has_minimum y leq S'"
        using has_minimum_def[of y leq S'] has_minimum_def[of y leq S] same_mod_updates_def[of "{i}" S S'] subset_mod_updatesE[of "{i}"]
          by metis
    qed

    show "⊨ { ?P } C2 { has_minimum y leq }"
    proof (rule consequence_rule)
      show "entails ?Q (has_minimum y leq)"
      proof (rule entailsI)
        fix S :: "(('a ⇒ 'b) × ('c ⇒ 'd)) set"
        assume "?Q S"
        then obtain asm0: "is_singleton (Set.filter (λω. fst ω i = one) S)" "is_monotonic i y one two leq S"
          "⋀ω'. ω' ∈ S ⟹ fst ω' i = one ∨ fst ω' i = two"
          by (simp add: conj_def)
        then obtain ω where "Set.filter (λω. fst ω i = one) S = {ω}"
          by (metis is_singleton_def)
        then have "ω ∈ S" by auto
        then show "has_minimum y leq S"
        proof (rule has_minimumI)
          fix ω'
          assume asm1: "ω' ∈ S"
          show "leq (snd ω y) (snd ω' y)"
          proof (cases "fst ω' i = one")
            case True
            then show ?thesis
              using ‹Set.filter (λω. fst ω i = one) S = {ω}› asm1 assms(5) by fastforce
          next
            case False
            then have "fst ω' i = two"
              using asm0(3) asm1 by blast
            then show ?thesis
              using ‹Set.filter (λω. fst ω i = one) S = {ω}› asm0(2) asm1 is_monotonic_def[of i y one two leq S] member_filter singleton_iff
              by force
          qed
        qed
      qed
      show "⊨ { ?P } C2 { ?Q }"
      proof (rule rule_and3)
        show " ⊨ {is_singleton ∘ Set.filter (λω. fst ω i = one)} C2 {is_singleton ∘ Set.filter (λω. fst ω i = one)}"
        proof (rule rule_apply)
          show "⊨ { (is_singleton :: ((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool)) } C2 {is_singleton}"
            using assms(3) by blast
          show "commute_with_sem (Set.filter (λω. fst ω i = one))"
            by (simp add: filter_prop_commute)
        qed
        show "⊨ {is_monotonic i x one two leq} C2 {is_monotonic i y one two leq}"
          by (simp add: assms(2))
  
        show "⊨ {(λS. ∀ω∈S. fst ω i = one ∨ fst ω i = two)} C2 {λS. ∀ω∈S. fst ω i = one ∨ fst ω i = two}"
          using rule_lframe_single by fast
      qed
    qed (auto simp add: entails_refl)
  qed
qed

text ‹In this definition, we use a logical variable for h, which records the initial value of the program variable h›

definition lGNI :: "'pvar ⇒ 'lvar ⇒ (('lvar, 'lval, 'pvar, 'pval) state) set ⇒ bool" where
  "lGNI l h S ⟷ (∀φ1 ∈ S. (∀φ2 ∈ S. ∃φ ∈ S. fst φ h = fst φ1 h ∧ snd φ l = snd φ2 l))"

text ‹Figure 13›
proposition composing_GNI_with_SNI:
  fixes h :: 'lvar
  fixes l :: 'pvar

  assumes "⊨ { (low l :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C2 { low l }"
      and "⊨ { (not_empty :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C2 { not_empty }"
      and "⊨ { (low l :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C1 { lGNI l h }"
    shows "⊨ { (low l :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C1;; C2 { lGNI l h }"
  using assms(3)
proof (rule seq_rule)
  show "⊨ { (lGNI l h :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion)} C2 {lGNI l h}"
    unfolding lGNI_def
  proof (rule rule_linking)
    fix φ1 φ1' :: "('lvar, 'lval, 'pvar, 'pval) state"
    assume asm0: "fst φ1 = fst φ1' ∧ ⊨ { (in_set φ1 :: ('lvar, 'lval, 'pvar, 'pval) state hyperassertion)} C2 {in_set φ1'}"
    show "⊨ {(λS. ∀φ2∈S. ∃φ∈S. fst φ h = fst φ1 h ∧ snd φ l = snd φ2 l)} C2 {λS. ∀φ2∈S. ∃φ∈S. fst φ h = fst φ1' h ∧ snd φ l = snd φ2 l}"
    proof (rule consequence_rule)
      let ?ex = "λS. ∃φ ∈ S. fst φ h = fst φ1 h"
      let ?P = "general_union (conj (low l) ?ex)"
      show "⊨ { (?P :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C2 {?P}"
      proof (rule rule_BigUnion; rule rule_And)
        show "⊨ {(low l :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion)} C2 {low l}"
          using assms(1) by blast
        show "⊨ { ?ex } C2 { ?ex }"
        proof (rule consequence_rule)
          let ?b = "λφ0. φ0 h = fst φ1 h"  
          show "⊨ {not_empty ∘ Set.filter (?b ∘ fst)} C2 { not_empty ∘ Set.filter (?b ∘ fst)}"
            using assms(2) rule_LFilter by auto
          show "entails (λS. ∃φ∈S. fst φ h = fst φ1 h) (not_empty ∘ Set.filter ((λφ0. φ0 h = fst φ1 h) ∘ fst))"
            using CollectI Set.filter_def comp_apply empty_iff not_empty_def
              entailsI[of "(λS. ∃φ∈S. fst φ h = fst φ1 h)" "(not_empty ∘ Set.filter ((λφ0. φ0 h = fst φ1 h) ∘ fst))"]
            by fastforce
          show "entails (not_empty ∘ Set.filter ((λφ0. φ0 h = fst φ1 h) ∘ fst)) (λS. ∃φ∈S. fst φ h = fst φ1 h)"
          proof (rule entailsI)
            fix S assume "(not_empty ∘ Set.filter ((λφ0. φ0 h = fst φ1 h) ∘ fst)) S"
            then obtain φ where "φ ∈ Set.filter ((λφ0. φ0 h = fst φ1 h) ∘ fst) S"
              by (metis comp_apply equals0I not_empty_def)
            then show "∃φ∈S. fst φ h = fst φ1 h"
              by auto
          qed
        qed
      qed
      show "entails (λS. ∀φ2∈S. ∃φ∈S. fst φ h = fst φ1 h ∧ snd φ l = snd φ2 l) ?P"
      proof (rule entailsI)
        fix S assume asm0: "∀φ2∈S. ∃φ∈S. fst φ h = fst φ1 h ∧ snd φ l = snd φ2 l"
        thm general_unionI
        let ?F = "{ {φ, φ2} |φ φ2. φ ∈ S ∧ φ2 ∈ S ∧ snd φ l = snd φ2 l ∧ fst φ h = fst φ1 h }"
        show "general_union (Logic.conj (low l) (λS. ∃φ∈S. fst φ h = fst φ1 h)) S"
        proof (rule general_unionI)
          show "S = ⋃ ?F"
          proof
            show "S ⊆ ⋃ ?F"
            proof
              fix φ2 assume "φ2 ∈ S"
              then obtain φ where "φ∈S" "fst φ h = fst φ1 h ∧ snd φ l = snd φ2 l"
                using asm0 by blast
              then have "{φ, φ2} ∈ ?F"
                using ‹φ2 ∈ S› by blast
              then show "φ2 ∈ ⋃ ?F" by blast
            qed
            show "⋃ ?F ⊆ S" by blast
          qed
          fix S' assume asm1: "S' ∈ {{φ, φ2} |φ φ2. φ ∈ S ∧ φ2 ∈ S ∧ snd φ l = snd φ2 l ∧ fst φ h = fst φ1 h}"
          then obtain φ φ2 where "S' = {φ, φ2}" "φ ∈ S ∧ φ2 ∈ S ∧ snd φ l = snd φ2 l ∧ fst φ h = fst φ1 h"
            by blast
          then show "Logic.conj (low l) (λS. ∃φ∈S. fst φ h = fst φ1 h) S'"
            using conj_def[of "low l" "λS. ∃φ∈S. fst φ h = fst φ1 h"] insert_iff low_def singletonD
            by fastforce
        qed
      qed
      show "entails ?P (λS. ∀φ2∈S. ∃φ∈S. fst φ h = fst φ1' h ∧ snd φ l = snd φ2 l)"
      proof (rule entailsI)
        fix S assume "general_union (Logic.conj (low l) (λS. ∃φ∈S. fst φ h = fst φ1 h)) S"
        then obtain F where "S = ⋃ F" "⋀S'. S' ∈ F ⟹ low l S' ∧ (∃φ∈S'. fst φ h = fst φ1 h)"
          using conj_def[of "low l" "λS. ∃φ∈S. fst φ h = fst φ1 h"]
            general_unionE[of "Logic.conj (low l) (λS. ∃φ∈S. fst φ h = fst φ1 h)" S]
          by (metis (mono_tags, lifting))
        then show "∀φ2∈S. ∃φ∈S. fst φ h = fst φ1' h ∧ snd φ l = snd φ2 l"
          by (metis (mono_tags, lifting) Union_iff asm0 low_def)
      qed
    qed
  qed
qed


subsection ‹Other examples›

lemma program_1_sat_gni:
  assumes "y ≠ l ∧ y ≠ h ∧ l ≠ h"
  shows "⊢ { low l } Seq (Havoc y) (Assign l (λσ. (σ h :: int) + σ y)) { GNI l h }"
proof (rule RuleSeq)
  let ?R = "λS. ∀φ1 φ2. φ1 ∈ S ∧ φ2 ∈ S
  ⟶ (∃φ ∈ S. (snd φ h :: int) = snd φ1 h ∧ snd φ h + snd φ y = snd φ2 h + snd φ2 y )"

  show "⊢ { low l } Havoc y {?R}"
  proof (rule RuleCons)
    show "⊢ {(λS. ?R {(l, σ(y := v)) |l σ v. (l, σ) ∈ S})} Havoc y {?R}"
      using RuleHavoc[of ?R] by blast
    show "entails (low l) (λS. ?R {(l, σ(y := v)) |l σ (v :: int). (l, σ) ∈ S})"
    proof (rule entailsI)
      fix S
      show "?R {(l, σ(y := v)) |l σ (v :: int). (l, σ) ∈ S}"
      proof (clarify)
        fix a b aa ba l la σ σ' v va
        assume asm0: "(l, σ) ∈ S" "(la, σ') ∈ S"
        let ?v = "(σ'(y := va)) h + (σ'(y := va)) y + - σ h"
        let ?φ = "(l, σ(y := ?v))"
        have "snd ?φ h = snd (l, σ(y := v)) h ∧ snd ?φ h + snd ?φ y = snd (la, σ'(y := va)) h + snd (la, σ'(y := va)) y"
          using assms by force
        then show "∃φ∈{(l, σ(y := v)) |l σ v. (l, σ) ∈ S}.
          snd φ h = snd (l, σ(y := v)) h ∧ snd φ h + snd φ y = snd (la, σ'(y := va)) h + snd (la, σ'(y := va)) y"
          using asm0(1) by blast
      qed
    qed
    show "entails ?R ?R"
      by (meson entailsI)
  qed
  show "⊢ {?R} (Assign l (λσ. σ h + σ y)) {GNI l h}"
  proof (rule RuleCons)
    show "⊢ {(λS. GNI l h {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S})} Assign l (λσ. σ h + σ y) {GNI l h}"
      using RuleAssign[of "GNI l h" l "λσ. σ h + σ y"] by blast
    show "entails (GNI l h) (GNI l h)"
      by (simp add: entails_def)
    show "entails ?R (λS. GNI l h {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S})"
    proof (rule entailsI)
      fix S
      assume asm0: "∀φ1 φ2. φ1 ∈ S ∧ φ2 ∈ S ⟶ (∃φ∈S. snd φ h = snd φ1 h ∧ snd φ h + snd φ y = snd φ2 h + snd φ2 y)"
      show "GNI l h {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}"
      proof (rule GNI_I)
        fix φ1 φ2
        assume asm1: "φ1 ∈ {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S} ∧ φ2 ∈ {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}"
        then obtain la σ la' σ' where "(la, σ) ∈ S" "(la', σ') ∈ S" "φ1 = (la, σ(l := σ h + σ y))" "φ2 = (la', σ'(l := σ' h + σ' y))" 
          by blast
        then obtain φ where "φ∈S" "snd φ h = σ h" "snd φ h + snd φ y = σ' h + σ' y"
          using asm0 snd_conv by force
        let ?φ = "(fst φ, (snd φ)(l := snd φ h + snd φ y))"
        have "snd ?φ h = snd φ1 h ∧ snd ?φ l = snd φ2 l"
          using ‹φ1 = (la, σ(l := σ h + σ y))› ‹φ2 = (la', σ'(l := σ' h + σ' y))›
            ‹snd φ h + snd φ y = σ' h + σ' y› ‹snd φ h = σ h› assms by force
        then show "∃φ∈{(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}. snd φ h = snd φ1 h ∧ snd φ l = snd φ2 l"
          using ‹φ ∈ S› mem_Collect_eq[of ?φ]
          by (metis (mono_tags, lifting) prod.collapse)
      qed
    qed
  qed
qed


lemma program_2_violates_gni:
  assumes "y ≠ l ∧ y ≠ h ∧ l ≠ h"
  shows "⊢ { conj (low l) (λS. ∃a ∈ S. ∃b ∈ S. (snd a h :: nat) ≠ snd b h) }
  Seq (Seq (Havoc y) (Assume (λσ. σ y ≥ (0 :: nat) ∧ σ y ≤ (100 :: nat)))) (Assign l (λσ. σ h + σ y))
  {λ(S :: (('lvar ⇒ 'lval) × ('a ⇒ nat)) set). ¬ GNI l h S}"
proof (rule RuleSeq)

  let ?R0 = "λ(S :: (('lvar ⇒ 'lval) × ('a ⇒ nat)) set).
    (∃a ∈ S. ∃b ∈ S. snd b h > snd a h ∧ snd a y ≥ (0 :: nat) ∧ snd a y ≤ 100 ∧ snd b y = 100)"
  let ?R1 = "λ(S :: (('lvar ⇒ 'lval) × ('a ⇒ nat)) set).
    (∃a ∈ S. ∃b ∈ S. snd b h > snd a h ∧ snd b y = 100) ∧ (∀c ∈ S. snd c y ≤ 100)"
  let ?R2 = "λ(S :: (('lvar ⇒ 'lval) × ('a ⇒ nat)) set).
    ∃a ∈ S. ∃b ∈ S. ∀c ∈ S. snd c h = snd a h ⟶ snd c h + snd c y = snd b h + snd b y"

  show "⊢ { conj (low l) (λS. ∃a∈S. ∃b∈S. snd a h ≠ snd b h)} Seq (Havoc y) (Assume (λσ. 0 ≤ σ y ∧ σ y ≤ (100 :: nat))) {?R1}"
  proof (rule RuleSeq)
    show "⊢ {conj (low l) (λS. ∃a∈S. ∃b∈S. snd a h ≠ snd b h)} Havoc y { ?R0 }"
    proof (rule RuleCons)
      show "⊢ {(λS. ?R0 {(l, σ(y := v)) |l σ v. (l, σ) ∈ S})} Havoc y {?R0}"
        using RuleHavoc[of _ y] by fast
      show "entails ?R0 ?R0"
        by (simp add: entailsI)
      show "entails (conj (low l) (λS. ∃a∈S. ∃b∈S. snd a h ≠ snd b h)) (λS. ?R0 {(l, σ(y := v)) |l σ v. (l, σ) ∈ S})"
      proof (rule entailsI)
        fix S :: "(('lvar ⇒ 'lval) × ('a ⇒ nat)) set"
        assume "conj (low l) (λS. ∃a∈S. ∃b∈S. snd a h ≠ snd b h) S"
        then have "∃a∈S. ∃b∈S. snd a h ≠ snd b h" using conj_def[of "low l" "λS. ∃a∈S. ∃b∈S. snd a h ≠ snd b h"]
          by blast
        then obtain a b where "a ∈ S" "b ∈ S" "snd b h > snd a h"
          by (meson linorder_neq_iff)
        let ?a = "(fst a, (snd a)(y := 100))"
        let ?b = "(fst b, (snd b)(y := 100))"
        have "?a ∈ {(l, σ(y := v)) |l σ v. (l, σ) ∈ S} ∧ ?b ∈ {(l, σ(y := v)) |l σ v. (l, σ) ∈ S}"
          using ‹a ∈ S› ‹b ∈ S› by fastforce
        moreover have "snd ?b h > snd ?a h ∧ snd ?a y ≥ (0 :: nat) ∧ snd ?a y ≤ 100 ∧ snd ?b y = 100"
          using ‹snd a h < snd b h› assms by force
        ultimately show "?R0 {(l, σ(y := v)) |l σ v. (l, σ) ∈ S}" by blast
      qed
    qed
    show "⊢ {?R0} Assume (λσ. 0 ≤ σ y ∧ σ y ≤ 100) {?R1}"
    proof (rule RuleCons)
      show "⊢ {(λS. ?R1 (Set.filter ((λσ. 0 ≤ σ y ∧ σ y ≤ 100) ∘ snd)
              S))} Assume (λσ. 0 ≤ σ y ∧ σ y ≤ 100) {?R1}"
        using RuleAssume[of _ "λσ. 0 ≤ σ y ∧ σ y ≤ 100"]
        by fast
      show "entails ?R1 ?R1"
        by (simp add: entailsI)
      show "entails ?R0 (λS. ?R1 (Set.filter ((λσ. 0 ≤ σ y ∧ σ y ≤ 100) ∘ snd) S))"
      proof (rule entailsI)
        fix S :: "(('lvar ⇒ 'lval) × ('a ⇒ nat)) set"
        assume asm0: "?R0 S"
        then obtain a b where "a∈S" "b∈S" "snd a h < snd b h ∧ 0 ≤ snd a y ∧ snd a y ≤ (100 :: nat) ∧ snd b y = 100 "
          by blast
        then have "a ∈ Set.filter ((λσ. 0 ≤ σ y ∧ σ y ≤ 100) ∘ snd) S ∧ b ∈ Set.filter ((λσ. 0 ≤ σ y ∧ σ y ≤ 100) ∘ snd) S"
          by (simp add: ‹a ∈ S› ‹b ∈ S›)
        then show "?R1 (Set.filter ((λσ. 0 ≤ σ y ∧ σ y ≤ 100) ∘ snd) S)"
          using ‹snd a h < snd b h ∧ 0 ≤ snd a y ∧ snd a y ≤ 100 ∧ snd b y = 100› by force
      qed
    qed
  qed
  show "⊢ { ?R1 } Assign l (λσ. σ h + σ y) {λS. ¬ GNI l h S}"
  proof (rule RuleCons)
    show "⊢ {(λS. ¬ GNI l h {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S})} Assign l (λσ. σ h + σ y) {λS. ¬ GNI l h S}"
      using RuleAssign[of "λS. ¬ GNI l h S" l "λσ. σ h + σ y"]
      by blast
    show "entails (λS. ¬ GNI l h S) (λS. ¬ GNI l h S)"
      by (simp add: entails_def)
    show "entails (λS. (∃a∈S. ∃b∈S. snd a h < snd b h ∧ snd b y = 100) ∧ (∀c∈S. snd c y ≤ 100))
        (λ(S :: (('lvar ⇒ 'lval) × ('a ⇒ nat)) set). ¬ GNI l h {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S})"
    proof (rule entailsI)
      fix S :: "(('lvar ⇒ 'lval) × ('a ⇒ nat)) set"
      assume asm0: "(∃a∈S. ∃b∈S. snd a h < snd b h ∧ snd b y = 100) ∧ (∀c∈S. snd c y ≤ 100)"
      then obtain a b where asm1: "a∈S" "b∈S" "snd a h < snd b h ∧ snd b y = 100" by blast
      let ?a = "(fst a, (snd a)(l := snd a h + snd a y))"
      let ?b = "(fst b, (snd b)(l := snd b h + snd b y))"
      have "⋀la σ. (la, σ) ∈ S ⟹ (σ(l := σ h + σ y)) h = snd ?a h ⟹ (σ(l := σ h + σ y)) l ≠ snd ?b l"
        using asm0 asm1(3) assms by fastforce
      moreover have r: "?a ∈ {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S} ∧ ?b ∈ {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}"
        using asm1(1) asm1(2) by fastforce
      show "¬ GNI l h {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}"
      proof (rule ccontr)
        assume "¬ ¬ GNI l h {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}"
        then have "GNI l h {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}"
          by blast
        then obtain φ where "φ ∈ {(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}" "snd φ h = snd ?a h" "snd φ l = snd ?b l"
          using GNI_def[of l h "{(la, σ(l := σ h + σ y)) |la σ. (la, σ) ∈ S}"] r
          by meson
        then show False
          using calculation by auto
      qed
    qed
  qed
qed



end