author  paulson 
Mon, 09 Oct 2000 12:24:12 +0200  
changeset 10173  1d097572d23b 
parent 9969  4753185f1dd2 
child 10450  60ddd5fdf93b 
permissions  rwrr 
2441  1 
(* Title: HOL/Nat.ML 
923  2 
ID: $Id$ 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

3 
Author: Lawrence C Paulson and Tobias Nipkow 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

4 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

5 
Proofs about natural numbers and elementary arithmetic: addition, 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

6 
multiplication, etc. Some from the Hoare example from Norbert Galm. 
923  7 
*) 
8 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

9 
(** conversion rules for nat_rec **) 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

10 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

11 
val [nat_rec_0, nat_rec_Suc] = nat.recs; 
9108  12 
bind_thm ("nat_rec_0", nat_rec_0); 
13 
bind_thm ("nat_rec_Suc", nat_rec_Suc); 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

14 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

15 
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) 
5316  16 
val prems = Goal 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

17 
"[ !!n. f(n) == nat_rec c h n ] ==> f(0) = c"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

18 
by (simp_tac (simpset() addsimps prems) 1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

19 
qed "def_nat_rec_0"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

20 

5316  21 
val prems = Goal 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

22 
"[ !!n. f(n) == nat_rec c h n ] ==> f(Suc(n)) = h n (f n)"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

23 
by (simp_tac (simpset() addsimps prems) 1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

24 
qed "def_nat_rec_Suc"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

25 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

26 
val [nat_case_0, nat_case_Suc] = nat.cases; 
9108  27 
bind_thm ("nat_case_0", nat_case_0); 
28 
bind_thm ("nat_case_Suc", nat_case_Suc); 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

29 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

30 
Goal "n ~= 0 ==> EX m. n = Suc m"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

31 
by (case_tac "n" 1); 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

32 
by (REPEAT (Blast_tac 1)); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

33 
qed "not0_implies_Suc"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

34 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8442
diff
changeset

35 
Goal "!!n::nat. m<n ==> n ~= 0"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

36 
by (case_tac "n" 1); 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

37 
by (ALLGOALS Asm_full_simp_tac); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

38 
qed "gr_implies_not0"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

39 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8442
diff
changeset

40 
Goal "!!n::nat. (n ~= 0) = (0 < n)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

41 
by (case_tac "n" 1); 
7089  42 
by Auto_tac; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

43 
qed "neq0_conv"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

44 
AddIffs [neq0_conv]; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

45 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8442
diff
changeset

46 
Goal "!!n::nat. (0 ~= n) = (0 < n)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

47 
by (case_tac "n" 1); 
7089  48 
by Auto_tac; 
5644  49 
qed "zero_neq_conv"; 
50 
AddIffs [zero_neq_conv]; 

51 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

52 
(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *) 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

53 
bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

54 

8115  55 
Goal "(0<n) = (EX m. n = Suc m)"; 
56 
by(fast_tac (claset() addIs [not0_implies_Suc]) 1); 

57 
qed "gr0_conv_Suc"; 

58 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8442
diff
changeset

59 
Goal "!!n::nat. (~(0 < n)) = (n=0)"; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

60 
by (rtac iffI 1); 
10173  61 
by (rtac ccontr 1); 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

62 
by (ALLGOALS Asm_full_simp_tac); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

63 
qed "not_gr0"; 
6109  64 
AddIffs [not_gr0]; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

65 

8260  66 
Goal "(Suc n <= m') > (? m. m' = Suc m)"; 
67 
by (induct_tac "m'" 1); 

68 
by Auto_tac; 

69 
qed_spec_mp "Suc_le_D"; 

70 

6805  71 
(*Useful in certain inductive arguments*) 
72 
Goal "(m < Suc n) = (m=0  (EX j. m = Suc j & j < n))"; 

8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

73 
by (case_tac "m" 1); 
6805  74 
by Auto_tac; 
75 
qed "less_Suc_eq_0_disj"; 

76 

7058  77 
Goalw [Least_nat_def] 
78 
"[ ? n. P(Suc n); ~ P 0 ] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"; 

9969  79 
by (rtac some_equality 1); 
7058  80 
by (fold_goals_tac [Least_nat_def]); 
81 
by (safe_tac (claset() addSEs [LeastI])); 

82 
by (rename_tac "j" 1); 

8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

83 
by (case_tac "j" 1); 
7058  84 
by (Blast_tac 1); 
85 
by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1); 

86 
by (rename_tac "k n" 1); 

8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

87 
by (case_tac "k" 1); 
7058  88 
by (Blast_tac 1); 
89 
by (hyp_subst_tac 1); 

90 
by (rewtac Least_nat_def); 

9969  91 
by (rtac (some_equality RS arg_cong RS sym) 1); 
7089  92 
by (blast_tac (claset() addDs [Suc_mono]) 1); 
93 
by (cut_inst_tac [("m","m")] less_linear 1); 

94 
by (blast_tac (claset() addIs [Suc_mono]) 1); 

7058  95 
qed "Least_Suc"; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

96 

7058  97 
val prems = Goal "[ P 0; P 1; !!k. P k ==> P (Suc (Suc k)) ] ==> P n"; 
9870  98 
by (rtac nat_less_induct 1); 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

99 
by (case_tac "n" 1); 
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

100 
by (case_tac "nat" 2); 
7089  101 
by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans]))); 
7058  102 
qed "nat_induct2"; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

