diff --git a/tools/c-parser/CProof.thy b/tools/c-parser/CProof.thy index 3c7484000..834f264f5 100644 --- a/tools/c-parser/CProof.thy +++ b/tools/c-parser/CProof.thy @@ -162,7 +162,7 @@ lemma c_guard_mono: apply clarsimp apply(drule_tac p=p in field_tag_sub) apply(clarsimp simp: field_lvalue_def field_offset_def field_offset_untyped_def typ_uinfo_t_def) - apply(metis (mono_tags, hide_lams) export_size_of subsetD typ_uinfo_t_def) + apply(metis (mono_tags) export_size_of subsetD typ_uinfo_t_def) done lemma c_guard_NULL_fl: diff --git a/tools/c-parser/umm_heap/Arrays.thy b/tools/c-parser/umm_heap/Arrays.thy index d09270617..98bbc7bcd 100644 --- a/tools/c-parser/umm_heap/Arrays.thy +++ b/tools/c-parser/umm_heap/Arrays.thy @@ -77,7 +77,7 @@ lemma finite_index_inj: lemma forall_finite_index: "(\k::'a::finite. P k) = (\i. i < CARD('a) \ P (finite_index i))" - by (metis (mono_tags, hide_lams) finite_index_works) + by (metis (mono_tags) finite_index_works) section \Finite Cartesian Products\ diff --git a/tools/c-parser/umm_heap/CTypesBase.thy b/tools/c-parser/umm_heap/CTypesBase.thy index 6aadefd96..977054859 100644 --- a/tools/c-parser/umm_heap/CTypesBase.thy +++ b/tools/c-parser/umm_heap/CTypesBase.thy @@ -319,9 +319,9 @@ lemma intvl_plus_sub_Suc: lemma intvl_neq_start: "\ (q::'a::len word) \ {p..+n}; p \ q \ \ q \ {p + 1..+n - Suc 0}" - by (clarsimp simp: intvl_def) - (metis One_nat_def diff_Suc_1 less_Suc_eq_0_disj less_imp_Suc_add of_nat_Suc take_bit_eq_0_iff - take_bit_of_0) + apply (clarsimp simp: intvl_def) + by (metis One_nat_def Suc_eq_plus1 gr0_conv_Suc less_diff_conv not_gr_zero of_nat_Suc + semiring_1_class.of_nat_0) lemmas unat_simps' = word_arith_nat_defs unat_of_nat len_of_addr_card mod_less diff --git a/tools/c-parser/umm_heap/SepCode.thy b/tools/c-parser/umm_heap/SepCode.thy index 21daf21d9..174158e97 100644 --- a/tools/c-parser/umm_heap/SepCode.thy +++ b/tools/c-parser/umm_heap/SepCode.thy @@ -93,7 +93,7 @@ lemma singleton_t_dom [simp]: apply(simp add: ptr_retyp_None) apply(case_tac "a \ {ptr_val p..+size_of TYPE('a)}") apply(simp add: ptr_retyp_footprint list_map_eq split: if_split_asm) - apply(drule intvlD, clarsimp simp del: unsigned_of_nat) + apply(drule intvlD, clarsimp) apply(rule s_footprintI) apply(subst (asm) word_unat.eq_norm) apply(subst (asm) mod_less) @@ -170,7 +170,7 @@ lemma ptr_retyp_tagd_exc: apply(case_tac "a \ {ptr_val p..+size_of TYPE('a)}") apply(subst (asm) ptr_retyp_footprint) apply simp - apply(drule intvlD, clarsimp simp del: unsigned_of_nat) + apply(drule intvlD, clarsimp) apply(subst (asm )word_unat.eq_norm) apply(subst (asm) mod_less) apply(subst len_of_addr_card) @@ -188,7 +188,7 @@ lemma ptr_retyp_tagd_exc: apply(case_tac "a \ {ptr_val p..+size_of TYPE('a)}") apply(subst (asm) ptr_retyp_footprint) apply simp - apply(drule intvlD, clarsimp simp del: unsigned_of_nat) + apply(drule intvlD, clarsimp) apply(subst (asm )word_unat.eq_norm) apply(subst (asm) mod_less) apply(subst len_of_addr_card) @@ -197,7 +197,7 @@ lemma ptr_retyp_tagd_exc: apply(subst (asm) list_map_eq) apply(clarsimp split: if_split_asm) apply(drule s_footprintD2) - apply(simp del: unsigned_of_nat) + apply simp apply(subst (asm) unat_of_nat) apply(subst (asm) mod_less) apply(subst len_of_addr_card) @@ -315,7 +315,7 @@ lemma heap_update_list_value': apply (simp only: heap_update_list_value addr_card_def card_word) apply (rule if_cong; simp) apply (rule iffI) - apply (drule intvlD, clarsimp simp: unat_of_nat simp del: unsigned_of_nat) + apply (drule intvlD, clarsimp simp: unat_of_nat) apply (simp add: intvl_def unat_arith_simps(4) unat_of_nat split: if_split_asm) apply (rule_tac x="unat x - unat ptr" in exI, simp) apply (rule_tac x="unat x + 2^addr_bitsize - unat ptr" in exI) @@ -772,7 +772,6 @@ lemma sep_map_field_unfold: export_uinfo t = typ_uinfo_t TYPE('b) \ \ (p \\<^sub>g\<^sup>F v) = (p \\<^sub>g\<^sup>({f}\F) (v::'a::mem_type) \\<^sup>* Ptr (&(p\f)) \\<^sub>g' ((from_bytes (access_ti\<^sub>0 t v))::'b::mem_type))" - supply unsigned_of_nat[simp del] apply(rule ext) apply(rule iffI) apply(rule_tac s\<^sub>0="x |` (dom x - fs_footprint p {f})" and @@ -1103,7 +1102,7 @@ lemma field_access_update_nth_disjD: lemma intvl_cut: "\ (x::addr) \ {p..+m}; x \ {p+of_nat k..+n}; m < addr_card \ \ unat (x - p) < k \ k + n \ unat (x - p)" - apply(drule intvlD, clarsimp simp del: unsigned_of_nat) + apply(drule intvlD, clarsimp) apply(subst unat_of_nat, subst mod_less, subst len_of_addr_card) apply(erule (1) less_trans) apply(subst (asm) unat_of_nat, subst (asm) mod_less, subst len_of_addr_card) @@ -1135,7 +1134,7 @@ lemma singleton_t_mask_out: apply(rule field_access_update_nth_disjD; simp?) apply(subst (asm) ptr_retyp_d_eq_fst) apply(clarsimp simp: empty_htd_def split: if_split_asm) - apply(drule intvlD, clarsimp simp del: unsigned_of_nat) + apply(drule intvlD, clarsimp) apply(subst unat_of_nat) apply(subst mod_less) apply(subst len_of_addr_card) diff --git a/tools/c-parser/umm_heap/SepFrame.thy b/tools/c-parser/umm_heap/SepFrame.thy index 16dd19328..c2a891821 100644 --- a/tools/c-parser/umm_heap/SepFrame.thy +++ b/tools/c-parser/umm_heap/SepFrame.thy @@ -596,7 +596,7 @@ lemma point_eq_mod_safe_ptr_safe_tag: k = (\s. lift_state (h s,d s)); htd_ind p \ \ point_eq_mod_safe {s. ptr_safe ((p s)::'b::mem_type ptr) (d s)} m k" - supply if_split_asm[split] unsigned_of_nat[simp del] + supply if_split_asm[split] apply(clarsimp simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def) apply(subgoal_tac "(a,b) \ s_footprint (p (restrict_htd s X))") prefer 2 @@ -644,7 +644,7 @@ proof (simp only: comm_restrict_safe_def comm_restrict_def, auto) apply(clarsimp simp: map_add_def list_map_eq) apply(subgoal_tac "(x,SIndexTyp y) \ s_footprint (p s)") apply(fastforce simp: dom_s_def split: if_split_asm) - apply(drule intvlD, clarsimp simp del: unsigned_of_nat) + apply(drule intvlD, clarsimp) apply(rule s_footprintI; assumption?) apply(metis len_of_addr_card less_trans max_size mod_less word_unat.eq_norm) done diff --git a/tools/c-parser/umm_heap/Separation.thy b/tools/c-parser/umm_heap/Separation.thy index c5fd6937e..c6ff4a51f 100644 --- a/tools/c-parser/umm_heap/Separation.thy +++ b/tools/c-parser/umm_heap/Separation.thy @@ -117,7 +117,7 @@ lemma lift_state_dom: apply(fastforce dest: s_footprintD intvlD simp: size_of_def) apply(frule s_footprintD2) apply(drule s_footprintD) - apply(drule intvlD, clarsimp simp del: unsigned_of_nat) + apply(drule intvlD, clarsimp) apply(rename_tac k) apply(drule_tac x=k in spec) apply(erule impE) diff --git a/tools/c-parser/umm_heap/TypHeap.thy b/tools/c-parser/umm_heap/TypHeap.thy index 53c83832f..6c73046c2 100644 --- a/tools/c-parser/umm_heap/TypHeap.thy +++ b/tools/c-parser/umm_heap/TypHeap.thy @@ -286,9 +286,7 @@ lemma typ_slice_t_not_empty [simp]: lemma list_map_typ_slice_t_not_empty [simp]: "list_map (typ_slice_t t n) \ Map.empty" - apply(simp add: list_map_def) - apply(cases "typ_slice_t t n", fastforce) - by (simp add: upt_rec) + by (simp add: list_map_def) lemma s_footprint: "s_footprint (p::'a::c_type ptr) = @@ -299,7 +297,7 @@ lemma s_footprint: lemma ptr_val_SIndexVal_in_s_footprint [simp]: "(ptr_val p, SIndexVal) \ s_footprint (p::'a::mem_type ptr)" - by (force simp: s_footprint) + by (clarsimp simp: s_footprint) (metis Abs_fnat_hom_0 sz_nzero) lemma s_footprintI: "\ n < length (typ_slice_t (typ_uinfo_t TYPE('a)) x); x < size_of TYPE('a) \ \ @@ -318,7 +316,7 @@ lemma s_footprintD2: "(x,SIndexTyp n) \ s_footprint (p::'a::mem_type ptr) \ n < length (typ_slice_t (typ_uinfo_t TYPE('a)) (unat (x - ptr_val p)))" by (clarsimp simp: s_footprint) - (metis addr_bitsize_def addr_card less_trans max_size take_bit_nat_eq_self) + (metis len_of_addr_card max_size nat_less_le of_nat_inverse order_less_le_trans) lemma s_footprint_restrict: "x \ s_footprint p \ (s |` s_footprint p) x = s x" @@ -503,7 +501,7 @@ lemma h_t_valid_ptr_safe: "d,g \\<^sub>t (p::'a::c_type ptr) \ ptr_safe p d" apply(clarsimp simp: ptr_safe_def h_t_valid_def valid_footprint_def s_footprint_def s_footprint_untyped_def dom_s_def size_of_def Let_def) - by (metis (mono_tags, hide_lams) domIff list_map map_le_def option.simps(3) surj_pair) + by (metis (mono_tags) domIff list_map map_le_def option.simps(3) surj_pair) lemma lift_t_ptr_safe: "lift_t g (h,d) (p::'a::c_type ptr) = Some x \ ptr_safe p d" @@ -803,7 +801,7 @@ lemma valid_footprint_neq_nmem: "\ valid_footprint d p f; valid_footprint d q g; p \ q; f \\<^sub>t g \ f=g \ \ p \ {q..+size_td g}" unfolding valid_footprint_def intvl_def Let_def by clarsimp - (metis add.right_neutral dvd_0_right map_prefix_same_cases semiring_1_class.of_nat_0 + (metis add.right_neutral map_prefix_same_cases semiring_1_class.of_nat_0 tag_disj_def tag_disj_prefix typ_slice_0_prefix zero_less_iff_neq_zero) lemma valid_footprint_sub: @@ -1520,13 +1518,13 @@ lemma lift_t_field_ind: apply(simp add: size_of_def) apply(drule td_set_field_lookupD[where k="(c,da)"]) apply(drule td_set_offset_size) - apply (metis (full_types) add.commute add_le_cancel_right le_trans take_bit_nat_less_eq_self) + apply(smt (verit) add.commute add_le_imp_le_right le_trans le_unat_uoi nat_le_linear) apply(rule intvl_sub_offset) apply(simp add: size_of_def) apply(drule td_set_field_lookupD) apply(drule td_set_offset_size) - by (metis (full_types) add.commute add_le_cancel_right le_trans take_bit_nat_less_eq_self) - + apply(smt (verit) add.commute add_le_imp_le_right le_trans le_unat_uoi nat_le_linear) + done (* case where 'b contains a field of type of 'a *) @@ -1559,8 +1557,9 @@ lemma field_of_t_nmem: apply(clarsimp simp: field_of_t_def field_of_def intvl_def) apply(drule td_set_offset_size) apply(simp add: addr_card_unat_minus size_of_def) - by (metis (no_types) addr_bitsize_def addr_card diff_diff_cancel le_diff_conv le_less_trans - max_size nat_less_le size_of_def take_bit_nat_eq_self_iff) + apply(thin_tac "ptr_val q = x" for x) + by (metis (no_types, opaque_lifting) Nat.add_diff_assoc add.commute le_unat_uoi less_irrefl_nat + linorder_not_le max_size order_less_trans size_of_def trans_less_add1) lemma field_of_t_init_neq_disjoint: "field_of_t p (x::'b::mem_type ptr) \ @@ -1572,13 +1571,12 @@ lemma field_of_t_init_neq_disjoint: apply(clarsimp simp: field_of_t_nmem) apply(drule intvlD) apply clarsimp - by (meson linorder_not_less take_bit_nat_less_eq_self) + by (metis le_unat_uoi nat_less_le) lemma field_of_t_final_neq_disjoint: "field_of_t (p::'a ptr) (x::'b ptr) \ {ptr_val p..+size_of TYPE('a::mem_type)} \ {ptr_val p + of_nat (size_of TYPE('a))..+size_of TYPE('b::mem_type) - (unat (ptr_val p - ptr_val x) + size_of TYPE('a))} = {}" - supply unsigned_of_nat[simp del] apply(rule ccontr) apply(drule intvl_inter) apply(erule disjE) @@ -2012,7 +2010,7 @@ lemma ptr_retyp_footprint: apply(subst htd_update_list_index; simp) apply(subst typ_slices_index; simp?) apply(drule intvlD, clarsimp) - by (meson le_less_trans take_bit_nat_less_eq_self) + by (metis le_def le_unat_uoi order_less_trans) lemma ptr_retyp_Some: "ptr_retyp (p::'a::mem_type ptr) d (ptr_val p) = @@ -2140,7 +2138,7 @@ lemma ptr_retyp_valid_footprint: apply(subst ptr_retyp_footprint) apply(rule intvlI) apply(simp add: size_of_def) - apply(clarsimp simp del: unsigned_of_nat) + apply clarsimp by (metis (no_types) len_of_addr_card less_trans map_le_map_add max_size of_nat_inverse size_of_def) lemma ptr_retyp_h_t_valid: @@ -2167,7 +2165,7 @@ lemma ptr_retyp_h_t_valid_same: apply(erule impE) apply(simp only: size_of_def [symmetric, where t="TYPE('a)"]) apply(drule intvlD, clarsimp) - apply (meson le_less_trans take_bit_nat_less_eq_self) + apply (simp add: lt_size_of_unat_simps) apply(fastforce intro: map_add_le_mapI) done @@ -2238,7 +2236,6 @@ proof - apply simp done from assms show ?thesis - supply unsigned_of_nat[simp del] apply(clarsimp simp: super_field_update_t_def) apply(rule ext) apply(clarsimp simp: field_lvalue_def split: option.splits)