theory Syscall_C

lemma scast_maxIRQ_is_less:
  fixes uc :: "irq \<Rightarrow> 16 word"
  and uc' :: "16 word\<Rightarrow> 32 sword"
  and b :: irq
  shows
  "(Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b \<Longrightarrow> scast Kernel_C.maxIRQ < b" apply (simp add: Kernel_C.maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp) apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<le> uint b"; (simp only: Kernel_C.maxIRQ_def)?) apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<noteq> uint b"; (simp only: Kernel_C.maxIRQ_def)?) apply (simp ) apply (subst  uint_is_up_compose[where uc="(ucast :: irq \<Rightarrow> 16 word)" and uc' = "(ucast :: 16 word \<Rightarrow> 32 sword)",symmetric];
         (simp add:  is_up_def target_size source_size )?) apply fastforce apply (subst sint_ucast_uint_pred[where uc="(ucast :: irq \<Rightarrow> 16 word)" and uc' = "(ucast :: 16 word \<Rightarrow> 32 sword)"];
        (simp add:  is_up_def target_size source_size  )?) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Kernel_C.maxIRQ <s (UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)) b \<Longrightarrow> SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ < b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024\<rbrakk> \<Longrightarrow> 159 < uint b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024; sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b\<rbrakk> \<Longrightarrow> 159 < uint b
 2. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024\<rbrakk> \<Longrightarrow> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024; sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b; sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<noteq> uint b\<rbrakk> \<Longrightarrow> 159 < uint b
 2. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024; sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b\<rbrakk> \<Longrightarrow> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<noteq> uint b
 3. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024\<rbrakk> \<Longrightarrow> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024; sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b\<rbrakk> \<Longrightarrow> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<noteq> uint b
 2. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024\<rbrakk> \<Longrightarrow> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024; 159 \<le> uint b\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32 signed) = UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16)
 2. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024\<rbrakk> \<Longrightarrow> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024\<rbrakk> \<Longrightarrow> sint (UCAST(32 signed \<rightarrow> 32 signed) 0x9F) \<le> uint b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>159 \<le> sint (UCAST(10 \<rightarrow> 32 signed) b); uint (UCAST(10 \<rightarrow> 32 signed) b) < 4294967296; uint (UCAST(10 \<rightarrow> 32 signed) b) \<noteq> 159; uint b < 1024\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32 signed) = UCAST(16 \<rightarrow> 32 signed) \<circ> UCAST(10 \<rightarrow> 16) proof (prove)
goal:
No subgoals!