(**** LK examples -- process using Doc/tout LK-eg.txt ****)
Pretty.setmargin 72; (*existing macros just allow this margin*)
print_depth 0;
context LK.thy;
Goal "|- EX y. ALL x. P(y)-->P(x)";
by (resolve_tac [exR] 1);
by (resolve_tac [allR] 1);
by (resolve_tac [impR] 1);
by (resolve_tac [basic] 1);
(*previous step fails!*)
by (resolve_tac [exR_thin] 1);
by (resolve_tac [allR] 1);
by (resolve_tac [impR] 1);
by (resolve_tac [basic] 1);
Goal "|- EX y. ALL x. P(y)-->P(x)";
by (best_tac LK_dup_pack 1);
Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
by (resolve_tac [notR] 1);
by (resolve_tac [exL] 1);
by (resolve_tac [allL_thin] 1);
by (resolve_tac [iffL] 1);
by (resolve_tac [notL] 2);
by (resolve_tac [basic] 2);
by (resolve_tac [notR] 1);
by (resolve_tac [basic] 1);
STOP_HERE;
> Goal "|- EX y. ALL x. P(y)-->P(x)";
Level 0
|- EX y. ALL x. P(y) --> P(x)
1. |- EX y. ALL x. P(y) --> P(x)
> by (resolve_tac [exR] 1);
Level 1
|- EX y. ALL x. P(y) --> P(x)
1. |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)
> by (resolve_tac [allR] 1);
Level 2
|- EX y. ALL x. P(y) --> P(x)
1. !!x. |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)
> by (resolve_tac [impR] 1);
Level 3
|- EX y. ALL x. P(y) --> P(x)
1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)
> by (resolve_tac [basic] 1);
by: tactic failed
> by (resolve_tac [exR_thin] 1);
Level 4
|- EX y. ALL x. P(y) --> P(x)
1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)
> by (resolve_tac [allR] 1);
Level 5
|- EX y. ALL x. P(y) --> P(x)
1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)
> by (resolve_tac [impR] 1);
Level 6
|- EX y. ALL x. P(y) --> P(x)
1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)
> by (resolve_tac [basic] 1);
Level 7
|- EX y. ALL x. P(y) --> P(x)
No subgoals!
> Goal "|- EX y. ALL x. P(y)-->P(x)";
Level 0
|- EX y. ALL x. P(y) --> P(x)
1. |- EX y. ALL x. P(y) --> P(x)
> by (best_tac LK_dup_pack 1);
Level 1
|- EX y. ALL x. P(y) --> P(x)
No subgoals!
> Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
Level 0
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
1. |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
> by (resolve_tac [notR] 1);
Level 1
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
1. EX x. ALL y. F(y,x) <-> ~F(y,y) |-
> by (resolve_tac [exL] 1);
Level 2
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
1. !!x. ALL y. F(y,x) <-> ~F(y,y) |-
> by (resolve_tac [allL_thin] 1);
Level 3
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
1. !!x. F(?x2(x),x) <-> ~F(?x2(x),?x2(x)) |-
> by (resolve_tac [iffL] 1);
Level 4
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
1. !!x. |- F(?x2(x),x), ~F(?x2(x),?x2(x))
2. !!x. ~F(?x2(x),?x2(x)), F(?x2(x),x) |-
> by (resolve_tac [notL] 2);
Level 5
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
1. !!x. |- F(?x2(x),x), ~F(?x2(x),?x2(x))
2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))
> by (resolve_tac [basic] 2);
Level 6
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
1. !!x. |- F(x,x), ~F(x,x)
> by (resolve_tac [notR] 1);
Level 7
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
1. !!x. F(x,x) |- F(x,x)
> by (resolve_tac [basic] 1);
Level 8
|- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
No subgoals!