src/HOL/Library/Numeral_Type.thy
changeset 66936 cf8d8fc23891
parent 66886 960509bfd47e
child 67236 d2be0579a2c8
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -168,7 +168,7 @@
     1.4    shows "P"
     1.5  apply (cases x rule: type_definition.Abs_cases [OF type])
     1.6  apply (rule_tac z="y" in 1)
     1.7 -apply (simp_all add: of_int_eq mod_pos_pos_trivial)
     1.8 +apply (simp_all add: of_int_eq)
     1.9  done
    1.10  
    1.11  lemma induct:
    1.12 @@ -229,7 +229,7 @@
    1.13             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
    1.14             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
    1.15  apply (rule mod_type.intro)
    1.16 -apply (simp add: of_nat_mult type_definition_bit0)
    1.17 +apply (simp add: type_definition_bit0)
    1.18  apply (rule one_less_int_card)
    1.19  apply (rule zero_bit0_def)
    1.20  apply (rule one_bit0_def)
    1.21 @@ -244,7 +244,7 @@
    1.22             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
    1.23             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
    1.24  apply (rule mod_type.intro)
    1.25 -apply (simp add: of_nat_mult type_definition_bit1)
    1.26 +apply (simp add: type_definition_bit1)
    1.27  apply (rule one_less_int_card)
    1.28  apply (rule zero_bit1_def)
    1.29  apply (rule one_bit1_def)
    1.30 @@ -411,12 +411,12 @@
    1.31  instance
    1.32  proof(intro_classes)
    1.33    show "distinct (enum_class.enum :: 'a bit0 list)"
    1.34 -    by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject mod_pos_pos_trivial)
    1.35 +    by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject)
    1.36  
    1.37    show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
    1.38      unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
    1.39 -    by(simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
    1.40 -      (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def mod_pos_pos_trivial)
    1.41 +    by (simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeast_lessThan)
    1.42 +      (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def)
    1.43  
    1.44    fix P :: "'a bit0 \<Rightarrow> bool"
    1.45    show "enum_class.enum_all P = Ball UNIV P"
    1.46 @@ -439,8 +439,8 @@
    1.47  
    1.48    show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
    1.49      unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
    1.50 -    by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
    1.51 -      (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def mod_pos_pos_trivial)
    1.52 +    by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeast_lessThan)
    1.53 +      (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def)
    1.54  
    1.55    fix P :: "'a bit1 \<Rightarrow> bool"
    1.56    show "enum_class.enum_all P = Ball UNIV P"