Structure alignmentTheory


Source File Identifier index Theory binding index

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


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14