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/Logics/LK-eg.txt
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 12 Aug 2010 15:03:34 +0200
branchisac-from-Isabelle2009-2
changeset 37913 20e3616b2d9c
parent 5153 51bd3cd9ee85
permissions -rw-r--r--
prepare reactivation of isac-update-Isa09-2 
     1 (**** LK examples -- process using Doc/tout LK-eg.txt ****)

     2 

     3 Pretty.setmargin 72;  (*existing macros just allow this margin*)

     4 print_depth 0;

     5 

     6 context LK.thy;

     7 

     8 Goal "|- EX y. ALL x. P(y)-->P(x)";

     9 by (resolve_tac [exR] 1);

    10 by (resolve_tac [allR] 1);

    11 by (resolve_tac [impR] 1);

    12 by (resolve_tac [basic] 1);

    13 (*previous step fails!*)

    14 by (resolve_tac [exR_thin] 1);

    15 by (resolve_tac [allR] 1);

    16 by (resolve_tac [impR] 1);

    17 by (resolve_tac [basic] 1);

    18 Goal "|- EX y. ALL x. P(y)-->P(x)";

    19 by (best_tac LK_dup_pack 1);

    20 

    21 

    22 

    23 Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";

    24 by (resolve_tac [notR] 1);

    25 by (resolve_tac [exL] 1);

    26 by (resolve_tac [allL_thin] 1);

    27 by (resolve_tac [iffL] 1);

    28 by (resolve_tac [notL] 2);

    29 by (resolve_tac [basic] 2);

    30 by (resolve_tac [notR] 1);

    31 by (resolve_tac [basic] 1);

    32 

    33 

    34 STOP_HERE;

    35 

    36 

    37 > Goal "|- EX y. ALL x. P(y)-->P(x)";

    38 Level 0

    39  |- EX y. ALL x. P(y) --> P(x)

    40  1.  |- EX y. ALL x. P(y) --> P(x)

    41 > by (resolve_tac [exR] 1);

    42 Level 1

    43  |- EX y. ALL x. P(y) --> P(x)

    44  1.  |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)

    45 > by (resolve_tac [allR] 1);

    46 Level 2

    47  |- EX y. ALL x. P(y) --> P(x)

    48  1. !!x.  |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)

    49 > by (resolve_tac [impR] 1);

    50 Level 3

    51  |- EX y. ALL x. P(y) --> P(x)

    52  1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)

    53 > by (resolve_tac [basic] 1);

    54 by: tactic failed

    55 > by (resolve_tac [exR_thin] 1);

    56 Level 4

    57  |- EX y. ALL x. P(y) --> P(x)

    58  1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)

    59 > by (resolve_tac [allR] 1);

    60 Level 5

    61  |- EX y. ALL x. P(y) --> P(x)

    62  1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)

    63 > by (resolve_tac [impR] 1);

    64 Level 6

    65  |- EX y. ALL x. P(y) --> P(x)

    66  1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)

    67 > by (resolve_tac [basic] 1);

    68 Level 7

    69  |- EX y. ALL x. P(y) --> P(x)

    70 No subgoals!

    71 

    72 > Goal "|- EX y. ALL x. P(y)-->P(x)";

    73 Level 0

    74  |- EX y. ALL x. P(y) --> P(x)

    75  1.  |- EX y. ALL x. P(y) --> P(x)

    76 > by (best_tac LK_dup_pack 1);

    77 Level 1

    78  |- EX y. ALL x. P(y) --> P(x)

    79 No subgoals!

    80 

    81 

    82 

    83 

    84 > Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";

    85 Level 0

    86  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

    87  1.  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

    88 > by (resolve_tac [notR] 1);

    89 Level 1

    90  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

    91  1. EX x. ALL y. F(y,x) <-> ~F(y,y) |-

    92 > by (resolve_tac [exL] 1);

    93 Level 2

    94  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

    95  1. !!x. ALL y. F(y,x) <-> ~F(y,y) |-

    96 > by (resolve_tac [allL_thin] 1);

    97 Level 3

    98  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

    99  1. !!x. F(?x2(x),x) <-> ~F(?x2(x),?x2(x)) |-

   100 > by (resolve_tac [iffL] 1);

   101 Level 4

   102  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

   103  1. !!x.  |- F(?x2(x),x), ~F(?x2(x),?x2(x))

   104  2. !!x. ~F(?x2(x),?x2(x)), F(?x2(x),x) |-

   105 > by (resolve_tac [notL] 2);

   106 Level 5

   107  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

   108  1. !!x.  |- F(?x2(x),x), ~F(?x2(x),?x2(x))

   109  2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))

   110 > by (resolve_tac [basic] 2);

   111 Level 6

   112  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

   113  1. !!x.  |- F(x,x), ~F(x,x)

   114 > by (resolve_tac [notR] 1);

   115 Level 7

   116  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

   117  1. !!x. F(x,x) |- F(x,x)

   118 > by (resolve_tac [basic] 1);

   119 Level 8

   120  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))

   121 No subgoals!
wneuper/isa