# Theory Impl_Cfun_Set

```section ‹Set by Characteristic Function›
theory Impl_Cfun_Set
imports "../Intf/Intf_Set"
begin

definition fun_set_rel where
fun_set_rel_internal_def:
"fun_set_rel R ≡ (R→bool_rel) O br Collect (λ_. True)"

lemma fun_set_rel_def: "⟨R⟩fun_set_rel = (R→bool_rel) O br Collect (λ_. True)"

lemma fun_set_rel_sv[relator_props]:
"⟦single_valued R; Range R = UNIV⟧ ⟹ single_valued (⟨R⟩fun_set_rel)"
unfolding fun_set_rel_def
by (tagged_solver (keep))

lemma fun_set_rel_RUNIV[relator_props]:
assumes SV: "single_valued R"
shows "Range (⟨R⟩fun_set_rel) = UNIV"
proof -
{
fix b
have "∃a. (a,b)∈⟨R⟩fun_set_rel" unfolding fun_set_rel_def
apply (rule exI)
apply (rule relcompI)
proof -
show "((λx. x∈b),b)∈br Collect (λ_. True)" by (auto simp: br_def)
show "(λx'. ∃x. (x',x)∈R ∧ x∈b,λx. x ∈ b)∈R → bool_rel"
by (auto dest: single_valuedD[OF SV])
qed
} thus ?thesis by blast
qed

lemmas [autoref_rel_intf] = REL_INTFI[of fun_set_rel i_set]

lemma fs_mem_refine[autoref_rules]: "(λx f. f x,(∈)) ∈ R → ⟨R⟩fun_set_rel → bool_rel"
apply (intro fun_relI)
apply (auto simp add: fun_set_rel_def br_def dest: fun_relD)
done

lemma fun_set_Collect_refine[autoref_rules]:
"(λx. x, Collect)∈(R→bool_rel) → ⟨R⟩fun_set_rel"
unfolding fun_set_rel_def
by (auto simp: br_def)

lemma fun_set_empty_refine[autoref_rules]:
"(λ_. False,{})∈⟨R⟩fun_set_rel"
by (force simp add: fun_set_rel_def br_def)

lemma fun_set_UNIV_refine[autoref_rules]:
"(λ_. True,UNIV)∈⟨R⟩fun_set_rel"
by (force simp add: fun_set_rel_def br_def)

lemma fun_set_union_refine[autoref_rules]:
"(λa b x. a x ∨ b x,(∪))∈⟨R⟩fun_set_rel → ⟨R⟩fun_set_rel → ⟨R⟩fun_set_rel"
proof -
have A: "⋀a b. (λx. x∈a ∨ x∈b, a ∪ b) ∈ br Collect (λ_. True)"
by (auto simp: br_def)

show ?thesis
apply (intro fun_relI)
apply clarsimp
apply rule
defer
apply (rule A)
apply (auto simp: br_def dest: fun_relD)
done
qed

lemma fun_set_inter_refine[autoref_rules]:
"(λa b x. a x ∧ b x,(∩))∈⟨R⟩fun_set_rel → ⟨R⟩fun_set_rel → ⟨R⟩fun_set_rel"
proof -
have A: "⋀a b. (λx. x∈a ∧ x∈b, a ∩ b) ∈ br Collect (λ_. True)"
by (auto simp: br_def)

show ?thesis
apply (intro fun_relI)
apply clarsimp
apply rule
defer
apply (rule A)
apply (auto simp: br_def dest: fun_relD)
done
qed

lemma fun_set_diff_refine[autoref_rules]:
"(λa b x. a x ∧ ¬b x,(-))∈⟨R⟩fun_set_rel → ⟨R⟩fun_set_rel → ⟨R⟩fun_set_rel"
proof -
have A: "⋀a b. (λx. x∈a ∧ ¬x∈b, a - b) ∈ br Collect (λ_. True)"
by (auto simp: br_def)

show ?thesis