theory Arch_C

lemma cpde_relation_invalid:
 "cpde_relation pdea pde \<Longrightarrow> (pde_get_tag pde = scast pde_pde_invalid) = isInvalidPDE pdea" apply (simp add: cpde_relation_def Let_def) apply (simp add: pde_pde_invalid_lift) apply (case_tac pdea, simp_all add: isInvalidPDE_def) [1] apply clarsimp apply (simp add: pde_pde_invalid_lift_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cpde_relation pdea pde \<Longrightarrow> (pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid) = isInvalidPDE pdea proof (prove)
goal (1 subgoal):
 1. case pdea of ARM_H.InvalidPDE \<Rightarrow> \<exists>inv. pde_lift pde = Some (Pde_pde_invalid inv) | ARM_H.PageTablePDE frame parity domain \<Rightarrow> pde_lift pde = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = frame, P_CL = of_bool parity, Domain_CL = domain\<rparr>) | ARM_H.SectionPDE frame parity domain cacheable global xn rights \<Rightarrow> pde_lift pde = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 0, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = domain, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) | ARM_H.SuperSectionPDE frame parity cacheable global xn rights \<Rightarrow> pde_lift pde = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 1, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = 0, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) \<Longrightarrow> (pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid) = isInvalidPDE pdea proof (prove)
goal (1 subgoal):
 1. case pdea of ARM_H.InvalidPDE \<Rightarrow> \<exists>inv. pde_lift pde = Some (Pde_pde_invalid inv) | ARM_H.PageTablePDE frame parity domain \<Rightarrow> pde_lift pde = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = frame, P_CL = of_bool parity, Domain_CL = domain\<rparr>) | ARM_H.SectionPDE frame parity domain cacheable global xn rights \<Rightarrow> pde_lift pde = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 0, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = domain, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) | ARM_H.SuperSectionPDE frame parity cacheable global xn rights \<Rightarrow> pde_lift pde = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = frame, size_CL = 1, nG_CL = of_bool (\<not> global), S_CL = s_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_from_cacheable cacheable, AP_CL = ap_from_vm_rights rights, P_CL = of_bool parity, Domain_CL = 0, XN_CL = of_bool xn, C_CL = 0, B_CL = b_from_cacheable cacheable\<rparr>) \<Longrightarrow> (pde_lift pde = Some (Pde_pde_invalid (pde_pde_invalid_lift pde))) = isInvalidPDE pdea proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>inv. pde_lift pde = Some (Pde_pde_invalid inv); pdea = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> pde_lift pde = Some (Pde_pde_invalid (pde_pde_invalid_lift pde)) proof (prove)
goal (1 subgoal):
 1. \<And>inv. \<lbrakk>pdea = ARM_H.InvalidPDE; pde_lift pde = Some (Pde_pde_invalid inv)\<rbrakk> \<Longrightarrow> inv = pde_pde_invalid_lift pde proof (prove)
goal:
No subgoals!