26322

1 
(* Title: FOLP/ex/Intuitionistic.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Intuitionistic FirstOrder Logic.


7 


8 
Singlestep commands:


9 
by (IntPr.step_tac 1)


10 
by (biresolve_tac safe_brls 1);


11 
by (biresolve_tac haz_brls 1);


12 
by (assume_tac 1);


13 
by (IntPr.safe_tac 1);


14 
by (IntPr.mp_tac 1);


15 
by (IntPr.fast_tac 1);


16 
*)


17 


18 
(*Note: for PROPOSITIONAL formulae...


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


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


21 


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


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


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


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


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


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


28 
*)


29 


30 
theory Intuitionistic


31 
imports IFOLP


32 
begin


33 


34 
lemma "?p : ~~(P&Q) <> ~~P & ~~Q"


35 
by (tactic {* IntPr.fast_tac 1 *})


36 


37 
lemma "?p : ~~~P <> ~P"


38 
by (tactic {* IntPr.fast_tac 1 *})


39 


40 
lemma "?p : ~~((P > Q  R) > (P>Q)  (P>R))"


41 
by (tactic {* IntPr.fast_tac 1 *})


42 


43 
lemma "?p : (P<>Q) <> (Q<>P)"


44 
by (tactic {* IntPr.fast_tac 1 *})


45 


46 


47 
subsection {* Lemmas for the propositional doublenegation translation *}


48 


49 
lemma "?p : P > ~~P"


50 
by (tactic {* IntPr.fast_tac 1 *})


51 


52 
lemma "?p : ~~(~~P > P)"


53 
by (tactic {* IntPr.fast_tac 1 *})


54 


55 
lemma "?p : ~~P & ~~(P > Q) > ~~Q"


56 
by (tactic {* IntPr.fast_tac 1 *})


57 


58 


59 
subsection {* The following are classically but not constructively valid *}


60 


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


62 
lemma "?p : ((P>Q) > P) > P"


63 
apply (tactic {* IntPr.fast_tac 1 *})?


64 
oops


65 


66 
lemma "?p : (P&Q>R) > (P>R)  (Q>R)"


67 
apply (tactic {* IntPr.fast_tac 1 *})?


68 
oops


69 


70 


71 
subsection {* Intuitionistic FOL: propositional problems based on Pelletier *}


72 


73 
text "Problem ~~1"


74 
lemma "?p : ~~((P>Q) <> (~Q > ~P))"


75 
by (tactic {* IntPr.fast_tac 1 *})


76 


77 
text "Problem ~~2"


78 
lemma "?p : ~~(~~P <> P)"


79 
by (tactic {* IntPr.fast_tac 1 *})


80 


81 
text "Problem 3"


82 
lemma "?p : ~(P>Q) > (Q>P)"


83 
by (tactic {* IntPr.fast_tac 1 *})


84 


85 
text "Problem ~~4"


86 
lemma "?p : ~~((~P>Q) <> (~Q > P))"


87 
by (tactic {* IntPr.fast_tac 1 *})


88 


89 
text "Problem ~~5"


90 
lemma "?p : ~~((PQ>PR) > P(Q>R))"


91 
by (tactic {* IntPr.fast_tac 1 *})


92 


93 
text "Problem ~~6"


94 
lemma "?p : ~~(P  ~P)"


95 
by (tactic {* IntPr.fast_tac 1 *})


96 


97 
text "Problem ~~7"


98 
lemma "?p : ~~(P  ~~~P)"


99 
by (tactic {* IntPr.fast_tac 1 *})


100 


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


102 
lemma "?p : ~~(((P>Q) > P) > P)"


103 
by (tactic {* IntPr.fast_tac 1 *})


104 


105 
text "Problem 9"


106 
lemma "?p : ((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"


107 
by (tactic {* IntPr.fast_tac 1 *})


108 


109 
text "Problem 10"


110 
lemma "?p : (Q>R) > (R>P&Q) > (P>(QR)) > (P<>Q)"


111 
by (tactic {* IntPr.fast_tac 1 *})


112 


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


114 
lemma "?p : P<>P"


115 
by (tactic {* IntPr.fast_tac 1 *})


116 


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


