Theory Impl_Cfun_Set

header {* 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)"
  by (simp add: relAPP_def fun_set_rel_internal_def)

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,op ∈) ∈ 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)


end