equal
deleted
inserted
replaced
364 local |
364 local |
365 |
365 |
366 (* reduce contradictory <= to False. |
366 (* reduce contradictory <= to False. |
367 Most of the work is done by the cancel tactics. |
367 Most of the work is done by the cancel tactics. |
368 *) |
368 *) |
369 val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,One_nat_def]; |
369 val add_rules = |
|
370 [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, |
|
371 add_not_0_if_left_not_0,add_not_0_if_right_not_0, |
|
372 add_not_0_if_left_not_0 RS not_sym,add_not_0_if_right_not_0 RS not_sym, |
|
373 One_nat_def]; |
370 |
374 |
371 val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s |
375 val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s |
372 (fn prems => [cut_facts_tac prems 1, |
376 (fn prems => [cut_facts_tac prems 1, |
373 blast_tac (claset() addIs [add_le_mono]) 1])) |
377 blast_tac (claset() addIs [add_le_mono]) 1])) |
374 ["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)", |
378 ["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)", |