Theory Generic_Memory
section ‹Memory Model›
theory Generic_Memory
imports NEMonad
begin
subsection ‹Miscellaneous›
definition "i_nth xs i ≡ if i∈{0..<int (length xs)} then xs!nat i else undefined"
definition "i_upd xs i x ≡ if i∈{0..<int (length xs)} then xs[nat i:=x] else xs"
lemma i_nth_simp[simp]:
"0≤i ⟹ nat i < length xs ⟹ i_nth xs i = xs!nat i"
"i<0 ⟹ i_nth xs i = undefined"
"length xs ≤ nat i ⟹ i_nth xs i = undefined"
by (auto simp: i_nth_def)
lemma i_upd_simp[simp]:
"0≤i ⟹ nat i < length xs ⟹ i_upd xs i v = xs[nat i:=v]"
"i<0 ⟹ i_upd xs i v = xs"
"length xs ≤ nat i ⟹ i_upd xs i v = xs"
"length (i_upd xs i v) = length xs"
by (auto simp: i_upd_def)
lemma i_get_upd_lens_laws[simp]:
"0≤i ⟹ nat i<length xs ⟹ i_nth (i_upd xs i x) i= x"
"i_upd xs i (i_nth xs i) = xs"
"i_upd (i_upd xs i y) i x = i_upd xs i x"
"i≠j ⟹ i_nth (i_upd xs i x) j = i_nth xs j"
by (auto simp: i_upd_def i_nth_def)
definition list_combine where
"list_combine xs⇩1 I xs⇩2 ≡ map (λi. if i∈I then xs⇩2!i else xs⇩1!i) [0..<length xs⇩1 ]"
lemma nth_undefined: "¬i<length xs ⟹ xs!i = undefined (i-length xs)"
apply (induction xs arbitrary: i)
apply (simp add: nth_def)
by auto
lemma list_combine_nth: "length xs⇩1 = length xs⇩2 ⟹ list_combine xs⇩1 I xs⇩2 ! i = (if i∈I then xs⇩2!i else xs⇩1!i)"
unfolding list_combine_def
apply (cases "i<length xs⇩2")
subgoal by (auto simp: )
subgoal by (simp add: nth_undefined)
done
lemma list_combine_length[simp]: "length (list_combine xs⇩1 I xs⇩2) = length xs⇩1"
by (auto simp: list_combine_def)
lemma list_combine_inth: "length xs⇩1 = length xs⇩2 ⟹ i_nth (list_combine xs⇩1 I xs⇩2) i = (if nat i∈I then i_nth xs⇩2 i else i_nth xs⇩1 i)"
apply (cases "0≤i"; simp)
apply (cases "nat i < length xs⇩1"; auto simp: list_combine_nth)
done
subsection ‹Memory Type Definition›
text ‹We define the memory model abstracted over the value type first.
Only later, we instantiate the value type with LLVM specific values
›