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