theory StoreWord_C

lemma update_ti_t_acc_foo:
  "\<And>acc f v. \<lbrakk> \<And>a ys v. \<lbrakk> a \<in> set adjs; length ys = size_td_pair a \<rbrakk>
                \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v);
              \<And>a. size_td_pair (f a) = size_td_pair a \<rbrakk> \<Longrightarrow>
       \<forall>xs. acc (update_ti_list_t adjs xs v) = update_ti_list_t (map f adjs) xs (acc v)" apply (simp add: update_ti_list_t_def size_td_list_map2 split: if_split) apply (induct adjs) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>acc f v. \<lbrakk>\<And>a ys v. \<lbrakk>a \<in> set adjs; length ys = size_td_pair a\<rbrakk> \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v); \<And>a. size_td_pair (f a) = size_td_pair a\<rbrakk> \<Longrightarrow> \<forall>xs. acc (update_ti_list_t adjs xs v) = update_ti_list_t (map f adjs) xs (acc v) proof (prove)
goal (1 subgoal):
 1. \<And>acc f v. \<lbrakk>\<And>a ys v. \<lbrakk>a \<in> set adjs; length ys = size_td_pair a\<rbrakk> \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v); \<And>a. size_td_pair (f a) = size_td_pair a\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list adjs \<longrightarrow> acc (update_ti_list adjs xs v) = update_ti_list (map f adjs) xs (acc v) proof (prove)
goal (2 subgoals):
 1. \<And>acc f v. \<lbrakk>\<And>a ys v. \<lbrakk>a \<in> set []; length ys = size_td_pair a\<rbrakk> \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v); \<And>a. size_td_pair (f a) = size_td_pair a\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list [] \<longrightarrow> acc (update_ti_list [] xs v) = update_ti_list (map f []) xs (acc v)
 2. \<And>x1 adjs acc f v. \<lbrakk>\<And>acc f v. \<lbrakk>\<And>a ys v. \<lbrakk>a \<in> set adjs; length ys = size_td_pair a\<rbrakk> \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v); \<And>a. size_td_pair (f a) = size_td_pair a\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list adjs \<longrightarrow> acc (update_ti_list adjs xs v) = update_ti_list (map f adjs) xs (acc v); \<And>a ys v. \<lbrakk>a \<in> set (x1 # adjs); length ys = size_td_pair a\<rbrakk> \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v); \<And>a. size_td_pair (f a) = size_td_pair a\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list (x1 # adjs) \<longrightarrow> acc (update_ti_list (x1 # adjs) xs v) = update_ti_list (map f (x1 # adjs)) xs (acc v) proof (prove)
goal (1 subgoal):
 1. \<And>x1 adjs acc f v. \<lbrakk>\<And>acc f v. \<lbrakk>\<And>a ys v. \<lbrakk>a \<in> set adjs; length ys = size_td_pair a\<rbrakk> \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v); \<And>a. size_td_pair (f a) = size_td_pair a\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list adjs \<longrightarrow> acc (update_ti_list adjs xs v) = update_ti_list (map f adjs) xs (acc v); \<And>a ys v. \<lbrakk>a \<in> set (x1 # adjs); length ys = size_td_pair a\<rbrakk> \<Longrightarrow> acc (update_ti_pair a ys v) = update_ti_pair (f a) ys (acc v); \<And>a. size_td_pair (f a) = size_td_pair a\<rbrakk> \<Longrightarrow> \<forall>xs. length xs = size_td_list (x1 # adjs) \<longrightarrow> acc (update_ti_list (x1 # adjs) xs v) = update_ti_list (map f (x1 # adjs)) xs (acc v) proof (prove)
goal:
No subgoals!