|
lcp@105
|
1 |
(* Deriving an inference rule *)
|
|
lcp@105
|
2 |
|
|
lcp@105
|
3 |
Pretty.setmargin 72; (*existing macros just allow this margin*)
|
|
lcp@105
|
4 |
print_depth 0;
|
|
lcp@105
|
5 |
|
|
lcp@105
|
6 |
|
|
paulson@14148
|
7 |
val [major,minor] = goal IFOL.thy
|
|
lcp@105
|
8 |
"[| P&Q; [| P; Q |] ==> R |] ==> R";
|
|
lcp@105
|
9 |
prth minor;
|
|
lcp@105
|
10 |
by (resolve_tac [minor] 1);
|
|
lcp@105
|
11 |
prth major;
|
|
lcp@105
|
12 |
prth (major RS conjunct1);
|
|
lcp@105
|
13 |
by (resolve_tac [major RS conjunct1] 1);
|
|
lcp@105
|
14 |
prth (major RS conjunct2);
|
|
lcp@105
|
15 |
by (resolve_tac [major RS conjunct2] 1);
|
|
lcp@105
|
16 |
prth (topthm());
|
|
lcp@105
|
17 |
val conjE = prth(result());
|
|
lcp@105
|
18 |
|
|
lcp@105
|
19 |
|
|
lcp@105
|
20 |
- val [major,minor] = goal Int_Rule.thy
|
|
lcp@105
|
21 |
= "[| P&Q; [| P; Q |] ==> R |] ==> R";
|
|
lcp@105
|
22 |
Level 0
|
|
lcp@105
|
23 |
R
|
|
lcp@105
|
24 |
1. R
|
|
lcp@105
|
25 |
val major = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
|
|
lcp@105
|
26 |
val minor = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
|
|
lcp@105
|
27 |
- prth minor;
|
|
lcp@105
|
28 |
[| P; Q |] ==> R [[| P; Q |] ==> R]
|
|
lcp@105
|
29 |
- by (resolve_tac [minor] 1);
|
|
lcp@105
|
30 |
Level 1
|
|
lcp@105
|
31 |
R
|
|
lcp@105
|
32 |
1. P
|
|
lcp@105
|
33 |
2. Q
|
|
lcp@105
|
34 |
- prth major;
|
|
lcp@105
|
35 |
P & Q [P & Q]
|
|
lcp@105
|
36 |
- prth (major RS conjunct1);
|
|
lcp@105
|
37 |
P [P & Q]
|
|
lcp@105
|
38 |
- by (resolve_tac [major RS conjunct1] 1);
|
|
lcp@105
|
39 |
Level 2
|
|
lcp@105
|
40 |
R
|
|
lcp@105
|
41 |
1. Q
|
|
lcp@105
|
42 |
- prth (major RS conjunct2);
|
|
lcp@105
|
43 |
Q [P & Q]
|
|
lcp@105
|
44 |
- by (resolve_tac [major RS conjunct2] 1);
|
|
lcp@105
|
45 |
Level 3
|
|
lcp@105
|
46 |
R
|
|
lcp@105
|
47 |
No subgoals!
|
|
lcp@105
|
48 |
- prth (topthm());
|
|
lcp@105
|
49 |
R [P & Q, P & Q, [| P; Q |] ==> R]
|
|
lcp@105
|
50 |
- val conjE = prth(result());
|
|
lcp@105
|
51 |
[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R
|
|
lcp@105
|
52 |
val conjE = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
|
|
lcp@105
|
53 |
|
|
lcp@105
|
54 |
|
|
lcp@105
|
55 |
(*** Derived rules involving definitions ***)
|
|
lcp@105
|
56 |
|
|
lcp@105
|
57 |
(** notI **)
|
|
lcp@105
|
58 |
|
|
lcp@105
|
59 |
val prems = goal Int_Rule.thy "(P ==> False) ==> ~P";
|
|
lcp@105
|
60 |
prth not_def;
|
|
lcp@105
|
61 |
by (rewrite_goals_tac [not_def]);
|
|
lcp@105
|
62 |
by (resolve_tac [impI] 1);
|
|
lcp@105
|
63 |
by (resolve_tac prems 1);
|
|
lcp@105
|
64 |
by (assume_tac 1);
|
|
lcp@105
|
65 |
val notI = prth(result());
|
|
lcp@105
|
66 |
|
|
lcp@105
|
67 |
val prems = goalw Int_Rule.thy [not_def]
|
|
lcp@105
|
68 |
"(P ==> False) ==> ~P";
|
|
lcp@105
|
69 |
|
|
lcp@105
|
70 |
|
|
lcp@105
|
71 |
- prth not_def;
|
|
lcp@105
|
72 |
~?P == ?P --> False
|
|
lcp@105
|
73 |
- val prems = goal Int_Rule.thy "(P ==> False) ==> ~P";
|
|
lcp@105
|
74 |
Level 0
|
|
lcp@105
|
75 |
~P
|
|
lcp@105
|
76 |
1. ~P
|
|
lcp@105
|
77 |
- by (rewrite_goals_tac [not_def]);
|
|
lcp@105
|
78 |
Level 1
|
|
lcp@105
|
79 |
~P
|
|
lcp@105
|
80 |
1. P --> False
|
|
lcp@105
|
81 |
- by (resolve_tac [impI] 1);
|
|
lcp@105
|
82 |
Level 2
|
|
lcp@105
|
83 |
~P
|
|
lcp@105
|
84 |
1. P ==> False
|
|
lcp@105
|
85 |
- by (resolve_tac prems 1);
|
|
lcp@105
|
86 |
Level 3
|
|
lcp@105
|
87 |
~P
|
|
lcp@105
|
88 |
1. P ==> P
|
|
lcp@105
|
89 |
- by (assume_tac 1);
|
|
lcp@105
|
90 |
Level 4
|
|
lcp@105
|
91 |
~P
|
|
lcp@105
|
92 |
No subgoals!
|
|
lcp@105
|
93 |
- val notI = prth(result());
|
|
lcp@105
|
94 |
(?P ==> False) ==> ~?P
|
|
lcp@105
|
95 |
val notI = # : thm
|
|
lcp@105
|
96 |
|
|
lcp@105
|
97 |
- val prems = goalw Int_Rule.thy [not_def]
|
|
lcp@105
|
98 |
= "(P ==> False) ==> ~P";
|
|
lcp@105
|
99 |
Level 0
|
|
lcp@105
|
100 |
~P
|
|
lcp@105
|
101 |
1. P --> False
|
|
lcp@105
|
102 |
|
|
lcp@105
|
103 |
|
|
lcp@105
|
104 |
(** notE **)
|
|
lcp@105
|
105 |
|
|
lcp@105
|
106 |
val [major,minor] = goal Int_Rule.thy "[| ~P; P |] ==> R";
|
|
lcp@105
|
107 |
by (resolve_tac [FalseE] 1);
|
|
lcp@105
|
108 |
by (resolve_tac [mp] 1);
|
|
lcp@105
|
109 |
prth (rewrite_rule [not_def] major);
|
|
lcp@105
|
110 |
by (resolve_tac [it] 1);
|
|
lcp@105
|
111 |
by (resolve_tac [minor] 1);
|
|
lcp@105
|
112 |
val notE = prth(result());
|
|
lcp@105
|
113 |
|
|
lcp@105
|
114 |
val [major,minor] = goalw Int_Rule.thy [not_def]
|
|
lcp@105
|
115 |
"[| ~P; P |] ==> R";
|
|
lcp@105
|
116 |
prth (minor RS (major RS mp RS FalseE));
|
|
lcp@105
|
117 |
by (resolve_tac [it] 1);
|
|
lcp@105
|
118 |
|
|
lcp@105
|
119 |
|
|
lcp@105
|
120 |
val prems = goalw Int_Rule.thy [not_def]
|
|
lcp@105
|
121 |
"[| ~P; P |] ==> R";
|
|
lcp@105
|
122 |
prths prems;
|
|
lcp@105
|
123 |
by (resolve_tac [FalseE] 1);
|
|
lcp@105
|
124 |
by (resolve_tac [mp] 1);
|
|
lcp@105
|
125 |
by (resolve_tac prems 1);
|
|
lcp@105
|
126 |
by (resolve_tac prems 1);
|
|
lcp@105
|
127 |
val notE = prth(result());
|
|
lcp@105
|
128 |
|
|
lcp@105
|
129 |
|
|
lcp@105
|
130 |
- val [major,minor] = goal Int_Rule.thy "[| ~P; P |] ==> R";
|
|
lcp@105
|
131 |
Level 0
|
|
lcp@105
|
132 |
R
|
|
lcp@105
|
133 |
1. R
|
|
lcp@105
|
134 |
val major = # : thm
|
|
lcp@105
|
135 |
val minor = # : thm
|
|
lcp@105
|
136 |
- by (resolve_tac [FalseE] 1);
|
|
lcp@105
|
137 |
Level 1
|
|
lcp@105
|
138 |
R
|
|
lcp@105
|
139 |
1. False
|
|
lcp@105
|
140 |
- by (resolve_tac [mp] 1);
|
|
lcp@105
|
141 |
Level 2
|
|
lcp@105
|
142 |
R
|
|
lcp@105
|
143 |
1. ?P1 --> False
|
|
lcp@105
|
144 |
2. ?P1
|
|
lcp@105
|
145 |
- prth (rewrite_rule [not_def] major);
|
|
lcp@105
|
146 |
P --> False [~P]
|
|
lcp@105
|
147 |
- by (resolve_tac [it] 1);
|
|
lcp@105
|
148 |
Level 3
|
|
lcp@105
|
149 |
R
|
|
lcp@105
|
150 |
1. P
|
|
lcp@105
|
151 |
- by (resolve_tac [minor] 1);
|
|
lcp@105
|
152 |
Level 4
|
|
lcp@105
|
153 |
R
|
|
lcp@105
|
154 |
No subgoals!
|
|
lcp@105
|
155 |
- val notE = prth(result());
|
|
lcp@105
|
156 |
[| ~?P; ?P |] ==> ?R
|
|
lcp@105
|
157 |
val notE = # : thm
|
|
lcp@105
|
158 |
- val [major,minor] = goalw Int_Rule.thy [not_def]
|
|
lcp@105
|
159 |
= "[| ~P; P |] ==> R";
|
|
lcp@105
|
160 |
Level 0
|
|
lcp@105
|
161 |
R
|
|
lcp@105
|
162 |
1. R
|
|
lcp@105
|
163 |
val major = # : thm
|
|
lcp@105
|
164 |
val minor = # : thm
|
|
lcp@105
|
165 |
- prth (minor RS (major RS mp RS FalseE));
|
|
lcp@105
|
166 |
?P [P, ~P]
|
|
lcp@105
|
167 |
- by (resolve_tac [it] 1);
|
|
lcp@105
|
168 |
Level 1
|
|
lcp@105
|
169 |
R
|
|
lcp@105
|
170 |
No subgoals!
|
|
lcp@105
|
171 |
|
|
lcp@105
|
172 |
|
|
lcp@105
|
173 |
|
|
lcp@105
|
174 |
|
|
lcp@105
|
175 |
- goal Int_Rule.thy "[| ~P; P |] ==> R";
|
|
lcp@105
|
176 |
Level 0
|
|
lcp@105
|
177 |
R
|
|
lcp@105
|
178 |
1. R
|
|
lcp@105
|
179 |
- prths (map (rewrite_rule [not_def]) it);
|
|
lcp@105
|
180 |
P --> False [~P]
|
|
lcp@105
|
181 |
|
|
lcp@105
|
182 |
P [P]
|
|
lcp@105
|
183 |
|
|
lcp@105
|
184 |
- val prems = goalw Int_Rule.thy [not_def]
|
|
lcp@105
|
185 |
= "[| ~P; P |] ==> R";
|
|
lcp@105
|
186 |
Level 0
|
|
lcp@105
|
187 |
R
|
|
lcp@105
|
188 |
1. R
|
|
lcp@105
|
189 |
val prems = # : thm list
|
|
lcp@105
|
190 |
- prths prems;
|
|
lcp@105
|
191 |
P --> False [~P]
|
|
lcp@105
|
192 |
|
|
lcp@105
|
193 |
P [P]
|
|
lcp@105
|
194 |
|
|
lcp@105
|
195 |
- by (resolve_tac [mp RS FalseE] 1);
|
|
lcp@105
|
196 |
Level 1
|
|
lcp@105
|
197 |
R
|
|
lcp@105
|
198 |
1. ?P1 --> False
|
|
lcp@105
|
199 |
2. ?P1
|
|
lcp@105
|
200 |
- by (resolve_tac prems 1);
|
|
lcp@105
|
201 |
Level 2
|
|
lcp@105
|
202 |
R
|
|
lcp@105
|
203 |
1. P
|
|
lcp@105
|
204 |
- by (resolve_tac prems 1);
|
|
lcp@105
|
205 |
Level 3
|
|
lcp@105
|
206 |
R
|
|
lcp@105
|
207 |
No subgoals!
|
|
lcp@105
|
208 |
- val notE = prth(result());
|
|
lcp@105
|
209 |
[| ~?P; ?P |] ==> ?R
|
|
lcp@105
|
210 |
val notE = # : thm
|