theory Syscall_DR

lemma transform_type_eq_None:
  "(transform_type a = None) \<Longrightarrow> (data_to_obj_type a = throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0))" apply (clarsimp simp:data_to_obj_type_def transform_type_def split:if_split_asm) apply (simp add:unat_arith_simps) apply (clarsimp simp:arch_data_to_obj_type_def) apply (rule conjI,arith,clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_type a = None \<Longrightarrow> data_to_obj_type a = throwError (InvalidArgument 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0; a \<noteq> 1; a \<noteq> 2; a \<noteq> 3; a \<noteq> 4; a \<noteq> 5; a \<noteq> 6; a \<noteq> 7; a \<noteq> 8; a \<noteq> 9; a \<noteq> 0xA\<rbrakk> \<Longrightarrow> (unat a = 4 \<longrightarrow> returnOk CapTableObject = throwError (InvalidArgument 0)) \<and> (unat a \<noteq> 4 \<longrightarrow> (unat a = 3 \<longrightarrow> returnOk NotificationObject = throwError (InvalidArgument 0)) \<and> (unat a \<noteq> 3 \<longrightarrow> (unat a = 2 \<longrightarrow> returnOk EndpointObject = throwError (InvalidArgument 0)) \<and> (unat a \<noteq> 2 \<longrightarrow> (unat a = Suc 0 \<longrightarrow> returnOk TCBObject = throwError (InvalidArgument 0)) \<and> (unat a \<noteq> Suc 0 \<longrightarrow> (unat a = 0 \<longrightarrow> returnOk apiobject_type.Untyped = throwError (InvalidArgument 0)) \<and> (0 < unat a \<longrightarrow> (case arch_data_to_obj_type (unat a - 5) of None \<Rightarrow> throwError (InvalidArgument 0) | Some tp \<Rightarrow> returnOk (ArchObject tp)) = throwError (InvalidArgument 0)))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < unat a; unat a \<noteq> Suc 0; unat a \<noteq> 2; unat a \<noteq> 3; unat a \<noteq> 4; unat a \<noteq> 5; unat a \<noteq> 6; unat a \<noteq> 7; unat a \<noteq> 8; unat a \<noteq> 9; unat a \<noteq> 10\<rbrakk> \<Longrightarrow> (case arch_data_to_obj_type (unat a - 5) of None \<Rightarrow> throwError (InvalidArgument 0) | Some tp \<Rightarrow> returnOk (ArchObject tp)) = throwError (InvalidArgument 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < unat a; unat a \<noteq> Suc 0; unat a \<noteq> 2; unat a \<noteq> 3; unat a \<noteq> 4; unat a \<noteq> 5; unat a \<noteq> 6; unat a \<noteq> 7; unat a \<noteq> 8; unat a \<noteq> 9; unat a \<noteq> 10\<rbrakk> \<Longrightarrow> (unat a - 5 = 5 \<longrightarrow> (unat a \<le> 5 \<longrightarrow> returnOk (ArchObject PageDirectoryObj) = throwError (InvalidArgument 0)) \<and> (\<not> unat a \<le> 5 \<longrightarrow> returnOk (ArchObject PageTableObj) = throwError (InvalidArgument 0))) \<and> (unat a - 5 \<noteq> 5 \<longrightarrow> (unat a - 5 = 4 \<longrightarrow> (unat a \<le> 5 \<longrightarrow> returnOk (ArchObject PageDirectoryObj) = throwError (InvalidArgument 0)) \<and> (\<not> unat a \<le> 5 \<longrightarrow> returnOk (ArchObject SuperSectionObj) = throwError (InvalidArgument 0))) \<and> (unat a - 5 \<noteq> 4 \<longrightarrow> (unat a - 5 = 3 \<longrightarrow> (unat a \<le> 5 \<longrightarrow> returnOk (ArchObject PageDirectoryObj) = throwError (InvalidArgument 0)) \<and> (\<not> unat a \<le> 5 \<longrightarrow> returnOk (ArchObject SectionObj) = throwError (InvalidArgument 0))) \<and> (unat a - 5 \<noteq> 3 \<longrightarrow> (unat a - 5 = 2 \<longrightarrow> (unat a \<le> 5 \<longrightarrow> returnOk (ArchObject PageDirectoryObj) = throwError (InvalidArgument 0)) \<and> (\<not> unat a \<le> 5 \<longrightarrow> returnOk (ArchObject LargePageObj) = throwError (InvalidArgument 0))) \<and> (unat a - 5 \<noteq> 2 \<longrightarrow> (unat a - 5 = Suc 0 \<longrightarrow> (unat a \<le> 5 \<longrightarrow> returnOk (ArchObject PageDirectoryObj) = throwError (InvalidArgument 0)) \<and> (\<not> unat a \<le> 5 \<longrightarrow> returnOk (ArchObject SmallPageObj) = throwError (InvalidArgument 0))) \<and> (unat a - 5 \<noteq> Suc 0 \<longrightarrow> unat a \<le> 5 \<longrightarrow> returnOk (ArchObject PageDirectoryObj) = throwError (InvalidArgument 0)))))) proof (prove)
goal:
No subgoals!