equal
deleted
inserted
replaced
978 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w" |
978 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w" |
979 proof (rule bit_list_cases [of w], simp_all) |
979 proof (rule bit_list_cases [of w], simp_all) |
980 fix xs |
980 fix xs |
981 assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)" |
981 assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)" |
982 thus "norm_signed (\<zero>#xs) = \<zero>#xs" |
982 thus "norm_signed (\<zero>#xs) = \<zero>#xs" |
983 by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm) |
983 by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI] |
|
984 split: split_if_asm) |
984 next |
985 next |
985 fix xs |
986 fix xs |
986 assume "length (norm_signed (\<one>#xs)) = Suc (length xs)" |
987 assume "length (norm_signed (\<one>#xs)) = Suc (length xs)" |
987 thus "norm_signed (\<one>#xs) = \<one>#xs" |
988 thus "norm_signed (\<one>#xs) = \<one>#xs" |
988 apply (simp add: norm_signed_Cons) |
989 apply (simp add: norm_signed_Cons) |