theory Arch_C

lemma framesize_from_H_eq_eq:
  "(framesize_from_H v = v') = (v' < 4 \<and> gen_framesize_to_H v' = v)" apply (rule iffI) apply (clarsimp simp: framesize_from_to_H) apply (simp add: framesize_from_H_def vm_page_size_defs split: vmpage_size.split) apply (clarsimp simp: gen_framesize_to_H_eq_from_H) apply (simp add: gen_framesize_to_H_def framesize_from_H_def split: if_split) apply (clarsimp simp: vm_page_size_defs) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (framesize_from_H v = v') = (v' < 4 \<and> gen_framesize_to_H v' = v) proof (prove)
goal (2 subgoals):
 1. framesize_from_H v = v' \<Longrightarrow> v' < 4 \<and> gen_framesize_to_H v' = v
 2. v' < 4 \<and> gen_framesize_to_H v' = v \<Longrightarrow> framesize_from_H v = v' proof (prove)
goal (2 subgoals):
 1. v' = framesize_from_H v \<Longrightarrow> framesize_from_H v < 4
 2. v' < 4 \<and> gen_framesize_to_H v' = v \<Longrightarrow> framesize_from_H v = v' proof (prove)
goal (1 subgoal):
 1. v' < 4 \<and> gen_framesize_to_H v' = v \<Longrightarrow> framesize_from_H v = v' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>framesize_from_H v < 4; v' = framesize_from_H v\<rbrakk> \<Longrightarrow> framesize_from_H (gen_framesize_to_H (framesize_from_H v)) = framesize_from_H v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) < 4; v' = (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)\<rbrakk> \<Longrightarrow> (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<longrightarrow> (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage \<longrightarrow> (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) < 4; v' = (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection); (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<noteq> 2; (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<noteq> 1; (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<noteq> 0\<rbrakk> \<Longrightarrow> (case v of local.ARMSmallPage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | local.ARMLargePage \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage | local.ARMSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection | local.ARMSuperSection \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) = 3 proof (prove)
goal:
No subgoals!