This instance will be upgraded to Heptapod 0.31.0rc on 2022-05-19 at 11:00 UTC+2 (a few minutes of down time)

Commit 1d3f634a authored by haftmann's avatar haftmann
Browse files

factored out auxiliary theory

parent b5b8255ae4c4
......@@ -1101,8 +1101,10 @@ begin
fix i
obtain q n where RI: "r' (Suc i) = (q,n)" by (cases "r' (Suc i)")
have "(n + (num_acc - n mod num_acc)) mod num_acc = 0"
by (metis NN0 R' \<open>r' (Suc i) = (q, n)\<close> add_diff_cancel_left'
degen_run_bound less_imp_add_positive mod_self nat_mod_eq' snd_conv)
apply (rule dvd_imp_mod_0)
apply (metis (mono_tags, lifting) NN0 add_diff_inverse mod_0_imp_dvd
mod_add_left_eq mod_less_divisor mod_self nat_diff_split not_gr_zero zero_less_diff)
done
then obtain ofs where
OFS_LESS: "ofs<num_acc"
and [simp]: "(n + ofs) mod num_acc = 0"
......
......@@ -675,8 +675,7 @@ lemma bool_of_val_impl: "(bool_of_val_impl, bool_of_val) \<in> val_rel \<rightar
lemma smod_by_div_abs: "a smod b = a - a sdiv b * b"
using sdiv_smod_id[of a b]
by (metis add_diff_cancel2)
by (subst (2) sdiv_smod_id [of a b, symmetric]) simp
lift_definition sdiv_impl :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(sdiv)" .
lift_definition smod_impl :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(smod)" .
......@@ -687,9 +686,7 @@ lemma [code]: "sdiv_impl x y = Abs_uint32' (Rep_uint32' x sdiv Rep_uint32' y)"
by simp
lemma [code]: "smod_impl a b = a - sdiv_impl a b * b"
apply transfer
using sdiv_smod_id
by (metis add_diff_cancel2)
by transfer (simp add: smod_by_div_abs)
primrec eval_bin_op_impl_aux :: "bin_op \<Rightarrow> uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" where
......
......@@ -210,7 +210,7 @@ lemma cfg_succ_list_invar: "distinct (cfg_succ_list c)"
lemma cfg_succ_list_refine: "set (cfg_succ_list c) = cfg_succ c"
apply (induction c)
apply (simp_all only: cfg_succ.simps cfg_succ_list.simps
if_distrib[of set] if_same_eq set_map)
if_distrib[of set] set_map)
apply (simp_all)
apply (auto, force+) []
done
......
......@@ -3,6 +3,11 @@ imports Main
"HOL-Word.Word"
begin
lemma zdiv_mult_self:
\<open>m \<noteq> 0 \<Longrightarrow> (a + m * n) div m = a div m + n\<close>
for a m n :: int
by simp
section\<open>Helper Lemmas for Low-Level Operations on Machine Words\<close>
text\<open>Needed for IPv4 Syntax\<close>
......
......@@ -840,13 +840,13 @@ unfolding thread_start_actions_ok_def by blast
lemma thread_start_actions_ok_prefix:
"\<lbrakk> thread_start_actions_ok E'; lprefix E E' \<rbrakk> \<Longrightarrow> thread_start_actions_ok E"
apply(clarsimp simp add: lprefix_conv_lappend)
apply(rule thread_start_actions_okI)
apply(drule_tac a=a in thread_start_actions_okD)
apply(simp add: actions_def)
apply(metis Suc_ile_eq enat_le_plus_same(1) xtr6)
apply(auto simp add: action_obs_def lnth_lappend1 actions_def action_tid_def le_less_trans[where y="enat a" for a])
done
apply(clarsimp simp add: lprefix_conv_lappend)
apply(rule thread_start_actions_okI)
apply(drule_tac a=a in thread_start_actions_okD)
apply(simp add: actions_def)
apply(auto simp add: action_obs_def lnth_lappend1 actions_def action_tid_def le_less_trans[where y="enat a" for a])
apply (metis add.right_neutral add_strict_mono not_gr_zero)
done
lemma wf_execI [intro?]:
"\<lbrakk> is_write_seen P E ws;
......
......@@ -81,9 +81,10 @@ proof (induction xs ys i rule: sublist_at.induct)
then show ?rhs by blast
next
assume ?rhs
then obtain xs where "\<exists>ys. t#ts = xs@ss@ys \<and> Suc i = length xs" by blast
then obtain xs where "\<exists>ys. t#ts = xs@ss@ys \<and> length xs = Suc i"
by (blast dest: sym)
then have "\<exists>ys. ts = (tl xs)@ss@ys \<and> i = length (tl xs)"
by (metis hd_Cons_tl length_0_conv list.sel(3) nat.simps(3) size_Cons_lem_eq tl_append2)
by (auto simp add: length_Suc_conv)
then have "\<exists>xs ys. ts = xs@ss@ys \<and> i = length xs" by blast
with "2.IH" show ?lhs by simp
qed
......
......@@ -696,7 +696,7 @@ next
by (rule iarray_cong', insert ii, auto)
have d': "(map (?d fs) (rev [0..<j])) = (map (?d fs'') (rev [0..<j]))"
by (rule nth_equalityI, force, simp, subst updates(1), insert j i, auto
simp: nth_rev)
simp: rev_nth)
have repr_id:
"(map ((!) fs) [0..<m])[i := (fs'' ! i)] = map ((!) fs'') [0..<m]" (is "?xs = ?ys")
proof (rule nth_equalityI, force)
......@@ -768,7 +768,7 @@ proof (atomize(full), goal_cases)
note start = this \<mu>_small_row_refl[of i fs]
have id: "small_fs_state state = map (\<lambda> i. fs ! i) (rev [0..<i])"
unfolding state using to_list_repr[OF impl inv state] i
unfolding list_repr_def by (auto intro!: nth_equalityI simp: nth_rev min_def)
unfolding list_repr_def by (auto intro!: nth_equalityI simp: rev_nth min_def)
from i have mm: "[0..<m] = [0 ..< i] @ [i] @ [Suc i ..< m]"
by (intro nth_equalityI, auto simp: nth_append nth_Cons split: nat.splits)
from res[unfolded def] True
......
......@@ -332,7 +332,7 @@ proof -
assume jk_i: "j + k < i"
have "[i>..j] = rev [j..<i]" using rev_upt_upt by simp
also have "... ! k = [j..<i] ! (length [j..<i] - 1 - k)"
by (rule nth_rev, insert jk_i, auto)
using jk_i by (simp add: rev_nth)
also have "... = [j..<i] ! (i - j - 1 - k)" by auto
also have "... = j + (i - j - 1 - k)" by (rule nth_upt, insert jk_i, auto)
finally show ?thesis using jk_i by auto
......
......@@ -13,7 +13,7 @@ section \<open>Implementations of bit operations on \<^typ>\<open>int\<close> op
lemma not_minus_numeral_inc_eq:
\<open>NOT (- numeral (Num.inc n)) = (numeral n :: int)\<close>
by (simp add: not_int_def sub_inc_One)
by (simp add: not_int_def sub_inc_One_eq)
lemma [code_abbrev]:
\<open>test_bit = (bit :: int \<Rightarrow> nat \<Rightarrow> bool)\<close>
......@@ -52,7 +52,7 @@ lemma int_and_code [code]: fixes i j :: int shows
"Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (bitORN_num (Num.BitM n) m) num.One"
"Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (bitORN_num (num.Bit0 n) m) num.One"
apply (simp_all add: int_numeral_bitAND_num Num.add_One
sub_inc_One inc_BitM not_minus_numeral_inc_eq
sub_inc_One_eq inc_BitM_eq not_minus_numeral_inc_eq
flip: int_not_neg_numeral int_or_not_bitORN_num split: option.split)
apply (simp_all add: ac_simps)
done
......
......@@ -11,10 +11,11 @@ begin
text \<open>More lemmas\<close>
lemma nat_div_eq_Suc_0_iff: "n div m = Suc 0 \<longleftrightarrow> n \<ge> m \<and> n < 2 * m"
apply (auto simp add: sdl)
using not_less apply fastforce
apply (metis One_nat_def Suc_1 div_eq_0_iff lessI neq0_conv td_gal_lt)
lemma nat_div_eq_Suc_0_iff: "n div m = Suc 0 \<longleftrightarrow> m \<le> n \<and> n < 2 * m"
apply auto
using div_greater_zero_iff apply fastforce
apply (metis One_nat_def div_greater_zero_iff dividend_less_div_times mult.right_neutral mult_Suc mult_numeral_1 numeral_2_eq_2 zero_less_numeral)
apply (simp add: div_nat_eqI)
done
lemma Suc_0_lt_2p_len_of: "Suc 0 < 2 ^ LENGTH('a :: len)"
......@@ -96,7 +97,7 @@ proof -
have "2 * (n div 2 div m) * m < 2 ^ LENGTH('a)" using n unfolding div_mult2_eq[symmetric]
by(subst (2) mult.commute)(simp add: minus_mod_eq_div_mult [symmetric] diff_mult_distrib minus_mod_eq_mult_div [symmetric] div_mult2_eq)
moreover have "2 * (n div 2 div m) * m \<le> n"
by(metis div_mult2_eq div_mult_le mult.assoc mult.commute)
by (metis div_mult2_eq dtle mult.assoc mult.left_commute)
ultimately
have r: "x - ?q * y = of_nat (n - ?q' * m)"
and "y \<le> x - ?q * y \<Longrightarrow> of_nat (n - ?q' * m) - y = of_nat (n - ?q' * m - m)"
......@@ -228,7 +229,7 @@ proof(cases "1 << (LENGTH('a) - 1) \<le> y")
finally have div: "x div of_nat n = 1" using False n
by(simp add: word_div_eq_1_iff not_less word_le_nat_alt unat_of_nat)
moreover have "x mod y = x - x div y * y"
by (metis add_diff_cancel2 word_mod_div_equality)
by (simp add: minus_div_mult_eq_mod)
with div n have "x mod y = x - y" by simp
ultimately show ?thesis using False y n by simp
qed
......
......@@ -4,6 +4,11 @@ imports
"HOL-ODE-Numerics.ODE_Numerics"
Result_File_Coarse
begin
lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x"
by (simp add: numeral_eq_Suc)
text \<open>\label{sec:lorenz}\<close>
text \<open>TODO: move to isabelle? \<close>
......
......@@ -2701,7 +2701,8 @@ lemma isFDERIV_product: "isFDERIV n xs fas vs \<longleftrightarrow>
length fas = n \<and> length xs = n \<and>
list_all (\<lambda>(x, f). isDERIV x f vs) (List.product xs fas)"
apply (auto simp: isFDERIV_def list_all2_iff in_set_zip list_all_length product_nth)
apply (metis gt_or_eq_0 less_mult_imp_div_less mod_less_divisor not_less0)
by auto
apply auto
apply (metis gr_implies_not_zero gr_zeroI less_mult_imp_div_less pos_mod_bound)
done
end
......@@ -149,9 +149,13 @@ begin
lemma lc2aux: "{l. length l=2 \<and> valid l} = {[B,B]}"
by (auto 4 3 intro: valid.intros elim: valid.cases simp: replicate_Cons_eq)
lemma valid_3R: \<open>valid [R, R, R]\<close>
using valid.intros(3) [of \<open>[]\<close> 3] by (simp add: numeral_eq_Suc valid.intros)
lemma lc3_aux: "{l. length l=3 \<and> valid l} = {[B,B,B], [R,R,R]}"
by (auto 4 4 intro: valid.intros valid_red[of 3, simplified] elim: valid.cases
simp: replicate_Cons_eq)
by (auto 4 4 intro: valid.intros valid_3R elim: valid.cases
simp: replicate_Cons_eq)
lemma lcounts_init: "lcount 0 = 1" "lcount 1 = 1" "lcount 2 = 1" "lcount 3 = 2"
using lc0 lc1aux lc2aux lc3_aux unfolding lcount_def by simp_all
......
......@@ -713,10 +713,8 @@ subsubsection \<open>Simulation\<close>
lemma mod_mult_mod_eq[mod_simps]: "x mod (k * N) mod N = x mod N"
by (meson dvd_eq_mod_eq_0 mod_mod_cancel mod_mult_self2_is_0)
lemma mod_eq_imp_eq_aux: "b mod N = (a::nat) mod N \<Longrightarrow> a\<le>b \<Longrightarrow> b<a+N \<Longrightarrow> b=a"
by (metis Groups.add_ac add_0_right
le_add_diff_inverse less_diff_conv2 nat_minus_mod
nat_minus_mod_plus_right mod_if)
lemma mod_eq_imp_eq_aux: "b mod N = (a::nat) mod N \<Longrightarrow> a\<le>b \<Longrightarrow> b<a+N \<Longrightarrow> b=a"
using nat_mod_eq_lemma by force
lemma mod_eq_imp_eq:
"\<lbrakk>b \<le> x; x < b + N; b \<le> y; y < b + N; x mod N = y mod N \<rbrakk> \<Longrightarrow> x=y"
......@@ -1034,9 +1032,8 @@ subsection \<open>Refinement 3: Using an Array\<close>text_raw \<open>\label{sec
apply clarify
apply (erule blstep.cases, erule bstep_sng.cases)
unfolding invar4_def
apply safe
apply (metis N_gt0 fun_upd_other fun_upd_same mod_mod_trivial
nat_mod_lem has_ticket_simps(2))
apply safe
apply (metis N_gt0 fun_upd_apply has_ticket_simps(2) mod_less_divisor)
apply (metis fun_upd_triv)
apply (metis fun_upd_other fun_upd_same has_ticket_simps(3))
apply (metis fun_upd_other fun_upd_same has_ticket_def has_ticket_simps(4))
......
......@@ -182,7 +182,7 @@ lemma rbl_word_scast:
apply (rule nth_equalityI)
apply (simp add: word_size takefill_last_def)
apply (clarsimp simp: nth_scast takefill_last_def
nth_takefill word_size nth_rev to_bl_nth)
nth_takefill word_size rev_nth to_bl_nth)
apply (cases "LENGTH('b)")
apply simp
apply (clarsimp simp: less_Suc_eq_le linorder_not_less
......@@ -376,7 +376,7 @@ lemma rev_bin_to_bl_simps:
lemma to_bl_upt: "to_bl x = rev (map ((!!) x) [0 ..< size x])"
apply (rule nth_equalityI)
apply (simp add: word_size)
apply (auto simp: to_bl_nth word_size nth_rev)
apply (auto simp: to_bl_nth word_size rev_nth)
done
lemma rev_to_bl_upt: "rev (to_bl x) = map ((!!) x) [0 ..< size x]"
......
......@@ -1647,7 +1647,7 @@ lemma nth_bounded:
"\<lbrakk>(x :: 'a :: len word) !! n; x < 2 ^ m; m \<le> len_of TYPE ('a)\<rbrakk> \<Longrightarrow> n < m"
apply (frule test_bit_size)
apply (clarsimp simp: test_bit_bl word_size)
apply (simp add: nth_rev)
apply (simp add: rev_nth)
apply (subst(asm) is_aligned_add_conv[OF is_aligned_0',
simplified add_0_left, rotated])
apply assumption+
......@@ -3513,7 +3513,7 @@ lemma word_rsplit_upt:
apply (rule nth_equalityI, simp)
apply (intro allI word_eqI impI)
apply (simp add: test_bit_rsplit_alt word_size)
apply (simp add: nth_ucast nth_shiftr nth_rev field_simps)
apply (simp add: nth_ucast nth_shiftr rev_nth field_simps)
apply (simp add: length_word_rsplit_exp_size)
apply (metis mult.commute given_quot_alt word_size word_size_gt_0)
done
......@@ -6171,7 +6171,7 @@ lemma bin_to_bl_of_bl_eq:
apply (clarsimp simp only: len_bin_to_bl nth_bin_to_bl word_test_bit_def[symmetric])
apply (simp add: nth_shiftr nth_shiftl
shiftl_t2n[where n=c, simplified mult.commute, simplified, symmetric])
apply (simp add: is_aligned_nth[THEN iffD1, rule_format] test_bit_of_bl nth_rev)
apply (simp add: is_aligned_nth[THEN iffD1, rule_format] test_bit_of_bl rev_nth)
apply arith
done
......
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