theory GraphRefine

lemma heap_update_list_If1:
  "length xs \<le> addr_card
   \<Longrightarrow> heap_update_list p xs hp
     = (\<lambda>x. if unat (x - p) < length xs then xs ! unat (x - p) else hp x)" apply (subst coerce_heap_update_to_heap_updates[where chunk = 1, OF _ refl]) apply simp apply (rule ext) apply (subst foldl_cong[OF refl refl]) apply (clarsimp simp: take_1_drop) apply (rule refl) apply (induct xs rule: rev_induct) apply simp apply (simp split del: if_split) apply (subst foldl_cong[OF refl refl]) apply (clarsimp simp: nth_append) apply (rule refl) apply (simp add: nth_append split del: if_split cong: if_cong) apply (auto simp: addr_card linorder_not_less less_Suc_eq take_bit_nat_eq_self unat_of_nat
              dest: word_unat.Rep_inverse') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs \<le> addr_card \<Longrightarrow> heap_update_list p xs hp = (\<lambda>x. if unat (x - p) < length xs then xs ! unat (x - p) else hp x) proof (prove)
goal (2 subgoals):
 1. length xs \<le> addr_card \<Longrightarrow> length xs = 1 * ?m
 2. length xs \<le> addr_card \<Longrightarrow> foldl (\<lambda>s n. heap_update_list (p + word_of_nat n * word_of_nat 1) (take 1 (drop (n * 1) xs)) s) hp [0..<?m] = (\<lambda>x. if unat (x - p) < length xs then xs ! unat (x - p) else hp x) proof (prove)
goal (1 subgoal):
 1. length xs \<le> addr_card \<Longrightarrow> foldl (\<lambda>s n. heap_update_list (p + word_of_nat n * word_of_nat 1) (take 1 (drop (n * 1) xs)) s) hp [0..<length xs] = (\<lambda>x. if unat (x - p) < length xs then xs ! unat (x - p) else hp x) proof (prove)
goal (1 subgoal):
 1. \<And>x. length xs \<le> addr_card \<Longrightarrow> foldl (\<lambda>s n. heap_update_list (p + word_of_nat n * word_of_nat 1) (take 1 (drop (n * 1) xs)) s) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x) proof (prove)
goal (2 subgoals):
 1. \<And>x a xa. \<lbrakk>length xs \<le> addr_card; xa \<in> set [0..<length xs]\<rbrakk> \<Longrightarrow> heap_update_list (p + word_of_nat xa * word_of_nat 1) (take 1 (drop (xa * 1) xs)) a = ?g4 x a xa
 2. \<And>x. length xs \<le> addr_card \<Longrightarrow> foldl (?g4 x) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x) proof (prove)
goal (2 subgoals):
 1. \<And>x a xa. \<lbrakk>length xs \<le> addr_card; xa < length xs\<rbrakk> \<Longrightarrow> a(p + word_of_nat xa := xs ! xa) = ?g4 x a xa
 2. \<And>x. length xs \<le> addr_card \<Longrightarrow> foldl (?g4 x) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x) proof (prove)
goal (1 subgoal):
 1. \<And>x. length xs \<le> addr_card \<Longrightarrow> foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x) proof (prove)
goal (2 subgoals):
 1. \<And>x. length [] \<le> addr_card \<Longrightarrow> foldl (\<lambda>a xa. a(p + word_of_nat xa := [] ! xa)) hp [0..<length []] x = (if unat (x - p) < length [] then [] ! unat (x - p) else hp x)
 2. \<And>x xs xa. \<lbrakk>\<And>x. length xs \<le> addr_card \<Longrightarrow> foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); length (xs @ [x]) \<le> addr_card\<rbrakk> \<Longrightarrow> foldl (\<lambda>a xa. a(p + word_of_nat xa := (xs @ [x]) ! xa)) hp [0..<length (xs @ [x])] xa = (if unat (xa - p) < length (xs @ [x]) then (xs @ [x]) ! unat (xa - p) else hp xa) proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. length xs \<le> addr_card \<Longrightarrow> foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); length (xs @ [x]) \<le> addr_card\<rbrakk> \<Longrightarrow> foldl (\<lambda>a xa. a(p + word_of_nat xa := (xs @ [x]) ! xa)) hp [0..<length (xs @ [x])] xa = (if unat (xa - p) < length (xs @ [x]) then (xs @ [x]) ! unat (xa - p) else hp xa) proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); Suc (length xs) \<le> addr_card\<rbrakk> \<Longrightarrow> (if xa = p + word_of_nat (length xs) then x else foldl (\<lambda>a xa. a(p + word_of_nat xa := (xs @ [x]) ! xa)) hp [0..<length xs] xa) = (if unat (xa - p) < Suc (length xs) then (xs @ [x]) ! unat (xa - p) else hp xa) proof (prove)
goal (2 subgoals):
 1. \<And>x xs xa a xb. \<lbrakk>\<And>x. foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); Suc (length xs) \<le> addr_card; xb \<in> set [0..<length xs]\<rbrakk> \<Longrightarrow> a(p + word_of_nat xb := (xs @ [x]) ! xb) = ?g9 x xs xa a xb
 2. \<And>x xs xa. \<lbrakk>\<And>x. foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); Suc (length xs) \<le> addr_card\<rbrakk> \<Longrightarrow> (if xa = p + word_of_nat (length xs) then x else foldl (?g9 x xs xa) hp [0..<length xs] xa) = (if unat (xa - p) < Suc (length xs) then (xs @ [x]) ! unat (xa - p) else hp xa) proof (prove)
goal (2 subgoals):
 1. \<And>x xs xa a xb. \<lbrakk>\<And>x. foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); Suc (length xs) \<le> addr_card; xb < length xs\<rbrakk> \<Longrightarrow> a(p + word_of_nat xb := xs ! xb) = ?g9 x xs xa a xb
 2. \<And>x xs xa. \<lbrakk>\<And>x. foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); Suc (length xs) \<le> addr_card\<rbrakk> \<Longrightarrow> (if xa = p + word_of_nat (length xs) then x else foldl (?g9 x xs xa) hp [0..<length xs] xa) = (if unat (xa - p) < Suc (length xs) then (xs @ [x]) ! unat (xa - p) else hp xa) proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); Suc (length xs) \<le> addr_card\<rbrakk> \<Longrightarrow> (if xa = p + word_of_nat (length xs) then x else foldl (\<lambda>a xb. a(p + word_of_nat xb := xs ! xb)) hp [0..<length xs] xa) = (if unat (xa - p) < Suc (length xs) then (xs @ [x]) ! unat (xa - p) else hp xa) proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. foldl (\<lambda>a xa. a(p + word_of_nat xa := xs ! xa)) hp [0..<length xs] x = (if unat (x - p) < length xs then xs ! unat (x - p) else hp x); Suc (length xs) \<le> addr_card\<rbrakk> \<Longrightarrow> (if xa = p + word_of_nat (length xs) then x else if unat (xa - p) < length xs then xs ! unat (xa - p) else hp xa) = (if unat (xa - p) < Suc (length xs) then if unat (xa - p) < length xs then xs ! unat (xa - p) else x else hp xa) proof (prove)
goal:
No subgoals!