# HG changeset patch # User wenzelm # Date 1393714135 -3600 # Node ID eebefb9a2b0185edee29620f257730e2411454a2 # Parent e21d83c8e1c74719dc6799d10b275612c9f7a5b8# Parent b7bdea5336dd68ca83b7a3235fe6bb533627f0da merged diff -r b7bdea5336dd -r eebefb9a2b01 NEWS --- a/NEWS Sat Mar 01 23:17:37 2014 +0100 +++ b/NEWS Sat Mar 01 23:48:55 2014 +0100 @@ -91,6 +91,13 @@ *** HOL *** +* HOL-Word: + * Abandoned fact collection "word_arith_alts", which is a + duplicate of "word_arith_wis". + * Dropped first (duplicated) element in fact collections + "sint_word_ariths", "word_arith_alts", "uint_word_ariths", + "uint_word_arith_bintrs". + * Code generator: explicit proof contexts in many ML interfaces. INCOMPATIBILITY. diff -r b7bdea5336dd -r eebefb9a2b01 src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Sat Mar 01 23:17:37 2014 +0100 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Sat Mar 01 23:48:55 2014 +0100 @@ -5,7 +5,7 @@ *) theory RMD -imports Word +imports "~~/src/HOL/Word/Word" begin diff -r b7bdea5336dd -r eebefb9a2b01 src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Sat Mar 01 23:17:37 2014 +0100 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Sat Mar 01 23:48:55 2014 +0100 @@ -5,7 +5,7 @@ *) theory RMD_Specification -imports RMD SPARK +imports RMD "~~/src/HOL/SPARK/SPARK" begin (* bit operations *) diff -r b7bdea5336dd -r eebefb9a2b01 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy --- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Mar 01 23:17:37 2014 +0100 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Mar 01 23:48:55 2014 +0100 @@ -456,7 +456,7 @@ unfolding round_def unfolding steps_to_steps' unfolding H1[symmetric] - by (simp add: uint_word_ariths(2) rdmods + by (simp add: uint_word_ariths(1) rdmods uint_word_of_int_id) qed diff -r b7bdea5336dd -r eebefb9a2b01 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Sat Mar 01 23:17:37 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Sat Mar 01 23:48:55 2014 +0100 @@ -47,7 +47,7 @@ end; fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs - absT_infos lthy = + (absT_infos : absT_info list) lthy = let fun of_fp_res get = map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars; @@ -122,13 +122,10 @@ val xTs = map (domain_type o fastype_of) xtors; val yTs = map (domain_type o fastype_of) xtor's; - fun abs_of allAs Ds bnf = mk_abs (mk_T_of_bnf Ds allAs bnf) o #abs; - fun rep_of absAT = mk_rep absAT o #rep; - - val absAs = map3 (abs_of allAs) Dss bnfs absT_infos; - val absBs = map3 (abs_of allBs) Dss bnfs absT_infos; - val fp_repAs = map2 rep_of absATs fp_absT_infos; - val fp_repBs = map2 rep_of absBTs fp_absT_infos; + val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss; + val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss; + val fp_repAs = map2 mk_rep absATs fp_reps; + val fp_repBs = map2 mk_rep absBTs fp_reps; val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy |> mk_Frees' "R" phiTs diff -r b7bdea5336dd -r eebefb9a2b01 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Sat Mar 01 23:17:37 2014 +0100 +++ b/src/HOL/Word/Word.thy Sat Mar 01 23:48:55 2014 +0100 @@ -1192,7 +1192,7 @@ subsection {* Word Arithmetic *} lemma word_less_alt: "(a < b) = (uint a < uint b)" - unfolding word_less_def word_le_def by (simp add: less_le) + by (fact word_less_def) lemma signed_linorder: "class.linorder word_sle word_sless" by default (unfold word_sle_def word_sless_def, auto) @@ -1236,16 +1236,20 @@ unfolding uint_bl 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) - -lemma unat_0_iff: "(unat x = 0) = (x = 0)" +lemma uint_0_iff: + "uint x = 0 \ x = 0" + by (simp add: word_uint_eq_iff) + +lemma unat_0_iff: + "unat x = 0 \ x = 0" unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff) -lemma unat_0 [simp]: "unat 0 = 0" +lemma unat_0 [simp]: + "unat 0 = 0" unfolding unat_def by auto -lemma size_0_same': "size w = 0 \ w = (v :: 'a :: len0 word)" +lemma size_0_same': + "size w = 0 \ w = (v :: 'a :: len0 word)" apply (unfold word_size) apply (rule box_equals) defer @@ -1278,8 +1282,7 @@ unfolding scast_def by simp lemma uint_1 [simp]: "uint (1::'a::len word) = 1" - unfolding word_1_wi - by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1) + by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4)) lemma unat_1 [simp]: "unat (1::'a::len word) = 1" unfolding unat_def by simp @@ -1289,10 +1292,6 @@ (* now, to get the weaker results analogous to word_div/mod_def *) -lemmas word_arith_alts = - word_sub_wi - word_arith_wis (* FIXME: duplicate *) - subsection {* Transferring goals from words to ints *} @@ -1308,16 +1307,44 @@ lemma uint_cong: "x = y \ uint x = uint y" by simp -lemmas uint_word_ariths = - word_arith_alts [THEN trans [OF uint_cong int_word_uint]] - -lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p] - -(* similar expressions for sint (arith operations) *) -lemmas sint_word_ariths = uint_word_arith_bintrs - [THEN uint_sint [symmetric, THEN trans], - unfolded uint_sint bintr_arith1s bintr_ariths - len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep] +lemma uint_word_ariths: + fixes a b :: "'a::len0 word" + shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)" + and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)" + and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)" + and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)" + and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)" + and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)" + and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)" + and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)" + by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]]) + +lemma uint_word_arith_bintrs: + fixes a b :: "'a::len0 word" + shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)" + and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)" + and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)" + and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)" + and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)" + and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)" + and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0" + and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1" + by (simp_all add: uint_word_ariths bintrunc_mod2p) + +lemma sint_word_ariths: + fixes a b :: "'a::len word" + shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)" + and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)" + and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)" + and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)" + and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)" + and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)" + and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0" + and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1" + by (simp_all add: uint_word_arith_bintrs + [THEN uint_sint [symmetric, THEN trans], + unfolded uint_sint bintr_arith1s bintr_ariths + len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]) lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]] lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]] @@ -1417,7 +1444,7 @@ with `1 \ uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1" by auto then show ?thesis - by (simp only: unat_def int_word_uint word_arith_alts mod_diff_right_eq [symmetric]) + by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric]) qed lemma measure_unat: "p ~= 0 \ unat (p - 1) < unat p" @@ -3930,7 +3957,7 @@ apply (clarsimp simp: word_size)+ apply (rule trans) apply (rule test_bit_rcat [OF refl refl]) - apply (simp add: word_size msrevs) + apply (simp add: word_size) apply (subst nth_rev) apply arith apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less]) @@ -4480,7 +4507,7 @@ uint x + uint y else uint x + uint y - 2^size x)" - by (simp add: word_arith_alts int_word_uint mod_add_if_z + by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size) lemma unat_plus_if_size: @@ -4501,16 +4528,7 @@ lemma max_lt: "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)" - apply (subst word_arith_nat_defs) - apply (subst word_unat.eq_norm) - apply (subst mod_if) - apply clarsimp - apply (erule notE) - apply (insert div_le_dividend [of "unat (max a b)" "unat c"]) - apply (erule order_le_less_trans) - apply (insert unat_lt2p [of "max a b"]) - apply simp - done + by (fact unat_div) lemma uint_sub_if_size: "uint (x - y) = @@ -4518,7 +4536,7 @@ uint x - uint y else uint x - uint y + 2^size x)" - by (simp add: word_arith_alts int_word_uint mod_sub_if_z + by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size) lemma unat_sub: @@ -4725,5 +4743,3 @@ end - -