(**** LK examples -- process using Doc/tout LK-eg.txt ****) Pretty.setmargin 72; (*existing macros just allow this margin*) print_depth 0; goal LK_Rule.thy "|- 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 LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)"; by (best_tac LK_dup_pack 1); goal LK_Rule.thy "|- ~ (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); > goal LK_Rule.thy "|- 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 LK_Rule.thy "|- 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 LK_Rule.thy "|- ~ (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!