118 
lemma "?p : ~~(((P <> Q) <> R) <> (P <> (Q <> R)))"


119 
by (tactic {* IntPr.fast_tac 1 *})


120 


121 
lemma "?p : ((P <> Q) <> R) > ~~(P <> (Q <> R))"


122 
by (tactic {* IntPr.fast_tac 1 *})


123 


124 
text "Problem 13. Distributive law"


125 
lemma "?p : P  (Q & R) <> (P  Q) & (P  R)"


126 
by (tactic {* IntPr.fast_tac 1 *})


127 


128 
text "Problem ~~14"


129 
lemma "?p : ~~((P <> Q) <> ((Q  ~P) & (~QP)))"


130 
by (tactic {* IntPr.fast_tac 1 *})


131 


132 
text "Problem ~~15"


133 
lemma "?p : ~~((P > Q) <> (~P  Q))"


134 
by (tactic {* IntPr.fast_tac 1 *})


135 


136 
text "Problem ~~16"


137 
lemma "?p : ~~((P>Q)  (Q>P))"


138 
by (tactic {* IntPr.fast_tac 1 *})


139 


140 
text "Problem ~~17"


141 
lemma "?p : ~~(((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S)))"


142 
by (tactic {* IntPr.fast_tac 1 *})  slow


143 


144 


145 
subsection {* Examples with quantifiers *}


146 


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


148 


149 
lemma "?p : (EX x. P(x)>Q) > (ALL x. P(x)) > Q"


150 
by (tactic {* IntPr.fast_tac 1 *})


151 


152 
lemma "?p : ((ALL x. P(x))>Q) > ~ (ALL x. P(x) & ~Q)"


153 
by (tactic {* IntPr.fast_tac 1 *})


154 


155 
lemma "?p : ((ALL x. ~P(x))>Q) > ~ (ALL x. ~ (P(x)Q))"


156 
by (tactic {* IntPr.fast_tac 1 *})


157 


158 
lemma "?p : (ALL x. P(x))  Q > (ALL x. P(x)  Q)"


159 
by (tactic {* IntPr.fast_tac 1 *})


160 


161 
lemma "?p : (EX x. P > Q(x)) > (P > (EX x. Q(x)))"


162 
by (tactic {* IntPr.fast_tac 1 *})


163 


164 


165 
text "The following are not constructively valid!"


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


167 


168 
lemma "?p : ((ALL x. P(x))>Q) > (EX x. P(x)>Q)"


169 
apply (tactic {* IntPr.fast_tac 1 *})?


170 
oops


171 


172 
lemma "?p : (P > (EX x. Q(x))) > (EX x. P>Q(x))"


173 
apply (tactic {* IntPr.fast_tac 1 *})?


174 
oops


175 


176 
lemma "?p : (ALL x. P(x)  Q) > ((ALL x. P(x))  Q)"


177 
apply (tactic {* IntPr.fast_tac 1 *})?


178 
oops


179 


180 
lemma "?p : (ALL x. ~~P(x)) > ~~(ALL x. P(x))"


181 
apply (tactic {* IntPr.fast_tac 1 *})?


182 
oops


183 


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


185 
lemma "?p : EX x. Q(x) > (ALL x. Q(x))"


186 
apply (tactic {* IntPr.fast_tac 1 *})?


187 
oops


188 


189 


190 
subsection "Hard examples with quantifiers"


191 


192 
text {*


193 
The ones that have not been proved are not known to be valid!


194 
Some will require quantifier duplication  not currently available.


195 
*}


196 


197 
text "Problem ~~18"


198 
lemma "?p : ~~(EX y. ALL x. P(y)>P(x))" oops


199 
(*NOT PROVED*)


200 


201 
text "Problem ~~19"


202 
lemma "?p : ~~(EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x)))" oops


203 
(*NOT PROVED*)


204 


205 
text "Problem 20"


206 
lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w)))


207 
> (EX x y. P(x) & Q(y)) > (EX z. R(z))"


208 
by (tactic {* IntPr.fast_tac 1 *})


209 


210 
text "Problem 21"


211 
lemma "?p : (EX x. P>Q(x)) & (EX x. Q(x)>P) > ~~(EX x. P<>Q(x))" oops


212 
(*NOT PROVED*)


