# HG changeset patch
# User traytel
# Date 1656344186 -7200
# Node ID 0dd3ac5fdbaabeb1ac4300177bec452ce654f858
# Parent  22d1c5f2b9f4ae08d2b66f9062adbee5b8e83eef
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS

diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Jun 27 15:54:18 2022 +0200
+++ b/CONTRIBUTORS	Mon Jun 27 17:36:26 2022 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* June 2022: Jan van Brügge, TU München
+  Strict cardinality bounds for BNFs.
+
 * April - August 2021: Denis Paluca and Fabian Huch, TU München
   Various improvements to Isabelle/VSCode.
 
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa NEWS
--- a/NEWS	Mon Jun 27 15:54:18 2022 +0200
+++ b/NEWS	Mon Jun 27 17:36:26 2022 +0200
@@ -156,6 +156,8 @@
   - Added support for polymorphic "using" facts. Minor INCOMPATIBILITY.
 
 * (Co)datatype package:
+  - BNFs now require a strict cardinality bound (<o instead of \<le>o).
+    Minor INCOMPATIBILITY for existing manual BNF declarations.
   - Lemma map_ident_strong is now generated for all BNFs.
 
 * More ambitious minimization of case expressions in generated code.
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Jun 27 17:36:26 2022 +0200
@@ -2855,7 +2855,7 @@
     bnf "('d, 'a) fn"
       map: map_fn
       sets: set_fn
-      bd: "card_suc (natLeq +c |UNIV :: 'd set| )"
+      bd: "natLeq +c card_suc |UNIV :: 'd set|"
       rel: rel_fn
       pred: pred_fn
     proof -
@@ -2875,24 +2875,23 @@
       show "set_fn \<circ> map_fn f = (`) f \<circ> set_fn"
         by transfer (auto simp add: comp_def)
     next
-      show "card_order (card_suc (natLeq +c |UNIV :: 'd set| ))"
-        by (rule card_order_card_suc_natLeq_UNIV)
+      show "card_order (natLeq +c card_suc |UNIV :: 'd set| )"
+        by (rule card_order_bd_fun)
     next
-      show "cinfinite (card_suc (natLeq +c |UNIV :: 'd set| ))"
-        by (rule cinfinite_card_suc_natLeq_UNIV)
+      show "cinfinite (natLeq +c card_suc |UNIV :: 'd set| )"
+        by (rule Cinfinite_bd_fun[THEN conjunct1])
     next
-      show "regularCard (card_suc (natLeq +c |UNIV :: 'd set| ))"
-        by (rule regularCard_card_suc_natLeq_UNIV)
+      show "regularCard (natLeq +c card_suc |UNIV :: 'd set| )"
+        by (rule regularCard_bd_fun)
     next
       fix F :: "('d, 'a) fn"
       have "|set_fn F| \<le>o |UNIV :: 'd set|" (is "_ \<le>o ?U")
         by transfer (rule card_of_image)
-      also have "?U \<le>o natLeq +c ?U"
-        by (rule ordLeq_csum2) (rule card_of_Card_order)
-      finally have "|set_fn F| \<le>o natLeq +c |UNIV :: 'd set|" .
-      then show "|set_fn F| <o card_suc (natLeq +c |UNIV :: 'd set| )"
-        using ordLeq_ordLess_trans card_suc_greater card_order_csum natLeq_card_order
-          card_of_card_order_on by blast
+      also have "?U <o card_suc ?U"
+        by (simp add: card_of_card_order_on card_suc_greater)
+      also have "card_suc ?U \<le>o natLeq +c card_suc ?U"
+        using Card_order_card_suc card_of_card_order_on ordLeq_csum2 by blast
+      finally show "|set_fn F| <o natLeq +c card_suc |UNIV :: 'd set|" .
     next
       fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
       show "rel_fn R OO rel_fn S \<le> rel_fn (R OO S)"
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Jun 27 17:36:26 2022 +0200
@@ -817,24 +817,15 @@
 lemma Cinfinite_card_suc: "\<lbrakk> Cinfinite r ; card_order r \<rbrakk> \<Longrightarrow> Cinfinite (card_suc r)"
   using Cinfinite_cong[OF cardSuc_ordIso_card_suc Cinfinite_cardSuc] .
 
