adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Isabelle2016-1: update Word_Lib 

Word_Lib now looks more like the current AFP entry, though there are
still some local modifications.
This commit is contained in:
Matthew Brecknell 2016-10-14 12:05:41 +11:00
parent 5b11be92e8
commit 1a590fbbb2
5 changed files with 49 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Word_Lib/Aligned.thy
View File

@ -296,7 +296,7 @@ proof cases
have "(2::nat) ^ m dvd unat (k << m)"
proof
have kv: "(unat k div 2 ^ q) * 2 ^ q + unat k mod 2 ^ q = unat k"
by (rule mod_div_equality)
by (rule div_mult_mod_eq)
have "unat (k << m) = unat (2 ^ m * k)" by (simp add: shiftl_t2n)
also have "\<dots> = (2 ^ m * unat k) mod (2 ^ len_of TYPE('a))" using mv

6
lib/Word_Lib/HOL_Lemmas.thy
View File

@ -42,11 +42,11 @@ lemma strict_part_mono_reverseE:
lemma takeWhile_take_has_property:
"n \<le> length (takeWhile P xs) \<Longrightarrow> \<forall>x \<in> set (take n xs). P x"
by (induct xs arbitrary: n; simp split: split_if_asm) (case_tac n, simp_all)
by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all)
lemma takeWhile_take_has_property_nth:
"\<lbrakk> n < length (takeWhile P xs) \<rbrakk> \<Longrightarrow> P (xs ! n)"
by (induct xs arbitrary: n; simp split: split_if_asm) (case_tac n, simp_all)
by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all)
lemma takeWhile_replicate:
"takeWhile f (replicate len x) = (if f x then replicate len x else [])"
@ -78,7 +78,7 @@ next
have "a ^ n * (a ^ m div a ^ n) = a ^ m"
proof (subst mult.commute)
have "a ^ m = (a ^ m div a ^ n) * a ^ n + a ^ m mod a ^ n"
by (rule mod_div_equality [symmetric])
by (rule div_mult_mod_eq [symmetric])
moreover have "a ^ m mod a ^ n = 0"
by (subst mod_eq_0_iff, rule exI [where x = "a ^ q"],

2
lib/Word_Lib/More_Divides.thy
View File

@ -23,7 +23,7 @@ lemma div_mult_le:
lemma diff_mod_le:
"\<lbrakk> (a::nat) < d; b dvd d \<rbrakk> \<Longrightarrow> a - a mod b \<le> d - b"
apply(subst mult_div_cancel [symmetric])
apply(subst minus_mod_eq_mult_div)
apply(clarsimp simp: dvd_def)
apply(case_tac "b = 0")
apply simp

99
lib/Word_Lib/Word_Lemmas.thy
View File

@ -11,7 +11,8 @@
section "Lemmas with Generic Word Length"
theory Word_Lemmas
imports
imports
Complex_Main
Aligned
Word_Enum
begin
@ -150,7 +151,7 @@ lemma no_plus_overflow_neg:
"(x :: 'a :: len word) < -y \<Longrightarrow> x \<le> x + y"
apply (simp add: no_plus_overflow_uint_size word_less_alt uint_word_ariths word_size)
apply (subst(asm) zmod_zminus1_eq_if)
apply (simp split: split_if_asm)
apply (simp split: if_split_asm)
done
lemma ucast_ucast_eq:
@ -593,7 +594,7 @@ qed
lemma upto_enum_len_less:
"\<lbrakk> n \<le> length [a, b .e. c]; n \<noteq> 0 \<rbrakk> \<Longrightarrow> a \<le> c"
unfolding upto_enum_step_def
by (simp split: split_if_asm)
by (simp split: if_split_asm)
lemma length_upto_enum_step:
fixes x :: "'a :: len word"
@ -1077,7 +1078,6 @@ lemma unat_less_power:
shows "unat k < 2 ^ sz"
using szv unat_mono [OF kv] by simp
(* This should replace some crud \<dots> search for unat_of_nat *)
lemma unat_mult_power_lem:
assumes kv: "k < 2 ^ (len_of TYPE('a::len) - sz)"
shows "unat (2 ^ sz * of_nat k :: (('a::len) word)) = 2 ^ sz * k"
@ -1478,7 +1478,7 @@ lemma power_le_mono:
lemma sublist_equal_part:
"xs \<le> ys \<Longrightarrow> take (length xs) ys = xs"
by (clarsimp simp: prefixeq_def less_eq_list_def)
by (clarsimp simp: prefix_def less_eq_list_def)
lemma two_power_eq:
"\<lbrakk>n < len_of TYPE('a); m < len_of TYPE('a)\<rbrakk>
@ -1488,20 +1488,15 @@ lemma two_power_eq:
apply (simp add: power_le_mono[where 'a='a])+
done
lemma less_list_def': "(xs < ys) = (prefix xs ys)"
apply (metis prefix_order.eq_iff prefix_def less_list_def less_eq_list_def)
done
lemma prefix_length_less:
"xs < ys \<Longrightarrow> length xs < length ys"
apply (clarsimp simp: less_list_def' prefix_def)
apply (frule prefixeq_length_le)
apply (clarsimp simp: less_list_def' strict_prefix_def less_eq_list_def[symmetric])
apply (frule prefix_length_le)
apply (rule ccontr, simp)
apply (clarsimp simp: prefixeq_def)
apply (clarsimp simp: less_eq_list_def prefix_def)
done
lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def']
lemmas take_strict_prefix = take_prefix [folded less_list_def']
lemmas take_less = take_strict_prefix [folded less_list_def']
lemma not_prefix_longer:
"\<lbrakk> length xs > length ys \<rbrakk> \<Longrightarrow> \<not> xs \<le> ys"
@ -1592,7 +1587,7 @@ lemma of_nat_inj:
lemma map_prefixI:
"xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
by (clarsimp simp: less_eq_list_def prefixeq_def)
by (clarsimp simp: less_eq_list_def prefix_def)
lemma if_Some_None_eq_None:
"((if P then Some v else None) = None) = (\<not> P)"
@ -1637,14 +1632,14 @@ lemma list_all2_induct_suffixeq [consumes 1, case_names Nil Cons]:
assumes lall: "list_all2 Q as bs"
and nilr: "P [] []"
and consr: "\<And>x xs y ys.
\<lbrakk>list_all2 Q xs ys; Q x y; P xs ys; suffixeq (x # xs) as; suffixeq (y # ys) bs\<rbrakk>
\<lbrakk>list_all2 Q xs ys; Q x y; P xs ys; suffix (x # xs) as; suffix (y # ys) bs\<rbrakk>
\<Longrightarrow> P (x # xs) (y # ys)"
shows "P as bs"
proof -
def as' == as
def bs' == bs
define as' where "as' == as"
define bs' where "bs' == bs"
have "suffixeq as as' \<and> suffixeq bs bs'" unfolding as'_def bs'_def by simp
have "suffix as as' \<and> suffix bs bs'" unfolding as'_def bs'_def by simp
then show ?thesis using lall
proof (induct rule: list_induct2 [OF list_all2_lengthD [OF lall]])
case 1 show ?case by fact
@ -1654,9 +1649,9 @@ proof -
show ?case
proof (rule consr)
from "2.prems" show "list_all2 Q xs ys" and "Q x y" by simp_all
then show "P xs ys" using "2.hyps" "2.prems" by (auto dest: suffixeq_ConsD)
from "2.prems" show "suffixeq (x # xs) as" and "suffixeq (y # ys) bs"
by (auto simp: as'_def bs'_def)
then show "P xs ys" using "2.hyps" "2.prems" by (auto dest: suffix_ConsD)
from "2.prems" show "suffix (x # xs) as" and "suffix (y # ys) bs"
by (auto simp: as'_def bs'_def)
qed
qed
qed
@ -1838,7 +1833,7 @@ lemma nth_bounded:
simplified add_0_left, rotated])
apply assumption+
apply (simp only: to_bl_0)
apply (simp add: nth_append split: split_if_asm)
apply (simp add: nth_append split: if_split_asm)
done
lemma is_aligned_add_or:
@ -1906,7 +1901,7 @@ qed
lemma take_is_prefix:
"take n xs \<le> xs"
apply (simp add: less_eq_list_def prefixeq_def)
apply (simp add: less_eq_list_def prefix_def)
apply (rule_tac x="drop n xs" in exI)
apply simp
done
@ -2136,7 +2131,7 @@ lemma word_and_1_shiftl:
fixes x :: "'a :: len word" shows
"x && (1 << n) = (if x !! n then (1 << n) else 0)"
apply (rule word_eqI)
apply (simp add: word_size nth_shiftl split: split_if del: shiftl_1)
apply (simp add: word_size nth_shiftl del: shiftl_1)
apply auto
done
@ -2301,7 +2296,7 @@ proof -
have "unat a div 2 ^ n * 2 ^ n \<noteq> unat a"
proof -
have "unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n"
by (simp add: mod_div_equality)
by (simp add: div_mult_mod_eq)
also have "\<dots> \<noteq> unat a div 2 ^ n * 2 ^ n" using sz anz
by (simp add: unat_arith_simps)
finally show ?thesis ..
@ -2481,7 +2476,7 @@ lemma int_div_sub_1:
apply (subgoal_tac "m = 0 \<or> (n - (1 :: int)) div m = (if m dvd n then (n div m) - 1 else n div m)")
apply fastforce
apply (subst mult_cancel_right[symmetric])
apply (simp only: left_diff_distrib split: split_if)
apply (simp only: left_diff_distrib split: if_split)
apply (simp only: mod_div_equality_div_eq)
apply (clarsimp simp: field_simps)
apply (clarsimp simp: dvd_eq_mod_eq_0)
@ -2682,7 +2677,7 @@ lemma bang_conj_lt:
lemma dom_if:
"dom (\<lambda>a. if a \<in> addrs then Some (f a) else g a) = addrs \<union> dom g"
by (auto simp: dom_def split: split_if)
by (auto simp: dom_def split: if_split)
lemma less_is_non_zero_p1:
fixes a :: "'a :: len word"
@ -3085,10 +3080,7 @@ lemma signed_arith_eq_checks_to_ord:
= ((0 <=s a - b) = (b <=s a))"
"(- sint a = sint (- a)) = (0 <=s (- a) = (a <=s 0))"
using sint_range'[where x=a] sint_range'[where x=b]
apply (simp_all add: sint_word_ariths
word_sle_def word_sless_alt sbintrunc_If)
apply arith+
done
by (simp_all add: sint_word_ariths word_sle_def word_sless_alt sbintrunc_If)
(* Basic proofs that signed word div/mod operations are
* truncations of their integer counterparts. *)
@ -3191,11 +3183,11 @@ lemma sgn_div_eq_sgn_mult:
lemma sgn_sdiv_eq_sgn_mult:
"a sdiv b \<noteq> 0 \<Longrightarrow> sgn ((a :: int) sdiv b) = sgn (a * b)"
apply (clarsimp simp: sdiv_int_def sgn_times)
apply (clarsimp simp: sdiv_int_def sgn_mult)
apply (subst sgn_div_eq_sgn_mult)
apply simp
apply (clarsimp simp: sgn_times)
apply (metis abs_mult div_0 div_mult_self2_is_id sgn_0_0 sgn_1_pos sgn_times zero_less_abs_iff)
apply (clarsimp simp: sgn_mult)
apply (metis abs_mult div_0 nonzero_mult_div_cancel_right sgn_0_0 sgn_1_pos sgn_mult zero_less_abs_iff)
done
lemma int_sdiv_same_is_1 [simp]:
@ -3211,10 +3203,10 @@ lemma int_sdiv_same_is_1 [simp]:
apply (case_tac "b = 0")
apply (clarsimp simp: sign_simps)
apply (rule classical)
apply (clarsimp simp: sign_simps sgn_times not_less)
apply (clarsimp simp: sign_simps sgn_mult not_less)
apply (metis le_less neg_0_less_iff_less not_less_iff_gr_or_eq pos_imp_zdiv_neg_iff)
apply (rule classical)
apply (clarsimp simp: sign_simps sgn_times not_less sgn_if split: if_splits)
apply (clarsimp simp: sign_simps sgn_mult not_less sgn_if split: if_splits)
apply (metis antisym less_le neg_imp_zdiv_nonneg_iff)
apply (clarsimp simp: sdiv_int_def sgn_if)
done
@ -3231,11 +3223,11 @@ lemma int_sdiv_negated_is_minus1 [simp]:
apply (clarsimp simp: sign_simps not_less)
apply (rule classical)
apply (case_tac "b = 0")
apply (clarsimp simp: sign_simps not_less sgn_times)
apply (clarsimp simp: sign_simps not_less sgn_mult)
apply (case_tac "a > 0")
apply (clarsimp simp: sign_simps not_less sgn_times)
apply (clarsimp simp: sign_simps not_less sgn_mult)
apply (metis less_le neg_less_0_iff_less not_less_iff_gr_or_eq pos_imp_zdiv_neg_iff)
apply (clarsimp simp: sign_simps not_less sgn_times)
apply (clarsimp simp: sign_simps not_less sgn_mult)
apply (metis Divides.transfer_nat_int_function_closures(1) eq_iff minus_zero neg_le_iff_le)
apply (clarsimp simp: sgn_if)
done
@ -3286,7 +3278,7 @@ lemma sdiv_word_min:
apply (cut_tac sint_range' [where x=b])
apply clarsimp
apply (insert sdiv_int_range [where a="sint a" and b="sint b"])
apply (clarsimp simp: max_def abs_if split: split_if_asm)
apply (clarsimp simp: max_def abs_if split: if_split_asm)
done
lemma sdiv_word_max:
@ -3321,7 +3313,7 @@ proof (rule classical)
apply (clarsimp simp: word_size)
apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1]
apply (insert word_sint.Rep [where x="a"])[1]
apply (clarsimp simp: minus_le_iff word_size abs_if sints_num split: split_if_asm)
apply (clarsimp simp: minus_le_iff word_size abs_if sints_num split: if_split_asm)
apply (metis minus_minus sint_int_min word_sint.Rep_inject)
done
@ -3355,7 +3347,7 @@ lemmas word_sdiv_numerals = word_sdiv_numerals_lhs[where b="numeral y" for y]
lemma smod_int_alt_def:
"(a::int) smod b = sgn (a) * (abs a mod abs b)"
apply (clarsimp simp: smod_int_def sdiv_int_def)
apply (clarsimp simp: zmod_zdiv_equality' abs_sgn sgn_times sgn_if sign_simps)
apply (clarsimp simp: minus_div_mult_eq_mod [symmetric] abs_sgn sgn_mult sgn_if sign_simps)
done
lemma smod_int_range:
@ -3411,7 +3403,7 @@ lemma smod_word_max:
apply (clarsimp)
apply (insert word_sint.Rep [where x="b", simplified sints_num])[1]
apply (insert smod_int_range [where a="sint a" and b="sint b"])
apply (clarsimp simp: abs_if split: split_if_asm)
apply (clarsimp simp: abs_if split: if_split_asm)
done
lemma smod_word_min:
@ -3421,7 +3413,7 @@ lemma smod_word_min:
apply clarsimp
apply (insert word_sint.Rep [where x=b, simplified sints_num])[1]
apply (insert smod_int_range [where a="sint a" and b="sint b"])
apply (clarsimp simp: abs_if add1_zle_eq split: split_if_asm)
apply (clarsimp simp: abs_if add1_zle_eq split: if_split_asm)
done
lemma smod_word_alt_def:
@ -3642,7 +3634,7 @@ lemma nat_mult_power_less_eq:
mult_less_cancel2[where m="a * b ^ (n - m)" and k="b ^ m" and n=1]
apply (simp only: power_add[symmetric] nat_minus_add_max)
apply (simp only: power_add[symmetric] nat_minus_add_max ac_simps)
apply (simp add: max_def split: split_if_asm)
apply (simp add: max_def split: if_split_asm)
done
lemma signed_shift_guard_to_word:
@ -3820,7 +3812,7 @@ lemma to_bool_0 [simp]: "\<not>to_bool 0" by (simp add: to_bool_def)
lemma from_bool_eq_if:
"(from_bool Q = (if P then 1 else 0)) = (P = Q)"
by (simp add: case_bool_If from_bool_def split: split_if)
by (simp add: case_bool_If from_bool_def split: if_split)
lemma to_bool_eq_0:
"(\<not> to_bool x) = (x = 0)"
@ -4127,13 +4119,8 @@ lemma uint_2_id:
done
lemma bintrunc_id:
"\<lbrakk>of_nat n \<ge> m; m > 0\<rbrakk> \<Longrightarrow> bintrunc n m = m"
apply (subst bintrunc_mod2p)
apply (rule int_mod_eq')
apply simp+
apply (induct n arbitrary:m)
apply simp+
by force
"\<lbrakk>m \<le> of_nat n; 0 < m\<rbrakk> \<Longrightarrow> bintrunc n m = m"
by (simp add: bintrunc_mod2p le_less_trans int_mod_eq')
lemma shiftr1_unfold: "shiftr1 x = x >> 1"
by (metis One_nat_def comp_apply funpow.simps(1) funpow.simps(2) id_apply shiftr_def)
@ -4141,7 +4128,7 @@ lemma shiftr1_unfold: "shiftr1 x = x >> 1"
lemma shiftr1_is_div_2: "(x::('a::len) word) >> 1 = x div 2"
apply (case_tac "len_of TYPE('a) = 1")
apply simp
apply (subgoal_tac "x = 0 \<or> x = 1")
apply (subgoal_tac "x = 0 \<or> x = 1")
apply (erule disjE)
apply (clarsimp simp:word_div_def)+
apply (metis One_nat_def less_irrefl_nat sint_1_cases)
@ -4446,7 +4433,7 @@ lemma card_enum_upto:
lemma unat_mask:
"unat (mask n :: 'a :: len word) = 2 ^ (min n (len_of TYPE('a))) - 1"
apply (subst min.commute)
apply (simp add: mask_def not_less min_def split: split_if_asm)
apply (simp add: mask_def not_less min_def split: if_split_asm)
apply (intro conjI impI)
apply (simp add: unat_sub_if_size)
apply (simp add: power_overflow word_size)

2
lib/Word_Lib/Word_Lemmas_64.thy
View File

@ -251,7 +251,7 @@ lemma mask_step_down_64:
done
lemma unat_of_int_64:
"\<lbrakk>i \<ge> 0; i \<le>2 ^ 31\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword64)) = nat i"
"\<lbrakk>i \<ge> 0; i \<le> 2 ^ 63\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword64)) = nat i"
unfolding unat_def
apply (subst eq_nat_nat_iff, clarsimp+)
apply (simp add: word_of_int uint_word_of_int int_mod_eq')