theory Recycle_C

lemma clift_foldl_hrs_mem_update:
  "\<lbrakk> \<forall>x \<in> set xs. hrs_htd s \<Turnstile>\<^sub>t f x;
     \<And>x s. hrs_htd s \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) s)
                                  = g (clift s :: ('a :: c_type) ptr \<rightharpoonup> 'a) x \<rbrakk>
   \<Longrightarrow>
   clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s xs) s)
       = foldl g (clift s :: 'a ptr \<rightharpoonup> 'a) xs" using [[hypsubst_thin]] apply (cases s, clarsimp) apply (induct xs arbitrary: a b) apply (simp add: hrs_mem_update_def) apply (clarsimp simp add: hrs_mem_update_def split_def hrs_htd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. hrs_htd s \<Turnstile>\<^sub>t f x; \<And>x s. hrs_htd s \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) s) = g (clift s) x\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s xs) s) = foldl g (clift s) xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. hrs_htd s \<Turnstile>\<^sub>t f x; \<And>x s. hrs_htd s \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) s) = g (clift s) x\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s xs) s) = foldl g (clift s) xs proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>set xs. hrs_htd (a, b) \<Turnstile>\<^sub>t f x; \<And>x a b. hrs_htd (a, b) \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) (a, b)) = g (clift (a, b)) x\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s xs) (a, b)) = foldl g (clift (a, b)) xs proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>set []. hrs_htd (a, b) \<Turnstile>\<^sub>t f x; \<And>x a b. hrs_htd (a, b) \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) (a, b)) = g (clift (a, b)) x\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s []) (a, b)) = foldl g (clift (a, b)) []
 2. \<And>x1 xs a b. \<lbrakk>\<And>a b. \<lbrakk>\<forall>x\<in>set xs. hrs_htd (a, b) \<Turnstile>\<^sub>t f x; \<And>x a b. hrs_htd (a, b) \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) (a, b)) = g (clift (a, b)) x\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s xs) (a, b)) = foldl g (clift (a, b)) xs; \<forall>x\<in>set (x1 # xs). hrs_htd (a, b) \<Turnstile>\<^sub>t f x; \<And>x a b. hrs_htd (a, b) \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) (a, b)) = g (clift (a, b)) x\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s (x1 # xs)) (a, b)) = foldl g (clift (a, b)) (x1 # xs) proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs a b. \<lbrakk>\<And>a b. \<lbrakk>\<forall>x\<in>set xs. hrs_htd (a, b) \<Turnstile>\<^sub>t f x; \<And>x a b. hrs_htd (a, b) \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) (a, b)) = g (clift (a, b)) x\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s xs) (a, b)) = foldl g (clift (a, b)) xs; \<forall>x\<in>set (x1 # xs). hrs_htd (a, b) \<Turnstile>\<^sub>t f x; \<And>x a b. hrs_htd (a, b) \<Turnstile>\<^sub>t f x \<Longrightarrow> clift (hrs_mem_update (heap_update (f x) v) (a, b)) = g (clift (a, b)) x\<rbrakk> \<Longrightarrow> clift (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (f x) v s) s (x1 # xs)) (a, b)) = foldl g (clift (a, b)) (x1 # xs) proof (prove)
goal:
No subgoals!