Theory Refine_Monadic.RefineG_Assert

section ‹{Assert and Assume}›
theory RefineG_Assert
imports RefineG_Transfer
begin

definition "iASSERT return Φ ≡ if Φ then return () else top"
definition "iASSUME return Φ ≡ if Φ then return () else bot"

  locale generic_Assert =
    fixes bind :: 
      "('mu::complete_lattice) ⇒ (unit ⇒ ('ma::complete_lattice)) ⇒ 'ma"
    fixes return :: "unit ⇒ 'mu"
    fixes ASSERT
    fixes ASSUME
    assumes ibind_strict: 
      "bind bot f = bot" 
      "bind top f = top"
    assumes imonad1: "bind (return u) f = f u"
    assumes ASSERT_eq: "ASSERT ≡ iASSERT return"
    assumes ASSUME_eq: "ASSUME ≡ iASSUME return"
  begin
     lemma ASSERT_simps[simp,code]: 
      "ASSERT True = return ()"
      "ASSERT False = top"
      unfolding ASSERT_eq iASSERT_def by auto

    lemma ASSUME_simps[simp,code]: 
      "ASSUME True = return ()"
      "ASSUME False = bot"
      unfolding ASSUME_eq iASSUME_def by auto

    lemma le_ASSERTI: "⟦ Φ ⟹ M≤M' ⟧ ⟹ M ≤ bind (ASSERT Φ) (λ_. M')"
      apply (cases Φ) by (auto simp: ibind_strict imonad1)

    lemma le_ASSERTI_pres: "⟦ Φ ⟹ M≤bind (ASSERT Φ) (λ_. M') ⟧ 
      ⟹ M ≤ bind (ASSERT Φ) (λ_. M')"
      apply (cases Φ) by (auto simp: ibind_strict imonad1)

    lemma ASSERT_leI: "⟦ Φ; Φ ⟹ M≤M' ⟧ ⟹ bind (ASSERT Φ) (λ_. M) ≤ M'"
      apply (cases Φ) by (auto simp: ibind_strict imonad1)


    lemma ASSUME_leI: "⟦ Φ ⟹ M≤M' ⟧ ⟹ bind (ASSUME Φ) (λ_. M) ≤ M'"
      apply (cases Φ) by (auto simp: ibind_strict imonad1)
    lemma ASSUME_leI_pres: "⟦ Φ ⟹ bind (ASSUME Φ) (λ_. M)≤M' ⟧ 
      ⟹ bind (ASSUME Φ) (λ_. M) ≤ M'"
      apply (cases Φ) by (auto simp: ibind_strict imonad1)
    lemma le_ASSUMEI: "⟦ Φ; Φ ⟹ M≤M' ⟧ ⟹ M ≤ bind (ASSUME Φ) (λ_. M')"
      apply (cases Φ) by (auto simp: ibind_strict imonad1)

    text ‹The order of these declarations does matter!›
    lemmas [intro?] = ASSERT_leI le_ASSUMEI
    lemmas [intro?] = le_ASSERTI ASSUME_leI

    lemma ASSERT_le_iff: 
      "bind (ASSERT Φ) (λ_. S) ≤ S' ⟷ (S'≠top ⟶ Φ) ∧ S≤S'"
      by (cases Φ) (auto simp: ibind_strict imonad1 simp: top_unique)

    lemma ASSUME_le_iff:
      "bind (ASSUME Φ) (λ_. S) ≤ S' ⟷ (Φ ⟶ S≤S')"
      by (cases Φ) (auto simp: ibind_strict imonad1)

    lemma le_ASSERT_iff:
      "S ≤ bind (ASSERT Φ) (λ_. S') ⟷ (Φ ⟶ S≤S')"
      by (cases Φ) (auto simp: ibind_strict imonad1)

    lemma le_ASSUME_iff:
      "S ≤ bind (ASSUME Φ) (λ_. S') ⟷ (S≠bot ⟶ Φ) ∧ S≤S'"
      by (cases Φ) (auto simp: ibind_strict imonad1 simp: bot_unique)
  end

  text ‹
    This locale transfer's asserts and assumes. 
    To remove them, use the next locale.
›
  locale transfer_generic_Assert = 
    c: generic_Assert cbind creturn cASSERT cASSUME +
    a: generic_Assert abind areturn aASSERT aASSUME +
    ordered_transfer α
    for cbind :: "('muc::complete_lattice) 
      ⇒ (unit⇒'mac) ⇒ ('mac::complete_lattice)" 
    and creturn :: "unit ⇒ 'muc" and cASSERT and cASSUME
    and abind :: "('mua::complete_lattice) 
      ⇒ (unit⇒'maa) ⇒ ('maa::complete_lattice)"
    and areturn :: "unit ⇒ 'mua" and aASSERT and aASSUME
    and α :: "'mac ⇒ 'maa"
  begin
    lemma transfer_ASSERT[refine_transfer]:
      "⟦Φ ⟹ α M ≤ M'⟧ 
      ⟹ α (cbind (cASSERT Φ) (λ_. M)) ≤ (abind (aASSERT Φ) (λ_. M'))"
      apply (cases Φ)
      apply (auto simp: c.ibind_strict a.ibind_strict c.imonad1 a.imonad1)
      done

    lemma transfer_ASSUME[refine_transfer]:
      "⟦Φ; Φ ⟹ α M ≤ M'⟧ 
      ⟹ α (cbind (cASSUME Φ) (λ_. M)) ≤ (abind (aASSUME Φ) (λ_. M'))"
      apply (auto simp: c.ibind_strict a.ibind_strict c.imonad1 a.imonad1)
      done

  end


  locale transfer_generic_Assert_remove = 
    a: generic_Assert abind areturn aASSERT aASSUME +
    transfer α
    for abind :: "('mua::complete_lattice) 
      ⇒ (unit⇒'maa) ⇒ ('maa::complete_lattice)"
    and areturn :: "unit ⇒ 'mua" and aASSERT and aASSUME
    and α :: "'mac ⇒ 'maa"
  begin
    lemma transfer_ASSERT_remove[refine_transfer]: 
      "⟦ Φ ⟹ α M ≤ M' ⟧ ⟹ α M ≤ abind (aASSERT Φ) (λ_. M')"
      by (rule a.le_ASSERTI)

    lemma transfer_ASSUME_remove[refine_transfer]: 
      "⟦ Φ; Φ ⟹ α M ≤ M' ⟧ ⟹ α M ≤ abind (aASSUME Φ) (λ_. M')"
      by (rule a.le_ASSUMEI)
  end

end