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/theorems.txt
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 12 Aug 2010 15:03:34 +0200
branchisac-from-Isabelle2009-2
changeset 37913 20e3616b2d9c
parent 459 03b445551763
permissions -rw-r--r--
prepare reactivation of isac-update-Isa09-2 
     1 Pretty.setmargin 72;  (*existing macros just allow this margin*)

     2 print_depth 0;

     3 

     4 (*operations for "thm"*)

     5 

     6 prth mp; 

     7 

     8 prth (mp RS mp);

     9 

    10 prth (conjunct1 RS mp);

    11 prth (conjunct1 RSN (2,mp));

    12 

    13 prth (mp RS conjunct1);

    14 prth (spec RS it);

    15 prth (standard it);

    16 

    17 prth spec;

    18 prth (it RS mp);

    19 prth (it RS conjunct1);

    20 prth (standard it);

    21 

    22 - prth spec;

    23 ALL x. ?P(x) ==> ?P(?x)

    24 - prth (it RS mp);

    25 [| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1)

    26 - prth (it RS conjunct1);

    27 [| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2)

    28 - prth (standard it);

    29 [| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x)

    30 

    31 (*flexflex pairs*)

    32 - prth refl;

    33 ?a = ?a

    34 - prth exI;

    35 ?P(?x) ==> EX x. ?P(x)

    36 - prth (refl RS exI);

    37 ?a3(?x) == ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)

    38 - prthq (flexflex_rule it);

    39 EX x. ?a4 = ?a4

    40 

    41 (*Usage of RL*)

    42 - val reflk = prth (read_instantiate [("a","k")] refl);

    43 k = k

    44 val reflk = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm

    45 - prth (reflk RS exI);

    46 

    47 uncaught exception THM

    48 - prths ([reflk] RL [exI]);

    49 EX x. x = x

    50 

    51 EX x. k = x

    52 

    53 EX x. x = k

    54 

    55 EX x. k = k

    56 

    57 

    58 

    59 (*tactics *)

    60 

    61 goal FOL.thy "P|P --> P";

    62 by (resolve_tac [impI] 1);

    63 by (resolve_tac [disjE] 1);

    64 by (assume_tac 3);

    65 by (assume_tac 2);

    66 by (assume_tac 1);

    67 val mythm = prth(result());

    68 

    69 

    70 goal FOL.thy "(P & Q) | R  --> (P | R)";

    71 by (resolve_tac [impI] 1);

    72 by (eresolve_tac [disjE] 1);

    73 by (dresolve_tac [conjunct1] 1);

    74 by (resolve_tac [disjI1] 1);

    75 by (resolve_tac [disjI2] 2);

    76 by (REPEAT (assume_tac 1));

    77 

    78 

    79 - goal FOL.thy "(P & Q) | R  --> (P | R)";

    80 Level 0

    81 P & Q | R --> P | R

    82  1. P & Q | R --> P | R

    83 - by (resolve_tac [impI] 1);

    84 Level 1

    85 P & Q | R --> P | R

    86  1. P & Q | R ==> P | R

    87 - by (eresolve_tac [disjE] 1);

    88 Level 2

    89 P & Q | R --> P | R

    90  1. P & Q ==> P | R

    91  2. R ==> P | R

    92 - by (dresolve_tac [conjunct1] 1);

    93 Level 3

    94 P & Q | R --> P | R

    95  1. P ==> P | R

    96  2. R ==> P | R

    97 - by (resolve_tac [disjI1] 1);

    98 Level 4

    99 P & Q | R --> P | R

   100  1. P ==> P

   101  2. R ==> P | R

   102 - by (resolve_tac [disjI2] 2);

   103 Level 5

   104 P & Q | R --> P | R

   105  1. P ==> P

   106  2. R ==> R

   107 - by (REPEAT (assume_tac 1));

   108 Level 6

   109 P & Q | R --> P | R

   110 No subgoals!

   111 

   112 

   113 goal FOL.thy "(P | Q) | R  -->  P | (Q | R)";

   114 by (resolve_tac [impI] 1);

   115 by (eresolve_tac [disjE] 1);

   116 by (eresolve_tac [disjE] 1);

   117 by (resolve_tac [disjI1] 1);

   118 by (resolve_tac [disjI2] 2);

   119 by (resolve_tac [disjI1] 2);

   120 by (resolve_tac [disjI2] 3);

   121 by (resolve_tac [disjI2] 3);

   122 by (REPEAT (assume_tac 1));
wneuper/isa