src/HOL/Library/Numeral_Type.thy
changeset 61649 268d88ec9087
parent 61585 a9599d3d7610
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -376,7 +376,6 @@
     1.4  lemma Abs_bit0'_code [code abstract]:
     1.5    "Rep_bit0 (Abs_bit0' x :: 'a :: finite bit0) = x mod int (CARD('a bit0))"
     1.6  by(auto simp add: Abs_bit0'_def intro!: Abs_bit0_inverse)
     1.7 -  (metis bit0.Rep_Abs_mod bit0.Rep_less_n card_bit0 of_nat_numeral zmult_int)
     1.8  
     1.9  lemma inj_on_Abs_bit0:
    1.10    "inj_on (Abs_bit0 :: int \<Rightarrow> 'a bit0) {0..<2 * int CARD('a :: finite)}"
    1.11 @@ -389,8 +388,7 @@
    1.12  
    1.13  lemma Abs_bit1'_code [code abstract]:
    1.14    "Rep_bit1 (Abs_bit1' x :: 'a :: finite bit1) = x mod int (CARD('a bit1))"
    1.15 -by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
    1.16 -  (metis of_nat_0_less_iff of_nat_Suc of_nat_mult of_nat_numeral pos_mod_conj zero_less_Suc)
    1.17 +  by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
    1.18  
    1.19  lemma inj_on_Abs_bit1:
    1.20    "inj_on (Abs_bit1 :: int \<Rightarrow> 'a bit1) {0..<1 + 2 * int CARD('a :: finite)}"
    1.21 @@ -414,7 +412,7 @@
    1.22  instance
    1.23  proof(intro_classes)
    1.24    show "distinct (enum_class.enum :: 'a bit0 list)"
    1.25 -    by(auto intro!: inj_onI simp add: Abs_bit0'_def Abs_bit0_inject zmod_int[symmetric] enum_bit0_def distinct_map)
    1.26 +    by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject mod_pos_pos_trivial)
    1.27  
    1.28    show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
    1.29      unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]