Changeset 1052 for src/utilities/HMap.ma
 Timestamp:
 Jul 4, 2011, 3:31:18 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/HMap.ma
r1050 r1052 230 230 ]. 231 231 232 lemma map_double_r_property_p_exists: 233 ∀key_type. 234 ∀elt_type. 235 ∀left: map key_type elt_type. 236 map_double_r_property_p key_type elt_type left → 237 ∃l_sz, l_key, l_elt, l_l, l_r. 238 left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r. 239 #KEY_TYPE #ELT_TYPE #LEFT 240 cases LEFT 241 [ normalize #HYP cases HYP 242  #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT 243 #HYP 244 @ex_intro 245 [1: @L_SZ 246 2: @ex_intro 247 [1: @L_KEY 248 2: @ex_intro 249 [1: @L_ELT 250 2: @ex_intro 251 [1: @L_LEFT 252 2: @ex_intro 253 [1: @L_RIGHT 254 2: % 255 ] 256 ] 257 ] 258 ] 259 ] 260 ] 261 qed. 262 263 lemma map_double_r_property_p_exists_l_r_not_nil_p: 264 ∀key_type. 265 ∀elt_type. 266 ∀left: map key_type elt_type. 267 map_double_r_property_p key_type elt_type left → 268 ∃l_sz, l_key, l_elt, l_l, l_r. 269 (left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r) ∧ 270 map_not_nil_p key_type elt_type l_r. 271 #KEY_TYPE #ELT_TYPE #LEFT 272 cases LEFT 273 [ normalize #HYP cases HYP 274  #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT 275 #HYP 276 @ex_intro 277 [1: @L_SZ 278 2: @ex_intro 279 [1: @L_KEY 280 2: @ex_intro 281 [1: @L_ELT 282 2: @ex_intro 283 [1: @L_LEFT 284 2: @ex_intro 285 [1: @L_RIGHT 286 2: @conj 287 [1: % 288 2: generalize in match HYP 289 cases L_RIGHT 290 [1: normalize // 291 2: #NEW_SZ #NEW_KEY #NEW_ELT #NEW_L #NEW_R 292 normalize // 293 ] 294 ] 295 ] 296 ] 297 ] 298 ] 299 ] 300 ] 301 qed. 302 232 303 definition map_double_r ≝ 233 304 λkey_type. … … 246 317 ] 247 318 ]. 248 249 definition map_double_r_safe ≝250 λkey_type.251 λelt_type.252 λkey: key_type.253 λelt: elt_type.254 λleft: map key_type elt_type.255 λright: map key_type elt_type.256 λprf: map_double_r_property_p key_type elt_type left.257 match left return λx. map_double_r_property_p key_type elt_type x → map key_type elt_type with258 [ map_nil ⇒ λleft_nil_absrd. ?259  map_fork l_sz l_key l_elt l_l l_r ⇒ λouter_prf.260 match l_r return λx. map_double_r_property_p key_type elt_type x → map key_type elt_type with261 [ map_nil ⇒ λl_r_nil_absrd. ?262  map_fork lr_sz lr_key lr_elt lr_l lr_r ⇒263 λl_r_fork_prf. map_binsert … lr_key lr_elt (map_binsert … l_key l_elt l_l lr_l) (map_binsert … key elt lr_r right)264 ] ?265 ] prf.266 [1: normalize in left_nil_absrd;267 cases left_nil_absrd;268 3: normalize in l_r_nil_absrd;269 cases l_r_nil_absrd;270 2: normalize in outer_prf;271 generalize in match outer_prf;272 cases l_r;273 [ normalize //274  #SZ #KEY_TYPE #ELT_TYPE #LEFT #RIGHT275 normalize276 #HYP277 ]278 qed.279 319 280 320 definition map_double_l ≝
Note: See TracChangeset
for help on using the changeset viewer.