 Timestamp:
 Nov 21, 2011, 12:10:57 PM (10 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1515 r1519 40 40 # H2 41 41 normalize 42 change in H2: (??%?) with (orb ??)42 change in H2: (??%?); with (orb ??) 43 43 cases (inclusive_disjunction_true … H2) 44 44 [ # K … … 77 77 # tl 78 78 # II 79 whd in ⊢ (% → ? → ?) 79 whd in ⊢ (% → ? → ?); 80 80 lapply (refl … (is_in … (he:::tl) a)) 81 cases (is_in … (he:::tl) a) in ⊢ (???% → %) 81 cases (is_in … (he:::tl) a) in ⊢ (???% → %); 82 82 [ # K 83 83 # _ 84 84 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 ⊢ (???% → %); 88 88 [ # K1 89 89 # _ 90 change in K1 with ((andb ? (subvector_with …)) = true)90 change in K1; with ((andb ? (subvector_with …)) = true) 91 91 cases (conjunction_true … K1) 92 92 # K3 … … 105 105  # K1 106 106 # K2 107 (normalize in K2 )107 (normalize in K2;) 108 108 cases K2; 109 109 ] 
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.