Changeset 2157 for src/ASM/Assembly.ma
 Timestamp:
 Jul 6, 2012, 11:34:09 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2156 r2157 731 731 whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct % 732 732 qed. 733 734 (* XXX: easy but tedious *) 735 lemma assembly1_lt_128: 736 ∀i: instruction. 737 (assembly1 i) < 128. 738 cases daemon 739 (* XXX: commented out as takes ages to type check 740 #i cases i 741 try (#assm1 #assm2) try #assm1 742 [8: 743 cases assm1 744 try (#assm1 #assm2) try #assm1 745 whd in match assembly1; normalize nodelta 746 whd in match assembly_preinstruction; normalize nodelta 747 try @(subaddressing_mode_elim … assm2) 748 try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta 749 [32: 750 cases assm1 assm1 #assm1 normalize nodelta 751 cases assm1 #addr1 #addr2 normalize nodelta 752 [1: 753 @(subaddressing_mode_elim … addr2) 754 2: 755 @(subaddressing_mode_elim … addr1) 756 ] 757 #w 758 35,36,37: 759 cases assm1 assm1 #assm1 normalize nodelta 760 [1,3: 761 cases assm1 assm1 #assm1 normalize nodelta 762 ] 763 cases assm1 #addr1 #addr2 normalize nodelta 764 @(subaddressing_mode_elim … addr2) try #w 765 49: 766 cases assm1 assm1 #assm1 normalize nodelta 767 [1: 768 cases assm1 assm1 #assm1 normalize nodelta 769 [1: 770 cases assm1 assm1 #assm1 normalize nodelta 771 [1: 772 cases assm1 assm1 #assm1 normalize nodelta 773 [1: 774 cases assm1 assm1 #assm1 normalize nodelta 775 ] 776 ] 777 ] 778 ] 779 cases assm1 #addr1 #addr2 normalize nodelta 780 [1,3,4,5: 781 @(subaddressing_mode_elim … addr2) try #w 782 *: 783 @(subaddressing_mode_elim … addr1) try #w 784 normalize nodelta 785 [1,2: 786 @(subaddressing_mode_elim … addr2) try #w 787 ] 788 ] 789 50: 790 cases assm1 assm1 #assm1 normalize nodelta 791 cases assm1 #addr1 #addr2 normalize nodelta 792 [1: 793 @(subaddressing_mode_elim … addr2) try #w 794 2: 795 @(subaddressing_mode_elim … addr1) try #w 796 ] 797 ] 798 normalize repeat @le_S_S @le_O_n 799 ] 800 whd in match assembly1; normalize nodelta 801 [6: 802 normalize repeat @le_S_S @le_O_n 803 7: 804 @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n 805 *: 806 @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n 807 ] 808 *) 809 qed. 810 811 lemma assembly1_pseudoinstruction_lt_2_to_16: 812 ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi. 813 \snd (assembly_1_pseudoinstruction 814 lookup_labels sigma policy ppc lookup_datalabels pi) 815 < 2^16. 816 #lookup_labels #sigma #policy #ppc #lookup_datalabels * 817 [ cut (128 < 2^16) [@leb_true_to_le %] #LT 818 * whd in match (assembly_1_pseudoinstruction ??????); 819 whd in match (expand_pseudo_instruction ??????); 820 whd in match assembly_1_pseudoinstruction; normalize nodelta 821 try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1 822 whd in match (expand_pseudo_instruction ??????); 823 try 824 (change with (flatten ? [assembly1 ?] < ?) 825 >flatten_singleton 826 @(transitive_lt … (assembly1_lt_128 ?)) 827 @LT) 828 @pair_elim #x #y #_ cases x normalize nodelta 829 try 830 (change with (flatten ? [assembly1 ?] < ?) 831 >flatten_singleton 832 @(transitive_lt … (assembly1_lt_128 ?)) 833 @LT) 834 change with (flatten ? [assembly1 ?; assembly1 ?; assembly1 ?] < ?) 835 >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O 836 <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???)) 837 try @assembly1_lt_128 @leb_true_to_le % 838 2,3: #msg normalize in ⊢ (?%?); // 839  #label whd in match (assembly_1_pseudoinstruction ??????); 840 whd in match (expand_pseudo_instruction ??????); 841 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_ 842 [2: @pair_elim #x #y #_ cases (?∧?)] 843 normalize in ⊢ (?%?); // 844  #label whd in match (assembly_1_pseudoinstruction ??????); 845 whd in match (expand_pseudo_instruction ??????); 846 @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_ 847 normalize in ⊢ (?%?); // 848  #dptr #id normalize in ⊢ (?%?); // 849 ] 850 qed. 851 852 733 853 734 854 definition assembly:
Note: See TracChangeset
for help on using the changeset viewer.