doc-src/Intro/deriv.txt
author wenzelm
Mon Oct 01 21:19:50 2007 +0200 (2007-10-01)
changeset 24803 38577b4b1fde
parent 14148 6580d374a509
permissions -rw-r--r--
Norbert Schirmer: record improvements;
lcp@105
     1
(* Deriving an inference rule *)
lcp@105
     2
lcp@105
     3
Pretty.setmargin 72;  (*existing macros just allow this margin*)
lcp@105
     4
print_depth 0;
lcp@105
     5
lcp@105
     6
paulson@14148
     7
val [major,minor] = goal IFOL.thy
lcp@105
     8
    "[| P&Q;  [| P; Q |] ==> R |] ==> R";
lcp@105
     9
prth minor;
lcp@105
    10
by (resolve_tac [minor] 1);
lcp@105
    11
prth major;
lcp@105
    12
prth (major RS conjunct1);
lcp@105
    13
by (resolve_tac [major RS conjunct1] 1);
lcp@105
    14
prth (major RS conjunct2);
lcp@105
    15
by (resolve_tac [major RS conjunct2] 1);
lcp@105
    16
prth (topthm());
lcp@105
    17
val conjE = prth(result());
lcp@105
    18
lcp@105
    19
lcp@105
    20
- val [major,minor] = goal Int_Rule.thy
lcp@105
    21
=     "[| P&Q;  [| P; Q |] ==> R |] ==> R";
lcp@105
    22
Level 0
lcp@105
    23
R
lcp@105
    24
 1. R
lcp@105
    25
val major = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
lcp@105
    26
val minor = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
lcp@105
    27
- prth minor;
lcp@105
    28
[| P; Q |] ==> R  [[| P; Q |] ==> R]
lcp@105
    29
- by (resolve_tac [minor] 1);
lcp@105
    30
Level 1
lcp@105
    31
R
lcp@105
    32
 1. P
lcp@105
    33
 2. Q
lcp@105
    34
- prth major;
lcp@105
    35
P & Q  [P & Q]
lcp@105
    36
- prth (major RS conjunct1);
lcp@105
    37
P  [P & Q]
lcp@105
    38
- by (resolve_tac [major RS conjunct1] 1);
lcp@105
    39
Level 2
lcp@105
    40
R
lcp@105
    41
 1. Q
lcp@105
    42
- prth (major RS conjunct2);
lcp@105
    43
Q  [P & Q]
lcp@105
    44
- by (resolve_tac [major RS conjunct2] 1);
lcp@105
    45
Level 3
lcp@105
    46
R
lcp@105
    47
No subgoals!
lcp@105
    48
- prth (topthm());
lcp@105
    49
R  [P & Q, P & Q, [| P; Q |] ==> R]
lcp@105
    50
- val conjE = prth(result());
lcp@105
    51
