# HG changeset patch # User haftmann # Date 1592471249 0 # Node ID 476b9e6904d97b580c658805b736e503360d9627 # Parent 4d4079159be7de7ea2b56908bea99474fb69972f replaced mere alias by input abbreviation diff -r 4d4079159be7 -r 476b9e6904d9 NEWS --- a/NEWS Thu Jun 18 09:07:29 2020 +0000 +++ b/NEWS Thu Jun 18 09:07:29 2020 +0000 @@ -48,8 +48,8 @@ * For the natural numbers, Sup {} = 0. -* Session HOL-Word: Operations "bin_last", "bin_rest" and "max_word" -are now mere input abbreviations. INCOMPATIBILITY. +* Session HOL-Word: Operations "bin_last", "bin_rest", "bintrunc" +and "max_word" are now mere input abbreviations. INCOMPATIBILITY. * Session HOL-Word: Compound operation "bin_split" simplifies by default into its components "drop_bit" and "take_bit". Minor INCOMPATIBILITY. diff -r 4d4079159be7 -r 476b9e6904d9 src/HOL/Word/Bits_Int.thy --- a/src/HOL/Word/Bits_Int.thy Thu Jun 18 09:07:29 2020 +0000 +++ b/src/HOL/Word/Bits_Int.thy Thu Jun 18 09:07:29 2020 +0000 @@ -404,26 +404,16 @@ lemma bin_sign_rest [simp]: "bin_sign (bin_rest w) = bin_sign w" by (cases w rule: bin_exhaust) auto -primrec bintrunc :: "nat \ int \ int" - where - Z : "bintrunc 0 bin = 0" - | Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" +abbreviation (input) bintrunc :: "nat \ int \ int" + where \bintrunc \ take_bit\ primrec sbintrunc :: "nat \ int \ int" where Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)" | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" -lemma bintrunc_eq_take_bit: - \bintrunc = take_bit\ -proof (rule ext)+ - fix n and k - show \bintrunc n k = take_bit n k\ - by (induction n arbitrary: k) (simp_all add: take_bit_Suc Bit_def mod_2_eq_odd) -qed - lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n" - by (simp add: bintrunc_eq_take_bit take_bit_eq_mod) + by (fact take_bit_eq_mod) lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n" proof (induction n arbitrary: w) @@ -470,7 +460,7 @@ "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT True" "bintrunc (Suc n) (- numeral (Num.Bit0 w)) = bintrunc n (- numeral w) BIT False" "bintrunc (Suc n) (- numeral (Num.Bit1 w)) = bintrunc n (- numeral (w + Num.One)) BIT True" - by simp_all + by (simp_all add: take_bit_Suc Bit_def) lemma sbintrunc_0_numeral [simp]: "sbintrunc 0 1 = -1" @@ -494,10 +484,7 @@ done lemma nth_bintr: "bin_nth (bintrunc m w) n \ n < m \ bin_nth w n" - apply (induct n arbitrary: w m) - apply (case_tac m, auto)[1] - apply (case_tac m, auto)[1] - done + by (simp add: bin_nth_iff bit_take_bit_iff) lemma nth_sbintr: "bin_nth (sbintrunc m w) n = (if n < m then bin_nth w n else bin_nth w m)" apply (induct n arbitrary: w m) @@ -521,7 +508,7 @@ using bin_nth_Bit [where w="numeral w" and b="True"] by simp lemma bintrunc_bintrunc_l: "n \ m \ bintrunc m (bintrunc n w) = bintrunc n w" - by (rule bin_eqI) (auto simp: nth_bintr) + by (simp add: min.absorb2) lemma sbintrunc_sbintrunc_l: "n \ m \ sbintrunc m (sbintrunc n w) = sbintrunc n w" by (rule bin_eqI) (auto simp: nth_sbintr) @@ -535,18 +522,6 @@ lemma sbintrunc_sbintrunc_min [simp]: "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w" by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2) -lemmas bintrunc_Pls = - bintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps] - -lemmas bintrunc_Min [simp] = - bintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps] - -lemmas bintrunc_BIT [simp] = - bintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b - -lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT - bintrunc_Suc_numeral - lemmas sbintrunc_Suc_Pls = sbintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps] @@ -576,7 +551,6 @@ lemmas sbintrunc_0_simps = sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1 -lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs lemma bintrunc_minus: "0 < n \ bintrunc (Suc (n - 1)) w = bintrunc n w" @@ -585,28 +559,11 @@ lemma sbintrunc_minus: "0 < n \ sbintrunc (Suc (n - 1)) w = sbintrunc n w" by auto -lemmas bintrunc_minus_simps = - bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]] lemmas sbintrunc_minus_simps = sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] lemmas thobini1 = arg_cong [where f = "\w. w BIT b"] for b -lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] -lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] - -lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]] -lemmas bintrunc_Pls_minus_I = bmsts(1) -lemmas bintrunc_Min_minus_I = bmsts(2) -lemmas bintrunc_BIT_minus_I = bmsts(3) - -lemma bintrunc_Suc_lem: "bintrunc (Suc n) x = y \ m = Suc n \ bintrunc m x = y" - by auto - -lemmas bintrunc_Suc_Ialts = - bintrunc_Min_I [THEN bintrunc_Suc_lem] - bintrunc_BIT_I [THEN bintrunc_Suc_lem] - lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] lemmas sbintrunc_Suc_Is = @@ -635,10 +592,10 @@ lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] lemma bintrunc_sbintrunc' [simp]: "0 < n \ bintrunc n (sbintrunc (n - 1) w) = bintrunc n w" - by (cases n) (auto simp del: bintrunc.Suc) + by (cases n) simp_all lemma sbintrunc_bintrunc' [simp]: "0 < n \ sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w" - by (cases n) (auto simp del: bintrunc.Suc) + by (cases n) simp_all lemma bin_sbin_eq_iff: "bintrunc (Suc n) x = bintrunc (Suc n) y \ sbintrunc n x = sbintrunc n y" apply (rule iffI) @@ -650,7 +607,7 @@ lemma bin_sbin_eq_iff': "0 < n \ bintrunc n x = bintrunc n y \ sbintrunc (n - 1) x = sbintrunc (n - 1) y" - by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc) + by (cases n) (simp_all add: bin_sbin_eq_iff) lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def] lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def] @@ -667,7 +624,7 @@ lemma bintrunc_numeral: "bintrunc (numeral k) x = bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x" - by (simp add: numeral_eq_Suc) + by (simp add: numeral_eq_Suc take_bit_Suc Bit_def mod_2_eq_odd) lemma sbintrunc_numeral: "sbintrunc (numeral k) x = sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x" @@ -762,24 +719,20 @@ by (simp add: bin_sign_def) lemma bin_rest_trunc: "bin_rest (bintrunc n bin) = bintrunc (n - 1) (bin_rest bin)" - by (induct n arbitrary: bin) auto + by (simp add: take_bit_rec [of n bin]) lemma bin_rest_power_trunc: "(bin_rest ^^ k) (bintrunc n bin) = bintrunc (n - k) ((bin_rest ^^ k) bin)" by (induct k) (auto simp: bin_rest_trunc) lemma bin_rest_trunc_i: "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)" - by auto + by (auto simp add: take_bit_Suc) lemma bin_rest_strunc: "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)" by (induct n arbitrary: bin) auto lemma bintrunc_rest [simp]: "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)" - apply (induct n arbitrary: bin) - apply simp - apply (case_tac bin rule: bin_exhaust) - apply (auto simp: bintrunc_bintrunc_l) - done + by (induct n arbitrary: bin) (simp_all add: take_bit_Suc) lemma sbintrunc_rest [simp]: "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)" apply (induct n arbitrary: bin) @@ -894,7 +847,7 @@ by (auto simp add: bin_nth_drop_bit_iff bin_nth_take_bit_iff) lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w" - by (simp add: bin_cat_eq_push_bit_add_take_bit bintrunc_eq_take_bit) + by (simp add: bin_cat_eq_push_bit_add_take_bit) lemma bintr_cat1: "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b" by (metis bin_cat_assoc bin_cat_zero) @@ -907,10 +860,10 @@ by (auto simp add : bintr_cat) lemma cat_bintr [simp]: "bin_cat a n (bintrunc n b) = bin_cat a n b" - by (induct n arbitrary: b) auto + by (simp add: bin_cat_eq_push_bit_add_take_bit) lemma split_bintrunc: "bin_split n c = (a, b) \ b = bintrunc n c" - by (simp add: bintrunc_eq_take_bit) + by simp lemma bin_cat_split: "bin_split n w = (u, v) \ w = bin_cat u n v" by (auto simp add: bin_cat_eq_push_bit_add_take_bit bits_ident) @@ -926,14 +879,14 @@ (simp_all add: Bit_def take_bit_Suc mod_2_eq_odd) lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)" - by (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq bintrunc_eq_take_bit) + by (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq) lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)" by simp lemma bin_split_minus1 [simp]: "bin_split n (- 1) = (- 1, bintrunc n (- 1))" - by (simp add: bintrunc_eq_take_bit) + by simp lemma bin_split_trunc: "bin_split (min m n) c = (a, b) \ @@ -954,10 +907,7 @@ done lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b" - apply (induct n arbitrary: b) - apply clarsimp - apply (simp add: Bit_def) - done + by (simp add: bin_cat_eq_push_bit_add_take_bit push_bit_eq_mult) lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)" by (simp add: drop_bit_eq_div take_bit_eq_mod) @@ -1032,7 +982,7 @@ apply (drule bthrs) apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) apply clarify - apply (simp add: bintrunc_eq_take_bit) + apply simp done lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl @@ -1061,7 +1011,7 @@ done lemma bin_rsplit_all: "0 < nw \ nw \ n \ bin_rsplit n (nw, w) = [bintrunc n w]" - by (auto simp: bin_rsplit_def rsplit_aux_simp2ls bintrunc_eq_take_bit split: prod.split dest!: split_bintrunc) + by (auto simp: bin_rsplit_def rsplit_aux_simp2ls split: prod.split dest!: split_bintrunc) lemma bin_rsplit_l [rule_format]: "\bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)" @@ -1071,7 +1021,7 @@ apply (subst bin_rsplitl_aux.simps) apply (subst bin_rsplit_aux.simps) apply (clarsimp simp: Let_def split: prod.split) - apply (simp add: bintrunc_eq_take_bit ac_simps) + apply (simp add: ac_simps) apply (subst rsplit_aux_alts(1)) apply (subst rsplit_aux_alts(2)) apply clarsimp @@ -1088,7 +1038,7 @@ apply clarsimp apply clarsimp apply (subst rsplit_aux_alts) - apply (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq bintrunc_eq_take_bit) + apply (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq) done lemma bin_rsplit_aux_len_le [rule_format] : @@ -1203,7 +1153,7 @@ lemma bin_sc_bintr [simp]: "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)" apply (induct n arbitrary: w m) apply (case_tac [!] w rule: bin_exhaust) - apply (case_tac [!] m, auto) + apply (case_tac [!] m, auto simp add: take_bit_Suc mod_2_eq_odd) done lemma bin_clr_le: "bin_sc n False w \ w" @@ -1223,7 +1173,7 @@ apply simp apply (case_tac w rule: bin_exhaust) apply (case_tac m) - apply (auto simp: le_Bits) + apply (auto simp: le_Bits take_bit_Suc mod_2_eq_odd) done lemma bintr_bin_set_ge: "bintrunc n (bin_sc m True w) \ bintrunc n w" @@ -1231,7 +1181,7 @@ apply simp apply (case_tac w rule: bin_exhaust) apply (case_tac m) - apply (auto simp: le_Bits) + apply (auto simp: le_Bits take_bit_Suc mod_2_eq_odd) done lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0" @@ -2218,7 +2168,7 @@ subsection \Semantic interpretation of \<^typ>\bool list\ as \<^typ>\int\\ lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)" - by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def) + by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc Bit_def ac_simps mod_2_eq_odd) lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w" by (auto simp: bin_to_bl_def bin_bl_bin') @@ -2239,7 +2189,7 @@ apply (clarsimp simp: bin_to_bl_zero_aux) apply (erule thin_rl) apply (induct_tac n) - apply auto + apply (auto simp add: take_bit_Suc) done lemma bin_to_bl_bintr: @@ -2380,7 +2330,7 @@ next case (Suc n) then have "m - Suc (length bl) = n" by simp - with Cons Suc show ?thesis by simp + with Cons Suc show ?thesis by (simp add: take_bit_Suc Bit_def ac_simps) qed qed diff -r 4d4079159be7 -r 476b9e6904d9 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Jun 18 09:07:29 2020 +0000 +++ b/src/HOL/Word/Word.thy Thu Jun 18 09:07:29 2020 +0000 @@ -1168,7 +1168,7 @@ by (simp add: scast_def) lemma uint_1 [simp]: "uint (1::'a::len word) = 1" - by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4)) + by (simp only: word_1_wi word_ubin.eq_norm) simp lemma unat_1 [simp]: "unat (1::'a::len word) = 1" by (simp add: unat_def) @@ -2646,10 +2646,8 @@ lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)" unfolding shiftl1_def - apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm) - apply (subst refl [THEN bintrunc_BIT_I, symmetric]) - apply (subst bintrunc_bintrunc_min) - apply simp + apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm Bit_def) + apply (simp add: mod_mult_right_eq take_bit_eq_mod) done lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)" @@ -3531,7 +3529,7 @@ apply safe defer apply (clarsimp split: prod.splits) - apply (metis bintrunc_eq_take_bit of_bl_drop' ucast_bl ucast_def word_size word_size_bl word_ubin.Abs_norm) + apply (metis of_bl_drop' ucast_bl ucast_def word_size word_size_bl) apply hypsubst_thin apply (drule word_ubin.norm_Rep [THEN ssubst]) apply (simp add: of_bl_def bl2bin_drop word_size @@ -3544,8 +3542,7 @@ apply (simp add : of_bl_def to_bl_def) apply (subst bin_to_bl_drop_bit [symmetric]) apply (subst diff_add) - apply (simp_all add: bintrunc_eq_take_bit take_bit_drop_bit) - apply (simp add: take_bit_eq_mod) + apply (simp_all add: take_bit_drop_bit) done lemma word_split_bl: "std = size c - size b \ @@ -4566,7 +4563,7 @@ by simp next case (Suc i) - then show ?case by (cases n) simp_all + then show ?case by (cases n) (simp_all add: take_bit_Suc Bit_def) qed lemma shiftl_transfer [transfer_rule]: