Changeset 1519 for src/ASM/StatusProofs.ma
 Timestamp:
 Nov 21, 2011, 12:10:57 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/StatusProofs.ma
r1515 r1519 41 41 set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem. 42 42 #T #U #ps #code_mem #x #val 43 whd in ⊢ (??%?) 44 whd in ⊢ (???(???%?)) 43 whd in ⊢ (??%?); 44 whd in ⊢ (???(???%?)); 45 45 cases (eqb ? 128) [ normalize nodelta cases not_implemented 46 46  normalize nodelta … … 115 115 #n #l #T #U #ps #code_mem #val * *; 116 116 #x try (#y #H) try #H whd in H; try cases H 117 whd in ⊢ (??(%)?) whd in ⊢ (???(???(%)?))try %117 whd in ⊢ (??(%)?); whd in ⊢ (???(???(%)?)); try % 118 118 cases (split bool 4 4 ?) #nu' #nl' normalize nodelta 119 119 cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta … … 137 137 #n #l #T #ps #pc #val * *; 138 138 #x try (#y #H) try #H whd in H; try cases H 139 whd in ⊢ (??(%)?) whd in ⊢ (???(??(%)?))try %139 whd in ⊢ (??(%)?); whd in ⊢ (???(??(%)?)); try % 140 140 cases (split bool 4 4 ?) #nu' #nl' normalize nodelta 141 141 cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta … … 175 175 special_function_registers_8051 T (write_at_stack_pointer T s x) 176 176 = special_function_registers_8051 T s. 177 #T #s #x whd in ⊢ (??(??%)?) 177 #T #s #x whd in ⊢ (??(??%)?); 178 178 cases (split ????) #nu #nl normalize nodelta; 179 179 cases (get_index_v bool ????) % … … 182 182 lemma get_8051_sfr_write_at_stack_pointer: 183 183 ∀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 @refl184 #T #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl 185 185 qed. 186 186 187 187 lemma code_memory_write_at_stack_pointer: 188 188 ∀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 ⊢ (??(??%)?); 190 190 cases (split ????) #nu #nl normalize nodelta; 191 191 cases (get_index_v bool ????) % … … 229 229 lemma external_ram_write_at_stack_pointer: 230 230 ∀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 ⊢ (??(??%)?); 232 232 cases (split ????) #nu #nl normalize nodelta; 233 233 cases (get_index_v bool ????) % … … 238 238 special_function_registers_8052 T (write_at_stack_pointer T s x) 239 239 = special_function_registers_8052 T s. 240 #T #s #x whd in ⊢ (??(??%)?) 240 #T #s #x whd in ⊢ (??(??%)?); 241 241 cases (split ????) #nu #nl normalize nodelta; 242 242 cases (get_index_v bool ????) % … … 245 245 lemma p1_latch_write_at_stack_pointer: 246 246 ∀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 ⊢ (??(??%)?); 248 248 cases (split ????) #nu #nl normalize nodelta; 249 249 cases (get_index_v bool ????) % … … 252 252 lemma p3_latch_write_at_stack_pointer: 253 253 ∀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 ⊢ (??(??%)?); 255 255 cases (split ????) #nu #nl normalize nodelta; 256 256 cases (get_index_v bool ????) % … … 259 259 lemma clock_write_at_stack_pointer: 260 260 ∀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 ⊢ (??(??%)?); 262 262 cases (split ????) #nu #nl normalize nodelta; 263 263 cases (get_index_v bool ????) % … … 269 269 lemma get_8051_sfr_set_8051_sfr: 270 270 ∀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 ⊢ (??(??%?)?); 272 272 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index 273 273 qed.
Note: See TracChangeset
for help on using the changeset viewer.