equal
deleted
inserted
replaced
502 lemma not_false_eq_true: "(~ False) = True" by simp |
502 lemma not_false_eq_true: "(~ False) = True" by simp |
503 |
503 |
504 lemma not_true_eq_false: "(~ True) = False" by simp |
504 lemma not_true_eq_false: "(~ True) = False" by simp |
505 |
505 |
506 lemmas binarith = |
506 lemmas binarith = |
507 Pls_0_eq Min_1_eq |
507 normalize_bin_simps |
508 pred_Pls pred_Min pred_1 pred_0 |
508 pred_bin_simps succ_bin_simps |
509 succ_Pls succ_Min succ_1 succ_0 |
509 add_bin_simps minus_bin_simps mult_bin_simps |
510 add_Pls add_Min add_BIT_0 add_BIT_10 |
|
511 add_BIT_11 minus_Pls minus_Min minus_1 |
|
512 minus_0 mult_Pls mult_Min mult_num1 mult_num0 |
|
513 add_Pls_right add_Min_right |
|
514 |
510 |
515 lemma int_eq_number_of_eq: |
511 lemma int_eq_number_of_eq: |
516 "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)" |
512 "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)" |
517 by simp |
513 by simp |
518 |
514 |