Changeset 862


Ignore:
Timestamp:
May 31, 2011, 2:33:18 AM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r861 r862  
    389389qed.
    390390
    391 axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop.
     391let 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
     396lemma 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 %]
     402qed.
     403
     404let 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
     413lemma 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 %]
     419qed.
     420
     421coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    392422
    393423lemma index_of_internal_None: ∀i,id,instr_list,n.
     
    396426   index_of_internal ? (address_of_word_labels_internal id) (instr_list@[〈None …,i〉]) n.
    397427 #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     | @IH
    403     ]]
     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 ]]]
    404434qed.
    405435
     
    409439  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    410440 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
     441 >(index_of_internal_None … H) %
     442qed.
    411443
    412444definition build_maps' ≝
     
    451483   whd in ⊢ (??(????%?)?) -labels1;
    452484   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 ⊢ (??(????%?)?)
    460490     
    461491    ]
Note: See TracChangeset for help on using the changeset viewer.