Ignore:
Timestamp:
Nov 21, 2011, 12:10:57 PM (8 years ago)
Author:
campbell
Message:

More syntax updates.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r1515 r1519  
    4141  set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
    4242  #T #U #ps #code_mem #x #val
    43   whd in ⊢ (??%?)
    44   whd in ⊢ (???(???%?))
     43  whd in ⊢ (??%?);
     44  whd in ⊢ (???(???%?));
    4545  cases (eqb ? 128) [ normalize nodelta cases not_implemented
    4646  | normalize nodelta
     
    115115  #n #l #T #U #ps #code_mem #val * *;
    116116  #x try (#y #H) try #H whd in H; try cases H
    117   whd in ⊢ (??(%)?) whd in ⊢ (???(???(%)?)) try %
     117  whd in ⊢ (??(%)?); whd in ⊢ (???(???(%)?)); try %
    118118  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    119119  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     
    137137  #n #l #T #ps #pc #val * *;
    138138  #x try (#y #H) try #H whd in H; try cases H
    139   whd in ⊢ (??(%)?) whd in ⊢ (???(??(%)?)) try %
     139  whd in ⊢ (??(%)?); whd in ⊢ (???(??(%)?)); try %
    140140  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    141141  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     
    175175    special_function_registers_8051 T (write_at_stack_pointer T s x)
    176176  = special_function_registers_8051 T s.
    177  #T #s #x whd in ⊢ (??(??%)?)
     177 #T #s #x whd in ⊢ (??(??%)?);
    178178 cases (split ????) #nu #nl normalize nodelta;
    179179 cases (get_index_v bool ????) %
     
    182182lemma get_8051_sfr_write_at_stack_pointer:
    183183 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
    184  #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl
     184 #T #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
    185185qed.
    186186
    187187lemma code_memory_write_at_stack_pointer:
    188188 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
    189  #T #s #x whd in ⊢ (??(??%)?)
     189 #T #s #x whd in ⊢ (??(??%)?);
    190190 cases (split ????) #nu #nl normalize nodelta;
    191191 cases (get_index_v bool ????) %
     
    229229lemma external_ram_write_at_stack_pointer:
    230230 ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
    231  #T #s #x whd in ⊢ (??(??%)?)
     231 #T #s #x whd in ⊢ (??(??%)?);
    232232 cases (split ????) #nu #nl normalize nodelta;
    233233 cases (get_index_v bool ????) %
     
    238238    special_function_registers_8052 T (write_at_stack_pointer T s x)
    239239  = special_function_registers_8052 T s.
    240  #T #s #x whd in ⊢ (??(??%)?)
     240 #T #s #x whd in ⊢ (??(??%)?);
    241241 cases (split ????) #nu #nl normalize nodelta;
    242242 cases (get_index_v bool ????) %
     
    245245lemma p1_latch_write_at_stack_pointer:
    246246 ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
    247  #T #s #x whd in ⊢ (??(??%)?)
     247 #T #s #x whd in ⊢ (??(??%)?);
    248248 cases (split ????) #nu #nl normalize nodelta;
    249249 cases (get_index_v bool ????) %
     
    252252lemma p3_latch_write_at_stack_pointer:
    253253 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
    254  #T #s #x whd in ⊢ (??(??%)?)
     254 #T #s #x whd in ⊢ (??(??%)?);
    255255 cases (split ????) #nu #nl normalize nodelta;
    256256 cases (get_index_v bool ????) %
     
    259259lemma clock_write_at_stack_pointer:
    260260 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
    261  #T #s #x whd in ⊢ (??(??%)?)
     261 #T #s #x whd in ⊢ (??(??%)?);
    262262 cases (split ????) #nu #nl normalize nodelta;
    263263 cases (get_index_v bool ????) %
     
    269269lemma get_8051_sfr_set_8051_sfr:
    270270 ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
    271  #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
     271 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?);
    272272 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
    273273qed.
Note: See TracChangeset for help on using the changeset viewer.