src/FOLP/ex/intro.ML
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 17480 fd19f77dcf60
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1464
a608f83e3421 expanded tabs; removed commit() from ROOT.ML
clasohm
parents: 1446
diff changeset
     1
(*  Title:      FOLP/ex/intro.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1446
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Examples for the manual "Introduction to Isabelle"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Derives some inference rules, illustrating the use of definitions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
To generate similar output to manual, execute these commands:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
    Pretty.setmargin 72; print_depth 0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
15661
9ef583b08647 reverted renaming of Some/None in comments and strings;
wenzelm
parents: 15531
diff changeset
    15
(**** Some simple backward proofs ****)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    17
goal (theory "FOLP") "?p:P|P --> P";
1446
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    18
by (rtac impI 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    19
by (rtac disjE 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (assume_tac 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (assume_tac 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
val mythm = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    25
goal (theory "FOLP") "?p:(P & Q) | R  --> (P | R)";
1446
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    26
by (rtac impI 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    27
by (etac disjE 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    28
by (dtac conjunct1 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    29
by (rtac disjI1 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    30
by (rtac disjI2 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
by (REPEAT (assume_tac 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
(*Correct version, delaying use of "spec" until last*)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    35
goal (theory "FOLP") "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
1446
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    36
by (rtac impI 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    37
by (rtac allI 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    38
by (rtac allI 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    39
by (dtac spec 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    40
by (dtac spec 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
(**** Demonstration of fast_tac ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    47
goal (theory "FOLP") "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
\       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
by (fast_tac FOLP_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    52
goal (theory "FOLP") "?p:ALL x. P(x,f(x)) <-> \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
\       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
by (fast_tac FOLP_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
(**** Derivation of conjunction elimination rule ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    60
val [major,minor] = goal (theory "FOLP") "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
1446
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    61
by (rtac minor 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (resolve_tac [major RS conjunct1] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (resolve_tac [major RS conjunct2] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
prth (topthm());
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
(**** Derived rules involving definitions ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
(** Derivation of negation introduction **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    72
val prems = goal (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P";
1446
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    73
by (rewtac not_def);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    74
by (rtac impI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
by (resolve_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    79
val [major,minor] = goal (theory "FOLP") "[| p:~P;  q:P |] ==> ?p:R";
1446
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    80
by (rtac FalseE 1);
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    81
by (rtac mp 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
by (resolve_tac [rewrite_rule [not_def] major] 1);
1446
a8387e934fa7 Ran expandshort
paulson
parents: 0
diff changeset
    83
by (rtac minor 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
(*Alternative proof of above result*)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 15661
diff changeset
    87
val [major,minor] = goalw (theory "FOLP") [not_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
    "[| p:~P;  q:P |] ==> ?p:R";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
result();