Commit c08a92f5 authored by haftmann's avatar haftmann
Browse files

new lemmas

parent d552c27edab9
......@@ -1062,9 +1062,10 @@ proof (induct x' y' arbitrary: x y rule: power_p.induct[of _ p])
apply transfer apply transfer
apply (auto simp add: int_eq_iff nat_take_bit_eq nat_mod_distrib zmod_int)
apply (auto simp add: zmod_int mod_2_eq_odd)
apply (metis (full_types) even_take_bit_eq le_less_trans odd_iff_mod_2_eq_one take_bit_nonnegative zero_neq_numeral zmod_le_nonneg_dividend)
apply (auto simp add: less_le)
apply (simp add: le_less)
apply (auto simp add: le_less)
apply (metis linorder_neqE_linordered_idom mod_pos_pos_trivial not_take_bit_negative power_0 take_bit_0 take_bit_eq_mod take_bit_nonnegative)
apply (metis even_take_bit_eq mod_pos_pos_trivial neq0_conv numeral_eq_Suc power_0 take_bit_eq_mod take_bit_nonnegative zero_less_Suc)
done
from urel64_eq[OF this urel64_0]
have rem: "(y AND 1 = 0) = (r' = 0)" by simp
......
......@@ -1423,7 +1423,7 @@ proof -
using AE_lim_wf_times AE_lim_acc
apply eventually_elim
using \<omega> assms
apply (auto simp add: trace_in_merge_at indicator_def Bex_def)
apply (auto simp add: trace_in_merge_at indicator_eq_1_iff)
done
done
also have "\<dots> = (\<integral>\<^sup>+ \<omega>. \<integral>\<^sup>+\<omega>'. \<integral>\<^sup>+z. of_bool (trace_in {z} t x \<omega> \<and> trace_in {y} t' z \<omega>')
......
......@@ -76,8 +76,6 @@ proof -
apply (simp_all add: of_nat_diff)
apply (subst of_nat_diff)
apply (simp_all add: word_le_nat_alt take_bit_nat_eq_self unat_sub_if' unat_word_ariths)
apply (cases \<open>2 \<le> LENGTH('a)\<close>)
apply (simp_all add: unat_word_ariths take_bit_nat_eq_self)
done
then show ?thesis using n m div_half_nat [OF \<open>m \<noteq> 0\<close>, of n] unfolding q
by (simp add: word_le_nat_alt word_div_def word_mod_def Let_def take_bit_nat_eq_self
......
......@@ -333,7 +333,7 @@ proof -
have "finite ker" by (auto simp: ker_def kernel_def)
moreover have "1 \<in> ker" using \<open>n > 1\<close> by (auto simp: ker_def kernel_def h_def)
ultimately have [simp]: "card ker > 0"
by (subst card_gt_0_iff) (auto simp: ker_def kernel_def h_def)
by (subst card_gt_0_iff) auto
have totatives_eq: "totatives n = {k\<in>{1..<n}. coprime k n}"
using totatives_less[of _ n] \<open>n > 1\<close> by (force simp: totatives_def)
......
......@@ -95,8 +95,8 @@ lemma composite_aux:
assumes "\<not>prime n"
shows "measure_pmf.expectation (primality_test P n) of_bool < q"
unfolding primality_test_def using assms composite_witness_bound q_pos
by (auto simp: pmf_expectation_bind[where A = "{2..< n}"] sum_of_bool_eq_card field_simps
simp flip: sum_divide_distrib)
by (clarsimp simp add: pmf_expectation_bind[where A = "{2..< n}"] sum_of_bool_eq_card field_simps Int_def
simp flip: sum_divide_distrib)
theorem composite:
assumes "\<not>prime n"
......
......@@ -850,7 +850,7 @@ next
by simp
ultimately show ?case
using Suc [of \<open>bin div 2\<close>]
by simp (simp add: bin_to_bl_aux_alt)
by simp (auto simp add: bin_to_bl_aux_alt)
qed
lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
......@@ -858,8 +858,7 @@ lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
apply (induction n arbitrary: bin)
apply simp_all
apply (case_tac bin rule: bin_exhaust)
apply simp
apply (simp add: bin_to_bl_aux_alt ac_simps)
apply (simp_all add: bin_to_bl_aux_alt ac_simps)
done
lemma rbl_add:
......@@ -918,13 +917,12 @@ lemma rbl_mult:
apply clarsimp
apply (case_tac bina rule: bin_exhaust)
apply (case_tac binb rule: bin_exhaust)
apply simp
apply (simp add: bin_to_bl_aux_alt)
apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
apply (simp_all add: bin_to_bl_aux_alt)
apply (simp_all add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
done
lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
by (induct xs) auto
by (simp add: length_concat comp_def sum_list_triv)
lemma bin_cat_foldl_lem:
"foldl (\<lambda>u. bin_cat u n) x xs =
......
......@@ -28,7 +28,7 @@ lemma strict_part_mono_singleton[simp]:
lemma strict_part_mono_lt:
"\<lbrakk> x < f 0; strict_part_mono {.. n :: nat} f \<rbrakk> \<Longrightarrow> \<forall>m \<le> n. x < f m"
by (metis atMost_iff le_0_eq le_cases neq0_conv order.strict_trans strict_part_mono_def)
by (auto simp add: strict_part_mono_def Ball_def intro: order.strict_trans)
lemma strict_part_mono_reverseE:
"\<lbrakk> f n \<le> f m; strict_part_mono {.. N :: nat} f; n \<le> N \<rbrakk> \<Longrightarrow> n \<le> m"
......
......@@ -452,12 +452,16 @@ proof -
apply (unfold sint_word_ariths)
apply (subst signed_take_bit_int_eq_self)
prefer 4
apply (subst signed_take_bit_int_eq_self)
prefer 7
apply (subst signed_take_bit_int_eq_self)
prefer 10
apply (subst signed_take_bit_int_eq_self)
prefer 7
apply (subst signed_take_bit_int_eq_self)
prefer 10
apply (subst signed_take_bit_int_eq_self)
apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
apply (smt (z3) take_bit_nonnegative)
apply (smt (z3) take_bit_int_less_exp)
apply (smt (z3) take_bit_nonnegative)
apply (smt (z3) take_bit_int_less_exp)
done
then show ?thesis
apply (simp only: One_nat_def word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment