# HG changeset patch
# User traytel
# Date 1554618417 -7200
# Node ID 3a1b2d8c89aaea6e9c64680b427243df611e1e50
# Parent  3b3089863edafc49a615f224fb329c9d1249194e
bundle for cardinal syntax

diff -r 3b3089863eda -r 3a1b2d8c89aa src/Doc/Datatypes/Datatypes.thy
--- 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,
diff -r 3b3089863eda -r 3a1b2d8c89aa src/HOL/Cardinals/Wellorder_Constructions.thy
--- 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]
diff -r 3b3089863eda -r 3a1b2d8c89aa src/HOL/Library/Cardinal_Notations.thy
--- 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
diff -r 3b3089863eda -r 3a1b2d8c89aa src/HOL/Library/Countable_Set_Type.thy
--- 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
diff -r 3b3089863eda -r 3a1b2d8c89aa src/HOL/Main.thy
--- 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)
diff -r 3b3089863eda -r 3a1b2d8c89aa src/HOL/ROOT
--- 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.
   "