+lemma card_suc_least: "\<lbrakk>card_order r; Card_order s; r <o s\<rbrakk> \<Longrightarrow> card_suc r \<le>o s"
+  by (rule ordIso_ordLeq_trans[OF ordIso_symmetric[OF cardSuc_ordIso_card_suc]])
+    (auto intro!: cardSuc_least simp: card_order_on_Card_order)
+
 lemma regularCard_cardSuc: "Cinfinite k \<Longrightarrow> regularCard (cardSuc k)"
   by (rule infinite_cardSuc_regularCard) (auto simp: cinfinite_def)
 
-lemma regular_card_suc: "card_order r \<Longrightarrow> Cinfinite r \<Longrightarrow> regularCard (card_suc r)"
+lemma regularCard_card_suc: "card_order r \<Longrightarrow> Cinfinite r \<Longrightarrow> regularCard (card_suc r)"
   using cardSuc_ordIso_card_suc Cinfinite_cardSuc regularCard_cardSuc regularCard_ordIso
   by blast
 
-(* card_suc (natLeq +c |UNIV| ) *)
-
-lemma card_order_card_suc_natLeq_UNIV: "card_order (card_suc (natLeq +c |UNIV :: 'a set| ))"
-  using card_order_card_suc card_order_csum natLeq_card_order card_of_card_order_on by blast
-
-lemma cinfinite_card_suc_natLeq_UNIV: "cinfinite (card_suc (natLeq +c |UNIV :: 'a set| ))"
-  using Cinfinite_card_suc card_order_csum natLeq_card_order card_of_card_order_on natLeq_Cinfinite
-      Cinfinite_csum1 by blast
-
-lemma regularCard_card_suc_natLeq_UNIV: "regularCard (card_suc (natLeq +c |UNIV :: 'a set| ))"
-  using regular_card_suc card_order_csum natLeq_card_order card_of_card_order_on Cinfinite_csum1
-      natLeq_Cinfinite by blast
-
 end
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/HOL/Basic_BNFs.thy	Mon Jun 27 17:36:26 2022 +0200
@@ -2,7 +2,7 @@
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
-    Author:     Jan van Brügge
+    Author:     Jan van Brügge, TU Muenchen
     Copyright   2012, 2022
 
 Registration of basic types as bounded natural functors.
@@ -190,10 +190,56 @@
   by auto
 qed auto
 
+lemma card_order_bd_fun: "card_order (natLeq +c card_suc ( |UNIV| ))"
+  by (auto simp: card_order_csum natLeq_card_order card_order_card_suc card_of_card_order_on)
+
+lemma Cinfinite_bd_fun: "Cinfinite (natLeq +c card_suc ( |UNIV| ))"
+  by (auto simp: Cinfinite_csum natLeq_Cinfinite)
+
+lemma regularCard_bd_fun: "regularCard (natLeq +c card_suc ( |UNIV| ))"
+  (is "regularCard (_ +c card_suc ?U)")
+  apply (cases "Cinfinite ?U")
+   apply (rule regularCard_csum)
+      apply (rule natLeq_Cinfinite)
+     apply (rule Cinfinite_card_suc)
+      apply assumption
+     apply (rule card_of_card_order_on)
+    apply (rule regularCard_natLeq)
+   apply (rule regularCard_card_suc)
+    apply (rule card_of_card_order_on)
+   apply assumption
+  apply (rule regularCard_ordIso[of natLeq])
+    apply (rule csum_absorb1[THEN ordIso_symmetric])
+     apply (rule natLeq_Cinfinite)
+    apply (rule card_suc_least)
+      apply (rule card_of_card_order_on)
+     apply (rule natLeq_Card_order)
+    apply (subst finite_iff_ordLess_natLeq[symmetric])
+    apply (simp add: cinfinite_def Field_card_of card_of_card_order_on)
+   apply (rule natLeq_Cinfinite)
+  apply (rule regularCard_natLeq)
+  done
+
+lemma ordLess_bd_fun: "|UNIV::'a set| <o natLeq +c card_suc ( |UNIV::'a set| )"
+  (is "_ <o (_ +c card_suc (?U :: 'a rel))")
+proof (cases "Cinfinite ?U")
+  case True
+  have "?U <o card_suc ?U" using card_of_card_order_on natLeq_card_order card_suc_greater by blast
+  also have "card_suc ?U =o natLeq +c card_suc ?U" by (rule csum_absorb2[THEN ordIso_symmetric])
+    (auto simp: True card_of_card_order_on intro!: Cinfinite_card_suc natLeq_ordLeq_cinfinite)
+  finally show ?thesis .
+next
+  case False
+  then have "?U <o natLeq"
+    by (auto simp: cinfinite_def Field_card_of card_of_card_order_on finite_iff_ordLess_natLeq[symmetric])
+  then show ?thesis
+    by (rule ordLess_ordLeq_trans[OF _ ordLeq_csum1[OF natLeq_Card_order]])
+qed
+
 bnf "'a \<Rightarrow> 'b"
   map: "(\<circ>)"
   sets: range
