summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/FOLP/ex/foundn.ML

author | clasohm |

Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) | |

changeset 0 | a5a9c433f639 |

child 1459 | d12da312eff4 |

permissions | -rw-r--r-- |

Initial revision

1 (* Title: FOL/ex/foundn

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1991 University of Cambridge

6 Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover

7 *)

9 writeln"File FOL/ex/foundn.";

11 goal IFOLP.thy "?p : A&B --> (C-->A&C)";

12 by (resolve_tac [impI] 1);

13 by (resolve_tac [impI] 1);

14 by (resolve_tac [conjI] 1);

15 by (assume_tac 2);

16 by (resolve_tac [conjunct1] 1);

17 by (assume_tac 1);

18 result();

20 (*A form of conj-elimination*)

21 val prems =

22 goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A; y:B |] ==> f(x,y):C) ==> ?p:C";

23 by (resolve_tac prems 1);

24 by (resolve_tac [conjunct1] 1);

25 by (resolve_tac prems 1);

26 by (resolve_tac [conjunct2] 1);

27 by (resolve_tac prems 1);

28 result();

31 val prems =

32 goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";

33 by (resolve_tac prems 1);

34 by (resolve_tac [notI] 1);

35 by (res_inst_tac [ ("P", "~B") ] notE 1);

36 by (resolve_tac [notI] 2);

37 by (res_inst_tac [ ("P", "B | ~B") ] notE 2);

38 by (assume_tac 2);

39 by (resolve_tac [disjI1] 2);

40 by (assume_tac 2);

41 by (resolve_tac [notI] 1);

42 by (res_inst_tac [ ("P", "B | ~B") ] notE 1);

43 by (assume_tac 1);

44 by (resolve_tac [disjI2] 1);

45 by (assume_tac 1);

46 result();

49 val prems =

50 goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";

51 by (resolve_tac prems 1);

52 by (resolve_tac [notI] 1);

53 by (resolve_tac [notE] 1);

54 by (resolve_tac [notI] 2);

55 by (eresolve_tac [notE] 2);

56 by (eresolve_tac [disjI1] 2);

57 by (resolve_tac [notI] 1);

58 by (eresolve_tac [notE] 1);

59 by (eresolve_tac [disjI2] 1);

60 result();

63 val prems =

64 goal IFOLP.thy "[| p:A | ~A; q:~ ~A |] ==> ?p:A";

65 by (resolve_tac [disjE] 1);

66 by (resolve_tac prems 1);

67 by (assume_tac 1);

68 by (resolve_tac [FalseE] 1);

69 by (res_inst_tac [ ("P", "~A") ] notE 1);

70 by (resolve_tac prems 1);

71 by (assume_tac 1);

72 result();

75 writeln"Examples with quantifiers";

77 val prems =

78 goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";

79 by (resolve_tac [allI] 1);

80 by (resolve_tac [disjI1] 1);

81 by (resolve_tac (prems RL [spec]) 1);

82 (*can use instead

83 by (resolve_tac [spec] 1); by (resolve_tac prems 1); *)

84 result();

87 goal IFOLP.thy "?p : ALL x. EX y. x=y";

88 by (resolve_tac [allI] 1);

89 by (resolve_tac [exI] 1);

90 by (resolve_tac [refl] 1);

91 result();

94 goal IFOLP.thy "?p : EX y. ALL x. x=y";

95 by (resolve_tac [exI] 1);

96 by (resolve_tac [allI] 1);

97 by (resolve_tac [refl] 1) handle ERROR => writeln"Failed, as expected";

98 getgoal 1;

101 (*Parallel lifting example. *)

102 goal IFOLP.thy "?p : EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";

103 by (resolve_tac [exI, allI] 1);

104 by (resolve_tac [exI, allI] 1);

105 by (resolve_tac [exI, allI] 1);

106 by (resolve_tac [exI, allI] 1);

107 by (resolve_tac [exI, allI] 1);

110 val prems =

111 goal IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";

112 by (resolve_tac [conjE] 1);

113 by (resolve_tac prems 1);

114 by (resolve_tac [exE] 1);

115 by (assume_tac 1);

116 by (resolve_tac [exI] 1);

117 by (resolve_tac [conjI] 1);

118 by (assume_tac 1);

119 by (assume_tac 1);

120 result();

123 (*A bigger demonstration of quantifiers -- not in the paper*)

124 goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";

125 by (resolve_tac [impI] 1);

126 by (resolve_tac [allI] 1);

127 by (resolve_tac [exE] 1 THEN assume_tac 1);

128 by (resolve_tac [exI] 1);

129 by (resolve_tac [allE] 1 THEN assume_tac 1);

130 by (assume_tac 1);

131 result();

134 writeln"Reached end of file.";