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)"
  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,(∈)) ∈ 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 (simp add: fun_set_rel_def)
    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 (simp add: fun_set_rel_def)
    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
    apply (simp add: fun_set_rel_def)
    apply (intro fun_relI)
    apply clarsimp
    apply rule
    defer
    apply (rule A)
    apply (auto simp: br_def dest: fun_relD)
    done
qed



end