doc-src/Logics/LK-eg.txt
changeset 5151 1e944fe5ce96
parent 104 d8205bb279a7
child 5153 51bd3cd9ee85
equal deleted inserted replaced
5150:6e2e9b92c301 5151:1e944fe5ce96
     1 (**** LK examples -- process using Doc/tout LK-eg.txt ****)
     1 (**** LK examples -- process using Doc/tout LK-eg.txt ****)
     2 
     2 
     3 Pretty.setmargin 72;  (*existing macros just allow this margin*)
     3 Pretty.setmargin 72;  (*existing macros just allow this margin*)
     4 print_depth 0;
     4 print_depth 0;
     5 
     5 
     6 goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
     6 Context LK.thy;
       
     7 
       
     8 Goal "|- EX y. ALL x. P(y)-->P(x)";
     7 by (resolve_tac [exR] 1);
     9 by (resolve_tac [exR] 1);
     8 by (resolve_tac [allR] 1);
    10 by (resolve_tac [allR] 1);
     9 by (resolve_tac [impR] 1);
    11 by (resolve_tac [impR] 1);
    10 by (resolve_tac [basic] 1);
    12 by (resolve_tac [basic] 1);
    11 (*previous step fails!*)
    13 (*previous step fails!*)
    12 by (resolve_tac [exR_thin] 1);
    14 by (resolve_tac [exR_thin] 1);
    13 by (resolve_tac [allR] 1);
    15 by (resolve_tac [allR] 1);
    14 by (resolve_tac [impR] 1);
    16 by (resolve_tac [impR] 1);
    15 by (resolve_tac [basic] 1);
    17 by (resolve_tac [basic] 1);
    16 goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
    18 Goal "|- EX y. ALL x. P(y)-->P(x)";
    17 by (best_tac LK_dup_pack 1);
    19 by (best_tac LK_dup_pack 1);
    18 
    20 
    19 
    21 
    20 
    22 
    21 goal LK_Rule.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
    23 Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
    22 by (resolve_tac [notR] 1);
    24 by (resolve_tac [notR] 1);
    23 by (resolve_tac [exL] 1);
    25 by (resolve_tac [exL] 1);
    24 by (resolve_tac [allL_thin] 1);
    26 by (resolve_tac [allL_thin] 1);
    25 by (resolve_tac [iffL] 1);
    27 by (resolve_tac [iffL] 1);
    26 by (resolve_tac [notL] 2);
    28 by (resolve_tac [notL] 2);
    27 by (resolve_tac [basic] 2);
    29 by (resolve_tac [basic] 2);
    28 by (resolve_tac [notR] 1);
    30 by (resolve_tac [notR] 1);
    29 by (resolve_tac [basic] 1);
    31 by (resolve_tac [basic] 1);
    30 
    32 
    31 
    33 
       
    34 STOP_HERE;
    32 
    35 
    33 > goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
    36 
       
    37 > Goal "|- EX y. ALL x. P(y)-->P(x)";
    34 Level 0
    38 Level 0
    35  |- EX y. ALL x. P(y) --> P(x)
    39  |- EX y. ALL x. P(y) --> P(x)
    36  1.  |- EX y. ALL x. P(y) --> P(x)
    40  1.  |- EX y. ALL x. P(y) --> P(x)
    37 > by (resolve_tac [exR] 1);
    41 > by (resolve_tac [exR] 1);
    38 Level 1
    42 Level 1
    63 > by (resolve_tac [basic] 1);
    67 > by (resolve_tac [basic] 1);
    64 Level 7
    68 Level 7
    65  |- EX y. ALL x. P(y) --> P(x)
    69  |- EX y. ALL x. P(y) --> P(x)
    66 No subgoals!
    70 No subgoals!
    67 
    71 
    68 > goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
    72 > Goal "|- EX y. ALL x. P(y)-->P(x)";
    69 Level 0
    73 Level 0
    70  |- EX y. ALL x. P(y) --> P(x)
    74  |- EX y. ALL x. P(y) --> P(x)
    71  1.  |- EX y. ALL x. P(y) --> P(x)
    75  1.  |- EX y. ALL x. P(y) --> P(x)
    72 > by (best_tac LK_dup_pack 1);
    76 > by (best_tac LK_dup_pack 1);
    73 Level 1
    77 Level 1
    75 No subgoals!
    79 No subgoals!
    76 
    80 
    77 
    81 
    78 
    82 
    79 
    83 
    80 > goal LK_Rule.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
    84 > Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
    81 Level 0
    85 Level 0
    82  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    86  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    83  1.  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    87  1.  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
    84 > by (resolve_tac [notR] 1);
    88 > by (resolve_tac [notR] 1);
    85 Level 1
    89 Level 1