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