# HG changeset patch
# User Andreas Lochbihler <mail@andreas-lochbihler.de>
# Date 1624903823 -7200
# Node ID 93ba8e3fdcdfe07bcf9ca8d12ded5225d030b8e6
# Parent  0a12ca4f3e8d5345f6c96803ef828aa364076bbf
move code setup from Cardinality to separate theory

diff -r 0a12ca4f3e8d -r 93ba8e3fdcdf NEWS
--- a/NEWS	Sat Jun 26 20:55:43 2021 +0200
+++ b/NEWS	Mon Jun 28 20:10:23 2021 +0200
@@ -133,6 +133,13 @@
 operations has been adjusted to match the corresponding precendences on
 sets. Rare INCOMPATIBILITY.
 
+* Theory "HOL-Library.Cardinality": code generator setup based on the
+type classes finite_UNIV and card_UNIV has been moved to
+"HOL-Library.Code_Cardinality", to avoid incompatibilities with
+other code setups for sets in AFP/Containers. Applications relying on
+this code setup should import "HOL-Library.Code_Cardinality". Minor
+INCOMPATIBILITY.
+
 * Session "HOL-Analysis" and "HOL-Probability": indexed products of
 discrete distributions, negative binomial distribution, Hoeffding's
 inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
diff -r 0a12ca4f3e8d -r 93ba8e3fdcdf src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jun 28 20:10:23 2021 +0200
@@ -21,10 +21,10 @@
   "Sup :: _ Predicate.pred set \<Rightarrow> _"
   pred_of_set
   Wellfounded.acc
-  Cardinality.card'
-  Cardinality.finite'
-  Cardinality.subset'
-  Cardinality.eq_set
+  Code_Cardinality.card'
+  Code_Cardinality.finite'
+  Code_Cardinality.subset'
+  Code_Cardinality.eq_set
   Euclidean_Algorithm.Gcd
   Euclidean_Algorithm.Lcm
   "Gcd :: _ poly set \<Rightarrow> _"
diff -r 0a12ca4f3e8d -r 93ba8e3fdcdf src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Library/Cardinality.thy	Mon Jun 28 20:10:23 2021 +0200
@@ -387,147 +387,4 @@
   by intro_classes (simp_all add: UNIV_finite_5 card_UNIV_finite_5_def finite_UNIV_finite_5_def)
 end
 
