src/HOL/Word/Bit_Representation.thy
changeset 67142 fa1173288322
parent 65363 5eb619751b14
child 67160 f37bf261bdf6
     1.1 --- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 05 16:54:37 2017 +0100
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 06 09:11:27 2017 +0100
     1.3 @@ -139,14 +139,8 @@
     1.4  lemma bin_ex_rl: "\<exists>w b. w BIT b = bin"
     1.5    by (metis bin_rl_simp)
     1.6  
     1.7 -lemma bin_exhaust:
     1.8 -  assumes that: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
     1.9 -  shows "Q"
    1.10 -  apply (insert bin_ex_rl [of bin])
    1.11 -  apply (erule exE)+
    1.12 -  apply (rule that)
    1.13 -  apply force
    1.14 -  done
    1.15 +lemma bin_exhaust: "(\<And>x b. bin = x BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
    1.16 +by (metis bin_ex_rl)
    1.17  
    1.18  primrec bin_nth
    1.19    where