src/HOL/ex/Intuitionistic.thy
 author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 41460 ea56b98aee83 child 58889 5b7a9633cfa8 permissions -rw-r--r--
introduce order topology
 berghofe@12450 ` 1` ```(* Title: HOL/ex/Intuitionistic.thy ``` berghofe@12450 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` berghofe@12450 ` 3` ``` Copyright 1991 University of Cambridge ``` berghofe@12450 ` 4` berghofe@12450 ` 5` ```Taken from FOL/ex/int.ML ``` berghofe@12450 ` 6` ```*) ``` berghofe@12450 ` 7` wenzelm@17388 ` 8` ```header {* Higher-Order Logic: Intuitionistic predicate calculus problems *} ``` wenzelm@17388 ` 9` haftmann@16417 ` 10` ```theory Intuitionistic imports Main begin ``` berghofe@12450 ` 11` berghofe@12450 ` 12` berghofe@12450 ` 13` ```(*Metatheorem (for PROPOSITIONAL formulae...): ``` berghofe@12450 ` 14` ``` P is classically provable iff ~~P is intuitionistically provable. ``` berghofe@12450 ` 15` ``` Therefore ~P is classically provable iff it is intuitionistically provable. ``` berghofe@12450 ` 16` berghofe@12450 ` 17` ```Proof: Let Q be the conjuction of the propositions A|~A, one for each atom A ``` berghofe@12450 ` 18` ```in P. Now ~~Q is intuitionistically provable because ~~(A|~A) is and because ``` berghofe@12450 ` 19` ```~~ distributes over &. If P is provable classically, then clearly Q-->P is ``` berghofe@12450 ` 20` ```provable intuitionistically, so ~~(Q-->P) is also provable intuitionistically. ``` berghofe@12450 ` 21` ```The latter is intuitionistically equivalent to ~~Q-->~~P, hence to ~~P, since ``` berghofe@12450 ` 22` ```~~Q is intuitionistically provable. Finally, if P is a negation then ~~P is ``` berghofe@12450 ` 23` ```intuitionstically equivalent to P. [Andy Pitts] *) ``` berghofe@12450 ` 24` berghofe@12450 ` 25` ```lemma "(~~(P&Q)) = ((~~P) & (~~Q))" ``` nipkow@17589 ` 26` ``` by iprover ``` berghofe@12450 ` 27` berghofe@12450 ` 28` ```lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)" ``` nipkow@17589 ` 29` ``` by iprover ``` berghofe@12450 ` 30` berghofe@12450 ` 31` ```(* ~~ does NOT distribute over | *) ``` berghofe@12450 ` 32` berghofe@12450 ` 33` ```lemma "(~~(P-->Q)) = (~~P --> ~~Q)" ``` nipkow@17589 ` 34` ``` by iprover ``` berghofe@12450 ` 35` berghofe@12450 ` 36` ```lemma "(~~~P) = (~P)" ``` nipkow@17589 ` 37` ``` by iprover ``` berghofe@12450 ` 38` berghofe@12450 ` 39` ```lemma "~~((P --> Q | R) --> (P-->Q) | (P-->R))" ``` nipkow@17589 ` 40` ``` by iprover ``` berghofe@12450 ` 41` berghofe@12450 ` 42` ```lemma "(P=Q) = (Q=P)" ``` nipkow@17589 ` 43` ``` by iprover ``` berghofe@12450 ` 44` berghofe@12450 ` 45` ```lemma "((P --> (Q | (Q-->R))) --> R) --> R" ``` nipkow@17589 ` 46` ``` by iprover ``` berghofe@12450 ` 47` berghofe@12450 ` 48` ```lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J) ``` berghofe@12450 ` 49` ``` --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C) ``` berghofe@12450 ` 50` ``` --> (((F-->A)-->B) --> I) --> E" ``` nipkow@17589 ` 51` ``` by iprover ``` berghofe@12450 ` 52` berghofe@12450 ` 53` berghofe@12450 ` 54` ```(* Lemmas for the propositional double-negation translation *) ``` berghofe@12450 ` 55` berghofe@12450 ` 56` ```lemma "P --> ~~P" ``` nipkow@17589 ` 57` ``` by iprover ``` berghofe@12450 ` 58` berghofe@12450 ` 59` ```lemma "~~(~~P --> P)" ``` nipkow@17589 ` 60` ``` by iprover ``` berghofe@12450 ` 61` berghofe@12450 ` 62` ```lemma "~~P & ~~(P --> Q) --> ~~Q" ``` nipkow@17589 ` 63` ``` by iprover ``` berghofe@12450 ` 64` berghofe@12450 ` 65` berghofe@12450 ` 66` ```(* de Bruijn formulae *) ``` berghofe@12450 ` 67` berghofe@12450 ` 68` ```(*de Bruijn formula with three predicates*) ``` berghofe@12450 ` 69` ```lemma "((P=Q) --> P&Q&R) & ``` berghofe@12450 ` 70` ``` ((Q=R) --> P&Q&R) & ``` berghofe@12450 ` 71` ``` ((R=P) --> P&Q&R) --> P&Q&R" ``` nipkow@17589 ` 72` ``` by iprover ``` berghofe@12450 ` 73` berghofe@12450 ` 74` ```(*de Bruijn formula with five predicates*) ``` berghofe@12450 ` 75` ```lemma "((P=Q) --> P&Q&R&S&T) & ``` berghofe@12450 ` 76` ``` ((Q=R) --> P&Q&R&S&T) & ``` berghofe@12450 ` 77` ``` ((R=S) --> P&Q&R&S&T) & ``` berghofe@12450 ` 78` ``` ((S=T) --> P&Q&R&S&T) & ``` berghofe@12450 ` 79` ``` ((T=P) --> P&Q&R&S&T) --> P&Q&R&S&T" ``` nipkow@17589 ` 80` ``` by iprover ``` berghofe@12450 ` 81` berghofe@12450 ` 82` berghofe@12450 ` 83` ```(*** Problems from Sahlin, Franzen and Haridi, ``` berghofe@12450 ` 84` ``` An Intuitionistic Predicate Logic Theorem Prover. ``` berghofe@12450 ` 85` ``` J. Logic and Comp. 2 (5), October 1992, 619-656. ``` berghofe@12450 ` 86` ```***) ``` berghofe@12450 ` 87` berghofe@12450 ` 88` ```(*Problem 1.1*) ``` berghofe@12450 ` 89` ```lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) = ``` berghofe@12450 ` 90` ``` (ALL z. EX y. ALL x. p(x) & q(y) & r(z))" ``` nipkow@17589 ` 91` ``` by (iprover del: allE elim 2: allE') ``` berghofe@12450 ` 92` berghofe@12450 ` 93` ```(*Problem 3.1*) ``` berghofe@12450 ` 94` ```lemma "~ (EX x. ALL y. p y x = (~ p x x))" ``` nipkow@17589 ` 95` ``` by iprover ``` berghofe@12450 ` 96` berghofe@12450 ` 97` berghofe@12450 ` 98` ```(* Intuitionistic FOL: propositional problems based on Pelletier. *) ``` berghofe@12450 ` 99` berghofe@12450 ` 100` ```(* Problem ~~1 *) ``` berghofe@12450 ` 101` ```lemma "~~((P-->Q) = (~Q --> ~P))" ``` nipkow@17589 ` 102` ``` by iprover ``` berghofe@12450 ` 103` berghofe@12450 ` 104` ```(* Problem ~~2 *) ``` berghofe@12450 ` 105` ```lemma "~~(~~P = P)" ``` nipkow@17589 ` 106` ``` by iprover ``` berghofe@12450 ` 107` berghofe@12450 ` 108` ```(* Problem 3 *) ``` berghofe@12450 ` 109` ```lemma "~(P-->Q) --> (Q-->P)" ``` nipkow@17589 ` 110` ``` by iprover ``` berghofe@12450 ` 111` berghofe@12450 ` 112` ```(* Problem ~~4 *) ``` berghofe@12450 ` 113` ```lemma "~~((~P-->Q) = (~Q --> P))" ``` nipkow@17589 ` 114` ``` by iprover ``` berghofe@12450 ` 115` berghofe@12450 ` 116` ```(* Problem ~~5 *) ``` berghofe@12450 ` 117` ```lemma "~~((P|Q-->P|R) --> P|(Q-->R))" ``` nipkow@17589 ` 118` ``` by iprover ``` berghofe@12450 ` 119` berghofe@12450 ` 120` ```(* Problem ~~6 *) ``` berghofe@12450 ` 121` ```lemma "~~(P | ~P)" ``` nipkow@17589 ` 122` ``` by iprover ``` berghofe@12450 ` 123` berghofe@12450 ` 124` ```(* Problem ~~7 *) ``` berghofe@12450 ` 125` ```lemma "~~(P | ~~~P)" ``` nipkow@17589 ` 126` ``` by iprover ``` berghofe@12450 ` 127` berghofe@12450 ` 128` ```(* Problem ~~8. Peirce's law *) ``` berghofe@12450 ` 129` ```lemma "~~(((P-->Q) --> P) --> P)" ``` nipkow@17589 ` 130` ``` by iprover ``` berghofe@12450 ` 131` berghofe@12450 ` 132` ```(* Problem 9 *) ``` berghofe@12450 ` 133` ```lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" ``` nipkow@17589 ` 134` ``` by iprover ``` berghofe@12450 ` 135` berghofe@12450 ` 136` ```(* Problem 10 *) ``` berghofe@12450 ` 137` ```lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P=Q)" ``` nipkow@17589 ` 138` ``` by iprover ``` berghofe@12450 ` 139` berghofe@12450 ` 140` ```(* 11. Proved in each direction (incorrectly, says Pelletier!!) *) ``` berghofe@12450 ` 141` ```lemma "P=P" ``` nipkow@17589 ` 142` ``` by iprover ``` berghofe@12450 ` 143` berghofe@12450 ` 144` ```(* Problem ~~12. Dijkstra's law *) ``` berghofe@12450 ` 145` ```lemma "~~(((P = Q) = R) = (P = (Q = R)))" ``` nipkow@17589 ` 146` ``` by iprover ``` berghofe@12450 ` 147` berghofe@12450 ` 148` ```lemma "((P = Q) = R) --> ~~(P = (Q = R))" ``` nipkow@17589 ` 149` ``` by iprover ``` berghofe@12450 ` 150` berghofe@12450 ` 151` ```(* Problem 13. Distributive law *) ``` berghofe@12450 ` 152` ```lemma "(P | (Q & R)) = ((P | Q) & (P | R))" ``` nipkow@17589 ` 153` ``` by iprover ``` berghofe@12450 ` 154` berghofe@12450 ` 155` ```(* Problem ~~14 *) ``` berghofe@12450 ` 156` ```lemma "~~((P = Q) = ((Q | ~P) & (~Q|P)))" ``` nipkow@17589 ` 157` ``` by iprover ``` berghofe@12450 ` 158` berghofe@12450 ` 159` ```(* Problem ~~15 *) ``` berghofe@12450 ` 160` ```lemma "~~((P --> Q) = (~P | Q))" ``` nipkow@17589 ` 161` ``` by iprover ``` berghofe@12450 ` 162` berghofe@12450 ` 163` ```(* Problem ~~16 *) ``` berghofe@12450 ` 164` ```lemma "~~((P-->Q) | (Q-->P))" ``` nipkow@17589 ` 165` ```by iprover ``` berghofe@12450 ` 166` berghofe@12450 ` 167` ```(* Problem ~~17 *) ``` berghofe@12450 ` 168` ```lemma "~~(((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S)))" ``` berghofe@12450 ` 169` ``` oops ``` berghofe@12450 ` 170` berghofe@12450 ` 171` ```(*Dijkstra's "Golden Rule"*) ``` berghofe@12450 ` 172` ```lemma "(P&Q) = (P = (Q = (P|Q)))" ``` nipkow@17589 ` 173` ``` by iprover ``` berghofe@12450 ` 174` berghofe@12450 ` 175` berghofe@12450 ` 176` ```(****Examples with quantifiers****) ``` berghofe@12450 ` 177` berghofe@12450 ` 178` ```(* The converse is classical in the following implications... *) ``` berghofe@12450 ` 179` berghofe@12450 ` 180` ```lemma "(EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q" ``` nipkow@17589 ` 181` ``` by iprover ``` berghofe@12450 ` 182` berghofe@12450 ` 183` ```lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)" ``` nipkow@17589 ` 184` ``` by iprover ``` berghofe@12450 ` 185` berghofe@12450 ` 186` ```lemma "((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))" ``` nipkow@17589 ` 187` ``` by iprover ``` berghofe@12450 ` 188` berghofe@12450 ` 189` ```lemma "(ALL x. P(x)) | Q --> (ALL x. P(x) | Q)" ``` nipkow@17589 ` 190` ``` by iprover ``` berghofe@12450 ` 191` berghofe@12450 ` 192` ```lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))" ``` nipkow@17589 ` 193` ``` by iprover ``` berghofe@12450 ` 194` berghofe@12450 ` 195` berghofe@12450 ` 196` ```(* Hard examples with quantifiers *) ``` berghofe@12450 ` 197` berghofe@12450 ` 198` ```(*The ones that have not been proved are not known to be valid! ``` berghofe@12450 ` 199` ``` Some will require quantifier duplication -- not currently available*) ``` berghofe@12450 ` 200` berghofe@12450 ` 201` ```(* Problem ~~19 *) ``` berghofe@12450 ` 202` ```lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" ``` nipkow@17589 ` 203` ``` by iprover ``` berghofe@12450 ` 204` berghofe@12450 ` 205` ```(* Problem 20 *) ``` berghofe@12450 ` 206` ```lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) ``` berghofe@12450 ` 207` ``` --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))" ``` nipkow@17589 ` 208` ``` by iprover ``` berghofe@12450 ` 209` berghofe@12450 ` 210` ```(* Problem 21 *) ``` berghofe@12450 ` 211` ```lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P=Q(x))" ``` nipkow@17589 ` 212` ``` by iprover ``` berghofe@12450 ` 213` berghofe@12450 ` 214` ```(* Problem 22 *) ``` berghofe@12450 ` 215` ```lemma "(ALL x. P = Q(x)) --> (P = (ALL x. Q(x)))" ``` nipkow@17589 ` 216` ``` by iprover ``` berghofe@12450 ` 217` berghofe@12450 ` 218` ```(* Problem ~~23 *) ``` berghofe@12450 ` 219` ```lemma "~~ ((ALL x. P | Q(x)) = (P | (ALL x. Q(x))))" ``` nipkow@17589 ` 220` ``` by iprover ``` berghofe@12450 ` 221` berghofe@12450 ` 222` ```(* Problem 25 *) ``` berghofe@12450 ` 223` ```lemma "(EX x. P(x)) & ``` berghofe@12450 ` 224` ``` (ALL x. L(x) --> ~ (M(x) & R(x))) & ``` berghofe@12450 ` 225` ``` (ALL x. P(x) --> (M(x) & L(x))) & ``` berghofe@12450 ` 226` ``` ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) ``` berghofe@12450 ` 227` ``` --> (EX x. Q(x)&P(x))" ``` nipkow@17589 ` 228` ``` by iprover ``` berghofe@12450 ` 229` berghofe@12450 ` 230` ```(* Problem 27 *) ``` berghofe@12450 ` 231` ```lemma "(EX x. P(x) & ~Q(x)) & ``` berghofe@12450 ` 232` ``` (ALL x. P(x) --> R(x)) & ``` berghofe@12450 ` 233` ``` (ALL x. M(x) & L(x) --> P(x)) & ``` berghofe@12450 ` 234` ``` ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) ``` berghofe@12450 ` 235` ``` --> (ALL x. M(x) --> ~L(x))" ``` nipkow@17589 ` 236` ``` by iprover ``` berghofe@12450 ` 237` berghofe@12450 ` 238` ```(* Problem ~~28. AMENDED *) ``` berghofe@12450 ` 239` ```lemma "(ALL x. P(x) --> (ALL x. Q(x))) & ``` berghofe@12450 ` 240` ``` (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & ``` berghofe@12450 ` 241` ``` (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x))) ``` berghofe@12450 ` 242` ``` --> (ALL x. P(x) & L(x) --> M(x))" ``` nipkow@17589 ` 243` ``` by iprover ``` berghofe@12450 ` 244` berghofe@12450 ` 245` ```(* Problem 29. Essentially the same as Principia Mathematica *11.71 *) ``` berghofe@12450 ` 246` ```lemma "(((EX x. P(x)) & (EX y. Q(y))) --> ``` berghofe@12450 ` 247` ``` (((ALL x. (P(x) --> R(x))) & (ALL y. (Q(y) --> S(y)))) = ``` berghofe@12450 ` 248` ``` (ALL x y. ((P(x) & Q(y)) --> (R(x) & S(y))))))" ``` nipkow@17589 ` 249` ``` by iprover ``` berghofe@12450 ` 250` berghofe@12450 ` 251` ```(* Problem ~~30 *) ``` berghofe@12450 ` 252` ```lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) & ``` berghofe@12450 ` 253` ``` (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) ``` berghofe@12450 ` 254` ``` --> (ALL x. ~~S(x))" ``` nipkow@17589 ` 255` ``` by iprover ``` berghofe@12450 ` 256` berghofe@12450 ` 257` ```(* Problem 31 *) ``` berghofe@12450 ` 258` ```lemma "~(EX x. P(x) & (Q(x) | R(x))) & ``` berghofe@12450 ` 259` ``` (EX x. L(x) & P(x)) & ``` berghofe@12450 ` 260` ``` (ALL x. ~ R(x) --> M(x)) ``` berghofe@12450 ` 261` ``` --> (EX x. L(x) & M(x))" ``` nipkow@17589 ` 262` ``` by iprover ``` berghofe@12450 ` 263` berghofe@12450 ` 264` ```(* Problem 32 *) ``` berghofe@12450 ` 265` ```lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & ``` berghofe@12450 ` 266` ``` (ALL x. S(x) & R(x) --> L(x)) & ``` berghofe@12450 ` 267` ``` (ALL x. M(x) --> R(x)) ``` berghofe@12450 ` 268` ``` --> (ALL x. P(x) & M(x) --> L(x))" ``` nipkow@17589 ` 269` ``` by iprover ``` berghofe@12450 ` 270` berghofe@12450 ` 271` ```(* Problem ~~33 *) ``` berghofe@12450 ` 272` ```lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c))) = ``` berghofe@12450 ` 273` ``` (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))" ``` berghofe@12450 ` 274` ``` oops ``` berghofe@12450 ` 275` berghofe@12450 ` 276` ```(* Problem 36 *) ``` berghofe@12450 ` 277` ```lemma ``` berghofe@12450 ` 278` ``` "(ALL x. EX y. J x y) & ``` berghofe@12450 ` 279` ``` (ALL x. EX y. G x y) & ``` berghofe@12450 ` 280` ``` (ALL x y. J x y | G x y --> (ALL z. J y z | G y z --> H x z)) ``` berghofe@12450 ` 281` ``` --> (ALL x. EX y. H x y)" ``` nipkow@17589 ` 282` ``` by iprover ``` berghofe@12450 ` 283` berghofe@12450 ` 284` ```(* Problem 39 *) ``` berghofe@12450 ` 285` ```lemma "~ (EX x. ALL y. F y x = (~F y y))" ``` nipkow@17589 ` 286` ``` by iprover ``` berghofe@12450 ` 287` berghofe@12450 ` 288` ```(* Problem 40. AMENDED *) ``` berghofe@12450 ` 289` ```lemma "(EX y. ALL x. F x y = F x x) --> ``` berghofe@12450 ` 290` ``` ~(ALL x. EX y. ALL z. F z y = (~ F z x))" ``` nipkow@17589 ` 291` ``` by iprover ``` berghofe@12450 ` 292` berghofe@12450 ` 293` ```(* Problem 44 *) ``` berghofe@12450 ` 294` ```lemma "(ALL x. f(x) --> ``` berghofe@12450 ` 295` ``` (EX y. g(y) & h x y & (EX y. g(y) & ~ h x y))) & ``` berghofe@12450 ` 296` ``` (EX x. j(x) & (ALL y. g(y) --> h x y)) ``` berghofe@12450 ` 297` ``` --> (EX x. j(x) & ~f(x))" ``` nipkow@17589 ` 298` ``` by iprover ``` berghofe@12450 ` 299` berghofe@12450 ` 300` ```(* Problem 48 *) ``` berghofe@12450 ` 301` ```lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c" ``` nipkow@17589 ` 302` ``` by iprover ``` berghofe@12450 ` 303` berghofe@12450 ` 304` ```(* Problem 51 *) ``` berghofe@12450 ` 305` ```lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) --> ``` berghofe@12450 ` 306` ``` (EX z. (ALL x. (EX w. ((ALL y. (P x y = (y = w))) = (x = z))))))" ``` nipkow@17589 ` 307` ``` by iprover ``` berghofe@12450 ` 308` berghofe@12450 ` 309` ```(* Problem 52 *) ``` berghofe@12450 ` 310` ```(*Almost the same as 51. *) ``` berghofe@12450 ` 311` ```lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) --> ``` berghofe@12450 ` 312` ``` (EX w. (ALL y. (EX z. ((ALL x. (P x y = (x = z))) = (y = w))))))" ``` nipkow@17589 ` 313` ``` by iprover ``` berghofe@12450 ` 314` berghofe@12450 ` 315` ```(* Problem 56 *) ``` berghofe@12450 ` 316` ```lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) = (ALL x. P(x) --> P(f(x)))" ``` nipkow@17589 ` 317` ``` by iprover ``` berghofe@12450 ` 318` berghofe@12450 ` 319` ```(* Problem 57 *) ``` berghofe@12450 ` 320` ```lemma "P (f a b) (f b c) & P (f b c) (f a c) & ``` berghofe@12450 ` 321` ``` (ALL x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)" ``` nipkow@17589 ` 322` ``` by iprover ``` berghofe@12450 ` 323` berghofe@12450 ` 324` ```(* Problem 60 *) ``` berghofe@12450 ` 325` ```lemma "ALL x. P x (f x) = (EX y. (ALL z. P z y --> P z (f x)) & P x y)" ``` nipkow@17589 ` 326` ``` by iprover ``` berghofe@12450 ` 327` berghofe@12450 ` 328` ```end ```