arm crefine: mark some lemmas as FIXME.

There are some good simp set candidates as well as ones that should be
moved.

proof/crefine/ARM/Finalise_C.thy

@@ -598,6 +598,8 @@ lemma cap_to_H_NTFNCap_tag:
   apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm)
      by (simp_all add: Let_def cap_lift_def split: if_splits)
 
+(* FIXME: lots of places end up unfolding option_to_ptr_def and option_to_0_def.
+   Create some suitable simp rules instead. *)
 lemma option_to_ptr_not_NULL:
   "option_to_ptr x \<noteq> NULL \<Longrightarrow> x \<noteq> None"
   by (auto simp: option_to_ptr_def option_to_0_def split: option.splits)

proof/crefine/ARM/Retype_C.thy

@@ -306,6 +306,7 @@ lemma lift_t_retyp_heap_same:
   apply simp
   done
 
+(* FIXME: Move to LemmaBucket_C. Stopped by: simp rules. *)
 lemma lift_t_retyp_heap_same_rep0:
   fixes p :: "'a :: mem_type ptr"
   assumes gp: "g p"
@@ -319,6 +320,7 @@ lemma lift_t_retyp_heap_same_rep0:
   apply simp
   done
 
+(* FIXME: Move to LemmaBucket_C. Stopped by: simp rules. *)
 lemma lift_t_retyp_heap_other2:
   fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
   assumes orth: "{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val p'..+size_of TYPE('b)} = {}"

proof/crefine/ARM/StateRelation_C.thy

@@ -20,6 +20,7 @@ definition
 definition
   "array_relation r n a c \<equiv> \<forall>i \<le> n. r (a i) (index c (unat i))"
 
+(* FIXME: this gets unfolded a lot. Consider adding the obvious simp rules. *)
 definition
   "option_to_ptr \<equiv> Ptr o option_to_0"