theory Untyped_DR

lemma transform_translate_type:
  "transform_type n = Some tp
      \<Longrightarrow> \<exists>v. data_to_obj_type n = returnOk v \<and> tp = translate_object_type v" apply (simp add: transform_type_def
            split: if_split_asm) apply (simp_all add: data_to_obj_type_def arch_data_to_obj_type_def) apply (auto simp add: translate_object_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_type n = Some tp \<Longrightarrow> \<exists>v. data_to_obj_type n = returnOk v \<and> tp = translate_object_type v proof (prove)
goal (11 subgoals):
 1. \<lbrakk>n = 0; UntypedType = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 0 = returnOk v \<and> UntypedType = translate_object_type v
 2. \<lbrakk>n = 1; TcbType = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 1 = returnOk v \<and> TcbType = translate_object_type v
 3. \<lbrakk>n = 2; EndpointType = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 2 = returnOk v \<and> EndpointType = translate_object_type v
 4. \<lbrakk>n = 3; NotificationType = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 3 = returnOk v \<and> NotificationType = translate_object_type v
 5. \<lbrakk>n = 4; CNodeType = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 4 = returnOk v \<and> CNodeType = translate_object_type v
 6. \<lbrakk>n = 5; PageDirectoryType = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 5 = returnOk v \<and> PageDirectoryType = translate_object_type v
 7. \<lbrakk>n = 6; FrameType 12 = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 6 = returnOk v \<and> tp = translate_object_type v
 8. \<lbrakk>n = 7; FrameType 16 = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 7 = returnOk v \<and> tp = translate_object_type v
 9. \<lbrakk>n = 8; FrameType 20 = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 8 = returnOk v \<and> tp = translate_object_type v
 10. \<lbrakk>n = 9; FrameType 24 = tp\<rbrakk> \<Longrightarrow> \<exists>v. data_to_obj_type 9 = returnOk v \<and> tp = translate_object_type v
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>n = 0; UntypedType = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk apiobject_type.Untyped = returnOk v \<and> UntypedType = translate_object_type v
 2. \<lbrakk>n = 1; TcbType = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk TCBObject = returnOk v \<and> TcbType = translate_object_type v
 3. \<lbrakk>n = 2; EndpointType = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk EndpointObject = returnOk v \<and> EndpointType = translate_object_type v
 4. \<lbrakk>n = 3; NotificationType = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk NotificationObject = returnOk v \<and> NotificationType = translate_object_type v
 5. \<lbrakk>n = 4; CNodeType = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk CapTableObject = returnOk v \<and> CNodeType = translate_object_type v
 6. \<lbrakk>n = 5; PageDirectoryType = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk (ArchObject PageDirectoryObj) = returnOk v \<and> PageDirectoryType = translate_object_type v
 7. \<lbrakk>n = 6; FrameType 12 = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk (ArchObject SmallPageObj) = returnOk v \<and> tp = translate_object_type v
 8. \<lbrakk>n = 7; FrameType 16 = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk (ArchObject LargePageObj) = returnOk v \<and> tp = translate_object_type v
 9. \<lbrakk>n = 8; FrameType 20 = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk (ArchObject SectionObj) = returnOk v \<and> tp = translate_object_type v
 10. \<lbrakk>n = 9; FrameType 24 = tp\<rbrakk> \<Longrightarrow> \<exists>v. returnOk (ArchObject SuperSectionObj) = returnOk v \<and> tp = translate_object_type v
A total of 11 subgoals... proof (prove)
goal:
No subgoals!