Theory Simps_To

✐‹creator "Kevin Kappelmann"›
section ‹Simps To›
theory Simps_To
  imports
    ML_Tactic_Utils
    Setup_Result_Commands
begin

paragraph ‹Summary›
text ‹Simple frameworks to ask for the simp-normal form of a term on the user-level.›

setup_result simps_to_base_logger = Logger.new_logger Logger.root "Simps_To_Base"

paragraph ‹Using Simplification On Left Term›

definition "SIMPS_TO s t  (s  t)"

lemma SIMPS_TO_eq: "SIMPS_TO s t  (s  t)"
  unfolding SIMPS_TO_def by simp

text ‹Prevent simplification of second/right argument›
lemma SIMPS_TO_cong [cong]: "s  s'  SIMPS_TO s t  SIMPS_TO s' t" by simp

lemma SIMPS_TOI: "PROP SIMPS_TO s s" unfolding SIMPS_TO_eq by simp
lemma SIMPS_TOD: "PROP SIMPS_TO s t  s  t" unfolding SIMPS_TO_eq by simp

ML_file‹simps_to.ML›


paragraph ‹Using Simplification On Left Term Followed By Unification›

definition "SIMPS_TO_UNIF s t  (s  t)"

text ‹Prevent simplification›
lemma SIMPS_TO_UNIF_cong [cong]: "SIMPS_TO_UNIF s t  SIMPS_TO_UNIF s t" by simp

lemma SIMPS_TO_UNIF_eq: "SIMPS_TO_UNIF s t  (s  t)" unfolding SIMPS_TO_UNIF_def by simp

lemma SIMPS_TO_UNIFI: "PROP SIMPS_TO s s'  s'  t  PROP SIMPS_TO_UNIF s t"
  unfolding SIMPS_TO_UNIF_eq SIMPS_TO_eq by simp
lemma SIMPS_TO_UNIFD: "PROP SIMPS_TO_UNIF s t  s  t"
  unfolding SIMPS_TO_UNIF_eq by simp

ML_file‹simps_to_unif.ML›


paragraph ‹Examples›

experiment
begin
lemma
  assumes [simp]: "P  Q"
  and [simp]: "Q  R"
  shows "PROP SIMPS_TO P Q"
  apply simp ―‹Note: only the left-hand side is simplified.›
  ML_command―‹obtaining the normal form theorem for a term in ML›
    Simps_To.SIMPS_TO_thm_resultsq (simp_tac @{context}) @{context} @{cterm P}
    |> Seq.list_of |> map @{print}
  oops

schematic_goal
  assumes [simp]: "P  Q"
  and [simp]: "Q  R"
  shows "PROP SIMPS_TO P ?Q"
  by (tactic Simps_To.SIMPS_TO_tac (Simps_To.simp_inst_tac (simp_tac @{context})) @{context} 1)

end

end