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