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

lib: More trivial helpers from CAmkES.

This commit is contained in:
Matthew Fernandez 2015-08-12 13:54:56 +10:00
parent 5073d065ad
commit e5340b5cca
2 changed files with 34 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
lib/LemmaBucket.thy
View File

@ -298,6 +298,9 @@ lemma Least28: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4;
25; \<not>P 26; \<not>P 27; P (28::nat)\<rbrakk> \<Longrightarrow> Least P = 28"
by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3))
lemma map_add_discard: "\<not> cond x \<Longrightarrow> (f ++ (\<lambda>x. if cond x then (g x) else None)) x = f x"
by (simp add: map_add_def)
lemma dom_split:"\<lbrakk>\<forall>x \<in> S. \<exists>y. f x = Some y; \<forall>x. x \<notin> S \<longrightarrow> f x = None\<rbrakk> \<Longrightarrow> dom f = S"
by (auto simp:dom_def)

31
lib/WordLemmaBucket.thy
View File

@ -6564,4 +6564,35 @@ lemma card_map_elide2: "n \<le> CARD(32 word) \<Longrightarrow> card ((of_nat::n
apply (subst card_map_elide)
by clarsimp+
lemma le_max_word_ucast_id:
"(x::'a::len word) \<le> ucast (max_word::'b::len word) \<Longrightarrow> ucast ((ucast x)::'b word) = x"
apply (unfold ucast_def)
apply (subst word_ubin.eq_norm)
apply (subst and_mask_bintr[symmetric])
apply (subst and_mask_eq_iff_le_mask)
apply (clarsimp simp:max_word_def mask_def)
proof -
assume a1: "x \<le> word_of_int (uint (word_of_int (2 ^ len_of (TYPE('b)\<Colon>'b itself) - 1)\<Colon>'b word))"
have f2: "((\<exists>i ia. (0\<Colon>int) \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or> \<not> (0\<Colon>int) \<le> - 1 + 2 ^ len_of (TYPE('b)\<Colon>'b itself) \<or> (0\<Colon>int) \<le> - 1 + 2 ^ len_of (TYPE('b)\<Colon>'b itself) + - 1 * 2 ^ len_of (TYPE('b)\<Colon>'b itself) \<or> (- (1\<Colon>int) + 2 ^ len_of (TYPE('b)\<Colon>'b itself)) mod 2 ^ len_of (TYPE('b)\<Colon>'b itself) = - 1 + 2 ^ len_of (TYPE('b)\<Colon>'b itself)) = ((\<exists>i ia. (0\<Colon>int) \<le> i \<and> \<not> 0 \<le> i + - 1 * ia \<and> i mod ia \<noteq> i) \<or> \<not> (1\<Colon>int) \<le> 2 ^ len_of (TYPE('b)\<Colon>'b itself) \<or> 2 ^ len_of (TYPE('b)\<Colon>'b itself) + - (1\<Colon>int) * ((- 1 + 2 ^ len_of (TYPE('b)\<Colon>'b itself)) mod 2 ^ len_of (TYPE('b)\<Colon>'b itself)) = 1)"
by force
have f3: "\<forall>i ia. \<not> (0\<Colon>int) \<le> i \<or> 0 \<le> i + - 1 * ia \<or> i mod ia = i"
using mod_pos_pos_trivial by force
have "(1\<Colon>int) \<le> 2 ^ len_of (TYPE('b)\<Colon>'b itself)"
by simp
hence "2 ^ len_of (TYPE('b)\<Colon>'b itself) + - (1\<Colon>int) * ((- 1 + 2 ^ len_of (TYPE('b)\<Colon>'b itself)) mod 2 ^ len_of (TYPE('b)\<Colon>'b itself)) = 1"
using f3 f2 by blast
hence f4: "- (1\<Colon>int) + 2 ^ len_of (TYPE('b)\<Colon>'b itself) = (- 1 + 2 ^ len_of (TYPE('b)\<Colon>'b itself)) mod 2 ^ len_of (TYPE('b)\<Colon>'b itself)"
by linarith
have f5: "x \<le> word_of_int (uint (word_of_int (- 1 + 2 ^ len_of (TYPE('b)\<Colon>'b itself))\<Colon>'b word))"
using a1 by force
have f6: "2 ^ len_of (TYPE('b)\<Colon>'b itself) + - (1\<Colon>int) = - 1 + 2 ^ len_of (TYPE('b)\<Colon>'b itself)"
by force
have f7: "- (1\<Colon>int) * 1 = - 1"
by auto
have "\<forall>x0 x1. (x1\<Colon>int) - x0 = x1 + - 1 * x0"
by force
thus "x \<le> 2 ^ len_of (TYPE('b)\<Colon>'b itself) - 1"
using f7 f6 f5 f4 by (metis uint_word_of_int wi_homs(2) word_arith_wis(8) word_of_int_2p)
qed
end