src/ZF/arith.ML
changeset 127 eec6bb9c58ea
parent 25 3ac1c0c0016e
equal deleted inserted replaced
126:0b0055b3ccfe 127:eec6bb9c58ea
   226     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   226     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   227 
   227 
   228 (*Addition is the inverse of subtraction*)
   228 (*Addition is the inverse of subtraction*)
   229 goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
   229 goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
   230 by (forward_tac [lt_nat_in_nat] 1);
   230 by (forward_tac [lt_nat_in_nat] 1);
   231 be nat_succI 1;
   231 by (etac nat_succI 1);
   232 by (etac rev_mp 1);
   232 by (etac rev_mp 1);
   233 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   233 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   234 by (ALLGOALS (asm_simp_tac arith_ss));
   234 by (ALLGOALS (asm_simp_tac arith_ss));
   235 val add_diff_inverse = result();
   235 val add_diff_inverse = result();
   236 
   236 
   332 (** Monotonicity of addition **)
   332 (** Monotonicity of addition **)
   333 
   333 
   334 (*strict, in 1st argument*)
   334 (*strict, in 1st argument*)
   335 goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
   335 goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
   336 by (forward_tac [lt_nat_in_nat] 1);
   336 by (forward_tac [lt_nat_in_nat] 1);
   337 ba 1;
   337 by (assume_tac 1);
   338 by (etac succ_lt_induct 1);
   338 by (etac succ_lt_induct 1);
   339 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
   339 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
   340 val add_lt_mono1 = result();
   340 val add_lt_mono1 = result();
   341 
   341 
   342 (*strict, in both arguments*)
   342 (*strict, in both arguments*)