Quelle  P2S2R.thy

(* Title: Isomorphisms Betweeen Predicates, Sets and Relations *}
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Isomorphisms Between Predicates, Sets and Relations›

theory P2S2R
imports Main

begin    

notation relcomp (infixl ‹;› 70)
notation inf (infixl ‹⊓› 70)  
notation sup (infixl ‹⊔› 65)
notation Id_on (‹s2r›)
notation Domain (‹r2s›)
notation Collect (‹p2s›)

definition rel_n :: "'a rel ==> 'a rel" where 
  "rel_n ≡ (λX. Id ∩ - X)"  

lemma subid_meet: "R ⊆ Id ==> S ⊆ Id ==> R ∩ S = R ; S"
  by blast

subsection‹Isomorphism Between Sets and Relations›

lemma srs: "r2s ∘ s2r = id"
  by auto

lemma rsr: "R ⊆ Id ==> s2r (r2s R) = R"
  by (auto simp: Id_def Id_on_def Domain_def) 

lemma s2r_inj: "inj s2r"
  by (metis Domain_Id_on injI)

lemma r2s_inj: "R ⊆ Id ==> S ⊆ Id ==> r2s R = r2s S ==> R = S"
  by (metis rsr)

lemma s2r_surj: "∀R ⊆ Id. ∃A. R = s2r A"
  using rsr by auto
 
lemma r2s_surj: "∀A. ∃R ⊆ Id. A = r2s R"
  by (metis Domain_Id_on Id_onE pair_in_Id_conv subsetI)

lemma s2r_union_hom: "s2r (A ∪ B) = s2r A ∪ s2r B"
  by (simp add: Id_on_def)

lemma s2r_inter_hom: "s2r (A ∩ B) = s2r A ∩ s2r B"
  by (auto simp: Id_on_def)  

lemma s2r_inter_hom_var: "s2r (A ∩ B) = s2r A ; s2r B"
  by (auto simp: Id_on_def)

lemma s2r_compl_hom: "s2r (- A) = rel_n (s2r A)"
  by (auto simp add: rel_n_def)

lemma r2s_union_hom: "r2s (R ∪ S) = r2s R ∪ r2s S"
  by auto

lemma r2s_inter_hom: "R ⊆ Id ==> S ⊆ Id ==> r2s (R ∩ S) = r2s R ∩ r2s S"
  by auto

lemma r2s_inter_hom_var: "R ⊆ Id ==> S ⊆ Id ==> r2s (R ; S) = r2s R ∩ r2s S"
  by (metis r2s_inter_hom subid_meet)

lemma r2s_ad_hom: "R ⊆ Id ==> r2s (rel_n R) = - r2s R"
  by (metis r2s_surj rsr s2r_compl_hom)

subsection ‹Isomorphism Between Predicates and Sets›

type_synonym 'a pred = "'a ==> bool"

definition s2p :: "'a set ==> 'a pred" where
  "s2p S = (λx. x ∈ S)"

lemma sps [simp]: "s2p ∘ p2s = id" 
  by (intro ext, simp add: s2p_def)

lemma psp [simp]: "p2s ∘ s2p = id"
  by (intro ext, simp add: s2p_def)

lemma s2p_bij: "bij s2p"
  using o_bij psp sps by blast

lemma p2s_bij: "bij p2s"
  using o_bij psp sps by blast

lemma s2p_compl_hom: "s2p (- A) = - (s2p A)"
  by (metis Collect_mem_eq comp_eq_dest_lhs id_apply sps uminus_set_def)
 
lemma s2p_inter_hom: "s2p (A ∩ B) = (s2p A) ⊓ (s2p B)"
  by (metis Collect_mem_eq comp_eq_dest_lhs id_apply inf_set_def sps)

lemma s2p_union_hom: "s2p (A ∪ B) = (s2p A) ⊔ (s2p B)"
  by (auto simp: s2p_def)

