src/HOL/Word/Word.thy
changeset 46617 8c5d10d41391
parent 46604 9f9e85264e4d
child 46618 a8c342aa53d6
equal deleted inserted replaced
46610:0c3a5e28f425 46617:8c5d10d41391
  1100   by (simp add: of_bl_def bl_to_bin_rep_False Pls_def)
  1100   by (simp add: of_bl_def bl_to_bin_rep_False Pls_def)
  1101 
  1101 
  1102 lemma to_bl_0 [simp]:
  1102 lemma to_bl_0 [simp]:
  1103   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
  1103   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
  1104   unfolding uint_bl
  1104   unfolding uint_bl
  1105   by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])
  1105   by (simp add: word_size bin_to_bl_zero)
  1106 
  1106 
  1107 lemma uint_0_iff: "(uint x = 0) = (x = 0)"
  1107 lemma uint_0_iff: "(uint x = 0) = (x = 0)"
  1108   by (auto intro!: word_uint.Rep_eqD)
  1108   by (auto intro!: word_uint.Rep_eqD)
  1109 
  1109 
  1110 lemma unat_0_iff: "(unat x = 0) = (x = 0)"
  1110 lemma unat_0_iff: "(unat x = 0) = (x = 0)"