1459

1 
(* Title: FOL/ex/nat2.ML

0

2 
ID: $Id$

1459

3 
Author: Tobias Nipkow

0

4 
Copyright 1991 University of Cambridge


5 
*)


6 

17245

7 
Addsimps [pred_0, pred_succ, plus_0, plus_succ,


8 
nat_distinct1, nat_distinct2, succ_inject,


9 
leq_0, leq_succ_succ, leq_succ_0,


10 
lt_0_succ, lt_succ_succ, lt_0];

0

11 


12 

17245

13 
val prems = goal (the_context ())

0

14 
"[ P(0); !!x. P(succ(x)) ] ==> All(P)";


15 
by (rtac nat_ind 1);


16 
by (REPEAT (resolve_tac (prems@[allI,impI]) 1));

725

17 
qed "nat_exh";

0

18 

5050

19 
Goal "~ n=succ(n)";

2469

20 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

21 
result();


22 

5050

23 
Goal "~ succ(n)=n";

2469

24 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

25 
result();


26 

5050

27 
Goal "~ succ(succ(n))=n";

2469

28 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

29 
result();


30 

5050

31 
Goal "~ n=succ(succ(n))";

2469

32 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

33 
result();


34 

5050

35 
Goal "m+0 = m";

2469

36 
by (IND_TAC nat_ind Simp_tac "m" 1);

725

37 
qed "plus_0_right";

0

38 

5050

39 
Goal "m+succ(n) = succ(m+n)";

2469

40 
by (IND_TAC nat_ind Simp_tac "m" 1);

725

41 
qed "plus_succ_right";

0

42 

2469

43 
Addsimps [plus_0_right, plus_succ_right];


44 

5050

45 
Goal "~n=0 > m+pred(n) = pred(m+n)";

2469

46 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

47 
result();


48 

5050

49 
Goal "~n=0 > succ(pred(n))=n";

2469

50 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

51 
result();


52 

5050

53 
Goal "m+n=0 <> m=0 & n=0";

2469

54 
by (IND_TAC nat_ind Simp_tac "m" 1);

0

55 
result();


56 

5050

57 
Goal "m <= n > m <= succ(n)";

2469

58 
by (IND_TAC nat_ind Simp_tac "m" 1);

0

59 
by (rtac (impI RS allI) 1);

2469

60 
by (ALL_IND_TAC nat_ind Simp_tac 1);


61 
by (Fast_tac 1);


62 
bind_thm("le_imp_le_succ", result() RS mp);

0

63 

5050

64 
Goal "n<succ(n)";

2469

65 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

66 
result();


67 

5050

68 
Goal "~ n<n";

2469

69 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

70 
result();


71 

5050

72 
Goal "m < n > m < succ(n)";

2469

73 
by (IND_TAC nat_ind Simp_tac "m" 1);

0

74 
by (rtac (impI RS allI) 1);

2469

75 
by (ALL_IND_TAC nat_ind Simp_tac 1);


76 
by (Fast_tac 1);

0

77 
result();


78 

5050

79 
Goal "m <= n > m <= n+k";

4091

80 
by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_imp_le_succ]))

0

81 
"k" 1);

755

82 
qed "le_plus";

0

83 

5050

84 
Goal "succ(m) <= n > m <= n";

0

85 
by (res_inst_tac [("x","n")]spec 1);

4091

86 
by (ALL_IND_TAC nat_exh (simp_tac (simpset() addsimps [le_imp_le_succ])) 1);

755

87 
qed "succ_le";

0

88 

5050

89 
Goal "~m<n <> n<=m";

2469

90 
by (IND_TAC nat_ind Simp_tac "n" 1);

0

91 
by (rtac (impI RS allI) 1);

2469

92 
by (ALL_IND_TAC nat_ind Asm_simp_tac 1);

725

93 
qed "not_less";

0

94 

5050

95 
Goal "n<=m > ~m<n";

4091

96 
by (simp_tac (simpset() addsimps [not_less]) 1);

755

97 
qed "le_imp_not_less";

0

98 

5050

99 
Goal "m<n > ~n<=m";

2469

100 
by (cut_facts_tac [not_less] 1 THEN Fast_tac 1);

755

101 
qed "not_le";

0

102 

5050

103 
Goal "m+k<=n > m<=n";

0

104 
by (IND_TAC nat_ind (K all_tac) "k" 1);

2469

105 
by (Simp_tac 1);

0

106 
by (rtac (impI RS allI) 1);

2469

107 
by (Simp_tac 1);

0

108 
by (REPEAT (resolve_tac [allI,impI] 1));


109 
by (cut_facts_tac [succ_le] 1);

2469

110 
by (Fast_tac 1);

755

111 
qed "plus_le";

0

112 

17245

113 
val prems = goal (the_context ()) "[ ~m=0; m <= n ] ==> ~n=0";

0

114 
by (cut_facts_tac prems 1);


115 
by (REPEAT (etac rev_mp 1));

2469

116 
by (IND_TAC nat_exh Simp_tac "m" 1);


117 
by (ALL_IND_TAC nat_exh Simp_tac 1);

755

118 
qed "not0";

0

119 

5050

120 
Goal "a<=a' & b<=b' > a+b<=a'+b'";

4091

121 
by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_plus])) "b" 1);

0

122 
by (resolve_tac [impI RS allI] 1);


123 
by (resolve_tac [allI RS allI] 1);

2469

124 
by (ALL_IND_TAC nat_exh Asm_simp_tac 1);

755

125 
qed "plus_le_plus";

0

126 

5050

127 
Goal "i<=j > j<=k > i<=k";

0

128 
by (IND_TAC nat_ind (K all_tac) "i" 1);

2469

129 
by (Simp_tac 1);

0

130 
by (resolve_tac [impI RS allI] 1);

2469

131 
by (ALL_IND_TAC nat_exh Simp_tac 1);

4423

132 
by (rtac impI 1);

2469

133 
by (ALL_IND_TAC nat_exh Simp_tac 1);


134 
by (Fast_tac 1);

755

135 
qed "le_trans";

0

136 

5050

137 
Goal "i < j > j <=k > i < k";

0

138 
by (IND_TAC nat_ind (K all_tac) "j" 1);

2469

139 
by (Simp_tac 1);

0

140 
by (resolve_tac [impI RS allI] 1);

2469

141 
by (ALL_IND_TAC nat_exh Simp_tac 1);


142 
by (ALL_IND_TAC nat_exh Simp_tac 1);


143 
by (ALL_IND_TAC nat_exh Simp_tac 1);


144 
by (Fast_tac 1);

755

145 
qed "less_le_trans";

0

146 

5050

147 
Goal "succ(i) <= j <> i < j";

2469

148 
by (IND_TAC nat_ind Simp_tac "j" 1);

0

149 
by (resolve_tac [impI RS allI] 1);

2469

150 
by (ALL_IND_TAC nat_exh Asm_simp_tac 1);

755

151 
qed "succ_le2";

0

152 

5050

153 
Goal "i<succ(j) <> i=j  i<j";

2469

154 
by (IND_TAC nat_ind Simp_tac "j" 1);


155 
by (ALL_IND_TAC nat_exh Simp_tac 1);

0

156 
by (resolve_tac [impI RS allI] 1);

2469

157 
by (ALL_IND_TAC nat_exh Simp_tac 1);


158 
by (Asm_simp_tac 1);

755

159 
qed "less_succ";
