<commit_before>(*  Title:      HOL/Quotient_Examples/FSet.thy
    Author:     <NAME>, TU Munich
    Author:     <NAME>, TU Munich

Type of finite sets.
*)

theory FSet
imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
begin

text {* 
  The type of finite sets is created by a quotient construction
  over lists. The definition of the equivalence:
*}

definition
  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
where
  [simp]: "xs \<approx> ys \<longleftrightarrow> set xs = set ys"

lemma list_eq_reflp:
  "reflp list_eq"
  by (auto intro: reflpI)

lemma list_eq_symp:
  "symp list_eq"
  by (auto intro: sympI)

lemma list_eq_transp:
  "transp list_eq"
  by (auto intro: transpI)

lemma list_eq_equivp:
  "equivp list_eq"
  by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp)

text {* The @{text fset} type *}

quotient_type
  'a fset = "'a list" / "list_eq"
  by (rule list_eq_equivp)

text {* 
  Definitions for sublist, cardinality, 
  intersection, difference and respectful fold over 
  lists.
*}

declare List.member_def [simp]

definition
  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where 
  [simp]: "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys"

definition
  card_list :: "'a list \<Rightarrow> nat"
where
  [simp]: "card_list xs = card (set xs)"

definition
  inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"

definition
  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"

definition
  rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
where
  "rsp_fold f \<longleftrightarrow> (\<forall>u v. f u \<circ> f v = f v \<circ> f u)"

lemma rsp_foldI:
  "(\<And>u v. f u \<circ> f v = f v \<circ> f u) \<Longrightarrow> rsp_fold f"
  by (simp add: rsp_fold_def)

lemma rsp_foldE:
  assumes "rsp_fold f"
  obtains "f u \<circ> f v = f v \<circ> f u"
  using assms by (simp add: rsp_fold_def)

definition
  fold_once :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
where
  "fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)"

lemma fold_once_default [simp]:
  "\<not> rsp_fold f \<Longrightarrow> fold_once f xs = id"
  by (simp add: fold_once_def)

lemma fold_once_fold_remdups:
  "rsp_fold f \<Longrightarrow> fold_once f xs = fold f (remdups xs)"
  by (simp add: fold_once_def)


section {* Quotient composition lemmas *}

lemma list_all2_refl':
  assumes q: "equivp R"
  shows "(list_all2 R) r r"
  by (rule list_all2_refl) (metis equivp_def q)

lemma compose_list_refl:
  assumes q: "equivp R"
  shows "(list_all2 R OOO op \<approx>) r r"
proof
  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
  show "list_all2 R r r" by (rule list_all2_refl'[OF q])
  with * show "(op \<approx> OO list_all2 R) r r" ..
qed

lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
  by (simp only: list_eq_def set_map)

lemma quotient_compose_list_g:
  assumes q: "Quotient R Abs Rep"
  and     e: "equivp R"
  shows  "Quotient ((list_all2 R) OOO (op \<approx>))
    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
  unfolding Quotient_def comp_def
proof (intro conjI allI)
  fix a r s
  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule list_all2_refl'[OF e])
  have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
  show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule, rule list_all2_refl'[OF e]) (rule c)
  show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
        (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
  proof (intro iffI conjI)
    show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e])
    show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e])
  next
    assume a: "(list_all2 R OOO op \<approx>) r s"
    then have b: "map Abs r \<approx> map Abs s"
    proof (elim pred_compE)
      fix b ba
      assume c: "list_all2 R r b"
      assume d: "b \<approx> ba"
      assume e: "list_all2 R ba s"
      have f: "map Abs r = map Abs b"
        using Quotient_rel[OF list_quotient[OF q]] c by blast
      have "map Abs ba = map Abs s"
        using Quotient_rel[OF list_quotient[OF q]] e by blast
      then have g: "map Abs s = map Abs ba" by simp
      then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
    qed
    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
      using Quotient_rel[OF Quotient_fset] by blast
  next
    assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
    then have s: "(list_all2 R OOO op \<approx>) s s" by simp
    have d: "map Abs r \<approx> map Abs s"
      by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
      by (rule map_list_eq_cong[OF d])
    have y: "list_all2 R (map Rep (map Abs s)) s"
      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
    have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
      by (rule pred_compI) (rule b, rule y)
    have z: "list_all2 R r (map Rep (map Abs r))"
      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
    then show "(list_all2 R OOO op \<approx>) r s"
      using a c pred_compI by simp
  qed
qed

lemma quotient_compose_list[quot_thm]:
  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
  by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)



subsection {* Respectfulness lemmas for list operations *}

lemma list_equiv_rsp [quot_respect]:
  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
  by (auto intro!: fun_relI)

lemma append_rsp [quot_respect]:
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
  by (auto intro!: fun_relI)

lemma sub_list_rsp [quot_respect]:
  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
  by (auto intro!: fun_relI)

lemma member_rsp [quot_respect]:
  shows "(op \<approx> ===> op =) List.member List.member"
  by (auto intro!: fun_relI simp add: mem_def)

lemma nil_rsp [quot_respect]:
  shows "(op \<approx>) Nil Nil"
  by simp

lemma cons_rsp [quot_respect]:
  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
  by (auto intro!: fun_relI)

lemma map_rsp [quot_respect]:
  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
  by (auto intro!: fun_relI)

lemma set_rsp [quot_respect]:
  "(op \<approx> ===> op =) set set"
  by (auto intro!: fun_relI)<commit_msg>FSet: Explicit proof without mem_def<commit_after>(*  Title:      HOL/Quotient_Examples/FSet.thy
    Author:     <NAME>, TU Munich
    Author:     <NAME>, TU Munich

Type of finite sets.
*)

