44 definition |
44 definition |
45 Unity :: unit ("'(')") |
45 Unity :: unit ("'(')") |
46 where |
46 where |
47 "() = Abs_unit True" |
47 "() = Abs_unit True" |
48 |
48 |
49 lemma unit_eq [noatp]: "u = ()" |
49 lemma unit_eq [no_atp]: "u = ()" |
50 by (induct u) (simp add: unit_def Unity_def) |
50 by (induct u) (simp add: unit_def Unity_def) |
51 |
51 |
52 text {* |
52 text {* |
53 Simplification procedure for @{thm [source] unit_eq}. Cannot use |
53 Simplification procedure for @{thm [source] unit_eq}. Cannot use |
54 this rule directly --- it loops! |
54 this rule directly --- it loops! |
76 This rewrite counters the effect of @{text unit_eq_proc} on @{term |
76 This rewrite counters the effect of @{text unit_eq_proc} on @{term |
77 [source] "%u::unit. f u"}, replacing it by @{term [source] |
77 [source] "%u::unit. f u"}, replacing it by @{term [source] |
78 f} rather than by @{term [source] "%u. f ()"}. |
78 f} rather than by @{term [source] "%u. f ()"}. |
79 *} |
79 *} |
80 |
80 |
81 lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f" |
81 lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f" |
82 by (rule ext) simp |
82 by (rule ext) simp |
83 |
83 |
84 instantiation unit :: default |
84 instantiation unit :: default |
85 begin |
85 begin |
86 |
86 |
495 *} |
495 *} |
496 |
496 |
497 lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)" |
497 lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)" |
498 by (subst surjective_pairing, rule split_conv) |
498 by (subst surjective_pairing, rule split_conv) |
499 |
499 |
500 lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))" |
500 lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))" |
501 -- {* For use with @{text split} and the Simplifier. *} |
501 -- {* For use with @{text split} and the Simplifier. *} |
502 by (insert surj_pair [of p], clarify, simp) |
502 by (insert surj_pair [of p], clarify, simp) |
503 |
503 |
504 text {* |
504 text {* |
505 @{thm [source] split_split} could be declared as @{text "[split]"} |
505 @{thm [source] split_split} could be declared as @{text "[split]"} |
506 done after the Splitter has been speeded up significantly; |
506 done after the Splitter has been speeded up significantly; |
507 precompute the constants involved and don't do anything unless the |
507 precompute the constants involved and don't do anything unless the |
508 current goal contains one of those constants. |
508 current goal contains one of those constants. |
509 *} |
509 *} |
510 |
510 |
511 lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))" |
511 lemma split_split_asm [no_atp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))" |
512 by (subst split_split, simp) |
512 by (subst split_split, simp) |
513 |
513 |
514 |
514 |
515 text {* |
515 text {* |
516 \medskip @{term split} used as a logical connective or set former. |
516 \medskip @{term split} used as a logical connective or set former. |
580 to quite time-consuming computations (in particular for nested tuples) *) |
580 to quite time-consuming computations (in particular for nested tuples) *) |
581 declaration {* fn _ => |
581 declaration {* fn _ => |
582 Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac)) |
582 Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac)) |
583 *} |
583 *} |
584 |
584 |
585 lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P" |
585 lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P" |
586 by (rule ext) fast |
586 by (rule ext) fast |
587 |
587 |
588 lemma split_eta_SetCompr2 [simp,noatp]: "(%u. EX x y. u = (x, y) & P x y) = split P" |
588 lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P" |
589 by (rule ext) fast |
589 by (rule ext) fast |
590 |
590 |
591 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)" |
591 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)" |
592 -- {* Allows simplifications of nested splits in case of independent predicates. *} |
592 -- {* Allows simplifications of nested splits in case of independent predicates. *} |
593 by (rule ext) blast |
593 by (rule ext) blast |
945 lemma UN_Times_distrib: |
945 lemma UN_Times_distrib: |
946 "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)" |
946 "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)" |
947 -- {* Suggested by Pierre Chartier *} |
947 -- {* Suggested by Pierre Chartier *} |
948 by blast |
948 by blast |
949 |
949 |
950 lemma split_paired_Ball_Sigma [simp,noatp]: |
950 lemma split_paired_Ball_Sigma [simp,no_atp]: |
951 "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))" |
951 "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))" |
952 by blast |
952 by blast |
953 |
953 |
954 lemma split_paired_Bex_Sigma [simp,noatp]: |
954 lemma split_paired_Bex_Sigma [simp,no_atp]: |
955 "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))" |
955 "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))" |
956 by blast |
956 by blast |
957 |
957 |
958 lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))" |
958 lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))" |
959 by blast |
959 by blast |