Changeset 370
 Timestamp:
 Dec 3, 2010, 4:47:03 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/ASM.ma
r367 r370 92 92  addr16 ⇒ match A with [ ADDR16 _ ⇒ true  _ ⇒ false ]]. 93 93 94 nlet rec is_in n (l: Vector addressing_mode_tag (S n)) (A:addressing_mode) on l : Bool ≝ 95 match l return λm.λ_:Vector addressing_mode_tag m .∀K:m=S n.Bool with 96 [ Empty ⇒ λK.⊥ 97  Cons m he (tl: Vector addressing_mode_tag m) ⇒ λ_. 98 match m return λz.m = z → Bool with 99 [ Z ⇒ λ_.is_a he A 100  S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n). 101 (* CSC: cast not working here: why? *) 102 ##[##4: #x; ncases K; napply x ] 103 //; ndestruct. 104 nqed. 94 95 nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : Bool ≝ 96 match l return λm.λ_:Vector addressing_mode_tag m.Bool with 97 [ Empty ⇒ false 98  Cons m he (tl: Vector addressing_mode_tag m) ⇒ 99 is_a he A ∨ is_in ? tl A ]. 105 100 106 101 ndefinition bool_to_Prop ≝ 
Deliverables/D4.1/Matita/Interpret.ma
r369 r370 6 6 zero eight @@ b. 7 7 8 nlemma inclusive_disjunction_true: 9 ∀b, c: Bool. 10 ((inclusive_disjunction b c) = true) → ((b = true) ∨ (c = true)). 11 #b c; 12 nelim b 13 [ nnormalize; #H; napply or_introl; @; 14 ## nnormalize; /2/; 15 ##] 16 nqed. 17 8 18 nlemma execute_1_technical: 9 19 ∀n,m: Nat. … … 14 24 bool_to_Prop (subvector_with ? ? ? eq_a v q) → 15 25 bool_to_Prop (is_in ? q a). 16 #n m v q a. 17 nelim v. 26 #n m v q a; nelim v 27 [ nnormalize; #K; ncases K 28  #n' he tl II; 29 nwhd in ⊢ (% → ? → ?); 30 nlapply (refl … (is_in … (he:::tl) a)); 31 ncases (is_in … (he:::tl) a) in ⊢ (???% → %) 32 [ #K; #_; nnormalize in K; nwhd in ⊢ (% → ?); 33 nlapply (refl … (subvector_with … eq_a (he:::tl) q)); 34 ncases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %) 35 [ #K1; #_; 36 nchange in K1 with ((conjunction ? (subvector_with …)) = true); 37 nlapply (inclusive_disjunction_true (is_a he a) (is_in n' tl a)); 38 #K2; 39 nlapply (K2 K); 40 #K3; 41 ## #K1 K2; nnormalize in K2; ncases K2 ] 42 ## #K1 K2; nnormalize in K2; ncases K2 ] 43 44 45 nlet rec execute_1_technical 46 (m: Nat) 47 (a: addressing_mode) 48 (q: Vector addressing_mode_tag (S m)) 49 (n: Nat) 50 (v: Vector addressing_mode_tag (S n)) 51 on v : bool_to_Prop (is_in ? v a) → 52 bool_to_Prop (subvector_with ? ? ? eq_a v q) → 53 bool_to_Prop (is_in ? q a) ≝ 54 match v with 55 [ Empty ⇒ ? 56  Cons o he tl ⇒ ? 57 ]. 58 ##[ @  ndestruct  59 nlapply (S_inj … H); #H2; 60 nrewrite > H2 in H1; #K2; 61 62 63 #n; nelim n 64 [ #m v; ninversion v [ #K; ncases (?: False); 65 66 67 nelim v 68 [ nnormalize; 69 #H1 H2; 70 ncases (is_in m q a); 71 nnormalize 72 [ @  //; 73 //. 74 75 #N H V IH H1 H2. 18 76 nnormalize. 19 #H1 H2.20 77 ncases (is_in m q a). 21 78 nnormalize. … … 23 80 nnormalize. 24 81 //. 82 nqed. 83 84 nlemma execute_1_technical: 85 ∀n,m: Nat. 86 ∀v: Vector addressing_mode_tag (S n). 87 ∀q: Vector addressing_mode_tag (S m). 88 ∀a: addressing_mode. 89 bool_to_Prop (is_in ? v a) → 90 bool_to_Prop (subvector_with ? ? ? eq_a v q) → 91 bool_to_Prop (is_in ? q a). 92 #n; nelim n 93 [ #m v; ninversion v [ #K; ncases (?: False); 94 95 96 nelim v 97 [ nnormalize; 98 #H1 H2; 99 ncases (is_in m q a); 100 nnormalize 101 [ @  //; 102 //. 103 25 104 #N H V IH H1 H2. 26 105 nnormalize. 
Deliverables/D4.1/Matita/Vector.ma
r368 r370 415 415 (* ===================================== *) 416 416 417 ndefinition mem ≝ 418 λA: Type[0]. 419 λeq_a : A → A → Bool. 420 λn: Nat. 421 λl: Vector A n. 422 λx: A. 423 fold_right … (λy,v. inclusive_disjunction (eq_a x y) v) false l. 424 417 425 ndefinition subvector_with ≝ 418 426 λA: Type[0]. … … 422 430 λv: Vector A n. 423 431 λq: Vector A m. 424 fold_right ? ? ? (λx, v. conjunction v (fold_right ? ? ? (λy, z. inclusive_disjunction z (f x y)) false q)) true v.432 fold_right ? ? ? (λx, v. conjunction (mem ? f ? q x) v) true v. 425 433 426 434 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.