diff --git a/proof/invariant-abstract/ADT_AI.thy b/proof/invariant-abstract/ADT_AI.thy index edf4320dd..3adec50f9 100644 --- a/proof/invariant-abstract/ADT_AI.thy +++ b/proof/invariant-abstract/ADT_AI.thy @@ -8,7 +8,7 @@ * @TAG(GD_GPL) *) -header {* Abstract datatype for the abstract specification *} +chapter {* Abstract datatype for the abstract specification *} (* "header" changed to "chapter" *) theory ADT_AI imports @@ -72,7 +72,7 @@ text {* returning an optional kernel-entry event. Note that the current-thread identifiers are identical in both specs - (i.e. @{term "Structures_A.cur_thread \ 'z state \ obj_ref"} + (i.e. @{term "Structures_A.cur_thread :: 'z state \ obj_ref"} in the abstract kernel model and @{text "KernelStateData_H.ksCurThread \ kernel_state \ machine_word"} in the executable specification). diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy index f1f1fe350..5f8e8f773 100644 --- a/proof/invariant-abstract/CNodeInv_AI.thy +++ b/proof/invariant-abstract/CNodeInv_AI.thy @@ -1045,7 +1045,7 @@ termination rec_del apply (rename_tac word option nat) apply (case_tac nat, simp_all) apply (simp only: trans_state_update'[symmetric] not_recursive_cspaces_more_update) - apply (clarsimp simp: in_monad Pair_fst_snd_eq rec_del.psimps) + apply (clarsimp simp: in_monad prod_eqI rec_del.psimps) apply (erule use_valid [OF _ cap_swap_fd_not_recursive]) apply (frule use_valid [OF _ get_cap_cte_wp_at], simp) apply (drule in_inv_by_hoareD [OF get_cap_inv]) diff --git a/proof/invariant-abstract/EmptyFail_AI.thy b/proof/invariant-abstract/EmptyFail_AI.thy index cfbc9af5d..ff5b4db46 100644 --- a/proof/invariant-abstract/EmptyFail_AI.thy +++ b/proof/invariant-abstract/EmptyFail_AI.thy @@ -136,7 +136,7 @@ lemma put_empty_fail[wp]: crunch_ignore (empty_fail) - (add: bind bindE lift liftE liftM when whenE unless unlessE return fail assert_opt + (add: bind bindE lift liftE liftM "when" whenE unless unlessE return fail assert_opt mapM mapM_x sequence_x catch handleE invalidateTLB_ASID_impl invalidateTLB_VAASID_impl cleanByVA_impl cleanByVA_PoU_impl invalidateByVA_impl invalidateByVA_I_impl invalidate_I_PoU_impl cleanInvalByVA_impl branchFlush_impl diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index 0323c5a02..984f2d508 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -2121,8 +2121,8 @@ lemma pd_shifting_again5: lemma pd_shifting_kernel_mapping_slots: "\is_aligned word pd_bits; - (sl :: word32) \ (kernel_base >> (20\nat)) - (1\word32)\ - \ ucast ((sl << (2\nat)) + word && mask pd_bits >> (2\nat)) + (sl :: word32) \ (kernel_base >> (20::nat)) - (1::word32)\ + \ ucast ((sl << (2::nat)) + word && mask pd_bits >> (2::nat)) \ kernel_mapping_slots" apply (subst pd_shifting_again5) apply assumption+ diff --git a/proof/invariant-abstract/PDPTEntries_AI.thy b/proof/invariant-abstract/PDPTEntries_AI.thy index 9c3c7e486..5bdfe1f3e 100644 --- a/proof/invariant-abstract/PDPTEntries_AI.thy +++ b/proof/invariant-abstract/PDPTEntries_AI.thy @@ -1288,13 +1288,13 @@ lemma pde_range_sz_le: (* BUG , revisit the following lemmas , moved from ArchAcc_R.thy *) lemma mask_pd_bits_shift_ucast_align[simp]: - "is_aligned (ucast (p && mask pd_bits >> 2)\12 word) 4 = - is_aligned ((p\word32) >> 2) 4" + "is_aligned (ucast (p && mask pd_bits >> 2)::12 word) 4 = + is_aligned ((p::word32) >> 2) 4" by (clarsimp simp: is_aligned_mask mask_def pd_bits) word_bitwise lemma mask_pt_bits_shift_ucast_align[simp]: - "is_aligned (ucast (p && mask pt_bits >> 2)\word8) 4 = - is_aligned ((p\word32) >> 2) 4" + "is_aligned (ucast (p && mask pt_bits >> 2)::word8) 4 = + is_aligned ((p::word32) >> 2) 4" by (clarsimp simp: is_aligned_mask mask_def pt_bits_def pageBits_def) word_bitwise diff --git a/proof/refine/Bits_R.thy b/proof/refine/Bits_R.thy index eee86146d..64dae3a0b 100644 --- a/proof/refine/Bits_R.thy +++ b/proof/refine/Bits_R.thy @@ -13,7 +13,7 @@ imports Corres begin crunch_ignore (add: - bind return when get gets fail + bind return "when" get gets fail assert put modify unless select alternative assert_opt gets_the returnOk throwError lift bindE diff --git a/proof/refine/KHeap_R.thy b/proof/refine/KHeap_R.thy index 782e02de9..f61816513 100644 --- a/proof/refine/KHeap_R.thy +++ b/proof/refine/KHeap_R.thy @@ -357,7 +357,7 @@ lemma setObject_cte_wp_at2': apply (erule exEI [where 'a=word32]) apply (clarsimp simp: ps_clear_upd' lookupAround2_char1) apply (drule(1) x) - apply (clarsimp simp: lookupAround2_char1 Pair_fst_snd_eq) + apply (clarsimp simp: lookupAround2_char1 prod_eqI) apply (fastforce dest: bspec [OF _ ranI]) apply (erule disjEI) apply (clarsimp simp: ps_clear_upd' lookupAround2_char1 @@ -370,7 +370,7 @@ lemma setObject_cte_wp_at2': apply (frule updateObject_type) apply (case_tac ba, simp_all) apply (drule(1) x) - apply (clarsimp simp: Pair_fst_snd_eq lookupAround2_char1) + apply (clarsimp simp: prod_eqI lookupAround2_char1) apply (fastforce dest: bspec [OF _ ranI]) done @@ -1230,7 +1230,7 @@ lemma setObject_valid_objs': apply (drule spec, erule mp) apply (drule(1) x) apply (simp add: ranI) - apply (simp add: Pair_fst_snd_eq lookupAround2_char1) + apply (simp add: prod_eqI lookupAround2_char1) apply (clarsimp elim!: ranE split: split_if_asm simp: ranI) done diff --git a/proof/refine/StateRelation.thy b/proof/refine/StateRelation.thy index 8ba724d12..0d617713a 100644 --- a/proof/refine/StateRelation.thy +++ b/proof/refine/StateRelation.thy @@ -472,7 +472,7 @@ lemma cap_relation_case': | _ \ cap_relation cap cap')" by (simp split: cap.split arch_cap.split) -schematic_lemma cap_relation_case: +schematic_goal cap_relation_case: "cap_relation cap cap' = ?P" apply (subst cap_relation_case') apply (clarsimp cong: cap.case_cong arch_cap.case_cong)