theory Recycle_C

lemma coerce_heap_update_to_heap_updates':
  "n = chunk * m \<Longrightarrow>
  heap_update_list x (replicateHider n 0)
  = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s
    (map (\<lambda>n. x + (of_nat n * of_nat chunk)) [0 ..< m]))" using [[hypsubst_thin]] apply clarsimp apply (induct m arbitrary: x) apply (rule ext, simp) apply (simp add: replicateHider_def) apply (rule ext) apply (simp only: map_upt_unfold map_Suc_upt[symmetric]) apply (simp add: replicate_add[folded replicateHider_def]
                   heap_update_list_concat_unfold
                   o_def field_simps
                   length_replicate[folded replicateHider_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = chunk * m \<Longrightarrow> heap_update_list x (replicateHider n 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<m])) proof (prove)
goal (1 subgoal):
 1. n = chunk * m \<Longrightarrow> heap_update_list x (replicateHider n 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<m])) proof (prove)
goal (1 subgoal):
 1. heap_update_list x (replicateHider (chunk * m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<m])) proof (prove)
goal (2 subgoals):
 1. \<And>x. heap_update_list x (replicateHider (chunk * 0) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<0]))
 2. \<And>m x. (\<And>x. heap_update_list x (replicateHider (chunk * m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<m]))) \<Longrightarrow> heap_update_list x (replicateHider (chunk * Suc m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<Suc m])) proof (prove)
goal (2 subgoals):
 1. \<And>x s. heap_update_list x (replicateHider 0 0) s = s
 2. \<And>m x. (\<And>x. heap_update_list x (replicateHider (chunk * m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<m]))) \<Longrightarrow> heap_update_list x (replicateHider (chunk * Suc m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<Suc m])) proof (prove)
goal (1 subgoal):
 1. \<And>m x. (\<And>x. heap_update_list x (replicateHider (chunk * m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<m]))) \<Longrightarrow> heap_update_list x (replicateHider (chunk * Suc m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<Suc m])) proof (prove)
goal (1 subgoal):
 1. \<And>m x s. (\<And>x. heap_update_list x (replicateHider (chunk * m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<m]))) \<Longrightarrow> heap_update_list x (replicateHider (chunk * Suc m) 0) s = foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<Suc m]) proof (prove)
goal (1 subgoal):
 1. \<And>m x s. (\<And>x. heap_update_list x (replicateHider (chunk * m) 0) = (\<lambda>s. foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s (map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) [0..<m]))) \<Longrightarrow> heap_update_list x (replicateHider (chunk * Suc m) 0) s = foldl (\<lambda>s x. heap_update_list x (replicateHider chunk 0) s) s ((x + word_of_nat 0 * word_of_nat chunk) # map (\<lambda>n. x + word_of_nat n * word_of_nat chunk) (map Suc [0..<m])) proof (prove)
goal:
No subgoals!