 Timestamp:
 May 27, 2011, 6:11:37 PM (9 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.