src/FOLP/ex/foundn.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 1459 d12da312eff4
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	FOL/ex/foundn
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
writeln"File FOL/ex/foundn.";
clasohm@0
    10
clasohm@0
    11
goal IFOLP.thy "?p : A&B  --> (C-->A&C)";
clasohm@0
    12
by (resolve_tac [impI] 1);
clasohm@0
    13
by (resolve_tac [impI] 1);
clasohm@0
    14
by (resolve_tac [conjI] 1);
clasohm@0
    15
by (assume_tac 2);
clasohm@0
    16
by (resolve_tac [conjunct1] 1);
clasohm@0
    17
by (assume_tac 1);
clasohm@0
    18
result();
clasohm@0
    19
clasohm@0
    20
(*A form of conj-elimination*)
clasohm@0
    21
val prems = 
clasohm@0
    22
goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
clasohm@0
    23
by (resolve_tac prems 1);
clasohm@0
    24
by (resolve_tac [conjunct1] 1);
clasohm@0
    25
by (resolve_tac prems 1);
clasohm@0
    26
by (resolve_tac [conjunct2] 1);
clasohm@0
    27
by (resolve_tac prems 1);
clasohm@0
    28
result();
clasohm@0
    29
clasohm@0
    30
clasohm@0
    31
val prems = 
clasohm@0
    32
goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
clasohm@0
    33
by (resolve_tac prems 1);
clasohm@0
    34
by (resolve_tac [notI] 1);
clasohm@0
    35
by (res_inst_tac [ ("P", "~B") ]  notE  1);
clasohm@0
    36
by (resolve_tac [notI] 2);
clasohm@0
    37
by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
clasohm@0
    38
by (assume_tac 2);
clasohm@0
    39
by (resolve_tac [disjI1] 2);
clasohm@0
    40
by (assume_tac 2);
clasohm@0
    41
by (resolve_tac [notI] 1);
clasohm@0
    42
by (res_inst_tac [ ("P", "B | ~B") ]  notE  1);
clasohm@0
    43
by (assume_tac 1);
clasohm@0
    44
by (resolve_tac [disjI2] 1);
clasohm@0
    45
by (assume_tac 1);
clasohm@0
    46
result();
clasohm@0
    47
clasohm@0
    48
clasohm@0
    49
val prems = 
clasohm@0
    50
goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
clasohm@0
    51
by (resolve_tac prems 1);
clasohm@0
    52
by (resolve_tac [notI] 1);
clasohm@0
    53
by (resolve_tac [notE] 1);
clasohm@0
    54
by (resolve_tac [notI] 2);
clasohm@0
    55
by (eresolve_tac [notE] 2);
clasohm@0
    56
by (eresolve_tac [disjI1] 2);
clasohm@0
    57
by (resolve_tac [notI] 1);
clasohm@0
    58
by (eresolve_tac [notE] 1);
clasohm@0
    59
by (eresolve_tac [disjI2] 1);
clasohm@0
    60
result();
clasohm@0
    61
clasohm@0
    62
clasohm@0
    63
val prems = 
clasohm@0
    64
goal IFOLP.thy "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
clasohm@0
    65
by (resolve_tac [disjE] 1);
clasohm@0
    66
by (resolve_tac prems 1);
clasohm@0
    67
by (assume_tac 1);
clasohm@0
    68
by (resolve_tac [FalseE] 1);
clasohm@0
    69
by (res_inst_tac [ ("P", "~A") ]  notE  1);
clasohm@0
    70
by (resolve_tac prems 1);
clasohm@0
    71
by (assume_tac 1);
clasohm@0
    72
result();
clasohm@0
    73
clasohm@0
    74
clasohm@0
    75
writeln"Examples with quantifiers";
clasohm@0
    76
clasohm@0
    77
val prems =
clasohm@0
    78
goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
clasohm@0
    79
by (resolve_tac [allI] 1);
clasohm@0
    80
by (resolve_tac [disjI1] 1);
clasohm@0
    81
by (resolve_tac (prems RL [spec]) 1); 
clasohm@0
    82
  (*can use instead
clasohm@0
    83
    by (resolve_tac [spec] 1);  by (resolve_tac prems 1); *)
clasohm@0
    84
result();
clasohm@0
    85
clasohm@0
    86
clasohm@0
    87
goal IFOLP.thy "?p : ALL x. EX y. x=y";
clasohm@0
    88
by (resolve_tac [allI] 1);
clasohm@0
    89
by (resolve_tac [exI] 1);
clasohm@0
    90
by (resolve_tac [refl] 1);
clasohm@0
    91
result();
clasohm@0
    92
clasohm@0
    93
clasohm@0
    94
goal IFOLP.thy "?p : EX y. ALL x. x=y";
clasohm@0
    95
by (resolve_tac [exI] 1);
clasohm@0
    96
by (resolve_tac [allI] 1);
clasohm@0
    97
by (resolve_tac [refl] 1) handle ERROR => writeln"Failed, as expected";  
clasohm@0
    98
getgoal 1; 
clasohm@0
    99
clasohm@0
   100
clasohm@0
   101
(*Parallel lifting example. *)
clasohm@0
   102
goal IFOLP.thy "?p : EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
clasohm@0
   103
by (resolve_tac [exI, allI] 1);
clasohm@0
   104
by (resolve_tac [exI, allI] 1);
clasohm@0
   105
by (resolve_tac [exI, allI] 1);
clasohm@0
   106
by (resolve_tac [exI, allI] 1);
clasohm@0
   107
by (resolve_tac [exI, allI] 1);
clasohm@0
   108
clasohm@0
   109
clasohm@0
   110
val prems =
clasohm@0
   111
goal IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";
clasohm@0
   112
by (resolve_tac [conjE] 1);
clasohm@0
   113
by (resolve_tac prems 1);
clasohm@0
   114
by (resolve_tac [exE] 1);
clasohm@0
   115
by (assume_tac 1);
clasohm@0
   116
by (resolve_tac [exI] 1);
clasohm@0
   117
by (resolve_tac [conjI] 1);
clasohm@0
   118
by (assume_tac 1);
clasohm@0
   119
by (assume_tac 1);
clasohm@0
   120
result();
clasohm@0
   121
clasohm@0
   122
clasohm@0
   123
(*A bigger demonstration of quantifiers -- not in the paper*)
clasohm@0
   124
goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
clasohm@0
   125
by (resolve_tac [impI] 1);
clasohm@0
   126
by (resolve_tac [allI] 1);
clasohm@0
   127
by (resolve_tac [exE] 1 THEN assume_tac 1);
clasohm@0
   128
by (resolve_tac [exI] 1);
clasohm@0
   129
by (resolve_tac [allE] 1 THEN assume_tac 1);
clasohm@0
   130
by (assume_tac 1);
clasohm@0
   131
result();  
clasohm@0
   132
clasohm@0
   133
clasohm@0
   134
writeln"Reached end of file.";