Theory DFS_Framework_Misc

theory DFS_Framework_Misc
imports Automatic_Refinement.Misc
begin

(* General *)
lemma tri_caseE:
  "¬P;¬Q  R; P  R; ¬P; Q  R  R"
by auto

(* TODO: How often have we formalized this now? *)
definition "opt_tag x y  x=y"
lemma opt_tagI: "opt_tag x x" unfolding opt_tag_def by simp
lemma opt_tagD: "opt_tag x y  x=y" unfolding opt_tag_def by simp

(* Usage example, to simplify term
  schematic_lemma "term = ?c"
    apply (rule opt_tagD)
    apply simp, unfold, whatever ...
    by (rule opt_tagI)
*)

end