lemma p2s_neg_hom: "p2s (- P) = - (p2s P)"
  by fastforce

lemma p2s_conj_hom: "p2s (P ⊓ Q) = p2s P ∩ p2s Q"
  by blast

lemma p2s_disj_hom: "p2s (P ⊔ Q) = p2s P ∪ p2s Q"
  by blast

subsection ‹Isomorphism Between Predicates and Relations›

definition p2r :: "'a pred ==> 'a rel" where
  "p2r P = {(s,s) |s. P s}"

definition r2p :: "'a rel ==> 'a pred" where
  "r2p R = (λx. x ∈ Domain R)"

lemma p2r_subid: "p2r P ⊆ Id"
  by (simp add: p2r_def subset_eq)

lemma p2s2r: "p2r = s2r ∘ p2s"
proof (intro ext)
  fix P :: "'a pred"
  have "{(a, a) |a. P a} = {(b, a). b = a ∧ P b}"
    by blast
  thus "p2r P = (s2r ∘ p2s) P"
    by (simp add: Id_on_def' p2r_def)
qed

lemma r2s2p: "r2p = s2p ∘ r2s"
  by (intro ext, simp add: r2p_def s2p_def)

lemma prp [simp]: "r2p ∘ p2r = id"
  by (intro ext, simp add: p2s2r r2p_def)

lemma rpr: "R ⊆ Id ==> p2r (r2p R) = R"
  by (metis comp_apply id_apply p2s2r psp r2s2p rsr)

lemma p2r_inj: "inj p2r"
  by (metis comp_eq_dest_lhs id_apply injI prp)

lemma r2p_inj: "R ⊆ Id ==> S ⊆ Id ==> r2p R = r2p S ==> R = S"
  by (metis rpr)

lemma p2r_surj: "∀ R ⊆ Id. ∃P. R = p2r P"
  using rpr by auto

lemma r2p_surj: "∀P. ∃R ⊆ Id. P = r2p R"
  by (metis comp_apply id_apply p2r_subid prp)

lemma p2r_neg_hom: "p2r (- P) = rel_n (p2r P)"
  by (simp add: p2s2r p2s_neg_hom s2r_compl_hom)

lemma p2r_conj_hom [simp]: "p2r P ∩ p2r Q = p2r (P ⊓ Q)"
  by (simp add: p2s2r p2s_conj_hom s2r_inter_hom)

lemma p2r_conj_hom_var [simp]: "p2r P ; p2r Q = p2r (P ⊓ Q)"
  by (simp add: p2s2r p2s_conj_hom s2r_inter_hom_var)

lemma p2r_id_neg [simp]: "Id ∩ - p2r p = p2r (-p)"
  by (auto simp: p2r_def)

lemma [simp]: "p2r bot = {}"
  by (auto simp: p2r_def)

lemma p2r_disj_hom [simp]: "p2r P ∪ p2r Q = p2r (P ⊔ Q)"
  by (simp add: p2s2r p2s_disj_hom s2r_union_hom)

lemma r2p_ad_hom: "R ⊆ Id ==> r2p (rel_n R) = - (r2p R)"
  by (simp add: r2s2p r2s_ad_hom s2p_compl_hom)

lemma r2p_inter_hom: "R ⊆ Id ==> S ⊆ Id ==> r2p (R ∩ S) = (r2p R) ⊓ (r2p S)"
  by (simp add: r2s2p r2s_inter_hom s2p_inter_hom)

lemma r2p_inter_hom_var: "R ⊆ Id ==> S ⊆ Id ==> r2p (R ; S) = (r2p R) ⊓ (r2p S)"
  by (simp add: r2s2p r2s_inter_hom_var s2p_inter_hom)

lemma rel_to_pred_union_hom: "R ⊆ Id ==> S ⊆ Id ==> r2p (R ∪ S) = (r2p R) ⊔ (r2p S)"
  by (simp add: Domain_Un_eq r2s2p s2p_union_hom)

end