Changeset 1356
 Timestamp:
 Oct 11, 2011, 5:33:11 PM (9 years ago)
 Files:

 3 added
 1 deleted
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r1354 r1356 89 89 ] 90 90 in 91 foldl ? ?initialize_local_env_internal 〈Stub …,runiverse〉 registers.91 foldl … initialize_local_env_internal 〈Stub …,runiverse〉 registers. 92 92 93 93 definition map_list_local_env_internal ≝ … … 550 550 in 551 551 translates @ tmp_destrs2'. 552 553 let rec remove_n_first_internal 554 (b: Type[0]) (n: nat) (the_list: list b) (i: nat) 555 on the_list ≝ 556 match the_list with 557 [ nil ⇒ [ ] 558  cons hd tl ⇒ 559 match eqb i n with 560 [ true ⇒ the_list 561  false ⇒ remove_n_first_internal b n tl (S i) 562 ] 563 ]. 564 565 definition remove_n_first ≝ 566 λb: Type[0]. 567 λn: nat. 568 λthe_list: list b. 569 remove_n_first_internal b n the_list 0. 570 571 axiom plus_m_n_eq_o_to_lt_m_o: 572 ∀m, n, o: nat. 573 m + n = o → m ≤ o. 574 575 include alias "arithmetics/nat.ma". 576 577 axiom minus_m_n_Sp_to_minus_m_Sn_p: 578 ∀m, n, p: nat. 579 minus m n = S p → minus m (S n) = p. 580 581 let rec foldi_strong_internal 582 (a: Type[0]) (b: Type[0]) (reference: nat) (the_list: list b) 583 (f: ∀j: nat. ∀proof: lt j (the_list). a → b → a) (seed: a) 584 (counter: nat) (counter_proof: minus reference counter = the_list) 585 on the_list: a ≝ 586 match the_list return λx. the_list = x → (minus reference counter = x) → a with 587 [ nil ⇒ λidentity. λbase_case. seed 588  cons hd tl ⇒ λidentity. λstep_case. 589 let f' ≝ λj: nat. λproof: j < tl. f j ? in 590 foldi_strong_internal a b reference tl f' (f counter ? seed hd) (S counter) ? 591 ] (refl … the_list) counter_proof. 592 [1: cut(reference > 0) 593 [2: #REFERENCE_HYP 594 2: generalize in match counter_proof; 595 >identity 596 #HYP 597 normalize in HYP:(???%); 598 generalize in match (minus_m_n_Sp_to_minus_m_Sn_p reference counter (tl) HYP); 599 #ASSM assumption 600 3: >identity 601 normalize 602 normalize in proof; 603 generalize in match(le_S … proof); 604 #HYP assumption 605 ] 606 qed. 607 608 609 let rec foldi_strong_from_until_internal 610 (a: Type[0]) (b: Type[0]) (the_list: list b) 611 (f: ∀j: nat. ∀proof: j ≤ the_list. a → b → a) (m: nat) (i: nat) (res: a) 612 (proof: i ≤ the_list) (m_length_proof: m = the_list) 613 on the_list: a ≝ 614 match the_list return λx. the_list = x → i ≤ x → a with 615 [ nil ⇒ λidentity. λsnd_proof. res 616  cons hd tl ⇒ λidentity. λsnd_proof. 617 match geb i m return λx. geb i m = x → a with 618 [ true ⇒ λabsrd_prf. res 619  false ⇒ λotherwise. 620 let f' ≝ λj. λthrd_proof: j ≤ tl. f j ? in 621 foldi_strong_from_until_internal a b tl f' m (S i) (f' i ? res hd) ? ? 622 ] (refl … (geb i m)) 623 ] (refl … the_list) proof. 624 [1: generalize in match otherwise; 625 >m_length_proof 626 >identity 627 #HYP 628 cases(geb_false_nge … HYP) 629 #HYP2 630 cases(ge_m_n_False_to_lt_m_n … HYP2) 631 2: 632 qed. 633 634 definition foldi_strong_from_until ≝ 635 λa: Type[0]. 636 λb: Type[0]. 637 λn: nat. 638 λm: nat. 639 λthe_list: list b. 640 λf: (∀i: nat. ∀proof: i ≤ the_list. a → b → a). 641 λseed: a. 642 λlength_proof: m = the_list. 643 foldi_strong_from_until_internal a b the_list f m 0 seed ? length_proof. 644 // 645 qed. 552 646 553 axiom foldi_strong: 554 ∀a: Type[0].555 ∀b: Type[0].556 ∀the_list: list b.557 ∀f: (∀i: nat. ∀proof: i ≤ the_list. a → b → a).558 ∀seed: a.559 a.647 definition foldi_strong ≝ 648 λa: Type[0]. 649 λb: Type[0]. 650 λthe_list: list b. 651 λf: (∀i: nat. ∀proof: i ≤ the_list. a → b → a). 652 λseed: a. 653 foldi_strong_from_until a b 0 (the_list) the_list f seed. 560 654 561 655 definition translate_mul ≝
Note: See TracChangeset
for help on using the changeset viewer.