adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

drefine: More updates for Isabelle 2014.

This commit is contained in:
David Greenaway 2014-09-18 11:04:47 +10:00
parent e3b893e7d6
commit cc71c3aadf
3 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/drefine/CNode_DR.thy
View File

@ -2262,7 +2262,7 @@ lemma dcorres_get_object_cnode_split:
apply simp_all
apply (clarsimp split: nat.splits)
apply (clarsimp simp: get_cnode'_def cnode_size_bits_def split: option.splits kernel_object.split)
apply (case_tac a, simp_all)
apply (case_tac x2, simp_all)
done
lemma arch_recycle_cap_ret:

6
proof/drefine/KHeap_DR.thy
View File

@ -421,14 +421,14 @@ shows "\<lbrakk>opt_cap_wp_at P slot (transform s);valid_objs s; valid_etcbs s\<
apply (clarsimp simp:transform_cnode_contents_def option_map_join_def
split:option.splits Structures_A.kernel_object.splits nat.splits)
apply (clarsimp simp:cte_wp_at_cases well_formed_cnode_invsI transform_cslot_ptr_def split:if_splits)
apply (rule_tac x = x2a in exI,simp add: nat_to_bl_bl_to_bin)
apply (rule_tac x = x2b in exI,simp add: nat_to_bl_bl_to_bin)
apply (drule(1) valid_etcbs_tcb_etcb, simp)
prefer 6 (* IRQ Node *)
apply (clarsimp split: Structures_A.kernel_object.splits nat.splits option.splits)
apply (clarsimp simp:transform_cnode_contents_def option_map_join_def
split:option.splits Structures_A.kernel_object.splits nat.splits)
apply (clarsimp simp:cte_wp_at_cases well_formed_cnode_invsI transform_cslot_ptr_def split:if_splits)
apply (rule_tac x = aa in exI,simp add: nat_to_bl_bl_to_bin)
apply (rule_tac x = x2a in exI,simp add: nat_to_bl_bl_to_bin)
apply (frule assms)
apply ((simp_all add:Let_def cap_counts_def transform_tcb_def
split:option.splits if_splits arch_kernel_obj.splits
@ -760,7 +760,7 @@ proof -
apply (clarsimp simp: transform_objects_def)
apply (rule ext)
apply clarsimp
apply (simp add: Option.map_def restrict_map_def map_add_def split: option.splits)
apply (simp add: option_map_def restrict_map_def map_add_def split: option.splits)
apply (frule (1) cdl_objects_cnode, simp)
apply (clarsimp simp: assert_opt_def has_slots_def)
apply (clarsimp simp: update_slots_def object_slots_def transform_cnode_contents_upd)

2
proof/drefine/StateTranslation_D.thy
View File

@ -331,7 +331,7 @@ definition
| IRQAckIRQ \<Rightarrow> Some (IrqHandlerIntent IrqHandlerAckIntent)
| IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent)
| IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent)
| IRQSetMode \<Rightarrow> Option.map IrqHandlerIntent (transform_intent_irq_set_mode args)
| IRQSetMode \<Rightarrow> option_map IrqHandlerIntent (transform_intent_irq_set_mode args)
| ARMPageTableMap \<Rightarrow>
map_option PageTableIntent
(transform_intent_page_table_map args)