103 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8442
diff
changeset

104 
Goal "min 0 n = (0::nat)"; 
3023  105 
by (rtac min_leastL 1); 
5983  106 
by (Simp_tac 1); 
2608  107 
qed "min_0L"; 
1301  108 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8442
diff
changeset

109 
Goal "min n 0 = (0::nat)"; 
3023  110 
by (rtac min_leastR 1); 
5983  111 
by (Simp_tac 1); 
2608  112 
qed "min_0R"; 
923  113 

5069  114 
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)"; 
3023  115 
by (Simp_tac 1); 
2608  116 
qed "min_Suc_Suc"; 
1660  117 

2608  118 
Addsimps [min_0L,min_0R,min_Suc_Suc]; 
6433  119 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8442
diff
changeset

120 
Goalw [max_def] "max 0 n = (n::nat)"; 
6433  121 
by (Simp_tac 1); 
122 
qed "max_0L"; 

123 

8942
6aad5381ba83
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8442
diff
changeset

124 
Goalw [max_def] "max n 0 = (n::nat)"; 
6433  125 
by (Simp_tac 1); 
126 
qed "max_0R"; 

127 

128 
Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)"; 

129 
by (Simp_tac 1); 

130 
qed "max_Suc_Suc"; 

131 

132 
Addsimps [max_0L,max_0R,max_Suc_Suc]; 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

133 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

134 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

135 
(*** Basic rewrite rules for the arithmetic operators ***) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

136 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

137 
(** Difference **) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

138 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

139 
Goal "0  n = (0::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

