# HG changeset patch # User huffman # Date 1330007862 -3600 # Node ID 8c5d10d4139125a138e526f5778b6fb561e11b1e # Parent 0c3a5e28f425dacad12b7d1e01cc1023cf2d1efb make bool list functions respect int/bin distinction diff -r 0c3a5e28f425 -r 8c5d10d41391 src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Thu Feb 23 15:23:16 2012 +0100 +++ b/src/HOL/Word/Bool_List_Representation.thy Thu Feb 23 15:37:42 2012 +0100 @@ -90,14 +90,14 @@ bin_to_bl_aux (n - 1) 0 (False # bl)" by (cases n) auto -lemma bin_to_bl_aux_Pls_minus_simp [simp]: - "0 < n ==> bin_to_bl_aux n Int.Pls bl = - bin_to_bl_aux (n - 1) Int.Pls (False # bl)" +lemma bin_to_bl_aux_minus1_minus_simp [simp]: + "0 < n ==> bin_to_bl_aux n -1 bl = + bin_to_bl_aux (n - 1) -1 (True # bl)" by (cases n) auto -lemma bin_to_bl_aux_Min_minus_simp [simp]: - "0 < n ==> bin_to_bl_aux n Int.Min bl = - bin_to_bl_aux (n - 1) Int.Min (True # bl)" +lemma bin_to_bl_aux_one_minus_simp [simp]: + "0 < n \ bin_to_bl_aux n 1 bl = + bin_to_bl_aux (n - 1) 0 (True # bl)" by (cases n) auto lemma bin_to_bl_aux_Bit_minus_simp [simp]: @@ -106,13 +106,13 @@ by (cases n) auto lemma bin_to_bl_aux_Bit0_minus_simp [simp]: - "0 < n ==> bin_to_bl_aux n (Int.Bit0 w) bl = - bin_to_bl_aux (n - 1) w (False # bl)" + "0 < n ==> bin_to_bl_aux n (number_of (Int.Bit0 w)) bl = + bin_to_bl_aux (n - 1) (number_of w) (False # bl)" by (cases n) auto lemma bin_to_bl_aux_Bit1_minus_simp [simp]: - "0 < n ==> bin_to_bl_aux n (Int.Bit1 w) bl = - bin_to_bl_aux (n - 1) w (True # bl)" + "0 < n ==> bin_to_bl_aux n (number_of (Int.Bit1 w)) bl = + bin_to_bl_aux (n - 1) (number_of w) (True # bl)" by (cases n) auto text {* Link between bin and bool list. *} @@ -188,19 +188,15 @@ "bin_to_bl_aux n 0 bl = replicate n False @ bl" by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) -lemma bin_to_bl_Pls_aux: - "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl" +lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False" + unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux) + +lemma bin_to_bl_minus1_aux: + "bin_to_bl_aux n -1 bl = replicate n True @ bl" by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) -lemma bin_to_bl_Pls: "bin_to_bl n Int.Pls = replicate n False" - unfolding bin_to_bl_def by (simp add : bin_to_bl_Pls_aux) - -lemma bin_to_bl_Min_aux: - "bin_to_bl_aux n Int.Min bl = replicate n True @ bl" - by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) - -lemma bin_to_bl_Min: "bin_to_bl n Int.Min = replicate n True" - unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux) +lemma bin_to_bl_minus1: "bin_to_bl n -1 = replicate n True" + unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux) lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl" @@ -238,7 +234,7 @@ by (induct n arbitrary: w bs) auto lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n" - unfolding bin_to_bl_def len_bin_to_bl_aux by auto + by (fact size_bin_to_bl) (* FIXME: duplicate *) lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w" @@ -344,7 +340,7 @@ apply (unfold bl_to_bin_def) apply (rule xtr4) apply (rule bl_to_bin_ge2p_aux) - apply (simp add: Pls_def) + apply simp done lemma butlast_rest_bin: diff -r 0c3a5e28f425 -r 8c5d10d41391 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Feb 23 15:23:16 2012 +0100 +++ b/src/HOL/Word/Word.thy Thu Feb 23 15:37:42 2012 +0100 @@ -1102,7 +1102,7 @@ lemma to_bl_0 [simp]: "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False" unfolding uint_bl - by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric]) + by (simp add: word_size bin_to_bl_zero) lemma uint_0_iff: "(uint x = 0) = (x = 0)" by (auto intro!: word_uint.Rep_eqD)