equal
deleted
inserted
replaced
1 (* Title: HOL/Word/Word_Miscellaneous.thy |
1 (* Title: HOL/Word/Word_Miscellaneous.thy |
2 Author: Miscellaneous |
2 Author: Miscellaneous |
3 *) |
3 *) |
4 |
4 |
5 section {* Miscellaneous lemmas, of at least doubtful value *} |
5 section \<open>Miscellaneous lemmas, of at least doubtful value\<close> |
6 |
6 |
7 theory Word_Miscellaneous |
7 theory Word_Miscellaneous |
8 imports Main "~~/src/HOL/Library/Bit" Misc_Numeric |
8 imports Main "~~/src/HOL/Library/Bit" Misc_Numeric |
9 begin |
9 begin |
10 |
10 |
65 apply (rule classical) |
65 apply (rule classical) |
66 apply (drule not_B1_is_B0) |
66 apply (drule not_B1_is_B0) |
67 apply (erule y) |
67 apply (erule y) |
68 done |
68 done |
69 |
69 |
70 -- "simplifications for specific word lengths" |
70 \<comment> "simplifications for specific word lengths" |
71 lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' |
71 lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' |
72 |
72 |
73 lemmas s2n_ths = n2s_ths [symmetric] |
73 lemmas s2n_ths = n2s_ths [symmetric] |
74 |
74 |
75 lemma and_len: "xs = ys ==> xs = ys & length xs = length ys" |
75 lemma and_len: "xs = ys ==> xs = ys & length xs = length ys" |