theory Recycle_C

lemma power_user_page_foldl_zero_ranges:
  " \<forall>p<2 ^ (pageBitsForSize sz - pageBits).
      hrs_htd hrs \<Turnstile>\<^sub>t (Ptr (ptr + of_nat p * 0x1000) :: user_data_C ptr)
    \<Longrightarrow> zero_ranges_are_zero rngs hrs
    \<Longrightarrow> zero_ranges_are_zero rngs
        (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (Ptr x) (user_data_C (arr x)) s) s
            (map (\<lambda>n. ptr + of_nat n * 0x1000) [0..<2 ^ (pageBitsForSize sz - pageBits)]))
            hrs)" apply (simp add: foldl_conv_fold hrs_mem_update_fold_eq) apply (rule conjunct1) apply (rule fold_invariant[where P="\<lambda>hrs'. zero_ranges_are_zero rngs hrs'
          \<and> hrs_htd hrs' = hrs_htd hrs"
      and xs=xs and Q="\<lambda>x. x \<in> set xs" for xs], simp_all) apply (subst zero_ranges_are_zero_update, simp_all) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p<2 ^ (pageBitsForSize sz - pageBits). hrs_htd hrs \<Turnstile>\<^sub>t PTR(user_data_C) (ptr + word_of_nat p * 0x1000); zero_ranges_are_zero rngs hrs\<rbrakk> \<Longrightarrow> zero_ranges_are_zero rngs (hrs_mem_update (\<lambda>s. foldl (\<lambda>s x. heap_update (PTR(user_data_C) x) (user_data_C (arr x)) s) s (map (\<lambda>n. ptr + word_of_nat n * 0x1000) [0..<2 ^ (pageBitsForSize sz - pageBits)])) hrs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p<2 ^ (pageBitsForSize sz - pageBits). hrs_htd hrs \<Turnstile>\<^sub>t PTR(user_data_C) (ptr + word_of_nat p * 0x1000); zero_ranges_are_zero rngs hrs\<rbrakk> \<Longrightarrow> zero_ranges_are_zero rngs (fold (hrs_mem_update \<circ> (\<lambda>x. heap_update (PTR(user_data_C) x) (user_data_C (arr x)))) (map (\<lambda>n. ptr + word_of_nat n * 0x1000) [0..<2 ^ (pageBitsForSize sz - pageBits)]) hrs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p<2 ^ (pageBitsForSize sz - pageBits). hrs_htd hrs \<Turnstile>\<^sub>t PTR(user_data_C) (ptr + word_of_nat p * 0x1000); zero_ranges_are_zero rngs hrs\<rbrakk> \<Longrightarrow> zero_ranges_are_zero rngs (fold (hrs_mem_update \<circ> (\<lambda>x. heap_update (PTR(user_data_C) x) (user_data_C (arr x)))) (map (\<lambda>n. ptr + word_of_nat n * 0x1000) [0..<2 ^ (pageBitsForSize sz - pageBits)]) hrs) \<and> ?Q proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>\<forall>p<2 ^ (pageBitsForSize sz - pageBits). hrs_htd hrs \<Turnstile>\<^sub>t PTR(user_data_C) (ptr + word_of_nat p * 0x1000); zero_ranges_are_zero rngs hrs; x \<in> (\<lambda>x. ptr + word_of_nat x * 0x1000) ` {0..<2 ^ (pageBitsForSize sz - pageBits)}; zero_ranges_are_zero rngs s \<and> hrs_htd s = hrs_htd hrs\<rbrakk> \<Longrightarrow> zero_ranges_are_zero rngs (hrs_mem_update (heap_update (PTR(user_data_C) x) (user_data_C (arr x))) s) proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>\<forall>p<2 ^ (pageBitsForSize sz - pageBits). hrs_htd hrs \<Turnstile>\<^sub>t PTR(user_data_C) (ptr + word_of_nat p * 0x1000); zero_ranges_are_zero rngs hrs; x \<in> (\<lambda>x. ptr + word_of_nat x * 0x1000) ` {0..<2 ^ (pageBitsForSize sz - pageBits)}; zero_ranges_are_zero rngs s \<and> hrs_htd s = hrs_htd hrs\<rbrakk> \<Longrightarrow> hrs_htd hrs \<Turnstile>\<^sub>t PTR(user_data_C) x proof (prove)
goal:
No subgoals!