102 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
102 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
103 by (auto_tac (claset(), |
103 by (auto_tac (claset(), |
104 simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, zadd_int])); |
104 simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, zadd_int])); |
105 qed "zless_add_int_Suc_eq"; |
105 qed "zless_add_int_Suc_eq"; |
106 |
106 |
107 |
|
108 Goal "(w + int (Suc m) <= z) = (w + int m < z)"; |
107 Goal "(w + int (Suc m) <= z) = (w + int m < z)"; |
109 by (simp_tac (simpset() addsimps [zle_def, zless_add_int_Suc_eq]) 1); |
108 by (simp_tac (simpset() addsimps [zle_def, zless_add_int_Suc_eq]) 1); |
110 by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym], |
109 by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym], |
111 simpset() addsimps [zless_imp_zle, symmetric zle_def])); |
110 simpset() addsimps [zless_imp_zle, symmetric zle_def])); |
112 qed "add_int_Suc_zle_eq"; |
111 qed "add_int_Suc_zle_eq"; |
113 |
|
114 |
|
115 (* (w < int (Suc m)) = (w < int m | w = int m) *) |
|
116 bind_thm ("less_int_Suc_eq", |
|
117 simplify (simpset()) |
|
118 (read_instantiate [("z", "int 0")] zless_add_int_Suc_eq)); |
|
119 |
|
120 Goal "(w <= int (Suc m)) = (w <= int m | w = int (Suc m))"; |
|
121 by (simp_tac (simpset() addsimps [less_int_Suc_eq, order_le_less]) 1); |
|
122 qed "le_int_Suc_eq"; |
|
123 |
112 |
124 |
113 |
125 (*** Monotonicity results ***) |
114 (*** Monotonicity results ***) |
126 |
115 |
127 Goal "(v+z < w+z) = (v < (w::int))"; |
116 Goal "(v+z < w+z) = (v < (w::int))"; |