Theory Relation_Extra

section ‹ Relational Universe ›

theory Relation_Extra
  imports "HOL-Library.FuncSet" "HOL-Library.AList" List_Extra Overriding
begin

no_notation SCons (infixr ‹##› 65)

text ‹ This theory develops a universe for a Z-like relational language, including the core 
  operators of the ISO Z metalanguage. Much of this already exists in @{theory HOL.Relation},
  but we need to add some additional functions and sets. It characterises relations, partial
  functions, total functions, and finite functions. ›

subsection ‹ Type Syntax›

text ‹ We set up some nice syntax for heterogeneous relations at the type level ›

syntax
  "_rel_type" :: "type ⇒ type ⇒ type" (infixr "↔" 0)

translations
  (type) "'a ↔ 'b" == (type) "('a × 'b) set"

text ‹ Setup pretty printing for homogeneous relations. ›

print_translation ‹
let fun tr' ctx [ Const (@{type_syntax "prod"},_) $ a $ b ] = 
      if a = b then Syntax.const @{type_syntax "rel"} $ a else raise Match;
in [(@{type_syntax "set"},tr')]
end
›

subsection ‹ Notation for types as sets ›

definition "TUNIV (a::'a itself) = (UNIV :: 'a set)"

syntax "_tvar" :: "type ⇒ logic" ("[_]⇩T")
translations "['a]⇩T" == "CONST TUNIV TYPE('a)"

lemma TUNIV_mem [simp]: "x ∈ ['a]⇩T"
  by (simp add: TUNIV_def)

subsection ‹ Relational Function Operations ›

text ‹ These functions are all adapted from their ISO Z counterparts. ›

definition rel_apply :: "('a ↔ 'b) ⇒ 'a ⇒ 'b" ("_'(_')⇩r" [999,0] 999) where
"rel_apply R x = (if (∃! y. (x, y) ∈ R) then THE y. (x, y) ∈ R else undefined)"

text ‹ If there exists a unique @{term "e⇩3"} such that @{term "(e⇩2, e⇩3)"} is in @{term "e⇩1"}, then 
  the value of @{term "e⇩1(e⇩2)⇩r"} is @{term e⇩3}, otherwise each @{term "e⇩1(e⇩2)⇩r"} has a fixed but 
  unknown value (i.e. @{const undefined}). ›

definition rel_domres :: "'a set ⇒ ('a ↔ 'b) ⇒ 'a ↔ 'b" (infixr "⊲⇩r" 85) where
"rel_domres A R = {p ∈ R. fst p ∈ A}"

lemma rel_domres_math_def: "A ⊲⇩r R = {(k, v) ∈ R. k ∈ A}"
  by (auto simp add: rel_domres_def)

text ‹ Domain restriction (@{term "A ⊲⇩r R"} contains the set of pairs in @{term R}, such that the
  first element of every such pair in in @{term A}. ›

definition rel_ranres :: "('a ↔ 'b) ⇒ 'b set ⇒ 'a ↔ 'b" (infixl "⊳⇩r" 85) where
"rel_ranres R A = {p ∈ R. snd p ∈ A}"

text ‹ We employ some type class trickery to enable a polymorphic operator for override that can
  instantiate @{typ "'a set"}, which is needed for relational overriding. The following class's
  sole purpose is to allow pairs to be the only valid instantiation element for the set type. ›

class pre_restrict =
  fixes cmpt :: "'a set ⇒ 'a set ⇒ bool"
  and res :: "'a set ⇒ 'a set ⇒ 'a set"

instantiation prod :: (type, type) pre_restrict
begin

text ‹ Relations are compatible is they agree on the values for maplets they both possess. ›

definition cmpt_prod :: "('a ↔ 'b) ⇒ ('a ↔ 'b) ⇒ bool"
  where [simp]: "cmpt_prod R S = ((Domain R) ⊲⇩r S = (Domain S) ⊲⇩r R)"
definition res_prod :: "('a ↔ 'b) ⇒ ('a ↔ 'b) ⇒ 'a ↔ 'b" 
  where [simp]: "res_prod R S = ((- Domain S) ⊲⇩r R) ∪ S"
instance ..
end

instantiation set :: (pre_restrict) oplus
begin

definition oplus_set :: "'a set ⇒ 'a set ⇒ 'a set" where
"oplus_set = res"

instance ..

end

definition rel_update :: "('a ↔ 'b) ⇒ 'a ⇒ 'b ⇒ 'a ↔ 'b" where
"rel_update R k v = R ⊕ {(k, v)}"

text ‹ Relational update adds a new pair to a relation. ›

definition rel_disjoint :: "('a ↔ 'b set) ⇒ bool" where
"rel_disjoint f = (∀ p ∈ f. ∀ q ∈ f. p ≠ q ⟶ snd p ∩ snd q = {})"

definition rel_partitions :: "('a ↔ 'b set) ⇒ 'b set ⇒ bool" where
"rel_partitions f a = (rel_disjoint f ∧ ⋃ (Range f) = a)"

subsection ‹ Domain laws ›

declare Domain_Un_eq [simp]

lemma Domain_Preimage: "Domain P = P¯ `` UNIV"
  by (simp add: Image_def Domain_unfold)

lemma Domain_relcomp [simp]: "Domain (P O Q) = Domain (P ⊳⇩r Domain Q)"
  by (force simp add: Domain_iff rel_ranres_def)

lemma Domain_relcomp_conv: "Domain (P O Q) = (P¯ `` Domain(Q))"
  by (simp add: Domain_Preimage converse_relcomp relcomp_Image)

lemma Domain_set: "Domain (set xs) = set (map fst xs)"
  by (simp add: Domain_fst)

subsection ‹ Range laws ›

lemma Range_Image: "Range P = P `` UNIV"
  by (simp add: Image_def Range_iff set_eq_iff)

lemma Range_relcomp: "Range (P O Q) = (Q `` Range(P))"
  by (simp add: Range_Image relcomp_Image)

subsection ‹ Domain Restriction ›

lemma Domain_rel_domres [simp]: "Domain (A ⊲⇩r R) = A ∩ Domain(R)"
  by (auto simp add: rel_domres_def)

lemma rel_domres_empty [simp]: "{} ⊲⇩r R = {}"
  by (simp add: rel_domres_def)

lemma rel_domres_UNIV [simp]: "UNIV ⊲⇩r R = R"
  by (simp add: rel_domres_def)

lemma rel_domres_nil [simp]: "A ⊲⇩r {} = {}"
  by (simp add: rel_domres_def)

lemma rel_domres_inter [simp]: "A ⊲⇩r B ⊲⇩r R = (A ∩ B) ⊲⇩r R"
  by (auto simp add: rel_domres_def)

lemma rel_domres_compl_disj: "A ∩ Domain P = {} ⟹ (- A) ⊲⇩r P = P"
  by (auto simp add: rel_domres_def)

lemma rel_domres_notin_Dom: "k ∉ Domain(f) ⟹ (- {k}) ⊲⇩r f = f"
  by (simp add: rel_domres_compl_disj)

lemma rel_domres_Id_on: "A ⊲⇩r R = Id_on A O R"
  by (auto simp add: rel_domres_def Id_on_def relcomp_unfold)

lemma rel_domres_insert [simp]:
 "A ⊲⇩r insert (k, v) R = (if (k ∈ A) then insert (k, v) (A ⊲⇩r R) else A ⊲⇩r R)"
  by (auto simp add: rel_domres_def)

lemma rel_domres_insert_set [simp]: "x ∉ Domain P ⟹ (insert x A) ⊲⇩r P = A ⊲⇩r P"
  by (auto simp add: rel_domres_def)

lemma Image_as_rel_domres: "R `` A = Range (A ⊲⇩r R)"
  by (auto simp add: rel_domres_def)

lemma rel_domres_Un [simp]: "A ⊲⇩r (S ∪ R) = (A ⊲⇩r S) ∪ (A ⊲⇩r R)"
  by (auto simp add: rel_domres_def)

subsection ‹ Range Restriction ›

lemma rel_ranres_UNIV [simp]: "P ⊳⇩r UNIV = P"
  by (auto simp add: rel_ranres_def)

lemma rel_ranres_Un [simp]: "(P ∪ Q) ⊳⇩r A = (P ⊳⇩r A ∪ Q ⊳⇩r A)"
  by (auto simp add: rel_ranres_def)

lemma rel_ranres_relcomp [simp]: "(P O Q) ⊳⇩r A = P O (Q ⊳⇩r A)"
  by (auto simp add: rel_ranres_def relcomp_unfold prod.case_eq_if)

lemma conv_rel_domres [simp]: "(P ⊳⇩r A)¯ = A ⊲⇩r P¯"
  by (auto simp add: rel_domres_def rel_ranres_def)

lemma rel_ranres_le: "A ⊆ B ⟹ f ⊳⇩r A ≤ f ⊳⇩r B"
  by (simp add: Collect_mono_iff in_mono rel_ranres_def)

subsection ‹ Relational Override ›

class restrict = pre_restrict +
  assumes cmpt_sym: "cmpt P Q ⟹ cmpt Q P"
  and cmpt_empty: "cmpt {} P"
  assumes res_idem: "res P P = P"
  and res_assoc: "res P (res Q R) = res (res P Q) R"
  and res_lzero: "res {} P = P"
  and res_comm: "cmpt P Q ⟹ res P Q = res Q P"
  and res_cmpt: "⟦ cmpt P Q; cmpt (res P Q) R ⟧ ⟹ cmpt P R"
  and res_cmptI: "⟦ cmpt P Q; cmpt P R; cmpt Q R ⟧ ⟹ cmpt (res P Q) R"

lemma res_cmpt_rel: "cmpt (P :: 'a ↔ 'b) Q ⟹ cmpt (res P Q) R ⟹ cmpt P R"
  by (fastforce simp add: rel_domres_def Domain_iff)

instance prod :: (type, type) restrict
  by (intro_classes, simp_all only: res_cmpt_rel, auto simp add: rel_domres_def Domain_unfold)
  
instantiation set :: (restrict) override
begin
definition compatible_set :: "'a set ⇒ 'a set ⇒ bool" where
"compatible_set = cmpt"

instance 
  apply (intro_classes, simp_all add: oplus_set_def compatible_set_def res_idem res_assoc res_lzero cmpt_sym cmpt_empty res_comm res_cmptI)
  using res_cmpt apply blast
  done
end

lemma override_eq: "R ⊕ S = ((- Domain S) ⊲⇩r R) ∪ S"
  by (simp add: oplus_set_def)

lemma Domain_rel_override [simp]: "Domain (R ⊕ S) = Domain(R) ∪ Domain(S)"
  by (auto simp add: oplus_set_def)

lemma Range_rel_override: "Range(R ⊕ S) ⊆ Range(R) ∪ Range(S)"
  by (auto simp add: oplus_set_def rel_domres_def)

lemma compatible_rel: "R ## S = (Domain R ⊲⇩r S = Domain S ⊲⇩r R)"
  by (simp add: compatible_set_def)

lemma compatible_relI: "Domain R ⊲⇩r S = Domain S ⊲⇩r R ⟹ R ## S"
  by (simp add: compatible_rel)

subsection ‹ Functional Relations ›

abbreviation functional :: "('a ↔ 'b) ⇒ bool" where
"functional R ≡ single_valued R"

lemma functional_def: "functional R ⟷ inj_on fst R"
  by (force simp add: single_valued_def inj_on_def)

lemma functional_algebraic: "functional R ⟷ R¯ O R ⊆ Id"
  apply (simp add: functional_def subset_iff relcomp_unfold, safe)
  using inj_on_eq_iff apply fastforce
  apply (metis inj_onI surjective_pairing)
  done

lemma functional_apply: 
  assumes "functional R" "(x, y) ∈ R"
  shows "R(x)⇩r = y"
  by (metis (no_types, lifting) Domain.intros DomainE assms(1) assms(2) single_valuedD rel_apply_def theI_unique)  

lemma functional_apply_iff: "functional R ⟹ (x, y) ∈ R ⟷ (x ∈ Domain R ∧ R(x)⇩r = y)"
  by (auto simp add: functional_apply)

lemma functional_elem:
  assumes "functional R" "x ∈ Domain(R)"
  shows "(x, R(x)⇩r) ∈ R"
  using assms(1) assms(2) functional_apply by fastforce

lemma functional_override [intro!]: "⟦ functional R; functional S ⟧ ⟹ functional (R ⊕ S)"
  by (auto simp add: functional_algebraic oplus_set_def rel_domres_def)

lemma functional_union [intro!]: "⟦ functional R; functional S; R ## S ⟧ ⟹ functional (R ∪ S)"
  by (metis functional_override le_sup_iff override_comm override_eq single_valued_subset subsetI)
  
definition functional_list :: "('a × 'b) list ⇒ bool" where
"functional_list xs = (∀ x y z. ListMem (x,y) xs ∧ ListMem (x,z) xs ⟶ y = z)"

lemma functional_insert [simp]: "functional (insert (x,y) g) ⟷ (g``{x} ⊆ {y} ∧ functional g)"
  by (auto simp add:functional_def inj_on_def image_def)

lemma functional_list_nil[simp]: "functional_list []"
  by (simp add:functional_list_def ListMem_iff)

lemma functional_list: "functional_list xs ⟷ functional (set xs)"
  apply (induct xs)
   apply (simp add:functional_def)
  apply (simp add:functional_def functional_list_def ListMem_iff)
  apply (safe)
         apply (force)
        apply (force)
       apply (force)
      apply (force)
     apply (force)
    apply (force)
   apply (force)
  apply (force)
  done

definition fun_rel :: "('a ⇒ 'b) ⇒ ('a ↔ 'b)" where
"fun_rel f = {(x, y). y = f x}"

lemma functional_fun_rel: "functional (fun_rel f)"
  by (simp add: fun_rel_def functional_def)
     (metis (mono_tags, lifting) Product_Type.Collect_case_prodD inj_onI prod.expand)

lemma rel_apply_fun [simp]: "(fun_rel f)(x)⇩r = f x"
  by (simp add: fun_rel_def rel_apply_def)

text ‹ Make a relation functional by removing any pairs that have duplicate distinct values. ›

definition mk_functional :: "('a ↔ 'b) ⇒ ('a ↔ 'b)" where
"mk_functional R = {(x, y) ∈ R. ∀ y'. (x, y') ∈ R ⟶ y = y'}"

lemma mk_functional [simp]: "functional (mk_functional R)"
  by (auto simp add: mk_functional_def single_valued_def)

lemma mk_functional_fp: "functional R ⟹ mk_functional R = R"
  by (auto simp add: mk_functional_def single_valued_def)

lemma mk_functional_idem: "mk_functional (mk_functional R) = mk_functional R"
  using mk_functional mk_functional_fp by blast

lemma mk_functional_subset [simp]: "mk_functional R ⊆ R"
  by (auto simp add: mk_functional_def)

lemma Domain_mk_functional: "Domain (mk_functional R) ⊆ Domain R"
  by (auto simp add: mk_functional_def)

definition single_valued_dom :: "('a × 'b) set ⇒ 'a set" where
"single_valued_dom R = {x ∈ Domain(R). ∃ y. R `` {x} = {y}}"

lemma mk_functional_single_valued_dom: "mk_functional R = single_valued_dom R ⊲⇩r R"
  by (auto simp add: mk_functional_def single_valued_dom_def rel_domres_math_def Domain_unfold)
     (metis Image_singleton_iff singletonD)
  
subsection ‹ Left-Total Relations›

definition left_totalr_on :: "'a set ⇒ ('a ↔ 'b) ⇒ bool" where
"left_totalr_on A R ⟷ (∀x∈A. ∃y. (x, y) ∈ R)"

abbreviation "left_totalr R ≡ left_totalr_on UNIV R"

lemma left_totalr_algebraic: "left_totalr R ⟷ Id ⊆ R O R¯"
  by (auto simp add: left_totalr_on_def)

lemma left_totalr_fun_rel: "left_totalr (fun_rel f)"
  by (simp add: left_totalr_on_def fun_rel_def)

subsection ‹ Injective Relations ›

definition injective :: "('a ↔ 'b) ⇒ bool" where
"injective R = (functional R ∧ R O R¯ ⊆ Id)"

lemma injectiveI: 
  assumes "functional R" "⋀ x y. ⟦ x ∈ Domain R; y ∈ Domain R; R(x)⇩r = R(y)⇩r ⟧ ⟹ x = y"
  shows "injective R"
  using assms by (auto simp add: injective_def functional_apply_iff)

subsection ‹ Relation Sets ›

definition rel_typed :: "'a set ⇒ 'b set ⇒ ('a ↔ 'b) set" (infixr "↔" 55) where
"rel_typed A B = {R. Domain(R) ⊆ A ∧ Range(R) ⊆ B}" ― ‹ Relations ›

lemma rel_typed_intro: "⟦ Domain(R) ⊆ A; Range(R) ⊆ B ⟧ ⟹ R ∈ A ↔ B"
  by (simp add: rel_typed_def)

definition rel_pfun :: "'a set ⇒ 'b set ⇒ ('a ↔ 'b) set" (infixr "→⇩p" 55) where
"rel_pfun A B = {R. R ∈ A ↔ B ∧ functional R}" ― ‹ Partial Functions ›

lemma rel_pfun_intro: "⟦ R ∈ A ↔ B; functional R ⟧ ⟹ R ∈ A →⇩p B"
  by (simp add: rel_pfun_def)

definition rel_tfun :: "'a set ⇒ 'b set ⇒ ('a ↔ 'b) set" (infixr "→⇩t" 55) where
"rel_tfun A B = {R. R ∈ A →⇩p B ∧ left_totalr R}" ― ‹ Total Functions ›

definition rel_ffun :: "'a set ⇒ 'b set ⇒ ('a ↔ 'b) set" (infixr "→⇩f" 55) where
"rel_ffun A B = {R. R ∈ A →⇩p B ∧ finite(Domain R)}" ― ‹ Finite Functions ›

subsection ‹ Closure Properties ›

text ‹ These can be seen as typing rules for relational functions ›

named_theorems rclos

lemma rel_ffun_is_pfun [rclos]: "R ∈ rel_ffun A B ⟹ R ∈ A →⇩p B"
  by (simp add: rel_ffun_def)

lemma rel_tfun_is_pfun [rclos]: "R ∈ A →⇩t B ⟹ R ∈ A →⇩p B"
  by (simp add: rel_tfun_def)

lemma rel_pfun_is_typed [rclos]: "R ∈ A →⇩p B ⟹ R ∈ A ↔ B"
  by (simp add: rel_pfun_def)

lemma rel_ffun_empty [rclos]: "{} ∈ rel_ffun A B"
  by (simp add: rel_ffun_def rel_pfun_def rel_typed_def)

lemma rel_pfun_apply [rclos]: "⟦ x ∈ Domain(R); R ∈ A →⇩p B ⟧ ⟹ R(x)⇩r ∈ B"
  using functional_apply by (fastforce simp add: rel_pfun_def rel_typed_def)

lemma rel_tfun_apply [rclos]: "⟦ x ∈ A; R ∈ A →⇩t B ⟧ ⟹ R(x)⇩r ∈ B"
  by (metis (no_types, lifting) Domain_iff iso_tuple_UNIV_I left_totalr_on_def mem_Collect_eq rel_pfun_apply rel_tfun_def)

lemma rel_typed_insert [rclos]: "⟦ R ∈ A ↔ B; x ∈ A; y ∈ B ⟧ ⟹ insert (x, y) R ∈ A ↔ B"
  by (simp add: rel_typed_def)

lemma rel_pfun_insert [rclos]: "⟦ R ∈ A →⇩p B; x ∈ A; y ∈ B; x ∉ Domain(R) ⟧ ⟹ insert (x, y) R ∈ A →⇩p B"
  by (auto intro: rclos simp add: rel_pfun_def)

lemma rel_pfun_override [rclos]: "⟦ R ∈ A →⇩p B; S ∈ A →⇩p B ⟧ ⟹ (R ⊕ S) ∈ A →⇩p B"
  apply (rule rel_pfun_intro)
   apply (rule rel_typed_intro)
  apply (simp_all add: rel_pfun_def rel_typed_def, safe)
  apply (metis (no_types, opaque_lifting) Range.simps Range_Un_eq Range_rel_override Un_iff rev_subsetD)
  done

subsection ‹ Code Generation ›

lemma rel_conv_alist [code]: "(set xs)¯ = set (map (λ(x, y). (y, x)) xs)"
  by (induct xs, auto)

lemma rel_domres_alist [code]: "A ⊲⇩r set xs = set (AList.restrict A xs)"
  by (induct xs, simp_all, safe, simp_all)

lemma Image_alist [code]: "set xs `` A = set (map snd (AList.restrict A xs))"
  by (simp add: Image_as_rel_domres rel_domres_alist Range_snd)

lemma Collect_set: "{x ∈ set xs. P x} = set (filter P xs)"
  by auto

lemma single_valued_dom_alist [code]:
  "single_valued_dom (set xs) = set (filter (λx. length (remdups (map snd (AList.restrict {x} xs))) = 1) (map fst xs))"
  by (simp only: single_valued_dom_def set_map[THEN sym] Image_alist Domain_set set_singleton_iff list_singleton_iff Collect_set)

lemma AList_restrict_in_dom: "AList.restrict (set (filter P (map fst xs))) xs = filter (λ (x, y). P x) xs"
  by (auto intro: filter_cong simp add: Domain.intros fst_eq_Domain AList.restrict_eq)

lemma mk_functional_alist [code]:
  "mk_functional (set xs) = set (filter (λ (x,y). length (remdups (map snd (AList.restrict {x} xs))) = 1) xs)"
  by (simp only: mk_functional_single_valued_dom rel_domres_alist single_valued_dom_alist AList_restrict_in_dom)

lemma rel_apply_set [code]:
  "rel_apply (set xs) k = 
  (let ys = filter (λ (k', v). k = k') xs in
   if (length ys > 0 ∧ ys = replicate (length ys) (hd ys)) then snd (hd ys) else undefined)"
proof -
  let ?ys = "filter (λ(k', v). k = k') xs"
  have 1: "⟦ ?ys ≠ []; ?ys = replicate (length ?ys) (hd ?ys) ⟧ ⟹
          set xs(k)⇩r = snd (hd ?ys)"
  proof -
    assume ys: "?ys ≠ []" "?ys = replicate (length ?ys) (hd ?ys)"
    have kmem: "⋀ y. (k, y) ∈ set xs ⟷ (k, y) ∈ set ?ys"
      by simp
    from ys obtain v where v: "(k, v) ∈ set xs"
      using hd_in_set by fastforce
    hence ys':"?ys = replicate (length ?ys) (k, v)"
      by (metis (mono_tags) case_prodI filter_set in_set_replicate member_filter ys(2))
    hence "snd (hd ?ys) = v"
      by (metis hd_replicate replicate_0 snd_conv ys(1))
    moreover have "(THE y. (k, y) ∈ set xs) = v"
      by (metis (no_types, lifting) v in_set_replicate kmem snd_conv the_equality ys')
    moreover have "(∃!y. (k, y) ∈ set xs)"
      by (metis Pair_inject v in_set_replicate kmem ys')
    ultimately show "set xs(k)⇩r = snd (hd ?ys)"
      by (simp add: rel_apply_def)
  qed

  have 2: "?ys = [] ⟹ set xs(k)⇩r = undefined"
  proof -
    assume "filter (λ(k', v). k = k') xs = []" 
    hence "∄v. (k, v) ∈ set xs"
      by (metis (mono_tags, lifting) case_prodI filter_empty_conv)
    thus "set xs(k)⇩r = undefined"
      by (auto simp add: rel_apply_def)
  qed

  have 3: "?ys ≠ replicate (length ?ys) (hd ?ys) ⟹ set xs(k)⇩r = undefined"
  proof -
    assume ys: "?ys ≠ replicate (length ?ys) (hd ?ys)"
    have keys: "∀ (k', v') ∈ set ?ys. k' = k"
      by auto
    show "set xs(k)⇩r = undefined"
    proof (cases "length ?ys = 0")
      case True
      then show ?thesis
        using ys by fastforce
    next
      case False
      hence "length ?ys > 1"
        by (metis hd_in_set in_set_conv_nth length_0_conv less_one linorder_neqE_nat replicate_length_same ys)
      have "fst (hd ?ys) = k"
        using False hd_in_set by force
      have "¬(∀ (k, v) ∈ set ?ys. v = snd (hd ?ys))"
      proof 
        assume "(∀ (k, v) ∈ set ?ys. v = snd (hd ?ys))"
        hence "(∀ p ∈ set ?ys. p = (k, snd (hd ?ys)))"
          by fastforce
        hence "?ys = replicate (length ?ys) (hd ?ys)"
          by (metis False length_0_conv list.set_sel(1) replicate_length_same)
        thus False
          using ys by blast
      qed
      then obtain v where "(k, v) ∈ set ?ys" "v ≠ snd (hd ?ys)"
        by fastforce
      hence "(¬ (∃!y. (k, y) ∈ set xs))"
        using False list.set_sel(1) by fastforce
      then show ?thesis
        by (simp add: rel_apply_def)
    qed
  qed
  from 1 2 3 show ?thesis
    by (simp add: Let_unfold)
qed

end