theory FieldAccessors

lemma to_bytes_array:
  "length xs = (size_of TYPE('a :: c_type) * CARD('b :: finite))
    \<Longrightarrow> to_bytes (v :: 'a['b]) xs
        = concat (map (\<lambda>i. to_bytes (index v i) (take (size_of TYPE('a))
            (drop (size_of TYPE('a) * i) xs))) [0 ..< CARD ('b)])" apply (simp add: to_bytes_def typ_info_array'
                   foldl_conv_concat[where xs=Nil, simplified, symmetric]) apply (subst fcp_eta[where g=v, symmetric], rule access_ti_list_array) apply simp apply (simp add: size_of_def) apply (clarsimp simp: size_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = size_of TYPE('a) * CARD('b) \<Longrightarrow> to_bytes v xs = concat (map (\<lambda>i. to_bytes (v.[i]) (take (size_of TYPE('a)) (drop (size_of TYPE('a) * i) xs))) [0..<CARD('b)]) proof (prove)
goal (1 subgoal):
 1. length xs = size_of TYPE('a) * CARD('b) \<Longrightarrow> access_ti_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<CARD('b)]) v xs = foldl (@) [] (map (\<lambda>i. access_ti (typ_info_t TYPE('a)) (v.[i]) (take (size_of TYPE('a)) (drop (size_of TYPE('a) * i) xs))) [0..<CARD('b)]) proof (prove)
goal (3 subgoals):
 1. length xs = size_of TYPE('a) * CARD('b) \<Longrightarrow> \<forall>n. size_td_pair (DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) = ?v3.0
 2. length xs = size_of TYPE('a) * CARD('b) \<Longrightarrow> length xs = ?v3.0 * CARD('b)
 3. length xs = size_of TYPE('a) * CARD('b) \<Longrightarrow> \<forall>m. m < CARD('b) \<and> ?v3.0 \<le> length (drop (?v3.0 * m) xs) \<longrightarrow> access_ti_pair (DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[m]) (\<lambda>x f. Arrays.update f m x)) (replicate m CHR ''1'')) (FCP (index v)) (take ?v3.0 (drop (?v3.0 * m) xs)) = access_ti (typ_info_t TYPE('a)) (v.[m]) (take (size_of TYPE('a)) (drop (size_of TYPE('a) * m) xs)) proof (prove)
goal (2 subgoals):
 1. length xs = size_of TYPE('a) * CARD('b) \<Longrightarrow> length xs = size_td (typ_info_t TYPE('a)) * CARD('b)
 2. length xs = size_of TYPE('a) * CARD('b) \<Longrightarrow> \<forall>m. m < CARD('b) \<and> size_td (typ_info_t TYPE('a)) \<le> length (drop (size_td (typ_info_t TYPE('a)) * m) xs) \<longrightarrow> access_ti_pair (DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[m]) (\<lambda>x f. Arrays.update f m x)) (replicate m CHR ''1'')) (FCP (index v)) (take (size_td (typ_info_t TYPE('a))) (drop (size_td (typ_info_t TYPE('a)) * m) xs)) = access_ti (typ_info_t TYPE('a)) (v.[m]) (take (size_of TYPE('a)) (drop (size_of TYPE('a) * m) xs)) proof (prove)
goal (1 subgoal):
 1. length xs = size_of TYPE('a) * CARD('b) \<Longrightarrow> \<forall>m. m < CARD('b) \<and> size_td (typ_info_t TYPE('a)) \<le> length (drop (size_td (typ_info_t TYPE('a)) * m) xs) \<longrightarrow> access_ti_pair (DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[m]) (\<lambda>x f. Arrays.update f m x)) (replicate m CHR ''1'')) (FCP (index v)) (take (size_td (typ_info_t TYPE('a))) (drop (size_td (typ_info_t TYPE('a)) * m) xs)) = access_ti (typ_info_t TYPE('a)) (v.[m]) (take (size_of TYPE('a)) (drop (size_of TYPE('a) * m) xs)) proof (prove)
goal:
No subgoals!