Changeset 2281 for src/ASM/Test.ma
- Timestamp:
- Jul 31, 2012, 2:22:35 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2279 r2281 445 445 qed. 446 446 447 lemma set_low_internal_ram_status_of_pseudo_status:448 ∀cm,sigma,policy,M,s,s',ram.449 s' = status_of_pseudo_status M cm s sigma policy →450 set_low_internal_ram (BitVectorTrie Byte 16)451 (code_memory_of_pseudo_assembly_program cm sigma policy)452 s'453 (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)454 = status_of_pseudo_status M cm455 (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.456 #cm #sigma #policy #M #s #s' #ram #s_refl >s_refl //457 qed.458 459 447 (* Real axiom ATM *) 460 448 axiom insert_low_internal_ram_of_pseudo_low_internal_ram: … … 573 561 qed. 574 562 563 definition internal_pseudo_address_map_equal_up_to_low ≝ 564 λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \snd (\fst M) = \snd (\fst M'). 565 566 lemma set_low_internal_ram_status_of_pseudo_status2: 567 ∀cm,sigma,policy,M,M',s,s',ram,ram'. 568 internal_pseudo_address_map_equal_up_to_low M M' → 569 s' = status_of_pseudo_status M' cm s sigma policy → 570 ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) → 571 set_low_internal_ram (BitVectorTrie Byte 16) 572 (code_memory_of_pseudo_assembly_program cm sigma policy) 573 s' 574 ram' 575 = status_of_pseudo_status M cm 576 (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy. 577 #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl 578 cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H 579 #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status % 580 qed. 581 582 lemma set_low_internal_ram_status_of_pseudo_status: 583 ∀cm,sigma,policy,M,s,s',ram,ram'. 584 s' = status_of_pseudo_status M cm s sigma policy → 585 ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) → 586 set_low_internal_ram (BitVectorTrie Byte 16) 587 (code_memory_of_pseudo_assembly_program cm sigma policy) 588 s' 589 ram' 590 = status_of_pseudo_status M cm 591 (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy. 592 #cm #sigma #policy #M #s #s' #ram #ram' @set_low_internal_ram_status_of_pseudo_status2 593 % % 594 qed. 595 575 596 lemma set_register_status_of_pseudo_status: 576 597 ∀M,sigma,policy,cm,s,s',r,v,v'. … … 586 607 whd in match set_register; normalize nodelta 587 608 >bit_address_of_register_status_of_pseudo_status 609 @set_low_internal_ram_status_of_pseudo_status try % 588 610 >(insert_low_internal_ram_status_of_pseudo_status … v_ok) 589 @set_low_internal_ram_status_of_pseudo_status%611 cases M * #low #high #accA % 590 612 qed. 591 613 … … 1945 1967 *) 1946 1968 1947 definition internal_pseudo_address_map_equal_up_to_low ≝1948 λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \snd (\fst M) = \snd (\fst M').1949 1950 lemma set_low_internal_ram_status_of_pseudo_status:1951 ∀cm,sigma,policy,M,M',s,s',ram,ram'.1952 internal_pseudo_address_map_equal_up_to_low M M' →1953 s' = status_of_pseudo_status M' cm s sigma policy →1954 ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →1955 set_low_internal_ram (BitVectorTrie Byte 16)1956 (code_memory_of_pseudo_assembly_program cm sigma policy)1957 s'1958 ram'1959 = status_of_pseudo_status M cm1960 (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.1961 #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl1962 cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H1963 #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %1964 qed.1965 1969 1966 1970 definition internal_pseudo_address_map_equal_up_to_high ≝ … … 2021 2025 whd in match high_internal_ram_of_pseudo_high_internal_ram; normalize nodelta 2022 2026 @insert_internal_ram_of_pseudo_internal_ram assumption 2023 | @(set_low_internal_ram_status_of_pseudo_status … 〈low',high',accA'〉 〈low,high,accA〉)2027 | @(set_low_internal_ram_status_of_pseudo_status2 … 〈low',high',accA'〉 〈low,high,accA〉) 2024 2028 try @refl try assumption 2025 2029 whd in match status_of_pseudo_status; normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.