theory FSet
imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
begin

text {* 
  The type of finite sets is created by a quotient construction
  over lists. The definition of the equivalence:
*}

definition
  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
where
  [simp]: "xs \<approx> ys \<longleftrightarrow> set xs = set ys"

lemma list_eq_reflp:
  "reflp list_eq"
  by (auto intro: reflpI)

lemma list_eq_symp:
  "symp list_eq"
  by (auto intro: sympI)

lemma list_eq_transp:
  "transp list_eq"
  by (auto intro: transpI)

lemma list_eq_equivp:
  "equivp list_eq"
  by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp)

text {* The @{text fset} type *}

quotient_type
  'a fset = "'a list" / "list_eq"
  by (rule list_eq_equivp)

text {* 
  Definitions for sublist, cardinality, 
  intersection, difference and respectful fold over 
  lists.
*}

declare List.member_def [simp]

definition
  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where 
  [simp]: "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys"

definition
  card_list :: "'a list \<Rightarrow> nat"
where
  [simp]: "card_list xs = card (set xs)"

definition
  inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"

definition
  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"

definition
  rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
where
  "rsp_fold f \<longleftrightarrow> (\<forall>u v. f u \<circ> f v = f v \<circ> f u)"

lemma rsp_foldI:
  "(\<And>u v. f u \<circ> f v = f v \<circ> f u) \<Longrightarrow> rsp_fold f"
  by (simp add: rsp_fold_def)

lemma rsp_foldE:
  assumes "rsp_fold f"
  obtains "f u \<circ> f v = f v \<circ> f u"
  using assms by (simp add: rsp_fold_def)

definition
  fold_once :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
where
  "fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)"

lemma fold_once_default [simp]:
  "\<not> rsp_fold f \<Longrightarrow> fold_once f xs = id"
  by (simp add: fold_once_def)

lemma fold_once_fold_remdups:
  "rsp_fold f \<Longrightarrow> fold_once f xs = fold f (remdups xs)"
  by (simp add: fold_once_def)


section {* Quotient composition lemmas *}

lemma list_all2_refl':
  assumes q: "equivp R"
  shows "(list_all2 R) r r"
  by (rule list_all2_refl) (metis equivp_def q)

lemma compose_list_refl:
  assumes q: "equivp R"
  shows "(list_all2 R OOO op \<approx>) r r"
proof
  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
  show "list_all2 R r r" by (rule list_all2_refl'[OF q])
  with * show "(op \<approx> OO list_all2 R) r r" ..
qed

lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
  by (simp only: list_eq_def set_map)

lemma quotient_compose_list_g:
  assumes q: "Quotient R Abs Rep"
  and     e: "equivp R"
  shows  "Quotient ((list_all2 R) OOO (op \<approx>))
    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
  unfolding Quotient_def comp_def
proof (intro conjI allI)
  fix a r s
  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule list_all2_refl'[OF e])
  have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
  show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule, rule list_all2_refl'[OF e]) (rule c)
  show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
        (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
  proof (intro iffI conjI)
    show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e])
    show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e])
  next
    assume a: "(list_all2 R OOO op \<approx>) r s"
    then have b: "map Abs r \<approx> map Abs s"
    proof (elim pred_compE)
      fix b ba
      assume c: "list_all2 R r b"
      assume d: "b \<approx> ba"
      assume e: "list_all2 R ba s"
      have f: "map Abs r = map Abs b"
        using Quotient_rel[OF list_quotient[OF q]] c by blast
      have "map Abs ba = map Abs s"
        using Quotient_rel[OF list_quotient[OF q]] e by blast
      then have g: "map Abs s = map Abs ba" by simp
      then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
    qed
    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
      using Quotient_rel[OF Quotient_fset] by blast
  next
    assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
    then have s: "(list_all2 R OOO op \<approx>) s s" by simp
    have d: "map Abs r \<approx> map Abs s"
      by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
      by (rule map_list_eq_cong[OF d])
    have y: "list_all2 R (map Rep (map Abs s)) s"
      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
    have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
      by (rule pred_compI) (rule b, rule y)
    have z: "list_all2 R r (map Rep (map Abs r))"
      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
    then show "(list_all2 R OOO op \<approx>) r s"
      using a c pred_compI by simp
  qed
qed

lemma quotient_compose_list[quot_thm]:
  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
  by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)



subsection {* Respectfulness lemmas for list operations *}

lemma list_equiv_rsp [quot_respect]:
  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
  by (auto intro!: fun_relI)

lemma append_rsp [quot_respect]:
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
  by (auto intro!: fun_relI)

lemma sub_list_rsp [quot_respect]:
  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
  by (auto intro!: fun_relI)

lemma member_rsp [quot_respect]:
  shows "(op \<approx> ===> op =) List.member List.member"
proof
  fix x y assume "x \<approx> y"
  then show "List.member x = List.member y"
    unfolding fun_eq_iff by simp
qed

lemma nil_rsp [quot_respect]:
  shows "(op \<approx>) Nil Nil"
  by simp

lemma cons_rsp [quot_respect]:
  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
  by (auto intro!: fun_relI)

lemma map_rsp [quot_respect]:
  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
  by (auto intro!: fun_relI)

lemma set_rsp [quot_respect]:
  "(op \<approx> ===> op =) set set"
  by (auto intro!: fun_relI)
{'fraction_non_alphanumeric': 0.13799699412488045, 'fraction_numerical': 0.004508812679327777, 'mean_word_length': 3.50569405971068, 'pattern_counts': {'":': 0, '<': 192, '<?xml version=': 0, '>': 216, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '504377', 'n_tokens_mistral': 5998, 'n_tokens_neox': 5718, 'n_words': 2019}