30 by (rtac (major RS UnE) 1); |
30 by (rtac (major RS UnE) 1); |
31 by (REPEAT (rtac refl 1 |
31 by (REPEAT (rtac refl 1 |
32 ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1)); |
32 ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1)); |
33 val sumE = result(); |
33 val sumE = result(); |
34 |
34 |
35 (** Injection and freeness rules **) |
|
36 |
|
37 val [major] = goalw Sum.thy sum_defs "Inl(a)=Inl(b) ==> a=b"; |
|
38 by (EVERY1 [rtac (major RS Pair_inject), assume_tac]); |
|
39 val Inl_inject = result(); |
|
40 |
|
41 val [major] = goalw Sum.thy sum_defs "Inr(a)=Inr(b) ==> a=b"; |
|
42 by (EVERY1 [rtac (major RS Pair_inject), assume_tac]); |
|
43 val Inr_inject = result(); |
|
44 |
|
45 val [major] = goalw Sum.thy sum_defs "Inl(a)=Inr(b) ==> P"; |
|
46 by (rtac (major RS Pair_inject) 1); |
|
47 by (etac (sym RS one_neq_0) 1); |
|
48 val Inl_neq_Inr = result(); |
|
49 |
|
50 val Inr_neq_Inl = sym RS Inl_neq_Inr; |
|
51 |
|
52 (** Injection and freeness equivalences, for rewriting **) |
35 (** Injection and freeness equivalences, for rewriting **) |
53 |
36 |
54 goal Sum.thy "Inl(a)=Inl(b) <-> a=b"; |
37 goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b"; |
55 by (rtac iffI 1); |
38 by (simp_tac (ZF_ss addsimps [Pair_iff]) 1); |
56 by (REPEAT (eresolve_tac [Inl_inject,subst_context] 1)); |
|
57 val Inl_iff = result(); |
39 val Inl_iff = result(); |
58 |
40 |
59 goal Sum.thy "Inr(a)=Inr(b) <-> a=b"; |
41 goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b"; |
60 by (rtac iffI 1); |
42 by (simp_tac (ZF_ss addsimps [Pair_iff]) 1); |
61 by (REPEAT (eresolve_tac [Inr_inject,subst_context] 1)); |
|
62 val Inr_iff = result(); |
43 val Inr_iff = result(); |
63 |
44 |
64 goal Sum.thy "Inl(a)=Inr(b) <-> False"; |
45 goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False"; |
65 by (rtac iffI 1); |
46 by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0 RS not_sym]) 1); |
66 by (REPEAT (eresolve_tac [Inl_neq_Inr,FalseE] 1)); |
|
67 val Inl_Inr_iff = result(); |
47 val Inl_Inr_iff = result(); |
68 |
48 |
69 goal Sum.thy "Inr(b)=Inl(a) <-> False"; |
49 goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False"; |
70 by (rtac iffI 1); |
50 by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1); |
71 by (REPEAT (eresolve_tac [Inr_neq_Inl,FalseE] 1)); |
|
72 val Inr_Inl_iff = result(); |
51 val Inr_Inl_iff = result(); |
73 |
52 |
74 val sum_cs = ZF_cs addIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl] |
53 (*Injection and freeness rules*) |
|
54 |
|
55 val Inl_inject = standard (Inl_iff RS iffD1); |
|
56 val Inr_inject = standard (Inr_iff RS iffD1); |
|
57 val Inl_neq_Inr = standard (Inl_Inr_iff RS iffD1 RS FalseE); |
|
58 val Inr_neq_Inl = standard (Inr_Inl_iff RS iffD1 RS FalseE); |
|
59 |
|
60 val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl] |
75 addSDs [Inl_inject,Inr_inject]; |
61 addSDs [Inl_inject,Inr_inject]; |
|
62 |
|
63 goal Sum.thy "!!A B. Inl(a): A+B ==> a: A"; |
|
64 by (fast_tac sum_cs 1); |
|
65 val InlD = result(); |
|
66 |
|
67 goal Sum.thy "!!A B. Inr(b): A+B ==> b: B"; |
|
68 by (fast_tac sum_cs 1); |
|
69 val InrD = result(); |
76 |
70 |
77 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"; |
71 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"; |
78 by (fast_tac sum_cs 1); |
72 by (fast_tac sum_cs 1); |
79 val sum_iff = result(); |
73 val sum_iff = result(); |
80 |
74 |