header {* \isaheader{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