--- a/src/Doc/Datatypes/Datatypes.thy Sun Apr 07 12:44:37 2019 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Sun Apr 07 08:26:57 2019 +0200
@@ -13,12 +13,16 @@
imports
Setup
"HOL-Library.BNF_Axiomatization"
- "HOL-Library.Cardinal_Notations"
"HOL-Library.Countable"
"HOL-Library.FSet"
"HOL-Library.Simps_Case_Conv"
begin
+
+(*<*)
+unbundle cardinal_syntax
+(*>*)
+
section \<open>Introduction
\label{sec:introduction}\<close>
@@ -2761,8 +2765,8 @@
text \<open>
The example below shows how to register a type as a BNF using the @{command bnf}
-command. Some of the proof obligations are best viewed with the theory
-\<^file>\<open>~~/src/HOL/Library/Cardinal_Notations.thy\<close> imported.
+command. Some of the proof obligations are best viewed with the bundle
+"cardinal_syntax" included.
The type is simply a copy of the function space \<^typ>\<open>'d \<Rightarrow> 'a\<close>, where \<^typ>\<open>'a\<close>
is live and \<^typ>\<open>'d\<close> is dead. We introduce it together with its map function,
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Sun Apr 07 12:44:37 2019 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Sun Apr 07 08:26:57 2019 +0200
@@ -10,9 +10,10 @@
theory Wellorder_Constructions
imports
Wellorder_Embedding Order_Union
- "HOL-Library.Cardinal_Notations"
begin
+unbundle cardinal_syntax
+
declare
ordLeq_Well_order_simp[simp]
not_ordLeq_iff_ordLess[simp]
--- a/src/HOL/Library/Cardinal_Notations.thy Sun Apr 07 12:44:37 2019 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: HOL/Library/Cardinal_Notations.thy
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2013
-
-Cardinal notations.
-*)
-
-section \<open>Cardinal Notations\<close>
-
-theory Cardinal_Notations
-imports Main
-begin
-
-notation
- ordLeq2 (infix "<=o" 50) and
- ordLeq3 (infix "\<le>o" 50) and
- ordLess2 (infix "<o" 50) and
- ordIso2 (infix "=o" 50) and
- card_of ("|_|") and
- BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
- BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
- BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
-
-abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
-abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
-abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
-abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"
-
-end
--- a/src/HOL/Library/Countable_Set_Type.thy Sun Apr 07 12:44:37 2019 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy Sun Apr 07 08:26:57 2019 +0200
@@ -9,12 +9,16 @@
section \<open>Type of (at Most) Countable Sets\<close>
theory Countable_Set_Type
-imports Countable_Set Cardinal_Notations
+imports Countable_Set
begin
subsection\<open>Cardinal stuff\<close>
+context
+ includes cardinal_syntax
+begin
+
lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
unfolding countable_def card_of_ordLeq[symmetric] by auto
@@ -54,6 +58,8 @@
shows "countable A"
using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
+end
+
subsection \<open>The type of countable sets\<close>
typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
@@ -515,6 +521,10 @@
subsection \<open>Registration as BNF\<close>
+context
+ includes cardinal_syntax
+begin
+
lemma card_of_countable_sets_range:
fixes A :: "'a set"
shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
@@ -531,6 +541,8 @@
"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
+end
+
lemma finite_countable_subset:
"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
apply (rule iffI)
@@ -574,6 +586,10 @@
by (simp add: subset_eq Ball_def)(transfer, auto simp add: cimage.rep_eq, metis snd_conv, metis fst_conv)
qed
+context
+ includes cardinal_syntax
+begin
+
bnf "'a cset"
map: cimage
sets: rcset
@@ -608,3 +624,5 @@
qed(simp add: bot_cset.rep_eq)
end
+
+end
--- a/src/HOL/Main.thy Sun Apr 07 12:44:37 2019 +0200
+++ b/src/HOL/Main.thy Sun Apr 07 08:26:57 2019 +0200
@@ -8,7 +8,7 @@
theory Main
imports
Predicate_Compile
- Quickcheck_Narrowing
+ Quickcheck_Narrowing
Extraction
Nunchaku
BNF_Greatest_Fixpoint
@@ -72,6 +72,23 @@
BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and
BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
+bundle cardinal_syntax begin
+notation
+ ordLeq2 (infix "<=o" 50) and
+ ordLeq3 (infix "\<le>o" 50) and
+ ordLess2 (infix "<o" 50) and
+ ordIso2 (infix "=o" 50) and
+ card_of ("|_|") and
+ BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
+ BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
+ BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
+
+alias cinfinite = BNF_Cardinal_Arithmetic.cinfinite
+alias czero = BNF_Cardinal_Arithmetic.czero
+alias cone = BNF_Cardinal_Arithmetic.cone
+alias ctwo = BNF_Cardinal_Arithmetic.ctwo
+end
+
no_syntax
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
--- a/src/HOL/ROOT Sun Apr 07 12:44:37 2019 +0200
+++ b/src/HOL/ROOT Sun Apr 07 08:26:57 2019 +0200
@@ -328,7 +328,7 @@
IntRing (* Ideals and residue classes *)
UnivPoly (* Polynomials *)
(* Main theory *)
- Algebra
+ Algebra
document_files "root.bib" "root.tex"
session "HOL-Auth" (timing) in Auth = "HOL-Library" +
@@ -761,7 +761,7 @@
theories [quick_and_dirty]
VC_Condition
-session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
+session "HOL-Cardinals" (timing) in Cardinals = HOL +
description "
Ordinals and Cardinals, Full Theories.
"