src/HOL/Word/Word.thy
changeset 61649 268d88ec9087
parent 61424 c3658c18b7bc
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Word/Word.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -960,7 +960,7 @@
     1.4    apply auto
     1.5    apply (erule_tac nat_less_iff [THEN iffD2])
     1.6    apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])
     1.7 -  apply (auto simp add : nat_power_eq int_power)
     1.8 +  apply (auto simp add : nat_power_eq of_nat_power)
     1.9    done
    1.10  
    1.11  lemma unats_uints: "unats n = nat ` uints n"
    1.12 @@ -1901,7 +1901,7 @@
    1.13  
    1.14  lemma Abs_fnat_hom_mult:
    1.15    "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
    1.16 -  by (simp add: word_of_nat wi_hom_mult zmult_int)
    1.17 +  by (simp add: word_of_nat wi_hom_mult)
    1.18  
    1.19  lemma Abs_fnat_hom_Suc:
    1.20    "word_succ (of_nat a) = of_nat (Suc a)"
    1.21 @@ -2125,9 +2125,7 @@
    1.22    "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
    1.23    apply (unfold uint_nat)
    1.24    apply (drule div_lt')
    1.25 -  apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 
    1.26 -                   nat_power_eq)
    1.27 -  done
    1.28 +  by (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
    1.29  
    1.30  lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
    1.31  
    1.32 @@ -2156,22 +2154,14 @@
    1.33  
    1.34  lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
    1.35  
    1.36 -lemma thd1:
    1.37 -  "a div b * b \<le> (a::nat)"
    1.38 -  using gt_or_eq_0 [of b]
    1.39 -  apply (rule disjE)
    1.40 -   apply (erule xtr4 [OF thd mult.commute])
    1.41 -  apply clarsimp
    1.42 -  done
    1.43 -
    1.44 -lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend thd1 
    1.45 +lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle 
    1.46  
    1.47  lemma word_mod_div_equality:
    1.48    "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
    1.49    apply (unfold word_less_nat_alt word_arith_nat_defs)
    1.50    apply (cut_tac y="unat b" in gt_or_eq_0)
    1.51    apply (erule disjE)
    1.52 -   apply (simp add: mod_div_equality uno_simps)
    1.53 +   apply (simp only: mod_div_equality uno_simps Word.word_unat.Rep_inverse)
    1.54    apply simp
    1.55    done
    1.56  
    1.57 @@ -2179,7 +2169,7 @@
    1.58    apply (unfold word_le_nat_alt word_arith_nat_defs)
    1.59    apply (cut_tac y="unat b" in gt_or_eq_0)
    1.60    apply (erule disjE)
    1.61 -   apply (simp add: div_mult_le uno_simps)
    1.62 +   apply (simp only: div_mult_le uno_simps Word.word_unat.Rep_inverse)
    1.63    apply simp
    1.64    done
    1.65  
    1.66 @@ -3305,7 +3295,7 @@
    1.67    apply (unfold dvd_def) 
    1.68    apply auto 
    1.69    apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
    1.70 -  apply (simp add : int_mult int_power)
    1.71 +  apply (simp add : int_mult of_nat_power)
    1.72    apply (simp add : nat_mult_distrib nat_power_eq)
    1.73    done
    1.74  
    1.75 @@ -4653,15 +4643,7 @@
    1.76    "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
    1.77    apply (simp add: word_rec_def unat_word_ariths)
    1.78    apply (subst nat_mod_eq')
    1.79 -   apply (cut_tac x=n in unat_lt2p)
    1.80 -   apply (drule Suc_mono)
    1.81 -   apply (simp add: less_Suc_eq_le)
    1.82 -   apply (simp only: order_less_le, simp)
    1.83 -   apply (erule contrapos_pn, simp)
    1.84 -   apply (drule arg_cong[where f=of_nat])
    1.85 -   apply simp
    1.86 -   apply (subst (asm) word_unat.Rep_inverse[of n])
    1.87 -   apply simp
    1.88 +   apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
    1.89    apply simp
    1.90    done
    1.91