Theory Collections.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  (Rbool_rel) O br Collect (λ_. True)"

lemma fun_set_rel_def: "Rfun_set_rel = (Rbool_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 (Rfun_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 (Rfun_set_rel) = UNIV"
proof -
  {
    fix b
    have "a. (a,b)Rfun_set_rel" unfolding fun_set_rel_def
      apply (rule exI)
      apply (rule relcompI)
    proof -
      show "((λx. xb),b)br Collect (λ_. True)" by (auto simp: br_def)
      show "(λx'. x. (x',x)R  xb,λ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  Rfun_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)(Rbool_rel)  Rfun_set_rel"
  unfolding fun_set_rel_def
  by (auto simp: br_def)

lemma fun_set_empty_refine[autoref_rules]: 
  "(λ_. False,{})Rfun_set_rel"
  by (force simp add: fun_set_rel_def br_def)

lemma fun_set_UNIV_refine[autoref_rules]: 
  "(λ_. True,UNIV)Rfun_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,(∪))Rfun_set_rel  Rfun_set_rel  Rfun_set_rel"
proof -
  have A: "a b. (λx. xa  xb, 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,(∩))Rfun_set_rel  Rfun_set_rel  Rfun_set_rel"
proof -
  have A: "a b. (λx. xa  xb, 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,(-))Rfun_set_rel  Rfun_set_rel  Rfun_set_rel"
proof -
  have A: "a b. (λx. xa  ¬xb, 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