--- 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
--- 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)
--- 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
--- 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 *}
--- 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
--- 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) =
--- 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 *}
--- 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)
--- 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:
--- /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
--- 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]