Changeset 1518

Timestamp:

Nov 21, 2011, 11:15:06 AM (8 years ago)

Author:

campbell

Message:

Update to new syntax.

File:

• src/ASM/Status.ma (modified) (16 diffs)

src/ASM/Status.ma

@@ -1014 +1014 @@
          @ le_O_n
       |1,2,4,5:
-         apply modulus_less_than
+         @modulus_less_than
       ]
 qed.
@@ -1086 +1086 @@
 lemma snd_fetch_pseudo_instruction:
  ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
- #l #ppc whd in ⊢ (??%?) whd in ⊢ (?? match % with [_ ⇒ ?]?) @pair_elim'
+ #l #ppc whd in ⊢ (??%?); whd in ⊢ (?? match % with [_ ⇒ ?]?); @pair_elim'
  #lft #rgt @pair_elim' #x #y #_ @pair_elim' #a #b #_ normalize #H
- generalize in match (pair_destruct_2 ????? H) normalize #K >K %
+ generalize in match (pair_destruct_2 ????? H); normalize #K >K %
 qed.
 
@@ -1109 +1109 @@
   does_not_occur id list_instr.
  #id #i #list_instr elim list_instr
-  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
+  [ % | #hd #tl #IH whd in ⊢ (??%%); >IH %]
 qed.
 
@@ -1119 +1119 @@
  #id #id' #i #list_instr elim list_instr
   [ #H normalize in H ⊢ %; >H %
-  | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
+  | * #x #i' #tl #IH #H whd in ⊢ (??%%); >(IH H) %]
 qed.
 
@@ -1128 +1128 @@
   [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
     >eq_identifier_refl %
-  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
+  | * #x #i' #tl #IH whd in ⊢ (??%%); >IH cases (notb ?) %]
 qed.
 
@@ -1146 +1146 @@
   occurs_exactly_once id list_instr.
  #id #i #list_instr elim list_instr
-  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
+  [ % | #hd #tl #IH whd in ⊢ (??%%); >IH >does_not_occur_None %]
 qed.
 
@@ -1153 +1153 @@
   occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
  #id #id' #i #prefix elim prefix
-  [ whd in ⊢ (?% → ?)
-    change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) with (eq_identifier ? id' id)
+  [ whd in ⊢ (?% → ?);
+    change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?); with (eq_identifier ? id' id);
     @eq_identifier_elim normalize nodelta; /2/
-  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
+  | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
     cases he; normalize nodelta
      [ #H @ (IH H)
-     | #x whd in ⊢ (? → ?(??%)) change in match (instruction_matches_identifier ??) with (eq_identifier ? x id)
+     | #x whd in ⊢ (? → ?(??%)); change in match (instruction_matches_identifier ??); with (eq_identifier ? x id)
        @eq_identifier_elim #E normalize nodelta
        [ destruct @eq_identifier_elim normalize nodelta;
@@ -1172 +1172 @@
     (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
  #id #id' #i #prefix elim prefix
- [ whd in ⊢ (?% → ?) change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?) with (eq_identifier ???)
+ [ whd in ⊢ (?% → ?); change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?); with (eq_identifier ???)
    @eq_identifier_elim #E
   [ normalize //
   | normalize #H @⊥ @H  
   ]
- | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
+ | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    cases he; normalize nodelta
    [ #H @ (IH H)
@@ -1184 +1184 @@
        [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
        | #H >(does_not_occur_Some)
-         [ #H2 whd in match (does_not_occur ??)
-           change in match (instruction_matches_identifier ??) with (eq_identifier ???)
+         [ #H2 whd in match (does_not_occur ??);
+           change in match (instruction_matches_identifier ??); with (eq_identifier ???)
            >Heq >eq_identifier_refl normalize nodelta
-           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??)
-           change in match (instruction_matches_identifier ??) with (eq_identifier ???)
+           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);
+           change in match (instruction_matches_identifier ??); with (eq_identifier ???)
            >eq_identifier_refl
            normalize nodelta @H2  
@@ -1198 +1198 @@
        #Hor @orb_elim
        [ <Heq2 in Hor; #Hor normalize in Hor;
-         whd in match (does_not_occur ??) change in match (instruction_matches_identifier ??) with (eq_identifier ???)
+         whd in match (does_not_occur ??); change in match (instruction_matches_identifier ??); with (eq_identifier ???)
          >eq_identifier_false // normalize nodelta
          cases (does_not_occur id' tl) in Hor; normalize nodelta //
-       | normalize nodelta whd in match (occurs_exactly_once ??)
-         change in match (instruction_matches_identifier ??) with (eq_identifier ???)
+       | normalize nodelta whd in match (occurs_exactly_once ??);
+         change in match (instruction_matches_identifier ??); with (eq_identifier ???)
          >eq_identifier_false //
        ] 
@@ -1235 +1235 @@
  #i #id #instr_list elim instr_list
   [ #n #abs whd in abs; cases abs
-  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
-    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
+  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
+    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%);
     [ #H %
-    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
+    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %;
       [ #_ % | #abs cases abs ]]]
 qed.
@@ -1249 +1249 @@
    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
  #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
- change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
+ change with (occurs_exactly_once ?? → ?) generalize in match n; -n -H; elim instr_list
   [ #n #abs cases abs
-  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
+  | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
     [ // | #K @IH //]]
 qed.
@@ -1261 +1261 @@
   = |instr_list| + n.
  #i #id #instr_list elim instr_list
-  [ #n #_ whd in ⊢ (??%%) change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
-  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
+  [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
+  | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
     [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
 qed.
@@ -1275 +1275 @@
   address_of_word_labels_code_mem instr_list id =
   address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
- #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
+ #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
  >(index_of_internal_None … H) %
 qed.
@@ -1284 +1284 @@
    address_of_word_labels_code_mem instr_list id =
    address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
- #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
+ #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
  >(index_of_internal_Some_miss … H) [ @refl | // ]
 qed.
@@ -1292 +1292 @@
    address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    = bitvector_of_nat … (|instr_list|).
- #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
+ #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
  >(index_of_internal_Some_hit … H) <plus_n_O @refl
 qed.