69 result(); |
79 result(); |
70 |
80 |
71 Goal "#1234567 <= #1234567"; |
81 Goal "#1234567 <= #1234567"; |
72 by (Simp_tac 1); |
82 by (Simp_tac 1); |
73 result(); |
83 result(); |
|
84 |
|
85 |
|
86 Addsimps normal.intrs; |
|
87 |
|
88 Goal "(w BIT b): normal ==> (w BIT b BIT c): normal"; |
|
89 by (case_tac "c" 1); |
|
90 by Auto_tac; |
|
91 qed "normal_BIT_I"; |
|
92 |
|
93 Addsimps [normal_BIT_I]; |
|
94 |
|
95 Goal "w BIT b: normal ==> w: normal"; |
|
96 by (etac normal.elim 1); |
|
97 by Auto_tac; |
|
98 qed "normal_BIT_D"; |
|
99 |
|
100 Goal "w : normal --> NCons w b : normal"; |
|
101 by (induct_tac "w" 1); |
|
102 by (auto_tac (claset(), simpset() addsimps [NCons_Pls, NCons_Min])); |
|
103 qed_spec_mp "NCons_normal"; |
|
104 |
|
105 Addsimps [NCons_normal]; |
|
106 |
|
107 Goal "NCons w True ~= Pls"; |
|
108 by (induct_tac "w" 1); |
|
109 by Auto_tac; |
|
110 qed "NCons_True"; |
|
111 |
|
112 Goal "NCons w False ~= Min"; |
|
113 by (induct_tac "w" 1); |
|
114 by Auto_tac; |
|
115 qed "NCons_False"; |
|
116 |
|
117 Goal "w: normal ==> bin_succ w : normal"; |
|
118 by (etac normal.induct 1); |
|
119 by (exhaust_tac "w" 4); |
|
120 by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT])); |
|
121 qed "bin_succ_normal"; |
|
122 |
|
123 Goal "w: normal ==> bin_pred w : normal"; |
|
124 by (etac normal.induct 1); |
|
125 by (exhaust_tac "w" 3); |
|
126 by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT])); |
|
127 qed "bin_pred_normal"; |
|
128 |
|
129 Addsimps [bin_succ_normal, bin_pred_normal]; |
|
130 |
|
131 Goal "w : normal --> (ALL z. z: normal --> bin_add w z : normal)"; |
|
132 by (induct_tac "w" 1); |
|
133 by (Simp_tac 1); |
|
134 by (Simp_tac 1); |
|
135 by (rtac impI 1); |
|
136 by (rtac allI 1); |
|
137 by (induct_tac "z" 1); |
|
138 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT]))); |
|
139 by (safe_tac (claset() addSDs [normal_BIT_D])); |
|
140 by (ALLGOALS Asm_simp_tac); |
|
141 qed_spec_mp "bin_add_normal"; |
|
142 |
|
143 |
|
144 |
|
145 Goal "w: normal ==> (w = Pls) = (integ_of w = #0)"; |
|
146 by (etac normal.induct 1); |
|
147 by Auto_tac; |
|
148 qed "normal_Pls_eq_0"; |
|
149 |
|
150 Goal "w : normal ==> bin_minus w : normal"; |
|
151 by (etac normal.induct 1); |
|
152 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT]))); |
|
153 by (resolve_tac normal.intrs 1); |
|
154 by (assume_tac 1); |
|
155 by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1); |
|
156 by (asm_full_simp_tac |
|
157 (simpset_of Integ.thy addsimps [integ_of_minus, iszero_def, |
|
158 zminus_exchange]) 1); |
|
159 qed "bin_minus_normal"; |
|
160 |
|
161 |
|
162 Goal "w : normal ==> z: normal --> bin_mult w z : normal"; |
|
163 by (etac normal.induct 1); |
|
164 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_normal, |
|
165 bin_mult_BIT]))); |
|
166 by (safe_tac (claset() addSDs [normal_BIT_D])); |
|
167 by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1); |
|
168 qed_spec_mp "bin_mult_normal"; |
|
169 |