Changeset 1518


Ignore:
Timestamp:
Nov 21, 2011, 11:15:06 AM (8 years ago)
Author:
campbell
Message:

Update to new syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1516 r1518  
    10141014         @ le_O_n
    10151015      |1,2,4,5:
    1016          apply modulus_less_than
     1016         @modulus_less_than
    10171017      ]
    10181018qed.
     
    10861086lemma snd_fetch_pseudo_instruction:
    10871087 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
    1088  #l #ppc whd in ⊢ (??%?) whd in ⊢ (?? match % with [_ ⇒ ?]?) @pair_elim'
     1088 #l #ppc whd in ⊢ (??%?); whd in ⊢ (?? match % with [_ ⇒ ?]?); @pair_elim'
    10891089 #lft #rgt @pair_elim' #x #y #_ @pair_elim' #a #b #_ normalize #H
    1090  generalize in match (pair_destruct_2 ????? H) normalize #K >K %
     1090 generalize in match (pair_destruct_2 ????? H); normalize #K >K %
    10911091qed.
    10921092
     
    11091109  does_not_occur id list_instr.
    11101110 #id #i #list_instr elim list_instr
    1111   [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
     1111  [ % | #hd #tl #IH whd in ⊢ (??%%); >IH %]
    11121112qed.
    11131113
     
    11191119 #id #id' #i #list_instr elim list_instr
    11201120  [ #H normalize in H ⊢ %; >H %
    1121   | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
     1121  | * #x #i' #tl #IH #H whd in ⊢ (??%%); >(IH H) %]
    11221122qed.
    11231123
     
    11281128  [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
    11291129    >eq_identifier_refl %
    1130   | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
     1130  | * #x #i' #tl #IH whd in ⊢ (??%%); >IH cases (notb ?) %]
    11311131qed.
    11321132
     
    11461146  occurs_exactly_once id list_instr.
    11471147 #id #i #list_instr elim list_instr
    1148   [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
     1148  [ % | #hd #tl #IH whd in ⊢ (??%%); >IH >does_not_occur_None %]
    11491149qed.
    11501150
     
    11531153  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
    11541154 #id #id' #i #prefix elim prefix
    1155   [ whd in ⊢ (?% → ?)
    1156     change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) with (eq_identifier ? id' id)
     1155  [ whd in ⊢ (?% → ?);
     1156    change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?); with (eq_identifier ? id' id);
    11571157    @eq_identifier_elim normalize nodelta; /2/
    1158   | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     1158  | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    11591159    cases he; normalize nodelta
    11601160     [ #H @ (IH H)
    1161      | #x whd in ⊢ (? → ?(??%)) change in match (instruction_matches_identifier ??) with (eq_identifier ? x id)
     1161     | #x whd in ⊢ (? → ?(??%)); change in match (instruction_matches_identifier ??); with (eq_identifier ? x id)
    11621162       @eq_identifier_elim #E normalize nodelta
    11631163       [ destruct @eq_identifier_elim normalize nodelta;
     
    11721172    (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
    11731173 #id #id' #i #prefix elim prefix
    1174  [ whd in ⊢ (?% → ?) change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?) with (eq_identifier ???)
     1174 [ whd in ⊢ (?% → ?); change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?); with (eq_identifier ???)
    11751175   @eq_identifier_elim #E
    11761176  [ normalize //
    11771177  | normalize #H @⊥ @H 
    11781178  ]
    1179  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     1179 | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    11801180   cases he; normalize nodelta
    11811181   [ #H @ (IH H)
     
    11841184       [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
    11851185       | #H >(does_not_occur_Some)
    1186          [ #H2 whd in match (does_not_occur ??)
    1187            change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1186         [ #H2 whd in match (does_not_occur ??);
     1187           change in match (instruction_matches_identifier ??); with (eq_identifier ???)
    11881188           >Heq >eq_identifier_refl normalize nodelta
    1189            @orb_elim normalize nodelta whd in match (occurs_exactly_once ??)
    1190            change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1189           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);
     1190           change in match (instruction_matches_identifier ??); with (eq_identifier ???)
    11911191           >eq_identifier_refl
    11921192           normalize nodelta @H2 
     
    11981198       #Hor @orb_elim
    11991199       [ <Heq2 in Hor; #Hor normalize in Hor;
    1200          whd in match (does_not_occur ??) change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1200         whd in match (does_not_occur ??); change in match (instruction_matches_identifier ??); with (eq_identifier ???)
    12011201         >eq_identifier_false // normalize nodelta
    12021202         cases (does_not_occur id' tl) in Hor; normalize nodelta //
    1203        | normalize nodelta whd in match (occurs_exactly_once ??)
    1204          change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1203       | normalize nodelta whd in match (occurs_exactly_once ??);
     1204         change in match (instruction_matches_identifier ??); with (eq_identifier ???)
    12051205         >eq_identifier_false //
    12061206       ]
     
    12351235 #i #id #instr_list elim instr_list
    12361236  [ #n #abs whd in abs; cases abs
    1237   | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
    1238     cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
     1237  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
     1238    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%);
    12391239    [ #H %
    1240     | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
     1240    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %;
    12411241      [ #_ % | #abs cases abs ]]]
    12421242qed.
     
    12491249   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
    12501250 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
    1251  change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
     1251 change with (occurs_exactly_once ?? → ?) generalize in match n; -n -H; elim instr_list
    12521252  [ #n #abs cases abs
    1253   | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
     1253  | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
    12541254    [ // | #K @IH //]]
    12551255qed.
     
    12611261  = |instr_list| + n.
    12621262 #i #id #instr_list elim instr_list
    1263   [ #n #_ whd in ⊢ (??%%) change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
    1264   | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
     1263  [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
     1264  | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
    12651265    [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
    12661266qed.
     
    12751275  address_of_word_labels_code_mem instr_list id =
    12761276  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    1277  #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
     1277 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    12781278 >(index_of_internal_None … H) %
    12791279qed.
     
    12841284   address_of_word_labels_code_mem instr_list id =
    12851285   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    1286  #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
     1286 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    12871287 >(index_of_internal_Some_miss … H) [ @refl | // ]
    12881288qed.
     
    12921292   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    12931293   = bitvector_of_nat … (|instr_list|).
    1294  #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
     1294 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
    12951295 >(index_of_internal_Some_hit … H) <plus_n_O @refl
    12961296qed.
Note: See TracChangeset for help on using the changeset viewer.