# Theory Refine_Intersection

```theory Refine_Intersection
imports Refine_Unions
begin

consts i_inter::"interface ⇒ interface ⇒ interface"
hide_const (open) Impl_Uv_Set.inter_rel

definition inter_rel_internal: "inter_rel AA BB = {((a, b), A ∩ B)|a b A B. (a, A) ∈ AA ∧ (b, B) ∈ BB}"
lemma inter_rel_def: "⟨AA, BB⟩inter_rel = {((a, b), A ∩ B)|a b A B. (a, A) ∈ AA ∧ (b, B) ∈ BB}"
by (auto simp: inter_rel_internal relAPP_def)
lemmas [autoref_rel_intf] = REL_INTFI[of inter_rel i_inter]

lemma inter_rel_br: "⟨(br a I), (br b J)⟩inter_rel = br (λ(x, y). a x ∩ b y) (λx. I (fst x) ∧ J (snd x))"
by (auto simp: inter_rel_def br_def)

definition mk_inter::"'a set ⇒ 'a set ⇒ 'a set"
where [simp]: "mk_inter ≡ λX Y. X ∩ Y"

definition mk_inter_coll::"'a set ⇒ 'a set ⇒ 'a set"
where [simp]: "mk_inter_coll ≡ λX Y. X ∩ Y"

context includes autoref_syntax begin
lemma [autoref_op_pat]: "mk_inter ≡ OP (mk_inter)"
by simp
lemma [autoref_op_pat]: "mk_inter ≡ OP (mk_inter_coll)"
by simp
end

lemma inter_plane_clw_autoref[autoref_rules]:
assumes "PREFER single_valued A"
assumes "PREFER single_valued B"
shows "(λxs sctni. map (λx. (x, sctni)) xs, mk_inter_coll) ∈ clw_rel A → B → clw_rel (⟨A,B⟩inter_rel)"
using assms
by (fastforce
intro!: nres_relI RETURN_SPEC_refine brI
dest!: brD
elim!: single_valued_as_brE
simp: RETURN_RES_refine_iff inter_rel_br Union_rel_br lw_rel_def)

lemma inter_plane_autoref[autoref_rules]:
assumes "PREFER single_valued A"
assumes "PREFER single_valued B"
shows "(λx sctn. (x, sctn), mk_inter) ∈ A → B → ⟨A,B⟩inter_rel"
using assms
by (fastforce
intro!: nres_relI RETURN_SPEC_refine brI
dest!: brD
elim!: single_valued_as_brE
simp: RETURN_RES_refine_iff inter_rel_br Union_rel_br lw_rel_def)

definition unintersect::"'a set ⇒ 'a set nres"
where [refine_vcg_def]: "unintersect X = SPEC (λR. X ⊆ R)"

definition unintersect_coll::"'a set ⇒ 'a set nres"
where [refine_vcg_def]: "unintersect_coll X = SPEC (λR. X ⊆ R)"

definition unintersect2::"'a set ⇒ 'a set nres"
where [refine_vcg_def]: "unintersect2 X = SPEC (λR. X ⊆ R)"

definition unintersect_coll2::"'a set ⇒ 'a set nres"
where [refine_vcg_def]: "unintersect_coll2 X = SPEC (λR. X ⊆ R)"

lemma unintersect_clw_impl[autoref_rules]:
assumes "PREFER single_valued A"
assumes "PREFER single_valued B"
shows "(λxs. RETURN ((map fst) xs), unintersect_coll) ∈ clw_rel (⟨A,B⟩inter_rel) → ⟨clw_rel A⟩nres_rel"
using assms
by (auto intro!: nres_relI RETURN_SPEC_refine elim!: single_valued_as_brE
simp: unintersect_coll_def inter_rel_br Union_rel_br lw_rel_def)
(auto simp: br_def)

lemma unintersect_impl[autoref_rules]:
assumes "PREFER single_valued A"
assumes "PREFER single_valued B"
shows "(λx. RETURN (fst x), unintersect) ∈ (⟨A,B⟩inter_rel) → ⟨A⟩nres_rel"
using assms
by (auto intro!: nres_relI RETURN_SPEC_refine elim!: single_valued_as_brE
simp: unintersect_def inter_rel_br Union_rel_br lw_rel_def)
(auto simp: br_def)

lemma unintersect_clw2_impl[autoref_rules]:
assumes "PREFER single_valued A"
assumes "PREFER single_valued B"
shows "(λxs. RETURN ((map snd) xs), unintersect_coll2) ∈ clw_rel (⟨A,B⟩inter_rel) → ⟨clw_rel B⟩nres_rel"
using assms
by (auto intro!: nres_relI RETURN_SPEC_refine elim!: single_valued_as_brE
simp: unintersect_coll2_def inter_rel_br Union_rel_br lw_rel_def)
(auto simp: br_def)

lemma unintersect2_impl[autoref_rules]:
assumes "PREFER single_valued A"
assumes "PREFER single_valued B"
shows "(λx. RETURN (snd x), unintersect2) ∈ (⟨A,B⟩inter_rel) → ⟨B⟩nres_rel"
using assms
by (auto intro!: nres_relI RETURN_SPEC_refine elim!: single_valued_as_brE
simp: unintersect2_def inter_rel_br Union_rel_br lw_rel_def)
(auto simp: br_def)

definition get_inter::"'a set ⇒ ('a set × 'a set) nres"
where [refine_vcg_def]: "get_inter X = SPEC (λ(Y, Z). X = Y ∩ Z)"

lemma get_inter_autoref[autoref_rules]:
"(λx. RETURN x, get_inter) ∈ ⟨X,S⟩inter_rel → ⟨X ×⇩r S⟩nres_rel"
by (force simp: get_inter_def inter_rel_def nres_rel_def intro!: RETURN_SPEC_refine)

definition split_by_inter::"'a set ⇒ ('a set × 'a set) nres"
where [refine_vcg_def]: "split_by_inter X = SPEC (λ(Y, YS). X = Y ∪ YS)"

context includes autoref_syntax begin
lemma split_by_inter_appr_plane_autoref[autoref_rules]:
assumes "PREFER single_valued A"
assumes "PREFER single_valued S"
assumes "(xs, X) ∈ clw_rel (⟨A,S⟩inter_rel)"
shows
"(let (a, b) = List.partition (λ(_, sctn). sctn = snd (hd xs)) xs in RETURN (a, b),
split_by_inter \$ X) ∈
⟨clw_rel (⟨A, S⟩inter_rel) ×⇩r clw_rel (⟨A, S⟩inter_rel)⟩nres_rel"
using assms
by (fastforce simp: Let_def split_by_inter_def split_beta'
lw_rel_def Union_rel_br inter_rel_br ex_br_conj_iff Id_br[where 'a="'a sctn"]
elim!: single_valued_as_brE
intro!: nres_relI RETURN_SPEC_refine
dest!: brD)

end

end```