 Timestamp:
 Jun 27, 2012, 5:05:33 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r2124 r2128 244 244 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN; 245 245 cases (is_a hd am) in ISIN; /2/ 246 qed. 247 248 lemma is_in_monotonic_wrt_append: 249 ∀m, n: nat. 250 ∀p: Vector addressing_mode_tag m. 251 ∀q: Vector addressing_mode_tag n. 252 ∀to_search: addressing_mode. 253 bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search). 254 #m #n #p #q #to_search #assm 255 elim q try assumption 256 #n' #hd #tl #inductive_hypothesis 257 normalize 258 cases (is_a ??) try @I 259 >inductive_hypothesis @I 260 qed. 261 262 corollary is_in_hd_tl: 263 ∀to_search: addressing_mode. 264 ∀hd: addressing_mode_tag. 265 ∀n: nat. 266 ∀v: Vector addressing_mode_tag n. 267 bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search). 268 #to_search #hd #n #v 269 elim v 270 [1: 271 #absurd 272 normalize in absurd; cases absurd 273 2: 274 #n' #hd' #tl #inductive_hypothesis #assm 275 >vector_cons_append >(vector_cons_append … hd' tl) 276 @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search) 277 assumption 278 ] 246 279 qed. 247 280 
src/ASM/AssemblyProof.ma
r2124 r2128 3 3 include "ASM/StatusProofs.ma". 4 4 include alias "arithmetics/nat.ma". 5 6 lemma is_in_monotonic_wrt_append:7 ∀m, n: nat.8 ∀p: Vector addressing_mode_tag m.9 ∀q: Vector addressing_mode_tag n.10 ∀to_search: addressing_mode.11 bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).12 #m #n #p #q #to_search #assm13 elim q try assumption14 #n' #hd #tl #inductive_hypothesis15 normalize16 cases (is_a ??) try @I17 >inductive_hypothesis @I18 qed.19 20 corollary is_in_hd_tl:21 ∀to_search: addressing_mode.22 ∀hd: addressing_mode_tag.23 ∀n: nat.24 ∀v: Vector addressing_mode_tag n.25 bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).26 #to_search #hd #n #v27 elim v28 [1:29 #absurd30 normalize in absurd; cases absurd31 2:32 #n' #hd' #tl #inductive_hypothesis #assm33 >vector_cons_append >(vector_cons_append … hd' tl)34 @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)35 assumption36 ]37 qed.38 5 39 6 let rec encoding_check
Note: See TracChangeset
for help on using the changeset viewer.