Changeset 855 for src/ASM/AssemblyProof.ma
- Timestamp:
- May 27, 2011, 6:11:37 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r854 r855 44 44 (* RUSSEL **) 45 45 46 definition bit_elim: ∀P: bool → bool. bool ≝ 47 λP. 48 P true ∧ P false. 49 46 50 let rec bitvector_elim_internal 47 51 (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝ … … 73 77 lemma subvector_hd_tl: 74 78 ∀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 ] 78 117 79 118 let rec list_addressing_mode_tags_elim
Note: See TracChangeset
for help on using the changeset viewer.