- Timestamp:
- May 31, 2011, 2:33:18 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r861 r862 389 389 qed. 390 390 391 axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop. 391 let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝ 392 match l with 393 [ nil ⇒ true 394 | cons hd tl ⇒ notb (address_of_word_labels_internal id hd) ∧ does_not_occur id tl]. 395 396 lemma does_not_occur_None: 397 ∀id,i,list_instr. 398 does_not_occur id (list_instr@[〈None …,i〉]) = 399 does_not_occur id list_instr. 400 #id #i #list_instr elim list_instr 401 [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %] 402 qed. 403 404 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝ 405 match l with 406 [ nil ⇒ false 407 | cons hd tl ⇒ 408 if address_of_word_labels_internal id hd then 409 does_not_occur id tl 410 else 411 occurs_exactly_once id tl ]. 412 413 lemma occurs_exactly_once_None: 414 ∀id,i,list_instr. 415 occurs_exactly_once id (list_instr@[〈None …,i〉]) = 416 occurs_exactly_once id list_instr. 417 #id #i #list_instr elim list_instr 418 [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %] 419 qed. 420 421 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 392 422 393 423 lemma index_of_internal_None: ∀i,id,instr_list,n. … … 396 426 index_of_internal ? (address_of_word_labels_internal id) (instr_list@[〈None …,i〉]) n. 397 427 #i #id #instr_list elim instr_list 398 [ #n #abs (* ASSURDO *)399 | #hd #tl #IH #n #H whd in ⊢ (??%%) cases (address_of_word_labels_internal id hd)400 whd in ⊢ (??%%)401 [ %402 | @IH403 ]]428 [ #n #abs whd in abs; cases abs 429 | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?) 430 cases (address_of_word_labels_internal id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%) 431 [ #H % 432 | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ % 433 [ #_ % | #abs cases abs ]]] 404 434 qed. 405 435 … … 409 439 address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id. 410 440 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?)) 441 >(index_of_internal_None … H) % 442 qed. 411 443 412 444 definition build_maps' ≝ … … 451 483 whd in ⊢ (??(????%?)?) -labels1; 452 484 cases label in Hid 453 [ #Hid whd in ⊢ (??(????%?)?) 454 (* COMPLETARE *) 455 >IH1 -IH1 456 [ 457 | 458 ] 459 | -label #label whd in ⊢ (??(????%?)?) 485 [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1 486 [ >(address_of_word_labels_code_mem_None … Hid) 487 (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *) 488 | whd in Hid >occurs_exactly_once_None in Hid // ] 489 | -label #label #Hid whd in ⊢ (??(????%?)?) 460 490 461 491 ]
Note: See TracChangeset
for help on using the changeset viewer.