Theory Misc_LLang

theory Misc_LLang
imports
  "Automatic_Refinement.Misc"
begin

  (* TODO: Move *)  
  lemma map_le_empty_iff[simp]: "m ⊆⇩m Map.empty ⟷ m=Map.empty"
    using map_le_antisym by fastforce  
    
  (* TODO: Move *)  
  lemma set_minus_minus_disj_conv: "A∩R={} ⟹ A - (B - R) = A - B" by auto

  (* TODO: Move *)  
  lemma ndomIff: "i∉dom m ⟷ m i = None" by auto
  
  lemma nat_minus1_less_if_neZ[simp]: "a - Suc 0 < a ⟷ a≠0" by auto  


end