diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index 4e7557447..ee723426c 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -112,9 +112,9 @@ lemma exec_handlers_Hoare_from_vcg_might_fail: \ exec_handlers_Hoare \ P (c # hs) Q A'" apply (clarsimp simp: exec_handlers_Hoare_def split del: if_split split: if_split_asm) - apply (erule exec_handlers.cases, simp_all) - apply (case_tac hsa, simp_all) - apply (erule exec_handlers.cases, simp_all) + apply (erule exec_handlers.cases; simp) + apply (cases hs; simp) + apply (erule exec_handlers.cases; simp) apply (frule exec_handlers_Cons_le, simp) apply (drule hoare_sound) apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) @@ -872,10 +872,11 @@ proof - apply (rule diff_Suc_less [OF lt0]) done qed - thus ?thesis using lxs - apply (auto simp: init_xs_def dest!: spec[where x=Nil] - simp: j pn word_less_nat_alt neq_Nil_conv unat_word_ariths unat_of_nat push_mods - elim!: ccorres_guard_imp2) + thus ?thesis using lxs j pn + apply (auto simp: init_xs_def word_less_nat_alt neq_Nil_conv unat_word_ariths unat_of_nat push_mods + simp del: unsigned_of_nat + elim!: ccorres_guard_imp2 + dest!: spec[where x=Nil]) done qed @@ -897,8 +898,7 @@ lemma ccorres_abstract_cslift: fixes p :: "'a :: c_type ptr" shows "(\rv. P rv \ ccorres_underlying sr Gamm rvr xf arrel axf G (G' rv) hs a c) \ ccorres_underlying sr Gamm rvr xf arrel axf G ({s. P ((f::'a \ ('b::{type})) s) \ s \ G' (f s)} \ {s. P (f s)}) hs a c" - apply (erule ccorres_abstract_h_val) - done + by (fact ccorres_abstract_h_val) lemma ccorres_cond2: assumes abs: "\s s'. (s, s') \ sr \ R s \ P = (s' \ P') " diff --git a/lib/clib/CTranslationNICTA.thy b/lib/clib/CTranslationNICTA.thy index 8c7eb2839..c45a5b22b 100644 --- a/lib/clib/CTranslationNICTA.thy +++ b/lib/clib/CTranslationNICTA.thy @@ -7,7 +7,6 @@ theory CTranslationNICTA imports "CParser.CTranslation" - "Word_Lib.Word_Lib" begin declare len_of_numeral_defs [simp del] diff --git a/lib/clib/LemmaBucket_C.thy b/lib/clib/LemmaBucket_C.thy index af74483b5..bb07dcef9 100644 --- a/lib/clib/LemmaBucket_C.thy +++ b/lib/clib/LemmaBucket_C.thy @@ -23,9 +23,8 @@ lemma hrs_mem_f: "f (hrs_mem s) = hrs_mem (hrs_mem_update f s)" done lemma hrs_mem_heap_update: - "heap_update p v (hrs_mem s) = hrs_mem (hrs_mem_update (heap_update p v) s)" - apply (rule hrs_mem_f) - done + "heap_update p v (hrs_mem s) = hrs_mem (hrs_mem_update (heap_update p v) s)" + by (rule hrs_mem_f) lemma addr_card_wb: "addr_card = 2 ^ word_bits" @@ -188,7 +187,7 @@ next apply (rule set_eqI) apply clarsimp apply (rename_tac w) - apply (case_tac w) + apply (case_tac w rule: word_nat_cases) apply (rename_tac m) apply (rule_tac x=m in exI) apply simp @@ -210,10 +209,7 @@ lemma upto_intvl_eq': apply (subst field_simps [symmetric], rule word_plus_mono_right) apply simp apply assumption - apply (subst Word_Lemmas.of_nat_mono_maybe_le [symmetric]) - apply simp - apply simp - apply simp + apply (rule of_nat_mono_maybe_le; simp) apply clarsimp apply (rule_tac x = "unat (xa - x)" in exI) apply simp @@ -221,13 +217,8 @@ lemma upto_intvl_eq': apply (rule nat_diff_less) apply (subst (asm) word_le_nat_alt, erule order_le_less_trans) apply (subst add_diff_eq[symmetric], subst unat_plus_if') - apply (simp add: no_olen_add_nat) - apply (simp add: le_eq_less_or_eq) - apply (erule disjE) - apply (subst unat_minus_one) - apply (erule (1) of_nat_neq_0) - apply (simp add: unat_of_nat) - apply (erule ssubst, rule unat_lt2p) + apply (simp add: no_olen_add_nat le_eq_less_or_eq) + apply (metis gt0_iff_gem1 unat_less_helper unat_ucast_less_no_overflow unsigned_0 unsigned_less) apply (simp add: word_le_nat_alt) done @@ -275,8 +266,8 @@ next qed lemma intvl_nowrap: - fixes x :: "'a::len word" - shows "\y \ 0; unat y + z \ 2 ^ len_of TYPE('a)\ \ x \ {x + y ..+ z}" + "\y \ 0; unat y + z \ 2 ^ len_of TYPE('a)\ \ x \ {x + y ..+ z}" for x :: "'a::len word" + supply unsigned_of_nat[simp del] apply clarsimp apply (drule intvlD) apply clarsimp @@ -391,7 +382,7 @@ proof (rule disjointI, rule notI) also have "\ \ c" by (rule abc) also have "\ \ c + of_nat ky" using cld dlt ky - by - (rule word_random [OF _ iffD1 [OF Word_Lemmas.of_nat_mono_maybe_le]], simp+ ) + by (meson less_imp_le of_nat_mono_maybe word_random) finally show False using ac by simp qed @@ -413,6 +404,7 @@ lemma intvl_off_disj: and zoff: "z + off < 2 ^ word_bits" shows "{x ..+ y} \ {x + of_nat off ..+ z} = {}" using ylt zoff + supply unsigned_of_nat[simp del] apply (cases "off = 0") apply simp apply (rule contrapos_pp [OF TrueI]) @@ -461,9 +453,7 @@ qed lemma typ_slice_t_self: "td \ fst ` set (typ_slice_t td m)" - apply (cases td) - apply (simp split: if_split) - done + by (fact ladder_set_self) lemma drop_heap_list_le2: "heap_list h n (x + of_nat k) @@ -777,6 +767,7 @@ proof - \ unat (of_nat x * of_nat (size_of TYPE('a)) + (of_nat k :: addr)) = x * size_of TYPE('a) + k" using size + supply unsigned_of_nat[simp del] apply (case_tac "size_of TYPE('a)", simp_all) apply (case_tac "CARD('b)", simp_all) apply (subst unat_add_lem[THEN iffD1]) @@ -881,6 +872,7 @@ lemma typ_slice_t_array: lemma h_t_valid_Array_element': "\ htd \\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); coerce \ n < CARD('b) \ \ htd \\<^sub>t array_ptr_index p coerce n" + supply unsigned_of_nat[simp del] apply (clarsimp simp only: h_t_valid_def valid_footprint_def Let_def c_guard_def c_null_guard_def) apply (subgoal_tac "\offs. array_ptr_index p coerce n = ptr_add (ptr_coerce p) (of_nat offs) @@ -958,10 +950,7 @@ lemma ptr_safe_Array_element: lemma from_bytes_eq: "from_bytes [x] = x" - apply (clarsimp simp:from_bytes_def update_ti_t_def typ_info_word) - apply (simp add:word_rcat_def) - apply (simp add:bin_rcat_def) - by (metis len8 word_of_int_uint word_ubin.Abs_norm) + by (clarsimp simp:from_bytes_def update_ti_t_def typ_info_word word_rcat_def) lemma bytes_disjoint:"(x::('a::c_type) ptr) \ y \ {ptr_val x + a ..+ 1} \ {ptr_val y + a ..+ 1} = {}" by (clarsimp simp:intvl_def) @@ -1076,7 +1065,7 @@ lemma neq_imp_bytes_disjoint: apply (subgoal_tac "(ptr_val x + j && ~~ mask n) = (ptr_val y + i && ~~ mask n)") apply (subst (asm) neg_mask_add_aligned, simp, simp add: word_less_nat_alt) apply (subst (asm) neg_mask_add_aligned, simp, simp add: word_less_nat_alt) - apply (clarsimp simp: is_aligned_neg_mask_eq) + apply clarsimp apply simp apply (clarsimp simp: c_guard_def ptr_aligned_def is_aligned_def) apply (clarsimp simp: c_guard_def ptr_aligned_def is_aligned_def) @@ -1206,7 +1195,7 @@ proof (rule classical) by blast then obtain k' where mv: "mv = ptr_val p' + of_nat k'" and klt: "k' < size_td (typ_info_t TYPE('b))" - by (clarsimp dest!: intvlD simp: size_of_def typ_uinfo_size) + by (clarsimp dest!: intvlD simp: size_of_def) let ?mv = "ptr_val p' + of_nat k'" diff --git a/lib/clib/SimplRewrite.thy b/lib/clib/SimplRewrite.thy index 59396f596..952c8a111 100644 --- a/lib/clib/SimplRewrite.thy +++ b/lib/clib/SimplRewrite.thy @@ -28,7 +28,7 @@ where lemma add_statefn_id1: "add_statefn id x = x" - by (induct x, simp_all add: inv_id[simplified id_def]) + by (induct x) auto lemma add_statefn_id[simp]: "add_statefn id = id"