doc-src/Logics/LK-eg.txt
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 5153 51bd3cd9ee85
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     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!