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  

  
  ML ‹
    fun trace_exn msg e x = e x
      handle exn => (
        if not (Exn.is_interrupt exn) then msg () |> tracing else ();
        Exn.reraise exn
      )
  ›
  
  

end