# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 235c7661a96b737ba4321ca657f011a86f440bca
# Parent  b3e44be901227bf9ee98f17b5ccb2f35c6b2597e
rationalized dependencies

diff -r b3e44be90122 -r 235c7661a96b src/HOL/BNF/BNF.thy
--- a/src/HOL/BNF/BNF.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/BNF.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -10,7 +10,7 @@
 header {* Bounded Natural Functors for (Co)datatypes *}
 
 theory BNF
-imports Countable_Set_Type BNF_Decl
+imports More_BNFs Countable_Set_Type BNF_Decl
 begin
 
 end
diff -r b3e44be90122 -r 235c7661a96b src/HOL/BNF/Countable_Set_Type.thy
--- a/src/HOL/BNF/Countable_Set_Type.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Countable_Set_Type.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,11 +9,13 @@
 
 theory Countable_Set_Type
 imports
-  More_BNFs
-  "~~/src/HOL/Cardinals/Cardinals"
+  "~~/src/HOL/Cardinals/Cardinal_Notations"
   "~~/src/HOL/Library/Countable_Set"
 begin
 
+abbreviation "Grp \<equiv> BNF_Util.Grp"
+
+
 subsection{* Cardinal stuff *}
 
 lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
@@ -26,12 +28,8 @@
 assumes "countable A"
 shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
        (infinite A  \<and> |A| =o |UNIV::nat set| )"
-proof (cases "finite A")
-  case True thus ?thesis by (metis finite_iff_cardOf_nat)
-next
-  case False with assms show ?thesis
-    by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
-qed
+by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq
+      ordLeq_iff_ordLess_or_ordIso)
 
 lemma countable_cases_card_of[elim]:
   assumes "countable A"
@@ -142,7 +140,7 @@
   def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
   (is "the_inv rcset ?L'")
   have L: "countable ?L'" by auto
-  hence *: "rcset R' = ?L'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset)
+  hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset)
   thus ?R unfolding Grp_def relcompp.simps conversep.simps
   proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
     from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times)
diff -r b3e44be90122 -r 235c7661a96b src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -1013,9 +1013,9 @@
 shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
 proof-
   have "?L = (n, (id \<oplus> root) ` cont (pick n))"
-  unfolding cont_H image_compose[symmetric] sum_map.comp id_comp comp_assoc
+  unfolding cont_H image_compose[symmetric] sum_map.comp id_comp comp_assoc[symmetric]
   unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
-  by(rule root_H_root[OF n])
+  by (rule root_H_root[OF n])
   moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
   ultimately show ?thesis by simp
 qed
diff -r b3e44be90122 -r 235c7661a96b src/HOL/BNF/Examples/Lambda_Term.thy
--- a/src/HOL/BNF/Examples/Lambda_Term.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Lambda_Term.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,9 +9,10 @@
 header {* Lambda-Terms *}
 
 theory Lambda_Term
-imports "../BNF"
+imports "../More_BNFs"
 begin
 
+thy_deps
 
 section {* Datatype definition *}
 
diff -r b3e44be90122 -r 235c7661a96b src/HOL/BNF/Examples/Misc_Codatatype.thy
--- a/src/HOL/BNF/Examples/Misc_Codatatype.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Misc_Codatatype.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -10,7 +10,7 @@
 header {* Miscellaneous Codatatype Definitions *}
 
 theory Misc_Codatatype
-imports "../BNF"
+imports More_BNFs
 begin
 
 codatatype simple = X1 | X2 | X3 | X4
diff -r b3e44be90122 -r 235c7661a96b src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,7 +9,7 @@
 header {* Infinite Streams *}
 
 theory Stream
-imports "../BNF"
+imports "~~/Library/Nat_Bijection"
 begin
 
 codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
diff -r b3e44be90122 -r 235c7661a96b src/HOL/BNF/Examples/Stream_Processor.thy
--- a/src/HOL/BNF/Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,7 +9,7 @@
 header {* Stream Processors *}
 
 theory Stream_Processor
-imports Stream
+imports Stream "../BNF_Decl"
 begin
 
 section {* Continuous Functions on Streams *}
diff -r b3e44be90122 -r 235c7661a96b src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -12,20 +12,14 @@
 
 theory More_BNFs
 imports
-  Basic_BNFs
+  "~~/src/HOL/Cardinals/Cardinal_Notations"
   "~~/src/HOL/Library/FSet"
   "~~/src/HOL/Library/Multiset"
 begin
 
-notation
-  ordLeq2 (infix "<=o" 50) and
-  ordLeq3 (infix "\<le>o" 50) and
-  ordLess2 (infix "<o" 50) and
-  ordIso2 (infix "=o" 50) and
-  csum (infixr "+c" 65) and
-  cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90) and
-  convol ("<_ , _>")
+abbreviation "Grp \<equiv> BNF_Util.Grp"
+abbreviation "fstOp \<equiv> BNF_Def.fstOp"
+abbreviation "sndOp \<equiv> BNF_Def.sndOp"
 
 lemma option_rec_conv_option_case: "option_rec = option_case"
 by (simp add: fun_eq_iff split: option.split)
diff -r b3e44be90122 -r 235c7661a96b src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,12 +11,6 @@
 imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
 begin
 
-notation
-  csum (infixr "+c" 65) and
-  cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90)
-
-
 subsection {* Binary sum *}
 
 lemma csum_Cnotzero2:
diff -r b3e44be90122 -r 235c7661a96b src/HOL/Cardinals/Cardinal_Notations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Cardinals/Cardinal_Notations.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -0,0 +1,23 @@
+(*  Title:      HOL/Cardinals/Cardinal_Notations.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2013
+
+Cardinal notations.
+*)
+
+header {* Cardinal Notations *}
+
+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
+  csum (infixr "+c" 65) and
+  cprod (infixr "*c" 80) and
+  cexp (infixr "^c" 90)
+
+end
diff -r b3e44be90122 -r 235c7661a96b src/HOL/Cardinals/Constructions_on_Wellorders.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -8,15 +8,9 @@
 header {* Constructions on Wellorders *}
 
 theory Constructions_on_Wellorders
-imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union
+imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union Cardinal_Notations
 begin
 
-notation
-  ordLeq2 (infix "<=o" 50) and
-  ordLeq3 (infix "\<le>o" 50) and
-  ordLess2 (infix "<o" 50) and
-  ordIso2 (infix "=o" 50)
-
 declare
   ordLeq_Well_order_simp[simp]
   not_ordLeq_iff_ordLess[simp]