doc-src/Logics/LK-eg.txt
author kleing
Mon, 29 Dec 2003 06:49:26 +0100
changeset 14333 14f29eb097a3
parent 5153 51bd3cd9ee85
permissions -rw-r--r--
\<^bsub> .. \<^esub>
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
(**** LK examples -- process using Doc/tout LK-eg.txt ****)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
Pretty.setmargin 72;  (*existing macros just allow this margin*)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
print_depth 0;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
5153
51bd3cd9ee85 now with Goal cmd
paulson
parents: 5151
diff changeset
     6
context LK.thy;
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
     7
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
     8
Goal "|- EX y. ALL x. P(y)-->P(x)";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
by (resolve_tac [exR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
by (resolve_tac [allR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
by (resolve_tac [impR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
(*previous step fails!*)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
by (resolve_tac [exR_thin] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
by (resolve_tac [allR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
by (resolve_tac [impR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
by (resolve_tac [basic] 1);
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
    18
Goal "|- EX y. ALL x. P(y)-->P(x)";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
by (best_tac LK_dup_pack 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
    23
Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
by (resolve_tac [notR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
by (resolve_tac [exL] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
by (resolve_tac [allL_thin] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
by (resolve_tac [iffL] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
by (resolve_tac [notL] 2);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
by (resolve_tac [basic] 2);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
by (resolve_tac [notR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
    34
STOP_HERE;
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
    36
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
    37
> Goal "|- EX y. ALL x. P(y)-->P(x)";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
 1.  |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
> by (resolve_tac [exR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
 1.  |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
> by (resolve_tac [allR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
 1. !!x.  |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
> by (resolve_tac [impR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
 1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
> by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
by: tactic failed
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
> by (resolve_tac [exR_thin] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
Level 4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
 1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
> by (resolve_tac [allR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
Level 5
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
 1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
> by (resolve_tac [impR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
Level 6
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
 1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
> by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
Level 7
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
    72
> Goal "|- EX y. ALL x. P(y)-->P(x)";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
 1.  |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
> by (best_tac LK_dup_pack 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
 |- EX y. ALL x. P(y) --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 104
diff changeset
    84
> Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
 1.  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
> by (resolve_tac [notR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
 1. EX x. ALL y. F(y,x) <-> ~F(y,y) |-
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
> by (resolve_tac [exL] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
 1. !!x. ALL y. F(y,x) <-> ~F(y,y) |-
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
> by (resolve_tac [allL_thin] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
 1. !!x. F(?x2(x),x) <-> ~F(?x2(x),?x2(x)) |-
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
> by (resolve_tac [iffL] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
Level 4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
 1. !!x.  |- F(?x2(x),x), ~F(?x2(x),?x2(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
 2. !!x. ~F(?x2(x),?x2(x)), F(?x2(x),x) |-
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
> by (resolve_tac [notL] 2);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
Level 5
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
 1. !!x.  |- F(?x2(x),x), ~F(?x2(x),?x2(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
 2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
> by (resolve_tac [basic] 2);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
Level 6
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
 1. !!x.  |- F(x,x), ~F(x,x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
> by (resolve_tac [notR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
Level 7
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
 1. !!x. F(x,x) |- F(x,x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
> by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
Level 8
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
 |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
No subgoals!