Theory Dict_Construction

section ‹Setup›

theory Dict_Construction
imports Automatic_Refinement.Refine_Util
keywords "declassify" :: thy_decl
begin

definition set_of :: "('a ⇒ 'b ⇒ bool) ⇒ ('a × 'b) set" where
"set_of P = {(x, y). P x y}"

lemma wfP_implies_wf_set_of: "wfP P ⟹ wf (set_of P)"
unfolding wfP_def set_of_def .

lemma wf_set_of_implies_wfP: "wf (set_of P) ⟹ wfP P"
unfolding wfP_def set_of_def .

lemma wf_simulate_simple:
  assumes "wf r"
  assumes "⋀x y. (x, y) ∈ r' ⟹ (g x, g y) ∈ r"
  shows "wf r'"
using assms
by (metis in_inv_image wf_eq_minimal wf_inv_image)

lemma set_ofI: "P x y ⟹ (x, y) ∈ set_of P"
unfolding set_of_def by simp

lemma set_ofD: "(x, y) ∈ set_of P ⟹ P x y"
unfolding set_of_def by simp

lemma wfP_simulate_simple:
  assumes "wfP r"
  assumes "⋀x y. r' x y ⟹ r (g x) (g y)"
  shows "wfP r'"
apply (rule wf_set_of_implies_wfP)
apply (rule wf_simulate_simple[where g = g])
apply (rule wfP_implies_wf_set_of)
apply (fact assms)
using assms(2) by (auto intro: set_ofI dest: set_ofD)

lemma wf_implies_dom: "wf (set_of R) ⟹ All (Wellfounded.accp R)"
apply (rule allI)
apply (rule accp_wfPD)
apply (rule wf_set_of_implies_wfP) .

lemma wfP_implies_dom: "wfP R ⟹ All (Wellfounded.accp R)"
by (metis wfP_implies_wf_set_of wf_implies_dom)

named_theorems dict_construction_specs

ML_file ‹dict_construction_util.ML›
ML_file ‹transfer_termination.ML›
ML_file ‹congruences.ML›
ML_file ‹side_conditions.ML›
ML_file ‹class_graph.ML›
ML_file ‹dict_construction.ML›

method_setup fo_cong_rule = ‹
  Attrib.thm >> (fn thm => fn ctxt => SIMPLE_METHOD' (Dict_Construction_Util.fo_cong_tac ctxt thm))
› "resolve congruence rule using first-order matching"

declare [[code drop: "(∧)"]]
lemma [code]: "True ∧ p ⟷ p" "False ∧ p ⟷ False" by auto

declare [[code drop: "(∨)"]]
lemma [code]: "True ∨ p ⟷ True" "False ∨ p ⟷ p" by auto

declare comp_cong[fundef_cong del]
declare fun.map_cong[fundef_cong]

end