17481

1 
(* Title: LK/ex/quant.ML

6252

2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Classical sequent calculus: examples with quantifiers.


7 
*)


8 

17481

9 
goal (theory "LK") " (ALL x. P) <> P";

6252

10 
by (fast_tac LK_pack 1);

17481

11 
result();

6252

12 

17481

13 
goal (theory "LK") " (ALL x y. P(x,y)) <> (ALL y x. P(x,y))";

6252

14 
by (fast_tac LK_pack 1);

17481

15 
result();

6252

16 

17481

17 
goal (theory "LK") "ALL u. P(u), ALL v. Q(v)  ALL u v. P(u) & Q(v)";

6252

18 
by (fast_tac LK_pack 1);

17481

19 
result();

6252

20 


21 
writeln"Permutation of existential quantifier.";

17481

22 
goal (theory "LK") " (EX x y. P(x,y)) <> (EX y x. P(x,y))";

6252

23 
by (fast_tac LK_pack 1);

17481

24 
result();

6252

25 

17481

26 
goal (theory "LK") " (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))";

6252

27 
by (fast_tac LK_pack 1);

17481

28 
result();

6252

29 


30 


31 
(*Converse is invalid*)

17481

32 
goal (theory "LK") " (ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)Q(x))";

6252

33 
by (fast_tac LK_pack 1);

17481

34 
result();

6252

35 


36 


37 
writeln"Pushing ALL into an implication.";

17481

38 
goal (theory "LK") " (ALL x. P > Q(x)) <> (P > (ALL x. Q(x)))";

6252

39 
by (fast_tac LK_pack 1);

17481

40 
result();

6252

41 


42 

17481

43 
goal (theory "LK") " (ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)";

6252

44 
by (fast_tac LK_pack 1);

17481

45 
result();

6252

46 


47 

17481

48 
goal (theory "LK") " (EX x. P) <> P";

6252

49 
by (fast_tac LK_pack 1);

17481

50 
result();

6252

51 


52 


53 
writeln"Distribution of EX over disjunction.";

17481

54 
goal (theory "LK") " (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))";

6252

55 
by (fast_tac LK_pack 1);

17481

56 
result();

6252

57 
(*5 secs*)


58 


59 
(*Converse is invalid*)

17481

60 
goal (theory "LK") " (EX x. P(x) & Q(x)) > (EX x. P(x)) & (EX x. Q(x))";

6252

61 
by (fast_tac LK_pack 1);

17481

62 
result();

6252

63 


64 


65 
writeln"Harder examples: classical theorems.";


66 

17481

67 
goal (theory "LK") " (EX x. P>Q(x)) <> (P > (EX x. Q(x)))";

6252

68 
by (fast_tac LK_pack 1);

17481

69 
result();

6252

70 
(*3 secs*)


71 


72 

17481

73 
goal (theory "LK") " (EX x. P(x)>Q) <> (ALL x. P(x)) > Q";

6252

74 
by (fast_tac LK_pack 1);

17481

75 
result();

6252

76 
(*5 secs*)


77 


78 

17481

79 
goal (theory "LK") " (ALL x. P(x))  Q <> (ALL x. P(x)  Q)";

6252

80 
by (fast_tac LK_pack 1);

17481

81 
result();

6252

82 


83 


84 
writeln"Basic test of quantifier reasoning";

17481

85 
goal (theory "LK")

6252

86 
" (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


87 
by (fast_tac LK_pack 1);

17481

88 
result();

6252

89 


90 

17481

91 
goal (theory "LK") " (ALL x. Q(x)) > (EX x. Q(x))";

6252

92 
by (fast_tac LK_pack 1);

17481

93 
result();

6252

94 


95 


96 
writeln"The following are invalid!";


97 


98 
(*INVALID*)

17481

99 
goal (theory "LK") " (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))";


100 
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";

6252

101 
(*Check that subgoals remain: proof failed.*)

17481

102 
getgoal 1;

6252

103 


104 
(*INVALID*)

17481

105 
goal (theory "LK") " (EX x. Q(x)) > (ALL x. Q(x))";

6252

106 
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";

17481

107 
getgoal 1;

6252

108 

17481

109 
goal (theory "LK") " P(?a) > (ALL x. P(x))";

6252

110 
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";


111 
(*Check that subgoals remain: proof failed.*)

17481

112 
getgoal 1;

6252

113 

17481

114 
goal (theory "LK") " (P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))";

6252

115 
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";

17481

116 
getgoal 1;

6252

117 


118 


119 
writeln"Back to things that are provable...";


120 

17481

121 
goal (theory "LK") " (ALL x. P(x)>Q(x)) & (EX x. P(x)) > (EX x. Q(x))";


122 
by (fast_tac LK_pack 1);


123 
result();

6252

124 


125 
(*An example of why exR should be delayed as long as possible*)

17481

126 
goal (theory "LK") " (P> (EX x. Q(x))) & P> (EX x. Q(x))";

6252

127 
by (fast_tac LK_pack 1);

17481

128 
result();

6252

129 


130 
writeln"Solving for a Var";

17481

131 
goal (theory "LK")

6252

132 
" (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)";


133 
by (fast_tac LK_pack 1);


134 
result();


135 


136 


137 
writeln"Principia Mathematica *11.53";

17481

138 
goal (theory "LK")

6252

139 
" (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))";


140 
by (fast_tac LK_pack 1);


141 
result();


142 


143 


144 
writeln"Principia Mathematica *11.55";

17481

145 
goal (theory "LK") " (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))";

6252

146 
by (fast_tac LK_pack 1);


147 
result();


148 


149 
writeln"Principia Mathematica *11.61";

17481

150 
goal (theory "LK")

6252

151 
" (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))";


152 
by (fast_tac LK_pack 1);


153 
result();


154 


155 
(*21 August 88: loaded in 45.7 secs*)

17481

156 
(*18 September 2005: loaded in 0.114 secs*)
