theory Retype_DP

lemma create_objects_mapM_x:
  "create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids " proof (induct 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 (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. create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids proof (state)
goal (2 subgoals):
 1. create_objects [] (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) []
 2. \<And>a ids. create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids \<Longrightarrow> create_objects (a # ids) (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) (a # ids) proof (state)
this:


goal (2 subgoals):
 1. create_objects [] (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) []
 2. \<And>a ids. create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids \<Longrightarrow> create_objects (a # ids) (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) (a # ids) proof (prove)
goal (1 subgoal):
 1. create_objects [] (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) [] proof (state)
this:
create_objects [] (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) []

goal (1 subgoal):
 1. \<And>a ids. create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids \<Longrightarrow> create_objects (a # ids) (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) (a # ids) proof (state)
goal (1 subgoal):
 1. \<And>a ids. create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids \<Longrightarrow> create_objects (a # ids) (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) (a # ids) proof (state)
this:
create_objects ids_ (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids_

goal (1 subgoal):
 1. \<And>a ids. create_objects ids (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids \<Longrightarrow> create_objects (a # ids) (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) (a # ids) proof (prove)
goal (1 subgoal):
 1. create_objects (a_ # ids_) (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) (a_ # ids_) proof (prove)
goal (1 subgoal):
 1. create_objects (a_ # ids_) (Some obj) = do y <- create_objects [a_] (Some obj);
mapM_x (\<lambda>id. create_objects [id] (Some obj)) ids_
od proof (prove)
goal (1 subgoal):
 1. create_objects (a_ # ids_) (Some obj) = do y <- create_objects [a_] (Some obj);
create_objects ids_ (Some obj)
od proof (prove)
goal (1 subgoal):
 1. \<And>x. create_objects (a_ # ids_) (Some obj) x = (do y <- create_objects [a_] (Some obj);
create_objects 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_ # ids_) (Some obj) x = (do y <- create_objects [a_] (Some obj);
create_objects 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> 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> 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> 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> 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 (a_ # ids_) (Some obj) = mapM_x (\<lambda>id. create_objects [id] (Some obj)) (a_ # ids_)

goal:
No subgoals!