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