Theory Automatic_Refinement.Automatic_Refinement

section ‹Entry Point for the Automatic Refinement Tool›
theory Automatic_Refinement
imports 
  "Tool/Autoref_Tool"
  Autoref_Bindings_HOL
begin
  text ‹The automatic refinement tool should be used by 
    importing this theory›

subsection ‹Convenience›

text ‹The following lemmas can be used to add tags to theorems›
lemma PREFER_I: "P x  PREFER P x" by simp
lemma PREFER_D: "PREFER P x  P x" by simp

lemmas PREFER_sv_D = PREFER_D[of single_valued]
lemma PREFER_id_D: "PREFER_id R  R=Id" by simp

abbreviation "PREFER_RUNIV  PREFER (λR. Range R = UNIV)"
lemmas PREFER_RUNIV_D = PREFER_D[of "(λR. Range R = UNIV)"]

lemma SIDE_GEN_ALGO_D: "SIDE_GEN_ALGO P  P" by simp

lemma GEN_OP_D: "GEN_OP c a R  (c,a)R"
  by simp

lemma MINOR_PRIO_TAG_I: "P  (MINOR_PRIO_TAG p  P)" by auto
lemma MAJOR_PRIO_TAG_I: "P  (MAJOR_PRIO_TAG p  P)" by auto
lemma PRIO_TAG_I: "P  (PRIO_TAG ma mi  P)" by auto

end