-  bd: "card_suc (natLeq +c |UNIV::'a set|)"
+  bd: "natLeq +c card_suc ( |UNIV::'a set| )"
   rel: "rel_fun (=)"
   pred: "pred_fun (\<lambda>_. True)"
 proof
@@ -209,38 +255,18 @@
   fix f show "range \<circ> (\<circ>) f = (`) f \<circ> range"
     by (auto simp add: fun_eq_iff)
 next
-  show "card_order (card_suc (natLeq +c |UNIV|))"
-    apply (rule card_order_card_suc)
-    apply (rule card_order_csum)
-     apply (rule natLeq_card_order)
-    by (rule card_of_card_order_on)
+  show "card_order (natLeq +c card_suc ( |UNIV| ))"
+    by (rule card_order_bd_fun)
 next
-  have "Cinfinite (card_suc (natLeq +c |UNIV| ))"
-    apply (rule Cinfinite_card_suc)
-     apply (rule Cinfinite_csum)
-     apply (rule disjI1)
-     apply (rule natLeq_Cinfinite)
-    apply (rule card_order_csum)
-     apply (rule natLeq_card_order)
-    by (rule card_of_card_order_on)
-  then show "cinfinite (card_suc (natLeq +c |UNIV|))" by blast
+  show "cinfinite (natLeq +c card_suc ( |UNIV| ))"
+    by (rule Cinfinite_bd_fun[THEN conjunct1])
 next
-  show "regularCard (card_suc (natLeq +c |UNIV|))"
-    apply (rule regular_card_suc)
-     apply (rule card_order_csum)
-      apply (rule natLeq_card_order)
-     apply (rule card_of_card_order_on)
-    apply (rule Cinfinite_csum)
-    apply (rule disjI1)
-    by (rule natLeq_Cinfinite)
+  show "regularCard (natLeq +c card_suc ( |UNIV| ))"
+    by (rule regularCard_bd_fun)
 next
-  fix f :: "'d => 'a"
-  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
-  then have 1: "|range f| \<le>o natLeq +c ?U" using ordLeq_transitive ordLeq_csum2 card_of_Card_order by blast
-  have "natLeq +c ?U <o card_suc (natLeq +c ?U)" using card_of_card_order_on card_order_csum natLeq_card_order card_suc_greater by blast
-  then have "|range f| <o card_suc (natLeq +c ?U)" by (rule ordLeq_ordLess_trans[OF 1])
-  then show "|range f| <o card_suc (natLeq +c ?U)"
-    using ordLess_ordLeq_trans ordLeq_csum2 card_of_card_order_on Card_order_card_suc by blast
+  fix f :: "'d \<Rightarrow> 'a"
+  show "|range f| <o natLeq +c card_suc |UNIV :: 'd set|"
+    by (rule ordLeq_ordLess_trans[OF card_of_image ordLess_bd_fun])
 next
   fix R S
   show "rel_fun (=) R OO rel_fun (=) S \<le> rel_fun (=) (R OO S)" by (auto simp: rel_fun_def)
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/HOL/Cardinals/Bounded_Set.thy
--- a/src/HOL/Cardinals/Bounded_Set.thy	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/HOL/Cardinals/Bounded_Set.thy	Mon Jun 27 17:36:26 2022 +0200
@@ -74,7 +74,7 @@
 bnf "'a set['k]"
   map: map_bset
   sets: set_bset
