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