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

c-parser umm_heap: larger cleanup pass 

Mainly proof indentation, elimination of non-terminal auto, and modernizing
ancient proofs.
This commit is contained in:
Gerwin Klein 2019-05-28 17:37:53 +10:00 committed by Matthew Brecknell
parent c13432b0c4
commit aea325ac6a
16 changed files with 3321 additions and 5333 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tools/c-parser/CProof.thy
View File

@ -202,7 +202,7 @@ apply(simp add: field_lvalue_def field_offset_def field_offset_untyped_def typ_u
apply(unfold c_guard_def)
apply clarsimp
apply(drule c_null_guard)+
apply clarsimp
apply (clarsimp simp: word_neq_0_conv)
done
lemma c_guard_ptr_aligned_fl:

61
tools/c-parser/umm_heap/ArrayAssertion.thy
View File

@ -45,37 +45,28 @@ definition
lemma map_td_list_map:
"map_td_list f = map (map_td_pair f)"
apply (rule ext)
apply (induct_tac x, simp_all)
done
by (rule ext, rename_tac x) (induct_tac x, simp_all)
lemma uinfo_array_tag_n_m_eq:
"n \<le> CARD('b)
\<Longrightarrow> export_uinfo (array_tag_n n :: (('a :: wf_type)['b :: finite]) field_desc typ_desc)
= uinfo_array_tag_n_m TYPE ('a) n (CARD('b))"
apply (clarsimp simp: uinfo_array_tag_n_m_def array_tag_n_eq
map_td_list_map o_def adjust_ti_def map_td_map)
apply (simp add: typ_uinfo_t_def export_uinfo_def)
apply (rule map_td_extI)
apply simp
apply (clarsimp simp: field_norm_blah)
apply (clarsimp simp: uinfo_array_tag_n_m_def array_tag_n_eq map_td_list_map
o_def adjust_ti_def map_td_map typ_uinfo_t_def export_uinfo_def)
apply (fastforce intro: map_td_extI simp: field_norm_blah)
done
lemma typ_uinfo_array_tag_n_m_eq:
"typ_uinfo_t TYPE (('a :: wf_type)['b :: finite])
= uinfo_array_tag_n_m TYPE ('a) (CARD('b)) (CARD('b))"
by (simp add: typ_uinfo_t_def typ_info_array array_tag_def
uinfo_array_tag_n_m_eq)
by (simp add: typ_uinfo_t_def typ_info_array array_tag_def uinfo_array_tag_n_m_eq)
text \<open>Alternative to h_t_valid for arrays. This allows reasoning
about arrays of variable width.\<close>
definition
h_t_array_valid :: "heap_typ_desc \<Rightarrow> ('a :: c_type) ptr \<Rightarrow> nat \<Rightarrow> bool"
where
definition h_t_array_valid :: "heap_typ_desc \<Rightarrow> ('a :: c_type) ptr \<Rightarrow> nat \<Rightarrow> bool" where
"h_t_array_valid htd ptr n = valid_footprint htd (ptr_val ptr) (uinfo_array_tag_n_m TYPE ('a) n n)"
text \<open>Assertion that pointer p is within an array that continues
for at least n more elements.\<close>
text \<open>Assertion that pointer p is within an array that continues for at least n more elements.\<close>
definition
"array_assertion (p :: ('a :: c_type) ptr) n htd
= (\<exists>q i j. h_t_array_valid htd q j
@ -102,8 +93,7 @@ lemma array_assertion_shrink_leftI:
lemma h_t_array_valid:
"h_t_valid htd gd (p :: (('a :: wf_type)['b :: finite]) ptr)
\<Longrightarrow> h_t_array_valid htd (ptr_coerce p :: 'a ptr) (CARD('b))"
by (clarsimp simp: h_t_valid_def h_t_array_valid_def
typ_uinfo_array_tag_n_m_eq)
by (clarsimp simp: h_t_valid_def h_t_array_valid_def typ_uinfo_array_tag_n_m_eq)
lemma array_ptr_valid_array_assertionD:
"h_t_valid htd gd (p :: (('a :: wf_type)['b :: finite]) ptr)
@ -129,13 +119,12 @@ if the pointer is not dereferenced, thus the strong/weak distinction.
If the pointer doesn't actually move, nothing is learned.
\<close>
definition
ptr_add_assertion :: "('a :: c_type) ptr \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> heap_typ_desc \<Rightarrow> bool"
where
"ptr_add_assertion ptr offs strong htd \<equiv> offs = 0
\<or> array_assertion (if offs < 0 then CTypesDefs.ptr_add ptr offs else ptr)
(if offs < 0 then nat (- offs) else if strong then Suc (nat offs) else nat offs)
htd"
definition ptr_add_assertion :: "('a :: c_type) ptr \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> heap_typ_desc \<Rightarrow> bool" where
"ptr_add_assertion ptr offs strong htd \<equiv>
offs = 0 \<or>
array_assertion (if offs < 0 then CTypesDefs.ptr_add ptr offs else ptr)
(if offs < 0 then nat (- offs) else if strong then Suc (nat offs) else nat offs)
htd"
lemma ptr_add_assertion_positive:
"offs \<ge> 0 \<Longrightarrow> ptr_add_assertion ptr offs strong htd
@ -158,12 +147,11 @@ lemma ptr_add_assertion_uint[simp]:
text \<open>Ignore char and void pointers. The C standard specifies that arithmetic on
char and void pointers doesn't create any special checks.\<close>
definition
ptr_add_assertion' :: "('a :: c_type) ptr \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> heap_typ_desc \<Rightarrow> bool"
where
"ptr_add_assertion' ptr offs strong htd = (typ_uinfo_t TYPE('a) = typ_uinfo_t TYPE(word8)
\<or> typ_uinfo_t TYPE ('a) = typ_uinfo_t TYPE(unit)
\<or> ptr_add_assertion ptr offs strong htd)"
definition ptr_add_assertion' :: "('a :: c_type) ptr \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> heap_typ_desc \<Rightarrow> bool" where
"ptr_add_assertion' ptr offs strong htd =
(typ_uinfo_t TYPE('a) = typ_uinfo_t TYPE(word8)
\<or> typ_uinfo_t TYPE ('a) = typ_uinfo_t TYPE(unit)
\<or> ptr_add_assertion ptr offs strong htd)"
(* Useful for clearing away these assumptions. *)
lemma td_diff_from_typ_name:
@ -178,20 +166,15 @@ lemmas ptr_add_assertion' = ptr_add_assertion'_def td_diff_from_typ_name typ_nam
text \<open>Mechanism for retyping a range of memory to a non-constant array size.\<close>
definition
ptr_arr_retyps :: "nat \<Rightarrow> ('a :: c_type) ptr \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc"
where
definition ptr_arr_retyps :: "nat \<Rightarrow> ('a :: c_type) ptr \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc" where
"ptr_arr_retyps n p \<equiv>
htd_update_list (ptr_val p)
(map (\<lambda>i. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) i))
[0..<n * size_of TYPE('a)])"
[0..<n * size_of TYPE('a)])"
lemma ptr_arr_retyps_to_retyp:
"n = CARD('b :: finite)
\<Longrightarrow> ptr_arr_retyps n (p :: ('c :: wf_type) ptr) = ptr_retyp (ptr_coerce p :: ('c['b]) ptr)"
apply (rule ext)
apply (simp add: ptr_arr_retyps_def ptr_retyp_def typ_slices_def
typ_uinfo_array_tag_n_m_eq)
done
by (auto simp: ptr_arr_retyps_def ptr_retyp_def typ_slices_def typ_uinfo_array_tag_n_m_eq)
end

91
tools/c-parser/umm_heap/Arrays.thy
View File

@ -16,23 +16,19 @@ imports
"HOL-Library.Numeral_Type"
begin
definition
has_size :: "'a set \<Rightarrow> nat \<Rightarrow> bool" where
definition has_size :: "'a set \<Rightarrow> nat \<Rightarrow> bool" where
"has_size s n = (finite s \<and> card s = n)"
\<comment> \<open>If @{typ 'a} is not finite, there is no @{term "n < CARD('a)"}\<close>
definition
finite_index :: "nat \<Rightarrow> 'a::finite" where
definition finite_index :: "nat \<Rightarrow> 'a::finite" where
"finite_index = (SOME f. \<forall>x. \<exists>!n. n < CARD('a) \<and> f n = x)"
lemma card_image_inj[rule_format]:
"finite S \<Longrightarrow> (\<forall>x y. x \<in> S \<and> y \<in> S \<and> f x = f y \<longrightarrow> x = y) \<longrightarrow>
card (f ` S) = card S"
by (erule finite_induct) (auto simp add: card_insert_if)
lemma card_image_inj:
"\<lbrakk> finite S; \<And>x y. \<lbrakk> x \<in> S; y \<in> S; f x = f y \<rbrakk> \<Longrightarrow> x = y \<rbrakk> \<Longrightarrow> card (f ` S) = card S"
by (induct rule: finite_induct) (auto simp: card_insert_if)
lemma has_size_image_inj:
"\<lbrakk> has_size S n; (\<And>x y. x \<in> S \<and> y \<in> S \<and> f x = f y \<Longrightarrow> x = y) \<rbrakk>
\<Longrightarrow> has_size (f ` S) n"
"\<lbrakk> has_size S n; \<And>x y. x \<in> S \<and> y \<in> S \<and> f x = f y \<Longrightarrow> x = y \<rbrakk> \<Longrightarrow> has_size (f ` S) n"
by (simp add: has_size_def card_image_inj)
lemma has_size_0[simp]:
@ -40,15 +36,14 @@ lemma has_size_0[simp]:
by (auto simp: has_size_def)
lemma has_size_suc:
"has_size S (Suc n) =
(S \<noteq> {} \<and> (\<forall>a. a \<in> S \<longrightarrow> has_size (S - {a}) n))"
"has_size S (Suc n) = (S \<noteq> {} \<and> (\<forall>a. a \<in> S \<longrightarrow> has_size (S - {a}) n))"
unfolding has_size_def
by (metis Diff_empty Suc_not_Zero bot_least card_Suc_Diff1 card_gt_0_iff finite_Diff_insert
nat.inject neq0_conv subsetI subset_antisym)
lemma has_index:
"\<lbrakk> finite S; card S = n \<rbrakk> \<Longrightarrow>
(\<exists>f. (\<forall>m. m < n \<longrightarrow> f m \<in> S) \<and> (\<forall>x. x\<in>S \<longrightarrow> (\<exists>!m. m < n \<and> f m = x)))"
(\<exists>f. (\<forall>m. m < n \<longrightarrow> f m \<in> S) \<and> (\<forall>x. x\<in>S \<longrightarrow> (\<exists>!m. m < n \<and> f m = x)))"
proof (induct n arbitrary: S)
case 0 thus ?case by (auto simp: card_eq_0_iff)
next
@ -69,12 +64,14 @@ next
thus ?case by blast
qed
lemma finite_index_works[rule_format]:
"\<forall>i::'n. \<exists>!n. n < CARD('n::finite) \<and> finite_index n = i"
lemma finite_index_works:
"\<exists>!n. n < CARD('n::finite) \<and> finite_index n = (i::'n)"
proof -
have "\<exists>f::nat \<Rightarrow> 'n. \<forall>i. \<exists>!n. n < CARD('n) \<and> f n = i"
using has_index[where S = "UNIV :: 'n set"] by simp
thus ?thesis unfolding finite_index_def by (rule someI_ex)
hence "\<forall>i. \<exists>!n. n < CARD('n::finite) \<and> finite_index n = (i::'n)"
unfolding finite_index_def by (rule someI_ex)
thus ?thesis ..
qed
lemma finite_index_inj:
@ -83,7 +80,7 @@ lemma finite_index_inj:
using finite_index_works[where i = "finite_index j"] by blast
lemma forall_finite_index:
"(\<forall>k::('a::finite). P k) = (\<forall>i. i < CARD('a) \<longrightarrow> P (finite_index i))"
"(\<forall>k::'a::finite. P k) = (\<forall>i. i < CARD('a) \<longrightarrow> P (finite_index i))"
by (metis (mono_tags, hide_lams) finite_index_works)
@ -93,9 +90,7 @@ typedef ('a,'n::finite) array ("_[_]" [30,0] 31) = "UNIV :: ('n => 'a) set"
by simp
definition
index :: "('a,'n::finite) array \<Rightarrow> nat \<Rightarrow> 'a" ("_.[_]" [900,0] 901)
where
definition index :: "('a,'n::finite) array \<Rightarrow> nat \<Rightarrow> 'a" ("_.[_]" [900,0] 901) where
"index x i \<equiv> Rep_array x (finite_index i)"
theorem array_index_eq:
@ -111,19 +106,13 @@ lemma array_ext:
shows "(\<And>i. i < CARD('n) \<Longrightarrow> x.[i] = y.[i]) \<Longrightarrow> x = y"
by (simp add: array_index_eq)
definition FCP :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a['b::finite]" where
definition FCP :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a['b::finite]" (binder "ARRAY " 10) where
"FCP \<equiv> \<lambda>g. SOME a. \<forall>i. i < CARD('b) \<longrightarrow> a.[i] = g i"
notation FCP (binder "ARRAY " 10)
definition
update :: "'a['n::finite] \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a['n]"
where
definition update :: "'a['n::finite] \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a['n]" where
"update f i x \<equiv> FCP ((index f)(i := x))"
definition
fupdate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a['b::finite] \<Rightarrow> 'a['b]"
where
definition fupdate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a['b::finite] \<Rightarrow> 'a['b]" where
"fupdate i f x \<equiv> update x i (f (index x i))"
lemma fcp_beta[rule_format, simp]:
@ -138,27 +127,27 @@ proof (rule someI_ex)
qed
lemma fcp_unique:
"(ALL i. i < CARD('b::finite) --> (index f i = g i)) =
"(\<forall>i. i < CARD('b::finite) \<longrightarrow> index f i = g i) =
(FCP g = (f :: ('a,'b) array))"
by (fastforce simp: cart_eq)
lemma fcp_eta [simp]:
lemma fcp_eta[simp]:
"(ARRAY i. g.[i]) = g"
by (simp add: cart_eq)
lemma index_update [simp]:
lemma index_update[simp]:
"n < CARD('b::finite) \<Longrightarrow> index (update (f::'a['b]) n x) n = x"
by (simp add: update_def)
lemma index_update2 [simp]:
lemma index_update2[simp]:
"\<lbrakk> k < CARD('b::finite); n \<noteq> k \<rbrakk> \<Longrightarrow> index (update (f::'a['b]) n x) k = index f k"
by (simp add: update_def)
lemma update_update [simp]:
lemma update_update[simp]:
"update (update f n x) n y = update f n y"
by (simp add: cart_eq update_def)
lemma update_comm [simp]:
lemma update_comm[simp]:
"n \<noteq> m \<Longrightarrow> update (update f m v) n v' = update (update f n v') m v"
by (simp add: cart_eq update_def)
@ -166,40 +155,30 @@ lemma update_index_same [simp]:
"update v n (index v n) = v"
by (simp add: cart_eq update_def)
function
foldli0 :: "(nat \<Rightarrow> 'acc \<Rightarrow> 'a \<Rightarrow> 'acc) \<Rightarrow> 'acc \<Rightarrow> nat \<Rightarrow> 'a['index::finite] \<Rightarrow> 'acc"
where
function foldli0 :: "(nat \<Rightarrow> 'acc \<Rightarrow> 'a \<Rightarrow> 'acc) \<Rightarrow> 'acc \<Rightarrow> nat \<Rightarrow> 'a['index::finite] \<Rightarrow> 'acc" where
"foldli0 f a i arr = (if CARD('index) \<le> i then a else foldli0 f (f i a (index arr i)) (i+1) arr)"
by pat_completeness auto
termination
by (relation "measure (\<lambda>(f,a,i,(arr::'b['c::finite])). CARD('c) - i)") auto
definition
foldli :: "(nat => 'acc => 'a => 'acc) => 'acc => ('a,'i::finite) array => 'acc"
where
"foldli f a arr == foldli0 f a 0 arr"
definition foldli :: "(nat \<Rightarrow> 'acc \<Rightarrow> 'a \<Rightarrow> 'acc) \<Rightarrow> 'acc \<Rightarrow> ('a,'i::finite) array \<Rightarrow> 'acc" where
"foldli f a arr = foldli0 f a 0 arr"
(* for a traditional word presentation, with MSB on the left, you'd
want a fold that numbered in the reverse direction (with element 0
on the right rather than the left) *)
definition
map_array :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a['n::finite] \<Rightarrow> 'b['n]"
where
definition map_array :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a['n::finite] \<Rightarrow> 'b['n]" where
"map_array f a \<equiv> ARRAY i. f (a.[i])"
definition
map_array2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a['n::finite] \<Rightarrow> 'b['n] \<Rightarrow> 'c['n]"
where
definition map_array2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a['n::finite] \<Rightarrow> 'b['n] \<Rightarrow> 'c['n]" where
"map_array2 f a b \<equiv> ARRAY i. f (a.[i]) (b.[i])"
definition
definition zip_array :: "'a['b::finite] \<Rightarrow> 'c['b] \<Rightarrow> ('a \<times> 'c)['b]" where
"zip_array \<equiv> map_array2 Pair"
definition
list_array :: "('a,'n::finite) array \<Rightarrow> 'a list"
where
definition list_array :: "('a,'n::finite) array \<Rightarrow> 'a list" where
"list_array a = map (index a) [0..<CARD('n)]"
setup_lifting type_definition_array
@ -210,9 +189,7 @@ lemma set_array_list:
by (simp add: list_array_def index_def set_array.rep_eq image_def)
(metis atLeast0LessThan finite_index_works lessThan_iff)
definition
rel_array :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a['n::finite] \<Rightarrow> 'b['n] \<Rightarrow> bool"
where
definition rel_array :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a['n::finite] \<Rightarrow> 'b['n] \<Rightarrow> bool" where
"rel_array f a b \<equiv> \<forall>i < CARD('n). f (a.[i]) (b.[i])"
lemma map_array_index:
@ -230,7 +207,7 @@ lemma zip_array_index:
shows "n < CARD('n) \<Longrightarrow> (zip_array a b).[n] = (a.[n],b.[n])"
by (simp add: zip_array_def map_array2_index)
lemma map_array_id [simp]:
lemma map_array_id[simp]:
"map_array id = id"
by (auto simp: map_array_index array_ext)
@ -252,7 +229,7 @@ lemma in_set_array_index_conv:
by (metis in_set_conv_nth list_array_length list_array_nth nth_mem set_array_list)
lemma in_set_arrayE [elim!]:
"\<lbrakk> z \<in> set_array (a :: 'a['n::finite]); (\<And>n . \<lbrakk>n < CARD('n); z = a.[n]\<rbrakk> \<Longrightarrow> P) \<rbrakk> \<Longrightarrow> P"
"\<lbrakk> z \<in> set_array (a :: 'a['n::finite]); \<And>n . \<lbrakk>n < CARD('n); z = a.[n]\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
by (metis in_set_array_index_conv)
lemma map_array_setI:

221
tools/c-parser/umm_heap/ArraysMemInstance.thy
View File

@ -24,204 +24,114 @@ where
(\<lambda>x. index x n) (\<lambda>x f. update f n x) (replicate n CHR ''1'')
(array_tag_n n))::('a,'b::finite) array typ_info)"
definition
array_tag :: "('a::c_type,'b::finite) array itself \<Rightarrow> ('a,'b) array typ_info" where
definition array_tag :: "('a::c_type,'b::finite) array itself \<Rightarrow> ('a,'b) array typ_info" where
"array_tag t \<equiv> array_tag_n (CARD('b))"
instance array :: (c_type,finite) c_type ..
overloading typ_info_array \<equiv> typ_info_t begin
definition
typ_info_array: "typ_info_array (w::('a::c_type,'b::finite) array itself) \<equiv> array_tag w"
definition typ_info_array: "typ_info_array (w::('a::c_type,'b::finite) array itself) \<equiv> array_tag w"
end
lemma field_names_array_tag_length [rule_format]:
"x \<in> set (field_names_list (array_tag_n n)) \<longrightarrow> length x < n"
apply(induct_tac n)
apply simp
apply clarsimp
done
by (induct n) auto
lemma replicate_mem_field_names_array_tag [simp]:
"replicate n x \<notin> set (field_names_list (array_tag_n n))"
apply clarsimp
apply(drule field_names_array_tag_length)
apply simp
done
by (fastforce dest: field_names_array_tag_length)
lemma aggregate_array_tag [simp]:
"aggregate (array_tag_n n)"
apply(case_tac n)
apply simp+
done
by (cases n; simp)
lemma wf_desc_array_tag [simp]:
"wf_desc ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info)"
apply(induct_tac n)
apply simp+
apply(erule wf_desc_ti_typ_combine)
apply simp
done
by (induct n; simp) (fastforce elim: wf_desc_ti_typ_combine)
lemma wf_size_desc_array_tag [simp, rule_format]:
"0 < n \<longrightarrow> wf_size_desc ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info)"
apply(induct n)
apply simp+
apply(case_tac "n=0")
apply simp
apply(rule wf_size_desc_ti_typ_combine)
apply simp
done
lemma wf_size_desc_array_tag [simp]:
"0 < n \<Longrightarrow> wf_size_desc ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info)"
apply(induct n; simp)
apply(case_tac "n=0"; simp)
apply(rule wf_size_desc_ti_typ_combine)
apply simp
done
lemma g_ind_array_tag_udpate [simp]:
"n \<le> m \<longrightarrow> n \<le> CARD('b) \<longrightarrow>
g_ind (lf_set ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info) []) (\<lambda>x f. update f m x)"
apply(induct_tac n)
apply clarsimp+
apply(erule g_ind_ti_typ_combine)
apply clarsimp+
done
"\<lbrakk> n \<le> m; n \<le> CARD('b) \<rbrakk> \<Longrightarrow>
g_ind (lf_set ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info) []) (\<lambda>x f. update f m x)"
by (induct n; fastforce elim: g_ind_ti_typ_combine)
lemma fc_array_tag_udpate [simp]:
"n \<le> m \<longrightarrow> n \<le> CARD('b) \<longrightarrow>
fu_commutes (update_ti_t ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info)) (\<lambda>x f. update f m x)"
apply(induct_tac n)
apply clarsimp+
apply(erule fc_ti_typ_combine)
apply(clarsimp simp: fg_cons_def)
apply clarsimp+
done
"\<lbrakk> n \<le> m; n \<le> CARD('b) \<rbrakk> \<Longrightarrow>
fu_commutes (update_ti_t ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info)) (\<lambda>x f. update f m x)"
by (induct n; fastforce elim: fc_ti_typ_combine simp: fg_cons_def)
lemma f_ind_array_tag_udpate [simp, rule_format]:
"n \<le> m \<longrightarrow> m < CARD('b) \<longrightarrow>
f_ind (\<lambda>x. index x m) (lf_fd ` lf_set ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info) [])"
apply(induct_tac n)
apply clarsimp+
apply(erule f_ind_ti_typ_combine)
apply clarsimp
apply simp
done
lemma f_ind_array_tag_udpate [simp]:
"\<lbrakk> n \<le> m; m < CARD('b) \<rbrakk> \<Longrightarrow>
f_ind (\<lambda>x. index x m) (lf_fd ` lf_set ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info) [])"
by (induct n; fastforce elim: f_ind_ti_typ_combine)
lemma fa_fu_g_array_tag_udpate [simp, rule_format]:
"n \<le> m \<longrightarrow> m < CARD('b) \<longrightarrow>
fa_ind (lf_fd ` lf_set ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info) []) (\<lambda>x f. update f m x)"
apply(induct_tac n)
apply clarsimp+
apply(erule fa_ind_ti_typ_combine)
apply clarsimp+
done
lemma fa_fu_g_array_tag_udpate [simp]:
"\<lbrakk> n \<le> m; m < CARD('b) \<rbrakk> \<Longrightarrow>
fa_ind (lf_fd ` lf_set ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info) []) (\<lambda>x f. update f m x)"
by (induct n; fastforce elim: fa_ind_ti_typ_combine)
lemma wf_fdp_array_tag [simp, rule_format]:
"n \<le> CARD('b) \<longrightarrow>
wf_lf (lf_set ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info) [])"
apply(induct_tac n)
apply clarsimp+
apply(erule wf_lf_ti_typ_combine)
apply simp+
done
lemma wf_fdp_array_tag [simp]:
"n \<le> CARD('b) \<Longrightarrow> wf_lf (lf_set ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info) [])"
by (induct n; fastforce elim: wf_lf_ti_typ_combine)
lemma upd_local_update [simp]:
"upd_local (\<lambda>x f. update f n x)"
apply(auto simp: upd_local_def)
apply(subst cart_eq)
apply clarsimp
apply(subst (asm) cart_eq)
apply(drule_tac x=i in spec)
apply clarsimp
apply(case_tac "i=n")
apply simp+
done
unfolding upd_local_def
by (metis update_update)
lemma fu_eq_mask_array_tag [simp, rule_format]:
"n \<le> CARD('b) \<longrightarrow> (\<forall>m. (\<forall>k v. k < CARD('b) \<longrightarrow>
index ((m v)::('a,'b) array) k = (if n \<le> k then
index (undefined::('a::mem_type,'b::finite) array) k
else index v k)) \<longrightarrow> fu_eq_mask (array_tag_n n) m)"
apply(induct n)
apply clarsimp
apply(rule fu_eq_mask_empty_typ_info)
apply clarsimp
apply(subst cart_eq)
apply simp
apply clarsimp
apply(rule fu_eq_mask_ti_typ_combine)
apply(drule_tac x="\<lambda>v. update (m v) n (index undefined n)" in spec)
apply(erule impE)
apply clarsimp
apply(drule_tac x=k in spec)
apply clarsimp
apply(case_tac "k=n")
apply simp
apply clarsimp
apply(subgoal_tac "\<forall>v bs. m (update v n bs) = update (m v) n bs")
apply clarsimp+
apply(subst cart_eq)
apply clarsimp
apply(drule_tac x=i in spec)
apply clarsimp
apply(case_tac "i=n")
apply clarsimp+
apply(frule_tac x="update v n bs" in spec)
apply(drule_tac x="v" in spec)
apply clarsimp
apply(case_tac "Suc n \<le> i")
apply clarsimp+
apply(clarsimp simp: fg_cons_def)
apply(clarsimp)
apply simp
done
apply(induct n; clarsimp)
apply(rule fu_eq_mask_empty_typ_info)
apply(clarsimp simp: array_index_eq)
apply(rule fu_eq_mask_ti_typ_combine; clarsimp?)
apply(drule_tac x="\<lambda>v. update (m v) n (index undefined n)" in spec)
apply(erule impE)
apply clarsimp
apply(case_tac "k=n"; simp)
apply(subgoal_tac "\<forall>v bs. m (update v n bs) = update (m v) n bs"; clarsimp)
apply(clarsimp simp: array_index_eq)
apply(case_tac "i=n"; clarsimp)
apply(case_tac "Suc n \<le> i"; clarsimp)
apply(clarsimp simp: fg_cons_def)
done
lemma size_td_array_tag [simp]:
"size_td (((array_tag_n n)::('a,'b::finite) array typ_info)) =
n * size_of TYPE('a::c_type)"
apply(induct_tac n)
apply simp
apply simp
apply(simp add: size_td_lt_ti_typ_combine size_of_def)
done
by (induct n; simp add: size_td_lt_ti_typ_combine size_of_def)
lemma align_td_array_tag [rule_format]:
"0 < n \<longrightarrow> align_td ((array_tag_n n)::('a,'b::finite) array typ_info) = (align_td (typ_info_t (TYPE('a::c_type))))"
apply(induct_tac n)
apply simp
apply(clarsimp simp: ti_typ_combine_def Let_def)
apply(case_tac "n = 0")
apply(clarsimp simp: align_of_def max_def)+
done
lemma align_td_array_tag:
"0 < n \<Longrightarrow>
align_td ((array_tag_n n)::('a,'b::finite) array typ_info) = (align_td (typ_info_t (TYPE('a::c_type))))"
by (induct n; clarsimp)
(case_tac "n = 0"; clarsimp simp: align_of_def max_def)
lemma align_field_array [simp]:
"align_field ((array_tag_n n)::('a::mem_type,'b::finite) array typ_info)"
apply(induct_tac n)
apply simp
apply clarsimp
apply(erule align_field_ti_typ_combine)
apply simp
apply(rule dvd_mult)
apply(subgoal_tac "align_of TYPE('a) dvd size_of TYPE('a)")
apply(simp add: align_of_def)
apply(rule align_size_of)
done
by (induct_tac n; clarsimp)
(metis align_field_ti_typ_combine align_of_def align_size_of dvd_mult size_td_array_tag)
instance array :: (mem_type,finite) mem_type_sans_size
apply intro_classes
apply(simp_all add: typ_info_array array_tag_def size_of_def
norm_bytes_def)
apply clarsimp
apply(rule fu_eq_mask)
apply(simp add: size_of_def)
apply(rule fu_eq_mask_array_tag)
apply simp+
apply(clarsimp simp: align_of_def typ_info_array array_tag_def)
apply(subst align_td_array_tag)
apply simp
apply(rule dvd_trans)
apply(subgoal_tac "align_of TYPE('a) dvd size_of TYPE('a)")
apply(simp only: align_of_def)
apply(rule align_size_of)
apply(simp add: size_of_def)
done
apply intro_classes
apply(simp_all add: typ_info_array array_tag_def size_of_def norm_bytes_def)
apply clarsimp
apply(rule fu_eq_mask)
apply(simp add: size_of_def)
apply(rule fu_eq_mask_array_tag; simp)
apply (clarsimp simp: align_of_def typ_info_array array_tag_def align_td_array_tag)
apply (metis align_of_def align_size_of dvd_mult size_of_def)
done
declare atn_base [simp del]
declare atn_rec [simp del]
@ -236,9 +146,6 @@ lemma size_td_array:
lemma align_td_array:
"2^align_td (typ_info_t TYPE(('a,'b::finite) array)) = align_of TYPE('a::c_type)"
apply(simp add: align_of_def typ_info_array array_tag_def)
apply(subst align_td_array_tag)
apply simp+
done
by (simp add: align_of_def typ_info_array array_tag_def align_td_array_tag)
end

5
tools/c-parser/umm_heap/CTypes.thy
View File

@ -605,8 +605,7 @@ instantiation typ_desc :: (type) order
begin
instance
apply intro_classes
apply(auto simp: typ_tag_lt_def typ_tag_le_def)[1]
apply(auto dest!: td_set_size_lte)[1]
apply(fastforce simp: typ_tag_lt_def typ_tag_le_def dest: td_set_size_lte)
apply(rule sub_tag_refl)
apply(erule (1) sub_tag_trans)
apply(erule (1) sub_tag_antisym)
@ -1177,7 +1176,7 @@ lemma ti_ind_fn:
"\<forall>fn. ti_ind (lf_set_list ts fn) Y = ti_ind (lf_set_list ts []) Y"
"\<forall>fn. ti_ind (lf_set_pair x fn) Y = ti_ind (lf_set_pair x []) Y"
apply(induct t and st and ts and x, all \<open>clarsimp\<close>)
apply (auto simp: ti_ind_def)[1]
apply (fastforce simp: ti_ind_def)
apply auto
done

1185
tools/c-parser/umm_heap/CompoundCTypes.thy
View File

File diff suppressed because it is too large Load Diff

16
tools/c-parser/umm_heap/HeapRawState.thy
View File

@ -18,9 +18,7 @@ type_synonym typ_base = bool
datatype s_heap_index = SIndexVal | SIndexTyp nat
datatype s_heap_value = SValue byte | STyp "typ_uinfo \<times> typ_base"
primrec (nonexhaustive)
s_heap_tag :: "s_heap_value \<Rightarrow> typ_uinfo \<times> typ_base"
where
primrec (nonexhaustive) s_heap_tag :: "s_heap_value \<Rightarrow> typ_uinfo \<times> typ_base" where
"s_heap_tag (STyp t) = t"
type_synonym typ_slice = "nat \<rightharpoonup> typ_uinfo \<times> typ_base"
@ -39,18 +37,14 @@ type_synonym heap_raw_state = "heap_mem \<times> heap_typ_desc"
definition hrs_mem :: "heap_raw_state \<Rightarrow> heap_mem" where
"hrs_mem \<equiv> fst"
definition
hrs_mem_update :: "(heap_mem \<Rightarrow> heap_mem) \<Rightarrow> heap_raw_state \<Rightarrow> heap_raw_state"
where
definition hrs_mem_update :: "(heap_mem \<Rightarrow> heap_mem) \<Rightarrow> heap_raw_state \<Rightarrow> heap_raw_state" where
"hrs_mem_update f \<equiv> \<lambda>(h,d). (f h,d)"
definition hrs_htd :: "heap_raw_state \<Rightarrow> heap_typ_desc" where
"hrs_htd \<equiv> snd"
definition
hrs_htd_update :: "(heap_typ_desc \<Rightarrow> heap_typ_desc) \<Rightarrow> heap_raw_state
\<Rightarrow> heap_raw_state"
where
definition hrs_htd_update :: "(heap_typ_desc \<Rightarrow> heap_typ_desc) \<Rightarrow> heap_raw_state \<Rightarrow> heap_raw_state"
where
"hrs_htd_update f \<equiv> \<lambda>(h,d). (h,f d)"
@ -62,7 +56,6 @@ lemma hrs_htd_update_htd_update:
"(\<lambda>s. hrs_htd_update d (hrs_htd_update d' s)) = hrs_htd_update (d \<circ> d')"
by (simp add: hrs_htd_update_def split_def)
lemma hrs_htd_mem_update [simp]:
"hrs_htd (hrs_mem_update f s) = hrs_htd s"
by (simp add: hrs_mem_update_def hrs_htd_def split_def)
@ -81,5 +74,4 @@ lemma hrs_htd_update:
lemmas hrs_update = hrs_mem_update hrs_htd_update
end

50
tools/c-parser/umm_heap/Padding.thy
View File

@ -17,34 +17,34 @@ definition padup :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
lemma padup_dvd:
"0 < b \<Longrightarrow> (padup b n = 0) = (b dvd n)"
unfolding padup_def
apply(subst dvd_eq_mod_eq_0)
apply(subst mod_if [where m="b - n mod b"])
apply clarsimp
apply(insert mod_less_divisor [of b n])
apply arith
done
unfolding padup_def
apply(subst dvd_eq_mod_eq_0)
apply(subst mod_if [where m="b - n mod b"])
apply clarsimp
apply(insert mod_less_divisor [of b n])
apply arith
done
lemma dvd_padup_add:
"0 < x \<Longrightarrow> x dvd y + padup x y"
apply(clarsimp simp: padup_def)
apply(subst mod_if [where m="x - y mod x"])
apply(clarsimp split: if_split_asm)
apply(rule conjI)
apply clarsimp
apply(subst ac_simps)
apply(subst diff_add_assoc)
apply(rule mod_less_eq_dividend)
apply(rule dvd_add)
apply simp
apply(subst minus_div_mult_eq_mod[symmetric])
apply(subst diff_diff_right)
apply(subst ac_simps)
apply(subst minus_mod_eq_mult_div[symmetric])
apply simp
apply simp
apply(auto simp: dvd_eq_mod_eq_0)
done
apply(clarsimp simp: padup_def)
apply(subst mod_if [where m="x - y mod x"])
apply(clarsimp split: if_split_asm)
apply(rule conjI)
apply clarsimp
apply(subst ac_simps)
apply(subst diff_add_assoc)
apply(rule mod_less_eq_dividend)
apply(rule dvd_add)
apply simp
apply(subst minus_div_mult_eq_mod[symmetric])
apply(subst diff_diff_right)
apply(subst ac_simps)
apply(subst minus_mod_eq_mult_div[symmetric])
apply simp
apply simp
apply(auto simp: dvd_eq_mod_eq_0)
done
end

2253
tools/c-parser/umm_heap/SepCode.thy
View File

File diff suppressed because it is too large Load Diff

407
tools/c-parser/umm_heap/SepFrame.thy
View File

@ -37,65 +37,43 @@ translations
definition lift_hst :: "'a::heap_state_type' \<Rightarrow> heap_state" where
"lift_hst s \<equiv> lift_state (hst_mem s,hst_htd s)"
definition
point_eq_mod :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
where
definition point_eq_mod :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where
"point_eq_mod f g X \<equiv> \<forall>x. x \<notin> X \<longrightarrow> f x = g x"
definition
exec_fatal :: "('s,'b,'c) com \<Rightarrow> ('s,'b,'c) body \<Rightarrow> 's \<Rightarrow> bool"
where
"exec_fatal C \<Gamma> s \<equiv> (\<exists>f. \<Gamma> \<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> Fault f) \<or>
(\<Gamma> \<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> Stuck)"
definition exec_fatal :: "('s,'b,'c) com \<Rightarrow> ('s,'b,'c) body \<Rightarrow> 's \<Rightarrow> bool" where
"exec_fatal C \<Gamma> s \<equiv> (\<exists>f. \<Gamma> \<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> Fault f) \<or> (\<Gamma> \<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> Stuck)"
definition
restrict_htd :: "'s::heap_state_type' \<Rightarrow> s_addr set \<Rightarrow> 's"
where
definition restrict_htd :: "'s::heap_state_type' \<Rightarrow> s_addr set \<Rightarrow> 's" where
"restrict_htd s X \<equiv> s\<lparr> hst_htd := restrict_s (hst_htd s) X \<rparr>"
definition
restrict_safe_OK :: "'s \<Rightarrow> 's \<Rightarrow> ('s \<Rightarrow> ('s,'c) xstate) \<Rightarrow>
s_addr set \<Rightarrow> ('s::heap_state_type','b,'c) com \<Rightarrow> ('s,'b,'c) body \<Rightarrow> bool"
where
definition restrict_safe_OK ::
"'s \<Rightarrow> 's \<Rightarrow> ('s \<Rightarrow> ('s,'c) xstate) \<Rightarrow> s_addr set \<Rightarrow> ('s::heap_state_type','b,'c) com \<Rightarrow>
('s,'b,'c) body \<Rightarrow> bool" where
"restrict_safe_OK s t f X C \<Gamma> \<equiv>
\<Gamma> \<turnstile> \<langle>C,(Normal (restrict_htd s X))\<rangle> \<Rightarrow> f (restrict_htd t X) \<and>
point_eq_mod (lift_state (hst_mem t,hst_htd t))
(lift_state (hst_mem s,hst_htd s)) X"
point_eq_mod (lift_state (hst_mem t,hst_htd t)) (lift_state (hst_mem s,hst_htd s)) X"
definition
restrict_safe :: "'s \<Rightarrow> ('s,'c) xstate \<Rightarrow>
('s::heap_state_type','b,'c) com \<Rightarrow> ('s,'b,'c) body \<Rightarrow> bool"
where
"restrict_safe s t C \<Gamma> \<equiv> \<forall>X. (case t of
Normal t' \<Rightarrow> restrict_safe_OK s t' Normal X C \<Gamma> |
Abrupt t' \<Rightarrow> restrict_safe_OK s t' Abrupt X C \<Gamma> |
_ \<Rightarrow> False) \<or>
exec_fatal C \<Gamma> (restrict_htd s X)"
definition restrict_safe ::
"'s \<Rightarrow> ('s,'c) xstate \<Rightarrow> ('s::heap_state_type','b,'c) com \<Rightarrow> ('s,'b,'c) body \<Rightarrow> bool" where
"restrict_safe s t C \<Gamma> \<equiv>
\<forall>X. (case t of
Normal t' \<Rightarrow> restrict_safe_OK s t' Normal X C \<Gamma>
| Abrupt t' \<Rightarrow> restrict_safe_OK s t' Abrupt X C \<Gamma>
| _ \<Rightarrow> False) \<or>
exec_fatal C \<Gamma> (restrict_htd s X)"
definition
mem_safe :: "('s::{heap_state_type',type},'b,'c) com \<Rightarrow>
('s,'b,'c) body \<Rightarrow> bool"
where
"mem_safe C \<Gamma> \<equiv> \<forall>s t. \<Gamma> \<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> t \<longrightarrow>
restrict_safe s t C \<Gamma>"
definition mem_safe :: "('s::{heap_state_type',type},'b,'c) com \<Rightarrow> ('s,'b,'c) body \<Rightarrow> bool" where
"mem_safe C \<Gamma> \<equiv> \<forall>s t. \<Gamma> \<turnstile> \<langle>C,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> restrict_safe s t C \<Gamma>"
definition
point_eq_mod_safe :: "'s::{heap_state_type',type} set \<Rightarrow>
('s \<Rightarrow> 's) \<Rightarrow> ('s \<Rightarrow> s_addr \<Rightarrow> 'c) \<Rightarrow> bool"
where
"point_eq_mod_safe P f g \<equiv> \<forall>s X. restrict_htd s X \<in> P \<longrightarrow>
point_eq_mod (g (f s)) (g s) X"
definition point_eq_mod_safe ::
"'s::{heap_state_type',type} set \<Rightarrow> ('s \<Rightarrow> 's) \<Rightarrow> ('s \<Rightarrow> s_addr \<Rightarrow> 'c) \<Rightarrow> bool" where
"point_eq_mod_safe P f g \<equiv> \<forall>s X. restrict_htd s X \<in> P \<longrightarrow> point_eq_mod (g (f s)) (g s) X"
definition
comm_restrict :: "('s::{heap_state_type',type} \<Rightarrow> 's) \<Rightarrow> 's \<Rightarrow> s_addr set \<Rightarrow> bool"
where
definition comm_restrict :: "('s::{heap_state_type',type} \<Rightarrow> 's) \<Rightarrow> 's \<Rightarrow> s_addr set \<Rightarrow> bool" where
"comm_restrict f s X \<equiv> f (restrict_htd s X) = restrict_htd (f s) X"
definition
comm_restrict_safe :: "'s set \<Rightarrow> ('s::{heap_state_type',type} \<Rightarrow> 's) \<Rightarrow> bool"
where
"comm_restrict_safe P f \<equiv> \<forall>s X. restrict_htd s X \<in> P \<longrightarrow>
comm_restrict f s X"
definition comm_restrict_safe :: "'s set \<Rightarrow> ('s::{heap_state_type',type} \<Rightarrow> 's) \<Rightarrow> bool" where
"comm_restrict_safe P f \<equiv> \<forall>s X. restrict_htd s X \<in> P \<longrightarrow> comm_restrict f s X"
definition htd_ind :: "('a::{heap_state_type',type} \<Rightarrow> 'b) \<Rightarrow> bool" where
"htd_ind f \<equiv> \<forall>x s. f s = f (hst_htd_update x s)"
@ -139,9 +117,7 @@ begin
end
instance state_ext :: (heap_state_type,type) heap_state_type
apply intro_classes
apply auto
done
by intro_classes auto
primrec
intra_deps :: "('s','b,'c) com \<Rightarrow> 'b set"
@ -254,22 +230,19 @@ proof (rule, rule hoare_complete, simp only: valid_def, clarify)
show "ta \<in> Normal ` {t. (Q (g x t) \<and>\<^sup>* R (h x)) (lift_hst t)}"
proof (cases ta)
case (Normal s)
moreover with ev safe nofault have ev': "\<Gamma> \<turnstile>
moreover from this ev safe nofault have ev': "\<Gamma> \<turnstile>
\<langle>C,Normal (x\<lparr> hst_htd := (restrict_s (hst_htd x) (dom s\<^sub>0)) \<rparr>)\<rangle> \<Rightarrow>
Normal (s\<lparr> hst_htd := (restrict_s (hst_htd s) (dom s\<^sub>0)) \<rparr>)" and
"point_eq_mod (lift_state (hst_mem s,hst_htd s))
(lift_state (hst_mem x,hst_htd x)) (dom s\<^sub>0)"
by (auto simp: restrict_htd_def dest: mem_safe_NormalD)
moreover with m disj have "s\<^sub>1 = lift_hst s |` (UNIV - dom s\<^sub>0)"
apply -
apply(clarsimp simp: lift_hst_def)
apply(subst lift_state_point_eq_mod)
apply(drule sym)
apply clarsimp
apply fast
apply(simp add: lift_hst_def lift_state_point_eq_mod map_add_restrict)
apply(subst restrict_map_subdom, auto dest: map_disjD)
done
moreover from this m disj have "s\<^sub>1 = lift_hst s |` (UNIV - dom s\<^sub>0)"
apply(clarsimp simp: lift_hst_def)
apply(subst lift_state_point_eq_mod)
apply(fastforce dest: sym)
apply(simp add: lift_hst_def lift_state_point_eq_mod map_add_restrict)
apply(subst restrict_map_subdom, auto dest: map_disjD)
done
ultimately show ?thesis using orig_spec hi_f hi_g hi_g' pre_P pre_R m
by (force simp: cvalid_def valid_def image_def lift_hst_def
map_disj_def
@ -298,22 +271,22 @@ lemma sep_frame:
\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. (P (f \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (h \<acute>(\<lambda>x. x))) (lift_state (k \<acute>(\<lambda>x. x)))\<rbrace>
C
\<lbrace>(Q (g s \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (h s)) (lift_state (k \<acute>(\<lambda>x. x)))\<rbrace>"
apply(simp only:)
apply(fold lift_hst_def)
apply(erule (4) sep_frame')
done
apply(simp only:)
apply(fold lift_hst_def)
apply(erule (4) sep_frame')
done
lemma point_eq_mod_safe [simp]:
"\<lbrakk> point_eq_mod_safe P f g; restrict_htd s X \<in> P; x \<notin> X \<rbrakk> \<Longrightarrow>
g (f s) x = (g s) x"
apply (simp add: point_eq_mod_safe_def point_eq_mod_def)
apply(case_tac x, force)
done
apply(simp add: point_eq_mod_safe_def point_eq_mod_def)
apply(case_tac x, force)
done
lemma comm_restrict_safe [simp]:
"\<lbrakk> comm_restrict_safe P f; restrict_htd s X \<in> P \<rbrakk> \<Longrightarrow>
restrict_htd (f s ) X = f (restrict_htd s X)"
restrict_htd (f s ) X = f (restrict_htd s X)"
by (simp add: comm_restrict_safe_def comm_restrict_def)
lemma mono_guardD:
@ -436,17 +409,10 @@ next
intro: exec_other_intros)
next
case (Spec r s t) thus ?case
apply (clarsimp simp: mem_safe_def)
apply (fastforce intro: exec.Spec)
done
by (fastforce simp: mem_safe_def intro: exec.Spec)
next
case (SpecStuck r s) thus ?case
apply clarsimp
apply (erule_tac x=\<Gamma> in allE)
apply (simp add: mem_safe_def)
apply (erule allE, erule allE, erule impE, erule exec.SpecStuck)
apply assumption
done
by (simp add: exec.SpecStuck mem_safe_StuckD restrict_safe_def)
next
case (Seq C s sa D ta) show ?case
proof (cases sa)
@ -567,51 +533,40 @@ lemma mono_guard_triv2:
lemma dom_restrict_s:
"x \<in> dom_s (restrict_s d X) \<Longrightarrow> x \<in> dom_s d \<and> x \<in> X"
apply(auto simp: restrict_s_def dom_s_def split: if_split_asm)
done
by (auto simp: restrict_s_def dom_s_def split: if_split_asm)
lemma mono_guard_ptr_safe:
"\<lbrakk> \<And>s. d s = hst_htd (s::'a::heap_state_type); htd_ind p \<rbrakk> \<Longrightarrow>
mono_guard {s. ptr_safe (p s) (d s)}"
apply (auto simp: mono_guard_def ptr_safe_def restrict_htd_def )
apply(drule (1) subsetD)
apply(drule dom_restrict_s)
apply simp
done
by (auto simp: mono_guard_def ptr_safe_def restrict_htd_def dest: subsetD dom_restrict_s)
lemma point_eq_mod_safe_ptr_safe_update:
"\<lbrakk> d = (hst_htd::'a::heap_state_type \<Rightarrow> heap_typ_desc);
m = (\<lambda>s. hst_mem_update (heap_update (p s) ((v s)::'b::mem_type)) s);
h = hst_mem; k = (\<lambda>s. lift_state (h s,d s)); htd_ind p \<rbrakk> \<Longrightarrow>
point_eq_mod_safe {s. ptr_safe (p s) (d s)} m k"
apply (auto simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def heap_update_def
restrict_htd_def lift_state_def
intro!: heap_update_nmem_same split: s_heap_index.splits)
apply(subgoal_tac "(a,SIndexVal) \<in> s_footprint (p s)")
apply(drule (1) subsetD)
apply(drule dom_restrict_s, clarsimp)
apply(drule intvlD, clarsimp)
apply(erule s_footprintI2)
done
apply (clarsimp simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def heap_update_def
restrict_htd_def lift_state_def
intro!: heap_update_nmem_same
split: s_heap_index.splits)
apply(subgoal_tac "(a,SIndexVal) \<in> s_footprint (p s)")
apply(drule (1) subsetD)
apply(drule dom_restrict_s, clarsimp)
apply(drule intvlD, clarsimp)
apply(erule s_footprintI2)
done
lemma field_ti_s_sub_typ:
"field_lookup (export_uinfo (typ_info_t TYPE('b::mem_type))) f 0 = Some (typ_uinfo_t TYPE('a),b) \<Longrightarrow>
s_footprint ((Ptr &(p\<rightarrow>f))::'a::mem_type ptr) \<subseteq> s_footprint (p::'b ptr)"
apply(drule field_ti_s_sub)
apply(simp add: s_footprint_def)
done
by (drule field_ti_s_sub) (simp add: s_footprint_def)
lemma ptr_safe_mono:
"\<lbrakk> ptr_safe (p::'a::mem_type ptr) d; field_lookup (typ_info_t TYPE('a)) f 0
= Some (t,n); export_uinfo t = typ_uinfo_t TYPE('b) \<rbrakk> \<Longrightarrow>
ptr_safe ((Ptr &(p\<rightarrow>f))::'b::mem_type ptr) d"
apply(simp add: ptr_safe_def)
apply(drule field_lookup_export_uinfo_Some)
apply simp
apply(drule field_ti_s_sub_typ)
apply(erule (1) subset_trans)
done
unfolding ptr_safe_def
by (drule field_lookup_export_uinfo_Some) (auto dest: field_ti_s_sub_typ)
lemma point_eq_mod_safe_ptr_safe_update_fl:
"\<lbrakk> d = (hst_htd::'a::heap_state_type \<Rightarrow> heap_typ_desc);
@ -620,168 +575,95 @@ lemma point_eq_mod_safe_ptr_safe_update_fl:
field_lookup (typ_info_t TYPE('c)) f 0 = Some (t,n);
export_uinfo t = typ_uinfo_t TYPE('b) \<rbrakk> \<Longrightarrow>
point_eq_mod_safe {s. ptr_safe ((p::'a \<Rightarrow> 'c::mem_type ptr) s) (d s)} m k"
apply(drule (3) point_eq_mod_safe_ptr_safe_update)
apply(simp only: htd_ind_def)
apply clarify
apply(clarsimp simp: point_eq_mod_safe_def)
apply(drule_tac x=s in spec)
apply(drule_tac x=X in spec)
apply(erule impE)
apply(erule (2) ptr_safe_mono)
apply simp
done
apply(drule (3) point_eq_mod_safe_ptr_safe_update)
apply(fastforce simp: htd_ind_def)
apply(fastforce simp: point_eq_mod_safe_def intro!: ptr_safe_mono)
done
context
begin
private method m =
(clarsimp simp: ptr_retyp_d_eq_snd ptr_retyp_footprint list_map_eq,
erule notE,
drule intvlD, clarsimp,
(rule s_footprintI; assumption?),
subst (asm) unat_of_nat,
(subst (asm) mod_less; assumption?),
subst len_of_addr_card,
erule less_trans,
simp)
lemma point_eq_mod_safe_ptr_safe_tag:
"\<lbrakk> d = (hst_htd::'a::heap_state_type \<Rightarrow> heap_typ_desc); h = hst_mem;
m = (\<lambda>s. hst_htd_update (ptr_retyp (p s)) s);
k = (\<lambda>s. lift_state (h s,d s));
htd_ind p \<rbrakk> \<Longrightarrow>
point_eq_mod_safe {s. ptr_safe ((p s)::'b::mem_type ptr) (d s)} m k"
apply(auto simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def)
apply(subgoal_tac "(a,b) \<notin> s_footprint (p (restrict_htd s X))")
prefer 2
apply clarsimp
apply(drule (1) subsetD)
apply(clarsimp simp: restrict_htd_def)
apply(drule dom_restrict_s, clarsimp)
apply(thin_tac "P \<notin> Q" for P Q)
apply(auto simp: restrict_htd_def lift_state_def split_def split: s_heap_index.splits split: option.splits)
apply(subst (asm) ptr_retyp_d_eq_fst)
apply(clarsimp split: if_split_asm)
apply(erule notE)
apply(drule intvlD, clarsimp)
apply(erule s_footprintI2)
apply(subst (asm) ptr_retyp_d_eq_fst)
apply(clarsimp split: if_split_asm)
apply(subst (asm) ptr_retyp_d_eq_snd)
apply(clarsimp split: if_split_asm)
apply(subst (asm) ptr_retyp_d_eq_snd)
apply(clarsimp split: if_split_asm)
apply(erule notE)
apply(frule intvlD, clarsimp)
apply(rule s_footprintI)
apply(subst (asm) ptr_retyp_footprint)
apply simp
apply clarsimp
apply(clarsimp simp: list_map_eq split: if_split_asm)
apply(subst (asm) unat_of_nat)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply simp
apply fast
apply assumption
apply(simp add: ptr_retyp_d_eq_snd)
apply(clarsimp split: if_split_asm)
apply(simp add: ptr_retyp_footprint)
apply(clarsimp simp: list_map_eq split: if_split_asm)
apply(erule notE)
apply(drule intvlD, clarsimp)
apply(rule s_footprintI)
apply(subst (asm) unat_of_nat)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply simp
apply assumption+
apply(simp add: ptr_retyp_d_eq_snd)
apply(clarsimp split: if_split_asm)
apply(simp add: ptr_retyp_footprint)
apply(clarsimp simp: list_map_eq split: if_split_asm)
apply(erule notE)
apply(drule intvlD, clarsimp)
apply(rule s_footprintI)
apply(subst (asm) unat_of_nat)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply simp
apply assumption+
apply(simp add: ptr_retyp_d_eq_snd)
apply(clarsimp split: if_split_asm)
apply(simp add: ptr_retyp_footprint)
apply(clarsimp simp: list_map_eq split: if_split_asm)
apply(erule notE)
apply(drule intvlD, clarsimp)
apply(rule s_footprintI)
apply(subst (asm) unat_of_nat)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply simp
apply assumption+
done
m = (\<lambda>s. hst_htd_update (ptr_retyp (p s)) s);
k = (\<lambda>s. lift_state (h s,d s));
htd_ind p \<rbrakk> \<Longrightarrow>
point_eq_mod_safe {s. ptr_safe ((p s)::'b::mem_type ptr) (d s)} m k"
supply if_split_asm[split]
apply(clarsimp simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def)
apply(subgoal_tac "(a,b) \<notin> s_footprint (p (restrict_htd s X))")
prefer 2
apply(fastforce simp: restrict_htd_def dest: dom_restrict_s)
apply(clarsimp simp: restrict_htd_def lift_state_def split: s_heap_index.split option.splits)
apply (safe; m?)
apply(fastforce simp: ptr_retyp_d_eq_fst dest!: intvlD dest: s_footprintI2)
apply(fastforce simp: ptr_retyp_d_eq_fst)
apply(subst (asm) ptr_retyp_d_eq_snd, clarsimp)
done
end
lemma comm_restrict_safe_ptr_safe_tag:
fixes d::"'a::heap_state_type \<Rightarrow> heap_typ_desc"
assumes fun_d: "d = hst_htd" and fun_upd:
"m = (\<lambda>s. hst_htd_update (ptr_retyp (p s)) s)" and ind: "htd_ind p" and
upd: "\<And>d d' (s::'a). hst_htd_update (d s) (hst_htd_update (d' s) s) =
hst_htd_update ((d s) \<circ> (d' s)) s"
shows "comm_restrict_safe {s. ptr_safe ((p s)::'b::mem_type ptr) (d s)}
m"
assumes
fun_d: "d = hst_htd" and
fun_upd: "m = (\<lambda>s. hst_htd_update (ptr_retyp (p s)) s)" and
ind: "htd_ind p" and
upd: "\<And>d d' (s::'a).
hst_htd_update (d s) (hst_htd_update (d' s) s) = hst_htd_update ((d s) \<circ> (d' s)) s"
shows "comm_restrict_safe {s. ptr_safe ((p s)::'b::mem_type ptr) (d s)} m"
proof (simp only: comm_restrict_safe_def comm_restrict_def, auto)
fix s X
assume "ptr_safe (p (restrict_htd s X)) (d (restrict_htd s X))"
moreover from ind have p: "p (restrict_htd s X) = p s"
moreover from ind
have p: "p (restrict_htd s X) = p s"
by (simp add: restrict_htd_def)
ultimately have "ptr_retyp (p s) (restrict_s (hst_htd s) X) =
restrict_s (ptr_retyp (p s) (hst_htd s)) X" using fun_d
apply -
apply(rule ext)
apply(auto simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def)
apply(auto simp: restrict_htd_def )
apply(case_tac "x \<notin> {ptr_val (p s)..+size_of TYPE('b)}")
apply(subst ptr_retyp_d)
apply clarsimp
apply(clarsimp simp: restrict_map_def restrict_s_def)
apply(subst ptr_retyp_d)
apply clarsimp
apply simp
apply(subst ptr_retyp_d)
apply clarsimp
apply simp
apply clarsimp
apply(subst ptr_retyp_footprint)
apply fast
apply(clarsimp simp: restrict_map_def restrict_s_def)
apply(subst ptr_retyp_footprint)
apply fast
apply simp
apply(subst ptr_retyp_footprint)
apply fast
apply(rule)
apply(subgoal_tac "(x,SIndexVal) \<in> s_footprint (p s)")
apply(drule (1) subsetD)
apply(clarsimp simp: dom_s_def)
apply(drule intvlD, clarsimp)
apply(erule s_footprintI2)
apply(rule ext)
apply(clarsimp simp: map_add_def list_map_eq)
apply(subgoal_tac "(x,SIndexTyp y) \<in> s_footprint (p s)")
apply(drule (1) subsetD)
apply(clarsimp simp: dom_s_def split: if_split_asm)
apply(drule intvlD, clarsimp)
apply(rule s_footprintI)
apply(subst (asm) unat_simps)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply simp
apply assumption+
done
hence "((ptr_retyp (p s) \<circ> (%x _. x) (restrict_s (hst_htd s) X)::heap_typ_desc \<Rightarrow> heap_typ_desc) =
(%x _. x) (restrict_s (ptr_retyp (p s) (hst_htd s)) X))"
ultimately
have "ptr_retyp (p s) (restrict_s (hst_htd s) X) = restrict_s (ptr_retyp (p s) (hst_htd s)) X"
using fun_d
apply -
apply(rule ext)
apply(clarsimp simp: point_eq_mod_safe_def point_eq_mod_def ptr_safe_def restrict_htd_def)
apply(case_tac "x \<notin> {ptr_val (p s)..+size_of TYPE('b)}")
apply(clarsimp simp: ptr_retyp_d restrict_map_def restrict_s_def)
apply(subst ptr_retyp_d; simp)
apply(clarsimp simp: ptr_retyp_footprint restrict_map_def restrict_s_def)
apply(subst ptr_retyp_footprint, simp)
apply(rule conjI)
apply(subgoal_tac "(x,SIndexVal) \<in> s_footprint (p s)")
apply(fastforce simp: dom_s_def)
apply(fastforce dest: intvlD elim: s_footprintI2)
apply(rule ext)
apply(clarsimp simp: map_add_def list_map_eq)
apply(subgoal_tac "(x,SIndexTyp y) \<in> s_footprint (p s)")
apply(fastforce simp: dom_s_def split: if_split_asm)
apply(drule intvlD, clarsimp)
apply(rule s_footprintI; assumption?)
apply(metis len_of_addr_card less_trans max_size mod_less word_unat.eq_norm)
done
hence "((ptr_retyp (p s) \<circ> (\<lambda>x _. x) (restrict_s (hst_htd s) X)::heap_typ_desc \<Rightarrow> heap_typ_desc) =
(\<lambda>x _. x) (restrict_s (ptr_retyp (p s) (hst_htd s)) X))"
by - (rule ext, simp)
moreover from upd have "hst_htd_update (ptr_retyp (p s))
(hst_htd_update ((%x _. x) (restrict_s (hst_htd s) X)) s) =
hst_htd_update (((ptr_retyp (p s)) \<circ> ((%x _. x) (restrict_s (hst_htd s) X)))) s" .
moreover from upd have "hst_htd_update ((%x _. x) (restrict_s (ptr_retyp (p s) (hst_htd s)) X))
(hst_htd_update (ptr_retyp (p s)) s) =
hst_htd_update (((%x _. x) (restrict_s ((ptr_retyp (p s) (hst_htd s))) X)) \<circ> (ptr_retyp (p s)))
s" .
ultimately show "m (restrict_htd s X) =
restrict_htd (m s) X" using fun_d fun_upd upd p
(hst_htd_update ((\<lambda>x _. x) (restrict_s (hst_htd s) X)) s) =
hst_htd_update (((ptr_retyp (p s)) \<circ> ((\<lambda>x _. x) (restrict_s (hst_htd s) X)))) s" .
moreover from upd
have
"hst_htd_update ((\<lambda>x _. x) (restrict_s (ptr_retyp (p s) (hst_htd s)) X))
(hst_htd_update (ptr_retyp (p s)) s) =
hst_htd_update (((\<lambda>x _. x) (restrict_s ((ptr_retyp (p s) (hst_htd s))) X)) \<circ> (ptr_retyp (p s))) s" .
ultimately show "m (restrict_htd s X) = restrict_htd (m s) X" using fun_d fun_upd upd p
by (simp add: restrict_htd_def o_def)
qed
@ -820,7 +702,7 @@ lemma proc_deps_Cond [simp]:
"proc_deps (Cond P C D) \<Gamma> = proc_deps C \<Gamma> \<union> proc_deps D \<Gamma>"
proof
show "proc_deps (Cond P C D) \<Gamma> \<subseteq> proc_deps C \<Gamma> \<union> proc_deps D \<Gamma>"
by - (rule, erule proc_deps.induct, auto intro: proc_deps.intros)
by (rule, erule proc_deps.induct, auto intro: proc_deps.intros)
next
show "proc_deps C \<Gamma> \<union> proc_deps D \<Gamma> \<subseteq> proc_deps (Cond P C D) \<Gamma>"
by auto (erule proc_deps.induct, auto intro: proc_deps.intros)+
@ -842,7 +724,7 @@ lemma proc_deps_Catch [simp]:
"proc_deps (Catch C D) \<Gamma> = proc_deps C \<Gamma> \<union> proc_deps D \<Gamma>"
proof
show "proc_deps (Catch C D) \<Gamma> \<subseteq> proc_deps C \<Gamma> \<union> proc_deps D \<Gamma>"
by - (rule, erule proc_deps.induct, auto intro: proc_deps.intros)
by (rule, erule proc_deps.induct, auto intro: proc_deps.intros)
next
show "proc_deps C \<Gamma> \<union> proc_deps D \<Gamma> \<subseteq> proc_deps (Catch C D) \<Gamma>"
by auto (erule proc_deps.induct, auto intro: proc_deps.intros)+
@ -852,10 +734,10 @@ lemma proc_deps_Call [simp]:
"proc_deps (Call p) \<Gamma> = {p} \<union> (case \<Gamma> p of Some C \<Rightarrow>
proc_deps C (\<Gamma>(p := None)) | _ \<Rightarrow> {})" (is "?X = ?Y \<union> ?Z")
proof
note proc_deps.intros[intro]
show "?X \<subseteq> ?Y \<union> ?Z"
by - (rule, erule proc_deps.induct,
auto intro: proc_deps.intros,
case_tac "xa = p", auto intro: proc_deps.intros split: option.splits)
by (rule subsetI, erule proc_deps.induct, fastforce)
(rename_tac x D y, case_tac "x = p"; fastforce split: option.splits)
next
show "?Y \<union> ?Z \<subseteq> ?X"
proof (clarsimp, rule)
@ -863,19 +745,18 @@ next
next
show "?Z \<subseteq> ?X"
by (split option.splits, rule, force intro: proc_deps.intros)
(clarify, erule proc_deps.induct, (force intro: proc_deps.intros
split: if_split_asm)+)
(clarify, erule proc_deps.induct;
force intro: proc_deps.intros split: if_split_asm)
qed
qed
lemma proc_deps_DynCom [simp]:
"proc_deps (DynCom f) \<Gamma> = \<Union>{proc_deps (f s) \<Gamma> | s. True}"
by auto (erule proc_deps.induct, force intro: proc_deps.intros,
force intro: proc_deps.intros)+
by (rule equalityI; clarsimp; erule proc_deps.induct; force intro: proc_deps.intros)
lemma proc_deps_restrict:
"proc_deps C \<Gamma> \<subseteq> proc_deps C (\<Gamma>(p := None)) \<union> proc_deps (Call p) \<Gamma>"
proof rule
proof
fix xa
assume mem: "xa \<in> proc_deps C \<Gamma>"
hence "\<forall>p. xa \<in> proc_deps C (\<Gamma>(p := None)) \<union> proc_deps (Call p) \<Gamma>" (is "?X")

402
tools/c-parser/umm_heap/SepInv.thy
View File

@ -18,8 +18,8 @@ begin
to avoid all the duplication in here *)
definition inv_footprint :: "'a::c_type ptr \<Rightarrow> heap_assert" where
"inv_footprint p \<equiv> \<lambda>s. dom s = {(x,y). x \<in> {ptr_val p..+size_of TYPE('a)}} -
s_footprint p"
"inv_footprint p \<equiv>
\<lambda>s. dom s = {(x,y). x \<in> {ptr_val p..+size_of TYPE('a)}} - s_footprint p"
text \<open>
Like in Separation.thy, these arrows are defined using bsub and esub but
@ -28,8 +28,7 @@ text \<open>
\<close>
definition
sep_map_inv :: "'a::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> 'a \<Rightarrow> heap_assert"
("_ \<mapsto>\<^sup>i\<^bsub>_\<^esub> _" [56,0,51] 56)
sep_map_inv :: "'a::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> 'a \<Rightarrow> heap_assert" ("_ \<mapsto>\<^sup>i\<^bsub>_\<^esub> _" [56,0,51] 56)
where
"p \<mapsto>\<^sup>i\<^bsub>g\<^esub> v \<equiv> p \<mapsto>\<^sub>g v \<and>\<^sup>* inv_footprint p"
@ -37,8 +36,7 @@ notation (input)
sep_map_inv ("_ \<mapsto>\<^sup>i\<^sub>_ _" [56,1000,51] 56)
definition
sep_map_any_inv :: "'a ::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> heap_assert"
("_ \<mapsto>\<^sup>i\<^bsub>_\<^esub> -" [56,0] 56)
sep_map_any_inv :: "'a ::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> heap_assert" ("_ \<mapsto>\<^sup>i\<^bsub>_\<^esub> -" [56,0] 56)
where
"p \<mapsto>\<^sup>i\<^bsub>g\<^esub> - \<equiv> p \<mapsto>\<^sub>g - \<and>\<^sup>* inv_footprint p"
@ -46,8 +44,7 @@ notation (input)
sep_map_any_inv ("_ \<mapsto>\<^sup>i\<^sub>_ -" [56,0] 56)
definition
sep_map'_inv :: "'a::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> 'a \<Rightarrow> heap_assert"
("_ \<hookrightarrow>\<^sup>i\<^bsub>_\<^esub> _" [56,0,51] 56)
sep_map'_inv :: "'a::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> 'a \<Rightarrow> heap_assert" ("_ \<hookrightarrow>\<^sup>i\<^bsub>_\<^esub> _" [56,0,51] 56)
where
"p \<hookrightarrow>\<^sup>i\<^bsub>g\<^esub> v \<equiv> p \<hookrightarrow>\<^sub>g v \<and>\<^sup>* inv_footprint p"
@ -55,8 +52,7 @@ notation (input)
sep_map'_inv ("_ \<hookrightarrow>\<^sup>i\<^sub>_ _" [56,1000,51] 56)
definition
sep_map'_any_inv :: "'a::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> heap_assert"
("_ \<hookrightarrow>\<^sup>i\<^bsub>_\<^esub> -" [56,0] 56)
sep_map'_any_inv :: "'a::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> heap_assert" ("_ \<hookrightarrow>\<^sup>i\<^bsub>_\<^esub> -" [56,0] 56)
where
"p \<hookrightarrow>\<^sup>i\<^bsub>g\<^esub> - \<equiv> p \<hookrightarrow>\<^sub>g - \<and>\<^sup>* inv_footprint p"
@ -72,11 +68,7 @@ text \<open>----\<close>
lemma sep_map'_g:
"(p \<hookrightarrow>\<^sup>i\<^sub>g v) s \<Longrightarrow> g p"
apply(unfold sep_map'_inv_def)
apply(drule sep_conjD)
apply clarsimp
apply(erule sep_map'_g_exc)
done
unfolding sep_map'_inv_def by (fastforce dest: sep_conjD sep_map'_g_exc)
lemma sep_map'_unfold:
"(p \<hookrightarrow>\<^sup>i\<^sub>g v) = ((p \<hookrightarrow>\<^sup>i\<^sub>g v) \<and>\<^sup>* sep_true)"
@ -84,20 +76,20 @@ lemma sep_map'_unfold:
lemma sep_map'_any_unfold:
"(i \<hookrightarrow>\<^sup>i\<^sub>g -) = ((i \<hookrightarrow>\<^sup>i\<^sub>g -) \<and>\<^sup>* sep_true)"
apply(rule ext, simp add: sep_map'_any_inv_def sep_map'_any_def sep_conj_ac)
apply rule
apply(subst sep_conj_com)
apply(subst sep_conj_assoc)+
apply(erule (1) sep_conj_impl)
apply(clarsimp simp: sep_conj_ac)
apply(subst (asm) sep_map'_unfold_exc, subst sep_conj_com)
apply(subst sep_conj_exists, fast)
apply(subst (asm) sep_conj_com)
apply(subst (asm) sep_conj_assoc)+
apply(erule (1) sep_conj_impl)
apply(subst sep_map'_unfold_exc)
apply(subst (asm) sep_conj_exists, fast)
done
apply(rule ext, simp add: sep_map'_any_inv_def sep_map'_any_def sep_conj_ac)
apply(rule iffI)
apply(subst sep_conj_com)
apply(subst sep_conj_assoc)+
apply(erule (1) sep_conj_impl)
apply(clarsimp simp: sep_conj_ac)
apply(subst (asm) sep_map'_unfold_exc, subst sep_conj_com)
apply(subst sep_conj_exists, fast)
apply(subst (asm) sep_conj_com)
apply(subst (asm) sep_conj_assoc)+
apply(erule (1) sep_conj_impl)
apply(subst sep_map'_unfold_exc)
apply(subst (asm) sep_conj_exists, fast)
done
lemma sep_map'_conjE1:
"\<lbrakk> (P \<and>\<^sup>* Q) s; \<And>s. P s \<Longrightarrow> (i \<hookrightarrow>\<^sup>i\<^sub>g v) s \<rbrakk> \<Longrightarrow> (i \<hookrightarrow>\<^sup>i\<^sub>g v) s"
@ -117,125 +109,98 @@ lemma sep_map'_any_conjE2:
lemma sep_map_any_old:
"(p \<mapsto>\<^sup>i\<^sub>g -) = (\<lambda>s. \<exists>v. (p \<mapsto>\<^sup>i\<^sub>g v) s)"
apply(rule ext)
apply(simp add: sep_map_inv_def sep_map_any_inv_def sep_map_any_def sep_conj_ac)
apply(subst sep_conj_com)
apply(subst sep_conj_exists)
apply(simp add: sep_conj_com)
done
by (simp add: sep_map_inv_def sep_map_any_inv_def sep_map_any_def sep_conj_ac sep_conj_exists)
lemma sep_map'_old:
"(p \<hookrightarrow>\<^sup>i\<^sub>g v) = ((p \<mapsto>\<^sup>i\<^sub>g v) \<and>\<^sup>* sep_true)"
apply(rule ext)
apply(simp add: sep_map'_inv_def sep_map_inv_def sep_map'_def sep_conj_ac)
done
by (simp add: sep_map'_inv_def sep_map_inv_def sep_map'_def sep_conj_ac)
lemma sep_map'_any_old:
"(p \<hookrightarrow>\<^sup>i\<^sub>g -) = (\<lambda>s. \<exists>v. (p \<hookrightarrow>\<^sup>i\<^sub>g v) s)"
apply(rule ext)
apply(simp add: sep_map'_inv_def sep_map'_any_inv_def sep_map'_any_def sep_conj_exists)
done
by (simp add: sep_map'_inv_def sep_map'_any_inv_def sep_map'_any_def sep_conj_exists)
lemma sep_map_sep_map' [simp]:
"(p \<mapsto>\<^sup>i\<^sub>g v) s \<Longrightarrow> (p \<hookrightarrow>\<^sup>i\<^sub>g v) s"
apply(unfold sep_map_inv_def sep_map'_inv_def sep_map'_def)
apply(simp add: sep_conj_ac)
apply(subst sep_conj_com)
apply(subst sep_conj_assoc)+
apply(erule (1) sep_conj_impl)
apply(erule sep_conj_sep_true)
done
unfolding sep_map_inv_def sep_map'_inv_def sep_map'_def
apply(simp add: sep_conj_ac)
apply(subst sep_conj_com)
apply(simp add: sep_conj_assoc sep_conj_impl sep_conj_sep_true)
done
lemmas guardI = sep_map'_g[OF sep_map_sep_map']
lemma sep_map_anyI [simp]:
"(p \<mapsto>\<^sup>i\<^sub>g v) s \<Longrightarrow> (p \<mapsto>\<^sup>i\<^sub>g -) s"
apply(simp add: sep_map_any_inv_def sep_map_inv_def sep_map_any_def sep_conj_ac)
apply(erule (1) sep_conj_impl)
apply fast
done
by (fastforce simp: sep_map_any_inv_def sep_map_inv_def sep_map_any_def sep_conj_ac
elim: sep_conj_impl)
lemma sep_map_anyD:
"(p \<mapsto>\<^sup>i\<^sub>g -) s \<Longrightarrow> \<exists>v. (p \<mapsto>\<^sup>i\<^sub>g v) s"
apply(simp add: sep_map_any_def sep_map_any_inv_def sep_map_inv_def sep_conj_ac)
apply(subst (asm) sep_conj_com)
apply(subst (asm) sep_conj_exists)
apply(clarsimp simp: sep_conj_ac)
done
apply(simp add: sep_map_any_def sep_map_any_inv_def sep_map_inv_def sep_conj_ac)
apply(subst (asm) sep_conj_com)
apply(clarsimp simp: sep_conj_exists sep_conj_ac)
done
lemma sep_conj_mapD:
"((i \<mapsto>\<^sup>i\<^sub>g v) \<and>\<^sup>* P) s \<Longrightarrow> (i \<hookrightarrow>\<^sup>i\<^sub>g v) s \<and> ((i \<mapsto>\<^sup>i\<^sub>g -) \<and>\<^sup>* P) s"
apply rule
apply(rule sep_map'_conjE2)
apply (simp add:sep_conj_ac)+
apply(erule sep_conj_impl)
apply simp+
done
by (simp add: sep_conj_impl sep_map'_conjE2 sep_conj_ac)
lemma sep_map'_ptr_safe:
"(p \<hookrightarrow>\<^sup>i\<^sub>g (v::'a::mem_type)) (lift_state (h,d)) \<Longrightarrow> ptr_safe p d"
apply(unfold sep_map'_inv_def)
apply(rule sep_map'_ptr_safe_exc)
apply(subst sep_map'_unfold_exc)
apply(erule (1) sep_conj_impl)
apply simp
done
unfolding sep_map'_inv_def
apply(rule sep_map'_ptr_safe_exc)
apply(subst sep_map'_unfold_exc)
apply(fastforce elim: sep_conj_impl)
done
lemmas sep_map_ptr_safe = sep_map'_ptr_safe[OF sep_map_sep_map']
lemma sep_map_any_ptr_safe:
fixes p::"'a::mem_type ptr"
shows "(p \<mapsto>\<^sup>i\<^sub>g -) (lift_state (h, d)) \<Longrightarrow> ptr_safe p d"
apply(drule sep_map_anyD)
apply(blast intro:sep_map_ptr_safe)
done
by (blast dest: sep_map_anyD intro: sep_map_ptr_safe)
lemma sep_heap_update':
"(g \<turnstile>\<^sub>s\<^sup>i p \<and>\<^sup>* (p \<mapsto>\<^sup>i\<^sub>g v \<longrightarrow>\<^sup>* P)) (lift_state (h,d)) \<Longrightarrow>
P (lift_state (heap_update p (v::'a::mem_type) h,d))"
apply(rule_tac g=g in sep_heap_update'_exc)
apply(unfold tagd_inv_def)
apply(subst (asm) sep_conj_assoc)+
apply(erule (1) sep_conj_impl)
apply(subst (asm) sep_map_inv_def)
apply(simp add: sep_conj_ac)
apply(drule sep_conjD, clarsimp)
apply(rule sep_implI, clarsimp)
apply(drule sep_implD)
apply(drule_tac x="s\<^sub>0 ++ s'" in spec)
apply(simp add: map_disj_com map_add_disj)
apply(clarsimp simp: map_disj_com)
apply(erule notE)
apply(erule (1) sep_conjI)
apply(simp add: map_disj_com)
apply(subst map_add_com)
apply simp+
done
apply(rule_tac g=g in sep_heap_update'_exc)
apply(unfold tagd_inv_def)
apply(subst (asm) sep_conj_assoc)+
apply(erule (1) sep_conj_impl)
apply(subst (asm) sep_map_inv_def)
apply(simp add: sep_conj_ac)
apply(drule sep_conjD, clarsimp)
apply(rule sep_implI, clarsimp)
apply(drule sep_implD)
apply(drule_tac x="s\<^sub>0 ++ s'" in spec)
apply(simp add: map_disj_com map_add_disj)
apply(clarsimp simp: map_disj_com)
apply(erule notE)
apply(erule (1) sep_conjI)
apply(simp add: map_disj_com)
apply(subst map_add_com; simp)
done
lemma tagd_g:
"(g \<turnstile>\<^sub>s\<^sup>i p \<and>\<^sup>* P) s \<Longrightarrow> g p"
apply(unfold tagd_inv_def)
apply(auto simp: tagd_def dest!: sep_conjD)
apply(erule s_valid_g)
done
by (auto simp: tagd_inv_def tagd_def dest!: sep_conjD elim: s_valid_g)
lemma tagd_ptr_safe:
"(g \<turnstile>\<^sub>s\<^sup>i p \<and>\<^sup>* sep_true) (lift_state (h,d)) \<Longrightarrow> ptr_safe p d"
apply(rule tagd_ptr_safe_exc)
apply(unfold tagd_inv_def)
apply(subst (asm) sep_conj_assoc)
apply(erule (1) sep_conj_impl)
apply simp
done
apply(rule tagd_ptr_safe_exc)
apply(unfold tagd_inv_def)
apply(subst (asm) sep_conj_assoc)
apply(erule (1) sep_conj_impl)
apply simp
done
lemma sep_map_tagd:
"(p \<mapsto>\<^sup>i\<^sub>g (v::'a::mem_type)) s \<Longrightarrow> (g \<turnstile>\<^sub>s\<^sup>i p) s"
apply(unfold sep_map_inv_def)
apply(unfold tagd_inv_def)
apply(erule sep_conj_impl)
apply(erule sep_map_tagd_exc)
apply assumption
done
apply(unfold sep_map_inv_def tagd_inv_def)
apply(erule sep_conj_impl)
apply(erule sep_map_tagd_exc)
apply assumption
done
lemma sep_map_any_tagd:
"(p \<mapsto>\<^sup>i\<^sub>g -) s \<Longrightarrow> (g \<turnstile>\<^sub>s\<^sup>i (p::'a::mem_type ptr)) s"
@ -263,98 +228,83 @@ lemma sep_heap_update_global_super_fl_inv:
export_uinfo t = (typ_uinfo_t TYPE('a)) \<rbrakk> \<Longrightarrow>
((p \<mapsto>\<^sup>i\<^sub>g update_ti_t t (to_bytes_p v) u) \<and>\<^sup>* R)
(lift_state (heap_update (Ptr &(p\<rightarrow>f)) (v::'a::mem_type) h,d))"
apply(unfold sep_map_inv_def)
apply(simp only: sep_conj_assoc)
apply(erule (2) sep_heap_update_global_super_fl)
done
apply(unfold sep_map_inv_def)
apply(simp only: sep_conj_assoc)
apply(erule (2) sep_heap_update_global_super_fl)
done
lemma sep_map'_inv:
"(p \<hookrightarrow>\<^sup>i\<^sub>g v) s \<Longrightarrow> (p \<hookrightarrow>\<^sub>g v) s"
apply(unfold sep_map'_inv_def)
apply(subst sep_map'_unfold_exc)
apply(erule (1) sep_conj_impl, simp)
done
apply(unfold sep_map'_inv_def)
apply(subst sep_map'_unfold_exc)
apply(erule (1) sep_conj_impl, simp)
done
lemma sep_map'_lift:
"(p \<hookrightarrow>\<^sup>i\<^sub>g (v::'a::mem_type)) (lift_state (h,d)) \<Longrightarrow> lift h p = v"
apply(drule sep_map'_inv)
apply(erule sep_map'_lift_exc)
done
apply(drule sep_map'_inv)
apply(erule sep_map'_lift_exc)
done
lemma sep_map_lift:
"((p::'a::mem_type ptr) \<mapsto>\<^sup>i\<^sub>g -) (lift_state (h,d)) \<Longrightarrow>
(p \<mapsto>\<^sup>i\<^sub>g lift h p) (lift_state (h,d))"
apply(frule sep_map_anyD)
apply clarsimp
apply(frule sep_map_sep_map')
apply(drule sep_map'_lift)
apply simp
done
(p \<mapsto>\<^sup>i\<^sub>g lift h p) (lift_state (h,d))"
apply(frule sep_map_anyD)
apply clarsimp
apply(frule sep_map_sep_map')
apply(drule sep_map'_lift)
apply simp
done
lemma sep_map_lift_wp:
"\<lbrakk> \<exists>v. (p \<mapsto>\<^sup>i\<^sub>g v \<and>\<^sup>* (p \<mapsto>\<^sup>i\<^sub>g v \<longrightarrow>\<^sup>* P v)) (lift_state (h,d)) \<rbrakk>
\<Longrightarrow> P (lift h (p::'a::mem_type ptr)) (lift_state (h,d))"
apply clarsimp thm sep_map'_lift
apply(subst sep_map'_lift [where g=g and d=d])
apply(subst sep_map'_inv_def)
apply(subst sep_map'_def)
apply(subst sep_conj_assoc)+
apply(subst sep_conj_com[where P=sep_true])
apply(subst sep_conj_assoc [symmetric])
apply(erule sep_conj_impl)
apply clarsimp
apply(subst sep_map'_lift [where g=g and d=d])
apply(subst sep_map'_inv_def)
apply(subst sep_map'_def)
apply(subst sep_conj_assoc)+
apply(subst sep_conj_com[where P=sep_true])
apply(subst sep_conj_assoc [symmetric])
apply(erule sep_conj_impl)
apply(simp add: sep_map_inv_def)
apply simp
apply(rule_tac P="p \<mapsto>\<^sup>i\<^sub>g v" and Q="P v" in sep_conj_impl_same)
apply(unfold sep_map_inv_def)
apply assumption
apply simp
apply(rule_tac P="p \<mapsto>\<^sup>i\<^sub>g v" and Q="P v" in sep_conj_impl_same)
apply(unfold sep_map_inv_def)
apply(erule (2) sep_conj_impl)
done
apply(erule (2) sep_conj_impl)
done
lemma sep_map'_anyI [simp]:
"(p \<hookrightarrow>\<^sup>i\<^sub>g v) s \<Longrightarrow> (p \<hookrightarrow>\<^sup>i\<^sub>g -) s"
apply(unfold sep_map'_inv_def sep_map'_any_inv_def)
apply(erule sep_conj_impl)
apply(erule sep_map'_anyI_exc)
apply assumption
done
apply(unfold sep_map'_inv_def sep_map'_any_inv_def)
apply(erule sep_conj_impl)
apply(erule sep_map'_anyI_exc)
apply assumption
done
lemma sep_map'_anyD:
"(p \<hookrightarrow>\<^sup>i\<^sub>g -) s \<Longrightarrow> \<exists>v. (p \<hookrightarrow>\<^sup>i\<^sub>g v) s"
apply(unfold sep_map'_inv_def sep_map'_any_inv_def sep_map'_any_def)
apply(subst (asm) sep_conj_exists)
apply clarsimp
done
unfolding sep_map'_inv_def sep_map'_any_inv_def sep_map'_any_def
by (clarsimp simp: sep_conj_exists)
lemma sep_map'_lift_rev:
"\<lbrakk> lift h p = (v::'a::mem_type); (p \<hookrightarrow>\<^sup>i\<^sub>g -) (lift_state (h,d)) \<rbrakk> \<Longrightarrow>
(p \<hookrightarrow>\<^sup>i\<^sub>g v) (lift_state (h,d))"
apply(drule sep_map'_anyD)
apply clarsimp
apply(frule sep_map'_lift)
apply simp
done
by (fastforce dest: sep_map'_anyD simp: sep_map'_lift)
lemma sep_map'_any_g:
"(p \<hookrightarrow>\<^sup>i\<^sub>g -) s \<Longrightarrow> g p"
apply(drule sep_map'_anyD)
apply(blast intro:sep_map'_g)
done
by (blast dest: sep_map'_anyD intro: sep_map'_g)
lemma any_guardI:
"(p \<mapsto>\<^sup>i\<^sub>g -) s \<Longrightarrow> g p"
apply(drule sep_map_anyD)
apply(blast intro:guardI)
done
by (drule sep_map_anyD) (blast intro: guardI)
lemma sep_map_sep_map_any:
"(p \<mapsto>\<^sup>i\<^sub>g v) s \<Longrightarrow> (p \<mapsto>\<^sup>i\<^sub>g -) s"
apply(simp)
done
by (rule sep_map_anyI)
(* FIXME: can be made more flexible when generalised separation conjunction
is added
lsf: should be fine with sep_select_tac
*)
lemma sep_lift_exists:
fixes p :: "'a::mem_type ptr"
assumes ex: "((\<lambda>s. \<exists>v. (p \<hookrightarrow>\<^sup>i\<^sub>g v) s \<and> P v s) \<and>\<^sup>* Q) (lift_state (h,d))"
@ -370,32 +320,18 @@ qed
lemma sep_map_dom:
"(p \<mapsto>\<^sup>i\<^sub>g (v::'a::c_type)) s \<Longrightarrow> dom s = {(a,b). a \<in> {ptr_val p..+size_of TYPE('a)}}"
apply(unfold sep_map_inv_def)
apply(drule sep_conjD, clarsimp)
apply(drule sep_map_dom_exc)
apply(clarsimp simp: inv_footprint_def)
apply auto
apply(erule s_footprintD)
done
unfolding sep_map_inv_def
by (drule sep_conjD, clarsimp)
(auto dest!: sep_map_dom_exc elim: s_footprintD simp: inv_footprint_def)
lemma sep_map'_dom:
"(p \<hookrightarrow>\<^sup>i\<^sub>g (v::'a::mem_type)) s \<Longrightarrow> (ptr_val p,SIndexVal) \<in> dom s"
apply(unfold sep_map'_inv_def)
apply(drule sep_conjD, clarsimp)
apply(drule sep_map'_dom_exc, clarsimp)
done
unfolding sep_map'_inv_def
by (drule sep_conjD, clarsimp) (drule sep_map'_dom_exc, clarsimp)
lemma sep_map'_inj:
"\<lbrakk> (p \<hookrightarrow>\<^sup>i\<^sub>g (v::'a::c_type)) s; (p \<hookrightarrow>\<^sup>i\<^sub>h v') s \<rbrakk> \<Longrightarrow> v=v'"
apply(drule sep_map'_inv)+
apply(drule (2) sep_map'_inj_exc)
done
lemma ptr_retyp_tagd:
"\<lbrakk> g (p::'a::mem_type ptr); {(a, b). a \<in> {ptr_val p..+size_of TYPE('a)}} \<subseteq> dom_s d \<rbrakk> \<Longrightarrow>
(g \<turnstile>\<^sub>s\<^sup>i p) (lift_state (h, ptr_retyp p d))"
apply(simp add: tagd_inv_def tagd_def ptr_retyp_s_valid lift_state_dom)
oops
by (drule sep_map'_inv)+ (drule (2) sep_map'_inj_exc)
lemma ptr_retyp_sep_cut':
fixes p::"'a::mem_type ptr"
@ -403,86 +339,58 @@ lemma ptr_retyp_sep_cut':
(lift_state (h,d))" and "g p"
shows "(g \<turnstile>\<^sub>s\<^sup>i p \<and>\<^sup>* P) (lift_state (h,(ptr_retyp p d)))"
proof -
from sc obtain s\<^sub>0 and s\<^sub>1 where "s\<^sub>0 \<bottom> s\<^sub>1" and "lift_state (h,d) = s\<^sub>1 ++ s\<^sub>0"
from sc
obtain s\<^sub>0 and s\<^sub>1
where "s\<^sub>0 \<bottom> s\<^sub>1" and "lift_state (h,d) = s\<^sub>1 ++ s\<^sub>0"
and "P s\<^sub>1" and d: "dom s\<^sub>0 = {(a,b). a \<in> {ptr_val p..+size_of TYPE('a)}}"
and k: "dom s\<^sub>0 \<subseteq> dom_s d"
apply -
apply(drule sep_conjD)
apply clarsimp
apply(drule sep_cut'_dom)
apply(subgoal_tac "dom s\<^sub>0 \<subseteq> dom_s d")
apply fast
apply(subst dom_lift_state_dom_s [where h=h,symmetric])
apply auto
done
moreover hence "lift_state (h, ptr_retyp p d) = s\<^sub>1 ++
lift_state (h, ptr_retyp p d) |` (dom s\<^sub>0)"
apply -
apply(rule ext, case_tac "x \<in> dom s\<^sub>0")
apply(case_tac "x \<in> dom s\<^sub>1")
apply(clarsimp simp: map_disj_def)
apply fast
apply(subst map_add_com)
apply(clarsimp simp: map_disj_def)
apply fast
apply(clarsimp simp: map_add_def split: option.splits)
apply(case_tac x, clarsimp)
apply(clarsimp simp: lift_state_ptr_retyp_d merge_dom2)
done
by (auto dest!: sep_conjD sep_cut'_dom simp: dom_lift_state_dom_s [where h=h,symmetric])
moreover from this
have "lift_state (h, ptr_retyp p d) = s\<^sub>1 ++ lift_state (h, ptr_retyp p d) |` (dom s\<^sub>0)"
apply -
apply(rule ext, rename_tac x)
apply(case_tac "x \<in> dom s\<^sub>0")
apply(case_tac "x \<in> dom s\<^sub>1")
apply(fastforce simp: map_disj_def)
apply(subst map_add_com)
apply(fastforce simp: map_disj_def)
apply(clarsimp simp: map_add_def split: option.splits)
apply(case_tac x, clarsimp)
apply(clarsimp simp: lift_state_ptr_retyp_d merge_dom2)
done
moreover have "g p" by fact
with d k have "(g \<turnstile>\<^sub>s\<^sup>i p) (lift_state (h, ptr_retyp p d) |` dom s\<^sub>0)"
apply -
apply(auto simp: lift_state_ptr_retyp_restrict sep_conj_ac)
apply(unfold tagd_inv_def)
apply(simp add: sep_conj_ac)
apply(rule_tac s\<^sub>0="lift_state (h,d) |` ({(a, b). a \<in> {ptr_val p..+size_of TYPE('a)}} - s_footprint p)" in sep_conjI)
apply(clarsimp simp: inv_footprint_def)
apply fast
apply(erule_tac h=h in ptr_retyp_tagd_exc)
apply(clarsimp simp: map_disj_def)
apply fast
apply(subst map_add_comm[of "lift_state (h, ptr_retyp p empty_htd)"])
apply(simp, fast)
apply(rule ext)
apply(clarsimp simp: map_add_def split: option.splits)
apply(subgoal_tac "(a,b) \<notin> s_footprint p")
apply(clarsimp simp: restrict_map_def)
apply(subgoal_tac "s_footprint p = dom (lift_state (h, ptr_retyp p empty_htd) )")
apply(simp only:)
apply fast
apply simp
done
apply(clarsimp simp: lift_state_ptr_retyp_restrict sep_conj_ac tagd_inv_def)
apply(rule_tac s\<^sub>0="lift_state (h,d) |` ({(a, b). a \<in> {ptr_val p..+size_of TYPE('a)}} - s_footprint p)"
in sep_conjI)
apply(fastforce simp: inv_footprint_def)
apply(erule_tac h=h in ptr_retyp_tagd_exc)
apply(fastforce simp: map_disj_def)
apply(subst map_add_comm[of "lift_state (h, ptr_retyp p empty_htd)"])
apply force
apply(rule ext)
apply(clarsimp simp: map_add_def split: option.splits)
by (metis (mono_tags) Diff_iff dom_ptr_retyp_empty_htd non_dom_eval_eq restrict_in_dom restrict_out)
ultimately show ?thesis
apply -
apply(rule_tac s\<^sub>0="(lift_state (h,ptr_retyp p d))|`dom s\<^sub>0" and s\<^sub>1=s\<^sub>1 in
sep_conjI, auto simp: map_disj_def)
done
by - (rule_tac s\<^sub>0="(lift_state (h,ptr_retyp p d))|`dom s\<^sub>0" and s\<^sub>1=s\<^sub>1 in sep_conjI,
auto simp: map_disj_def)
qed
lemma ptr_retyp_sep_cut'_wp:
"\<lbrakk> (sep_cut' (ptr_val p) (size_of TYPE('a)) \<and>\<^sup>* (g \<turnstile>\<^sub>s\<^sup>i p \<longrightarrow>\<^sup>* P))
(lift_state (h,d)); g (p::'a::mem_type ptr) \<rbrakk>
\<Longrightarrow> P (lift_state (h,(ptr_retyp p d)))"
apply(rule_tac P="g \<turnstile>\<^sub>s\<^sup>i p" and Q=P in sep_conj_impl_same)
apply(rule ptr_retyp_sep_cut')
apply simp+
done
by (rule_tac P="g \<turnstile>\<^sub>s\<^sup>i p" and Q=P in sep_conj_impl_same) (simp add: ptr_retyp_sep_cut')
lemma tagd_dom:
"(g \<turnstile>\<^sub>s\<^sup>i p) s \<Longrightarrow> dom s = {(a,b). a \<in> {ptr_val (p::'a::c_type ptr)..+size_of TYPE('a)}}"
apply (clarsimp simp: tagd_inv_def)
apply(drule sep_conjD, clarsimp)
apply(clarsimp simp: inv_footprint_def)
apply(drule tagd_dom_exc)
apply auto
apply(erule s_footprintD)
done
unfolding tagd_inv_def
by (drule sep_conjD, clarsimp)
(auto simp: inv_footprint_def dest!: tagd_dom_exc elim: s_footprintD)
lemma tagd_dom_p:
"(g \<turnstile>\<^sub>s\<^sup>i p) s \<Longrightarrow> (ptr_val (p::'a::mem_type ptr),SIndexVal) \<in> dom s"
apply(drule tagd_dom)
apply(clarsimp)
done
by (drule tagd_dom) clarsimp
end

40
tools/c-parser/umm_heap/SepTactic.thy
View File

@ -37,16 +37,16 @@ lemma sep_conj_extract_assoc:
lemma sep_conj_extract_decomposeD:
"(sep_conj_extract (P \<and>\<^sup>* Q) \<and>\<^sup>* sep_true) s \<Longrightarrow> sep_points P s \<and>
(sep_conj_extract Q \<and>\<^sup>* sep_true) s"
apply (rule conjI)
apply(simp add: sep_conj_extract_def sep_points_def sep_conj_ac)
apply(erule (1) sep_conj_impl, simp)
apply(simp add: sep_conj_extract_def sep_conj_ac)
apply(subst (asm) sep_conj_assoc [symmetric])
apply(subst (asm) sep_conj_com)
apply(subst (asm) sep_conj_assoc)
apply(erule (1) sep_conj_impl)
apply simp
done
apply (rule conjI)
apply(simp add: sep_conj_extract_def sep_points_def sep_conj_ac)
apply(erule (1) sep_conj_impl, simp)
apply(simp add: sep_conj_extract_def sep_conj_ac)
apply(subst (asm) sep_conj_assoc [symmetric])
apply(subst (asm) sep_conj_com)
apply(subst (asm) sep_conj_assoc)
apply(erule (1) sep_conj_impl)
apply simp
done
lemma sep_conj_extract_decomposeD2:
"(sep_conj_extract P \<and>\<^sup>* sep_true) s \<Longrightarrow> sep_points P s"
@ -222,21 +222,21 @@ method_setup sep_select_tac =
lemma
"\<And>R x f n. ((P::heap_assert) \<and>\<^sup>* fac x n \<and>\<^sup>* R (f x)) s"
apply(sep_select_tac "fac _ _")
apply(sep_select_tac "R _")
apply(sep_select_tac "fac x _")
apply(sep_select_tac "R _")
oops
apply(sep_select_tac "fac _ _")
apply(sep_select_tac "R _")
apply(sep_select_tac "fac x _")
apply(sep_select_tac "R _")
oops
lemma
"((P::heap_assert) \<and>\<^sup>* fac x n) s"
apply(sep_select_tac "fac _ _")
oops
apply(sep_select_tac "fac _ _")
oops
lemma
"((P::heap_assert) \<and>\<^sup>* long_name) s"
apply(sep_select_tac "long_name")
oops
oops
consts c_guard :: "'a::c_type ptr_guard"
@ -340,8 +340,8 @@ method_setup sep_wp_tac =
(* see testfiles/sep_example_pre_list.thy for a more detailed example *)
lemma
"((\<lambda>z. lift (hrs_mem s) (p::(32 word) ptr) + 1 = 2) \<and>\<^sup>* P) (lift_state s)"
apply sep_wp_tac
oops
apply sep_wp_tac
oops
end

540
tools/c-parser/umm_heap/Separation.thy
View File

@ -29,14 +29,12 @@ definition sep_false :: "('a,'b) map_assert" where
"sep_false \<equiv> \<lambda>s. False"
definition
sep_conj :: "('a,'b) map_assert \<Rightarrow> ('a,'b) map_assert \<Rightarrow> ('a,'b) map_assert"
(infixr "\<and>\<^sup>*" 35)
sep_conj :: "('a,'b) map_assert \<Rightarrow> ('a,'b) map_assert \<Rightarrow> ('a,'b) map_assert" (infixr "\<and>\<^sup>*" 35)
where
"P \<and>\<^sup>* Q \<equiv> \<lambda>s. \<exists>s\<^sub>0 s\<^sub>1. s\<^sub>0 \<bottom> s\<^sub>1 \<and> s = s\<^sub>1 ++ s\<^sub>0 \<and> P s\<^sub>0 \<and> Q s\<^sub>1"
definition
sep_impl :: "('a,'b) map_assert \<Rightarrow> ('a,'b) map_assert \<Rightarrow> ('a,'b) map_assert"
(infixr "\<longrightarrow>\<^sup>*" 25)
sep_impl :: "('a,'b) map_assert \<Rightarrow> ('a,'b) map_assert \<Rightarrow> ('a,'b) map_assert" (infixr "\<longrightarrow>\<^sup>*" 25)
where
"x \<longrightarrow>\<^sup>* y \<equiv> \<lambda>s. \<forall>s'. s \<bottom> s' \<and> x s' \<longrightarrow> y (s ++ s')"
@ -55,8 +53,7 @@ text \<open>
\<close>
definition
sep_map :: "'a::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> 'a \<Rightarrow> heap_assert"
("_ \<mapsto>\<^bsub>_\<^esub> _" [56,0,51] 56)
sep_map :: "'a::c_type ptr \<Rightarrow> 'a ptr_guard \<Rightarrow> 'a \<Rightarrow> heap_assert" ("_ \<mapsto>\<^bsub>_\<^esub> _" [56,0,51] 56)
where
"p \<mapsto>\<^bsub>g\<^esub> v \<equiv> \<lambda>s. lift_typ_heap g s p = Some v \<and> dom s = s_footprint p \<and> wf_heap_val s"
@ -113,143 +110,104 @@ declare sep_false_def [symmetric, simp add]
lemma singleton_dom':
"dom (singleton p (v::'a::mem_type) h d) = dom (lift_state (h,d)) \<inter> s_footprint p"
apply(auto simp: singleton_def lift_state_def
by (auto simp: singleton_def lift_state_def
split: if_split_asm s_heap_index.splits)
done
lemma lift_state_dom:
"d,g \<Turnstile>\<^sub>t p \<Longrightarrow> s_footprint (p::'a::mem_type ptr) \<subseteq> dom (lift_state (h,d))"
apply(clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
apply(auto simp: lift_state_def split: s_heap_index.splits option.splits)
apply(drule s_footprintD)
apply(drule intvlD, clarsimp simp: size_of_def)
apply(frule s_footprintD2)
apply(rename_tac nat)
apply(drule s_footprintD)
apply(drule intvlD, clarsimp)
apply(drule_tac x=k in spec)
apply(erule impE)
apply(simp add: size_of_def)
apply(subst (asm) word_unat.eq_norm)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply(rule max_size)
apply(simp add: map_le_def)
apply auto
apply(drule_tac x=nat in bspec)
apply clarsimp+
done
apply(clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
apply(clarsimp simp: lift_state_def split: s_heap_index.splits option.splits)
apply(rule conjI; clarsimp)
apply(fastforce dest: s_footprintD intvlD simp: size_of_def)
apply(frule s_footprintD2)
apply(drule s_footprintD)
apply(drule intvlD, clarsimp)
apply(rename_tac k)
apply(drule_tac x=k in spec)
apply(erule impE)
apply(simp add: size_of_def)
apply(subst (asm) word_unat.eq_norm)
apply(subst (asm) mod_less)
apply(subst len_of_addr_card)
apply(erule less_trans)
apply(rule max_size)
apply(force simp: map_le_def)
done
lemma singleton_dom:
"d,g \<Turnstile>\<^sub>t p \<Longrightarrow> dom (singleton p (v::'a::mem_type) h d) = s_footprint p"
apply(subst singleton_dom')
apply(drule lift_state_dom)
apply fast
done
apply(subst singleton_dom')
apply(fastforce dest: lift_state_dom)
done
lemma wf_heap_val_restrict [simp]:
"wf_heap_val s \<Longrightarrow> wf_heap_val (s |` X)"
apply(unfold wf_heap_val_def, clarify)
apply(auto simp: restrict_map_def)
done
unfolding wf_heap_val_def by (auto simp: restrict_map_def)
lemma singleton_wf_heap_val [simp]:
"wf_heap_val (singleton p v h d)"
apply(unfold singleton_def)
apply simp
done
unfolding singleton_def by simp
lemma h_t_valid_restrict_proj_d:
"\<lbrakk> proj_d s,g \<Turnstile>\<^sub>t p; \<forall>x. x \<in> s_footprint p \<longrightarrow> s x = s' x \<rbrakk> \<Longrightarrow>
proj_d s',g \<Turnstile>\<^sub>t p"
apply(auto simp: h_t_valid_def valid_footprint_def Let_def)
apply(drule_tac x=y in spec)
apply simp
apply(auto simp: proj_d_def map_le_def split: if_split_asm option.splits)
apply(clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
apply(rule conjI)
apply(drule_tac x=y in spec)
apply simp
apply(clarsimp simp: proj_d_def map_le_def)
apply(drule_tac x="ptr_val p + of_nat y" in spec)
apply(drule_tac x="SIndexTyp a" in spec)
apply(erule impE)
apply(erule s_footprintI)
apply(simp add: size_of_def)
apply simp
apply(clarsimp simp: proj_d_def)
apply(drule_tac x=y in spec)
apply clarsimp
apply(drule_tac x="ptr_val p + of_nat y" in spec)
apply(drule_tac x="SIndexTyp a" in spec)
apply(drule_tac x="SIndexVal" in spec)
apply(erule impE)
apply(erule s_footprintI)
apply(rule s_footprintI2)
apply(simp add: size_of_def)
apply simp
apply(drule_tac x="ptr_val p + of_nat y" in spec)
apply(drule_tac x="SIndexTyp a" in spec)
apply(erule impE)
apply(erule s_footprintI)
apply(simp add: size_of_def)
apply simp
apply(drule_tac x=y in spec)
apply clarsimp
apply(drule_tac x="ptr_val p + of_nat y" in spec)
apply(drule_tac x="SIndexVal" in spec)
apply(erule impE)
apply(rule s_footprintI2)
apply(simp add: size_of_def)
apply(rule_tac x=ya in exI)
apply simp
done
apply force
done
lemma s_valid_restrict [simp]:
"s |` s_footprint p,g \<Turnstile>\<^sub>s p = s,g \<Turnstile>\<^sub>s p"
apply(auto simp: s_valid_def )
apply(erule h_t_valid_restrict_proj_d)
apply(simp add: s_footprint_restrict)
apply(erule h_t_valid_restrict_proj_d)
apply(simp add: s_footprint_restrict)
done
by (fastforce simp: s_valid_def elim: h_t_valid_restrict_proj_d)
lemma proj_h_restrict:
"(x,SIndexVal) \<in> X \<Longrightarrow> proj_h (s |` X) x = proj_h s x"
apply(auto simp: proj_h_def)
done
by (auto simp: proj_h_def)
lemma heap_list_s_restrict [rule_format]:
"\<forall>p. (\<lambda>x. (x,SIndexVal)) ` {p..+n} \<subseteq> X \<longrightarrow>
heap_list_s (s |` X) n p = heap_list_s s n p"
apply(induct_tac n)
apply(simp add: heap_list_s_def)
apply(auto simp: heap_list_s_def)
apply(rule proj_h_restrict)
apply(subgoal_tac "p \<in> {p..+Suc n}")
apply fast
apply(rule intvl_self, simp)
apply(drule_tac x="p+1" in spec)
apply clarsimp
apply(subgoal_tac "{p+1..+n} \<subseteq> {p..+Suc n}")
apply fast
apply clarsimp
apply(rule intvl_plus_sub_Suc)
apply simp
done
"(\<lambda>x. (x,SIndexVal)) ` {p..+n} \<subseteq> X \<Longrightarrow> heap_list_s (s |` X) n p = heap_list_s s n p"
apply(induct n arbitrary: p)
apply(simp add: heap_list_s_def)
apply(clarsimp simp: heap_list_s_def)
apply(rule conjI)
apply(fastforce intro: proj_h_restrict intvl_self)
apply(fastforce intro: intvl_plus_sub_Suc)
done
lemma lift_typ_heap_restrict [simp]:
"lift_typ_heap g (s |` s_footprint p) p = lift_typ_heap g s p"
apply(auto simp: lift_typ_heap_if)
apply(subst heap_list_s_restrict)
apply clarsimp
apply(drule intvlD, clarsimp)
apply(erule s_footprintI2)
apply simp
done
apply(clarsimp simp: lift_typ_heap_if)
apply(subst heap_list_s_restrict)
apply clarsimp
apply(drule intvlD, clarsimp)
apply(erule s_footprintI2)
apply simp
done
lemma singleton_s_valid:
"d,g \<Turnstile>\<^sub>t p \<Longrightarrow> singleton p (v::'a::mem_type) h d,g \<Turnstile>\<^sub>s p"
apply(simp add: singleton_def)
thm h_t_valid_restrict
apply(subst h_t_s_valid)
apply simp
done
by (simp add: singleton_def h_t_s_valid)
lemma singleton_lift_typ_heap_Some:
"d,g \<Turnstile>\<^sub>t p \<Longrightarrow> lift_typ_heap g (singleton p v h d) p = Some (v::'a::mem_type)"
apply(subst singleton_def)
apply simp
apply(subst lift_t)
apply(subst lift_t_heap_update)
apply(simp add: h_t_valid_restrict)
apply(simp add: ptr_retyp_h_t_valid)
done
by (simp add: singleton_def lift_t lift_t_heap_update h_t_valid_restrict)
lemma sep_map_g:
"(p \<mapsto>\<^sub>g v) s \<Longrightarrow> g p"
@ -261,7 +219,7 @@ lemma sep_map_g_sep_false:
lemma sep_map_singleton:
"d,g \<Turnstile>\<^sub>t p \<Longrightarrow> ((p::'a::mem_type ptr) \<mapsto>\<^sub>g v) (singleton p v h d)"
by (simp add: sep_map_def singleton_lift_typ_heap_Some singleton_dom)
by (simp add: sep_map_def singleton_lift_typ_heap_Some singleton_dom)
lemma sep_mapD:
"(p \<mapsto>\<^sub>g v) s \<Longrightarrow> lift_typ_heap g s p = Some v \<and>
@ -298,58 +256,54 @@ lemma proj_h_heap_merge:
lemma s_valid_heap_merge_right:
"s\<^sub>1,g \<Turnstile>\<^sub>s p \<Longrightarrow> s\<^sub>0 ++ s\<^sub>1,g \<Turnstile>\<^sub>s p"
apply (simp add: s_valid_def h_t_valid_def valid_footprint_def Let_def
(*proj_d_heap_merge*))
apply auto
apply(drule_tac x=y in spec, simp)
apply clarsimp
apply(erule map_le_trans)
apply(clarsimp simp: proj_d_def map_le_def split: option.splits)
apply(drule_tac x=y in spec, simp)
apply(clarsimp simp: proj_d_def map_le_def split: option.splits)
done
apply (clarsimp simp: s_valid_def h_t_valid_def valid_footprint_def Let_def)
apply (rule conjI)
apply(drule_tac x=y in spec, simp)
apply clarsimp
apply(erule map_le_trans)
apply(clarsimp simp: proj_d_def map_le_def split: option.splits)
apply(drule_tac x=y in spec, simp)
apply(clarsimp simp: proj_d_def map_le_def split: option.splits)
done
lemma proj_d_map_add_fst:
"fst (proj_d (s ++ t) x) = (if (x,SIndexVal) \<in> dom t then fst (proj_d t x) else
fst (proj_d s x))"
apply(auto simp: proj_d_def split: option.splits)
done
by (auto simp: proj_d_def split: option.splits)
lemma proj_d_map_add_snd:
"snd (proj_d (s ++ t) x) n = (if (x,SIndexTyp n) \<in> dom t then snd (proj_d t x) n else
snd (proj_d s x) n)"
apply(auto simp: proj_d_def split: option.splits)
done
by (auto simp: proj_d_def split: option.splits)
lemma proj_d_restrict_map_fst:
"(x,SIndexVal) \<in> X \<Longrightarrow> fst (proj_d (s |` X) x) = fst (proj_d s x)"
apply(auto simp: proj_d_def)
done
by (auto simp: proj_d_def)
lemma proj_d_restrict_map_snd:
"(x,SIndexTyp n) \<in> X \<Longrightarrow> snd (proj_d (s |` X) x) n = snd (proj_d s x) n"
apply(auto simp: proj_d_def)
done
by (auto simp: proj_d_def)
lemma s_valid_heap_merge_right2:
"\<lbrakk> s\<^sub>0 ++ s\<^sub>1,g \<Turnstile>\<^sub>s p; s_footprint p \<subseteq> dom s\<^sub>1 \<rbrakk> \<Longrightarrow> s\<^sub>1,g \<Turnstile>\<^sub>s p"
apply(auto simp: s_valid_def h_t_valid_def valid_footprint_def Let_def)
apply(clarsimp simp: map_le_def)
apply(subst proj_d_map_add_snd)
apply(clarsimp split: if_split_asm)
apply(subgoal_tac "(ptr_val p + of_nat y,SIndexTyp a) \<in> s_footprint p")
apply fast
apply(erule s_footprintI)
apply(simp add: size_of_def)
apply(subgoal_tac "(ptr_val p + of_nat y,SIndexVal) \<in> s_footprint p")
apply(drule (1) subsetD)
apply clarsimp
apply(subst (asm) proj_d_map_add_fst)
apply(drule_tac x=y in spec)
apply(clarsimp split: if_split_asm)
apply(rule s_footprintI2)
apply(simp add: size_of_def)
done
apply(clarsimp simp: s_valid_def h_t_valid_def valid_footprint_def Let_def)
apply(rule conjI)
apply(clarsimp simp: map_le_def)
apply(subst proj_d_map_add_snd)
apply(clarsimp split: if_split_asm)
apply(subgoal_tac "(ptr_val p + of_nat y,SIndexTyp a) \<in> s_footprint p")
apply fast
apply(erule s_footprintI)
apply(simp add: size_of_def)
apply(subgoal_tac "(ptr_val p + of_nat y,SIndexVal) \<in> s_footprint p")
apply(drule (1) subsetD)
apply clarsimp
apply(subst (asm) proj_d_map_add_fst)
apply(drule_tac x=y in spec)
apply(clarsimp split: if_split_asm)
apply(rule s_footprintI2)
apply(simp add: size_of_def)
done
lemma heap_list_s_heap_merge_right':
"\<lbrakk> s\<^sub>1,g \<Turnstile>\<^sub>s (p::'a::c_type ptr); n \<le> size_of TYPE('a) \<rbrakk> \<Longrightarrow>
@ -360,8 +314,6 @@ proof (induct n)
next
case (Suc n)
hence "(ptr_val p + (of_nat (size_of TYPE('a) - Suc n)),SIndexVal) \<in> dom s\<^sub>1"
apply -
apply auto
by - (drule_tac x="size_of TYPE('a) - Suc n" in s_valid_Some, auto)
with Suc show ?case
by (simp add: heap_list_s_def proj_h_heap_merge algebra_simps)
@ -514,7 +466,7 @@ proof rule
then obtain s\<^sub>0 s\<^sub>1 where "s\<^sub>0 \<bottom> s\<^sub>1" and "s = s\<^sub>1 ++ s\<^sub>0" and "P s\<^sub>0 \<or> Q s\<^sub>0" and
"R s\<^sub>1"
by - (drule sep_conjD, auto)
moreover hence "\<not> ?z \<Longrightarrow> \<not> Q s\<^sub>0"
moreover from this have "\<not> ?z \<Longrightarrow> \<not> Q s\<^sub>0"
by - (clarsimp, erule notE, erule (2) sep_conjI, simp)
ultimately show "?y \<or> ?z" by (force intro: sep_conjI)
next
@ -580,13 +532,13 @@ lemma sep_implD:
lemma sep_emp_sep_impl [simp]:
"(\<box> \<longrightarrow>\<^sup>* P) = P"
apply(rule ext)
apply(auto simp: sep_impl_def)
apply(drule_tac x=Map.empty in spec)
apply auto
apply(drule sep_empD)
apply simp
done
apply(rule ext)
apply(clarsimp simp: sep_impl_def)
apply(rule iffI; clarsimp?)
apply(drule_tac x=Map.empty in spec)
apply fastforce
apply(fastforce dest: sep_empD)
done
lemma sep_impl_sep_true [simp]:
"(P \<longrightarrow>\<^sup>* sep_true) = sep_true"
@ -606,37 +558,37 @@ lemma sep_impl_sep_true_false [simp]:
lemma sep_impl_impl:
"(P \<longrightarrow>\<^sup>* Q \<longrightarrow>\<^sup>* R) = (P \<and>\<^sup>* Q \<longrightarrow>\<^sup>* R)"
apply(rule ext)
apply rule
apply(rule sep_implI)
apply clarsimp
apply(drule sep_conjD, clarsimp)
apply(drule sep_implD)
apply(drule_tac x=s\<^sub>0 in spec)
apply(erule impE)
apply(clarsimp simp: map_disj_def, fast)
apply(drule sep_implD)
apply(drule_tac x=s\<^sub>1 in spec)
apply(erule impE)
apply(clarsimp simp: map_disj_def, fast)
apply(subst map_add_com [where h\<^sub>0=s\<^sub>1])
apply(clarsimp simp: map_disj_def, fast)
apply(subst map_add_assoc)
apply simp
apply(rule sep_implI, clarsimp)
apply(rule sep_implI, clarsimp)
apply(drule sep_implD)
apply(drule_tac x="s' ++ s'a" in spec)
apply(erule impE)
apply rule
apply(clarsimp simp: map_disj_def, fast)
apply(erule (1) sep_conjI)
apply(clarsimp simp: map_disj_def, fast)
apply(subst map_add_com)
apply(clarsimp simp: map_disj_def, fast)
apply simp
apply(simp add: map_add_assoc)
done
apply(rule ext)
apply(rule iffI)
apply(rule sep_implI)
apply clarsimp
apply(drule sep_conjD, clarsimp)
apply(drule sep_implD)
apply(drule_tac x=s\<^sub>0 in spec)
apply(erule impE)
apply(clarsimp simp: map_disj_def, fast)
apply(drule sep_implD)
apply(drule_tac x=s\<^sub>1 in spec)
apply(erule impE)
apply(clarsimp simp: map_disj_def, fast)
apply(subst map_add_com [where h\<^sub>0=s\<^sub>1])
apply(clarsimp simp: map_disj_def, fast)
apply(subst map_add_assoc)
apply simp
apply(rule sep_implI, clarsimp)
apply(rule sep_implI, clarsimp)
apply(drule sep_implD)
apply(drule_tac x="s' ++ s'a" in spec)
apply(erule impE)
apply(rule conjI)
apply(clarsimp simp: map_disj_def, fast)
apply(erule (1) sep_conjI)
apply(clarsimp simp: map_disj_def, fast)
apply(subst map_add_com)
apply(clarsimp simp: map_disj_def, fast)
apply simp
apply(simp add: map_add_assoc)
done
lemma sep_conj_sep_impl:
"\<lbrakk> P s; \<And>s. (P \<and>\<^sup>* Q) s \<Longrightarrow> R s \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s"
@ -686,15 +638,15 @@ lemma sep_map'_any_dom_exc:
lemma sep_map'_dom_exc:
"(p \<hookrightarrow>\<^sub>g (v::'a::mem_type)) s \<Longrightarrow> (ptr_val p,SIndexVal) \<in> dom s"
apply(clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
apply(subgoal_tac "s\<^sub>1 (ptr_val p, SIndexVal) \<noteq> None")
apply(force simp: map_ac_simps)
apply(drule sep_map_dom_exc)
apply(subgoal_tac "(ptr_val p, SIndexVal) \<in> s_footprint p")
apply fast
apply(rule s_footprintI2 [where x=0, simplified])
apply simp
done
apply(clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
apply(subgoal_tac "s\<^sub>1 (ptr_val p, SIndexVal) \<noteq> None")
apply(force simp: map_ac_simps)
apply(drule sep_map_dom_exc)
apply(subgoal_tac "(ptr_val p, SIndexVal) \<in> s_footprint p")
apply fast
apply(rule s_footprintI2 [where x=0, simplified])
apply simp
done
lemma sep_map'_lift_typ_heapD:
"(p \<hookrightarrow>\<^sub>g v) s \<Longrightarrow>
@ -723,47 +675,45 @@ qed
lemma sep_conj_overlapD:
"\<lbrakk> (P \<and>\<^sup>* Q) s; \<And>s. P s \<Longrightarrow> ((p::'a::mem_type ptr) \<hookrightarrow>\<^sub>g -) s;
\<And>s. Q s \<Longrightarrow> (p \<hookrightarrow>\<^sub>h -) s \<rbrakk> \<Longrightarrow> False"
apply(drule sep_conjD, clarsimp simp: map_disj_def)
apply(subgoal_tac "(ptr_val p,SIndexVal) \<in> dom s\<^sub>0 \<and> (ptr_val p,SIndexVal) \<in> dom s\<^sub>1")
apply fast
apply(fast intro!: sep_map'_any_dom_exc)
done
apply(drule sep_conjD, clarsimp simp: map_disj_def)
apply(subgoal_tac "(ptr_val p,SIndexVal) \<in> dom s\<^sub>0 \<and> (ptr_val p,SIndexVal) \<in> dom s\<^sub>1")
apply fast
apply(fast intro!: sep_map'_any_dom_exc)
done
lemma sep_no_skew:
"(\<lambda>s. (p \<hookrightarrow>\<^sub>g v) s \<and> (q \<hookrightarrow>\<^sub>h w) s) s \<Longrightarrow>
p=q \<or> {ptr_val (p::'a::c_type ptr)..+size_of TYPE('a)} \<inter>
{ptr_val q..+size_of TYPE('a)} = {}"
apply clarsimp
apply(drule sep_map'_lift_typ_heapD)+
apply(clarsimp simp: lift_typ_heap_if s_valid_def split: if_split_asm)
apply(rule ccontr)
apply(drule (1) h_t_valid_neq_disjoint)
apply simp
apply(rule peer_typ_not_field_of)
apply simp+
done
apply clarsimp
apply(drule sep_map'_lift_typ_heapD)+
apply(clarsimp simp: lift_typ_heap_if s_valid_def split: if_split_asm)
apply(rule ccontr)
apply(drule (1) h_t_valid_neq_disjoint; simp?)
apply(rule peer_typ_not_field_of; simp)
done
lemma sep_no_skew2:
"\<lbrakk> (\<lambda>s. (p \<hookrightarrow>\<^sub>g v) s \<and> (q \<hookrightarrow>\<^sub>h w) s) s; typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b) \<rbrakk>
\<Longrightarrow> {ptr_val (p::'a::c_type ptr)..+size_of TYPE('a)} \<inter>
{ptr_val (q::'b::c_type ptr)..+size_of TYPE('b)} = {}"
apply clarsimp
apply(drule sep_map'_lift_typ_heapD)+
apply(clarsimp simp: lift_typ_heap_if s_valid_def split: if_split_asm)
apply(frule (1) h_t_valid_neq_disjoint[where q=q])
apply(clarsimp simp: tag_disj_def sub_typ_proper_def)
apply(simp add: typ_tag_lt_def)
apply(clarsimp simp: tag_disj_def typ_tag_le_def field_of_t_def field_of_def)
apply assumption
done
apply clarsimp
apply(drule sep_map'_lift_typ_heapD)+
apply(clarsimp simp: lift_typ_heap_if s_valid_def split: if_split_asm)
apply(frule (1) h_t_valid_neq_disjoint[where q=q])
apply(clarsimp simp: tag_disj_def sub_typ_proper_def)
apply(simp add: typ_tag_lt_def)
apply(clarsimp simp: tag_disj_def typ_tag_le_def field_of_t_def field_of_def)
apply assumption
done
lemma sep_conj_impl_same:
"(P \<and>\<^sup>* (P \<longrightarrow>\<^sup>* Q)) s \<Longrightarrow> Q s"
apply(drule sep_conjD, clarsimp)
apply(drule sep_implD)
apply(drule_tac x="s\<^sub>0" in spec)
apply(clarsimp simp: map_disj_com)
done
apply(drule sep_conjD, clarsimp)
apply(drule sep_implD)
apply(drule_tac x="s\<^sub>0" in spec)
apply(clarsimp simp: map_disj_com)
done
(* Pure *)
@ -855,7 +805,7 @@ lemma intuitionistic_sep_impl_sep_true:
proof (rule intuitionisticI, rule sep_implI, clarsimp)
fix s s' s'a
assume "(sep_true \<longrightarrow>\<^sup>* P) s" and le: "s \<subseteq>\<^sub>m s'" and "s' \<bottom> s'a"
moreover hence "P (s ++ (s' |` (dom s' - dom s) ++ s'a))"
moreover from this have "P (s ++ (s' |` (dom s' - dom s) ++ s'a))"
by - (drule sep_implD,
drule_tac x="s'|`(dom s' - dom s) ++ s'a" in spec,
force simp: map_disj_def dest: map_disj_map_le)
@ -910,7 +860,7 @@ lemma intuitionistic_sep_impl:
proof (rule intuitionisticI, rule sep_implI, clarsimp)
fix s s' s'a
assume le: "s \<subseteq>\<^sub>m s'" and disj: "s' \<bottom> (s'a::'a \<rightharpoonup> 'b)"
moreover hence "s ++ s'a \<subseteq>\<^sub>m s' ++ s'a"
moreover from this have "s ++ s'a \<subseteq>\<^sub>m s' ++ s'a"
proof -
from le disj have "s \<subseteq>\<^sub>m s ++ s'a"
by (subst map_add_com)
@ -933,10 +883,11 @@ lemma weakest_intuitionistic:
"\<not> (\<exists>Q. (\<forall>s. ((sep_true \<longrightarrow>\<^sup>* P) s \<longrightarrow> Q s)) \<and> intuitionistic Q \<and>
Q \<noteq> (sep_true \<longrightarrow>\<^sup>* P) \<and> (\<forall>s. Q s \<longrightarrow> P s))"
apply (clarsimp, rule ext)
apply (rule iffI)
apply (rule sep_implI')
apply (drule_tac s=x and s'="x ++ h'" in intuitionisticD)
apply (clarsimp simp: map_ac_simps)+
apply (rename_tac Q x)
apply (rule iffI; clarsimp?)
apply (rule sep_implI')
apply (rename_tac h')
apply (drule_tac s=x and s'="x ++ h'" in intuitionisticD; clarsimp simp: map_ac_simps)
done
lemma intuitionistic_sep_conj_sep_true_P:
@ -1088,23 +1039,23 @@ lemma strictly_exact_conj_impl:
lemma dom_eps_sep_emp [simp]:
"dom_eps \<box> = {}"
apply(subst dom_eps [symmetric])
apply(rule strictly_exact_dom_exact)
apply(rule strictly_exact_sep_emp)
apply(rule sep_emp_empty)
apply simp
done
apply(subst dom_eps [symmetric])
apply(rule strictly_exact_dom_exact)
apply(rule strictly_exact_sep_emp)
apply(rule sep_emp_empty)
apply simp
done
lemma dom_eps_sep_map:
"g p \<Longrightarrow> dom_eps (p \<mapsto>\<^sub>g (v::'a::mem_type)) = s_footprint p"
apply(subst dom_eps [symmetric])
apply(rule dom_exact_sep_map)
apply(rule sep_map_singleton)
apply(erule ptr_retyp_h_t_valid)
apply(subst singleton_dom)
apply(erule ptr_retyp_h_t_valid)
apply simp
done
apply(subst dom_eps [symmetric])
apply(rule dom_exact_sep_map)
apply(rule sep_map_singleton)
apply(erule ptr_retyp_h_t_valid)
apply(subst singleton_dom)
apply(erule ptr_retyp_h_t_valid)
apply simp
done
(* Non-empty *)
@ -1129,49 +1080,48 @@ lemma non_empty_sep_false:
lemma non_empty_sep_emp:
"non_empty \<box>"
apply(unfold non_empty_def)
apply(rule exI, rule sep_emp_empty)
done
unfolding non_empty_def by (rule exI, rule sep_emp_empty)
lemma non_empty_sep_map:
"g p \<Longrightarrow> non_empty (p \<mapsto>\<^sub>g (v::'a::mem_type))"
apply(unfold non_empty_def)
apply(rule exI, rule sep_map_singleton)
apply(erule ptr_retyp_h_t_valid)
done
apply(unfold non_empty_def)
apply(rule exI, rule sep_map_singleton)
apply(erule ptr_retyp_h_t_valid)
done
lemma non_empty_sep_conj:
"\<lbrakk> non_empty P; non_empty Q; dom_exact P; dom_exact Q;
dom_eps P \<inter> dom_eps Q = {} \<rbrakk> \<Longrightarrow> non_empty (P \<and>\<^sup>* Q)"
apply(clarsimp simp: non_empty_def)
apply(rule_tac x="s++sa" in exI)
apply(rule sep_conjI, assumption+)
apply(clarsimp simp: map_disj_def dom_eps)
apply(subst map_add_com)
apply(clarsimp simp: map_disj_def dom_eps)
apply simp
done
apply(clarsimp simp: non_empty_def)
apply(rename_tac s s')
apply(rule_tac x="s++s'" in exI)
apply(rule sep_conjI, assumption+)
apply(clarsimp simp: map_disj_def dom_eps)
apply(subst map_add_com)
apply(clarsimp simp: map_disj_def dom_eps)
apply simp
done
lemma non_empty_sep_map':
"g p \<Longrightarrow> non_empty (p \<hookrightarrow>\<^sub>g (v::'a::mem_type))"
apply(unfold sep_map'_def)
apply(clarsimp simp: non_empty_def sep_conj_ac)
apply(rule_tac x="singleton p v h (ptr_retyp p d)" in exI)
apply(rule_tac s\<^sub>0=Map.empty in sep_conjI)
apply simp
apply(rule sep_map_singleton)
apply(erule ptr_retyp_h_t_valid)
apply(simp add: map_disj_def)
apply simp
done
apply(unfold sep_map'_def)
apply(clarsimp simp: non_empty_def sep_conj_ac)
apply(rule_tac x="singleton p v h (ptr_retyp p d)" in exI)
apply(rule_tac s\<^sub>0=Map.empty in sep_conjI)
apply simp
apply(rule sep_map_singleton)
apply(erule ptr_retyp_h_t_valid)
apply(simp add: map_disj_def)
apply simp
done
lemma non_empty_sep_impl:
"\<not> P Map.empty \<Longrightarrow> non_empty (P \<longrightarrow>\<^sup>* Q)"
apply(clarsimp simp: non_empty_def)
apply(rule_tac x="\<lambda>s. Some undefined" in exI)
apply(rule sep_implI)
apply(clarsimp simp: map_disj_def)
done
apply(clarsimp simp: non_empty_def)
apply(rule_tac x="\<lambda>s. Some undefined" in exI)
apply(rule sep_implI)
apply(clarsimp simp: map_disj_def)
done
(* Some useful lemmas *)
@ -1188,8 +1138,7 @@ lemma pure_conj_left: "((\<lambda>s. P' \<and> Q' s) \<and>\<^sup>* Q) = (\<lamb
lemma pure_conj_left': "((\<lambda>s. P' s \<and> Q') \<and>\<^sup>* Q) = (\<lambda>s. Q' \<and> (P' \<and>\<^sup>* Q) s)"
by (subst conj_comms, subst pure_conj_left, simp)
lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left
pure_conj_left'
lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left pure_conj_left'
declare pure_conj [simp add]
@ -1220,33 +1169,28 @@ lemma sep_conj_mapD_exc:
lemma sep_impl_conj_sameD:
"\<lbrakk> (P \<longrightarrow>\<^sup>* P \<and>\<^sup>* Q) s; dom_exact P; non_empty P; dom s \<subseteq> UNIV - dom_eps P \<rbrakk>
\<Longrightarrow> Q s"
apply(drule sep_implD)
apply(clarsimp simp: non_empty_def)
apply(drule_tac x=sa in spec)
apply(erule impE)
apply(clarsimp simp: map_disj_def dom_eps)
apply fast
apply(drule sep_conjD, clarsimp)
apply(clarsimp simp: map_disj_def)
apply(subst (asm) map_add_comm)
apply(clarsimp simp: dom_eps)
apply fast
apply(subst (asm) map_add_comm[of s\<^sub>1])
apply fast
apply(drule map_disj_add_eq_dom_right_eq)
apply(simp add: dom_eps)
apply(clarsimp simp: dom_eps map_disj_def)
apply fast
apply(simp add: map_disj_def)
apply clarsimp
done
apply(drule sep_implD)
apply(clarsimp simp: non_empty_def)
apply(rename_tac s')
apply(drule_tac x=s' in spec)
apply(erule impE)
apply(fastforce simp: map_disj_def dom_eps)
apply(drule sep_conjD, clarsimp)
apply(clarsimp simp: map_disj_def)
apply(subst (asm) map_add_comm)
apply(clarsimp simp: dom_eps)
apply fast
apply(subst (asm) map_add_comm, fast)
apply(drule map_disj_add_eq_dom_right_eq)
apply(simp add: dom_eps)
apply(clarsimp simp: dom_eps map_disj_def)
apply fast
apply(simp add: map_disj_def)
apply clarsimp
done
lemma sep_impl_conj_sameI:
"Q s \<Longrightarrow> (P \<longrightarrow>\<^sup>* P \<and>\<^sup>* Q) s "
apply(rule sep_implI, clarsimp)
apply(rule sep_conjI, assumption+)
apply(simp add: map_disj_com)
apply simp
done
"Q s \<Longrightarrow> (P \<longrightarrow>\<^sup>* P \<and>\<^sup>* Q) s"
by (fastforce intro: sep_implI sep_conjI simp: map_disj_com)
end

491
tools/c-parser/umm_heap/StructSupport.thy
View File

@ -13,60 +13,39 @@ imports SepCode SepInv
begin
lemma field_lookup_list_Some2 [rule_format]:
"\<forall>m. fn \<notin> dt_snd ` set ts \<longrightarrow> field_lookup_list (ts@[DTPair t fn]) (fn # fs) m =
field_lookup t fs (m + size_td_list ts)"
apply(induct_tac ts)
apply(clarsimp split: option.splits)
apply(rename_tac a list)
apply(clarsimp split: option.splits)
apply auto
apply(case_tac a, clarsimp split: if_split_asm)
apply(simp add: ac_simps)+
apply(case_tac a, clarsimp split: if_split_asm)
done
"fn \<notin> dt_snd ` set ts \<Longrightarrow>
field_lookup_list (ts@[DTPair t fn]) (fn # fs) m = field_lookup t fs (m + size_td_list ts)"
apply(induct ts arbitrary: m; clarsimp split: option.splits)
apply(rename_tac a list m)
apply(safe; case_tac a; clarsimp simp: ac_simps split: if_split_asm)
done
lemma fnl_set:
"set (CompoundCTypes.field_names_list (TypDesc (TypAggregate xs) tn)) =
dt_snd ` set xs"
apply(clarsimp simp: CompoundCTypes.field_names_list_def)
apply auto
done
"set (CompoundCTypes.field_names_list (TypDesc (TypAggregate xs) tn)) = dt_snd ` set xs"
by (auto simp: CompoundCTypes.field_names_list_def)
lemma fnl_extend_ti:
"\<lbrakk> fn \<notin> set (CompoundCTypes.field_names_list tag); aggregate tag \<rbrakk> \<Longrightarrow>
field_lookup (extend_ti tag t fn) (f # fs) m =
(if f=fn then field_lookup t fs (size_td tag+m) else field_lookup tag (f # fs) m)"
apply(case_tac tag, simp)
apply(rename_tac typ_struct xs)
apply(case_tac typ_struct, simp)
apply auto
apply(subst field_lookup_list_Some2)
apply(simp add: fnl_set)
apply(simp add: ac_simps)
apply(subst field_lookup_list_append)
apply(clarsimp split: option.splits)
done
apply(cases tag, rename_tac typ_struct xs)
apply(case_tac typ_struct; simp)
apply(simp add: ac_simps field_lookup_list_Some2 fnl_set)
apply(clarsimp simp: field_lookup_list_append split: option.splits)
done
lemma fl_ti_pad_combine:
"\<lbrakk> hd f \<noteq> CHR ''!''; aggregate tag \<rbrakk> \<Longrightarrow>
field_lookup (ti_pad_combine n tag) (f#fs) m = field_lookup tag (f#fs) m"
apply(clarsimp simp: ti_pad_combine_def Let_def)
apply(subst fnl_extend_ti)
apply(rule foldl_append_nmem)
apply simp
apply assumption
apply auto
done
by (auto simp: ti_pad_combine_def Let_def fnl_extend_ti foldl_append_nmem)
lemma fl_ti_typ_combine:
"\<lbrakk> fn \<notin> set (CompoundCTypes.field_names_list tag); aggregate tag \<rbrakk> \<Longrightarrow>
field_lookup (ti_typ_combine (t_b::'b::c_type itself) f_ab f_upd_ab fn tag) (f#fs) m =
(if f=fn then field_lookup (adjust_ti (typ_info_t TYPE('b)) f_ab f_upd_ab) fs (size_td tag+m) else field_lookup tag (f # fs) m)"
apply(unfold ti_typ_combine_def Let_def)
apply(subst fnl_extend_ti)
apply assumption+
apply clarsimp
done
(if f=fn
then field_lookup (adjust_ti (typ_info_t TYPE('b)) f_ab f_upd_ab) fs (size_td tag+m)
else field_lookup tag (f # fs) m)"
by (simp add: ti_typ_combine_def Let_def fnl_extend_ti)
lemma fl_ti_typ_combine_match:
"\<lbrakk> fn \<notin> set (CompoundCTypes.field_names_list tag); aggregate tag \<rbrakk> \<Longrightarrow>
@ -84,20 +63,21 @@ lemma fl_ti_typ_pad_combine:
"\<lbrakk> fn \<notin> set (CompoundCTypes.field_names_list tag); hd f \<noteq> CHR ''!''; hd fn \<noteq> CHR ''!'';
aggregate tag \<rbrakk> \<Longrightarrow>
field_lookup (ti_typ_pad_combine (t_b::'b::c_type itself) f_ab f_upd_ab fn tag) (f#fs) m =
(if f=fn then field_lookup (adjust_ti (typ_info_t TYPE('b)) f_ab f_upd_ab) fs (padup (align_of TYPE('b)) (size_td tag) + size_td tag+m) else field_lookup tag (f # fs) m)"
apply(unfold ti_typ_pad_combine_def Let_def)
apply(subst fl_ti_typ_combine)
apply clarsimp
apply clarsimp
apply clarsimp
apply(simp add: fl_ti_pad_combine size_td_ti_pad_combine)
done
(if f=fn
then field_lookup (adjust_ti (typ_info_t TYPE('b)) f_ab f_upd_ab) fs
(padup (align_of TYPE('b))
(size_td tag) + size_td tag+m)
else field_lookup tag (f # fs) m)"
unfolding ti_typ_pad_combine_def Let_def
by (subst fl_ti_typ_combine; clarsimp) (simp add: fl_ti_pad_combine size_td_ti_pad_combine)
lemma fl_ti_typ_pad_combine_match:
"\<lbrakk> fn \<notin> set (CompoundCTypes.field_names_list tag); hd fn \<noteq> CHR ''!'';
aggregate tag \<rbrakk> \<Longrightarrow>
field_lookup (ti_typ_pad_combine (t_b::'b::c_type itself) f_ab f_upd_ab fn tag) (fn#fs) m =
field_lookup (adjust_ti (typ_info_t TYPE('b)) f_ab f_upd_ab) fs (padup (align_of TYPE('b)) (size_td tag) + size_td tag+m)"
field_lookup (adjust_ti (typ_info_t TYPE('b)) f_ab f_upd_ab) fs
(padup (align_of TYPE('b))
(size_td tag) + size_td tag+m)"
by (simp add: fl_ti_typ_pad_combine)
lemma fl_ti_typ_pad_combine_mismatch:
@ -110,46 +90,39 @@ lemma fl_ti_typ_pad_combine_mismatch:
lemma fl_final_pad:
"\<lbrakk> hd f \<noteq> CHR ''!''; aggregate tag \<rbrakk> \<Longrightarrow>
field_lookup (final_pad tag) (f#fs) m = field_lookup tag (f#fs) m"
apply(clarsimp simp: final_pad_def Let_def fl_ti_pad_combine)
done
by (clarsimp simp: final_pad_def Let_def fl_ti_pad_combine)
lemma field_lookup_adjust_ti2' [rule_format]:
"\<forall>fn m s n. field_lookup ti fn m = Some (s,n) \<longrightarrow>
(field_lookup (adjust_ti ti f g) fn m = Some (adjust_ti s f g,n))"
"\<forall>fn m s n. field_lookup_struct st fn m = Some (s,n) \<longrightarrow> field_lookup_struct (map_td_struct (\<lambda>n algn d. update_desc f g d) st)
fn m = Some (adjust_ti s f g,n)"
"\<forall>fn m s n. field_lookup_list ts fn m = Some (s,n) \<longrightarrow> field_lookup_list (map_td_list (\<lambda>n algn d. update_desc f g d) ts) fn m = Some (adjust_ti s f g,n)"
"\<forall>fn m s n. field_lookup_pair x fn m = Some (s,n) \<longrightarrow> field_lookup_pair (map_td_pair (\<lambda>n algn d. update_desc f g d) x) fn m = Some (adjust_ti s f g,n)"
apply(induct ti and st and ts and x)
apply auto
apply(clarsimp simp: adjust_ti_def)
apply(clarsimp split: option.splits)
apply(rule, clarsimp)
apply(case_tac dt_pair, clarsimp)
apply clarsimp
apply(case_tac dt_pair, clarsimp split: if_split_asm)
apply(drule_tac x=fn in spec)
apply clarsimp
apply(fold adjust_ti_def)
apply(drule field_lookup_adjust_ti)
apply clarsimp
apply clarsimp
done
"\<forall>fn m s n. field_lookup_struct st fn m = Some (s,n) \<longrightarrow>
field_lookup_struct (map_td_struct (\<lambda>n algn d. update_desc f g d) st) fn m = Some (adjust_ti s f g,n)"
"\<forall>fn m s n. field_lookup_list ts fn m = Some (s,n) \<longrightarrow>
field_lookup_list (map_td_list (\<lambda>n algn d. update_desc f g d) ts) fn m = Some (adjust_ti s f g,n)"
"\<forall>fn m s n. field_lookup_pair x fn m = Some (s,n) \<longrightarrow>
field_lookup_pair (map_td_pair (\<lambda>n algn d. update_desc f g d) x) fn m = Some (adjust_ti s f g,n)"
apply(induct ti and st and ts and x, all \<open>clarsimp\<close>)
apply(clarsimp simp: adjust_ti_def)
apply(clarsimp split: option.splits)
apply(fastforce simp: split_DTPair_all simp flip: adjust_ti_def split: if_split_asm
dest: field_lookup_adjust_ti)
apply (clarsimp simp flip: adjust_ti_def)
done
lemma field_lookup_adjust_ti2:
"field_lookup t fn m = Some (s,n) \<Longrightarrow>
field_lookup (adjust_ti t f g) fn m = Some (adjust_ti s f g,n)"
apply(simp add: field_lookup_adjust_ti2')
done
by (simp add: field_lookup_adjust_ti2')
lemma fl_update:
"field_lookup (adjust_ti ti f g) fs m =
(case_option None (\<lambda>(t,n). Some (adjust_ti t f g,n)) (field_lookup ti fs m))"
apply(auto split: option.splits)
apply(rule ccontr, clarsimp)
apply(drule field_lookup_adjust_ti, clarsimp)
apply(erule field_lookup_adjust_ti2)
done
apply(clarsimp split: option.splits)
apply safe
apply(rule ccontr, clarsimp)
apply(drule field_lookup_adjust_ti, clarsimp)
apply(erule field_lookup_adjust_ti2)
done
lemmas fl_simps = fl_final_pad fl_ti_pad_combine
fl_ti_typ_combine_match fl_ti_typ_combine_mismatch
@ -160,17 +133,13 @@ lemma access_ti_props_simps [simp]:
"\<forall>g x. access_ti_struct (map_td_struct (\<lambda>n algn d. update_desc f g d) (st::'a field_desc typ_struct)) x = access_ti_struct st (f x)"
"\<forall>g x. access_ti_list (map_td_list (\<lambda>n algn d. update_desc f g d) (ts::('a field_desc typ_desc, char list) dt_pair list)) x = access_ti_list ts (f x)"
"\<forall>g x. access_ti_pair (map_td_pair (\<lambda>n algn d. update_desc f g d) (k::('a field_desc typ_desc, char list) dt_pair)) x = access_ti_pair k (f x)"
unfolding adjust_ti_def
apply(induct tag and st and ts and k)
apply (auto simp: update_desc_def)
done
unfolding adjust_ti_def
by (induct tag and st and ts and k) (auto simp: update_desc_def)
lemma field_norm_blah:
"\<lbrakk> \<forall>u v. f (g u v) = u; fd_cons_access_update d n \<rbrakk> \<Longrightarrow>
field_norm n algn (update_desc f g d) = field_norm n algn d"
apply(rule ext)+
apply(auto simp: update_desc_def field_norm_def fd_cons_access_update_def)
done
by (auto simp: update_desc_def field_norm_def fd_cons_access_update_def)
(* FIXME: should be generalised to just an extensionality principle on the
@ -181,9 +150,8 @@ lemma map_td_ext':
"wf_fd_struct st \<and> (\<forall>n algn d. fd_cons_access_update d n \<longrightarrow> (f n algn d = g n algn d)) \<longrightarrow> map_td_struct f st = map_td_struct g st"
"wf_fd_list ts \<and> (\<forall>n algn d. fd_cons_access_update d n \<longrightarrow> (f n algn d = g n algn d)) \<longrightarrow> map_td_list f ts = map_td_list g ts"
"wf_fd_pair x \<and> (\<forall>n algn d. fd_cons_access_update d n \<longrightarrow> (f n algn d = g n algn d)) \<longrightarrow> map_td_pair f x = map_td_pair g x"
apply(induct t and st and ts and x)
apply (auto simp: fd_cons_struct_def fd_cons_access_update_def fd_cons_desc_def)
done
by (induct t and st and ts and x)
(auto simp: fd_cons_struct_def fd_cons_access_update_def fd_cons_desc_def)
lemma map_td_extI:
"\<lbrakk> wf_fd t; (\<forall>n algn d. fd_cons_access_update d n \<longrightarrow> (f n algn d = g n algn d)) \<rbrakk>
@ -193,63 +161,54 @@ lemma map_td_extI:
lemma export_tag_adjust_ti2 [simp]:
"\<lbrakk> \<forall>u v. f (g u v) = u; wf_lf (lf_set t []); wf_desc t \<rbrakk> \<Longrightarrow>
export_uinfo (adjust_ti t f g) = (export_uinfo t)"
apply(simp add: export_uinfo_def adjust_ti_def map_td_map)
apply(rule map_td_extI)
apply(rule wf_fdp_fdD)
apply(erule (2) wf_lf_fdp)
apply clarsimp
apply(simp add: field_norm_blah)
done
unfolding export_uinfo_def adjust_ti_def map_td_map
by (fastforce simp: field_norm_blah intro: wf_fdp_fdD map_td_extI elim: wf_lf_fdp)
lemma field_names_list:
"field_names_list (xs@ys) t = field_names_list xs t @ field_names_list ys t"
by (induct xs) auto
lemma field_names_extend_ti:
"typ_name t \<noteq> typ_name ti \<Longrightarrow> field_names (extend_ti ti xi fn) t = field_names ti t @ (map (\<lambda>fs. fn#fs) (field_names xi t))"
apply(cases ti, clarsimp)
apply(rename_tac typ_struct xs)
apply(case_tac typ_struct, auto)
apply(simp add: field_names_list)
done
"typ_name t \<noteq> typ_name ti \<Longrightarrow>
field_names (extend_ti ti xi fn) t = field_names ti t @ (map (\<lambda>fs. fn#fs) (field_names xi t))"
by (cases ti, rename_tac typ_struct xs)
(case_tac typ_struct; fastforce simp: field_names_list)
lemma field_names_ti_pad_combine:
"\<lbrakk> typ_name t \<noteq> typ_name ti; hd (typ_name t) \<noteq> CHR ''!'' \<rbrakk> \<Longrightarrow>
field_names (ti_pad_combine n ti) t = field_names ti t"
apply(clarsimp simp: ti_pad_combine_def Let_def)
apply(subst field_names_extend_ti)
apply(simp add: export_uinfo_def size_map_td)
apply clarsimp
done
by (clarsimp simp: ti_pad_combine_def Let_def field_names_extend_ti export_uinfo_def size_map_td)
lemma field_names_final_pad:
"\<lbrakk> typ_name t \<noteq> typ_name ti; hd (typ_name t) \<noteq> CHR ''!'' \<rbrakk> \<Longrightarrow>
field_names (final_pad ti) t = field_names ti t"
apply(clarsimp simp: final_pad_def Let_def)
apply(rule field_names_ti_pad_combine)
apply auto
done
by (clarsimp simp: final_pad_def Let_def field_names_ti_pad_combine)
lemma field_names_adjust_ti:
assumes "fg_cons f g"
shows
"wf_fd ti \<longrightarrow> field_names (adjust_ti (ti::'a typ_info) f g) t = field_names ti t"
"wf_fd_struct st \<longrightarrow> field_names_struct ((map_td_struct (\<lambda>n algn d. update_desc f g d) (st::'a field_desc typ_struct))) t = field_names_struct st t"
"wf_fd_list ts \<longrightarrow> field_names_list (map_td_list (\<lambda>n algn d. update_desc f g d) (ts::('a field_desc typ_desc, char list) dt_pair list)) t = field_names_list ts t"
"wf_fd_pair x \<longrightarrow> field_names_pair (map_td_pair (\<lambda>n algn d. update_desc f g d) (x::('a field_desc typ_desc, char list) dt_pair)) t = field_names_pair x t" using assms
apply(induct ti and st and ts and x)
apply(auto simp: adjust_ti_def)
done
"wf_fd ti \<longrightarrow>
field_names (adjust_ti (ti::'a typ_info) f g) t = field_names ti t"
"wf_fd_struct st \<longrightarrow>
field_names_struct ((map_td_struct (\<lambda>n algn d. update_desc f g d)
(st::'a field_desc typ_struct))) t =
field_names_struct st t"
"wf_fd_list ts \<longrightarrow>
field_names_list (map_td_list (\<lambda>n algn d. update_desc f g d)
(ts::('a field_desc typ_desc, char list) dt_pair list)) t =
field_names_list ts t"
"wf_fd_pair x \<longrightarrow>
field_names_pair (map_td_pair (\<lambda>n algn d. update_desc f g d)
(x::('a field_desc typ_desc, char list) dt_pair)) t =
field_names_pair x t" using assms
by (induct ti and st and ts and x) (auto simp: adjust_ti_def)
lemma field_names_ti_typ_combine:
"\<lbrakk> typ_name t \<noteq> typ_name ti; fg_cons f g \<rbrakk> \<Longrightarrow>
field_names (ti_typ_combine (t_b::'b::mem_type itself) f g fn ti) t =
field_names ti t @ map ((#) fn) (field_names (typ_info_t TYPE('b)) t)"
apply(clarsimp simp: ti_typ_combine_def Let_def)
apply(subst field_names_extend_ti)
apply(simp add: export_uinfo_def size_map_td)
apply(simp add: field_names_adjust_ti)
done
by (clarsimp simp: ti_typ_combine_def Let_def field_names_adjust_ti field_names_extend_ti
export_uinfo_def size_map_td)
lemma size_empty_typ_info [simp]:
"size (empty_typ_info tn) = 2"
@ -261,10 +220,7 @@ lemma list_size_char:
lemma size_ti_extend_ti [simp]:
"aggregate ti \<Longrightarrow> size (extend_ti ti t fn) = size ti + size t + 2"
apply(cases ti, clarsimp)
apply(rename_tac typ_struct xs)
apply(case_tac typ_struct, auto simp: list_size_char)
done
by (cases ti, rename_tac typ_struct xs) (case_tac typ_struct, auto simp: list_size_char)
lemma typ_name_empty_typ_info [simp]:
"typ_name (empty_typ_info tn) = tn"
@ -298,20 +254,12 @@ lemma field_names_ti_typ_pad_combine:
"\<lbrakk> typ_name t \<noteq> typ_name ti; fg_cons f g; aggregate ti; hd (typ_name t) \<noteq> CHR ''!'' \<rbrakk> \<Longrightarrow>
field_names (ti_typ_pad_combine (t_b::'b::mem_type itself) f g fn ti) t =
field_names ti t @ map ((#) fn) (field_names (typ_info_t TYPE('b)) t)"
apply(auto simp: ti_typ_pad_combine_def Let_def)
apply(subst field_names_ti_typ_combine)
apply simp
apply assumption
apply(simp add: field_names_ti_pad_combine)
apply(simp add: field_names_ti_typ_combine)
done
by (auto simp: ti_typ_pad_combine_def Let_def field_names_ti_typ_combine field_names_ti_pad_combine)
lemma field_names_empty_typ_info:
"typ_name t \<noteq> tn \<Longrightarrow> field_names (empty_typ_info tn) t = []"
by(clarsimp simp: empty_typ_info_def)
lemma sep_heap_update_global_super_fl':
"\<lbrakk> (p \<mapsto>\<^sub>g u \<and>\<^sup>* R) (lift_state (h,d));
field_lookup (typ_info_t TYPE('b::mem_type)) f 0 = Some (t,n);
@ -319,168 +267,122 @@ lemma sep_heap_update_global_super_fl':
w = update_ti_t t (to_bytes_p v) u \<rbrakk> \<Longrightarrow>
((p \<mapsto>\<^sub>g w) \<and>\<^sup>* R)
(lift_state (heap_update (Ptr &(p\<rightarrow>f)) (v::'a::mem_type) h,d))"
apply(drule_tac v=v in sep_heap_update_global_super_fl)
apply assumption+
apply simp
done
by (auto dest: sep_heap_update_global_super_fl)
lemma sep_heap_update_global_super_fl'_inv:
"\<lbrakk> (p \<mapsto>\<^sup>i\<^sub>g u \<and>\<^sup>* R) (lift_state (h,d));
field_lookup (typ_info_t TYPE('b::mem_type)) f 0 = Some (t,n);
export_uinfo t = (typ_uinfo_t TYPE('a));
w = update_ti_t t (to_bytes_p v) u\<rbrakk> \<Longrightarrow>
((p \<mapsto>\<^sup>i\<^sub>g w) \<and>\<^sup>* R)
(lift_state (heap_update (Ptr &(p\<rightarrow>f)) (v::'a::mem_type) h,d))"
apply(unfold sep_map_inv_def)
apply(simp only:sep_conj_assoc)
apply(erule (2) sep_heap_update_global_super_fl)
done
((p \<mapsto>\<^sup>i\<^sub>g w) \<and>\<^sup>* R) (lift_state (heap_update (Ptr &(p\<rightarrow>f)) (v::'a::mem_type) h,d))"
unfolding sep_map_inv_def
by (simp only:sep_conj_assoc) (erule (2) sep_heap_update_global_super_fl)
lemma sep_map'_field_map':
"\<lbrakk> ((p::'b::mem_type ptr) \<hookrightarrow>\<^sub>g v) s; field_lookup (typ_info_t TYPE('b)) f 0
= Some (d,n); export_uinfo d = typ_uinfo_t TYPE('a);
guard_mono g h \<rbrakk> \<Longrightarrow>
((Ptr (&(p\<rightarrow>f))::'a::mem_type ptr) \<hookrightarrow>\<^sub>h from_bytes (access_ti\<^sub>0 d v)) s"
apply(subst sep_map'_unfold_exc)
apply(subst (asm) sep_map'_def)
apply(erule sep_conj_impl)
apply(erule (4) sep_map_field_map')
done
by (subst sep_map'_unfold_exc, subst (asm) sep_map'_def)
(fastforce simp: sep_map'_def elim: sep_conj_impl sep_map_field_map')
lemma sep_map'_field_map:
"\<lbrakk> ((p::'b::mem_type ptr) \<hookrightarrow>\<^sub>g v) s; field_lookup (typ_info_t TYPE('b)) f 0
= Some (d,n); export_uinfo d = typ_uinfo_t TYPE('a);
guard_mono g h; w=from_bytes (access_ti\<^sub>0 d v) \<rbrakk> \<Longrightarrow>
((Ptr (&(p\<rightarrow>f))::'a::mem_type ptr) \<hookrightarrow>\<^sub>h w) s"
apply(simp add: sep_map'_field_map')
done
by (simp add: sep_map'_field_map')
lemma inter_sub:
"\<lbrakk> Y \<subseteq> X; Y = Z \<rbrakk> \<Longrightarrow> X \<inter> Y = Z"
apply fast
done
by fast
lemma sep_map'_field_map_inv:
"\<lbrakk> ((p::'b::mem_type ptr) \<hookrightarrow>\<^sup>i\<^sub>g v) s; field_lookup (typ_info_t TYPE('b)) f 0
= Some (d,n); export_uinfo d = typ_uinfo_t TYPE('a);
guard_mono g h; w=from_bytes (access_ti\<^sub>0 d v) \<rbrakk> \<Longrightarrow>
((Ptr (&(p\<rightarrow>f))::'a::mem_type ptr) \<hookrightarrow>\<^sup>i\<^sub>h w) s"
apply(unfold sep_map'_inv_def)
apply(drule sep_conjD, clarsimp simp: sep_conj_ac)
apply(subst sep_map'_unfold_exc)
apply(subst sep_conj_assoc [symmetric])
apply(rule_tac s\<^sub>0="(s\<^sub>1 ++ s\<^sub>0) |` {(x,y) | x y. x \<in> {&(p\<rightarrow>f)..+size_td d}}" and
s\<^sub>1="(s\<^sub>1 ++ s\<^sub>0) |` (dom (s\<^sub>1 ++ s\<^sub>0) - {(x,y) | x y. x \<in> {&(p\<rightarrow>f)..+size_td d}})" in sep_conjI)
apply(subst sep_conj_com)
apply(rule_tac s\<^sub>0="(s\<^sub>1 ++ s\<^sub>0) |` s_footprint ((Ptr &(p\<rightarrow>f))::'a::mem_type ptr)" and s\<^sub>1="(s\<^sub>1 ++ s\<^sub>0) |` ({(x, y) |x y. x \<in> {&(p\<rightarrow>f)..+size_td d}} - s_footprint ((Ptr &(p\<rightarrow>f))::'a::mem_type ptr))"in sep_conjI)
apply(drule (3) sep_map'_field_map')
apply(clarsimp simp: sep_conj_ac sep_map'_def sep_conj_def)
apply(rule_tac x="s\<^sub>0' |` s_footprint ((Ptr &(p\<rightarrow>f))::'a::mem_type ptr)" in exI)
apply(rule_tac x="s\<^sub>1'" in exI)
apply(clarsimp simp: sep_conj_ac)
apply rule
apply(clarsimp simp: map_disj_def sep_conj_ac)
apply fast
apply(subst map_add_com[where h\<^sub>1=s\<^sub>0'])
apply(clarsimp simp: map_disj_def sep_conj_ac)
apply fast
apply(subst map_add_assoc)
apply(subst map_add_restrict)+
apply(frule sep_map_dom_exc)
apply(rotate_tac -1)
apply(drule sym)
apply(thin_tac "s = x" for x)
apply(clarsimp simp: restrict_map_disj_dom_empty map_ac_simps sep_conj_ac)
apply(clarsimp simp: inv_footprint_def sep_conj_ac)
apply(rule inter_sub)
apply(clarsimp simp: sep_conj_ac)
apply(frule_tac p=p in field_tag_sub)
apply(drule (1) subsetD)
apply(clarsimp simp: sep_conj_ac)
apply(clarsimp simp: sep_conj_ac sep_map'_def sep_conj_def)
apply(drule sep_map_dom_exc)
apply(subgoal_tac "s\<^sub>1' (x,y) \<noteq> None")
apply(clarsimp simp: sep_conj_ac)
apply(subst map_add_comm)
apply(clarsimp simp: map_disj_def sep_conj_ac)
apply fast
apply(subst map_add_find_right)
apply fast
apply fast
apply(clarsimp simp: sep_conj_ac)
apply fast
apply(frule export_size_of)
apply simp
apply fast
apply(clarsimp simp: map_disj_def)
apply fast
apply clarsimp
apply(subst subset_map_restrict_sub_add)
apply(clarsimp simp: s_footprint_def s_footprint_untyped_def)
apply(rule intvlI)
apply(frule export_size_of)
apply(simp add: size_of_def)
apply simp
apply simp
apply(clarsimp simp: map_disj_def)
apply blast
apply(subst map_add_com[of "m|`S" for m S])
apply(clarsimp simp: map_disj_def)
apply blast
apply(subst map_add_restrict_comp_right_dom)
apply simp
done
"\<lbrakk> ((p::'b::mem_type ptr) \<hookrightarrow>\<^sup>i\<^sub>g v) s; field_lookup (typ_info_t TYPE('b)) f 0 = Some (d,n);
export_uinfo d = typ_uinfo_t TYPE('a); guard_mono g h; w=from_bytes (access_ti\<^sub>0 d v) \<rbrakk> \<Longrightarrow>
((Ptr &(p\<rightarrow>f)::'a::mem_type ptr) \<hookrightarrow>\<^sup>i\<^sub>h w) s"
apply(unfold sep_map'_inv_def)
apply(drule sep_conjD, clarsimp simp: sep_conj_ac)
apply(subst sep_map'_unfold_exc)
apply(subst sep_conj_assoc [symmetric])
apply(rule_tac s\<^sub>0="(s\<^sub>1 ++ s\<^sub>0) |` {(x,y) | x y. x \<in> {&(p\<rightarrow>f)..+size_td d}}" and
s\<^sub>1="(s\<^sub>1 ++ s\<^sub>0) |` (dom (s\<^sub>1 ++ s\<^sub>0) - {(x,y) | x y. x \<in> {&(p\<rightarrow>f)..+size_td d}})"
in sep_conjI)
apply(subst sep_conj_com)
apply(rule_tac s\<^sub>0="(s\<^sub>1 ++ s\<^sub>0) |` s_footprint ((Ptr &(p\<rightarrow>f))::'a::mem_type ptr)" and
s\<^sub>1="(s\<^sub>1 ++ s\<^sub>0) |` ({(x, y) |x y. x \<in> {&(p\<rightarrow>f)..+size_td d}} -
s_footprint ((Ptr &(p\<rightarrow>f))::'a::mem_type ptr))" in sep_conjI)
apply(drule (3) sep_map'_field_map')
apply(clarsimp simp: sep_conj_ac sep_map'_def sep_conj_def)
apply(rule_tac x="s\<^sub>0' |` s_footprint ((Ptr &(p\<rightarrow>f))::'a::mem_type ptr)" in exI)
apply(rule_tac x="s\<^sub>1'" in exI)
apply(clarsimp simp: sep_conj_ac)
apply(rule conjI)
apply(fastforce simp: map_disj_def sep_conj_ac)
apply(subst map_add_com[where h\<^sub>0="a ++ b" for a b])
apply(fastforce simp: map_disj_def sep_conj_ac)
apply(subst map_add_assoc)
apply(simp add: map_add_restrict)
apply(frule sep_map_dom_exc)
apply(rotate_tac -1)
apply(drule sym)
apply(thin_tac "s = x" for x)
apply(fastforce simp: restrict_map_disj_dom_empty map_ac_simps sep_conj_ac)
apply(clarsimp simp: inv_footprint_def sep_conj_ac)
apply(rule inter_sub)
apply(clarsimp simp: sep_conj_ac)
apply(frule_tac p=p in field_tag_sub)
apply(drule (1) subsetD)
apply(clarsimp simp: sep_conj_ac)
apply(clarsimp simp: sep_conj_ac sep_map'_def sep_conj_def)
apply(drule sep_map_dom_exc)
apply(subgoal_tac "s\<^sub>1' (x,y) \<noteq> None")
apply(clarsimp simp: sep_conj_ac)
apply(subst map_add_comm)
apply(fastforce simp: map_disj_def sep_conj_ac)
apply simp
apply(clarsimp simp: sep_conj_ac, fast)
apply(fastforce dest: export_size_of)
apply(fastforce simp: map_disj_def)
apply clarsimp
apply(subst subset_map_restrict_sub_add; simp?)
apply(fastforce intro!: intvlI dest: export_size_of
simp: size_of_def s_footprint_def s_footprint_untyped_def)
apply simp
apply(fastforce simp: map_disj_def)
apply (metis (lifting) map_add_com map_add_restrict_comp_right_dom map_le_iff_map_add_commute
restrict_map_sub_add restrict_map_sub_disj)
done
lemma guard_mono_True [simp]:
"guard_mono f (\<lambda>x. True)"
by (simp add: guard_mono_def)
lemma from_bytes:
"length bs = size_of TYPE('a) \<Longrightarrow>
update_ti_t (typ_info_t TYPE('a::mem_type)) bs v = from_bytes bs"
apply(simp add: from_bytes_def upd size_of_def)
done
lemma access_ti\<^sub>0_to_bytes [simp]:
"access_ti\<^sub>0 (typ_info_t TYPE('a::c_type)) = (to_bytes_p::'a \<Rightarrow> byte list)"
apply(rule ext)
apply(simp add: to_bytes_p_def to_bytes_def access_ti\<^sub>0_def size_of_def)
done
by (auto simp: to_bytes_p_def to_bytes_def access_ti\<^sub>0_def size_of_def)
lemma update_ti_s_from_bytes:
"length bs = size_of TYPE('a) \<Longrightarrow>
update_ti_t (typ_info_t TYPE('a::mem_type)) bs x =
(from_bytes::byte list \<Rightarrow> 'a) bs"
apply(simp add: from_bytes_def upd)
done
update_ti_t (typ_info_t TYPE('a::mem_type)) bs x = from_bytes bs"
by (simp add: from_bytes_def upd)
lemma access_ti\<^sub>0_update_ti [simp]:
"access_ti\<^sub>0 (adjust_ti ti f g) = access_ti\<^sub>0 ti \<circ> f"
apply(rule ext)
apply(simp add: access_ti\<^sub>0_def)
done
by (auto simp: access_ti\<^sub>0_def)
lemma update_ti_s_adjust_ti:
"\<lbrakk> length bs = size_td ti ; fg_cons f g \<rbrakk> \<Longrightarrow>
update_ti_t (adjust_ti ti f g) bs v =
g (update_ti_t ti bs (f v)) v"
apply(simp add: update_ti_adjust_ti)
done
lemma update_ti_s_adjust_ti: (* FIXME: eliminate; first assumption redundant *)
"\<lbrakk> length bs = size_td ti; fg_cons f g \<rbrakk> \<Longrightarrow>
update_ti_t (adjust_ti ti f g) bs v = g (update_ti_t ti bs (f v)) v"
by (rule update_ti_adjust_ti)
lemma update_ti_s_adjust_ti_to_bytes_p [simp]:
"fg_cons f g \<Longrightarrow>
update_ti_t (adjust_ti (typ_info_t TYPE('a)) f g) (to_bytes_p (v::'a::mem_type)) w =
g v w"
apply(simp add: update_ti_adjust_ti to_bytes_p_def to_bytes_def)
apply(subst upd_rf)
apply(subst fd_cons_length)
apply simp
apply(simp add: size_of_def)+
apply(subst fd_cons_update_access)
apply simp+
done
update_ti_t (adjust_ti (typ_info_t TYPE('a)) f g) (to_bytes_p (v::'a::mem_type)) w = g v w"
apply(simp add: update_ti_adjust_ti to_bytes_p_def to_bytes_def)
apply(subst upd_rf; simp add: size_of_def fd_cons_length)
apply(subst fd_cons_update_access; simp)
done
(* td_names stuff *)
@ -504,25 +406,26 @@ where
| tnm5: "td_names_pair (DTPair t nm) = td_names t"
lemma td_set_td_names:
"\<And>(tp :: 'a typ_desc) n m. \<lbrakk>(tp, n) \<in> td_set tp' m; typ_name tp \<noteq> pad_typ_name \<rbrakk> \<Longrightarrow> typ_name tp \<in> td_names tp'" and
"\<And>(tp :: 'a typ_desc) n m. \<lbrakk>(tp, n) \<in> td_set_struct tps m; typ_name tp \<noteq> pad_typ_name \<rbrakk> \<Longrightarrow> typ_name tp \<in> td_names_struct tps" and
"\<And>(tp :: 'a typ_desc) n m. \<lbrakk>(tp, n) \<in> td_set_list tpl m; typ_name tp \<noteq> pad_typ_name \<rbrakk> \<Longrightarrow> typ_name tp \<in> td_names_list tpl" and
"\<And>(tp :: 'a typ_desc) n m. \<lbrakk>(tp, n) \<in> td_set_pair tpr m; typ_name tp \<noteq> pad_typ_name \<rbrakk>\<Longrightarrow> typ_name tp \<in> td_names_pair tpr"
"\<And>(tp :: 'a typ_desc) n m. \<lbrakk>(tp, n) \<in> td_set tp' m; typ_name tp \<noteq> pad_typ_name \<rbrakk> \<Longrightarrow>
typ_name tp \<in> td_names tp'" and
"\<And>(tp :: 'a typ_desc) n m. \<lbrakk>(tp, n) \<in> td_set_struct tps m; typ_name tp \<noteq> pad_typ_name \<rbrakk> \<Longrightarrow>
typ_name tp \<in> td_names_struct tps" and
"\<And>(tp :: 'a typ_desc) n m. \<lbrakk>(tp, n) \<in> td_set_list tpl m; typ_name tp \<noteq> pad_typ_name \<rbrakk> \<Longrightarrow>
typ_name tp \<in> td_names_list tpl" and
"\<And>(tp :: 'a typ_desc) n m. \<lbrakk>(tp, n) \<in> td_set_pair tpr m; typ_name tp \<noteq> pad_typ_name \<rbrakk>\<Longrightarrow>
typ_name tp \<in> td_names_pair tpr"
by (induct tp' and tps and tpl and tpr) auto
lemma td_names_map_td [simp]:
shows "td_names (map_td f tp) = td_names tp" and
"td_names_struct (map_td_struct f tps) = td_names_struct tps" and
"td_names_list (map_td_list f tpl) = td_names_list tpl" and
"td_names (map_td f tp) = td_names tp"
"td_names_struct (map_td_struct f tps) = td_names_struct tps"
"td_names_list (map_td_list f tpl) = td_names_list tpl"
"td_names_pair (map_td_pair f tpr) = td_names_pair tpr"
by (induct tp and tps and tpl and tpr) simp_all
lemma td_names_list_append [simp]:
"td_names_list (a @ b) = td_names_list a \<union> td_names_list b"
apply (induct a)
apply simp
apply (simp add: Un_assoc)
done
by (induct a; simp add: Un_assoc)
lemma pad_typ_name_td_names: (* dangerous in [simp]? *)
"A - {pad_typ_name} \<union> td_names tp = (A \<union> td_names tp) - {pad_typ_name}"
@ -594,33 +497,24 @@ lemma typ_name_export_uinfo [simp]:
lemma replicate_Suc_append:
"replicate (Suc n) x = replicate n x @ [x]"
apply (induct n)
apply simp
apply simp
done
by (induct n; simp)
lemma list_eq_subset:
"xs = ys \<Longrightarrow> set ys \<subseteq> set xs" by simp
lemma td_names_array_tag_n:
"td_names ((array_tag_n n) :: (('a::c_type,'b::finite) array field_desc typ_desc))
= {typ_name (typ_info_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b set))}
\<union> (if n = 0 then {} else td_names (typ_info_t TYPE('a)))"
apply (induct n)
apply (simp add: array_tag_n.simps pad_typ_name_def)
defer
apply (simp add: array_tag_n.simps pad_typ_name_def)
apply (subst Diff_triv)
apply (clarsimp)
apply (drule list_eq_subset)
apply clarsimp
apply (simp add: typ_uinfo_t_def)
"td_names ((array_tag_n n) :: (('a::c_type,'b::finite) array field_desc typ_desc)) =
{typ_name (typ_info_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b set))} \<union>
(if n = 0 then {} else td_names (typ_info_t TYPE('a)))"
apply (induct n; simp add: array_tag_n.simps pad_typ_name_def)
apply (subst Diff_triv; clarsimp simp: typ_uinfo_t_def)
apply (fastforce dest: list_eq_subset)
done
lemma td_names_array [simp]:
"td_names (typ_info_t TYPE(('a :: c_type)['b :: finite])) =
{typ_name (typ_info_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b set))}
\<union> td_names (typ_info_t TYPE('a))"
{typ_name (typ_info_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b set))} \<union>
td_names (typ_info_t TYPE('a))"
by (simp add: typ_info_array array_tag_def td_names_array_tag_n)
lemma tag_disj_via_td_name:
@ -634,19 +528,16 @@ lemma tag_disj_via_td_name:
lemma lift_t_hrs_mem_update_fld:
fixes val :: "'b :: mem_type" and ptr :: "'a :: mem_type ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 \<equiv>
Some (adjust_ti (typ_info_t TYPE('b)) xf (xfu \<circ> (\<lambda>x _. x)), m')"
Some (adjust_ti (typ_info_t TYPE('b)) xf (xfu \<circ> (\<lambda>x _. x)), m')"
and xf_xfu: "fg_cons xf (xfu \<circ> (\<lambda>x _. x))"
and cl: "lift_t g hp ptr = Some z"
shows "(lift_t g (hrs_mem_update (heap_update (Ptr &(ptr\<rightarrow>f)) val) hp)) =
lift_t g hp(ptr \<mapsto> xfu (\<lambda>_. val) z)"
lift_t g hp(ptr \<mapsto> xfu (\<lambda>_. val) z)"
(is "?LHS = ?RHS")
proof -
let ?ati = "adjust_ti (typ_info_t TYPE('b)) xf (xfu \<circ> (\<lambda>x _. x))"
have eui: "typ_uinfo_t TYPE('b) = export_uinfo (?ati)" using xf_xfu
apply (subst export_tag_adjust_ti2 [OF _ wf_lf wf_desc])
apply (simp add: fg_cons_def )
apply (rule meta_eq_to_obj_eq [OF typ_uinfo_t_def])
done
by (simp add: typ_uinfo_t_def)
have cl': "lift_t g (fst hp, snd hp) ptr = Some z" using cl by simp
@ -664,16 +555,13 @@ proof -
ultimately show "TYPE('b) \<le>\<^sub>\<tau> TYPE('a)" by (rule field_ti_sub_typ)
qed
also have "\<dots> =
lift_t g hp(ptr \<mapsto> update_ti_t
(adjust_ti (typ_info_t TYPE('b)) xf (xfu \<circ> (\<lambda>x _. x))) (to_bytes_p val) z)"
apply (subst super_field_update_lookup [OF _ eui cl'])
apply (rule meta_eq_to_obj_eq [OF fl])
apply simp
done
also
have "\<dots> = lift_t g hp(ptr \<mapsto> update_ti_t (adjust_ti (typ_info_t TYPE('b)) xf (xfu \<circ> (\<lambda>x _. x)))
(to_bytes_p val) z)"
by (simp add: cl eui fl super_field_update_lookup)
also have "\<dots> = ?RHS" using xf_xfu
by (simp add: update_ti_adjust_ti from_bytes)
by (simp add: update_ti_adjust_ti update_ti_s_from_bytes)
finally show ?thesis .
qed
@ -682,11 +570,8 @@ declare pad_typ_name_def [simp]
lemma typ_name_array_tag_n:
"typ_name (array_tag_n n :: ('a ::c_type ['b :: finite]) field_desc typ_desc) =
typ_name (typ_info_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b set))"
apply (induct n)
apply (clarsimp simp: array_tag_n.simps typ_uinfo_t_def)
apply (clarsimp simp: array_tag_n.simps typ_uinfo_t_def)
done
typ_name (typ_info_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b set))"
by (induct n; clarsimp simp: array_tag_n.simps typ_uinfo_t_def)
lemma typ_name_array [simp]:
"typ_name (typ_info_t TYPE('a::c_type['b :: finite])) =

2882
tools/c-parser/umm_heap/TypHeap.thy
View File

File diff suppressed because it is too large Load Diff

8
tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy
View File

@ -95,10 +95,10 @@ begin
lemma len8_size:
"len_of TYPE('a) div 8 < addr_card"
apply(subgoal_tac "len_of TYPE('a) \<le> 128")
apply(simp add: addr_card)
apply(rule len8_width)
done
apply(subgoal_tac "len_of TYPE('a) \<le> 128")
apply(simp add: addr_card)
apply(rule len8_width)
done
lemma len8_dv8:
"8 dvd len_of TYPE('a)"