Theory ConstOn

theory ConstOn
imports Main
begin

definition const_on :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b ⇒ bool"
  where "const_on f S x = (∀ y ∈ S . f y = x)"

lemma const_onI[intro]: "(⋀y. y ∈ S ⟹ f y = x) ⟹ const_on f S x"
  by (simp add: const_on_def)

lemma const_onD[dest]: "const_on f S x ⟹ y ∈ S ⟹ f y = x"
  by (simp add: const_on_def)

(*
lemma const_onE[elim]: "const_on f S r ==> x : S ==> r = r' ==> f x = r'" 
*)

lemma const_on_insert[simp]: "const_on f (insert x S) y ⟷ const_on f S y ∧ f x = y"
   by auto

lemma const_on_union[simp]: "const_on f (S ∪ S') y ⟷ const_on f S y ∧ const_on f S' y"
  by auto

lemma const_on_subset[elim]: "const_on f S y ⟹ S' ⊆ S ⟹ const_on f S' y"
  by auto


end