Theory Binary_Relations_Function_Lambda

✐‹creator "Kevin Kappelmann"›
subsection ‹Lambda Abstractions›
theory Binary_Relations_Function_Lambda
  imports Binary_Relations_Clean_Functions
begin

consts rel_lambda :: "'a ⇒ ('b ⇒ 'c) ⇒ 'd"

definition "rel_lambda_pred A f x y ≡ A x ∧ f x = y"
adhoc_overloading rel_lambda rel_lambda_pred

open_bundle rel_lambda_syntax
begin
syntax
  "_rel_lambda"  :: "pttrns ⇒ 'a ⇒ 'b ⇒ 'c" (‹(2λ_ : _./ _)› 60)
end

syntax_consts
  "_rel_lambda" ⇌ rel_lambda
translations
  "λx xs : A. f" ⇀ "CONST rel_lambda A (λx. (λxs : A. f))"
  "λx : A. f" ⇌ "CONST rel_lambda A (λx. f)"

lemma rel_lambdaI [intro]:
  assumes "A x"
  and "f x = y"
  shows "(λx : A. f x) x y"
  using assms unfolding rel_lambda_pred_def by auto

lemma rel_lambda_appI:
  assumes "A x"
  shows "(λx : A. f x) x (f x)"
  using assms by auto

lemma rel_lambdaE [elim!]:
  assumes "(λx : A. f x) x y"
  obtains "A x" "y = f x"
  using assms unfolding rel_lambda_pred_def by auto

lemma rel_lambda_cong [cong]:
  "⟦⋀x. A x ⟷ A' x; ⋀x. A' x ⟹ f x = f' x⟧ ⟹ (λx : A. f x) = λx : A'. f' x"
  by (intro ext) auto

lemma in_dom_rel_lambda_eq [simp]: "in_dom (λx : A. f x) = A"
  by auto

lemma in_codom_rel_lambda_eq_has_inverse_on [simp]: "in_codom (λx : A. f x) = has_inverse_on A f"
  by fastforce

lemma left_total_on_rel_lambda: "left_total_on A (λx : A. f x)"
  by auto

lemma right_unique_on_rel_lambda: "right_unique_on A (λx : A. f x)"
  by auto

lemma crel_dep_mono_wrt_pred_rel_lambda: "((x : A) →⇩c ((=) (f x))) (λx : A. f x)"
  by (intro crel_dep_mono_wrt_predI') auto

text ‹Compare the following with @{thm mono_rel_dep_mono_wrt_pred_dep_mono_wrt_pred_eval}.›

lemma mono_dep_mono_wrt_pred_crel_dep_mono_wrt_pred_rel_lambda:
  "((A : ⊤) ⇒ ((x : A) ⇒ B x) ⇒ (x : A) →⇩c B x) rel_lambda"
  by (urule (rr) dep_mono_wrt_predI crel_dep_mono_wrt_predI') auto

lemma rel_lambda_eval_eq [simp]:
  assumes "A x"
  shows "(λx : A. f x)`x = f x"
  using assms by (intro eval_eq_if_right_unique_onI) auto

lemma app_eq_if_rel_lambda_eqI:
  assumes "(λx : A. f x) = (λx : A. g x)"
  and "A x"
  shows "f x = g x"
  using assms by (auto dest: fun_cong)

lemma crel_dep_mono_wrt_pred_inf_rel_lambda_inf_if_rel_dep_mono_wrt_pred:
  assumes "((x : A) → B x) R"
  shows "((x : A ⊓ A') →⇩c B x) (λx : A ⊓ A'. R`x)"
  using assms by force

corollary crel_dep_mono_wrt_pred_rel_lambda_if_le_if_rel_dep_mono_wrt_pred:
  assumes "((x : A) → B x) R"
  and [uhint]: "A' ≤ A"
  shows "((x : A') →⇩c B x) (λx : A'. R`x)"
  supply inf_absorb2[uhint]
  by (urule crel_dep_mono_wrt_pred_inf_rel_lambda_inf_if_rel_dep_mono_wrt_pred) (fact assms)

lemma rel_lambda_ext:
  assumes "((x : A) →⇩c B x) R"
  and "⋀x. A x ⟹ f x = R`x"
  shows "(λx : A. f x) = R"
  using assms by (intro ext iffI) (auto intro!: rel_lambdaI intro: rel_eval_if_rel_dep_mono_wrt_predI)

lemma rel_lambda_eval_eq_if_crel_dep_mono_wrt_pred [simp]: "((x : A) →⇩c B x) R ⟹ (λx : A. R`x) = R"
  by (rule rel_lambda_ext) auto

text ‹Every element of @{term "(x : A) →⇩c (B x)"} may be expressed as a lambda abstraction.›

lemma eq_rel_lambda_if_crel_dep_mono_wrt_predE:
  assumes "((x : A) →⇩c B x) R"
  obtains f where "R = (λx : A. f x)"
proof
  let ?f="(λx. R`x)"
  from assms show "R = (λx : A. (λx. R`x) x)" by simp
qed

lemma rel_restrict_left_eq_rel_lambda_if_le_if_rel_dep_mono_wrt_pred:
  assumes "((x : A) → B x) R"
  and "A' ≤ A"
  shows "R↾⇘A'⇙ = (λx : A'. R`x)"
proof -
  from assms mono_rel_dep_mono_wrt_pred_ge_crel_dep_mono_wrt_pred_rel_restrict_left
    have "((x : A') →⇩c B x) R↾⇘A'⇙" by force
  then show ?thesis
    supply ‹A' ≤ A›[uhint] inf_absorb2[uhint] by (urule rel_lambda_ext[symmetric]) auto
qed

lemma mono_rel_lambda: "mono (λA. λx : A. f x)"
  by auto


end