Theory RefineG_Assert

header {* \isaheader {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