theory Retype_DP

lemma create_objects_mapM_x':
  "ids = map (\<lambda>x. {x}) ids' \<Longrightarrow>
  create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids' " apply simp proof (induct ids' arbitrary: ids) case Nil show ?case by (simp add:create_objects_def mapM_x_Nil simpler_modify_def return_def) next case Cons show ?case apply (simp add:mapM_x_Cons) apply (subst local.Cons[symmetric]) apply simp apply (rule ext) apply (case_tac x) apply (clarsimp simp:create_objects_def simpler_modify_def bind_def) apply (rule ext) apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ids = map (\<lambda>x. {x}) ids' \<Longrightarrow> create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids' proof (prove)
goal (1 subgoal):
 1. ids = map (\<lambda>x. {x}) ids' \<Longrightarrow> create_objects (map (\<lambda>x. {x}) ids') (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids' proof (state)
goal (2 subgoals):
 1. \<And>ids. ids = map (\<lambda>x. {x}) [] \<Longrightarrow> create_objects (map (\<lambda>x. {x}) []) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) []
 2. \<And>a ids' ids. \<lbrakk>\<And>ids. ids = map (\<lambda>x. {x}) ids' \<Longrightarrow> create_objects (map (\<lambda>x. {x}) ids') (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids'; ids = map (\<lambda>x. {x}) (a # ids')\<rbrakk> \<Longrightarrow> create_objects (map (\<lambda>x. {x}) (a # ids')) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (a # ids') proof (state)
this:
ids = map (\<lambda>x. {x}) []

goal (2 subgoals):
 1. \<And>ids. ids = map (\<lambda>x. {x}) [] \<Longrightarrow> create_objects (map (\<lambda>x. {x}) []) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) []
 2. \<And>a ids' ids. \<lbrakk>\<And>ids. ids = map (\<lambda>x. {x}) ids' \<Longrightarrow> create_objects (map (\<lambda>x. {x}) ids') (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids'; ids = map (\<lambda>x. {x}) (a # ids')\<rbrakk> \<Longrightarrow> create_objects (map (\<lambda>x. {x}) (a # ids')) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (a # ids') proof (prove)
goal (1 subgoal):
 1. create_objects (map (\<lambda>x. {x}) []) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) [] proof (state)
this:
create_objects (map (\<lambda>x. {x}) []) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) []

goal (1 subgoal):
 1. \<And>a ids' ids. \<lbrakk>\<And>ids. ids = map (\<lambda>x. {x}) ids' \<Longrightarrow> create_objects (map (\<lambda>x. {x}) ids') (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids'; ids = map (\<lambda>x. {x}) (a # ids')\<rbrakk> \<Longrightarrow> create_objects (map (\<lambda>x. {x}) (a # ids')) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (a # ids') proof (state)
goal (1 subgoal):
 1. \<And>a ids' ids. \<lbrakk>\<And>ids. ids = map (\<lambda>x. {x}) ids' \<Longrightarrow> create_objects (map (\<lambda>x. {x}) ids') (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids'; ids = map (\<lambda>x. {x}) (a # ids')\<rbrakk> \<Longrightarrow> create_objects (map (\<lambda>x. {x}) (a # ids')) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (a # ids') proof (state)
this:
?ids = map (\<lambda>x. {x}) ids'_ \<Longrightarrow> create_objects (map (\<lambda>x. {x}) ids'_) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids'_
ids = map (\<lambda>x. {x}) (a_ # ids'_)

goal (1 subgoal):
 1. \<And>a ids' ids. \<lbrakk>\<And>ids. ids = map (\<lambda>x. {x}) ids' \<Longrightarrow> create_objects (map (\<lambda>x. {x}) ids') (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids'; ids = map (\<lambda>x. {x}) (a # ids')\<rbrakk> \<Longrightarrow> create_objects (map (\<lambda>x. {x}) (a # ids')) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (a # ids') proof (prove)
goal (1 subgoal):
 1. create_objects (map (\<lambda>x. {x}) (a_ # ids'_)) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (a_ # ids'_) proof (prove)
goal (1 subgoal):
 1. create_objects ({a_} # map (\<lambda>x. {x}) ids'_) (Some obj) = do y <- create_objects [{a_}] (Some obj);
mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) ids'_
od proof (prove)
goal (2 subgoals):
 1. \<And>y aa. ?ids = map (\<lambda>x. {x}) ids'_
 2. create_objects ({a_} # map (\<lambda>x. {x}) ids'_) (Some obj) = do y <- create_objects [{a_}] (Some obj);
create_objects (map (\<lambda>x. {x}) ids'_) (Some obj)
od proof (prove)
goal (1 subgoal):
 1. create_objects ({a_} # map (\<lambda>x. {x}) ids'_) (Some obj) = do y <- create_objects [{a_}] (Some obj);
create_objects (map (\<lambda>x. {x}) ids'_) (Some obj)
od proof (prove)
goal (1 subgoal):
 1. \<And>x. create_objects ({a_} # map (\<lambda>x. {x}) ids'_) (Some obj) x = (do y <- create_objects [{a_}] (Some obj);
create_objects (map (\<lambda>x. {x}) ids'_) (Some obj)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x cdl_arch cdl_objects cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. x = \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objects, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> \<Longrightarrow> create_objects ({a_} # map (\<lambda>x. {x}) ids'_) (Some obj) x = (do y <- create_objects [{a_}] (Some obj);
create_objects (map (\<lambda>x. {x}) ids'_) (Some obj)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain. (\<lambda>x. if x = a_ \<or> {x} \<in> (\<lambda>x. {x}) ` set ids'_ then Some obj else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x) = (\<lambda>x. if {x} \<in> (\<lambda>x. {x}) ` set ids'_ then Some obj else cdl_objects (\<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>\<lparr>cdl_objects := \<lambda>x. if x = a_ then Some obj else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x\<rparr>) x) proof (prove)
goal (1 subgoal):
 1. \<And>cdl_arch cdl_objectsa cdl_cdt cdl_current_thread cdl_irq_node cdl_asid_table cdl_current_domain x. (if x = a_ \<or> {x} \<in> (\<lambda>x. {x}) ` set ids'_ then Some obj else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x) = (if {x} \<in> (\<lambda>x. {x}) ` set ids'_ then Some obj else cdl_objects (\<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr>\<lparr>cdl_objects := \<lambda>x. if x = a_ then Some obj else cdl_objects \<lparr>cdl_arch = cdl_arch, cdl_objects = cdl_objectsa, cdl_cdt = cdl_cdt, cdl_current_thread = cdl_current_thread, cdl_irq_node = cdl_irq_node, cdl_asid_table = cdl_asid_table, cdl_current_domain = cdl_current_domain\<rparr> x\<rparr>) x) proof (prove)
goal:
No subgoals! proof (state)
this:
create_objects (map (\<lambda>x. {x}) (a_ # ids'_)) (Some obj) = mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (a_ # ids'_)

goal:
No subgoals!