Theory list_reverse_norm
theory list_reverse_norm
imports "AutoCorres2.CTranslation" "MachineWords"
begin
declare sep_conj_ac [simp add]
declare hrs_simps [simp add]
primrec
list :: "machine_word typ_heap ⇒ machine_word list ⇒ machine_word ptr ⇒ bool"
where
"list h [] i = (i = Ptr 0)"
| "list h (x#xs) i =
(∃j. ptr_val i = x ∧ x≠0 ∧ h i = Some j ∧ list h xs (Ptr j))"
lemma list_empty [simp]:
"list h xs (Ptr 0) = (xs = [])"
by (induct xs) auto
lemma list_ptr_aligned:
"list (lift_t_c s) xs p ⟹ ptr_aligned p"
by (induct xs) (auto dest: lift_t_g c_guard_ptr_aligned)
lemma list_in [simp]:
"⋀p. ⟦ list h xs p; p ≠ Ptr 0 ⟧ ⟹ ptr_val p ∈ set xs"
by (induct xs) auto
lemma list_non_NULL:
"ptr_val p ≠ 0 ⟹
list h xs p = (∃ys q. xs=ptr_val p#ys ∧ h p=Some q ∧ list h ys (Ptr q))"
by (cases xs) auto
lemma list_unique:
"⋀ys p. list h xs p ⟹ list h ys p ⟹ xs = ys"
by (induct xs) (auto simp add: list_non_NULL)
lemma list_append_Ex:
"⋀p ys. list h (xs@ys) p ⟹ (∃q. list h ys q)"
by (induct xs) auto
lemma list_distinct [simp]:
"⋀p. list h xs p ⟹ distinct xs"
apply (induct xs)
apply simp
apply (clarsimp dest!: split_list)
apply (frule list_append_Ex)
apply (auto dest: list_unique)
done
lemma in_list_Some:
"⋀p. ⟦ list h xs p; ptr_val q ∈ set xs ⟧ ⟹ ∃x. h q = Some x"
by (induct xs) auto
lemma in_list_valid [simp]:
"⟦ list (lift_t_c (h,d)) xs p; ptr_val q ∈ set xs ⟧
⟹ d ⊨⇩t (q::machine_word ptr)"
by (auto dest: in_list_Some simp: lift_t_if split: if_split_asm)
lemma list_restrict:
"⋀s S h. Ptr`set ps ⊆ S ⟹ list (h|`S) ps s = list h ps s"
by (induct ps) (auto simp: restrict_map_def)
lemma list_restrict_dom:
"list (h|`(Ptr`set ps)) ps s = list h ps s"
by (simp add: list_restrict)
lemma list_heapE:
"⟦ list h xs p; h'|`(Ptr`set xs) = h|`(Ptr`set xs) ⟧ ⟹ list h' xs p"
by (subst list_restrict_dom [symmetric]) (simp add: list_restrict_dom)
lemma list_heap_update_ignore [simp]:
"ptr_val x ∉ set xs ⟹ list (h (x := Some v)) xs p = list h xs p"
by (cases x) (auto elim: list_heapE)
declare typ_simps [simp]