Theory ML_Unification.Simps_To

✐‹creator "Kevin Kappelmann"›
section ‹Simps To›
theory Simps_To
  imports
    ML_Unifiers_Base
    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

schematic_goal
  assumes [simp]: "P ≡ Q"
  and [simp]: "Q ≡ R"
  shows "PROP SIMPS_TO_UNIF P ?A"
  by (tactic ‹Simps_To_Unif.SIMPS_TO_UNIF_tac (simp_tac @{context})
    (K all_tac) 1 @{context} 1›)

end

end