Structure alignmentTheory
signature alignmentTheory =
sig
type thm = Thm.thm
(* Definitions *)
val align_def : thm
val aligned_def : thm
val byte_align_def : thm
val byte_aligned_def : thm
(* Theorems *)
val MOD_0_aligned : thm
val align_0 : thm
val align_add_aligned : thm
val align_add_aligned_gen : thm
val align_align : thm
val align_align_MAX : thm
val align_aligned : thm
val align_bitwise_and : thm
val align_lo : thm
val align_ls : thm
val align_shift : thm
val align_sub : thm
val align_w2n : thm
val aligned_0 : thm
val aligned_1_lsb : thm
val aligned_add_pow : thm
val aligned_add_sub : thm
val aligned_add_sub_123 : thm
val aligned_add_sub_cor : thm
val aligned_add_sub_prod : thm
val aligned_align : thm
val aligned_between : thm
val aligned_bit_count_upto : thm
val aligned_bitwise_and : thm
val aligned_extract : thm
val aligned_ge_dim : thm
val aligned_imp : thm
val aligned_lsl : thm
val aligned_lsl_leq : thm
val aligned_mul_shift_1 : thm
val aligned_numeric : thm
val aligned_or : thm
val aligned_pow2 : thm
val aligned_w2n : thm
val byte_align_aligned : thm
val byte_aligned_add : thm
val lt_align_eq_0 : thm
val pow2_eq_0 : thm
val word_msb_align : thm
val alignment_grammars : type_grammar.grammar * term_grammar.grammar
(*
[words] Parent theory of "alignment"
[align_def] Definition
⊢ ∀p w. align p w = (dimindex (:α) − 1 '' p) w
[aligned_def] Definition
⊢ ∀p w. aligned p w ⇔ align p w = w
[byte_align_def] Definition
⊢ ∀w. byte_align w = align (LOG2 (dimindex (:α) DIV 8)) w
[byte_aligned_def] Definition
⊢ ∀w. byte_aligned w ⇔ aligned (LOG2 (dimindex (:α) DIV 8)) w
[MOD_0_aligned] Theorem
⊢ ∀n p. n MOD 2 ** p = 0 ⇒ aligned p (n2w n)
[align_0] Theorem
⊢ ∀w. align 0 w = w
[align_add_aligned] Theorem
⊢ ∀p a b. aligned p a ∧ w2n b < 2 ** p ⇒ align p (a + b) = a
[align_add_aligned_gen] Theorem
⊢ ∀a. aligned p a ⇒ align p (a + b) = a + align p b
[align_align] Theorem
⊢ ∀p w. align p (align p w) = align p w
[align_align_MAX] Theorem
⊢ ∀k l w. align k (align l w) = align (MAX k l) w
[align_aligned] Theorem
⊢ ∀p w. aligned p w ⇒ align p w = w
[align_bitwise_and] Theorem
⊢ ∀p w. align p w = w && UINT_MAXw ≪ p
[align_lo] Theorem
⊢ ¬aligned p n ⇒ align p n <₊ n
[align_ls] Theorem
⊢ align p n ≤₊ n
[align_shift] Theorem
⊢ ∀p w. align p w = w ⋙ p ≪ p
[align_sub] Theorem
⊢ ∀p w. align p w = if p = 0 then w else w − (p − 1 >< 0) w
[align_w2n] Theorem
⊢ ∀p w. align p w = n2w (w2n w DIV 2 ** p * 2 ** p)
[aligned_0] Theorem
⊢ (∀p. aligned p 0w) ∧ ∀w. aligned 0 w
[aligned_1_lsb] Theorem
⊢ ∀w. aligned 1 w ⇔ ¬word_lsb w
[aligned_add_pow] Theorem
⊢ (∀w k. aligned k (w + n2w (2 ** k)) ⇔ aligned k w) ∧
∀k n w. aligned k (w + n2w (n * 2 ** k)) ⇔ aligned k w
[aligned_add_sub] Theorem
⊢ ∀p a b.
aligned p b ⇒
(aligned p (a + b) ⇔ aligned p a) ∧
(aligned p (a − b) ⇔ aligned p a)
[aligned_add_sub_123] Theorem
⊢ (∀w x.
(aligned 1 (w + 2w * x) ⇔ aligned 1 w) ∧
(aligned 1 (w − 2w * x) ⇔ aligned 1 w)) ∧
(∀x. aligned 1 (2w * x) ∧ aligned 1 (-2w * x)) ∧
(∀w x.
(aligned 2 (w + 4w * x) ⇔ aligned 2 w) ∧
(aligned 2 (w − 4w * x) ⇔ aligned 2 w)) ∧
(∀x. aligned 2 (4w * x) ∧ aligned 2 (-4w * x)) ∧
(∀w x.
(aligned 3 (w + 8w * x) ⇔ aligned 3 w) ∧
(aligned 3 (w − 8w * x) ⇔ aligned 3 w)) ∧
∀x. aligned 3 (8w * x) ∧ aligned 3 (-8w * x)
[aligned_add_sub_cor] Theorem
⊢ ∀p a b.
aligned p a ∧ aligned p b ⇒
aligned p (a + b) ∧ aligned p (a − b)
[aligned_add_sub_prod] Theorem
⊢ ∀p w x.
(aligned p (w + 1w ≪ p * x) ⇔ aligned p w) ∧
(aligned p (w − 1w ≪ p * x) ⇔ aligned p w)
[aligned_align] Theorem
⊢ ∀p w. aligned p (align p w)
[aligned_between] Theorem
⊢ ¬aligned p n ∧ aligned p m ∧ align p n <₊ m ⇒ n <₊ m
[aligned_bit_count_upto] Theorem
⊢ ∀p w. aligned p w ⇔ bit_count_upto (MIN (dimindex (:α)) p) w = 0
[aligned_bitwise_and] Theorem
⊢ ∀p w. aligned p w ⇔ w && n2w (2 ** p − 1) = 0w
[aligned_extract] Theorem
⊢ ∀p w. aligned p w ⇔ p = 0 ∨ (p − 1 >< 0) w = 0w
[aligned_ge_dim] Theorem
⊢ ∀p w. dimindex (:α) ≤ p ⇒ (aligned p w ⇔ w = 0w)
[aligned_imp] Theorem
⊢ ∀p q w. p < q ∧ aligned q w ⇒ aligned p w
[aligned_lsl] Theorem
⊢ aligned k (w ≪ k)
[aligned_lsl_leq] Theorem
⊢ k ≤ l ⇒ aligned k (w ≪ l)
[aligned_mul_shift_1] Theorem
⊢ ∀p w. aligned p (1w ≪ p * w)
[aligned_numeric] Theorem
⊢ (∀x. aligned 3 (n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) ∧
(∀x. aligned 2 (n2w (NUMERAL (BIT2 (BIT1 x))))) ∧
(∀x. aligned 1 (n2w (NUMERAL (BIT2 x)))) ∧
(∀x. aligned 3 (-n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) ∧
(∀x. aligned 2 (-n2w (NUMERAL (BIT2 (BIT1 x))))) ∧
(∀x. aligned 1 (-n2w (NUMERAL (BIT2 x)))) ∧
(∀x y f.
aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) ⇔
aligned 3 (y + 7w)) ∧
(∀x y f.
aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) ⇔
aligned 3 (y + 3w)) ∧
(∀x y f.
aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) ⇔
aligned 3 (y + 1w)) ∧
(∀x y f.
aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) ⇔
aligned 3 (y + 5w)) ∧
(∀x y f.
aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) ⇔
aligned 3 y) ∧
(∀x y f.
aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) ⇔
aligned 3 (y + 4w)) ∧
(∀x y f.
aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) ⇔
aligned 3 (y + 2w)) ∧
(∀x y f.
aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) ⇔
aligned 3 (y + 6w)) ∧
(∀x y f.
aligned 3 (y − n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) ⇔
aligned 3 (y − 7w)) ∧
(∀x y f.
aligned 3 (y − n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) ⇔
aligned 3 (y − 3w)) ∧
(∀x y f.
aligned 3 (y − n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) ⇔
aligned 3 (y − 1w)) ∧
(∀x y f.
aligned 3 (y − n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) ⇔
aligned 3 (y − 5w)) ∧
(∀x y f.
aligned 3 (y − n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) ⇔
aligned 3 y) ∧
(∀x y f.
aligned 3 (y − n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) ⇔
aligned 3 (y − 4w)) ∧
(∀x y f.
aligned 3 (y − n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) ⇔
aligned 3 (y − 2w)) ∧
(∀x y f.
aligned 3 (y − n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) ⇔
aligned 3 (y − 6w)) ∧
(∀x y f.
aligned 2 (y + n2w (NUMERAL (BIT1 (BIT1 (f x))))) ⇔
aligned 2 (y + 3w)) ∧
(∀x y.
aligned 2 (y + n2w (NUMERAL (BIT1 (BIT2 x)))) ⇔
aligned 2 (y + 1w)) ∧
(∀x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT1 x)))) ⇔ aligned 2 y) ∧
(∀x y.
aligned 2 (y + n2w (NUMERAL (BIT2 (BIT2 x)))) ⇔
aligned 2 (y + 2w)) ∧
(∀x y f.
aligned 2 (y − n2w (NUMERAL (BIT1 (BIT1 (f x))))) ⇔
aligned 2 (y − 3w)) ∧
(∀x y.
aligned 2 (y − n2w (NUMERAL (BIT1 (BIT2 x)))) ⇔
aligned 2 (y − 1w)) ∧
(∀x y. aligned 2 (y − n2w (NUMERAL (BIT2 (BIT1 x)))) ⇔ aligned 2 y) ∧
(∀x y.
aligned 2 (y − n2w (NUMERAL (BIT2 (BIT2 x)))) ⇔
aligned 2 (y − 2w)) ∧
(∀x y f.
aligned 1 (y + n2w (NUMERAL (BIT1 (f x)))) ⇔
aligned 1 (y + 1w)) ∧
(∀x y f.
aligned 1 (y − n2w (NUMERAL (BIT1 (f x)))) ⇔
aligned 1 (y − 1w)) ∧
(∀x y. aligned 1 (y + n2w (NUMERAL (BIT2 x))) ⇔ aligned 1 y) ∧
∀x y. aligned 1 (y − n2w (NUMERAL (BIT2 x))) ⇔ aligned 1 y
[aligned_or] Theorem
⊢ aligned n (w ‖ v) ⇔ aligned n w ∧ aligned n v
[aligned_pow2] Theorem
⊢ aligned k (n2w (2 ** k))
[aligned_w2n] Theorem
⊢ aligned k w ⇔ w2n w MOD 2 ** k = 0
[byte_align_aligned] Theorem
⊢ byte_aligned x ⇔ byte_align x = x
[byte_aligned_add] Theorem
⊢ byte_aligned x ∧ byte_aligned y ⇒ byte_aligned (x + y)
[lt_align_eq_0] Theorem
⊢ w2n a < 2 ** p ⇒ align p a = 0w
[pow2_eq_0] Theorem
⊢ dimindex (:α) ≤ k ⇒ n2w (2 ** k) = 0w
[word_msb_align] Theorem
⊢ p < dimindex (:α) ⇒ (word_msb (align p w) ⇔ word_msb w)
*)
end
HOL 4, Kananaskis-13