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