213 


214 
text "Problem 22"


215 
lemma "?p : (ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))"


216 
by (tactic {* IntPr.fast_tac 1 *})


217 


218 
text "Problem ~~23"


219 
lemma "?p : ~~ ((ALL x. P  Q(x)) <> (P  (ALL x. Q(x))))"


220 
by (tactic {* IntPr.fast_tac 1 *})


221 


222 
text "Problem 24"


223 
lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) &


224 
(~(EX x. P(x)) > (EX x. Q(x))) & (ALL x. Q(x)R(x) > S(x))


225 
> ~~(EX x. P(x)&R(x))"


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


227 
apply (tactic "IntPr.safe_tac")


228 
apply (erule impE)


229 
apply (tactic "IntPr.fast_tac 1")


230 
apply (tactic "IntPr.fast_tac 1")


231 
done


232 


233 
text "Problem 25"


234 
lemma "?p : (EX x. P(x)) &


235 
(ALL x. L(x) > ~ (M(x) & R(x))) &


236 
(ALL x. P(x) > (M(x) & L(x))) &


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


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


239 
by (tactic "IntPr.best_tac 1")


240 


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


242 
lemma "?p : (EX x. P(x)) & (EX y. Q(y))


243 
> ((ALL x. P(x)>R(x)) & (ALL y. Q(y)>S(y)) <>


244 
(ALL x y. P(x) & Q(y) > R(x) & S(y)))"


245 
by (tactic "IntPr.fast_tac 1")


246 


247 
text "Problem ~~30"


248 
lemma "?p : (ALL x. (P(x)  Q(x)) > ~ R(x)) &


249 
(ALL x. (Q(x) > ~ S(x)) > P(x) & R(x))


250 
> (ALL x. ~~S(x))"


251 
by (tactic "IntPr.fast_tac 1")


252 


253 
text "Problem 31"


254 
lemma "?p : ~(EX x. P(x) & (Q(x)  R(x))) &


255 
(EX x. L(x) & P(x)) &


256 
(ALL x. ~ R(x) > M(x))


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


258 
by (tactic "IntPr.fast_tac 1")


259 


260 
text "Problem 32"


261 
lemma "?p : (ALL x. P(x) & (Q(x)R(x))>S(x)) &


262 
(ALL x. S(x) & R(x) > L(x)) &


263 
(ALL x. M(x) > R(x))


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


265 
by (tactic "IntPr.best_tac 1")  slow


266 


267 
text "Problem 39"


268 
lemma "?p : ~ (EX x. ALL y. F(y,x) <> ~F(y,y))"


269 
by (tactic "IntPr.best_tac 1")


270 


271 
text "Problem 40. AMENDED"


272 
lemma "?p : (EX y. ALL x. F(x,y) <> F(x,x)) >


273 
~(ALL x. EX y. ALL z. F(z,y) <> ~ F(z,x))"


274 
by (tactic "IntPr.best_tac 1")  slow


275 


276 
text "Problem 44"


277 
lemma "?p : (ALL x. f(x) >


278 
(EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &


279 
(EX x. j(x) & (ALL y. g(y) > h(x,y)))


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


281 
by (tactic "IntPr.best_tac 1")


282 


283 
text "Problem 48"


284 
lemma "?p : (a=b  c=d) & (a=c  b=d) > a=d  b=c"


285 
by (tactic "IntPr.best_tac 1")


286 


287 
text "Problem 51"


288 
lemma


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


290 
(EX z. ALL x. EX w. (ALL y. P(x,y) <> y=w) <> x=z)"


291 
by (tactic "IntPr.best_tac 1")  {*60 seconds*}


292 


293 
text "Problem 56"


294 
lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) > P(x)) <> (ALL x. P(x) > P(f(x)))"


295 
by (tactic "IntPr.best_tac 1")


296 


297 
text "Problem 57"


298 
lemma


299 
"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &


300 
(ALL x y z. P(x,y) & P(y,z) > P(x,z)) > P(f(a,b), f(a,c))"


301 
by (tactic "IntPr.best_tac 1")


302 


303 
text "Problem 60"


304 
lemma "?p : ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))"


305 
by (tactic "IntPr.best_tac 1")


306 


307 
end
