src/FOLP/ex/foundn.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 18678 dd0c569fa43d
permissions -rw-r--r--
filtering out some package theorems
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
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
     9
goal (theory "IFOLP") "?p : A&B  --> (C-->A&C)";
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    10
by (rtac impI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    11
by (rtac impI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    12
by (rtac conjI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
by (assume_tac 2);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    14
by (rtac conjunct1 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
(*A form of conj-elimination*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
val prems = 
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
    20
goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (resolve_tac prems 1);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    22
by (rtac conjunct1 1);
0
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 conjunct2 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val prems = 
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
    30
goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
by (resolve_tac prems 1);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    32
by (rtac notI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
by (res_inst_tac [ ("P", "~B") ]  notE  1);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    34
by (rtac notI 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
by (assume_tac 2);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    37
by (rtac disjI1 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (assume_tac 2);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    39
by (rtac notI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
by (res_inst_tac [ ("P", "B | ~B") ]  notE  1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (assume_tac 1);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    42
by (rtac disjI2 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val prems = 
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
    48
goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
by (resolve_tac prems 1);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    50
by (rtac notI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    51
by (rtac notE 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    52
by (rtac notI 2);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    53
by (etac notE 2);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    54
by (etac disjI1 2);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    55
by (rtac notI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    56
by (etac notE 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    57
by (etac disjI2 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val prems = 
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
    62
goal (theory "IFOLP") "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    63
by (rtac disjE 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (assume_tac 1);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    66
by (rtac FalseE 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
by (res_inst_tac [ ("P", "~A") ]  notE  1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
writeln"Examples with quantifiers";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val prems =
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
    76
goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    77
by (rtac allI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    78
by (rtac disjI1 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
by (resolve_tac (prems RL [spec]) 1); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
  (*can use instead
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    81
    by (rtac spec 1);  by (resolve_tac prems 1); *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
    85
goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    86
by (rtac allI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    87
by (rtac exI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    88
by (rtac refl 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
    92
goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    93
by (rtac exI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    94
by (rtac allI 1);
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 17480
diff changeset
    95
by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";  
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
getgoal 1; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
(*Parallel lifting example. *)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
   100
goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
by (resolve_tac [exI, allI] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
by (resolve_tac [exI, allI] 1);
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val prems =
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
   109
goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   110
by (rtac conjE 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
by (resolve_tac prems 1);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   112
by (rtac exE 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
by (assume_tac 1);
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   114
by (rtac exI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   115
by (rtac conjI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
(*A bigger demonstration of quantifiers -- not in the paper*)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 3836
diff changeset
   122
goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   123
by (rtac impI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   124
by (rtac allI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   125
by (rtac exE 1 THEN assume_tac 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   126
by (rtac exI 1);
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
   127
by (rtac allE 1 THEN assume_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
result();