 Timestamp:
 Jun 3, 2011, 11:21:12 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r874 r875 442 442 λi, j: instruction. 443 443 true. 444 445 let rec list_addressing_mode_tags_elim_prop 446 (n: nat) (l: Vector addressing_mode_tag (S n)) 447 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 448 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 449 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 450 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 451 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 452 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 453 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 454 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 455 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 456 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 457 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 458 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 459 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 460 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 461 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 462 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 463 (if is_in ? l relative then ∀x. P (RELATIVE x) else True) → 464 (if is_in ? l addr11 then ∀x. P (ADDR11 x) else True) → 465 (if is_in ? l addr16 then ∀x. P (ADDR16 x) else True) → 466 (P: addressing_mode → Prop) (x: l) 467 on l : P x ≝ 468 match l return λx.match x with [O ⇒ λl: Vector … O. bool  S x' ⇒ λl: Vector addressing_mode_tag (S x'). 469 (l → bool) → bool ] with 470 [ VEmpty ⇒ true 471  VCons len hd tl ⇒ λP. 472 let process_hd ≝ 473 match hd return λhd. ∀P: hd:::tl → bool. bool with 474 [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x)) 475  indirect ⇒ λP.bit_elim (λx. P (INDIRECT x)) 476  ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x)) 477  registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x)) 478  acc_a ⇒ λP.P ACC_A 479  acc_b ⇒ λP.P ACC_B 480  dptr ⇒ λP.P DPTR 481  data ⇒ λP.bitvector_elim 8 (λx. P (DATA x)) 482  data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x)) 483  acc_dptr ⇒ λP.P ACC_DPTR 484  acc_pc ⇒ λP.P ACC_PC 485  ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR 486  indirect_dptr ⇒ λP.P INDIRECT_DPTR 487  carry ⇒ λP.P CARRY 488  bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x)) 489  n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x)) 490  relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x)) 491  addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x)) 492  addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x)) 493 ] 494 in 495 andb (process_hd P) 496 (match len return λx. x = len → bool with 497 [ O ⇒ λprf. true 498  S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len)) 499 ]. 500 try % 501 [ 2: cases (sym_eq ??? prf); @tl 502  generalize in match H; generalize in match tl; cases prf; 503 (* cases prf in tl H; : ??? WAS WORKING BEFORE *) 504 #tl 505 normalize in ⊢ (∀_: %. ?) 506 # H 507 whd 508 normalize in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]) 509 cases (is_a hd (subaddressing_modeel y tl H)) whd // ] 510 qed. 511 444 512 (* 445 513 lemma test: … … 461 529 let 〈instr_pc, ticks〉 ≝ fetched in 462 530 eq_instruction (\fst instr_pc)) i = true. 463 [ @ (instruction_elim_complete ) 531 [ #i cases i #arg try #arg2 whd in ⊢ (??%?) 532 [2: whd in ⊢ (??(match ? (? %) ?with [ _ ⇒ ?] ?)?) 533 cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP; 534 whd in ⊢ (??(match ? (? %) ? with [ _ ⇒ ?] ?)?) 535 536 [2: #addr whd in ⊢ (??%?) 537 538 @ (instruction_elim_complete ) 464 539  @ zero 465 540 ]
Note: See TracChangeset
for help on using the changeset viewer.