Theory ML_Unification.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