Changeset 1519 for src/ASM


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

More syntax updates.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1515 r1519  
    4040   # H2
    4141   normalize
    42    change in H2: (??%?) with (orb ??)
     42   change in H2: (??%?); with (orb ??)
    4343   cases (inclusive_disjunction_true … H2)
    4444   [ # K
     
    7777   # tl
    7878   # II
    79    whd in ⊢ (% → ? → ?)
     79   whd in ⊢ (% → ? → ?);
    8080   lapply (refl … (is_in … (he:::tl) a))
    81    cases (is_in … (he:::tl) a) in ⊢ (???% → %)
     81   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
    8282   [ # K
    8383     # _
    8484     normalize in K;
    85      whd in ⊢ (% → ?)
    86      lapply (refl … (subvector_with … eq_a (he:::tl) q))
    87      cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
     85     whd in ⊢ (% → ?);
     86     lapply (refl … (subvector_with … eq_a (he:::tl) q));
     87     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
    8888     [ # K1
    8989       # _
    90        change in K1 with ((andb ? (subvector_with …)) = true)
     90       change in K1; with ((andb ? (subvector_with …)) = true)
    9191       cases (conjunction_true … K1)
    9292       # K3
     
    105105     | # K1
    106106       # K2
    107        (normalize in K2)
     107       (normalize in K2;)
    108108       cases K2;
    109109     ]
  • 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.