<commit_before>(*  Title:      HOL/Library/Executable_Set.thy
    Author:     <NAME>, <NAME>
*)

header {* Implementation of finite sets by lists *}

theory Executable_Set
imports Main Code_Set
begin

subsection {* Derived set operations *}

declare member [code] 

definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
  "subset = op \<le>"

declare subset_def [symmetric, code unfold]

lemma [code]:
  "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
  by (simp add: subset_def subset_eq)

definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
  [code del]: "eq_set = op ="

(* FIXME allow for Stefan's code generator:
declare set_eq_subset[code unfold]
*)

lemma [code]:
  "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
  by (simp add: eq_set_def set_eq)

declare inter [code]

declare Inter_image_eq [symmetric, code]
declare Union_image_eq [symmetric, code]


subsection {* Rewrites for primitive operations *}

declare List_Set.project_def [symmetric, code unfold]


subsection {* code generator setup *}

text {* eliminate popular infixes *}

ML {*
nonfix inter;
nonfix union;
nonfix subset;
*}

text {* type @{typ "'a fset"} *}

types_code
  fset ("(_/ list)")

consts_code
  Set ("_")

text {* primitive operations *}

definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
  "flip f a b = f b a"

consts_code
  "Set.empty"         ("{*Code_Set.empty*}")
  "List_Set.is_empty" ("{*Code_Set.is_empty*}")
  "Set.insert"        ("{*Code_Set.insert*}")
  "List_Set.remove"   ("{*Code_Set.remove*}")
  "Set.image"         ("{*Code_Set.map*}")
  "List_Set.project"  ("{*Code_Set.filter*}")
  "Ball"              ("{*flip Code_Set.forall*}")
  "Bex"               ("{*flip Code_Set.exists*}")
  "op \<union>"              ("{*Code_Set.union*}")
  "op \<inter>"              ("{*Code_Set.inter*}")
  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip subtract*}")
  "Set.Union"         ("{*Code_Set.union*}")
  "Set.Inter"         ("{*Code_Set.inter*}")
  fold                ("{*foldl o flip*}")

end<commit_msg>Executable_Set is now a simple wrapper around Fset<commit_after>(*  Title:      HOL/Library/Executable_Set.thy
    Author:     <NAME>, <NAME>
*)

header {* Implementation of finite sets by lists *}

theory Executable_Set
imports Main Fset
begin

subsection {* Derived set operations *}

declare member [code] 

definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
  "subset = op \<le>"

declare subset_def [symmetric, code unfold]

lemma [code]:
  "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
  by (simp add: subset_def subset_eq)

definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
  [code del]: "eq_set = op ="

(* FIXME allow for Stefan's code generator:
declare set_eq_subset[code unfold]
*)

lemma [code]:
  "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
  by (simp add: eq_set_def set_eq)

declare inter [code]

declare Inter_image_eq [symmetric, code]
declare Union_image_eq [symmetric, code]


subsection {* Rewrites for primitive operations *}

declare List_Set.project_def [symmetric, code unfold]


subsection {* code generator setup *}

ML {*
nonfix inter;
nonfix union;
nonfix subset;
*}

definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
  "flip f a b = f b a"

types_code
  fset ("(_/ \<module>fset)")
attach {*
datatype 'a fset = Set of 'a list;
*}

consts_code
  Set ("\<module>Set")

consts_code
  "Set.empty"         ("{*Fset.empty*}")
  "List_Set.is_empty" ("{*Fset.is_empty*}")
  "Set.insert"        ("{*Fset.insert*}")
  "List_Set.remove"   ("{*Fset.remove*}")
  "Set.image"         ("{*Fset.map*}")
  "List_Set.project"  ("{*Fset.filter*}")
  "Ball"              ("{*flip Fset.forall*}")
  "Bex"               ("{*flip Fset.exists*}")
  "op \<union>"              ("{*Fset.union*}")
  "op \<inter>"              ("{*Fset.inter*}")
  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
  "Set.Union"         ("{*Fset.Union*}")
  "Set.Inter"         ("{*Fset.Inter*}")
  card                ("{*Fset.card*}")
  fold                ("{*foldl o flip*}")

end
{'fraction_non_alphanumeric': 0.1759450171821306, 'fraction_numerical': 0.0, 'mean_word_length': 3.3529411764705883, 'pattern_counts': {'":': 0, '<': 55, '<?xml version=': 0, '>': 55, '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': '2868447', 'n_tokens_mistral': 1674, 'n_tokens_neox': 1537, 'n_words': 437}