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

Don't reuse the s_footprint_intvl theorem name.

This commit is contained in:
Thomas Sewell 2014-10-01 11:16:40 +10:00
parent ea63ccd7ed
commit a818e13e3e
2 changed files with 4 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
proof/asmrefine/TestGraphRefine.thy
View File

@ -103,28 +103,6 @@ schematic_lemma "PROP ?P"
apply (tactic {* ALLGOALS (nth (tacs @{context}) 6) *})
apply (simp add: pglobal_valid_def)
apply (erule_tac g="kernel_all_global_addresses.ksReadyQueues_global_data" in ptr_inverse_safe_htd_safe_globals_list_distinct, rule globals_list_distinct)
apply (rule kernel_all_global_addresses.global_data_mems)
apply (simp add: global_data_defs global_data_region_def global_data_def
)
apply (rule order_trans, rule s_footprint_intvl)
apply simp
thm globals_list_valid_def
find_theorems s_footprint
thm s_footprint_intvl
find_theorems global_data_region
thm global_data_defs
term
find_theorems ptr_inverse_safe
find_theorems "_ - _ = _ + (- _)"
thm word_minus_def
apply (simp_all add: diff_conv_add_uminus add.commute)
apply (tactic {* ALLGOALS (nth (tacs @{context}) 7) *})
apply (tactic {* ALLGOALS (nth (tacs @{context}) 8) *})

8
tools/asmrefine/GlobalsSwap.thy
View File

@ -777,7 +777,7 @@ lemma globals_list_distinct_filter_member:
apply (erule distinct_prop_weaken, simp)
done
lemma s_footprint_intvl:
lemma s_footprint_intvl_subset:
"s_footprint (p :: 'a ptr) \<subseteq> {ptr_val p ..+ size_of TYPE ('a :: c_type)} \<times> UNIV"
by (auto simp: s_footprint_def s_footprint_untyped_def
intvl_def size_of_def)
@ -793,7 +793,7 @@ lemma h_val_globals_swap_in_const_global:
apply (erule disjoint_h_val_globals_swap_filter,
erule(1) globals_list_distinct_filter_member)
apply simp
apply (rule order_trans, rule s_footprint_intvl)
apply (rule order_trans, rule s_footprint_intvl_subset)
apply (simp add: global_data_region_def const_global_data_def
Times_subset_cancel2)
apply (erule intvl_sub_offset)
@ -814,7 +814,7 @@ lemma const_globals_in_memory_to_h_val_with_swap:
erule(1) globals_list_distinct_filter_member)
apply simp
apply (simp add: global_data_region_def const_global_data_def)
apply (rule order_trans, rule s_footprint_intvl)
apply (rule order_trans, rule s_footprint_intvl_subset)
apply simp
apply (erule(1) const_globals_in_memory_h_val[symmetric])
done
@ -840,7 +840,7 @@ lemma global_data_implies_ptr_inverse_safe:
htd_safe_def globals_list_distinct_def)
apply (drule(1) bspec)+
apply (simp add: global_data_region_def global_data_ok_def global_data_def)
apply (auto dest!: s_footprint_intvl[THEN subsetD])
apply (auto dest!: s_footprint_intvl_subset[THEN subsetD])
done
ML {*