-subsection \<open>Code setup for sets\<close>
-
-text \<open>
-  Implement \<^term>\<open>CARD('a)\<close> via \<^term>\<open>card_UNIV\<close> and provide
-  implementations for \<^term>\<open>finite\<close>, \<^term>\<open>card\<close>, \<^term>\<open>(\<subseteq>)\<close>, 
-  and \<^term>\<open>(=)\<close>if the calling context already provides \<^class>\<open>finite_UNIV\<close>
-  and \<^class>\<open>card_UNIV\<close> instances. If we implemented the latter
-  always via \<^term>\<open>card_UNIV\<close>, we would require instances of essentially all 
-  element types, i.e., a lot of instantiation proofs and -- at run time --
-  possibly slow dictionary constructions.
-\<close>
-
-context
-begin
-
-qualified definition card_UNIV' :: "'a card_UNIV"
-where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
-
-lemma CARD_code [code_unfold]:
-  "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)"
-by(simp add: card_UNIV'_def)
-
-lemma card_UNIV'_code [code]:
-  "card_UNIV' = card_UNIV"
-by(simp add: card_UNIV card_UNIV'_def)
-
 end
-
-lemma card_Compl:
-  "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
-by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
-
-context fixes xs :: "'a :: finite_UNIV list"
-begin
-
-qualified definition finite' :: "'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "finite' = finite"
-
-lemma finite'_code [code]:
-  "finite' (set xs) \<longleftrightarrow> True"
-  "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
-by(simp_all add: card_gt_0_iff finite_UNIV)
-
-end
-
-context fixes xs :: "'a :: card_UNIV list"
-begin
-
-qualified definition card' :: "'a set \<Rightarrow> nat" 
-where [simp, code del, code_abbrev]: "card' = card"
- 
-lemma card'_code [code]:
-  "card' (set xs) = length (remdups xs)"
-  "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
-by(simp_all add: List.card_set card_Compl card_UNIV)
-
-
-qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "subset' = (\<subseteq>)"
-
-lemma subset'_code [code]:
-  "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
-  "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
-  "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
-by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
-  (metis finite_compl finite_set rev_finite_subset)
-
-qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "eq_set = (=)"
-
-lemma eq_set_code [code]:
-  fixes ys
-  defines "rhs \<equiv> 
-  let n = CARD('a)
-  in if n = 0 then False else 
-        let xs' = remdups xs; ys' = remdups ys 
-        in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
-  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs"
-  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
-  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
-  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
-proof goal_cases
-  {
-    case 1
-    show ?case (is "?lhs \<longleftrightarrow> ?rhs")
-    proof
-      show ?rhs if ?lhs
-        using that
-        by (auto simp add: rhs_def Let_def List.card_set[symmetric]
-          card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV
-          Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
-      show ?lhs if ?rhs
-      proof - 
-        have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
-        with that show ?thesis
-          by (auto simp add: rhs_def Let_def List.card_set[symmetric]
-            card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
-            dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm)
-      qed
-    qed
-  }
-  moreover
-  case 2
-  ultimately show ?case unfolding eq_set_def by blast
-next
-  case 3
-  show ?case unfolding eq_set_def List.coset_def by blast
-next
-  case 4
-  show ?case unfolding eq_set_def List.coset_def by blast
-qed
-
-end
-
-text \<open>
-  Provide more informative exceptions than Match for non-rewritten cases.
-  If generated code raises one these exceptions, then a code equation calls
-  the mentioned operator for an element type that is not an instance of
-  \<^class>\<open>card_UNIV\<close> and is therefore not implemented via \<^term>\<open>card_UNIV\<close>.
-  Constrain the element type with sort \<^class>\<open>card_UNIV\<close> to change this.
-\<close>
-
-lemma card_coset_error [code]:
-  "card (List.coset xs) = 
-   Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'')
-     (\<lambda>_. card (List.coset xs))"
-by(simp)
-
-lemma coset_subseteq_set_code [code]:
-  "List.coset xs \<subseteq> set ys \<longleftrightarrow> 
-  (if xs = [] \<and> ys = [] then False 
-   else Code.abort
-     (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'')
-     (\<lambda>_. List.coset xs \<subseteq> set ys))"
-by simp
-
-notepad begin \<comment> \<open>test code setup\<close>
-have "List.coset [True] = set [False] \<and> 
-      List.coset [] \<subseteq> List.set [True, False] \<and> 
-      finite (List.coset [True])"
-  by eval
-end
-
-end
diff -r 0a12ca4f3e8d -r 93ba8e3fdcdf src/HOL/Library/Code_Cardinality.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Cardinality.thy	Mon Jun 28 20:10:23 2021 +0200
@@ -0,0 +1,147 @@
+subsection \<open>Code setup for sets with cardinality type information\<close>
+
+theory Code_Cardinality imports Cardinality begin
+
+text \<open>
+  Implement \<^term>\<open>CARD('a)\<close> via \<^term>\<open>card_UNIV\<close> and provide
+  implementations for \<^term>\<open>finite\<close>, \<^term>\<open>card\<close>, \<^term>\<open>(\<subseteq>)\<close>, 
+  and \<^term>\<open>(=)\<close>if the calling context already provides \<^class>\<open>finite_UNIV\<close>
+  and \<^class>\<open>card_UNIV\<close> instances. If we implemented the latter
+  always via \<^term>\<open>card_UNIV\<close>, we would require instances of essentially all 
+  element types, i.e., a lot of instantiation proofs and -- at run time --
+  possibly slow dictionary constructions.
+\<close>
+
+context
+begin
+
+qualified definition card_UNIV' :: "'a card_UNIV"
+where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
+
+lemma CARD_code [code_unfold]:
+  "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)"
+by(simp add: card_UNIV'_def)
+
+lemma card_UNIV'_code [code]:
+  "card_UNIV' = card_UNIV"
+by(simp add: card_UNIV card_UNIV'_def)
+
+end
+
+lemma card_Compl:
+  "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
+by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
+
+context fixes xs :: "'a :: finite_UNIV list"
+begin
+
+qualified definition finite' :: "'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "finite' = finite"
+
+lemma finite'_code [code]:
+  "finite' (set xs) \<longleftrightarrow> True"
+  "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
+by(simp_all add: card_gt_0_iff finite_UNIV)
+
+end
+
+context fixes xs :: "'a :: card_UNIV list"
+begin
+
+qualified definition card' :: "'a set \<Rightarrow> nat" 
+where [simp, code del, code_abbrev]: "card' = card"
+ 
+lemma card'_code [code]:
+  "card' (set xs) = length (remdups xs)"
+  "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
+by(simp_all add: List.card_set card_Compl card_UNIV)
+
+
+qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "subset' = (\<subseteq>)"
+
+lemma subset'_code [code]:
+  "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
+  "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
+  "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
+by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
+  (metis finite_compl finite_set rev_finite_subset)
+
+qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "eq_set = (=)"
+
+lemma eq_set_code [code]:
+  fixes ys
+  defines "rhs \<equiv> 
+  let n = CARD('a)
+  in if n = 0 then False else 
+        let xs' = remdups xs; ys' = remdups ys 
+        in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
+  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs"
+  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
+  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
+  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
+proof goal_cases
+  {
+    case 1
+    show ?case (is "?lhs \<longleftrightarrow> ?rhs")
+    proof
+      show ?rhs if ?lhs
+        using that
+        by (auto simp add: rhs_def Let_def List.card_set[symmetric]
+          card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV
+          Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
+      show ?lhs if ?rhs
+      proof - 
+        have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
+        with that show ?thesis
+          by (auto simp add: rhs_def Let_def List.card_set[symmetric]
+            card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
+            dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm)
+      qed
+    qed
+  }
+  moreover
+  case 2
+  ultimately show ?case unfolding eq_set_def by blast
+next
+  case 3
+  show ?case unfolding eq_set_def List.coset_def by blast
+next
+  case 4
+  show ?case unfolding eq_set_def List.coset_def by blast
+qed
+
+end
+
+text \<open>
+  Provide more informative exceptions than Match for non-rewritten cases.
+  If generated code raises one these exceptions, then a code equation calls
+  the mentioned operator for an element type that is not an instance of
+  \<^class>\<open>card_UNIV\<close> and is therefore not implemented via \<^term>\<open>card_UNIV\<close>.
+  Constrain the element type with sort \<^class>\<open>card_UNIV\<close> to change this.
+\<close>
+
+lemma card_coset_error [code]:
+  "card (List.coset xs) = 
+   Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'')
+     (\<lambda>_. card (List.coset xs))"
+by(simp)
+
+lemma coset_subseteq_set_code [code]:
+  "List.coset xs \<subseteq> set ys \<longleftrightarrow> 
+  (if xs = [] \<and> ys = [] then False 
+   else Code.abort
+     (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'')
+     (\<lambda>_. List.coset xs \<subseteq> set ys))"
+by simp
+
+notepad begin \<comment> \<open>test code setup\<close>
+have "List.coset [True] = set [False] \<and> 
+      List.coset [] \<subseteq> List.set [True, False] \<and> 
+      finite (List.coset [True])"
+  by eval
+
+end
+
+end
\ No newline at end of file
diff -r 0a12ca4f3e8d -r 93ba8e3fdcdf src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Library/Library.thy	Mon Jun 28 20:10:23 2021 +0200
@@ -10,6 +10,7 @@
   Boolean_Algebra
   Bourbaki_Witt_Fixpoint
   Char_ord
+  Code_Cardinality
   Code_Lazy
   Code_Test
   Combine_PER