I have defined the restriction of a function to a smaller domain in this way:
First, a valuation is a partial function that maps a variable to its interpretation in an universe 'a
type_synonym 'a Valuation = "Variable ⇀ 'a"
Second, the projection of f over U is as follows:
definition projectVal :: "'a Valuation ⇒ Variable set ⇒ 'a Valuation" where
"projectVal f U =
(
λx. if U ⊆ dom(f) ∧ x ∈ U then f x else undefined
)"
However, with this definition is difficult to prove a lemma like this:
lemma projectVal_Lemma:
assumes "U ⊆ dom(f)"
shows "dom(projectVal f U) = U"
Even, I cannot prove the next lemma!!:
lemma domain_iff_not_undefined:
shows "(∀f x. x ∈ dom f ⟷ f x ≠ undefined)"