[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R
lcp@105
    52
val conjE = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm
lcp@105
    53
lcp@105
    54
lcp@105
    55
(*** Derived rules involving definitions ***)
lcp@105
    56
lcp@105
    57
(** notI **)
lcp@105
    58
lcp@105
    59
val prems = goal Int_Rule.thy "(P ==> False) ==> ~P";
lcp@105
    60
prth not_def;
lcp@105
    61
by (rewrite_goals_tac [not_def]);
lcp@105
    62
by (resolve_tac [impI] 1);
lcp@105
    63
by (resolve_tac prems 1);
lcp@105
    64
by (assume_tac 1);
lcp@105
    65
val notI = prth(result());
lcp@105
    66
lcp@105
    67
val prems = goalw Int_Rule.thy [not_def]
lcp@105
    68
    "(P ==> False) ==> ~P";
lcp@105
    69
lcp@105
    70
lcp@105
    71
- prth not_def;
lcp@105
    72
~?P == ?P --> False
lcp@105
    73
- val prems = goal Int_Rule.thy "(P ==> False) ==> ~P";
lcp@105
    74
Level 0
lcp@105
    75
~P
lcp@105
    76
 1. ~P
lcp@105
    77
- by (rewrite_goals_tac [not_def]);
lcp@105
    78
Level 1
lcp@105
    79
~P
lcp@105
    80
 1. P --> False
lcp@105
    81
- by (resolve_tac [impI] 1);
lcp@105
    82
Level 2
lcp@105
    83
~P
lcp@105
    84
 1. P ==> False
lcp@105
    85
- by (resolve_tac prems 1);
lcp@105
    86
Level 3
lcp@105
    87
~P
lcp@105
    88
 1. P ==> P
lcp@105
    89
- by (assume_tac 1);
lcp@105
    90
Level 4
lcp@105
    91
~P
lcp@105
    92
No subgoals!
lcp@105
    93
- val notI = prth(result());
lcp@105
    94
(?P ==> False) ==> ~?P
lcp@105
    95
val notI = # : thm
lcp@105
    96
lcp@105
    97
- val prems = goalw Int_Rule.thy [not_def]
lcp@105
    98
=     "(P ==> False) ==> ~P";
lcp@105
    99
Level 0
lcp@105
   100
~P
lcp@105
   101
 1. P --> False
lcp@105
   102
lcp@105
   103
lcp@105
   104
(** notE **)
lcp@105
   105
lcp@105
   106
val [major,minor] = goal Int_Rule.thy "[| ~P;  P |] ==> R";
lcp@105
   107
by (resolve_tac [FalseE] 1);
lcp@105
   108
by (resolve_tac [mp] 1);
lcp@105
   109
prth (rewrite_rule [not_def] major);
lcp@105
   110
by (resolve_tac [it] 1);
lcp@105
   111
by (resolve_tac [minor] 1);
lcp@105
   112
val notE = prth(result());
lcp@105
   113
lcp@105
   114
val [major,minor] = goalw Int_Rule.thy [not_def]
lcp@105
   115
    "[| ~P;  P |] ==> R";
lcp@105
   116
prth (minor RS (major RS mp RS FalseE));
lcp@105
   117
by (resolve_tac [it] 1);
lcp@105
   118
lcp@105
   119
lcp@105
   120
val prems = goalw Int_Rule.thy [not_def]
lcp@105
   121
    "[| ~P;  P |] ==> R";
lcp@105
   122
prths prems;
lcp@105
   123
by (resolve_tac [FalseE] 1);
lcp@105
   124
by (resolve_tac [mp] 1);
lcp@105
   125
by (resolve_tac prems 1);
lcp@105
   126
by (resolve_tac prems 1);
lcp@105
   127
val notE = prth(result());
lcp@105
   128
lcp@105
   129
lcp@105
   130
- val [major,minor] = goal Int_Rule.thy "[| ~P;  P |] ==> R";
lcp@105
   131
Level 0
lcp@105
   132
R
lcp@105
   133
 1. R
lcp@105
   134
val major = # : thm
lcp@105
   135
val minor = # : thm
lcp@105
   136
- by (resolve_tac [FalseE] 1);
lcp@105
   137
Level 1
lcp@105
   138
R
lcp@105
   139
 1. False
lcp@105
   140
- by (resolve_tac [mp] 1);
lcp@105
   141
Level 2
lcp@105
   142
R
lcp@105
   143
 1. ?P1 --> False
lcp@105
   144
 2. ?P1
lcp@105
   145
- prth (rewrite_rule [not_def] major);
lcp@105
   146
P --> False  [~P]
lcp@105
   147
- by (resolve_tac [it] 1);
lcp@105
   148
Level 3
lcp@105
   149
R
lcp@105
   150
 1. P
lcp@105
   151
- by (resolve_tac [minor] 1);
lcp@105
   152
Level 4
lcp@105
   153
R
lcp@105
   154
No subgoals!
lcp@105
   155
- val notE = prth(result());
lcp@105
   156
[| ~?P; ?P |] ==> ?R
lcp@105
   157
val notE = # : thm
lcp@105
   158
- val [major,minor] = goalw Int_Rule.thy [not_def]
lcp@105
   159
=     "[| ~P;  P |] ==> R";
lcp@105
   160
Level 0
lcp@105
   161
R
lcp@105
   162
 1. R
lcp@105
   163
val major = # : thm
lcp@105
   164
val minor = # : thm
lcp@105
   165
- prth (minor RS (major RS mp RS FalseE));
lcp@105
   166
?P  [P, ~P]
lcp@105
   167
- by (resolve_tac [it] 1);
lcp@105
   168
Level 1
lcp@105
   169
R
lcp@105
   170
No subgoals!
lcp@105
   171
lcp@105
   172
lcp@105
   173
lcp@105
   174
lcp@105
   175
- goal Int_Rule.thy "[| ~P;  P |] ==> R";
lcp@105
   176
Level 0
lcp@105
   177
R
lcp@105
   178
 1. R
lcp@105
   179
- prths (map (rewrite_rule [not_def]) it);
lcp@105
   180
P --> False  [~P]
lcp@105
   181
lcp@105
   182
P  [P]
lcp@105
   183
lcp@105
   184
- val prems = goalw Int_Rule.thy [not_def]
lcp@105
   185
=     "[| ~P;  P |] ==> R";
lcp@105
   186
Level 0
lcp@105
   187
R
lcp@105
   188
 1. R
lcp@105
   189
val prems = # : thm list
lcp@105
   190
- prths prems;
lcp@105
   191
P --> False  [~P]
lcp@105
   192
lcp@105
   193
P  [P]
lcp@105
   194
lcp@105
   195
- by (resolve_tac [mp RS FalseE] 1);
lcp@105
   196
Level 1
lcp@105
   197
R
lcp@105
   198
 1. ?P1 --> False
lcp@105
   199
 2. ?P1
lcp@105
   200
- by (resolve_tac prems 1);
lcp@105
   201
Level 2
lcp@105
   202
R
lcp@105
   203
 1. P
lcp@105
   204
- by (resolve_tac prems 1);
lcp@105
   205
Level 3
lcp@105
   206
R
lcp@105
   207
No subgoals!
lcp@105
   208
- val notE = prth(result());
lcp@105
   209
[| ~?P; ?P |] ==> ?R
lcp@105
   210
val notE = # : thm