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)"

open_bundle SIMPS_TO_syntax
begin
notation SIMPS_TO ("_ ≡> _" [50,50] 50)
end

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

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

lemma SIMPS_TOI: "s ≡> s" unfolding SIMPS_TO_eq by simp
lemma SIMPS_TOD: "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)"

open_bundle SIMPS_TO_UNIF_syntax
begin
notation SIMPS_TO_UNIF ("_ ≡⇧?> _" [50,50] 50)
end

text ‹Prevent simplification›
lemma SIMPS_TO_UNIF_cong [cong]: "s ≡⇧?>t ≡ s ≡⇧?> t" by simp

lemma SIMPS_TO_UNIF_eq: "s ≡⇧?> t ≡ (s ≡ t)" unfolding SIMPS_TO_UNIF_def by simp

lemma SIMPS_TO_UNIFI: "s ≡> s' ⟹ s' ≡ t ⟹ s ≡⇧?> t"
  unfolding SIMPS_TO_UNIF_eq SIMPS_TO_eq by simp
lemma SIMPS_TO_UNIFD: "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 "P ≡⇧?> ?A"
  apply (tactic ‹HEADGOAL (Simps_To_Unif.SIMPS_TO_UNIF_tac (simp_tac @{context})
    (K all_tac) 1 @{context})›)
  by (rule reflexive)

end

end