--- 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.
--- 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.
--- 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)"
--- 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
--- 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)
--- 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"
--- 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)
--- 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$:
--- 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,
--- 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';