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 

5153

6 
context LK.thy;

5151

7 


8 
Goal " EX y. ALL x. P(y)>P(x)";

104

9 
by (resolve_tac [exR] 1);


10 
by (resolve_tac [allR] 1);


11 
by (resolve_tac [impR] 1);


12 
by (resolve_tac [basic] 1);


13 
(*previous step fails!*)


14 
by (resolve_tac [exR_thin] 1);


15 
by (resolve_tac [allR] 1);


16 
by (resolve_tac [impR] 1);


17 
by (resolve_tac [basic] 1);

5151

18 
Goal " EX y. ALL x. P(y)>P(x)";

104

19 
by (best_tac LK_dup_pack 1);


20 


21 


22 

5151

23 
Goal " ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";

104

24 
by (resolve_tac [notR] 1);


25 
by (resolve_tac [exL] 1);


26 
by (resolve_tac [allL_thin] 1);


27 
by (resolve_tac [iffL] 1);


28 
by (resolve_tac [notL] 2);


29 
by (resolve_tac [basic] 2);


30 
by (resolve_tac [notR] 1);


31 
by (resolve_tac [basic] 1);


32 


33 

5151

34 
STOP_HERE;

104

35 

5151

36 


37 
> Goal " EX y. ALL x. P(y)>P(x)";

104

38 
Level 0


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


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


41 
> by (resolve_tac [exR] 1);


42 
Level 1


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


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


45 
> by (resolve_tac [allR] 1);


46 
Level 2


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 [impR] 1);


50 
Level 3


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


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


53 
> by (resolve_tac [basic] 1);


54 
by: tactic failed


55 
> by (resolve_tac [exR_thin] 1);


56 
Level 4


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


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


59 
> by (resolve_tac [allR] 1);


60 
Level 5


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


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


63 
> by (resolve_tac [impR] 1);


64 
Level 6


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


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


67 
> by (resolve_tac [basic] 1);


68 
Level 7


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


70 
No subgoals!


71 

5151

72 
> Goal " EX y. ALL x. P(y)>P(x)";

104

73 
Level 0


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


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


76 
> by (best_tac LK_dup_pack 1);


77 
Level 1


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


79 
No subgoals!


80 


81 


82 


83 

5151

84 
> Goal " ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";

104

85 
Level 0


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 [notR] 1);


89 
Level 1


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


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


92 
> by (resolve_tac [exL] 1);


93 
Level 2


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


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


96 
> by (resolve_tac [allL_thin] 1);


97 
Level 3


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


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


100 
> by (resolve_tac [iffL] 1);


101 
Level 4


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


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


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


105 
> by (resolve_tac [notL] 2);


106 
Level 5


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


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


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


110 
> by (resolve_tac [basic] 2);


111 
Level 6


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


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


114 
> by (resolve_tac [notR] 1);


115 
Level 7


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


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


118 
> by (resolve_tac [basic] 1);


119 
Level 8


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


121 
No subgoals!
