Theory Binary_Relations_Function_Evaluation

✐‹creator "Kevin Kappelmann"›
subsection ‹Evaluation of Functions as Binary Relations›
theory Binary_Relations_Function_Evaluation
  imports
    Binary_Relations_Right_Unique
    Binary_Relations_Extend
begin

consts eval :: "'a ⇒ 'b ⇒ 'c"

definition "eval_rel R x ≡ THE y. R x y"
adhoc_overloading eval eval_rel

bundle eval_syntax
begin
notation eval ("'(`')")
notation eval ("(_`_)" [999, 1000] 999)
end
bundle no_eval_syntax
begin
no_notation eval ("'(`')")
no_notation eval ("(_`_)" [999, 1000] 999)
end
unbundle eval_syntax

lemma eval_eq_if_right_unique_onI:
  assumes "right_unique_on P R"
  and "P x"
  and "R x y"
  shows "R`x = y"
  using assms unfolding eval_rel_def by (auto dest: right_unique_onD)

lemma eval_eq_if_right_unique_on_eqI:
  assumes "right_unique_on ((=) x) R"
  and "R x y"
  shows "R`x = y"
  using assms by (auto intro: eval_eq_if_right_unique_onI)

lemma rel_eval_if_ex1:
  assumes "∃!y. R x y"
  shows "R x (R`x)"
  using assms unfolding eval_rel_def by (rule theI')

lemma rel_if_eval_eq_if_in_dom_if_right_unique_on_eq:
  assumes "right_unique_on ((=) x) R"
  and "in_dom R x"
  and "R`x = y"
  shows "R x y"
  using assms by (blast intro: rel_eval_if_ex1[of R x] dest: right_unique_onD)

corollary rel_eval_if_in_dom_if_right_unique_on_eq:
  assumes "right_unique_on ((=) x) R"
  and "in_dom R x"
  shows "R x (R`x)"
  using assms by (rule rel_if_eval_eq_if_in_dom_if_right_unique_on_eq) simp

lemma eq_app_eval_eq_eq [simp]: "(λx. (=) (f x))`x = f x"
  by (auto intro: eval_eq_if_right_unique_onI)

lemma extend_eval_eq_if_not_in_dom [simp]:
  assumes "¬(in_dom R x)"
  shows "(extend x y R)`x = y"
  using assms by (force intro: eval_eq_if_right_unique_on_eqI)

corollary extend_bottom_eval_eq [simp]:
  fixes x :: 'a and y :: 'b
  shows "(extend x y (⊥ :: 'a ⇒ 'b ⇒ bool))`x = y"
  by (intro extend_eval_eq_if_not_in_dom) auto

lemma glue_eval_eqI:
  assumes "right_unique_on P (glue ℛ)"
  and "ℛ R"
  and "P x"
  and "R x y"
  shows "(glue ℛ)`x = y"
  using assms by (auto intro: eval_eq_if_right_unique_onI)

lemma glue_eval_eq_evalI:
  assumes "right_unique_on P (glue ℛ)"
  and "ℛ R"
  and "P x"
  and "in_dom R x"
  shows "(glue ℛ)`x = R`x"
  using assms by (intro glue_eval_eqI[of P ℛ R])
  (auto intro: rel_if_eval_eq_if_in_dom_if_right_unique_on_eq[of x] dest: right_unique_onD)

text ‹Note: the following rest on the definition of extend and eval:›

lemma extend_eval_eq_if_neq [simp]:
  fixes R :: "'a ⇒ 'b ⇒ bool"
  shows "x ≠ y ⟹ (extend y z R)`x = R`x"
  unfolding extend_rel_def eval_rel_def by auto

lemma sup_eval_eq_left_eval_if_not_in_dom [simp]:
  fixes R S :: "'a ⇒ 'b ⇒ bool"
  shows "¬(in_dom S x) ⟹ (R ⊔ S)`x = R`x"
  unfolding eval_rel_def by (cases "∃y. S x y") auto

lemma sup_eval_eq_right_eval_if_not_in_dom [simp]:
  fixes R S :: "'a ⇒ 'b ⇒ bool"
  shows "¬(in_dom R x) ⟹ (R ⊔ S)`x = S`x"
  unfolding eval_rel_def by (cases "∃y. R x y") auto

lemma rel_restrict_left_eval_eq_if_pred [simp]:
  fixes R :: "'a ⇒ 'b ⇒ bool"
  assumes "P x"
  shows "(R↾⇘P⇙)`x = R`x"
  (*FIXME: proof relying on specific definitions; can we do better?*)
  using assms unfolding eval_rel_def rel_restrict_left_pred_def by auto

end