-  bd: "card_suc (natLeq +c |UNIV :: 'k set| )"
+  bd: "natLeq +c card_suc |UNIV :: 'k set|"
   wits: bempty
   rel: rel_bset
 proof -
@@ -92,9 +92,8 @@
 next
   fix X :: "'a set['k]"
   have "|set_bset X| <o natLeq +c |UNIV :: 'k set|" by transfer blast
-  then show "|set_bset X| <o card_suc (natLeq +c |UNIV :: 'k set| )"
-    using card_suc_greater card_order_csum natLeq_card_order
-      card_of_card_order_on ordLess_transitive by blast
+  then show "|set_bset X| <o natLeq +c card_suc |UNIV :: 'k set|"
+    by (rule ordLess_ordLeq_trans[OF _ csum_mono2[OF ordLess_imp_ordLeq[OF card_suc_greater[OF card_of_card_order_on]]]])
 next
   fix R S
   show "rel_bset R OO rel_bset S \<le> rel_bset (R OO S)"
@@ -109,8 +108,7 @@
   fix x
   assume "x \<in> set_bset bempty"
   then show False by transfer simp
-qed (simp_all add: card_order_card_suc_natLeq_UNIV cinfinite_card_suc_natLeq_UNIV
-  regularCard_card_suc_natLeq_UNIV)
+qed (simp_all add: card_order_bd_fun Cinfinite_bd_fun regularCard_bd_fun)
 
 
 lemma map_bset_bempty[simp]: "map_bset f bempty = bempty"
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy	Mon Jun 27 17:36:26 2022 +0200
@@ -612,7 +612,7 @@
     by simp
 next
   show "regularCard (card_suc natLeq)" using natLeq_card_order natLeq_Cinfinite
-    by (rule regular_card_suc)
+    by (rule regularCard_card_suc)
 next
   fix C
   have "|rcset C| \<le>o natLeq" including cset.lifting by transfer (unfold countable_card_le_natLeq)
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Jun 27 17:36:26 2022 +0200
@@ -532,7 +532,7 @@
 
 lemma integrable_map_pmf_eq [simp]:
   fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
-  shows "integrable (map_pmf f p) g \<longleftrightarrow> integrable (measure_pmf p) (\<lambda>x. g (f x))"              
+  shows "integrable (map_pmf f p) g \<longleftrightarrow> integrable (measure_pmf p) (\<lambda>x. g (f x))"
   by (subst map_pmf_rep_eq, subst integrable_distr_eq) auto
 
 lemma integrable_map_pmf [intro]:
@@ -694,7 +694,7 @@
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   shows "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (fst x)) = measure_pmf.expectation p f"
 proof -
-  have "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (fst x)) = 
+  have "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (fst x)) =
           measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f" by simp
   also have "map_pmf fst (pair_pmf p q) = p"
     by (simp add: map_fst_pair_pmf)
@@ -705,7 +705,7 @@
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   shows "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (snd x)) = measure_pmf.expectation q f"
 proof -
-  have "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (snd x)) = 
+  have "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (snd x)) =
           measure_pmf.expectation (map_pmf snd (pair_pmf p q)) f" by simp
   also have "map_pmf snd (pair_pmf p q) = q"
     by (simp add: map_snd_pair_pmf)
@@ -1369,7 +1369,7 @@
   show "BNF_Cardinal_Arithmetic.cinfinite (card_suc natLeq)"
     using natLeq_Cinfinite natLeq_card_order Cinfinite_card_suc by blast
   show "regularCard (card_suc natLeq)" using natLeq_card_order natLeq_Cinfinite
-    by (rule regular_card_suc)
+    by (rule regularCard_card_suc)
 
   show "(card_of (set_pmf p), card_suc natLeq) \<in> ordLess" for p :: "'s pmf"
   proof -
