theory Arch_R

lemma retype_region2_ext_retype_region_ArchObject:
  "retype_region ptr n us (ArchObject x)=
  retype_region2 ptr n us (ArchObject x)" apply (rule ext) apply (simp add:retype_region_def retype_region2_def bind_assoc
    retype_region2_ext_def retype_region_ext_def default_ext_def) apply (rule ext) apply (intro monad_eq_split_tail ext)+ apply simp apply simp apply (simp add:gets_def get_def bind_def return_def simpler_modify_def ) apply (rule_tac x = xc in fun_cong) apply (rule_tac f = do_extended_op in arg_cong) apply (rule ext) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retype_region ptr n us (ArchObject x) = retype_region2 ptr n us (ArchObject x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. retype_region ptr n us (ArchObject x) xa = retype_region2 ptr n us (ArchObject x) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. do xb <- gets kheap;
xc <- do_extended_op (do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) ekh))
od);
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x) xa us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xb));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])
od = do xb <- gets kheap;
xc <- do_extended_op (modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]))));
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x) xa us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xb));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])
od proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. (do xb <- gets kheap;
xc <- do_extended_op (do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) ekh))
od);
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x) xa us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xb));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])
od) xaa = (do xb <- gets kheap;
xc <- do_extended_op (modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]))));
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x) xa us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xb));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])
od) xaa proof (prove)
goal (4 subgoals):
 1. \<And>xa xaa xb xc xd xe y xf. return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xf = return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xf
 2. \<And>xa xaa xb xc xd xe. modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x) xa us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xb)) xe = modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x) xa us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xb)) xe
 3. \<And>xa xaa xb xc. do_extended_op (do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) ekh))
od) xc = do_extended_op (modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])))) xc
 4. \<And>x xa. gets kheap xa = gets kheap xa proof (prove)
goal (3 subgoals):
 1. \<And>xa xaa xb xc xd xe. modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x) xa us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xb)) xe = modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x) xa us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) xb)) xe
 2. \<And>xa xaa xb xc. do_extended_op (do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) ekh))
od) xc = do_extended_op (modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])))) xc
 3. \<And>x xa. gets kheap xa = gets kheap xa proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa xb xc. do_extended_op (do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) ekh))
od) xc = do_extended_op (modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])))) xc
 2. \<And>x xa. gets kheap xa = gets kheap xa proof (prove)
goal (2 subgoals):
 1. \<And>xc. do_extended_op (\<lambda>s. ({((), ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) (ekheap s)) s)}, False)) xc = do_extended_op (\<lambda>s. ({((), ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])) s)}, False)) xc
 2. \<And>x xa. gets kheap xa = gets kheap xa proof (prove)
goal (2 subgoals):
 1. \<And>xc. do_extended_op (\<lambda>s. ({((), ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) (ekheap s)) s)}, False)) = do_extended_op (\<lambda>s. ({((), ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])) s)}, False))
 2. \<And>x xa. gets kheap xa = gets kheap xa proof (prove)
goal (2 subgoals):
 1. \<And>xc. (\<lambda>s. ({((), ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) (ekheap s)) s)}, False)) = (\<lambda>s. ({((), ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])) s)}, False))
 2. \<And>x xa. gets kheap xa = gets kheap xa proof (prove)
goal (2 subgoals):
 1. \<And>xc s. ({((), ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n]) (ekheap s)) s)}, False) = ({((), ekheap_update (foldr (\<lambda>p ekh. ekh(p := None)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x) us)) [0..<n])) s)}, False)
 2. \<And>x xa. gets kheap xa = gets kheap xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa. gets kheap xa = gets kheap xa proof (prove)
goal:
No subgoals!