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