doc-src/Logics/LK-eg.txt
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 104 d8205bb279a7
child 5151 1e944fe5ce96
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     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 goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
     7 by (resolve_tac [exR] 1);
     8 by (resolve_tac [allR] 1);
     9 by (resolve_tac [impR] 1);
    10 by (resolve_tac [basic] 1);
    11 (*previous step fails!*)
    12 by (resolve_tac [exR_thin] 1);
    13 by (resolve_tac [allR] 1);
    14 by (resolve_tac [impR] 1);
    15 by (resolve_tac [basic] 1);
    16 goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
    17 by (best_tac LK_dup_pack 1);
    18 
    19 
    20 
    21 goal LK_Rule.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
    22 by (resolve_tac [notR] 1);
    23 by (resolve_tac [exL] 1);
    24 by (resolve_tac [allL_thin] 1);
    25 by (resolve_tac [iffL] 1);
    26 by (resolve_tac [notL] 2);
    27 by (resolve_tac [basic] 2);
    28 by (resolve_tac [notR] 1);
    29 by (resolve_tac [basic] 1);
    30 
    31 
    32 
    33 > goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
    34 Level 0
    35  |- EX y. ALL x. P(y) --> P(x)
    36  1.  |- EX y. ALL x. P(y) --> P(x)
    37 > by (resolve_tac [exR] 1);
    38 Level 1
    39  |- EX y. ALL x. P(y) --> P(x)
    40  1.  |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)
    41 > by (resolve_tac [allR] 1);
    42 Level 2
    43  |- EX y. ALL x. P(y) --> P(x)
    44  1. !!x.  |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)
    45 > by (resolve_tac [impR] 1);
    46 Level 3
    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 [basic] 1);
    50 by: tactic failed
    51 > by (resolve_tac [exR_thin] 1);
    52 Level 4
    53  |- EX y. ALL x. P(y) --> P(x)
    54  1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)
    55 > by (resolve_tac [allR] 1);
    56 Level 5
    57  |- EX y. ALL x. P(y) --> P(x)
    58  1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)
    59 > by (resolve_tac [impR] 1);
    60 Level 6
    61  |- EX y. ALL x. P(y) --> P(x)
    62  1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)
    63 > by (resolve_tac [basic] 1);
    64 Level 7
    65  |- EX y. ALL x. P(y) --> P(x)
    66 No subgoals!
    67 
    68 > goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
    69 Level 0
    70  |- EX y. ALL x. P(y) --> P(x)
    71  1.  |- EX y. ALL x. P(y) --> P(x)
    72 > by (best_tac LK_dup_pack 1);
    73 Level 1
    74  |- EX y. ALL x. P(y) --> P(x)
    75 No subgoals!
    76 
    77 
    78 
    79 
    80 > goal LK_Rule.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
    81 Level 0
    82  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    83  1.  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    84 > by (resolve_tac [notR] 1);
    85 Level 1
    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 [exL] 1);
    89 Level 2
    90  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    91  1. !!x. ALL y. F(y,x) <-> ~F(y,y) |-
    92 > by (resolve_tac [allL_thin] 1);
    93 Level 3
    94  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    95  1. !!x. F(?x2(x),x) <-> ~F(?x2(x),?x2(x)) |-
    96 > by (resolve_tac [iffL] 1);
    97 Level 4
    98  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    99  1. !!x.  |- F(?x2(x),x), ~F(?x2(x),?x2(x))
   100  2. !!x. ~F(?x2(x),?x2(x)), F(?x2(x),x) |-
   101 > by (resolve_tac [notL] 2);
   102 Level 5
   103  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
   104  1. !!x.  |- F(?x2(x),x), ~F(?x2(x),?x2(x))
   105  2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))
   106 > by (resolve_tac [basic] 2);
   107 Level 6
   108  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
   109  1. !!x.  |- F(x,x), ~F(x,x)
   110 > by (resolve_tac [notR] 1);
   111 Level 7
   112  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
   113  1. !!x. F(x,x) |- F(x,x)
   114 > by (resolve_tac [basic] 1);
   115 Level 8
   116  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
   117 No subgoals!