540 |
540 |
541 text\<open>Difference and less-than\<close> |
541 text\<open>Difference and less-than\<close> |
542 |
542 |
543 lemma diff_lt_imp_lt: "[|(k#-i) < (k#-j); i\<in>nat; j\<in>nat; k\<in>nat|] ==> j<i" |
543 lemma diff_lt_imp_lt: "[|(k#-i) < (k#-j); i\<in>nat; j\<in>nat; k\<in>nat|] ==> j<i" |
544 apply (erule rev_mp) |
544 apply (erule rev_mp) |
545 apply (simp split add: nat_diff_split, auto) |
545 apply (simp split: nat_diff_split, auto) |
546 apply (blast intro: add_le_self lt_trans1) |
546 apply (blast intro: add_le_self lt_trans1) |
547 apply (rule not_le_iff_lt [THEN iffD1], auto) |
547 apply (rule not_le_iff_lt [THEN iffD1], auto) |
548 apply (subgoal_tac "i #+ da < j #+ d", force) |
548 apply (subgoal_tac "i #+ da < j #+ d", force) |
549 apply (blast intro: add_le_lt_mono) |
549 apply (blast intro: add_le_lt_mono) |
550 done |
550 done |
551 |
551 |
552 lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)" |
552 lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)" |
553 apply (frule le_in_nat, assumption) |
553 apply (frule le_in_nat, assumption) |
554 apply (frule lt_nat_in_nat, assumption) |
554 apply (frule lt_nat_in_nat, assumption) |
555 apply (simp split add: nat_diff_split, auto) |
555 apply (simp split: nat_diff_split, auto) |
556 apply (blast intro: lt_asym lt_trans2) |
556 apply (blast intro: lt_asym lt_trans2) |
557 apply (blast intro: lt_irrefl lt_trans2) |
557 apply (blast intro: lt_irrefl lt_trans2) |
558 apply (rule not_le_iff_lt [THEN iffD1], auto) |
558 apply (rule not_le_iff_lt [THEN iffD1], auto) |
559 apply (subgoal_tac "j #+ d < i #+ da", force) |
559 apply (subgoal_tac "j #+ d < i #+ da", force) |
560 apply (blast intro: add_lt_le_mono) |
560 apply (blast intro: add_lt_le_mono) |