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