theory Retype_R

lemma pde_relation_aligned_eq:
  "\<lbrakk>is_aligned (pd::word32) 6; is_aligned pd' 6\<rbrakk>
   \<Longrightarrow> pde_relation_aligned (pd + x >> 2) xa ya =
       pde_relation_aligned (pd' + x >> 2) xa ya" apply (clarsimp simp: pde_relation_aligned_def is_aligned_mask mask_def
                 split: ARM_H.pde.splits) apply word_bitwise apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd 6; is_aligned pd' 6\<rbrakk> \<Longrightarrow> pde_relation_aligned (pd + x >> 2) xa ya = pde_relation_aligned (pd' + x >> 2) xa ya proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>pd && 0x3F = 0; pd' && 0x3F = 0; ya = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> ((pd + x >> 2) && 0xF = 0 \<longrightarrow> (pd' + x >> 2) && 0xF \<noteq> 0 \<longrightarrow> pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46) = (xa = ARM_A.InvalidPDE)) \<and> ((pd + x >> 2) && 0xF \<noteq> 0 \<longrightarrow> (pd' + x >> 2) && 0xF = 0 \<longrightarrow> (xa = ARM_A.InvalidPDE) = pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>\<not> pd !! 0 \<and> \<not> pd !! 1 \<and> \<not> pd !! 2 \<and> \<not> pd !! 3 \<and> \<not> pd !! 4 \<and> \<not> pd !! 5; \<not> pd' !! 0 \<and> \<not> pd' !! 1 \<and> \<not> pd' !! 2 \<and> \<not> pd' !! 3 \<and> \<not> pd' !! 4 \<and> \<not> pd' !! 5; ya = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> (\<not> xor3 (pd !! 2) (x !! 2) (carry (pd !! 1) (x !! 1) (pd !! 0 \<and> x !! 0)) \<and> \<not> xor3 (pd !! 3) (x !! 3) (carry (pd !! 2) (x !! 2) (carry (pd !! 1) (x !! 1) (pd !! 0 \<and> x !! 0))) \<and> \<not> xor3 (pd !! 4) (x !! 4) (carry (pd !! 3) (x !! 3) (carry (pd !! 2) (x !! 2) (carry (pd !! 1) (x !! 1) (pd !! 0 \<and> x !! 0)))) \<and> \<not> xor3 (pd !! 5) (x !! 5) (carry (pd !! 4) (x !! 4) (carry (pd !! 3) (x !! 3) (carry (pd !! 2) (x !! 2) (carry (pd !! 1) (x !! 1) (pd !! 0 \<and> x !! 0))))) \<longrightarrow> (xor3 (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)) \<longrightarrow> pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46) = (xa = ARM_A.InvalidPDE)) \<and> (xor3 (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))) \<longrightarrow> pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46) = (xa = ARM_A.InvalidPDE)) \<and> (xor3 (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)))) \<longrightarrow> pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46) = (xa = ARM_A.InvalidPDE)) \<and> (xor3 (pd' !! 5) (x !! 5) (carry (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))))) \<longrightarrow> pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46) = (xa = ARM_A.InvalidPDE))) \<and> (xor3 (pd !! 2) (x !! 2) (carry (pd !! 1) (x !! 1) (pd !! 0 \<and> x !! 0)) \<longrightarrow> \<not> xor3 (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)) \<and> \<not> xor3 (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))) \<and> \<not> xor3 (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)))) \<and> \<not> xor3 (pd' !! 5) (x !! 5) (carry (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))))) \<longrightarrow> (xa = ARM_A.InvalidPDE) = pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)) \<and> (xor3 (pd !! 3) (x !! 3) (carry (pd !! 2) (x !! 2) (carry (pd !! 1) (x !! 1) (pd !! 0 \<and> x !! 0))) \<longrightarrow> \<not> xor3 (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)) \<and> \<not> xor3 (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))) \<and> \<not> xor3 (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)))) \<and> \<not> xor3 (pd' !! 5) (x !! 5) (carry (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))))) \<longrightarrow> (xa = ARM_A.InvalidPDE) = pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)) \<and> (xor3 (pd !! 4) (x !! 4) (carry (pd !! 3) (x !! 3) (carry (pd !! 2) (x !! 2) (carry (pd !! 1) (x !! 1) (pd !! 0 \<and> x !! 0)))) \<longrightarrow> \<not> xor3 (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)) \<and> \<not> xor3 (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))) \<and> \<not> xor3 (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)))) \<and> \<not> xor3 (pd' !! 5) (x !! 5) (carry (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))))) \<longrightarrow> (xa = ARM_A.InvalidPDE) = pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)) \<and> (xor3 (pd !! 5) (x !! 5) (carry (pd !! 4) (x !! 4) (carry (pd !! 3) (x !! 3) (carry (pd !! 2) (x !! 2) (carry (pd !! 1) (x !! 1) (pd !! 0 \<and> x !! 0))))) \<longrightarrow> \<not> xor3 (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)) \<and> \<not> xor3 (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))) \<and> \<not> xor3 (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0)))) \<and> \<not> xor3 (pd' !! 5) (x !! 5) (carry (pd' !! 4) (x !! 4) (carry (pd' !! 3) (x !! 3) (carry (pd' !! 2) (x !! 2) (carry (pd' !! 1) (x !! 1) (pd' !! 0 \<and> x !! 0))))) \<longrightarrow> (xa = ARM_A.InvalidPDE) = pde_relation' xa (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)) proof (prove)
goal:
No subgoals!