src/HOL/Word/Word.thy
changeset 48196 b7313810b6e6
parent 47941 22e001795641
child 48891 c0eafbd55de3
equal deleted inserted replaced
48195:3127f9ce52fb 48196:b7313810b6e6
  2342   shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
  2342   shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
  2343 lemma leao: 
  2343 lemma leao: 
  2344   fixes x' :: "'a::len0 word"
  2344   fixes x' :: "'a::len0 word"
  2345   shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 
  2345   shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 
  2346 
  2346 
  2347 lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
  2347 lemma word_ao_equiv:
       
  2348   fixes w w' :: "'a::len0 word"
       
  2349   shows "(w = w OR w') = (w' = w AND w')"
       
  2350   by (auto intro: leoa leao)
  2348 
  2351 
  2349 lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
  2352 lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
  2350   unfolding word_le_def uint_or
  2353   unfolding word_le_def uint_or
  2351   by (auto intro: le_int_or) 
  2354   by (auto intro: le_int_or) 
  2352 
  2355