391 (* reduce contradictory <= to False. |
391 (* reduce contradictory <= to False. |
392 Most of the work is done by the cancel tactics. |
392 Most of the work is done by the cancel tactics. |
393 *) |
393 *) |
394 val add_rules = |
394 val add_rules = |
395 [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, |
395 [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, |
396 One_nat_def,isolateSuc, |
396 add_Suc, One_nat_def,isolateSuc, |
397 order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, |
397 order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, |
398 zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero]; |
398 zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero]; |
399 |
399 |
400 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s |
400 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s |
401 (fn prems => [cut_facts_tac prems 1, |
401 (fn prems => [cut_facts_tac prems 1, |