# 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 \ BNF_Util.Grp" + + subsection{* Cardinal stuff *} lemma countable_card_of_nat: "countable A \ |A| \o |UNIV::nat set|" @@ -26,12 +28,8 @@ assumes "countable A" shows "(finite A \ |A| (infinite A \ |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' \ "the_inv rcset (Collect (split R) \ (rcset a \ 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 \ root) ` cont (H n)) \ P" (is "?L \ P") proof- have "?L = (n, (id \ 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 "... \ 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 "\o" 50) and - ordLess2 (infix "") +abbreviation "Grp \ BNF_Util.Grp" +abbreviation "fstOp \ BNF_Def.fstOp" +abbreviation "sndOp \ 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 "\o" 50) and + ordLess2 (infix "o" 50) and - ordLess2 (infix "