Isabelle 2016 update: minor fixes
This commit is contained in:
parent
92cde6069f
commit
b7376a56e2
|
@ -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 \<Colon> 'z state \<Rightarrow> obj_ref"}
|
||||
(i.e. @{term "Structures_A.cur_thread :: 'z state \<Rightarrow> obj_ref"}
|
||||
in the abstract kernel model and
|
||||
@{text "KernelStateData_H.ksCurThread \<Colon> kernel_state \<Rightarrow> machine_word"}
|
||||
in the executable specification).
|
||||
|
|
|
@ -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])
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -2121,8 +2121,8 @@ lemma pd_shifting_again5:
|
|||
|
||||
lemma pd_shifting_kernel_mapping_slots:
|
||||
"\<lbrakk>is_aligned word pd_bits;
|
||||
(sl :: word32) \<le> (kernel_base >> (20\<Colon>nat)) - (1\<Colon>word32)\<rbrakk>
|
||||
\<Longrightarrow> ucast ((sl << (2\<Colon>nat)) + word && mask pd_bits >> (2\<Colon>nat))
|
||||
(sl :: word32) \<le> (kernel_base >> (20::nat)) - (1::word32)\<rbrakk>
|
||||
\<Longrightarrow> ucast ((sl << (2::nat)) + word && mask pd_bits >> (2::nat))
|
||||
\<notin> kernel_mapping_slots"
|
||||
apply (subst pd_shifting_again5)
|
||||
apply assumption+
|
||||
|
|
|
@ -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)\<Colon>12 word) 4 =
|
||||
is_aligned ((p\<Colon>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)\<Colon>word8) 4 =
|
||||
is_aligned ((p\<Colon>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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -472,7 +472,7 @@ lemma cap_relation_case':
|
|||
| _ \<Rightarrow> 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)
|
||||
|
|
Loading…
Reference in New Issue