104

1 
(**** LK examples  process using Doc/tout LKeg.txt ****)


2 


3 
Pretty.setmargin 72; (*existing macros just allow this margin*)


4 
print_depth 0;


5 


6 
goal LK_Rule.thy " EX y. ALL x. P(y)>P(x)";


7 
by (resolve_tac [exR] 1);


8 
by (resolve_tac [allR] 1);


9 
by (resolve_tac [impR] 1);


10 
by (resolve_tac [basic] 1);


11 
(*previous step fails!*)


12 
by (resolve_tac [exR_thin] 1);


13 
by (resolve_tac [allR] 1);


14 
by (resolve_tac [impR] 1);


15 
by (resolve_tac [basic] 1);


16 
goal LK_Rule.thy " EX y. ALL x. P(y)>P(x)";


17 
by (best_tac LK_dup_pack 1);


18 


19 


20 


21 
goal LK_Rule.thy " ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";


22 
by (resolve_tac [notR] 1);


23 
by (resolve_tac [exL] 1);


24 
by (resolve_tac [allL_thin] 1);


25 
by (resolve_tac [iffL] 1);


26 
by (resolve_tac [notL] 2);


27 
by (resolve_tac [basic] 2);


28 
by (resolve_tac [notR] 1);


29 
by (resolve_tac [basic] 1);


30 


31 


32 


33 
> goal LK_Rule.thy " EX y. ALL x. P(y)>P(x)";


34 
Level 0


35 
 EX y. ALL x. P(y) > P(x)


36 
1.  EX y. ALL x. P(y) > P(x)


37 
> by (resolve_tac [exR] 1);


38 
Level 1


39 
 EX y. ALL x. P(y) > P(x)


40 
1.  ALL x. P(?x) > P(x), EX x. ALL xa. P(x) > P(xa)


41 
> by (resolve_tac [allR] 1);


42 
Level 2


43 
 EX y. ALL x. P(y) > P(x)


44 
1. !!x.  P(?x) > P(x), EX x. ALL xa. P(x) > P(xa)


45 
> by (resolve_tac [impR] 1);


46 
Level 3


47 
 EX y. ALL x. P(y) > P(x)


48 
1. !!x. P(?x)  P(x), EX x. ALL xa. P(x) > P(xa)


49 
> by (resolve_tac [basic] 1);


50 
by: tactic failed


51 
> by (resolve_tac [exR_thin] 1);


52 
Level 4


53 
 EX y. ALL x. P(y) > P(x)


54 
1. !!x. P(?x)  P(x), ALL xa. P(?x7(x)) > P(xa)


55 
> by (resolve_tac [allR] 1);


56 
Level 5


57 
 EX y. ALL x. P(y) > P(x)


58 
1. !!x xa. P(?x)  P(x), P(?x7(x)) > P(xa)


59 
> by (resolve_tac [impR] 1);


60 
Level 6


61 
 EX y. ALL x. P(y) > P(x)


62 
1. !!x xa. P(?x), P(?x7(x))  P(x), P(xa)


63 
> by (resolve_tac [basic] 1);


64 
Level 7


65 
 EX y. ALL x. P(y) > P(x)


66 
No subgoals!


67 


68 
> goal LK_Rule.thy " EX y. ALL x. P(y)>P(x)";


69 
Level 0


70 
 EX y. ALL x. P(y) > P(x)


71 
1.  EX y. ALL x. P(y) > P(x)


72 
> by (best_tac LK_dup_pack 1);


73 
Level 1


74 
 EX y. ALL x. P(y) > P(x)


75 
No subgoals!


76 


77 


78 


79 


80 
> goal LK_Rule.thy " ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";


81 
Level 0


82 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


83 
1.  ~(EX x. ALL y. F(y,x) <> ~F(y,y))


84 
> by (resolve_tac [notR] 1);


85 
Level 1


86 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


87 
1. EX x. ALL y. F(y,x) <> ~F(y,y) 


88 
> by (resolve_tac [exL] 1);


89 
Level 2


90 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


91 
1. !!x. ALL y. F(y,x) <> ~F(y,y) 


92 
> by (resolve_tac [allL_thin] 1);


93 
Level 3


94 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


95 
1. !!x. F(?x2(x),x) <> ~F(?x2(x),?x2(x)) 


96 
> by (resolve_tac [iffL] 1);


97 
Level 4


98 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


99 
1. !!x.  F(?x2(x),x), ~F(?x2(x),?x2(x))


100 
2. !!x. ~F(?x2(x),?x2(x)), F(?x2(x),x) 


101 
> by (resolve_tac [notL] 2);


102 
Level 5


103 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


104 
1. !!x.  F(?x2(x),x), ~F(?x2(x),?x2(x))


105 
2. !!x. F(?x2(x),x)  F(?x2(x),?x2(x))


106 
> by (resolve_tac [basic] 2);


107 
Level 6


108 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


109 
1. !!x.  F(x,x), ~F(x,x)


110 
> by (resolve_tac [notR] 1);


111 
Level 7


112 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


113 
1. !!x. F(x,x)  F(x,x)


114 
> by (resolve_tac [basic] 1);


115 
Level 8


116 
 ~(EX x. ALL y. F(y,x) <> ~F(y,y))


117 
No subgoals!