@@ -2234,7 +2234,7 @@
     have "pmf (neg_binomial_pmf (Suc n) p) k =
             pmf (geometric_pmf p \<bind> (\<lambda>x. map_pmf ((+) x) (neg_binomial_pmf n p))) k"
       by (auto simp: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf neg_binomial_pmf_Suc)
-    also have "\<dots> = measure_pmf.expectation (geometric_pmf p) 
+    also have "\<dots> = measure_pmf.expectation (geometric_pmf p)
                       (\<lambda>x. measure_pmf.prob (neg_binomial_pmf n p) ((+) x -` {k}))"
       by (simp add: pmf_bind pmf_map)
     also have "(\<lambda>x. (+) x -` {k}) = (\<lambda>x. if x \<le> k then {k - x} else {})"
@@ -2257,7 +2257,7 @@
       finally show ?case by simp
     qed
     also have "(\<Sum>i\<le>k. (k - i + n - 1) choose (k - i)) = (\<Sum>i\<le>k. (n - 1 + i) choose i)"
-      by (intro sum.reindex_bij_witness[of _ "\<lambda>i. k - i" "\<lambda>i. k - i"]) 
+      by (intro sum.reindex_bij_witness[of _ "\<lambda>i. k - i" "\<lambda>i. k - i"])
          (use \<open>n \<noteq> 0\<close> in \<open>auto simp: algebra_simps\<close>)
     also have "\<dots> = (n + k) choose k"
       by (subst sum_choose_lower) (use \<open>n \<noteq> 0\<close> in auto)
@@ -2332,7 +2332,7 @@
     by auto
   thus ?thesis
     using prob_neg_binomial_pmf_atMost[OF p, of n "k - 1"] False by simp
-qed auto  
+qed auto
 
 text \<open>
   The expected value of the negative binomial distribution is $n(1-p)/p$:
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/HOL/Tools/BNF/bnf_comp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Jun 27 17:36:26 2022 +0200
@@ -131,14 +131,16 @@
   rtac ctxt @{thm regularCard_natLeq} 1 ORELSE
   EVERY1 [
     rtac ctxt @{thm regularCard_cprod},
-    TRY o rtac ctxt @{thm Cinfinite_csum1},
-    resolve_tac ctxt Fbd_Cinfinites,
+    resolve_tac ctxt (Fbd_Cinfinites) ORELSE'
+    ((TRY o rtac ctxt @{thm Cinfinite_csum1}) THEN'
+    resolve_tac ctxt (Fbd_Cinfinites)),
     rtac ctxt Gbd_Cinfinite,
     REPEAT_DETERM o EVERY' [
       rtac ctxt @{thm regularCard_csum},
       resolve_tac ctxt Fbd_Cinfinites,
-      TRY o rtac ctxt @{thm Cinfinite_csum1},
-      resolve_tac ctxt Fbd_Cinfinites,
+      resolve_tac ctxt (Fbd_Cinfinites) ORELSE'
+      ((TRY o rtac ctxt @{thm Cinfinite_csum1}) THEN'
+      resolve_tac ctxt (Fbd_Cinfinites)),
       resolve_tac ctxt Fbd_regularCards
     ],
     resolve_tac ctxt Fbd_regularCards,
diff -r 22d1c5f2b9f4 -r 0dd3ac5fdbaa src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jun 27 15:54:18 2022 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jun 27 17:36:26 2022 +0200
@@ -806,7 +806,7 @@
     val sbd_card_order = @{thm card_order_card_suc} OF [sbd_card_order'];
     val sbd_Cinfinite = @{thm Cinfinite_card_suc} OF [sbd_Cinfinite', sbd_card_order'];
     val sbd_Card_order = @{thm Card_order_card_suc} OF [sbd_card_order'];
-    val sbd_regularCard = @{thm regular_card_suc} OF [sbd_card_order', sbd_Cinfinite'];
+    val sbd_regularCard = @{thm regularCard_card_suc} OF [sbd_card_order', sbd_Cinfinite'];
     val set_sbdss = map (map (fn thm => @{thm ordLess_transitive} OF [
       thm, @{thm card_suc_greater} OF [sbd_card_order']
     ])) set_sbdss';