theory Scratch
  imports
    Main
begin

context includes lifting_syntax begin

lemma Inf_fun_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total T" "bi_unique T"
  shows "(rel_set (T ===> (=)) ===> T ===> (=)) Inf Inf"
  unfolding Inf_fun_def
  by transfer_prover

lemma less_eq_fun_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total T" "bi_unique T"
  shows "((T ===> (=)) ===> (T ===> (=)) ===> (=)) (\<lambda>f g. \<forall>x\<in>Collect(Domainp T). f x \<le> g x) (\<le>)"
  unfolding le_fun_def
  by transfer_prover

lemma lfp_fun_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A" "bi_unique A"
  defines "R \<equiv> (((A ===> (=)) ===> (A ===> (=))) ===> (A ===> (=)))"
  shows "R (\<lambda>f. lfp (\<lambda>u x. if Domainp A x then f u x else bot)) lfp"
proof -
  have "R (\<lambda>f. Inf {u. \<forall>x\<in>Collect (Domainp A). f u x \<le> u x}) lfp"
    unfolding R_def lfp_def
    by transfer_prover
  then show ?thesis
    by (auto simp: le_fun_def lfp_def)
qed

end

end