theory Finalise_C

lemma irq_opt_relation_Some_ucast_left:
  "\<lbrakk> x && mask 10 = x; ucast x \<le> (ucast Kernel_C.maxIRQ :: 10 word) \<or> x \<le> (ucast Kernel_C.maxIRQ :: machine_word) \<rbrakk>
    \<Longrightarrow> irq_opt_relation (Some (ucast x)) x" apply (rule_tac P = "%y. irq_opt_relation (Some (ucast x)) y" in subst[rotated]) apply (rule irq_opt_relation_Some_ucast[rotated]) apply simp+ apply (rule word_eqI) apply (drule_tac f = "%x. test_bit x n" in arg_cong) apply (auto simp: nth_ucast word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> irq_opt_relation (Some (UCAST(32 \<rightarrow> 10) x)) x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> irq_opt_relation (Some (UCAST(32 \<rightarrow> 10) x)) ?s
 2. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> ?s = x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ
 2. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> x && mask 10 = x
 3. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) = x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) = x proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> n < size (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)) \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) !! n = x !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; (x && mask 10) !! n = x !! n\<rbrakk> \<Longrightarrow> n < size (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)) \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) !! n = x !! n proof (prove)
goal:
No subgoals!