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: " Φ  MM'   M  bind (ASSERT Φ) (λ_. M')"
      apply (cases Φ) by (auto simp: ibind_strict imonad1)

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

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


    lemma ASSUME_leI: " Φ  MM'   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: " Φ; Φ  MM'   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  Φ)  SS'"
      by (cases Φ) (auto simp: ibind_strict imonad1 simp: top_unique)

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

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

    lemma le_ASSUME_iff:
      "S  bind (ASSUME Φ) (λ_. S')  (Sbot  Φ)  SS'"
      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