author  wenzelm 
Fri, 01 Jan 2016 10:49:00 +0100  
changeset 62020  5d208fd2507d 
parent 61337  4645502c3c64 
child 67443  3abf6a722518 
permissions  rwrr 
26322  1 
(* Title: FOLP/ex/Intuitionistic.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1991 University of Cambridge 

4 

5 
Intuitionistic FirstOrder Logic. 

6 

7 
Singlestep commands: 

8 
by (IntPr.step_tac 1) 

9 
by (biresolve_tac safe_brls 1); 

10 
by (biresolve_tac haz_brls 1); 

11 
by (assume_tac 1); 

12 
by (IntPr.safe_tac 1); 

13 
by (IntPr.mp_tac 1); 

14 
by (IntPr.fast_tac 1); 

15 
*) 

16 

17 
(*Note: for PROPOSITIONAL formulae... 

18 
~A is classically provable iff it is intuitionistically provable. 

19 
Therefore A is classically provable iff ~~A is intuitionistically provable. 

20 

21 
Let Q be the conjuction of the propositions A~A, one for each atom A in 

22 
P. If P is provable classically, then clearly P&Q is provable 

23 
intuitionistically, so ~~(P&Q) is also provable intuitionistically. 

24 
The latter is intuitionistically equivalent to ~~P&~~Q, hence to ~~P, 

25 
since ~~Q is intuitionistically provable. Finally, if P is a negation then 

26 
~~P is intuitionstically equivalent to P. [Andy Pitts] 

27 
*) 

28 

29 
theory Intuitionistic 

30 
imports IFOLP 

31 
begin 

32 

61337  33 
schematic_goal "?p : ~~(P&Q) <> ~~P & ~~Q" 
60770  34 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  35 

61337  36 
schematic_goal "?p : ~~~P <> ~P" 
60770  37 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  38 

61337  39 
schematic_goal "?p : ~~((P > Q  R) > (P>Q)  (P>R))" 
60770  40 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  41 

61337  42 
schematic_goal "?p : (P<>Q) <> (Q<>P)" 
60770  43 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  44 

45 

60770  46 
subsection \<open>Lemmas for the propositional doublenegation translation\<close> 
26322  47 

61337  48 
schematic_goal "?p : P > ~~P" 
60770  49 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  50 

61337  51 
schematic_goal "?p : ~~(~~P > P)" 
60770  52 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  53 

61337  54 
schematic_goal "?p : ~~P & ~~(P > Q) > ~~Q" 
60770  55 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  56 

57 

60770  58 
subsection \<open>The following are classically but not constructively valid\<close> 
26322  59 

60 
(*The attempt to prove them terminates quickly!*) 

61337  61 
schematic_goal "?p : ((P>Q) > P) > P" 
60770  62 
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? 
26322  63 
oops 
64 

61337  65 
schematic_goal "?p : (P&Q>R) > (P>R)  (Q>R)" 
60770  66 
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? 
26322  67 
oops 
68 

69 

60770  70 
subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier\<close> 
26322  71 

72 
text "Problem ~~1" 

61337  73 
schematic_goal "?p : ~~((P>Q) <> (~Q > ~P))" 
60770  74 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  75 

76 
text "Problem ~~2" 

61337  77 
schematic_goal "?p : ~~(~~P <> P)" 
60770  78 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  79 

80 
text "Problem 3" 

61337  81 
schematic_goal "?p : ~(P>Q) > (Q>P)" 
60770  82 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  83 

84 
text "Problem ~~4" 

61337  85 
schematic_goal "?p : ~~((~P>Q) <> (~Q > P))" 
60770  86 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  87 

88 
text "Problem ~~5" 

61337  89 
schematic_goal "?p : ~~((PQ>PR) > P(Q>R))" 
60770  90 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  91 

92 
text "Problem ~~6" 

61337  93 
schematic_goal "?p : ~~(P  ~P)" 
60770  94 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  95 

96 
text "Problem ~~7" 

61337  97 
schematic_goal "?p : ~~(P  ~~~P)" 
60770  98 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  99 

100 
text "Problem ~~8. Peirce's law" 

61337  101 
schematic_goal "?p : ~~(((P>Q) > P) > P)" 
60770  102 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  103 

104 
text "Problem 9" 

61337  105 
schematic_goal "?p : ((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)" 
60770  106 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  107 

108 
text "Problem 10" 

61337  109 
schematic_goal "?p : (Q>R) > (R>P&Q) > (P>(QR)) > (P<>Q)" 
60770  110 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  111 

112 
text "11. Proved in each direction (incorrectly, says Pelletier!!) " 

61337  113 
schematic_goal "?p : P<>P" 
60770  114 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  115 

116 
text "Problem ~~12. Dijkstra's law " 

