avoid using Int.Pls_def in proofs
authorhuffman
Fri Feb 24 13:50:37 2012 +0100 (2012-02-24)
changeset 46648689ebcbd6343
parent 46647 de514a98f6b6
child 46649 bb185c45037e
child 46652 bec50f8b3727
avoid using Int.Pls_def in proofs
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Word/Word.thy	Fri Feb 24 13:37:23 2012 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Fri Feb 24 13:50:37 2012 +0100
     1.3 @@ -1086,19 +1086,17 @@
     1.4  lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
     1.5    by (simp add: word_m1_wi number_of_eq)
     1.6  
     1.7 -lemma word_0_bl [simp]: "of_bl [] = 0" 
     1.8 -  unfolding of_bl_def by (simp add: Pls_def)
     1.9 +lemma word_0_bl [simp]: "of_bl [] = 0"
    1.10 +  unfolding of_bl_def by simp
    1.11  
    1.12  lemma word_1_bl: "of_bl [True] = 1" 
    1.13 -  unfolding of_bl_def
    1.14 -  by (simp add: bl_to_bin_def Bit_def Pls_def)
    1.15 -
    1.16 -lemma uint_eq_0 [simp] : "(uint 0 = 0)" 
    1.17 -  unfolding word_0_wi
    1.18 -  by (simp add: word_ubin.eq_norm Pls_def [symmetric])
    1.19 +  unfolding of_bl_def by (simp add: bl_to_bin_def)
    1.20 +
    1.21 +lemma uint_eq_0 [simp]: "uint 0 = 0"
    1.22 +  unfolding word_0_wi word_ubin.eq_norm by simp
    1.23  
    1.24  lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
    1.25 -  by (simp add: of_bl_def bl_to_bin_rep_False Pls_def)
    1.26 +  by (simp add: of_bl_def bl_to_bin_rep_False)
    1.27  
    1.28  lemma to_bl_0 [simp]:
    1.29    "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"