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