# HG changeset patch # User huffman # Date 1187908632 -7200 # Node ID 737622204802e6ce7b3f60b4868e19ce51a5e8bf # Parent 7e42e986b1a11a3086d7b60ee89365cfef884ee6 remove unused lemmas diff -r 7e42e986b1a1 -r 737622204802 src/HOL/Word/BinGeneral.thy --- a/src/HOL/Word/BinGeneral.thy Fri Aug 24 00:23:51 2007 +0200 +++ b/src/HOL/Word/BinGeneral.thy Fri Aug 24 00:37:12 2007 +0200 @@ -17,18 +17,8 @@ (** ways in which type Bin resembles a datatype **) -lemmas BIT_eqE = BIT_eq [THEN conjE, standard] - lemmas BIT_eqI = conjI [THEN BIT_eq_iff [THEN iffD2]] -lemma less_Bits: - "(v BIT b < w BIT c) = (v < w | v <= w & b = bit.B0 & c = bit.B1)" - unfolding Bit_def by (auto split: bit.split) - -lemma le_Bits: - "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))" - unfolding Bit_def by (auto split: bit.split) - lemma neB1E [elim!]: assumes ne: "y \ bit.B1" assumes y: "y = bit.B0 \ P" @@ -38,9 +28,6 @@ apply (simp add: ne) done -lemma bin_ex_rl: "EX w b. w BIT b = bin" - by (insert BIT_exhausts [of bin], auto) - lemma bin_exhaust: assumes Q: "\x b. bin = x BIT b \ Q" shows "Q" @@ -247,12 +234,6 @@ text "Simplifications for (s)bintrunc" -lemma bit_bool: - "(b = (b' = bit.B1)) = (b' = (if b then bit.B1 else bit.B0))" - by (cases b') auto - -lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric] - lemma bin_sign_lem: "!!bin. (bin_sign (sbintrunc n bin) = Numeral.Min) = bin_nth bin n" apply (induct n)