author | paulson |
Fri, 09 Jan 2004 10:46:18 +0100 | |
changeset 14348 | 744c868ee0b7 |
parent 14336 | 8f731d3cd65b |
child 14373 | 67a628beb981 |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title: ComplexArith0.ML |
2 |
Author: Jacques D. Fleuriot |
|
3 |
Copyright: 2001 University of Edinburgh |
|
4 |
Description: Assorted facts that need binary literals |
|
5 |
Also, common factor cancellation (see e.g. HyperArith0) |
|
6 |
*) |
|
7 |
||
8 |
local |
|
9 |
open Complex_Numeral_Simprocs |
|
10 |
in |
|
11 |
||
12 |
val rel_complex_number_of = [eq_complex_number_of]; |
|
13 |
||
14 |
||
15 |
structure CancelNumeralFactorCommon = |
|
16 |
struct |
|
17 |
val mk_coeff = mk_coeff |
|
18 |
val dest_coeff = dest_coeff 1 |
|
19 |
val trans_tac = Real_Numeral_Simprocs.trans_tac |
|
20 |
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps @ mult_1s)) |
|
21 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@complex_mult_minus_simps)) |
|
22 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps complex_mult_ac)) |
|
23 |
val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps rel_complex_number_of@bin_simps)) |
|
24 |
val simplify_meta_eq = simplify_meta_eq |
|
25 |
end |
|
26 |
||
27 |
||
28 |
structure DivCancelNumeralFactor = CancelNumeralFactorFun |
|
29 |
(open CancelNumeralFactorCommon |
|
30 |
val prove_conv = Bin_Simprocs.prove_conv |
|
31 |
val mk_bal = HOLogic.mk_binop "HOL.divide" |
|
32 |
val dest_bal = HOLogic.dest_bin "HOL.divide" complexT |
|
14336 | 33 |
val cancel = mult_divide_cancel_left RS trans |
13957 | 34 |
val neg_exchanges = false |
35 |
) |
|
36 |
||
37 |
||
38 |
structure EqCancelNumeralFactor = CancelNumeralFactorFun |
|
39 |
(open CancelNumeralFactorCommon |
|
40 |
val prove_conv = Bin_Simprocs.prove_conv |
|
41 |
val mk_bal = HOLogic.mk_eq |
|
42 |
val dest_bal = HOLogic.dest_bin "op =" complexT |
|
14336 | 43 |
val cancel = field_mult_cancel_left RS trans |
13957 | 44 |
val neg_exchanges = false |
45 |
) |
|
46 |
||
47 |
val complex_cancel_numeral_factors_relations = |
|
48 |
map prep_simproc |
|
49 |
[("complexeq_cancel_numeral_factor", |
|
50 |
["(l::complex) * m = n", "(l::complex) = m * n"], |
|
51 |
EqCancelNumeralFactor.proc)]; |
|
52 |
||
53 |
val complex_cancel_numeral_factors_divide = prep_simproc |
|
54 |
("complexdiv_cancel_numeral_factor", |
|
55 |
["((l::complex) * m) / n", "(l::complex) / (m * n)", |
|
56 |
"((number_of v)::complex) / (number_of w)"], |
|
57 |
DivCancelNumeralFactor.proc); |
|
58 |
||
59 |
val complex_cancel_numeral_factors = |
|
60 |
complex_cancel_numeral_factors_relations @ |
|
61 |
[complex_cancel_numeral_factors_divide]; |
|
62 |
||
63 |
end; |
|
64 |
||
65 |
||
66 |
Addsimprocs complex_cancel_numeral_factors; |
|
67 |
||
68 |
||
69 |
(*examples: |
|
70 |
print_depth 22; |
|
71 |
set timing; |
|
72 |
set trace_simp; |
|
73 |
fun test s = (Goal s; by (Simp_tac 1)); |
|
74 |
||
75 |
||
76 |
test "9*x = 12 * (y::complex)"; |
|
77 |
test "(9*x) / (12 * (y::complex)) = z"; |
|
78 |
||
79 |
test "-99*x = 132 * (y::complex)"; |
|
80 |
||
81 |
test "999*x = -396 * (y::complex)"; |
|
82 |
test "(999*x) / (-396 * (y::complex)) = z"; |
|
83 |
||
84 |
test "-99*x = -81 * (y::complex)"; |
|
85 |
test "(-99*x) / (-81 * (y::complex)) = z"; |
|
86 |
||
87 |
test "-2 * x = -1 * (y::complex)"; |
|
88 |
test "-2 * x = -(y::complex)"; |
|
89 |
test "(-2 * x) / (-1 * (y::complex)) = z"; |
|
90 |
||
91 |
*) |
|
92 |
||
93 |
||
94 |
(** Declarations for ExtractCommonTerm **) |
|
95 |
||
96 |
local |
|
97 |
open Complex_Numeral_Simprocs |
|
98 |
in |
|
99 |
||
100 |
structure CancelFactorCommon = |
|
101 |
struct |
|
102 |
val mk_sum = long_mk_prod |
|
103 |
val dest_sum = dest_prod |
|
104 |
val mk_coeff = mk_coeff |
|
105 |
val dest_coeff = dest_coeff |
|
106 |
val find_first = find_first [] |
|
107 |
val trans_tac = Real_Numeral_Simprocs.trans_tac |
|
108 |
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@complex_mult_ac)) |
|
109 |
end; |
|
110 |
||
111 |
||
112 |
structure EqCancelFactor = ExtractCommonTermFun |
|
113 |
(open CancelFactorCommon |
|
114 |
val prove_conv = Bin_Simprocs.prove_conv |
|
115 |
val mk_bal = HOLogic.mk_eq |
|
116 |
val dest_bal = HOLogic.dest_bin "op =" complexT |
|
14336 | 117 |
val simplify_meta_eq = cancel_simplify_meta_eq field_mult_cancel_left |
13957 | 118 |
); |
119 |
||
120 |
||
121 |
structure DivideCancelFactor = ExtractCommonTermFun |
|
122 |
(open CancelFactorCommon |
|
123 |
val prove_conv = Bin_Simprocs.prove_conv |
|
124 |
val mk_bal = HOLogic.mk_binop "HOL.divide" |
|
125 |
val dest_bal = HOLogic.dest_bin "HOL.divide" complexT |
|
14336 | 126 |
val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if |
13957 | 127 |
); |
128 |
||
129 |
val complex_cancel_factor = |
|
130 |
map prep_simproc |
|
131 |
[("complex_eq_cancel_factor", ["(l::complex) * m = n", "(l::complex) = m * n"], |
|
132 |
EqCancelFactor.proc), |
|
133 |
("complex_divide_cancel_factor", ["((l::complex) * m) / n", "(l::complex) / (m * n)"], |
|
134 |
DivideCancelFactor.proc)]; |
|
135 |
||
136 |
end; |
|
137 |
||
138 |
Addsimprocs complex_cancel_factor; |
|
139 |
||
140 |
||
141 |
(*examples: |
|
142 |
print_depth 22; |
|
143 |
set timing; |
|
144 |
set trace_simp; |
|
145 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
|
146 |
||
147 |
test "x*k = k*(y::complex)"; |
|
148 |
test "k = k*(y::complex)"; |
|
149 |
test "a*(b*c) = (b::complex)"; |
|
150 |
test "a*(b*c) = d*(b::complex)*(x*a)"; |
|
151 |
||
152 |
||
153 |
test "(x*k) / (k*(y::complex)) = (uu::complex)"; |
|
154 |
test "(k) / (k*(y::complex)) = (uu::complex)"; |
|
155 |
test "(a*(b*c)) / ((b::complex)) = (uu::complex)"; |
|
156 |
test "(a*(b*c)) / (d*(b::complex)*(x*a)) = (uu::complex)"; |
|
157 |
||
158 |
(*FIXME: what do we do about this?*) |
|
159 |
test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z"; |
|
160 |
*) |
|
161 |
||
162 |
||
163 |
(** Division by 1, -1 **) |
|
164 |
||
165 |
Goal "x/-1 = -(x::complex)"; |
|
166 |
by (Simp_tac 1); |
|
167 |
qed "complex_divide_minus1"; |
|
168 |
Addsimps [complex_divide_minus1]; |
|
169 |
||
170 |
Goal "-1/(x::complex) = - (1/x)"; |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14336
diff
changeset
|
171 |
by (simp_tac (simpset() addsimps [complex_divide_def, inverse_minus_eq]) 1); |
13957 | 172 |
qed "complex_minus1_divide"; |
173 |
Addsimps [complex_minus1_divide]; |
|
174 |
||
175 |
Goal "(x + - a = (0::complex)) = (x=a)"; |
|
176 |
by (simp_tac (simpset() addsimps [complex_diff_eq_eq,symmetric complex_diff_def]) 1); |
|
177 |
qed "complex_add_minus_iff"; |
|
178 |
Addsimps [complex_add_minus_iff]; |
|
179 |
||
180 |
Goal "(x+y = (0::complex)) = (y = -x)"; |
|
181 |
by Auto_tac; |
|
182 |
by (dtac (sym RS (complex_diff_eq_eq RS iffD2)) 1); |
|
183 |
by Auto_tac; |
|
184 |
qed "complex_add_eq_0_iff"; |
|
185 |
AddIffs [complex_add_eq_0_iff]; |
|
186 |
||
187 |