Changeset 1256 for src/ERTL/ERTLToLTL.ma
- Timestamp:
- Sep 22, 2011, 6:03:03 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLToLTL.ma
r1251 r1256 375 375 ]. 376 376 377 axiom Sm_leq_n_m_leq_n: 378 ∀m, n: nat. 379 S m ≤ n → m ≤ n. 380 381 let rec mapi_aux 382 (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat) 383 on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n ≝ 384 match n return λn. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with 385 [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16. 386 match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with 387 [ Leaf l ⇒ λprf. Leaf … (f accu l) 388 | Stub s ⇒ λprf. Stub … s 389 | Node n' l r ⇒ λabsrd. ⊥ 390 ] (refl … 0) 391 | S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16 - (S n')). 392 match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with 393 [ Leaf l ⇒ λabsrd. ⊥ 394 | Stub s ⇒ λprf. Stub … s 395 | Node n'' l r ⇒ λprf. 396 Node ? n'' ? ? 397 (* (mapi_aux a b f n' ? (l⌈n'' ↦ n'⌉) ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉)) 398 (mapi_aux a b f n' ? (r⌈n'' ↦ n'⌉) ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))*) 399 ] (refl ? (S n')) 400 ]. 401 [ 1,2: destruct(absrd) 402 | 3 : destruct(prf) 403 @(mapi_aux a b f n' ? l ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉)) 404 [ 1: @Sm_leq_n_m_leq_n 405 assumption 406 | 2: <minus_Sn_m 407 [ 1: >minus_S_S % 408 | 2: assumption 409 ] 410 ] 411 | 4 : destruct(prf) 412 @(mapi_aux a b f n' ? r ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉)) 413 [ 1: @Sm_leq_n_m_leq_n 414 assumption 415 | 2: <minus_Sn_m 416 [ 1: >minus_S_S % 417 | 2: assumption 418 ] 419 ] 420 ] 421 qed. 422 423 check mapi_aux. 424 377 425 definition translate_internal ≝ 378 426 λglobals. 379 427 λint_fun. 380 let uses ≝ examine_internal globals int_fun in ?. 428 let uses ≝ examine_internal globals int_fun in 429 let 381 430 382 431 definition translate_funct ≝
Note: See TracChangeset
for help on using the changeset viewer.