1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Aug 31 15:36:57 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Aug 31 16:00:13 2010 +0200
1.3 @@ -2764,8 +2764,8 @@
1.4 rules =
1.5 [Calc ("op =",eval_equal "#equal_"),
1.6 Calc ("Atools.is'_const",eval_const "#is_const_"),
1.7 - Thm ("not_true",num_str not_true),
1.8 - Thm ("not_false",num_str not_false)
1.9 + Thm ("not_true",num_str @{not_true),
1.10 + Thm ("not_false",num_str @{not_false)
1.11 ],
1.12 scr = EmptyScr});
1.13
1.14 @@ -2782,43 +2782,43 @@
1.15 [Calc ("HOL.divide" ,eval_cancel "#divide_"),
1.16
1.17 Thm ("minus_divide_left",
1.18 - num_str (real_minus_divide_eq RS sym)),
1.19 + num_str @{(real_minus_divide_eq RS sym)),
1.20 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.21
1.22 - Thm ("rat_add",num_str rat_add),
1.23 + Thm ("rat_add",num_str @{rat_add),
1.24 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
1.25 \"a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
1.26 - Thm ("rat_add1",num_str rat_add1),
1.27 + Thm ("rat_add1",num_str @{rat_add1),
1.28 (*"[| a is_const; b is_const; c is_const |] ==> \
1.29 \"a / c + b / c = (a + b) / c"*)
1.30 - Thm ("rat_add2",num_str rat_add2),
1.31 + Thm ("rat_add2",num_str @{rat_add2),
1.32 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> \
1.33 \?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
1.34 - Thm ("rat_add3",num_str rat_add3),
1.35 + Thm ("rat_add3",num_str @{rat_add3),
1.36 (*"[| a is_const; b is_const; c is_const |] ==> \
1.37 \"a + b / c = (a * c) / c + b / c"\
1.38 \.... is_const to be omitted here FIXME*)
1.39
1.40 - Thm ("rat_mult",num_str rat_mult),
1.41 + Thm ("rat_mult",num_str @{rat_mult),
1.42 (*a / b * (c / d) = a * c / (b * d)*)
1.43 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
1.44 (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.45 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
1.46 (*?y / ?z * ?x = ?y * ?x / ?z*)
1.47
1.48 - Thm ("real_divide_divide1",num_str real_divide_divide1),
1.49 + Thm ("real_divide_divide1",num_str @{real_divide_divide1),
1.50 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
1.51 Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left}),
1.52 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.53
1.54 - Thm ("rat_power", num_str rat_power),
1.55 + Thm ("rat_power", num_str @{rat_power),
1.56 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.57
1.58 - Thm ("mult_cross",num_str mult_cross),
1.59 + Thm ("mult_cross",num_str @{mult_cross),
1.60 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
1.61 - Thm ("mult_cross1",num_str mult_cross1),
1.62 + Thm ("mult_cross1",num_str @{mult_cross1),
1.63 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
1.64 - Thm ("mult_cross2",num_str mult_cross2)
1.65 + Thm ("mult_cross2",num_str @{mult_cross2)
1.66 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)
1.67 ], scr = EmptyScr})
1.68 calculate_Poly);
1.69 @@ -2912,7 +2912,7 @@
1.70 val SOME (t'',asm) = cancel_p_ thy t
1.71 val der = reverse_deriv thy eval_rls rules ro NONE t'
1.72 val der = der @ [(Thm ("real_mult_div_cancel2",
1.73 - num_str real_mult_div_cancel2),
1.74 + num_str @{real_mult_div_cancel2),
1.75 (t'',asm))]
1.76 val rs = (distinct_Thm o (map #1)) der
1.77 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
1.78 @@ -3043,7 +3043,7 @@
1.79 val SOME (t'',asm) = cancel_ thy t;
1.80 val der = reverse_deriv thy eval_rls rules ro NONE t';
1.81 val der = der @ [(Thm ("real_mult_div_cancel2",
1.82 - num_str real_mult_div_cancel2),
1.83 + num_str @{real_mult_div_cancel2),
1.84 (t'',asm))]
1.85 val rs = map #1 der;
1.86 in (t,t'',[rs],der) end;
1.87 @@ -3137,7 +3137,7 @@
1.88 val SOME (t'',asm) = add_fraction_p_ thy t;
1.89 val der = reverse_deriv thy eval_rls rules ro NONE t';
1.90 val der = der @ [(Thm ("real_mult_div_cancel2",
1.91 - num_str real_mult_div_cancel2),
1.92 + num_str @{real_mult_div_cancel2),
1.93 (t'',asm))]
1.94 val rs = (distinct_Thm o (map #1)) der;
1.95 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
1.96 @@ -3286,7 +3286,7 @@
1.97 val SOME (t'',asm) = add_fraction_ thy t;
1.98 val der = reverse_deriv thy eval_rls rules ro NONE t';
1.99 val der = der @ [(Thm ("real_mult_div_cancel2",
1.100 - num_str real_mult_div_cancel2),
1.101 + num_str @{real_mult_div_cancel2),
1.102 (t'',asm))]
1.103 val rs = (distinct_Thm o (map #1)) der;
1.104 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
1.105 @@ -3457,9 +3457,9 @@
1.106 val discard_minus = prep_rls(
1.107 Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.108 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
1.109 - rules = [Thm ("real_diff_minus", num_str real_diff_minus),
1.110 + rules = [Thm ("real_diff_minus", num_str @{real_diff_minus),
1.111 (*"a - b = a + -1 * b"*)
1.112 - Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
1.113 + Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym))
1.114 (*- ?z = "-1 * ?z"*)
1.115 ],
1.116 scr = Script ((term_of o the o (parse thy))
1.117 @@ -3484,29 +3484,29 @@
1.118 val powers = prep_rls(
1.119 Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.120 erls = powers_erls, srls = Erls, calc = [], (*asm_thm = [],*)
1.121 - rules = [Thm ("realpow_multI", num_str realpow_multI),
1.122 + rules = [Thm ("realpow_multI", num_str @{realpow_multI),
1.123 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.124 - Thm ("realpow_pow",num_str realpow_pow),
1.125 + Thm ("realpow_pow",num_str @{realpow_pow),
1.126 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.127 - Thm ("realpow_oneI",num_str realpow_oneI),
1.128 + Thm ("realpow_oneI",num_str @{realpow_oneI),
1.129 (*"r ^^^ 1 = r"*)
1.130 - Thm ("realpow_minus_even",num_str realpow_minus_even),
1.131 + Thm ("realpow_minus_even",num_str @{realpow_minus_even),
1.132 (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*)
1.133 - Thm ("realpow_minus_odd",num_str realpow_minus_odd),
1.134 + Thm ("realpow_minus_odd",num_str @{realpow_minus_odd),
1.135 (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*)
1.136
1.137 (*----- collect atoms over * -----*)
1.138 - Thm ("realpow_two_atom",num_str realpow_two_atom),
1.139 + Thm ("realpow_two_atom",num_str @{realpow_two_atom),
1.140 (*"r is_atom ==> r * r = r ^^^ 2"*)
1.141 - Thm ("realpow_plus_1",num_str realpow_plus_1),
1.142 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
1.143 (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*)
1.144 - Thm ("realpow_addI_atom",num_str realpow_addI_atom),
1.145 + Thm ("realpow_addI_atom",num_str @{realpow_addI_atom),
1.146 (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.147
1.148 (*----- distribute none-atoms -----*)
1.149 - Thm ("realpow_def_atom",num_str realpow_def_atom),
1.150 + Thm ("realpow_def_atom",num_str @{realpow_def_atom),
1.151 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
1.152 - Thm ("realpow_eq_oneI",num_str realpow_eq_oneI),
1.153 + Thm ("realpow_eq_oneI",num_str @{realpow_eq_oneI),
1.154 (*"1 ^^^ n = 1"*)
1.155 Calc ("op +",eval_binop "#add_")
1.156 ],
1.157 @@ -3518,7 +3518,7 @@
1.158 Rls {id = "rat_mult_divide", preconds = [],
1.159 rew_ord = ("dummy_ord",dummy_ord),
1.160 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
1.161 - rules = [Thm ("rat_mult",num_str rat_mult),
1.162 + rules = [Thm ("rat_mult",num_str @{rat_mult),
1.163 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.164 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
1.165 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.166 @@ -3543,9 +3543,9 @@
1.167 "?x / 1 = ?x" unnecess.for normalform*)
1.168 Thm ("mult_1_left",num_str @{thm mult_1_left}),
1.169 (*"1 * z = z"*)
1.170 - (*Thm ("real_mult_minus1",num_str real_mult_minus1),
1.171 + (*Thm ("real_mult_minus1",num_str @{real_mult_minus1),
1.172 "-1 * z = - z"*)
1.173 - (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
1.174 + (*Thm ("real_minus_mult_cancel",num_str @{real_minus_mult_cancel),
1.175 "- ?x * - ?y = ?x * ?y"*)
1.176
1.177 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1.178 @@ -3555,9 +3555,9 @@
1.179 (*Thm ("right_minus",num_str @{thm right_minus}),
1.180 "?z + - ?z = 0"*)
1.181
1.182 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.183 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
1.184 (*"z1 + z1 = 2 * z1"*)
1.185 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.186 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
1.187 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.188
1.189 Thm ("divide_zero_left",num_str @{thm divide_zero_left})
1.190 @@ -3617,22 +3617,22 @@
1.191 (append_rls "divide" calculate_Rational
1.192 [Thm ("divide_1",num_str @{thm divide_1}),
1.193 (*"?x / 1 = ?x"*)
1.194 - Thm ("rat_mult",num_str rat_mult),
1.195 + Thm ("rat_mult",num_str @{rat_mult),
1.196 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.197 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
1.198 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.199 otherwise inv.to a / b / c = ...*)
1.200 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
1.201 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
1.202 - Thm ("add_minus",num_str add_minus),
1.203 + Thm ("add_minus",num_str @{add_minus),
1.204 (*"?a + ?b - ?b = ?a"*)
1.205 - Thm ("add_minus1",num_str add_minus1),
1.206 + Thm ("add_minus1",num_str @{add_minus1),
1.207 (*"?a - ?b + ?b = ?a"*)
1.208 - Thm ("real_divide_minus1",num_str real_divide_minus1)
1.209 + Thm ("real_divide_minus1",num_str @{real_divide_minus1)
1.210 (*"?x / -1 = - ?x"*)
1.211 (*
1.212 ,
1.213 - Thm ("",num_str )
1.214 + Thm ("",num_str @{)
1.215 *)
1.216 ]);
1.217
1.218 @@ -3674,9 +3674,9 @@
1.219 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.220 srls = Erls, calc = [],
1.221 rules =
1.222 - [Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),
1.223 + [Thm ("rat_mult_poly_l",num_str @{rat_mult_poly_l),
1.224 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.225 - Thm ("rat_mult_poly_r",num_str rat_mult_poly_r)
1.226 + Thm ("rat_mult_poly_r",num_str @{rat_mult_poly_r)
1.227 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.228 ],
1.229 scr = EmptyScr});
1.230 @@ -3696,11 +3696,11 @@
1.231 error "rational.sml.sml: diff.behav. in norm_Rational_mg 29" etc.
1.232 thus we decided to go on with this flaw*)
1.233 srls = Erls, calc = [],
1.234 - rules = [Thm ("rat_mult",num_str rat_mult),
1.235 + rules = [Thm ("rat_mult",num_str @{rat_mult),
1.236 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.237 - Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),
1.238 + Thm ("rat_mult_poly_l",num_str @{rat_mult_poly_l),
1.239 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.240 - Thm ("rat_mult_poly_r",num_str rat_mult_poly_r),
1.241 + Thm ("rat_mult_poly_r",num_str @{rat_mult_poly_r),
1.242 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.243
1.244 Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
1.245 @@ -3711,7 +3711,7 @@
1.246 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.247 Calc ("HOL.divide" ,eval_cancel "#divide_"),
1.248
1.249 - Thm ("rat_power", num_str rat_power)
1.250 + Thm ("rat_power", num_str @{rat_power)
1.251 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.252 ],
1.253 scr = Script ((term_of o the o (parse thy)) "empty_script")