Changeset 855


Ignore:
Timestamp:
May 27, 2011, 6:11:37 PM (8 years ago)
Author:
mulligan
Message:

changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r854 r855  
    4444(* RUSSEL **)
    4545
     46definition bit_elim: ∀P: bool → bool. bool ≝
     47  λP.
     48    P true ∧ P false.
     49
    4650let rec bitvector_elim_internal
    4751  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
     
    7377lemma subvector_hd_tl:
    7478  ∀A: Type[0].
    75   ∀
    76   ∀hd: A.
    77   ∀
     79  ∀n: nat.
     80  ∀h: A.
     81  ∀eq: A → A → bool.
     82  ∀v: Vector A n.
     83  ∀m: nat.
     84  ∀q: Vector A m.
     85    bool_to_Prop (subvector_with A ? ? eq v (h ::: q @@ v)).
     86  # A
     87  # N
     88  # H
     89  # EQ
     90  # V
     91  elim V
     92  [ normalize
     93    # M
     94    # Q
     95    %
     96  | # NN
     97    # AA
     98    # VV
     99    # IH
     100    # MM
     101    # QQ
     102    whd
     103    whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     104    change in ⊢ (match (match ? with [_ ⇒ % | _ ⇒ ?]) with [_ ⇒ ? | _ ⇒ ?])
     105     with (subvector_with ??????)
     106    change in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]) with (andb ??)
     107    change with (bool_to_Prop ?);
     108    cut ((mem A EQ (S MM+S NN) (H:::QQ@@AA:::VV) AA) = true)
     109    [
     110    | # H
     111      > H
     112      applyS (IH ? (QQ@@[[AA]]))
     113    ]
     114    generalize in match (IH ? (QQ@@[[AA]]))
     115    whd in ⊢ (% → ?)
     116  ]
    78117
    79118let rec list_addressing_mode_tags_elim
Note: See TracChangeset for help on using the changeset viewer.