61337  117 
schematic_goal "?p : ~~(((P <> Q) <> R) <> (P <> (Q <> R)))" 
60770  118 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  119 

61337  120 
schematic_goal "?p : ((P <> Q) <> R) > ~~(P <> (Q <> R))" 
60770  121 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  122 

123 
text "Problem 13. Distributive law" 

61337  124 
schematic_goal "?p : P  (Q & R) <> (P  Q) & (P  R)" 
60770  125 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  126 

127 
text "Problem ~~14" 

61337  128 
schematic_goal "?p : ~~((P <> Q) <> ((Q  ~P) & (~QP)))" 
60770  129 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  130 

131 
text "Problem ~~15" 

61337  132 
schematic_goal "?p : ~~((P > Q) <> (~P  Q))" 
60770  133 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  134 

135 
text "Problem ~~16" 

61337  136 
schematic_goal "?p : ~~((P>Q)  (Q>P))" 
60770  137 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  138 

139 
text "Problem ~~17" 

61337  140 
schematic_goal "?p : ~~(((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S)))" 
62020  141 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) \<comment> slow 
26322  142 

143 

60770  144 
subsection \<open>Examples with quantifiers\<close> 
26322  145 

146 
text "The converse is classical in the following implications..." 

147 

61337  148 
schematic_goal "?p : (EX x. P(x)>Q) > (ALL x. P(x)) > Q" 
60770  149 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  150 

61337  151 
schematic_goal "?p : ((ALL x. P(x))>Q) > ~ (ALL x. P(x) & ~Q)" 
60770  152 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  153 

61337  154 
schematic_goal "?p : ((ALL x. ~P(x))>Q) > ~ (ALL x. ~ (P(x)Q))" 
60770  155 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  156 

61337  157 
schematic_goal "?p : (ALL x. P(x))  Q > (ALL x. P(x)  Q)" 
60770  158 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  159 

61337  160 
schematic_goal "?p : (EX x. P > Q(x)) > (P > (EX x. Q(x)))" 
60770  161 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  162 

163 

164 
text "The following are not constructively valid!" 

165 
text "The attempt to prove them terminates quickly!" 

166 

61337  167 
schematic_goal "?p : ((ALL x. P(x))>Q) > (EX x. P(x)>Q)" 
60770  168 
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? 
26322  169 
oops 
170 

61337  171 
schematic_goal "?p : (P > (EX x. Q(x))) > (EX x. P>Q(x))" 
60770  172 
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? 
26322  173 
oops 
174 

61337  175 
schematic_goal "?p : (ALL x. P(x)  Q) > ((ALL x. P(x))  Q)" 
60770  176 
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? 
26322  177 
oops 
178 

61337  179 
schematic_goal "?p : (ALL x. ~~P(x)) > ~~(ALL x. P(x))" 
60770  180 
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? 
26322  181 
oops 
182 

183 
(*Classically but not intuitionistically valid. Proved by a bug in 1986!*) 

61337  184 
schematic_goal "?p : EX x. Q(x) > (ALL x. Q(x))" 
60770  185 
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? 
26322  186 
oops 
187 

188 

189 
subsection "Hard examples with quantifiers" 

190 

60770  191 
text \<open> 
26322  192 
The ones that have not been proved are not known to be valid! 
193 
Some will require quantifier duplication  not currently available. 

60770  194 
\<close> 
26322  195 

196 
text "Problem ~~18" 

61337  197 
schematic_goal "?p : ~~(EX y. ALL x. P(y)>P(x))" oops 
26322  198 
(*NOT PROVED*) 
199 

200 
text "Problem ~~19" 

61337  201 
schematic_goal "?p : ~~(EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x)))" oops 
26322  202 
(*NOT PROVED*) 
203 

204 
text "Problem 20" 

61337  205 
schematic_goal "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w))) 
26322  206 
> (EX x y. P(x) & Q(y)) > (EX z. R(z))" 
60770  207 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  208 

209 
text "Problem 21" 

61337  210 
schematic_goal "?p : (EX x. P>Q(x)) & (EX x. Q(x)>P) > ~~(EX x. P<>Q(x))" oops 
26322  211 
(*NOT PROVED*) 
212 

213 
text "Problem 22" 

61337  214 
schematic_goal "?p : (ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))" 
60770  215 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  216 

217 
text "Problem ~~23" 

61337  218 
schematic_goal "?p : ~~ ((ALL x. P  Q(x)) <> (P  (ALL x. Q(x))))" 
60770  219 
by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) 
26322  220 

221 
text "Problem 24" 

61337  222 
schematic_goal "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) & 
26322  223 
(~(EX x. P(x)) > (EX x. Q(x))) & (ALL x. Q(x)R(x) > S(x)) 
224 
> ~~(EX x. P(x)&R(x))" 

