Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/Intro/deriv.txt
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 12 Aug 2010 15:03:34 +0200
branchisac-from-Isabelle2009-2
changeset 37913 20e3616b2d9c
parent 14148 6580d374a509
permissions -rw-r--r--
prepare reactivation of isac-update-Isa09-2 
     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
wneuper/isa