Theory DBM_Misc

theory DBM_Misc
  imports 
    Main 
    HOL.Real
begin

lemma finite_set_of_finite_funs2:
  fixes A :: "'a set" 
    and B :: "'b set"
    and C :: "'c set"
    and d :: "'c" 
  assumes "finite A"
    and "finite B"
    and "finite C"
  shows "finite {f. ∀x. ∀y. (x ∈ A ∧ y ∈ B ⟶ f x y ∈ C) ∧ (x ∉ A ⟶ f x y = d) ∧ (y ∉ B ⟶ f x y = d)}"
proof -
  let ?S = "{f. ∀x. ∀y. (x ∈ A ∧ y ∈ B ⟶ f x y ∈ C) ∧ (x ∉ A ⟶ f x y = d) ∧ (y ∉ B ⟶ f x y = d)}"
  let ?R = "{g. ∀x. (x ∈ B ⟶ g x ∈ C) ∧ (x ∉ B ⟶ g x = d)}"
  let ?Q = "{f. ∀x. (x ∈ A ⟶ f x ∈ ?R) ∧ (x ∉ A ⟶ f x = (λy. d))}"
  from finite_set_of_finite_funs[OF assms(2,3)] have "finite ?R" .
  from finite_set_of_finite_funs[OF assms(1) this, of "λ y. d"] have "finite ?Q" .
  moreover have "?S = ?Q"
    by force+
  ultimately show ?thesis by simp
qed

end