theory Retype_C

lemma update_ti_t_array_tag_n_rep:
  fixes x :: "'a :: c_type ['b :: finite]"
  shows "\<lbrakk> bs = replicate (n * size_td (typ_info_t TYPE('a))) v; n \<le> card (UNIV  :: 'b set) \<rbrakk> \<Longrightarrow>
  update_ti_t (array_tag_n n) bs x =
  foldr (\<lambda>n arr. Arrays.update arr n
        (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (index arr n)))
        [0..<n] x" apply (induct n arbitrary: bs x) apply (simp add: array_tag_n_eq) apply (simp add: array_tag_n_eq size_td_map_list iffD2 [OF linorder_min_same1] field_simps
    cong: if_cong ) apply (simp add: update_ti_adjust_ti) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bs = replicate (n * size_td (typ_info_t TYPE('a))) v; n \<le> CARD('b)\<rbrakk> \<Longrightarrow> update_ti_t (array_tag_n n) bs x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<n] x proof (prove)
goal (2 subgoals):
 1. \<And>bs x. \<lbrakk>bs = replicate (0 * size_td (typ_info_t TYPE('a))) v; 0 \<le> CARD('b)\<rbrakk> \<Longrightarrow> update_ti_t (array_tag_n 0) bs x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<0] x
 2. \<And>n bs x. \<lbrakk>\<And>bs x. \<lbrakk>bs = replicate (n * size_td (typ_info_t TYPE('a))) v; n \<le> CARD('b)\<rbrakk> \<Longrightarrow> update_ti_t (array_tag_n n) bs x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<n] x; bs = replicate (Suc n * size_td (typ_info_t TYPE('a))) v; Suc n \<le> CARD('b)\<rbrakk> \<Longrightarrow> update_ti_t (array_tag_n (Suc n)) bs x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<Suc n] x proof (prove)
goal (1 subgoal):
 1. \<And>n bs x. \<lbrakk>\<And>bs x. \<lbrakk>bs = replicate (n * size_td (typ_info_t TYPE('a))) v; n \<le> CARD('b)\<rbrakk> \<Longrightarrow> update_ti_t (array_tag_n n) bs x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<n] x; bs = replicate (Suc n * size_td (typ_info_t TYPE('a))) v; Suc n \<le> CARD('b)\<rbrakk> \<Longrightarrow> update_ti_t (array_tag_n (Suc n)) bs x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<Suc n] x proof (prove)
goal (1 subgoal):
 1. \<And>n bs x. \<lbrakk>\<And>bs x. bs = replicate (n * size_td (typ_info_t TYPE('a))) v \<Longrightarrow> update_ti_list_t (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..<n]) (replicate (n * size_td (typ_info_t TYPE('a))) v) x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<n] x; bs = replicate (size_td (typ_info_t TYPE('a)) + n * size_td (typ_info_t TYPE('a))) v; Suc n \<le> CARD('b)\<rbrakk> \<Longrightarrow> foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<n] (update_ti_t (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate (size_td (typ_info_t TYPE('a))) v) x) = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<n] (Arrays.update x n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (x.[n]))) proof (prove)
goal:
No subgoals!