equal
deleted
inserted
replaced
1586 using inc_induct[of "k - i" k P, simplified] by blast |
1586 using inc_induct[of "k - i" k P, simplified] by blast |
1587 |
1587 |
1588 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0" |
1588 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0" |
1589 using inc_induct[of 0 k P] by blast |
1589 using inc_induct[of 0 k P] by blast |
1590 |
1590 |
1591 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False" |
|
1592 by auto |
|
1593 |
|
1594 (*The others are |
1591 (*The others are |
1595 i - j - k = i - (j + k), |
1592 i - j - k = i - (j + k), |
1596 k \<le> j ==> j - k + i = j + i - k, |
1593 k \<le> j ==> j - k + i = j + i - k, |
1597 k \<le> j ==> i + (j - k) = i + j - k *) |
1594 k \<le> j ==> i + (j - k) = i + j - k *) |
1598 lemmas add_diff_assoc = diff_add_assoc [symmetric] |
1595 lemmas add_diff_assoc = diff_add_assoc [symmetric] |