equal
deleted
inserted
replaced
22 text {*A form of conj-elimination*} |
22 text {*A form of conj-elimination*} |
23 lemma |
23 lemma |
24 assumes "A & B" |
24 assumes "A & B" |
25 and "A ==> B ==> C" |
25 and "A ==> B ==> C" |
26 shows C |
26 shows C |
27 apply (rule prems) |
27 apply (rule assms) |
28 apply (rule conjunct1) |
28 apply (rule conjunct1) |
29 apply (rule prems) |
29 apply (rule assms) |
30 apply (rule conjunct2) |
30 apply (rule conjunct2) |
31 apply (rule prems) |
31 apply (rule assms) |
32 done |
32 done |
33 |
33 |
34 lemma |
34 lemma |
35 assumes "!!A. ~ ~A ==> A" |
35 assumes "!!A. ~ ~A ==> A" |
36 shows "B | ~B" |
36 shows "B | ~B" |
37 apply (rule prems) |
37 apply (rule assms) |
38 apply (rule notI) |
38 apply (rule notI) |
39 apply (rule_tac P = "~B" in notE) |
39 apply (rule_tac P = "~B" in notE) |
40 apply (rule_tac [2] notI) |
40 apply (rule_tac [2] notI) |
41 apply (rule_tac [2] P = "B | ~B" in notE) |
41 apply (rule_tac [2] P = "B | ~B" in notE) |
42 prefer 2 apply assumption |
42 prefer 2 apply assumption |
50 done |
50 done |
51 |
51 |
52 lemma |
52 lemma |
53 assumes "!!A. ~ ~A ==> A" |
53 assumes "!!A. ~ ~A ==> A" |
54 shows "B | ~B" |
54 shows "B | ~B" |
55 apply (rule prems) |
55 apply (rule assms) |
56 apply (rule notI) |
56 apply (rule notI) |
57 apply (rule notE) |
57 apply (rule notE) |
58 apply (rule_tac [2] notI) |
58 apply (rule_tac [2] notI) |
59 apply (erule_tac [2] notE) |
59 apply (erule_tac [2] notE) |
60 apply (erule_tac [2] disjI1) |
60 apply (erule_tac [2] disjI1) |
67 lemma |
67 lemma |
68 assumes "A | ~A" |
68 assumes "A | ~A" |
69 and "~ ~A" |
69 and "~ ~A" |
70 shows A |
70 shows A |
71 apply (rule disjE) |
71 apply (rule disjE) |
72 apply (rule prems) |
72 apply (rule assms) |
73 apply assumption |
73 apply assumption |
74 apply (rule FalseE) |
74 apply (rule FalseE) |
75 apply (rule_tac P = "~A" in notE) |
75 apply (rule_tac P = "~A" in notE) |
76 apply (rule prems) |
76 apply (rule assms) |
77 apply assumption |
77 apply assumption |
78 done |
78 done |
79 |
79 |
80 |
80 |
81 subsection "Examples with quantifiers" |
81 subsection "Examples with quantifiers" |
83 lemma |
83 lemma |
84 assumes "ALL z. G(z)" |
84 assumes "ALL z. G(z)" |
85 shows "ALL z. G(z)|H(z)" |
85 shows "ALL z. G(z)|H(z)" |
86 apply (rule allI) |
86 apply (rule allI) |
87 apply (rule disjI1) |
87 apply (rule disjI1) |
88 apply (rule prems [THEN spec]) |
88 apply (rule assms [THEN spec]) |
89 done |
89 done |
90 |
90 |
91 lemma "ALL x. EX y. x=y" |
91 lemma "ALL x. EX y. x=y" |
92 apply (rule allI) |
92 apply (rule allI) |
93 apply (rule exI) |
93 apply (rule exI) |
111 |
111 |
112 lemma |
112 lemma |
113 assumes "(EX z. F(z)) & B" |
113 assumes "(EX z. F(z)) & B" |
114 shows "EX z. F(z) & B" |
114 shows "EX z. F(z) & B" |
115 apply (rule conjE) |
115 apply (rule conjE) |
116 apply (rule prems) |
116 apply (rule assms) |
117 apply (rule exE) |
117 apply (rule exE) |
118 apply assumption |
118 apply assumption |
119 apply (rule exI) |
119 apply (rule exI) |
120 apply (rule conjI) |
120 apply (rule conjI) |
121 apply assumption |
121 apply assumption |