Changeset 372
 Timestamp:
 Dec 3, 2010, 11:52:05 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/DoTest.ma
r369 r372 28 28 *) 29 29 30 (* 30 31 nlemma xoo: 31 32 (let testfinal ≝ testfinal in … … 35 36 nqed. 36 37 38 ndefinition is_JZ ≝ 39 λi: instruction.match i with 40 [ Jump arg ⇒ 41 match arg with 42 [ JZ arg ⇒ 43 match arg with 44 [ RELATIVE arg ⇒ arg 45  _ ⇒ zero eight ] 46  _ ⇒ zero eight ] 47  _ ⇒ zero eight ]. 48 49 nlemma xoo: 50 (let testfinal ≝ testfinal in 51 is_JZ 52 (first … (first … (fetch (code_memory testfinal) (program_counter testfinal)))) 53 ) 54 = zero eight. 55 nnormalize in ⊢ (??%?); 56 57 *) 58 59 37 60 nlemma xoo: program_counter testfinal = program_counter testfinal. 38 61 nnormalize in ⊢ (??%?); 62 nnormalize in ⊢ (???%); 63 @. 39 64 nqed. 
Deliverables/D4.1/Matita/Interpret.ma
r370 r372 8 8 nlemma inclusive_disjunction_true: 9 9 ∀b, c: Bool. 10 ((inclusive_disjunction b c) = true) → ((b = true) ∨ (c = true)).10 inclusive_disjunction b c = true → b = true ∨ c = true. 11 11 #b c; 12 12 nelim b … … 14 14 ## nnormalize; /2/; 15 15 ##] 16 nqed. 17 18 nlemma conjunction_true: 19 ∀b, c: Bool. 20 conjunction b c = true → b = true ∧ c = true. 21 #b c; 22 nelim b; nnormalize 23 [ /2/  #K; ndestruct ] 24 nqed. 25 26 nlemma eq_true_false: false=true → False. 27 #K; ndestruct. 28 nqed. 29 30 nlemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b. 31 #a; #b; ncases a; ncases b; nnormalize; //; #K; ncases (eq_true_false K). 32 nqed. 33 34 nlemma inclusive_disjunction_b_true: ∀b. inclusive_disjunction b true = true. 35 #b; ncases b; @. 36 nqed. 37 38 nlemma is_a_to_mem_to_is_in: 39 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. 40 #he a m q; nelim q 41 [ nnormalize; #_; #K; nassumption 42  #m' t q' II H1 H2; nnormalize; 43 nchange in H2:(??%?) with (inclusive_disjunction ??); 44 ncases (inclusive_disjunction_true … H2) 45 [ #K; nrewrite < (eq_a_to_eq … K); nrewrite > H1; @ 46  #K; nrewrite > II; ntry nassumption; // ] 16 47 nqed. 17 48 … … 35 66 [ #K1; #_; 36 67 nchange in K1 with ((conjunction ? (subvector_with …)) = true); 37 n lapply (inclusive_disjunction_true (is_a he a) (is_in n' tl a));38 #K2;39 nlapply (K2 K);40 #K3;68 ncases (conjunction_true … K1); #K3; #K4; 69 ncases (inclusive_disjunction_true … K); #K2 70 [ nrewrite > (is_a_to_mem_to_is_in … K2 K3); @ 71  napply II [ nrewrite > K2; @  nrewrite > K4; @]##] 41 72 ## #K1 K2; nnormalize in K2; ncases K2 ] 42 73 ## #K1 K2; nnormalize in K2; ncases K2 ] 43 44 45 nlet rec execute_1_technical46 (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 with55 [ 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 n64 [ #m v; ninversion v [ #K; ncases (?: False);65 66 67 nelim v68 [ nnormalize;69 #H1 H2;70 ncases (is_in m q a);71 nnormalize72 [ @  //;73 //.74 75 #N H V IH H1 H2.76 nnormalize.77 ncases (is_in m q a).78 nnormalize.79 napply I.80 nnormalize.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 n93 [ #m v; ninversion v [ #K; ncases (?: False);94 95 96 nelim v97 [ nnormalize;98 #H1 H2;99 ncases (is_in m q a);100 nnormalize101 [ @  //;102 //.103 104 #N H V IH H1 H2.105 nnormalize.106 ncases (is_in m q a).107 nnormalize.108 napply I.109 nnormalize.110 //.111 74 nqed. 112 75
Note: See TracChangeset
for help on using the changeset viewer.