140 
by (induct_tac "n" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

141 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

142 
qed "diff_0_eq_0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

143 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

144 
(*Must simplify BEFORE the induction! (Else we get a critical pair) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

145 
Suc(m)  Suc(n) rewrites to pred(Suc(m)  n) *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

146 
Goal "Suc(m)  Suc(n) = m  n"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

147 
by (Simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

148 
by (induct_tac "n" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

149 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

150 
qed "diff_Suc_Suc"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

151 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

152 
Addsimps [diff_0_eq_0, diff_Suc_Suc]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

153 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

154 
(* Could be (and is, below) generalized in various ways; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

155 
However, none of the generalizations are currently in the simpset, 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

156 
and I dread to think what happens if I put them in *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

157 
Goal "0 < n ==> Suc(n1) = n"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

158 
by (asm_simp_tac (simpset() addsplits [nat.split]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

159 
qed "Suc_pred"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

160 
Addsimps [Suc_pred]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

161 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

162 
Delsimps [diff_Suc]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

163 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

164 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

165 
(**** Inductive properties of the operators ****) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

166 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

167 
(*** Addition ***) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

168 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

169 
Goal "m + 0 = (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

170 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

171 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

172 
qed "add_0_right"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

173 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

174 
Goal "m + Suc(n) = Suc(m+n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

175 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

176 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

177 
qed "add_Suc_right"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

178 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

179 
Addsimps [add_0_right,add_Suc_right]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

180 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

181 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

182 
(*Associative law for addition*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

183 
Goal "(m + n) + k = m + ((n + k)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

184 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

185 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

186 
qed "add_assoc"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

187 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

188 
(*Commutative law for addition*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

189 
Goal "m + n = n + (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

190 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

191 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

192 
qed "add_commute"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

193 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

194 
Goal "x+(y+z)=y+((x+z)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

195 
by (rtac (add_commute RS trans) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

196 
by (rtac (add_assoc RS trans) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

197 
by (rtac (add_commute RS arg_cong) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

198 
qed "add_left_commute"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

199 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

200 
(*Addition is an ACoperator*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

201 
bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

202 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

203 
Goal "(k + m = k + n) = (m=(n::nat))"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

204 
by (induct_tac "k" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

205 
by (Simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

206 
by (Asm_simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

207 
qed "add_left_cancel"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

208 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

209 
Goal "(m + k = n + k) = (m=(n::nat))"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

210 
by (induct_tac "k" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

211 
by (Simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

212 
by (Asm_simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

213 
qed "add_right_cancel"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

214 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

215 
Goal "(k + m <= k + n) = (m<=(n::nat))"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

216 
by (induct_tac "k" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

217 
by (Simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

218 
by (Asm_simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

219 
qed "add_left_cancel_le"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

220 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

221 
Goal "(k + m < k + n) = (m<(n::nat))"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

222 
by (induct_tac "k" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

223 
by (Simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

224 
by (Asm_simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

225 
qed "add_left_cancel_less"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

226 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

227 
Addsimps [add_left_cancel, add_right_cancel, 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

228 
add_left_cancel_le, add_left_cancel_less]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

229 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

230 
(** Reasoning about m+0=0, etc. **) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

231 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

232 
Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

233 
by (case_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

234 
by (Auto_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

235 
qed "add_is_0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

236 
AddIffs [add_is_0]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

237 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

238 
Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

239 
by (case_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

240 
by (Auto_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

241 
qed "zero_is_add"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

242 
AddIffs [zero_is_add]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

243 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

244 
Goal "!!m::nat. (m+n=1) = (m=1 & n=0  m=0 & n=1)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

245 
by (case_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

246 
by (Auto_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

247 
qed "add_is_1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

248 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

249 
Goal "!!m::nat. (1=m+n) = (m=1 & n=0  m=0 & n=1)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

250 
by (case_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

251 
by (Auto_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

252 
qed "one_is_add"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

253 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

254 
Goal "!!m::nat. (0<m+n) = (0<m  0<n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

255 
by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

256 
qed "add_gr_0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

257 
AddIffs [add_gr_0]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

258 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

259 
Goal "!!m::nat. m + n = m ==> n = 0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

260 
by (dtac (add_0_right RS ssubst) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

261 
by (asm_full_simp_tac (simpset() addsimps [add_assoc] 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

262 
delsimps [add_0_right]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

263 
qed "add_eq_self_zero"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

264 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

265 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

266 
(**** Additional theorems about "less than" ****) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

267 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

268 
(*Deleted less_natE; instead use less_eq_Suc_add RS exE*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

269 
Goal "m<n > (EX k. n=Suc(m+k))"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

270 
by (induct_tac "n" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

271 
by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

272 
by (blast_tac (claset() addSEs [less_SucE] 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

273 
addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

274 
qed_spec_mp "less_eq_Suc_add"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

275 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

276 
Goal "n <= ((m + n)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

277 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

278 
by (ALLGOALS Simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

279 
by (etac le_SucI 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

280 
qed "le_add2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

281 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

282 
Goal "n <= ((n + m)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

283 
by (simp_tac (simpset() addsimps add_ac) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

284 
by (rtac le_add2 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

285 
qed "le_add1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

286 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

287 
bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

288 
bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

289 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

290 
Goal "(m<n) = (EX k. n=Suc(m+k))"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

291 
by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

292 
qed "less_iff_Suc_add"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

293 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

294 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

295 
(*"i <= j ==> i <= j+m"*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

296 
bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans)); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

297 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

298 
(*"i <= j ==> i <= m+j"*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

299 
bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans)); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

300 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

301 
(*"i < j ==> i < j+m"*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

302 
bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans)); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

303 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

304 
(*"i < j ==> i < m+j"*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

305 
bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans)); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

306 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

307 
Goal "i+j < (k::nat) > i<k"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

308 
by (induct_tac "j" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

309 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

310 
by (blast_tac (claset() addDs [Suc_lessD]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

311 
qed_spec_mp "add_lessD1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

312 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

313 
Goal "~ (i+j < (i::nat))"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

314 
by (rtac notI 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

315 
by (etac (add_lessD1 RS less_irrefl) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

316 
qed "not_add_less1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

317 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

318 
Goal "~ (j+i < (i::nat))"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

319 
by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

320 
qed "not_add_less2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

321 
AddIffs [not_add_less1, not_add_less2]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

322 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

323 
Goal "m+k<=n > m<=(n::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

324 
by (induct_tac "k" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

325 
by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

326 
qed_spec_mp "add_leD1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

327 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

328 
Goal "m+k<=n ==> k<=(n::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

329 
by (full_simp_tac (simpset() addsimps [add_commute]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

330 
by (etac add_leD1 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

331 
qed_spec_mp "add_leD2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

332 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

333 
Goal "m+k<=n ==> m<=n & k<=(n::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

334 
by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

335 
bind_thm ("add_leE", result() RS conjE); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

336 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

337 
(*needs !!k for add_ac to work*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

338 
Goal "!!k:: nat. [ k<l; m+l = k+n ] ==> m<n"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

339 
by (force_tac (claset(), 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

340 
simpset() delsimps [add_Suc_right] 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

341 
addsimps [less_iff_Suc_add, 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

342 
add_Suc_right RS sym] @ add_ac) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

343 
qed "less_add_eq_less"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

344 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

345 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

346 
(*** Monotonicity of Addition ***) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

347 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

348 
(*strict, in 1st argument*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

349 
Goal "i < j ==> i + k < j + (k::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

350 
by (induct_tac "k" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

351 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

352 
qed "add_less_mono1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

353 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

354 
(*strict, in both arguments*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

355 
Goal "[i < j; k < l] ==> i + k < j + (l::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

356 
by (rtac (add_less_mono1 RS less_trans) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

357 
by (REPEAT (assume_tac 1)); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

358 
by (induct_tac "j" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

359 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

360 
qed "add_less_mono"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

361 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

362 
(*A [clumsy] way of lifting < monotonicity to <= monotonicity *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

363 
val [lt_mono,le] = Goal 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

364 
"[ !!i j::nat. i<j ==> f(i) < f(j); \ 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

365 
\ i <= j \ 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

366 
\ ] ==> f(i) <= (f(j)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

367 
by (cut_facts_tac [le] 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

368 
by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

369 
by (blast_tac (claset() addSIs [lt_mono]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

370 
qed "less_mono_imp_le_mono"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

371 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

372 
(*nonstrict, in 1st argument*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

373 
Goal "i<=j ==> i + k <= j + (k::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

374 
by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

375 
by (etac add_less_mono1 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

376 
by (assume_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

377 
qed "add_le_mono1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

378 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

379 
(*nonstrict, in both arguments*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

380 
Goal "[i<=j; k<=l ] ==> i + k <= j + (l::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

381 
by (etac (add_le_mono1 RS le_trans) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

382 
by (simp_tac (simpset() addsimps [add_commute]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

383 
qed "add_le_mono"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

384 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

385 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

386 
(*** Multiplication ***) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

387 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

388 
(*right annihilation in product*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

389 
Goal "!!m::nat. m * 0 = 0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

390 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

391 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

392 
qed "mult_0_right"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

393 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

394 
(*right successor law for multiplication*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

395 
Goal "m * Suc(n) = m + (m * n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

396 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

397 
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

398 
qed "mult_Suc_right"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

399 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

400 
Addsimps [mult_0_right, mult_Suc_right]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

401 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

402 
Goal "1 * n = n"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

403 
by (Asm_simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

404 
qed "mult_1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

405 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

406 
Goal "n * 1 = n"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

407 
by (Asm_simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

408 
qed "mult_1_right"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

409 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

410 
(*Commutative law for multiplication*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

411 
Goal "m * n = n * (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

412 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

413 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

414 
qed "mult_commute"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

415 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

416 
(*addition distributes over multiplication*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

417 
Goal "(m + n)*k = (m*k) + ((n*k)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

418 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

419 
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

420 
qed "add_mult_distrib"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

421 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

422 
Goal "k*(m + n) = (k*m) + ((k*n)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

423 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

424 
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

425 
qed "add_mult_distrib2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

426 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

427 
(*Associative law for multiplication*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

428 
Goal "(m * n) * k = m * ((n * k)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

429 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

430 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

431 
qed "mult_assoc"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

432 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

433 
Goal "x*(y*z) = y*((x*z)::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

434 
by (rtac trans 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

435 
by (rtac mult_commute 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

436 
by (rtac trans 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

437 
by (rtac mult_assoc 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

438 
by (rtac (mult_commute RS arg_cong) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

439 
qed "mult_left_commute"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

440 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

441 
bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

442 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

443 
Goal "!!m::nat. (m*n = 0) = (m=0  n=0)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

444 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

445 
by (induct_tac "n" 2); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

446 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

447 
qed "mult_is_0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

448 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

449 
Goal "!!m::nat. (0 = m*n) = (0=m  0=n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

450 
by (stac eq_commute 1 THEN stac mult_is_0 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

451 
by Auto_tac; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

452 
qed "zero_is_mult"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

453 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

454 
Addsimps [mult_is_0, zero_is_mult]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

455 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

456 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

457 
(*** Difference ***) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

458 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

459 
Goal "!!m::nat. m  m = 0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

460 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

461 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

462 
qed "diff_self_eq_0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

463 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

464 
Addsimps [diff_self_eq_0]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

465 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

466 
(*Addition is the inverse of subtraction: if n<=m then n+(mn) = m. *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

467 
Goal "~ m<n > n+(mn) = (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

468 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

469 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

470 
qed_spec_mp "add_diff_inverse"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

471 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

472 
Goal "n<=m ==> n+(mn) = (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

473 
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

474 
qed "le_add_diff_inverse"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

475 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

476 
Goal "n<=m ==> (mn)+n = (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

477 
by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

478 
qed "le_add_diff_inverse2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

479 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

480 
Addsimps [le_add_diff_inverse, le_add_diff_inverse2]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

481 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

482 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

483 
(*** More results about difference ***) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

484 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

485 
Goal "n <= m ==> Suc(m)n = Suc(mn)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

486 
by (etac rev_mp 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

487 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

488 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

489 
qed "Suc_diff_le"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

490 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

491 
Goal "m  n < Suc(m)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

492 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

493 
by (etac less_SucE 3); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

494 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

495 
qed "diff_less_Suc"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

496 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

497 
Goal "m  n <= (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

498 
by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

499 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

500 
qed "diff_le_self"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

501 
Addsimps [diff_le_self]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

502 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

503 
(* j<k ==> jn < k *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

504 
bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

505 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

506 
Goal "!!i::nat. ijk = i  (j+k)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

507 
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

508 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

509 
qed "diff_diff_left"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

510 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

511 
Goal "(Suc m  n)  Suc k = m  n  k"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

512 
by (simp_tac (simpset() addsimps [diff_diff_left]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

513 
qed "Suc_diff_diff"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

514 
Addsimps [Suc_diff_diff]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

515 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

516 
Goal "0<n ==> n  Suc i < n"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

517 
by (case_tac "n" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

518 
by Safe_tac; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

519 
by (asm_simp_tac (simpset() addsimps le_simps) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

520 
qed "diff_Suc_less"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

521 
Addsimps [diff_Suc_less]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

522 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

523 
(*This and the next few suggested by Florian Kammueller*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

524 
Goal "!!i::nat. ijk = ikj"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

525 
by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

526 
qed "diff_commute"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

527 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

528 
Goal "k <= (j::nat) > (i + j)  k = i + (j  k)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

529 
by (res_inst_tac [("m","j"),("n","k")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

530 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

531 
qed_spec_mp "diff_add_assoc"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

532 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

533 
Goal "k <= (j::nat) > (j + i)  k = (j  k) + i"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

534 
by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

535 
qed_spec_mp "diff_add_assoc2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

536 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

537 
Goal "(n+m)  n = (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

538 
by (induct_tac "n" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

539 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

540 
qed "diff_add_inverse"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

541 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

542 
Goal "(m+n)  n = (m::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

543 
by (simp_tac (simpset() addsimps [diff_add_assoc]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

544 
qed "diff_add_inverse2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

545 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

546 
Goal "i <= (j::nat) ==> (ji=k) = (j=k+i)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

547 
by Safe_tac; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

548 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

549 
qed "le_imp_diff_is_add"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

550 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

551 
Goal "!!m::nat. (mn = 0) = (m <= n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

552 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

553 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

554 
qed "diff_is_0_eq"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

555 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

556 
Goal "!!m::nat. (0 = mn) = (m <= n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

557 
by (stac (diff_is_0_eq RS sym) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

558 
by (rtac eq_sym_conv 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

559 
qed "zero_is_diff_eq"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

560 
Addsimps [diff_is_0_eq, zero_is_diff_eq]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

561 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

562 
Goal "!!m::nat. (0<nm) = (m<n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

563 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

564 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

565 
qed "zero_less_diff"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

566 
Addsimps [zero_less_diff]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

567 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

568 
Goal "i < j ==> EX k::nat. 0<k & i+k = j"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

569 
by (res_inst_tac [("x","j  i")] exI 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

570 
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

571 
qed "less_imp_add_positive"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

572 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

573 
Goal "P(k) > (ALL n. P(Suc(n))> P(n)) > P(ki)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

574 
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

575 
by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac)); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

576 
qed "zero_induct_lemma"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

577 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

578 
val prems = Goal "[ P(k); !!n. P(Suc(n)) ==> P(n) ] ==> P(0)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

579 
by (rtac (diff_self_eq_0 RS subst) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

580 
by (rtac (zero_induct_lemma RS mp RS mp) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

581 
by (REPEAT (ares_tac ([impI,allI]@prems) 1)); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

582 
qed "zero_induct"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

583 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

584 
Goal "(k+m)  (k+n) = m  (n::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

585 
by (induct_tac "k" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

586 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

587 
qed "diff_cancel"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

588 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

589 
Goal "(m+k)  (n+k) = m  (n::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

590 
by (asm_simp_tac 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

591 
(simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

592 
qed "diff_cancel2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

593 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

594 
Goal "n  (n+m) = (0::nat)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

595 
by (induct_tac "n" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

596 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

597 
qed "diff_add_0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

598 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

599 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

600 
(** Difference distributes over multiplication **) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

601 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

602 
Goal "!!m::nat. (m  n) * k = (m * k)  (n * k)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

603 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

604 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

605 
qed "diff_mult_distrib" ; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

606 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

607 
Goal "!!m::nat. k * (m  n) = (k * m)  (k * n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

608 
val mult_commute_k = read_instantiate [("m","k")] mult_commute; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

609 
by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

610 
qed "diff_mult_distrib2" ; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

611 
(*NOT added as rewrites, since sometimes they are used from righttoleft*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

612 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

613 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

614 
(*** Monotonicity of Multiplication ***) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

615 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

616 
Goal "i <= (j::nat) ==> i*k<=j*k"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

617 
by (induct_tac "k" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

618 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

619 
qed "mult_le_mono1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

620 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

621 
Goal "i <= (j::nat) ==> k*i <= k*j"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

622 
by (dtac mult_le_mono1 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

623 
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

624 
qed "mult_le_mono2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

625 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

626 
(* <= monotonicity, BOTH arguments*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

627 
Goal "[ i <= (j::nat); k <= l ] ==> i*k <= j*l"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

628 
by (etac (mult_le_mono1 RS le_trans) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

629 
by (etac mult_le_mono2 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

630 
qed "mult_le_mono"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

631 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

632 
(*strict, in 1st argument; proof is by induction on k>0*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

633 
Goal "!!i::nat. [ i<j; 0<k ] ==> k*i < k*j"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

634 
by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

635 
by (Asm_simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

636 
by (induct_tac "x" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

637 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

638 
qed "mult_less_mono2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

639 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

640 
Goal "!!i::nat. [ i<j; 0<k ] ==> i*k < j*k"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

641 
by (dtac mult_less_mono2 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

642 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute]))); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

643 
qed "mult_less_mono1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

644 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

645 
Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

646 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

647 
by (case_tac "n" 2); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

648 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

649 
qed "zero_less_mult_iff"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

650 
Addsimps [zero_less_mult_iff]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

651 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

652 
Goal "(1 <= m*n) = (1<=m & 1<=n)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

653 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

654 
by (case_tac "n" 2); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

655 
by (ALLGOALS Asm_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

656 
qed "one_le_mult_iff"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

657 
Addsimps [one_le_mult_iff]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

658 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

659 
Goal "(m*n = 1) = (m=1 & n=1)"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

660 
by (induct_tac "m" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

661 
by (Simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

662 
by (induct_tac "n" 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

663 
by (Simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

664 
by (fast_tac (claset() addss simpset()) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

665 
qed "mult_eq_1_iff"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

666 
Addsimps [mult_eq_1_iff]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

667 

9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

668 
Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)"; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

669 
by (safe_tac (claset() addSIs [mult_less_mono1])); 
9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

670 
by (case_tac "k" 1); 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

671 
by Auto_tac; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

672 
by (full_simp_tac (simpset() delsimps [le_0_eq] 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

673 
addsimps [linorder_not_le RS sym]) 1); 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

674 
by (blast_tac (claset() addIs [mult_le_mono1]) 1); 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

675 
qed "mult_less_cancel2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

676 

9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

677 
Goal "!!m::nat. (k*m < k*n) = (0<k & m<n)"; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

678 
by (simp_tac (simpset() addsimps [mult_less_cancel2, 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

679 
inst "m" "k" mult_commute]) 1); 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

680 
qed "mult_less_cancel1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

681 
Addsimps [mult_less_cancel1, mult_less_cancel2]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

682 

9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

683 
Goal "!!m::nat. (m*k <= n*k) = (0<k > m<=n)"; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

684 
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

685 
by Auto_tac; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

686 
qed "mult_le_cancel2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

687 

9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

688 
Goal "!!m::nat. (k*m <= k*n) = (0<k > m<=n)"; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

689 
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

690 
by Auto_tac; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

691 
qed "mult_le_cancel1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

692 
Addsimps [mult_le_cancel1, mult_le_cancel2]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

693 

9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

694 
Goal "(m*k = n*k) = (m=n  (k = (0::nat)))"; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

695 
by (cut_facts_tac [less_linear] 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

696 
by Safe_tac; 
9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

697 
by Auto_tac; 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

698 
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac)); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

699 
by (ALLGOALS Asm_full_simp_tac); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

700 
qed "mult_cancel2"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

701 

9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

702 
Goal "(k*m = k*n) = (m=n  (k = (0::nat)))"; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

703 
by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1); 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

704 
qed "mult_cancel1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

705 
Addsimps [mult_cancel1, mult_cancel2]; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

706 

9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

707 
Goal "(Suc k * m < Suc k * n) = (m < n)"; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

708 
by (stac mult_less_cancel1 1); 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

709 
by (Simp_tac 1); 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

710 
qed "Suc_mult_less_cancel1"; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

711 

47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

712 
Goal "(Suc k * m <= Suc k * n) = (m <= n)"; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

713 
by (stac mult_le_cancel1 1); 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

714 
by (Simp_tac 1); 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

715 
qed "Suc_mult_le_cancel1"; 
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

716 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

717 
Goal "(Suc k * m = Suc k * n) = (m = n)"; 
9637
47d39a31eb2f
better rules for cancellation of common factors across comparisons
paulson
parents:
9436
diff
changeset

718 
by (stac mult_cancel1 1); 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

719 
by (Simp_tac 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

720 
qed "Suc_mult_cancel1"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

721 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

722 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

723 
(*Lemma for gcd*) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

724 
Goal "!!m::nat. m = m*n ==> n=1  m=0"; 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

725 
by (dtac sym 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

726 
by (rtac disjCI 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

727 
by (rtac nat_less_cases 1 THEN assume_tac 2); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

728 
by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

729 
by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1); 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9108
diff
changeset

730 
qed "mult_eq_self_implies_10"; 