lib: add generic lemmas from SELFOUR-584 updates
Mainly concerning word_ctz and enumeration_both.
This commit is contained in:
Rafal Kolanski
parent
a837d38012
commit
d4996217b3
|
|
@ -1088,6 +1088,8 @@ lemmas corres_split_noop_rhs
|
|||
lemmas corres_split_noop_rhs2
|
||||
= corres_split_nor[THEN corres_add_noop_lhs2]
|
||||
|
||||
lemmas corres_split_dc = corres_split[where r'=dc, simplified]
|
||||
|
||||
lemma isLeft_case_sum:
|
||||
"isLeft v \<Longrightarrow> (case v of Inl v' \<Rightarrow> f v' | Inr v' \<Rightarrow> g v') = f (theLeft v)"
|
||||
by (clarsimp simp: isLeft_def)
|
||||
|
|
@ -1111,6 +1113,34 @@ lemma corres_return_eq_same:
|
|||
apply (simp add: corres_underlying_def return_def)
|
||||
done
|
||||
|
||||
lemmas corres_discard_r =
|
||||
corres_symb_exec_r [where P'=P' and Q'="\<lambda>_. P'" for P', simplified]
|
||||
|
||||
lemmas corres_returnTT = corres_return[where P=\<top> and P'=\<top>, THEN iffD2]
|
||||
|
||||
lemma corres_assert_gen_asm:
|
||||
"\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk>
|
||||
\<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>_. F)) Q f (assert F >>= g)"
|
||||
by (simp add: corres_gen_asm)
|
||||
|
||||
lemma corres_assert_gen_asm2:
|
||||
"\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk>
|
||||
\<Longrightarrow> corres_underlying sr nf nf' r P (Q and (\<lambda>_. F)) f (assert F >>= g)"
|
||||
by (simp add: corres_gen_asm2)
|
||||
|
||||
lemma corres_add_guard:
|
||||
"\<lbrakk>\<And>s s'. \<lbrakk>Q s; Q' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> P s \<and> P' s';
|
||||
corres_underlying sr nf nf' r (Q and P) (Q' and P') f g\<rbrakk> \<Longrightarrow>
|
||||
corres_underlying sr nf nf' r Q Q' f g"
|
||||
by (auto simp: corres_underlying_def)
|
||||
|
||||
(* safer non-rewrite version of corres_gets *)
|
||||
lemma corres_gets_trivial:
|
||||
"\<lbrakk>\<And>s s'. (s,s') \<in> sr \<Longrightarrow> f s = f' s' \<rbrakk>
|
||||
\<Longrightarrow> corres_underlying sr nf nf' op = \<top> \<top> (gets f) (gets f')"
|
||||
unfolding corres_underlying_def gets_def get_def return_def bind_def
|
||||
by clarsimp
|
||||
|
||||
text {* Some setup of specialised methods. *}
|
||||
|
||||
lemma (in strengthen_implementation) wpfix_strengthen_corres_guard_imp:
|
||||
|
|
|
|||
|
|
@ -336,6 +336,9 @@ lemma fromIntegral_simp3[simp]: "fromIntegral = ucast"
|
|||
apply (simp add: unat_def)
|
||||
done
|
||||
|
||||
lemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \<Rightarrow> nat) = id"
|
||||
by (simp add: fromIntegral_def fromInteger_nat toInteger_nat)
|
||||
|
||||
definition
|
||||
infix_apply :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("_ `~_~` _" [81, 100, 80] 80) where
|
||||
infix_apply_def[simp]:
|
||||
|
|
|
|||
|
|
@ -471,4 +471,46 @@ lemma foldl_fun_or_alt:
|
|||
apply clarsimp
|
||||
by (simp add: foldl_map)
|
||||
|
||||
lemma length_takeWhile_less:
|
||||
"\<exists>x\<in>set xs. \<not> P x \<Longrightarrow> length (takeWhile P xs) < length xs"
|
||||
by (induct xs) (auto split: if_splits)
|
||||
|
||||
(* FIXME move to Word_Lib (note needs lemmas from Lib/LemmaBucket) *)
|
||||
lemma word_ctz_le:
|
||||
"word_ctz (w :: ('a::len word)) \<le> LENGTH('a)"
|
||||
apply (clarsimp simp: word_ctz_def)
|
||||
apply (rule nat_le_Suc_less_imp[where y="LENGTH('a) + 1" , simplified])
|
||||
apply (rule order_le_less_trans[OF List.length_takeWhile_le])
|
||||
apply simp
|
||||
done
|
||||
|
||||
(* FIXME move to Word_Lib (note needs lemmas from Lib/LemmaBucket) *)
|
||||
lemma word_ctz_less:
|
||||
"w \<noteq> 0 \<Longrightarrow> word_ctz (w :: ('a::len word)) < LENGTH('a)"
|
||||
apply (clarsimp simp: word_ctz_def eq_zero_set_bl)
|
||||
apply (rule order_less_le_trans[OF length_takeWhile_less])
|
||||
apply fastforce+
|
||||
done
|
||||
|
||||
lemma suc_le_pow_2:
|
||||
"1 < (n::nat) \<Longrightarrow> Suc n < 2 ^ n"
|
||||
by (induct n; clarsimp)
|
||||
(case_tac "n = 1"; clarsimp)
|
||||
|
||||
lemma word_ctz_not_minus_1:
|
||||
"1 < LENGTH('a) \<Longrightarrow> of_nat (word_ctz (w :: ('a :: len) word)) \<noteq> (- 1 :: ('a::len) word)"
|
||||
apply (cut_tac w=w in word_ctz_le)
|
||||
apply (subst word_unat.Rep_inject[symmetric])
|
||||
apply (subst unat_of_nat_eq)
|
||||
apply (erule order_le_less_trans, fastforce)
|
||||
apply (subst unat_minus_one_word)
|
||||
apply (rule less_imp_neq)
|
||||
apply (erule order_le_less_trans)
|
||||
apply (subst less_eq_Suc_le)
|
||||
apply (subst le_diff_conv2, fastforce)
|
||||
apply (clarsimp simp: le_diff_conv2 less_eq_Suc_le[symmetric] suc_le_pow_2)
|
||||
done
|
||||
|
||||
lemmas word_ctz_not_minus_1_32 = word_ctz_not_minus_1[where 'a=32, simplified]
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -800,11 +800,11 @@ lemma no_fail_returnOK [simp, wp]:
|
|||
|
||||
text {* Empty results implies non-failure *}
|
||||
|
||||
lemma empty_fail_modify [simp]:
|
||||
lemma empty_fail_modify [simp, wp]:
|
||||
"empty_fail (modify f)"
|
||||
by (simp add: empty_fail_def simpler_modify_def)
|
||||
|
||||
lemma empty_fail_gets [simp]:
|
||||
lemma empty_fail_gets [simp, wp]:
|
||||
"empty_fail (gets f)"
|
||||
by (simp add: empty_fail_def simpler_gets_def)
|
||||
|
||||
|
|
@ -826,7 +826,7 @@ lemma empty_fail_bind [simp]:
|
|||
apply (clarsimp simp: ex_in_conv [symmetric])
|
||||
done
|
||||
|
||||
lemma empty_fail_return [simp]:
|
||||
lemma empty_fail_return [simp, wp]:
|
||||
"empty_fail (return x)"
|
||||
by (simp add: empty_fail_def return_def)
|
||||
|
||||
|
|
|
|||
|
|
@ -196,6 +196,16 @@ lemma monadic_rewrite_symb_exec_r:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma monadic_rewrite_symb_exec_r':
|
||||
"\<lbrakk> \<And>s. \<lbrace>op = s\<rbrace> m \<lbrace>\<lambda>r. op = s\<rbrace>; no_fail P m;
|
||||
\<And>rv. monadic_rewrite F False (Q rv) x (y rv);
|
||||
\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk>
|
||||
\<Longrightarrow> monadic_rewrite F False P x (m >>= y)"
|
||||
apply (rule monadic_rewrite_imp)
|
||||
apply (rule monadic_rewrite_symb_exec_r; assumption)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma monadic_rewrite_symb_exec_l'':
|
||||
"\<lbrakk> \<And>s. \<lbrace>op = s\<rbrace> m \<lbrace>\<lambda>r. op = s\<rbrace>; empty_fail m;
|
||||
\<not> F \<longrightarrow> no_fail P' m;
|
||||
|
|
|
|||
|
|
@ -610,6 +610,46 @@ lemma upto_enum_set_conv2:
|
|||
shows "set [a .e. b] = {a .. b}"
|
||||
by auto
|
||||
|
||||
lemma fromEnum_upto_nth:
|
||||
fixes start :: "'a :: enumeration_both"
|
||||
assumes "n < length [start .e. end]"
|
||||
shows "fromEnum ([start .e. end] ! n) = fromEnum start + n"
|
||||
proof -
|
||||
have less_sub: "\<And>m k m' n. \<lbrakk> (n::nat) < m - k ; m \<le> m' \<rbrakk> \<Longrightarrow> n < m' - k" by fastforce
|
||||
note upt_Suc[simp del]
|
||||
show ?thesis using assms
|
||||
by (fastforce simp: upto_enum_red from_to_enum
|
||||
dest: less_sub[where m'="Suc (fromEnum maxBound)"] intro: maxBound_is_bound)
|
||||
qed
|
||||
|
||||
lemma length_upto_enum_le_maxBound:
|
||||
fixes start :: "'a :: enumeration_both"
|
||||
shows "length [start .e. end] \<le> Suc (fromEnum (maxBound :: 'a))"
|
||||
apply (clarsimp simp add: upto_enum_red split: if_splits)
|
||||
apply (rule le_imp_diff_le[OF maxBound_is_bound[of "end"]])
|
||||
done
|
||||
|
||||
lemma less_length_upto_enum_maxBoundD:
|
||||
fixes start :: "'a :: enumeration_both"
|
||||
assumes "n < length [start .e. end]"
|
||||
shows "n \<le> fromEnum (maxBound :: 'a)"
|
||||
using assms
|
||||
by (simp add: upto_enum_red less_Suc_eq_le
|
||||
le_trans[OF _ le_imp_diff_le[OF maxBound_is_bound[of "end"]]]
|
||||
split: if_splits)
|
||||
|
||||
lemma fromEnum_eq_iff:
|
||||
"(fromEnum e = fromEnum f) = (e = f)"
|
||||
proof -
|
||||
have a: "e \<in> set enum" by auto
|
||||
have b: "f \<in> set enum" by auto
|
||||
from nth_the_index[OF a] nth_the_index[OF b] show ?thesis unfolding fromEnum_def by metis
|
||||
qed
|
||||
|
||||
lemma maxBound_is_bound':
|
||||
"i = fromEnum (e::('a::enum)) \<Longrightarrow> i \<le> fromEnum (maxBound::('a::enum))"
|
||||
by (clarsimp simp: maxBound_is_bound)
|
||||
|
||||
lemma of_nat_unat [simp]:
|
||||
"of_nat \<circ> unat = id"
|
||||
by (rule ext, simp)
|
||||
|
|
@ -5590,4 +5630,14 @@ lemma sign_extend_eq:
|
|||
"w && mask (Suc n) = v && mask (Suc n) \<Longrightarrow> sign_extend n w = sign_extend n v"
|
||||
by (rule word_eqI, fastforce dest: word_eqD simp: sign_extend_bitwise_if' word_size)
|
||||
|
||||
lemma unat_minus_one_word:
|
||||
"unat (-1 :: 'a :: len word) = 2 ^ len_of TYPE('a) - 1"
|
||||
by (subst minus_one_word)
|
||||
(subst unat_sub_if', clarsimp)
|
||||
|
||||
lemma of_nat_eq_signed_scast:
|
||||
"(of_nat x = (y :: ('a::len) signed word))
|
||||
= (of_nat x = (scast y :: 'a word))"
|
||||
by (metis scast_of_nat scast_scast_id(2))
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue