From 9e8fea8dade0a2a7c75ad3c3c34f8352d4537a32 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 17 Nov 2021 09:44:18 +1100 Subject: [PATCH] isabelle2021-1 ainvs arm: AInvs update Mostly word proof changes, and small number of places where tactics solve more. Signed-off-by: Gerwin Klein --- proof/invariant-abstract/ARM/ArchAcc_AI.thy | 12 ++--- .../ARM/ArchCSpaceInv_AI.thy | 2 +- .../invariant-abstract/ARM/ArchCSpace_AI.thy | 3 -- .../invariant-abstract/ARM/ArchDetype_AI.thy | 2 +- .../ARM/ArchInvariants_AI.thy | 6 ++- .../ARM/ArchLevityCatch_AI.thy | 13 +++-- .../invariant-abstract/ARM/ArchRetype_AI.thy | 2 +- .../ARM/ArchSchedule_AI.thy | 2 +- .../invariant-abstract/ARM/ArchUntyped_AI.thy | 2 +- .../ARM/ArchVSpaceEntries_AI.thy | 8 ++- .../invariant-abstract/ARM/ArchVSpace_AI.thy | 35 ++++--------- proof/invariant-abstract/CSpaceInv_AI.thy | 50 +++++++++---------- proof/invariant-abstract/CSpace_AI.thy | 4 +- proof/invariant-abstract/LevityCatch_AI.thy | 23 +++------ proof/invariant-abstract/Retype_AI.thy | 2 +- proof/invariant-abstract/Schedule_AI.thy | 6 +-- proof/invariant-abstract/TcbAcc_AI.thy | 5 +- proof/invariant-abstract/Untyped_AI.thy | 10 ++-- proof/invariant-abstract/VSpaceEntries_AI.thy | 10 ---- 19 files changed, 75 insertions(+), 122 deletions(-) diff --git a/proof/invariant-abstract/ARM/ArchAcc_AI.thy b/proof/invariant-abstract/ARM/ArchAcc_AI.thy index cced3e28e..a6f80af24 100644 --- a/proof/invariant-abstract/ARM/ArchAcc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchAcc_AI.thy @@ -352,6 +352,7 @@ lemma pde_at_aligned_vptr: is_aligned_shiftl_self)+ apply (prove "pd = (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits)") subgoal + supply bit_simps[simp del] apply (subst mask_lower_twice[symmetric, where n=6]) apply (simp add: pd_bits_def pageBits_def) apply (subst add.commute, subst add_mask_lower_bits) @@ -392,11 +393,9 @@ lemma pde_shifting: have H: "(0xF::word32) < 2 ^ 4" by simp from prems show ?thesis apply (subst (asm) word_plus_and_or_coroll) - apply (rule word_eqI) + apply word_eqI subgoal for n - apply (clarsimp simp: word_size nth_shiftr is_aligned_nth) - apply (spec "n + 20") - apply (frule test_bit_size[where n="n + 20"]) + apply (spec "20 + n") apply (simp add: word_size) apply (insert H) apply (drule (1) order_le_less_trans) @@ -404,7 +403,6 @@ lemma pde_shifting: apply (drule_tac z="2 ^ 4" in order_le_less_trans, assumption) apply (drule word_power_increasing) by simp+ - apply (clarsimp simp: word_size nth_shiftl nth_shiftr is_aligned_nth) apply (erule disjE) apply (insert H)[1] @@ -412,8 +410,8 @@ lemma pde_shifting: apply (drule bang_is_le) apply (drule order_le_less_trans[where z="2 ^ 4"], assumption) apply (drule word_power_increasing; simp) - apply (spec "n' + 20") - apply (frule test_bit_size[where n = "n' + 20"]) + apply (spec "20 + n'") + apply (frule test_bit_size) by (simp add: word_size) qed done diff --git a/proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy b/proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy index 379f26880..aa736a7ac 100644 --- a/proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy @@ -79,7 +79,7 @@ lemma replace_cap_invs: apply (erule allEI, erule allEI) apply (drule_tac x="fst p" in spec, drule_tac x="snd p" in spec) apply (clarsimp simp: gen_obj_refs_subset) - apply (drule(1) disjoint_subset, simp) + apply (drule(1) disjoint_subset, erule (1) notE) apply (rule conjI) apply (erule descendants_inc_minor) apply simp diff --git a/proof/invariant-abstract/ARM/ArchCSpace_AI.thy b/proof/invariant-abstract/ARM/ArchCSpace_AI.thy index 2db693ce7..a9d8aabf8 100644 --- a/proof/invariant-abstract/ARM/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpace_AI.thy @@ -420,9 +420,6 @@ lemma tcb_cnode_index_def2 [CSpace_AI_assms]: apply (rule nth_equalityI) apply (simp add: word_bits_def) apply (clarsimp simp: to_bl_nth word_size word_bits_def) - apply (subst of_nat_ucast[where 'a=32 and 'b=3]) - apply (simp add: is_down_def target_size_def source_size_def word_size) - apply (simp add: nth_ucast del: unsigned_of_nat) apply fastforce done diff --git a/proof/invariant-abstract/ARM/ArchDetype_AI.thy b/proof/invariant-abstract/ARM/ArchDetype_AI.thy index c8ad02632..58062ba37 100644 --- a/proof/invariant-abstract/ARM/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetype_AI.thy @@ -71,7 +71,7 @@ next x = ptr + of_nat n' * 4 + 2 \ x = ptr + of_nat n' * 4 + 3)" by (simp add: xin' conj_disj_distribL ex_disj_distrib field_simps) - show "?thesis m x" by (simp add: xin word_rsplit_0 cong: if_cong) + show "?thesis m x" by (simp add: xin word_rsplit_0 word_bits_conv cong: if_cong) qed from al have "is_aligned (ptr + of_nat n' * 4) 2" diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy index 10ade024a..220a57c20 100644 --- a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy @@ -1410,6 +1410,7 @@ lemmas abs_atyp_at_lifts = lemma page_directory_pde_atI: "\ page_directory_at p s; x < 2 ^ pageBits; pspace_aligned s \ \ pde_at (p + (x << 2)) s" + supply bit_simps[simp del] apply (clarsimp simp: obj_at_def pde_at_def) apply (drule (1) pspace_alignedD[rotated]) apply (clarsimp simp: a_type_def @@ -1429,6 +1430,7 @@ lemma page_directory_pde_atI: lemma page_table_pte_atI: "\ page_table_at p s; x < 2^(pt_bits - 2); pspace_aligned s \ \ pte_at (p + (x << 2)) s" + supply bit_simps[simp del] apply (clarsimp simp: obj_at_def pte_at_def) apply (drule (1) pspace_alignedD[rotated]) apply (clarsimp simp: a_type_def @@ -1889,7 +1891,7 @@ proof - apply (erule (6) 2) apply (clarsimp simp: vs_refs_pages_def graph_of_def obj_at_def pde_ref_pages_def data_at_def - dest!: vs_lookup_pages1D elim!: disjE + dest!: vs_lookup_pages1D split: if_split_asm pde.splits) apply (frule_tac d=ac in vpt, assumption+) apply (erule converse_rtranclE) @@ -2431,7 +2433,7 @@ lemma valid_arch_mdb_eqI: assumes "caps_of_state s = caps_of_state s'" assumes "is_original_cap s = is_original_cap s'" shows "valid_arch_mdb (is original_cap s') (caps_of_state s')" - by (clarsimp simp: valid_arch_mdb_def) + by clarsimp lemma arch_tcb_context_absorbs[simp]: "arch_tcb_context_set uc2 (arch_tcb_context_set uc1 a_tcb) \ arch_tcb_context_set uc2 a_tcb" diff --git a/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy b/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy index 516cc8727..481b6c955 100644 --- a/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy +++ b/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy @@ -30,21 +30,20 @@ lemma asid_high_bits_of_add_ucast: "is_aligned w asid_low_bits \ asid_high_bits_of (ucast (x::10 word) + w) = asid_high_bits_of w" apply (rule word_eqI) - apply (simp add: word_size asid_high_bits_of_def nth_ucast nth_shiftr is_aligned_nth) + apply (simp add: word_size asid_high_bits_of_def is_aligned_nth) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) - apply (clarsimp simp: nth_ucast) + apply clarsimp apply (drule test_bit_size) - apply (simp add: word_size asid_low_bits_def) - apply (auto dest: test_bit_size simp: word_size asid_low_bits_def nth_ucast) + apply (simp add: asid_low_bits_def) + apply (auto dest: test_bit_size simp: word_size asid_low_bits_def) done lemma asid_high_bits_of_add: "\is_aligned w asid_low_bits; x \ 2 ^ asid_low_bits - 1\ \ asid_high_bits_of (w + x) = asid_high_bits_of w" apply (rule word_eqI) - apply (simp add: word_size asid_high_bits_of_def nth_ucast nth_shiftr - is_aligned_nth) + apply (simp add: word_size asid_high_bits_of_def is_aligned_nth) apply (drule le2p_bits_unset_32, simp add: asid_low_bits_def) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) @@ -52,7 +51,7 @@ lemma asid_high_bits_of_add: apply (case_tac "na < asid_low_bits") apply (simp add: asid_low_bits_def linorder_not_less word_bits_def) apply (auto dest: test_bit_size - simp: asid_low_bits_def word_bits_def nth_ucast) + simp: asid_low_bits_def word_bits_def) done lemma pageBits_less_word_bits [simp]: diff --git a/proof/invariant-abstract/ARM/ArchRetype_AI.thy b/proof/invariant-abstract/ARM/ArchRetype_AI.thy index 4bbeb69f6..53df89922 100644 --- a/proof/invariant-abstract/ARM/ArchRetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchRetype_AI.thy @@ -1264,7 +1264,7 @@ lemma storeWord_um_eq_0: "\\m. underlying_memory m p = 0\ storeWord x 0 \\_ m. underlying_memory m p = 0\" - by (simp add: storeWord_def word_rsplit_0 | wp)+ + by (simp add: storeWord_def word_rsplit_0 word_bits_conv | wp)+ lemma clearMemory_um_eq_0: "\\m. underlying_memory m p = 0\ diff --git a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy index 733e870d4..ed41554a3 100644 --- a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy @@ -25,7 +25,7 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: apply (erule use_valid) apply (simp add: storeWord_def word_rsplit_0) apply wp - apply simp + apply (clarsimp simp: word_bits_conv) done crunch device_state_inv[wp]: clearExMonitor "\ms. P (device_state ms)" diff --git a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy index dbc2cc981..0e5b8a32e 100644 --- a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy @@ -18,7 +18,7 @@ lemma of_bl_nat_to_cref[Untyped_AI_assms]: apply (clarsimp intro!: less_mask_eq simp: nat_to_cref_def of_drop_to_bl word_size word_less_nat_alt word_bits_def) - by (simp add: take_bit_nat_def) + by (metis add_lessD1 le_unat_uoi nat_le_iff_add nat_le_linear) lemma cnode_cap_ex_cte[Untyped_AI_assms]: diff --git a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy index f20fc38fa..03a62391a 100644 --- a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy @@ -115,8 +115,6 @@ lemma shift_0x3C_set: nth_shiftl neg_mask_test_bit word_bits_conv) apply (safe, simp_all add: is_aligned_nth)[1] - apply (drule_tac x="Suc (Suc n)" in spec) - apply simp apply (rule_tac x="ucast x && mask 4" in image_eqI) apply (rule word_eqI[rule_format]) apply (drule_tac x=n in word_eqD) @@ -1089,7 +1087,7 @@ lemma neg_mask_pt_6_4: (ptr::word32) && ~~ mask 6 && mask pt_bits >> 2" apply (simp add:pt_bits_def pageBits_def) apply word_bitwise - apply (simp add:word_size) + apply (simp add:word_size mask_def) done lemma neg_mask_pd_6_4: @@ -1097,7 +1095,7 @@ lemma neg_mask_pd_6_4: (ptr::word32) && ~~ mask 6 && mask pd_bits >> 2" apply (simp add:pd_bits_def pageBits_def) apply word_bitwise - apply (simp add:word_size) + apply (simp add:word_size mask_def) done lemma mask_out_same_pt: @@ -1192,7 +1190,7 @@ lemma ensure_safe_mapping_ensures[wp]: apply (clarsimp simp :upto_enum_def upto_enum_step_def Fun.comp_def upto_0_to_n2) apply (cut_tac x = "of_nat x" and n = 2 in word_power_nonzero_32) - apply (simp add:word_of_nat_less word_bits_def of_nat_neq_0 del: word_of_nat_eq_0_iff)+ + apply (simp add:word_of_nat_less word_bits_def of_nat_neq_0)+ done have neq_pt_offset: "\z zs xa (p::word32). \[0 , 4 .e. 0x3C] = z # zs; xa \ set zs;is_aligned p 6 \ \ diff --git a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy index 3a7ec5884..3d662dbb4 100644 --- a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy @@ -83,15 +83,7 @@ lemma asid_low_high_bits': asid_high_bits_of x = asid_high_bits_of y; x \ 2 ^ asid_bits - 1; y \ 2 ^ asid_bits - 1 \ \ x = y" - apply (rule asid_low_high_bits) - apply (rule word_eqI) - apply (subst (asm) bang_eq) - apply (simp add: nth_ucast asid_low_bits_def word_size) - apply (rule word_eqI) - apply (subst (asm) bang_eq)+ - apply (simp add: nth_ucast asid_low_bits_def) - apply assumption+ - done + by (rule asid_low_high_bits; (assumption|word_eqI_solve simp: asid_low_bits_def)?) lemma table_cap_ref_at_eq: "table_cap_ref c = Some [x] \ vs_cap_ref c = Some [x]" @@ -680,34 +672,29 @@ lemma ex_asid_high_bits_plus: apply (rule word_and_le1) apply (subst (asm) mask_def) apply (simp add: upper_bits_unset_is_l2p_32 [symmetric]) - apply (subst word_plus_and_or_coroll) - apply (rule word_eqI) - apply (clarsimp simp: word_size nth_ucast nth_shiftl) - apply (rule word_eqI) - apply (clarsimp simp: word_size nth_ucast nth_shiftl nth_shiftr asid_high_bits_of_def - asid_low_bits_def word_bits_def asid_bits_def) + apply (subst word_plus_and_or_coroll; word_eqI) + apply (clarsimp simp: asid_high_bits_of_def asid_low_bits_def word_bits_def asid_bits_def) apply (rule iffI) prefer 2 apply fastforce apply (clarsimp simp: linorder_not_less) - apply (subgoal_tac "n < 17", simp) - apply (clarsimp simp add: linorder_not_le [symmetric]) - done + by (metis add_One_commute add_diff_inverse_nat le_add1 less_diff_conv2 less_imp_diff_less + numeral_plus_numeral semiring_norm(10) semiring_norm(2) semiring_norm(3) + semiring_norm(4) semiring_norm(9)) lemma asid_high_bits_shl: "\ is_aligned base asid_low_bits; base \ mask asid_bits \ \ ucast (asid_high_bits_of base) << asid_low_bits = base" apply (simp add: mask_def upper_bits_unset_is_l2p_32 [symmetric]) - apply (rule word_eqI[rule_format]) - apply (simp add: is_aligned_nth nth_ucast nth_shiftl nth_shiftr asid_low_bits_def - asid_high_bits_of_def word_size asid_bits_def word_bits_def) + apply word_eqI + apply (simp add: asid_low_bits_def asid_high_bits_of_def word_bits_conv asid_bits_def) apply (rule iffI, clarsimp) apply (rule context_conjI) apply (clarsimp simp add: linorder_not_less [symmetric]) apply simp - apply (subgoal_tac "n < 17", simp) - apply (clarsimp simp add: linorder_not_le [symmetric]) - done + by (metis less_imp_le_nat linorder_neqE_nat nat_diff_less numeral_plus_numeral pl_pl_rels + semiring_norm(10) semiring_norm(2) semiring_norm(3) semiring_norm(8) semiring_norm(9) + trans_less_add1) lemma valid_asid_map_unmap: diff --git a/proof/invariant-abstract/CSpaceInv_AI.thy b/proof/invariant-abstract/CSpaceInv_AI.thy index 4ed0f4852..3bd69dc5f 100644 --- a/proof/invariant-abstract/CSpaceInv_AI.thy +++ b/proof/invariant-abstract/CSpaceInv_AI.thy @@ -496,7 +496,7 @@ lemma set_cap_cte_wp_at: set_cap cap ptr \\uu s. cte_wp_at P p s\" apply (simp add: cte_wp_at_caps_of_state) - apply (wpx set_cap_caps_of_state) + apply (wp set_cap_caps_of_state) apply clarsimp done @@ -506,7 +506,7 @@ lemma set_cap_cte_wp_at': set_cap cap ptr \\uu s. cte_wp_at P p s\" apply (simp add: cte_wp_at_caps_of_state) - apply (wpx set_cap_caps_of_state) + apply (wp set_cap_caps_of_state) apply clarsimp done @@ -536,7 +536,7 @@ lemma set_cap_tcb: lemma set_cap_sets: "\\\ set_cap cap p \\rv s. cte_wp_at (\c. c = cap) p s\" apply (simp add: cte_wp_at_caps_of_state) - apply (wpx set_cap_caps_of_state) + apply (wp set_cap_caps_of_state) apply clarsimp done @@ -655,13 +655,10 @@ lemma set_cap_cte_cap_wp_to: \ ex_cte_cap_wp_to P p' s\ set_cap cap p \\rv. ex_cte_cap_wp_to P p'\" - apply (simp add: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) - apply wpx - apply (intro impI, elim conjE exE) - apply (case_tac "(a, b) = p") - apply fastforce - apply fastforce - done + apply (simp add: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state del: split_paired_Ex) + apply (wp hoare_vcg_ex_lift) + apply clarify + by (metis fun_upd_other fun_upd_same option.sel) lemma set_cap_iflive: @@ -684,7 +681,7 @@ lemma update_cap_iflive: "\cte_wp_at (\cap'. zobj_refs cap' = zobj_refs cap) p and if_live_then_nonz_cap\ set_cap cap p \\rv s. if_live_then_nonz_cap s\" - apply (wpx set_cap_iflive) + apply (wp set_cap_iflive) apply (clarsimp elim!: cte_wp_at_weakenE) done @@ -701,7 +698,7 @@ lemma set_cap_ifunsafe: \ (cap \ cap.NullCap \ ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\ set_cap cap p \\rv s. if_unsafe_then_cap s\" apply (simp add: if_unsafe_then_cap_def) - apply (wpx set_cap_cte_cap_wp_to) + apply (wp set_cap_cte_cap_wp_to hoare_vcg_all_lift hoare_vcg_imp_lift) apply clarsimp apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state) @@ -720,7 +717,7 @@ lemma update_cap_ifunsafe: and if_unsafe_then_cap and (\s. cap \ cap.NullCap \ ex_cte_cap_wp_to (appropriate_cte_cap cap) p s)\ set_cap cap p \\rv s. if_unsafe_then_cap s\" - apply (wpx set_cap_ifunsafe) + apply (wp set_cap_ifunsafe) apply (clarsimp elim!: cte_wp_at_weakenE) done @@ -737,8 +734,8 @@ lemma set_cap_globals [wp]: "\valid_global_refs and (\s. global_refs s \ cap_range cap = {})\ set_cap cap p \\_. valid_global_refs\" - apply (simp add: valid_global_refs_def valid_refs_def2) - apply (wpx set_cap_caps_of_state) + apply (simp add: valid_global_refs_def valid_refs_def2 Ball_def) + apply (wp set_cap_caps_of_state hoare_vcg_all_lift hoare_vcg_imp_lift) apply (clarsimp simp: ran_def) apply blast done @@ -1009,7 +1006,7 @@ lemma new_cap_valid_pspace: set_cap cap p \\rv. valid_pspace\" apply (simp add: valid_pspace_def) - apply (wpx set_cap_valid_objs new_cap_iflive new_cap_ifunsafe new_cap_zombies) + apply (wp set_cap_valid_objs new_cap_iflive new_cap_ifunsafe new_cap_zombies) apply (auto simp: cte_wp_at_caps_of_state) done @@ -1244,7 +1241,7 @@ lemma delete_duplicate_valid_pspace: set_cap cap.NullCap p \\rv. valid_pspace\" apply (simp add: valid_pspace_def) - apply (wpx set_cap_valid_objs delete_duplicate_iflive delete_duplicate_ifunsafe + apply (wp set_cap_valid_objs delete_duplicate_iflive delete_duplicate_ifunsafe set_cap_zombies, auto elim!: cte_wp_at_weakenE) done @@ -1258,7 +1255,7 @@ lemma set_cap_valid_pspace: set_cap cap p \\rv. valid_pspace\" apply (simp add: valid_pspace_def) - apply (wpx set_cap_valid_objs set_cap_iflive set_cap_zombies) + apply (wp set_cap_valid_objs set_cap_iflive set_cap_zombies) apply (clarsimp elim!: cte_wp_at_weakenE | rule conjI)+ done @@ -1289,7 +1286,7 @@ lemma set_cap_idle[wp]: lemma set_cap_cte_at_neg[wp]: "\\s. \ cte_at sl s\ set_cap cap sl' \\rv s. \ cte_at sl s\" apply (simp add: cte_at_typ) - apply (wpx set_cap_typ_at) + apply (wp set_cap_typ_at) done lemma set_cap_cte_wp_at_neg: @@ -1338,10 +1335,10 @@ lemma set_cap_irq_handlers: \ cte_wp_at (\cap'. \irq \ cap_irqs cap - cap_irqs cap'. irq_issued irq s) ptr s\ set_cap cap ptr \\rv. valid_irq_handlers\" - apply (simp add: valid_irq_handlers_def irq_issued_def) - apply wpx + apply (simp add: valid_irq_handlers_def irq_issued_def Ball_def) + apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift) apply (clarsimp simp: cte_wp_at_caps_of_state elim!: ranE split: if_split_asm) - apply (auto intro: ranI) + apply auto done lemma arch_obj_caps_of: @@ -1819,7 +1816,7 @@ lemma cap_insert_ex_cap: apply (simp add: cap_insert_def) apply (wp|simp split del: if_split)+ apply (wp set_cap_cap_to get_cap_wp set_cap_cte_wp_at set_untyped_cap_as_full_cte_wp_at)+ - apply (clarsimp simp: set_untyped_cap_as_full_def split del: if_splits) + apply (clarsimp simp: set_untyped_cap_as_full_def split del: if_split) apply (wp set_cap_cap_to get_cap_wp)+ apply (clarsimp elim!: cte_wp_at_weakenE simp: is_cap_simps cte_wp_at_caps_of_state) apply (simp add: masked_as_full_def) @@ -1865,7 +1862,7 @@ lemma cap_insert_ifunsafe: apply (simp add: cap_insert_def) apply (wp get_cap_wp | simp split del: if_split)+ apply (rule new_cap_ifunsafe) - apply (simp add: set_untyped_cap_as_full_def split del: if_splits) + apply (simp add: set_untyped_cap_as_full_def split del: if_split) apply (wp set_cap_cte_wp_at set_cap_ifunsafe set_cap_cte_cap_wp_to get_cap_wp)+ apply (clarsimp simp: is_cap_simps cte_wp_at_caps_of_state) apply (rule untyped_cap_update_ex_cte_cap_wp_to) @@ -1907,7 +1904,7 @@ lemma cap_insert_cap_wp_to[wp]: cte_wp_at_caps_of_state update_cdt_def) apply (wp get_cap_wp | simp split del: if_split)+ apply (rule allI) - apply (clarsimp simp del: split_def,rule conjI) + apply (clarsimp, rule conjI) apply (clarsimp simp: is_cap_simps cte_wp_at_caps_of_state) apply (rule_tac x = a in exI) apply (rule_tac x = b in exI) @@ -2002,8 +1999,7 @@ lemma set_untyped_cap_full_valid_objs: \\r. valid_objs\" apply (simp add: set_untyped_cap_as_full_def split del: if_split) apply (wp set_cap_valid_objs) - apply (clarsimp simp: valid_cap_free_index_update tcb_cap_valid_caps_of_stateD - cte_wp_at_caps_of_state caps_of_state_valid_cap) + apply (clarsimp simp: tcb_cap_valid_caps_of_stateD cte_wp_at_caps_of_state caps_of_state_valid_cap) done diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index 6617286fc..adbd61728 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -388,9 +388,7 @@ lemma of_bl_take: "length xs < len_of TYPE('a) \ of_bl (take n xs) = ((of_bl xs) >> (length xs - n) :: ('a :: len) word)" apply (clarsimp simp: bang_eq and_bang test_bit_of_bl rev_take conj_comms nth_shiftr) - apply safe - apply simp_all - apply (clarsimp elim!: rsubst[where P="\x. rev xs ! x"])+ + apply auto done diff --git a/proof/invariant-abstract/LevityCatch_AI.thy b/proof/invariant-abstract/LevityCatch_AI.thy index 5d246715a..b07f68a68 100644 --- a/proof/invariant-abstract/LevityCatch_AI.thy +++ b/proof/invariant-abstract/LevityCatch_AI.thy @@ -105,18 +105,15 @@ lemma mask_split_aligned_neg: shows "(p && ~~ mask m) + (ucast x << a) = p \ False" apply (subst (asm) word_plus_and_or_coroll) apply (clarsimp simp: word_simps bang_eq) - subgoal for n - apply (drule test_bit_size) - apply (clarsimp simp: word_simps) - using len by arith + apply (metis bit_imp_le_length diff_add_inverse le_add1 len(2) less_diff_iff) apply (insert x) apply (erule notE) - apply (rule word_eqI) + apply word_eqI subgoal for n using len - apply (clarsimp simp: word_simps bang_eq) + apply (clarsimp) apply (spec "n + a") - by (clarsimp simp: word_ops_nth_size word_size) + by (clarsimp simp: add.commute) done lemma mask_alignment_ugliness: @@ -126,14 +123,8 @@ lemma mask_alignment_ugliness: \n \ m. \z !! n\ \ False" apply (erule notE) - apply (rule word_eqI) - apply (clarsimp simp: is_aligned_nth word_ops_nth_size word_size) - apply (subst word_plus_and_or_coroll) - apply (rule word_eqI) - apply (clarsimp simp: word_size) - subgoal for \ na - apply (spec na)+ - by simp - by auto + apply (subst word_plus_and_or_coroll; word_eqI) + apply (meson linorder_not_le) + by (auto simp: le_def) end diff --git a/proof/invariant-abstract/Retype_AI.thy b/proof/invariant-abstract/Retype_AI.thy index 63fa0004f..d08e3573a 100644 --- a/proof/invariant-abstract/Retype_AI.thy +++ b/proof/invariant-abstract/Retype_AI.thy @@ -278,7 +278,7 @@ lemma range_cover_le_n_less: lemma unat_of_nat_n :"unat ((of_nat n):: 'a :: len word) = n" using range_cover_n_less - by (simp add:unat_of_nat del: unsigned_of_nat) + by (simp add:unat_of_nat) lemma unat_of_nat_n_shift: diff --git a/proof/invariant-abstract/Schedule_AI.thy b/proof/invariant-abstract/Schedule_AI.thy index 73eecd7e4..059dd5be1 100644 --- a/proof/invariant-abstract/Schedule_AI.thy +++ b/proof/invariant-abstract/Schedule_AI.thy @@ -54,10 +54,10 @@ lemma findM_inv'': apply simp done -lemmas findM_inv' = findM_inv''[OF suffix_order.order.refl] +lemmas findM_inv' = findM_inv''[OF suffix_order.refl] lemma findM_inv: - assumes x: "\x xs. \P\ m x \\rv. P\" + assumes x: "\x. \P\ m x \\rv. P\" shows "\P\ findM m xs \\rv. P\" by (rule findM_inv', simp_all add: x) @@ -78,7 +78,7 @@ lemma postfix_tails: apply clarsimp apply clarsimp apply (erule meta_allE, erule meta_allE, drule meta_mp, - rule suffix_appendI[OF suffix_order.order.refl]) + rule suffix_appendI[OF suffix_order.refl]) apply clarsimp apply (erule suffix_ConsI) done diff --git a/proof/invariant-abstract/TcbAcc_AI.thy b/proof/invariant-abstract/TcbAcc_AI.thy index 82b1d1c25..7fcf42425 100644 --- a/proof/invariant-abstract/TcbAcc_AI.thy +++ b/proof/invariant-abstract/TcbAcc_AI.thy @@ -892,10 +892,9 @@ lemma get_cap_aligned: lemma shiftr_eq_mask_eq: "a && ~~ mask b = c && ~~ mask b \ a >> b = c >> b" apply (rule word_eqI) - apply (drule_tac x="n + b" in word_eqD) - apply (case_tac "n + b < size a") + apply (drule_tac x="b + n" in word_eqD) + apply (case_tac "b + n < size a") apply (simp add: nth_shiftr word_size word_ops_nth_size) - apply (simp add: nth_shiftr) apply (auto dest!: test_bit_size simp: word_size) done diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index f40671de4..eb9187f0c 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -419,10 +419,8 @@ lemma range_cover_stuff: apply simp apply (subst shiftl_shiftr1) apply (simp_all add: word_size) - apply (rule bit_eqI) - apply (simp add: word_bits_conv shiftl_word_eq bit_and_iff bit_push_bit_iff bit_1_iff bit_mask_iff bit_exp_iff not_le) - apply auto - done + apply (word_eqI_solve simp: word_bits_conv) + done have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: machine_word) ^ sz" using bound cmp not_0 @@ -478,7 +476,7 @@ lemma range_cover_stuff: apply (subst unat_shiftl_absorb[where p = "sz - bits"]) apply (rule order_trans[OF le_shiftr]) apply (rule space) - apply (simp add: shiftr_div_2n_w word_bits_def)+ + apply (simp add: word_bits_def power_minus_is_div)+ apply (simp add: shiftl_t2n[symmetric] field_simps shiftr_shiftl1) apply (subst is_aligned_diff_neg_mask[OF is_aligned_weaken]) apply (rule is_aligned_triv) @@ -512,7 +510,7 @@ lemma range_cover_stuff: apply (subst word_of_nat_le) apply (subst unat_power_lower_machine) apply ((simp add: word_bits_def)+)[3] - apply (simp del: word_of_nat_eq_0_iff) + apply simp apply (erule of_nat_neq_0) apply (erule le_less_trans) apply (rule power_strict_increasing) diff --git a/proof/invariant-abstract/VSpaceEntries_AI.thy b/proof/invariant-abstract/VSpaceEntries_AI.thy index 65916c31c..7f2967540 100644 --- a/proof/invariant-abstract/VSpaceEntries_AI.thy +++ b/proof/invariant-abstract/VSpaceEntries_AI.thy @@ -87,16 +87,6 @@ lemma ucast_neg_mask: apply (auto simp:nth_ucast neg_mask_test_bit word_size) done -lemma shiftr_eq_neg_mask_eq: - "a >> b = c >> b \ a && ~~ mask b = c && ~~ mask b" - apply (rule word_eqI[rule_format]) - apply (simp add:neg_mask_test_bit) - apply (drule_tac f = "\x. x !! (n - b)" in arg_cong) - apply (simp add:nth_shiftr) - apply (rule iffI) - apply simp+ - done - lemma delete_objects_reduct: "valid (\s. P (kheap (s :: ('z::state_ext) state))) (modify (detype {ptr..ptr + 2 ^ bits - 1})) (\_ s. P(kheap (s :: ('z::state_ext) state))) \