225 
(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

226 
apply (tactic "IntPr.safe_tac @{context}") 
26322  227 
apply (erule impE) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

228 
apply (tactic "IntPr.fast_tac @{context} 1") 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

229 
apply (tactic "IntPr.fast_tac @{context} 1") 
26322  230 
done 
231 

232 
text "Problem 25" 

61337  233 
schematic_goal "?p : (EX x. P(x)) & 
26322  234 
(ALL x. L(x) > ~ (M(x) & R(x))) & 
235 
(ALL x. P(x) > (M(x) & L(x))) & 

236 
((ALL x. P(x)>Q(x))  (EX x. P(x)&R(x))) 

237 
> (EX x. Q(x)&P(x))" 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

238 
by (tactic "IntPr.best_tac @{context} 1") 
26322  239 

240 
text "Problem 29. Essentially the same as Principia Mathematica *11.71" 

61337  241 
schematic_goal "?p : (EX x. P(x)) & (EX y. Q(y)) 
26322  242 
> ((ALL x. P(x)>R(x)) & (ALL y. Q(y)>S(y)) <> 
243 
(ALL x y. P(x) & Q(y) > R(x) & S(y)))" 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

244 
by (tactic "IntPr.fast_tac @{context} 1") 
26322  245 

246 
text "Problem ~~30" 

61337  247 
schematic_goal "?p : (ALL x. (P(x)  Q(x)) > ~ R(x)) & 
26322  248 
(ALL x. (Q(x) > ~ S(x)) > P(x) & R(x)) 
249 
> (ALL x. ~~S(x))" 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

250 
by (tactic "IntPr.fast_tac @{context} 1") 
26322  251 

252 
text "Problem 31" 

61337  253 
schematic_goal "?p : ~(EX x. P(x) & (Q(x)  R(x))) & 
26322  254 
(EX x. L(x) & P(x)) & 
255 
(ALL x. ~ R(x) > M(x)) 

256 
> (EX x. L(x) & M(x))" 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

257 
by (tactic "IntPr.fast_tac @{context} 1") 
26322  258 

259 
text "Problem 32" 

61337  260 
schematic_goal "?p : (ALL x. P(x) & (Q(x)R(x))>S(x)) & 
26322  261 
(ALL x. S(x) & R(x) > L(x)) & 
262 
(ALL x. M(x) > R(x)) 

263 
> (ALL x. P(x) & M(x) > L(x))" 

62020  264 
by (tactic "IntPr.best_tac @{context} 1") \<comment> slow 
26322  265 

266 
text "Problem 39" 

61337  267 
schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <> ~F(y,y))" 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

268 
by (tactic "IntPr.best_tac @{context} 1") 
26322  269 

270 
text "Problem 40. AMENDED" 

61337  271 
schematic_goal "?p : (EX y. ALL x. F(x,y) <> F(x,x)) > 
26322  272 
~(ALL x. EX y. ALL z. F(z,y) <> ~ F(z,x))" 
62020  273 
by (tactic "IntPr.best_tac @{context} 1") \<comment> slow 
26322  274 

275 
text "Problem 44" 

61337  276 
schematic_goal "?p : (ALL x. f(x) > 
26322  277 
(EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & 
278 
(EX x. j(x) & (ALL y. g(y) > h(x,y))) 

279 
> (EX x. j(x) & ~f(x))" 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

280 
by (tactic "IntPr.best_tac @{context} 1") 
26322  281 

282 
text "Problem 48" 

61337  283 
schematic_goal "?p : (a=b  c=d) & (a=c  b=d) > a=d  b=c" 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

284 
by (tactic "IntPr.best_tac @{context} 1") 
26322  285 

286 
text "Problem 51" 

61337  287 
schematic_goal 
26322  288 
"?p : (EX z w. ALL x y. P(x,y) <> (x=z & y=w)) > 
289 
(EX z. ALL x. EX w. (ALL y. P(x,y) <> y=w) <> x=z)" 

62020  290 
by (tactic "IntPr.best_tac @{context} 1") \<comment> \<open>60 seconds\<close> 
26322  291 

292 
text "Problem 56" 

61337  293 
schematic_goal "?p : (ALL x. (EX y. P(y) & x=f(y)) > P(x)) <> (ALL x. P(x) > P(f(x)))" 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

294 
by (tactic "IntPr.best_tac @{context} 1") 
26322  295 

296 
text "Problem 57" 

61337  297 
schematic_goal 
26322  298 
"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & 
299 
(ALL x y z. P(x,y) & P(y,z) > P(x,z)) > P(f(a,b), f(a,c))" 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

300 
by (tactic "IntPr.best_tac @{context} 1") 
26322  301 

302 
text "Problem 60" 

61337  303 
schematic_goal "?p : ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))" 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
36319
diff
changeset

304 
by (tactic "IntPr.best_tac @{context} 1") 
26322  305 

306 
end 