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