# HG changeset patch # User huffman # Date 1323783554 -3600 # Node ID 40554613b4f09cb5544b872a5333de642d7f4f03 # Parent cbb6f2243b52c05a6c5555debdce2213b356ea43 replace many uses of 'lemmas' with explicit 'lemma' diff -r cbb6f2243b52 -r 40554613b4f0 src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Tue Dec 13 14:02:02 2011 +0100 +++ b/src/HOL/Word/Bool_List_Representation.thy Tue Dec 13 14:39:14 2011 +0100 @@ -231,8 +231,10 @@ apply auto done -lemmas bin_to_bl_bintr = - bin_to_bl_aux_bintr [where bl = "[]", folded bin_to_bl_def] +lemma bin_to_bl_bintr: + "bin_to_bl n (bintrunc m bin) = + replicate (n - m) False @ bin_to_bl (min n m) bin" + unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr) lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls" by (induct n) auto @@ -301,7 +303,8 @@ apply arith done -lemmas nth_rev_alt = nth_rev [where xs = "rev ys", simplified] for ys +lemma nth_rev_alt: "n < length ys \ ys ! n = rev ys ! (length ys - Suc n)" + by (simp add: nth_rev) lemma nth_bin_to_bl_aux [rule_format] : "ALL w n bl. n < m + length bl --> (bin_to_bl_aux m w bl) ! n = @@ -362,8 +365,9 @@ apply (auto simp add: bin_to_bl_aux_alt) done -lemmas butlast_bin_rest = butlast_rest_bin - [where w="bl_to_bin bl" and n="length bl", simplified] for bl +lemma butlast_bin_rest: + "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))" + using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp lemma butlast_rest_bl2bin_aux: "bl ~= [] \ @@ -402,8 +406,9 @@ "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)" unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux) -lemmas trunc_bl2bin_len [simp] = - trunc_bl2bin [of "length bl" bl, simplified] for bl +lemma trunc_bl2bin_len [simp]: + "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl" + by (simp add: trunc_bl2bin) lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)" @@ -493,17 +498,20 @@ apply clarsimp done -lemmas bl_not_bin = bl_not_aux_bin - [where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps] +lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)" + unfolding bin_to_bl_def by (simp add: bl_not_aux_bin) -lemmas bl_and_bin = bl_and_aux_bin [where bs="[]" and cs="[]", - unfolded map2_Nil, folded bin_to_bl_def] +lemma bl_and_bin: + "map2 (op \) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)" + unfolding bin_to_bl_def by (simp add: bl_and_aux_bin) -lemmas bl_or_bin = bl_or_aux_bin [where bs="[]" and cs="[]", - unfolded map2_Nil, folded bin_to_bl_def] +lemma bl_or_bin: + "map2 (op \) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)" + unfolding bin_to_bl_def by (simp add: bl_or_aux_bin) -lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]", - unfolded map2_Nil, folded bin_to_bl_def] +lemma bl_xor_bin: + "map2 (\x y. x \ y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)" + unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil) lemma drop_bin2bl_aux [rule_format] : "ALL m bin bs. drop m (bin_to_bl_aux n bin bs) = @@ -617,10 +625,11 @@ lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))" by (simp add : takefill_bintrunc) - -lemmas bl_bin_bl_rep_drop = - bl_bin_bl_rtf [simplified takefill_alt, - simplified, simplified rev_take, simplified] + +lemma bl_bin_bl_rep_drop: + "bin_to_bl n (bl_to_bin bl) = + replicate (n - length bl) False @ drop (length bl - n) bl" + by (simp add: bl_bin_bl_rtf takefill_alt rev_take) lemma tf_rev: "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) = @@ -662,12 +671,15 @@ bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)" by (induct nw) auto -lemmas bl_to_bin_aux_alt = - bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls", - simplified bl_to_bin_def [symmetric], simplified] +lemma bl_to_bin_aux_alt: + "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)" + using bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls"] + unfolding bl_to_bin_def [symmetric] by simp -lemmas bin_to_bl_cat = - bin_to_bl_aux_cat [where bs = "[]", folded bin_to_bl_def] +lemma bin_to_bl_cat: + "bin_to_bl (nv + nw) (bin_cat v nw w) = + bin_to_bl_aux nv v (bin_to_bl nw w)" + unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat) lemmas bl_to_bin_aux_app_cat = trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt] @@ -675,11 +687,13 @@ lemmas bin_to_bl_aux_cat_app = trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt] -lemmas bl_to_bin_app_cat = bl_to_bin_aux_app_cat - [where w = "Int.Pls", folded bl_to_bin_def] +lemma bl_to_bin_app_cat: + "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)" + by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def) -lemmas bin_to_bl_cat_app = bin_to_bl_aux_cat_app - [where bs = "[]", folded bin_to_bl_def] +lemma bin_to_bl_cat_app: + "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa" + by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app) (* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *) lemma bl_to_bin_app_cat_alt: @@ -727,7 +741,8 @@ apply simp done -lemmas bl_of_nth_nth [simp] = order_refl [THEN bl_of_nth_nth_le, simplified] +lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) (op ! (rev xs)) = xs" + by (simp add: bl_of_nth_nth_le) lemma size_rbl_pred: "length (rbl_pred bl) = length bl" by (induct bl) auto @@ -929,8 +944,9 @@ lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps -lemmas seqr = eq_reflection [where x = "size w"] for w +lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *) +(* TODO: move name bindings to List.thy *) lemmas tl_Nil = tl.simps (1) lemmas tl_Cons = tl.simps (2)