1.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue Jul 26 16:50:27 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Wed Jul 27 09:30:15 2011 +0200
1.3 @@ -43,32 +43,32 @@
1.4 ("filter'_sameFunId _ _" 10)
1.5 boollist2sum :: "bool list => real"
1.6
1.7 -axiomatization where (*for evaluating the assumptions of conditional rules*)
1.8 +axioms(*axiomatization where*) (*for evaluating the assumptions of conditional rules*)
1.9
1.10 - last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and
1.11 - real_unari_minus: "- a = (-1) * a" and
1.12 + last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" (*and*)
1.13 + real_unari_minus: "- a = (-1) * a" (*and*)
1.14
1.15 - rle_refl: "(n::real) <= n" and
1.16 - radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
1.17 - not_true: "(~ True) = False" and
1.18 + rle_refl: "(n::real) <= n" (*and*)
1.19 + radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" (*and*)
1.20 + not_true: "(~ True) = False" (*and*)
1.21 not_false: "(~ False) = True"
1.22 -axiomatization where (*..if replaced by "and" we get error:
1.23 +axioms(*axiomatization where*) (*..if replaced by "and" we get error:
1.24 Type unification failed: No type arity bool :: zero ...*)
1.25 - and_true: "(a & True) = a" and
1.26 - and_false: "(a & False) = False" and
1.27 - or_true: "(a | True) = True" and
1.28 - or_false: "(a | False) = a" and
1.29 - and_commute: "(a & b) = (b & a)" and
1.30 + and_true: "(a & True) = a" (*and*)
1.31 + and_false: "(a & False) = False" (*and*)
1.32 + or_true: "(a | True) = True" (*and*)
1.33 + or_false: "(a | False) = a" (*and*)
1.34 + and_commute: "(a & b) = (b & a)" (*and*)
1.35 or_commute: "(a | b) = (b | a)"
1.36
1.37 (*.should be in Rational.thy, but:
1.38 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
1.39 - axiomatization where (*..if replaced by "and" we get error:
1.40 +axioms(*axiomatization where*) (*..if replaced by "and" we get error:
1.41 Type unification failed: No type arity bool :: zero ...*)
1.42 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
1.43 - ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
1.44 + ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) (*and*)
1.45 rat_leq2: "d ~= 0 ==>
1.46 - ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
1.47 + ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) (*and*)
1.48 rat_leq3: "b ~= 0 ==>
1.49 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
1.50
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Tue Jul 26 16:50:27 2011 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Jul 27 09:30:15 2011 +0200
2.3 @@ -56,16 +56,16 @@
2.4 bool list] => bool list"
2.5 ("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
2.6
2.7 -axiomatization where
2.8 +axioms(*axiomatization where*)
2.9
2.10 - Querkraft_Belastung: "Q' x = -q_ x" and
2.11 - Belastung_Querkraft: "-q_ x = Q' x" and
2.12 + Querkraft_Belastung: "Q' x = -q_ x" (*and*)
2.13 + Belastung_Querkraft: "-q_ x = Q' x" (*and*)
2.14
2.15 - Moment_Querkraft: "M_b' x = Q x" and
2.16 - Querkraft_Moment: "Q x = M_b' x" and
2.17 + Moment_Querkraft: "M_b' x = Q x" (*and*)
2.18 + Querkraft_Moment: "Q x = M_b' x" (*and*)
2.19
2.20 - Neigung_Moment: "y'' x = -M_b x/ EI" and
2.21 - Moment_Neigung: "M_b x = -EI * y'' x" and
2.22 + Neigung_Moment: "y'' x = -M_b x/ EI" (*and*)
2.23 + Moment_Neigung: "M_b x = -EI * y'' x" (*and*)
2.24
2.25 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
2.26 make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
3.1 --- a/src/Tools/isac/Knowledge/Delete.thy Tue Jul 26 16:50:27 2011 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Wed Jul 27 09:30:15 2011 +0200
3.3 @@ -5,13 +5,13 @@
3.4
3.5 theory Delete imports "../ProgLang/ProgLang" begin
3.6
3.7 -axiomatization where (* theorems which are available only with long names,
3.8 +axioms(*axiomatization where*) (* theorems which are available only with long names,
3.9 which can not yet be handled in isac's scripts *)
3.10
3.11 - real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" and
3.12 + real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" (*and*)
3.13 (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)
3.14 - real_mult_minus1: "-1 * z = - (z::real)" and
3.15 - real_mult_2: "2 * z = z + (z::real)" and
3.16 + real_mult_minus1: "-1 * z = - (z::real)" (*and*)
3.17 + real_mult_2: "2 * z = z + (z::real)" (*and*)
3.18 real_diff_0: "0 - x = - (x::real)"
3.19
3.20
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Jul 26 16:50:27 2011 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Jul 27 09:30:15 2011 +0200
4.3 @@ -50,29 +50,29 @@
4.4 disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
4.5 *}
4.6
4.7 -axiomatization where (*stated as axioms, todo: prove as theorems
4.8 +axioms(*axiomatization where*) (*stated as axioms, todo: prove as theorems
4.9 'bdv' is a constant on the meta-level *)
4.10 - diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" and
4.11 - diff_var: "d_d bdv bdv = 1" and
4.12 + diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" (*and*)
4.13 + diff_var: "d_d bdv bdv = 1" (*and*)
4.14 diff_prod_const:"[| Not (bdv occurs_in u) |] ==>
4.15 - d_d bdv (u * v) = u * d_d bdv v" and
4.16 + d_d bdv (u * v) = u * d_d bdv v" (*and*)
4.17
4.18 - diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v" and
4.19 - diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v" and
4.20 - diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" and
4.21 + diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v" (*and*)
4.22 + diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v" (*and*)
4.23 + diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" (*and*)
4.24 diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) =
4.25 - (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" and
4.26 + (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" (*and*)
4.27
4.28 - diff_sin: "d_d bdv (sin bdv) = cos bdv" and
4.29 - diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u" and
4.30 - diff_cos: "d_d bdv (cos bdv) = - sin bdv" and
4.31 - diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u" and
4.32 - diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" and
4.33 - diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" and
4.34 - diff_ln: "d_d bdv (ln bdv) = 1 / bdv" and
4.35 - diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u" and
4.36 - diff_exp: "d_d bdv (exp bdv) = exp bdv" and
4.37 - diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u" and
4.38 + diff_sin: "d_d bdv (sin bdv) = cos bdv" (*and*)
4.39 + diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u" (*and*)
4.40 + diff_cos: "d_d bdv (cos bdv) = - sin bdv" (*and*)
4.41 + diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u" (*and*)
4.42 + diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" (*and*)
4.43 + diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" (*and*)
4.44 + diff_ln: "d_d bdv (ln bdv) = 1 / bdv" (*and*)
4.45 + diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u" (*and*)
4.46 + diff_exp: "d_d bdv (exp bdv) = exp bdv" (*and*)
4.47 + diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u" (*and*)
4.48 (*
4.49 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
4.50 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
4.51 @@ -80,16 +80,16 @@
4.52 (*...*)
4.53
4.54 frac_conv: "[| bdv occurs_in b; 0 < n |] ==>
4.55 - a / (b ^^^ n) = a * b ^^^ (-n)" and
4.56 - frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" and
4.57 + a / (b ^^^ n) = a * b ^^^ (-n)" (*and*)
4.58 + frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" (*and*)
4.59
4.60 - sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)" and
4.61 - sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" and
4.62 - sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" and
4.63 - sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)" and
4.64 + sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)" (*and*)
4.65 + sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" (*and*)
4.66 + sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" (*and*)
4.67 + sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)" (*and*)
4.68
4.69 - root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" and
4.70 - root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)" and
4.71 + root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" (*and*)
4.72 + root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)" (*and*)
4.73
4.74 realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
4.75
5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Tue Jul 26 16:50:27 2011 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Jul 27 09:30:15 2011 +0200
5.3 @@ -28,8 +28,8 @@
5.4 (*for script Maximum_value*)
5.5 filterVar :: "[real, 'a list] => 'a list"
5.6
5.7 -(*primrec*)axiomatization where
5.8 - filterVar_Nil: "filterVar v [] = []" and
5.9 +(*primrec*)axioms(*axiomatization where*)
5.10 + filterVar_Nil: "filterVar v [] = []" (*and*)
5.11 filterVar_Const: "filterVar v (x#xs) =
5.12 (if (v : set (Vars x)) then x#(filterVar v xs)
5.13 else filterVar v xs) "
6.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Tue Jul 26 16:50:27 2011 +0200
6.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed Jul 27 09:30:15 2011 +0200
6.3 @@ -12,7 +12,7 @@
6.4 Diophant'_equation :: "[bool, int, bool ]
6.5 => bool "
6.6 ("((Script Diophant'_equation (_ _ =))//(_))" 9)
6.7 -axiomatization where
6.8 +axioms(*axiomatization where*)
6.9
6.10 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
6.11
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Jul 26 16:50:27 2011 +0200
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Jul 27 09:30:15 2011 +0200
7.3 @@ -23,31 +23,31 @@
7.4 => bool list"
7.5 ("((Script SolveSystemScript (_ _ =))// (_))" 9)
7.6
7.7 -axiomatization where
7.8 +axioms(*axiomatization where *)
7.9 (*stated as axioms, todo: prove as theorems
7.10 'bdv' is a constant handled on the meta-level
7.11 specifically as a 'bound variable' *)
7.12
7.13 - commute_0_equality: "(0 = a) = (a = 0)" and
7.14 + commute_0_equality: "(0 = a) = (a = 0)" (*and*)
7.15
7.16 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
7.17 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
7.18 separate_bdvs_add:
7.19 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]
7.20 - ==> (a + b = c) = (b = c + -1*a)" and
7.21 + ==> (a + b = c) = (b = c + -1*a)" (*and*)
7.22 separate_bdvs0:
7.23 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |]
7.24 - ==> (a = b) = (a + -1*b = 0)" and
7.25 + ==> (a = b) = (a + -1*b = 0)" (*and*)
7.26 separate_bdvs_add1:
7.27 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]
7.28 - ==> (a = b + c) = (a + -1*c = b)" and
7.29 + ==> (a = b + c) = (a + -1*c = b)" (*and*)
7.30 separate_bdvs_add2:
7.31 "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |]
7.32 - ==> (a + b = c) = (b = -1*a + c)" and
7.33 + ==> (a + b = c) = (b = -1*a + c)" (*and*)
7.34 separate_bdvs_mult:
7.35 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]
7.36 ==>(a * b = c) = (b = c / a)"
7.37 -axiomatization where (*..if replaced by "and" we get an error in
7.38 +axioms(*axiomatization where*) (*..if replaced by "and" we get an error in
7.39 --- rewrite in [EqSystem,normalize,2x2] --- step "--- 3---";*)
7.40 order_system_NxN: "[a,b] = [b,a]"
7.41 (*requires rew_ord for termination, eg. ord_simplify_Integral;
8.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Tue Jul 26 16:50:27 2011 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Jul 27 09:30:15 2011 +0200
8.3 @@ -26,18 +26,18 @@
8.4 NamedIntegrationScript :: "[real,real, real=>real, bool] => bool"
8.5 ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
8.6
8.7 -axiomatization where
8.8 +axioms(*axiomatization where*)
8.9 (*stated as axioms, todo: prove as theorems
8.10 'bdv' is a constant handled on the meta-level
8.11 specifically as a 'bound variable' *)
8.12
8.13 - integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
8.14 - integral_var: "Integral bdv D bdv = bdv ^^^ 2 / 2" and
8.15 + integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" (*and*)
8.16 + integral_var: "Integral bdv D bdv = bdv ^^^ 2 / 2" (*and*)
8.17
8.18 integral_add: "Integral (u + v) D bdv =
8.19 - (Integral u D bdv) + (Integral v D bdv)" and
8.20 + (Integral u D bdv) + (Integral v D bdv)" (*and*)
8.21 integral_mult: "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>
8.22 - Integral (u * v) D bdv = u * (Integral v D bdv)" and
8.23 + Integral (u * v) D bdv = u * (Integral v D bdv)" (*and*)
8.24 (*WN080222: this goes into sub-terms, too ...
8.25 call_for_new_c: "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>
8.26 a = a + new_c a"
9.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Jul 26 16:50:27 2011 +0200
9.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Jul 27 09:30:15 2011 +0200
9.3 @@ -16,17 +16,17 @@
9.4 ("((Script Solve'_lineq'_equation (_ _ =))//
9.5 (_))" 9)
9.6
9.7 -axiomatization where
9.8 +axioms(*axiomatization where*)
9.9 (*-- normalize --*)
9.10 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
9.11 - all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
9.12 - makex1_x: "a^^^1 = a" and
9.13 - real_assoc_1: "a+(b+c) = a+b+c" and
9.14 - real_assoc_2: "a*(b*c) = a*b*c" and
9.15 + all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
9.16 + makex1_x: "a^^^1 = a"
9.17 + real_assoc_1: "a+(b+c) = a+b+c"
9.18 + real_assoc_2: "a*(b*c) = a*b*c"
9.19
9.20 (*-- solve --*)
9.21 - lin_isolate_add1: "(a + b*bdv = 0) = (b*bdv = (-1)*a)" and
9.22 - lin_isolate_add2: "(a + bdv = 0) = ( bdv = (-1)*a)" and
9.23 + lin_isolate_add1: "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
9.24 + lin_isolate_add2: "(a + bdv = 0) = ( bdv = (-1)*a)"
9.25 lin_isolate_div: "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
9.26
9.27 ML {*
10.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Tue Jul 26 16:50:27 2011 +0200
10.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Jul 27 09:30:15 2011 +0200
10.3 @@ -17,11 +17,11 @@
10.4 => bool list"
10.5 ("((Script Solve'_log (_ _=))//(_))" 9)
10.6
10.7 -axiomatization where
10.8 +axioms(*axiomatization where*)
10.9
10.10 - equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)" and
10.11 + equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)" (*and*)
10.12 (* this is what students ^^^^^^^... are told to do *)
10.13 - equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)" and
10.14 + equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)" (*and*)
10.15 exp_invers_log: "a^^^(a log b) = b"
10.16
10.17 ML {*
11.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Jul 26 16:50:27 2011 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Jul 27 09:30:15 2011 +0200
11.3 @@ -27,111 +27,111 @@
11.4 (_))" 9)
11.5
11.6 (*-------------------- rules------------------------------------------------*)
11.7 -axiomatization where (*.not contained in Isabelle2002,
11.8 +axioms(*axiomatization where*) (*.not contained in Isabelle2002,
11.9 stated as axioms, TODO: prove as theorems;
11.10 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
11.11
11.12 - realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
11.13 - realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
11.14 - realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
11.15 - realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
11.16 + realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" (*and*)
11.17 + realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" (*and*)
11.18 + realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" (*and*)
11.19 + realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" (*and*)
11.20
11.21 - realpow_oneI: "r ^^^ 1 = r" and
11.22 - realpow_zeroI: "r ^^^ 0 = 1" and
11.23 - realpow_eq_oneI: "1 ^^^ n = 1" and
11.24 - realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
11.25 + realpow_oneI: "r ^^^ 1 = r" (*and*)
11.26 + realpow_zeroI: "r ^^^ 0 = 1" (*and*)
11.27 + realpow_eq_oneI: "1 ^^^ n = 1" (*and*)
11.28 + realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" (*and*)
11.29 realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
11.30 - (r * s) ^^^ n = r ^^^ n * s ^^^ n" and
11.31 - realpow_minus_oneI: "-1 ^^^ (2 * n) = 1" and
11.32 + (r * s) ^^^ n = r ^^^ n * s ^^^ n" (*and*)
11.33 + realpow_minus_oneI: "-1 ^^^ (2 * n) = 1" (*and*)
11.34
11.35 - realpow_twoI: "r ^^^ 2 = r * r" and
11.36 - realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" and
11.37 - realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" and
11.38 - realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" and
11.39 - realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" and
11.40 - realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" and
11.41 - realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" and
11.42 - realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
11.43 - realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
11.44 + realpow_twoI: "r ^^^ 2 = r * r" (*and*)
11.45 + realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" (*and*)
11.46 + realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" (*and*)
11.47 + realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" (*and*)
11.48 + realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" (*and*)
11.49 + realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" (*and*)
11.50 + realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" (*and*)
11.51 + realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" (*and*)
11.52 + realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" (*and*)
11.53 realpow_def_atom: "[| Not (r is_atom); 1 < n |]
11.54 - ==> r ^^^ n = r * r ^^^ (n + -1)" and
11.55 - realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
11.56 + ==> r ^^^ n = r * r ^^^ (n + -1)" (*and*)
11.57 + realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" (*and*)
11.58
11.59
11.60 - realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" and
11.61 - realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
11.62 + realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" (*and*)
11.63 + realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" (*and*)
11.64
11.65
11.66 (* RL 020914 *)
11.67 - real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
11.68 - real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
11.69 - real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
11.70 - real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
11.71 - real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
11.72 + real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" (*and*)
11.73 + real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" (*and*)
11.74 + real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" (*and*)
11.75 + real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" (*and*)
11.76 + real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" (*and*)
11.77 real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
11.78 - (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
11.79 - real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
11.80 + (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" (*and*)
11.81 + real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" (*and*)
11.82 real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
11.83 - -1*b^^^3" and
11.84 + -1*b^^^3" (*and*)
11.85 (* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
11.86 (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
11.87 real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
11.88 - *(a + b)" and
11.89 + *(a + b)" (*and*)
11.90 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
11.91 (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
11.92 - *(a + b)" and
11.93 + *(a + b)" (*and*)
11.94 real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
11.95 - *(a^^^2 + 2*a*b + b^^^2)" and
11.96 + *(a^^^2 + 2*a*b + b^^^2)" (*and*)
11.97 real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
11.98 (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
11.99 - + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" and
11.100 - real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) and
11.101 - real_diff_minus: "a - b = a + -1 * b" and
11.102 - real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
11.103 - real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
11.104 + + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" (*and*)
11.105 + real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) (*and*)
11.106 + real_diff_minus: "a - b = a + -1 * b" (*and*)
11.107 + real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" (*and*)
11.108 + real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" (*and*)
11.109 (*WN071229 changed for Schaerding -----vvv*)
11.110 (*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
11.111 - real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" and
11.112 + real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" (*and*)
11.113 (*WN071229 changed for Schaerding -----^^^*)
11.114 real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
11.115 - (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
11.116 - real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
11.117 - real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
11.118 - real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
11.119 - real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
11.120 - real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
11.121 - real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
11.122 - real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
11.123 - real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
11.124 - real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
11.125 - real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" and
11.126 + (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" (*and*)
11.127 + real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" (*and*)
11.128 + real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" (*and*)
11.129 + real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" (*and*)
11.130 + real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" (*and*)
11.131 + real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" (*and*)
11.132 + real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" (*and*)
11.133 + real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" (*and*)
11.134 + real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" (*and*)
11.135 + real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" (*and*)
11.136 + real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" (*and*)
11.137
11.138 real_num_collect: "[| l is_const; m is_const |] ==>
11.139 - l * n + m * n = (l + m) * n" and
11.140 + l * n + m * n = (l + m) * n" (*and*)
11.141 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
11.142 by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
11.143 real_num_collect_assoc: "[| l is_const; m is_const |] ==>
11.144 - l * n + (m * n + k) = (l + m) * n + k" and
11.145 + l * n + (m * n + k) = (l + m) * n + k" (*and*)
11.146 real_num_collect_assoc_l: "[| l is_const; m is_const |] ==>
11.147 l * n + (m * n + k) = (l + m)
11.148 - * n + k" and
11.149 + * n + k" (*and*)
11.150 real_num_collect_assoc_r: "[| l is_const; m is_const |] ==>
11.151 - (k + m * n) + l * n = k + (l + m) * n" and
11.152 - real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" and
11.153 + (k + m * n) + l * n = k + (l + m) * n" (*and*)
11.154 + real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" (*and*)
11.155 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
11.156 by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
11.157 - real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
11.158 + real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" (*and*)
11.159
11.160 - real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
11.161 - real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" and
11.162 + real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" (*and*)
11.163 + real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" (*and*)
11.164
11.165 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
11.166 by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
11.167 - real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" and
11.168 - real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" and
11.169 - real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" and
11.170 + real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" (*and*)
11.171 + real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" (*and*)
11.172 + real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" (*and*)
11.173
11.174 - real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
11.175 + real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" (*and*)
11.176 real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
11.177
11.178 text {* remark on 'polynomials'
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Jul 26 16:50:27 2011 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Jul 27 09:30:15 2011 +0200
12.3 @@ -78,98 +78,98 @@
12.4 (_))" 9)
12.5
12.6 (*-------------------- rules -------------------------------------------------*)
12.7 -axiomatization where
12.8 +axioms(*axiomatization where*)
12.9 cancel_leading_coeff1: "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) =
12.10 - (a/c + b/c*bdv + bdv^^^2 = 0)" and
12.11 + (a/c + b/c*bdv + bdv^^^2 = 0)" (*and*)
12.12 cancel_leading_coeff2: "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) =
12.13 - (a/c - b/c*bdv + bdv^^^2 = 0)" and
12.14 + (a/c - b/c*bdv + bdv^^^2 = 0)" (*and*)
12.15 cancel_leading_coeff3: "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) =
12.16 - (a/c + b/c*bdv - bdv^^^2 = 0)" and
12.17 + (a/c + b/c*bdv - bdv^^^2 = 0)" (*and*)
12.18
12.19 cancel_leading_coeff4: "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) =
12.20 - (a/c + 1/c*bdv + bdv^^^2 = 0)" and
12.21 + (a/c + 1/c*bdv + bdv^^^2 = 0)" (*and*)
12.22 cancel_leading_coeff5: "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) =
12.23 - (a/c - 1/c*bdv + bdv^^^2 = 0)" and
12.24 + (a/c - 1/c*bdv + bdv^^^2 = 0)" (*and*)
12.25 cancel_leading_coeff6: "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) =
12.26 - (a/c + 1/c*bdv - bdv^^^2 = 0)" and
12.27 + (a/c + 1/c*bdv - bdv^^^2 = 0)" (*and*)
12.28
12.29 cancel_leading_coeff7: "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) =
12.30 - ( b/c*bdv + bdv^^^2 = 0)" and
12.31 + ( b/c*bdv + bdv^^^2 = 0)" (*and*)
12.32 cancel_leading_coeff8: "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) =
12.33 - ( b/c*bdv - bdv^^^2 = 0)" and
12.34 + ( b/c*bdv - bdv^^^2 = 0)" (*and*)
12.35
12.36 cancel_leading_coeff9: "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) =
12.37 - ( 1/c*bdv + bdv^^^2 = 0)" and
12.38 + ( 1/c*bdv + bdv^^^2 = 0)" (*and*)
12.39 cancel_leading_coeff10:"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) =
12.40 - ( 1/c*bdv - bdv^^^2 = 0)" and
12.41 + ( 1/c*bdv - bdv^^^2 = 0)" (*and*)
12.42
12.43 cancel_leading_coeff11:"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) =
12.44 - (a/b + bdv^^^2 = 0)" and
12.45 + (a/b + bdv^^^2 = 0)" (*and*)
12.46 cancel_leading_coeff12:"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) =
12.47 - (a/b - bdv^^^2 = 0)" and
12.48 + (a/b - bdv^^^2 = 0)" (*and*)
12.49 cancel_leading_coeff13:"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) =
12.50 - ( bdv^^^2 = 0/b)" and
12.51 + ( bdv^^^2 = 0/b)" (*and*)
12.52
12.53 complete_square1: "(q + p*bdv + bdv^^^2 = 0) =
12.54 - (q + (p/2 + bdv)^^^2 = (p/2)^^^2)" and
12.55 + (q + (p/2 + bdv)^^^2 = (p/2)^^^2)" (*and*)
12.56 complete_square2: "( p*bdv + bdv^^^2 = 0) =
12.57 - ( (p/2 + bdv)^^^2 = (p/2)^^^2)" and
12.58 + ( (p/2 + bdv)^^^2 = (p/2)^^^2)" (*and*)
12.59 complete_square3: "( bdv + bdv^^^2 = 0) =
12.60 - ( (1/2 + bdv)^^^2 = (1/2)^^^2)" and
12.61 + ( (1/2 + bdv)^^^2 = (1/2)^^^2)" (*and*)
12.62
12.63 complete_square4: "(q - p*bdv + bdv^^^2 = 0) =
12.64 - (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" and
12.65 + (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" (*and*)
12.66 complete_square5: "(q + p*bdv - bdv^^^2 = 0) =
12.67 - (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" and
12.68 + (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" (*and*)
12.69
12.70 - square_explicit1: "(a + b^^^2 = c) = ( b^^^2 = c - a)" and
12.71 - square_explicit2: "(a - b^^^2 = c) = (-(b^^^2) = c - a)" and
12.72 + square_explicit1: "(a + b^^^2 = c) = ( b^^^2 = c - a)" (*and*)
12.73 + square_explicit2: "(a - b^^^2 = c) = (-(b^^^2) = c - a)" (*and*)
12.74
12.75 - bdv_explicit1: "(a + bdv = b) = (bdv = - a + b)" and
12.76 - bdv_explicit2: "(a - bdv = b) = ((-1)*bdv = - a + b)" and
12.77 - bdv_explicit3: "((-1)*bdv = b) = (bdv = (-1)*b)" and
12.78 + bdv_explicit1: "(a + bdv = b) = (bdv = - a + b)" (*and*)
12.79 + bdv_explicit2: "(a - bdv = b) = ((-1)*bdv = - a + b)" (*and*)
12.80 + bdv_explicit3: "((-1)*bdv = b) = (bdv = (-1)*b)" (*and*)
12.81
12.82 - plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) and
12.83 - minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*) and
12.84 + plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) (*and*)
12.85 + minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*) (*and*)
12.86
12.87 (*-- normalize --*)
12.88 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
12.89 - all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
12.90 - makex1_x: "a^^^1 = a" and
12.91 - real_assoc_1: "a+(b+c) = a+b+c" and
12.92 - real_assoc_2: "a*(b*c) = a*b*c" and
12.93 + all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" (*and*)
12.94 + makex1_x: "a^^^1 = a" (*and*)
12.95 + real_assoc_1: "a+(b+c) = a+b+c" (*and*)
12.96 + real_assoc_2: "a*(b*c) = a*b*c" (*and*)
12.97
12.98 (* ---- degree 0 ----*)
12.99 - d0_true: "(0=0) = True" and
12.100 - d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" and
12.101 + d0_true: "(0=0) = True" (*and*)
12.102 + d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" (*and*)
12.103 (* ---- degree 1 ----*)
12.104 d1_isolate_add1:
12.105 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" and
12.106 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" (*and*)
12.107 d1_isolate_add2:
12.108 - "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" and
12.109 + "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" (*and*)
12.110 d1_isolate_div:
12.111 - "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" and
12.112 + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" (*and*)
12.113 (* ---- degree 2 ----*)
12.114 d2_isolate_add1:
12.115 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" and
12.116 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" (*and*)
12.117 d2_isolate_add2:
12.118 - "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" and
12.119 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" (*and*)
12.120 d2_isolate_div:
12.121 - "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)" and
12.122 + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)" (*and*)
12.123
12.124 - d2_prescind1: "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" and
12.125 - d2_prescind2: "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)" and
12.126 - d2_prescind3: "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" and
12.127 - d2_prescind4: "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)" and
12.128 + d2_prescind1: "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" (*and*)
12.129 + d2_prescind2: "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)" (*and*)
12.130 + d2_prescind3: "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" (*and*)
12.131 + d2_prescind4: "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)" (*and*)
12.132 (* eliminate degree 2 *)
12.133 (* thm for neg arguments in sqroot have postfix _neg *)
12.134 d2_sqrt_equation1: "[|(0<=c);Not(bdv occurs_in c)|] ==>
12.135 - (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" and
12.136 + (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" (*and*)
12.137 d2_sqrt_equation1_neg:
12.138 - "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" and
12.139 - d2_sqrt_equation2: "(bdv^^^2=0) = (bdv=0)" and
12.140 + "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" (*and*)
12.141 + d2_sqrt_equation2: "(bdv^^^2=0) = (bdv=0)" (*and*)
12.142 d2_sqrt_equation3: "(b*bdv^^^2=0) = (bdv=0)"
12.143 -axiomatization where (*..if replaced by "and" we get errors:
12.144 +axioms(*axiomatization where*) (*..if replaced by "and" we get errors:
12.145 exception PTREE "nth _ []" raised
12.146 (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):
12.147 'fun nth _ [] = raise PTREE "nth _ []"'
12.148 @@ -177,9 +177,9 @@
12.149 exception Bind raised
12.150 (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):
12.151 'val (Form f, tac, asms) = pt_extract (pt, p);' *)
12.152 - d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" and
12.153 + d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" (*and*)
12.154 d2_reduce_equation2: "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
12.155 -axiomatization where (*..if replaced by "and" we get errors:
12.156 +axioms(*axiomatization where*) (*..if replaced by "and" we get errors:
12.157 exception PTREE "nth _ []" raised
12.158 (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):
12.159 'fun nth _ [] = raise PTREE "nth _ []"'
12.160 @@ -189,193 +189,193 @@
12.161 'val (Form f, tac, asms) = pt_extract (pt, p);' *)
12.162 d2_pqformula1: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
12.163 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
12.164 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" and
12.165 - d2_pqformula1_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False" and
12.166 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" (*and*)
12.167 + d2_pqformula1_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False" (*and*)
12.168 d2_pqformula2: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
12.169 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
12.170 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" and
12.171 - d2_pqformula2_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False" and
12.172 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" (*and*)
12.173 + d2_pqformula2_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False" (*and*)
12.174 d2_pqformula3: "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
12.175 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
12.176 - | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
12.177 - d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False" and
12.178 + | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" (*and*)
12.179 + d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False" (*and*)
12.180 d2_pqformula4: "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
12.181 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
12.182 - | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
12.183 - d2_pqformula4_neg: "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False" and
12.184 + | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" (*and*)
12.185 + d2_pqformula4_neg: "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False" (*and*)
12.186 d2_pqformula5: "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
12.187 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
12.188 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" and
12.189 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" (*and*)
12.190 (* d2_pqformula5_neg not need p^2 never less zero in R *)
12.191 d2_pqformula6: "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
12.192 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
12.193 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" and
12.194 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" (*and*)
12.195 (* d2_pqformula6_neg not need p^2 never less zero in R *)
12.196 d2_pqformula7: "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
12.197 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
12.198 - | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" and
12.199 + | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" (*and*)
12.200 (* d2_pqformula7_neg not need, because 1<0 ==> False*)
12.201 d2_pqformula8: "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) =
12.202 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
12.203 - | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" and
12.204 + | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" (*and*)
12.205 (* d2_pqformula8_neg not need, because 1<0 ==> False*)
12.206 d2_pqformula9: "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==>
12.207 (q+ 1*bdv^^^2=0) = ((bdv= 0 + sqrt(0 - 4*q)/2)
12.208 - | (bdv= 0 - sqrt(0 - 4*q)/2))" and
12.209 + | (bdv= 0 - sqrt(0 - 4*q)/2))" (*and*)
12.210 d2_pqformula9_neg:
12.211 - "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" and
12.212 + "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" (*and*)
12.213 d2_pqformula10:
12.214 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) =
12.215 ((bdv= 0 + sqrt(0 - 4*q)/2)
12.216 - | (bdv= 0 - sqrt(0 - 4*q)/2))" and
12.217 + | (bdv= 0 - sqrt(0 - 4*q)/2))" (*and*)
12.218 d2_pqformula10_neg:
12.219 - "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" and
12.220 + "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" (*and*)
12.221 d2_abcformula1:
12.222 "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
12.223 ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a))
12.224 - | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))" and
12.225 + | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))" (*and*)
12.226 d2_abcformula1_neg:
12.227 - "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" and
12.228 + "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" (*and*)
12.229 d2_abcformula2:
12.230 "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) =
12.231 ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
12.232 - | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" and
12.233 + | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" (*and*)
12.234 d2_abcformula2_neg:
12.235 - "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" and
12.236 + "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" (*and*)
12.237 d2_abcformula3:
12.238 "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) =
12.239 ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1))
12.240 - | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))" and
12.241 + | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))" (*and*)
12.242 d2_abcformula3_neg:
12.243 - "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" and
12.244 + "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" (*and*)
12.245 d2_abcformula4:
12.246 "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) =
12.247 ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1))
12.248 - | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" and
12.249 + | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" (*and*)
12.250 d2_abcformula4_neg:
12.251 - "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" and
12.252 + "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" (*and*)
12.253 d2_abcformula5:
12.254 "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) =
12.255 ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
12.256 - | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" and
12.257 + | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" (*and*)
12.258 d2_abcformula5_neg:
12.259 - "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" and
12.260 + "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" (*and*)
12.261 d2_abcformula6:
12.262 "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) =
12.263 ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
12.264 - | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" and
12.265 + | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" (*and*)
12.266 d2_abcformula6_neg:
12.267 - "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" and
12.268 + "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" (*and*)
12.269 d2_abcformula7:
12.270 "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) =
12.271 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
12.272 - | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))" and
12.273 + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))" (*and*)
12.274 (* d2_abcformula7_neg not need b^2 never less zero in R *)
12.275 d2_abcformula8:
12.276 "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) =
12.277 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
12.278 - | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))" and
12.279 + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))" (*and*)
12.280 (* d2_abcformula8_neg not need b^2 never less zero in R *)
12.281 d2_abcformula9:
12.282 "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) =
12.283 ((bdv=( -1 + sqrt(1 - 0))/(2*a))
12.284 - | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" and
12.285 + | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" (*and*)
12.286 (* d2_abcformula9_neg not need, because 1<0 ==> False*)
12.287 d2_abcformula10:
12.288 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
12.289 ((bdv=( -1 + sqrt(1 - 0))/(2*1))
12.290 - | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" and
12.291 + | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" (*and*)
12.292 (* d2_abcformula10_neg not need, because 1<0 ==> False*)
12.293
12.294
12.295 (* ---- degree 3 ----*)
12.296 d3_reduce_equation1:
12.297 - "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" and
12.298 + "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" (*and*)
12.299 d3_reduce_equation2:
12.300 - "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" and
12.301 + "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" (*and*)
12.302 d3_reduce_equation3:
12.303 - "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" and
12.304 + "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" (*and*)
12.305 d3_reduce_equation4:
12.306 - "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" and
12.307 + "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" (*and*)
12.308 d3_reduce_equation5:
12.309 - "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" and
12.310 + "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" (*and*)
12.311 d3_reduce_equation6:
12.312 - "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" and
12.313 + "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" (*and*)
12.314 d3_reduce_equation7:
12.315 - "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" and
12.316 + "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" (*and*)
12.317 d3_reduce_equation8:
12.318 - "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" and
12.319 + "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" (*and*)
12.320 d3_reduce_equation9:
12.321 - "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" and
12.322 + "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" (*and*)
12.323 d3_reduce_equation10:
12.324 - "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" and
12.325 + "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" (*and*)
12.326 d3_reduce_equation11:
12.327 - "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" and
12.328 + "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" (*and*)
12.329 d3_reduce_equation12:
12.330 - "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" and
12.331 + "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" (*and*)
12.332 d3_reduce_equation13:
12.333 - "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" and
12.334 + "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" (*and*)
12.335 d3_reduce_equation14:
12.336 - "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" and
12.337 + "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" (*and*)
12.338 d3_reduce_equation15:
12.339 - "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" and
12.340 + "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" (*and*)
12.341 d3_reduce_equation16:
12.342 - "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" and
12.343 + "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" (*and*)
12.344 d3_isolate_add1:
12.345 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" and
12.346 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" (*and*)
12.347 d3_isolate_add2:
12.348 - "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" and
12.349 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" (*and*)
12.350 d3_isolate_div:
12.351 - "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" and
12.352 + "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" (*and*)
12.353 d3_root_equation2:
12.354 - "(bdv^^^3=0) = (bdv=0)" and
12.355 + "(bdv^^^3=0) = (bdv=0)" (*and*)
12.356 d3_root_equation1:
12.357 - "(bdv^^^3=c) = (bdv = nroot 3 c)" and
12.358 + "(bdv^^^3=c) = (bdv = nroot 3 c)" (*and*)
12.359
12.360 (* ---- degree 4 ----*)
12.361 (* RL03.FIXME es wir nicht getestet ob u>0 *)
12.362 d4_sub_u1:
12.363 "(c+b*bdv^^^2+a*bdv^^^4=0) =
12.364 - ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))" and
12.365 + ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))" (*and*)
12.366
12.367 (* ---- 7.3.02 von Termorder ---- *)
12.368
12.369 - bdv_collect_1: "l * bdv + m * bdv = (l + m) * bdv" and
12.370 - bdv_collect_2: "bdv + m * bdv = (1 + m) * bdv" and
12.371 - bdv_collect_3: "l * bdv + bdv = (l + 1) * bdv" and
12.372 + bdv_collect_1: "l * bdv + m * bdv = (l + m) * bdv" (*and*)
12.373 + bdv_collect_2: "bdv + m * bdv = (1 + m) * bdv" (*and*)
12.374 + bdv_collect_3: "l * bdv + bdv = (l + 1) * bdv" (*and*)
12.375
12.376 (* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
12.377 bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
12.378 bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
12.379 *)
12.380 - bdv_collect_assoc1_1: "l * bdv + (m * bdv + k) = (l + m) * bdv + k" and
12.381 - bdv_collect_assoc1_2: "bdv + (m * bdv + k) = (1 + m) * bdv + k" and
12.382 - bdv_collect_assoc1_3: "l * bdv + (bdv + k) = (l + 1) * bdv + k" and
12.383 + bdv_collect_assoc1_1: "l * bdv + (m * bdv + k) = (l + m) * bdv + k" (*and*)
12.384 + bdv_collect_assoc1_2: "bdv + (m * bdv + k) = (1 + m) * bdv + k" (*and*)
12.385 + bdv_collect_assoc1_3: "l * bdv + (bdv + k) = (l + 1) * bdv + k" (*and*)
12.386
12.387 - bdv_collect_assoc2_1: "k + l * bdv + m * bdv = k + (l + m) * bdv" and
12.388 - bdv_collect_assoc2_2: "k + bdv + m * bdv = k + (1 + m) * bdv" and
12.389 - bdv_collect_assoc2_3: "k + l * bdv + bdv = k + (l + 1) * bdv" and
12.390 + bdv_collect_assoc2_1: "k + l * bdv + m * bdv = k + (l + m) * bdv" (*and*)
12.391 + bdv_collect_assoc2_2: "k + bdv + m * bdv = k + (1 + m) * bdv" (*and*)
12.392 + bdv_collect_assoc2_3: "k + l * bdv + bdv = k + (l + 1) * bdv" (*and*)
12.393
12.394
12.395 - bdv_n_collect_1: "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n" and
12.396 - bdv_n_collect_2: " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n" and
12.397 - bdv_n_collect_3: "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*) and
12.398 + bdv_n_collect_1: "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n" (*and*)
12.399 + bdv_n_collect_2: " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n" (*and*)
12.400 + bdv_n_collect_3: "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*) (*and*)
12.401
12.402 bdv_n_collect_assoc1_1:
12.403 - "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k" and
12.404 - bdv_n_collect_assoc1_2: "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k" and
12.405 - bdv_n_collect_assoc1_3: "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k" and
12.406 + "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k" (*and*)
12.407 + bdv_n_collect_assoc1_2: "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k" (*and*)
12.408 + bdv_n_collect_assoc1_3: "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k" (*and*)
12.409
12.410 - bdv_n_collect_assoc2_1: "k + l * bdv^^^n + m * bdv^^^n = k +(l + m) * bdv^^^n" and
12.411 - bdv_n_collect_assoc2_2: "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n" and
12.412 - bdv_n_collect_assoc2_3: "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n" and
12.413 + bdv_n_collect_assoc2_1: "k + l * bdv^^^n + m * bdv^^^n = k +(l + m) * bdv^^^n" (*and*)
12.414 + bdv_n_collect_assoc2_2: "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n" (*and*)
12.415 + bdv_n_collect_assoc2_3: "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n" (*and*)
12.416
12.417 (*WN.14.3.03*)
12.418 - real_minus_div: "- (a / b) = (-1 * a) / b" and
12.419 + real_minus_div: "- (a / b) = (-1 * a) / b" (*and*)
12.420
12.421 - separate_bdv: "(a * bdv) / b = (a / b) * (bdv::real)" and
12.422 - separate_bdv_n: "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n" and
12.423 - separate_1_bdv: "bdv / b = (1 / b) * (bdv::real)" and
12.424 + separate_bdv: "(a * bdv) / b = (a / b) * (bdv::real)" (*and*)
12.425 + separate_bdv_n: "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n" (*and*)
12.426 + separate_1_bdv: "bdv / b = (1 / b) * (bdv::real)" (*and*)
12.427 separate_1_bdv_n: "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
12.428
12.429 ML {*
13.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jul 26 16:50:27 2011 +0200
13.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Jul 27 09:30:15 2011 +0200
13.3 @@ -25,84 +25,84 @@
13.4 => bool"
13.5 ("((Script ProbeScript (_ _ =))// (_))" 9)
13.6
13.7 -axiomatization where
13.8 +axioms(*axiomatization where*)
13.9
13.10 - null_minus: "0 - a = -a" and
13.11 - vor_minus_mal: "- a * b = (-a) * b" and
13.12 + null_minus: "0 - a = -a" (*and*)
13.13 + vor_minus_mal: "- a * b = (-a) * b" (*and*)
13.14
13.15 (*commute with invariant (a.b).c -association*)
13.16 tausche_plus: "[| b ist_monom; a kleiner b |] ==>
13.17 - (b + a) = (a + b)" and
13.18 + (b + a) = (a + b)" (*and*)
13.19 tausche_minus: "[| b ist_monom; a kleiner b |] ==>
13.20 - (b - a) = (-a + b)" and
13.21 + (b - a) = (-a + b)" (*and*)
13.22 tausche_vor_plus: "[| b ist_monom; a kleiner b |] ==>
13.23 - (- b + a) = (a - b)" and
13.24 + (- b + a) = (a - b)" (*and*)
13.25 tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==>
13.26 - (- b - a) = (-a - b)" and
13.27 - tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" and
13.28 - tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" and
13.29 - tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" and
13.30 - tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" and
13.31 + (- b - a) = (-a - b)" (*and*)
13.32 + tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" (*and*)
13.33 + tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" (*and*)
13.34 + tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" (*and*)
13.35 + tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" (*and*)
13.36
13.37 (*commute with invariant (a.b).c -association*)
13.38 tausche_mal: "[| b is_atom; a kleiner b |] ==>
13.39 - (b * a) = (a * b)" and
13.40 + (b * a) = (a * b)" (*and*)
13.41 tausche_vor_mal: "[| b is_atom; a kleiner b |] ==>
13.42 - (-b * a) = (-a * b)" and
13.43 + (-b * a) = (-a * b)" (*and*)
13.44 tausche_mal_mal: "[| c is_atom; b kleiner c |] ==>
13.45 - (x * c * b) = (x * b * c)" and
13.46 - x_quadrat: "(x * a) * a = x * a ^^^ 2" and
13.47 + (x * c * b) = (x * b * c)" (*and*)
13.48 + x_quadrat: "(x * a) * a = x * a ^^^ 2" (*and*)
13.49
13.50
13.51 subtrahiere: "[| l is_const; m is_const |] ==>
13.52 - m * v - l * v = (m - l) * v" and
13.53 + m * v - l * v = (m - l) * v" (*and*)
13.54 subtrahiere_von_1: "[| l is_const |] ==>
13.55 - v - l * v = (1 - l) * v" and
13.56 + v - l * v = (1 - l) * v" (*and*)
13.57 subtrahiere_1: "[| l is_const; m is_const |] ==>
13.58 - m * v - v = (m - 1) * v" and
13.59 + m * v - v = (m - 1) * v" (*and*)
13.60
13.61 subtrahiere_x_plus_minus: "[| l is_const; m is_const |] ==>
13.62 - (x + m * v) - l * v = x + (m - l) * v" and
13.63 + (x + m * v) - l * v = x + (m - l) * v" (*and*)
13.64 subtrahiere_x_plus1_minus: "[| l is_const |] ==>
13.65 - (x + v) - l * v = x + (1 - l) * v" and
13.66 + (x + v) - l * v = x + (1 - l) * v" (*and*)
13.67 subtrahiere_x_plus_minus1: "[| m is_const |] ==>
13.68 - (x + m * v) - v = x + (m - 1) * v" and
13.69 + (x + m * v) - v = x + (m - 1) * v" (*and*)
13.70
13.71 subtrahiere_x_minus_plus: "[| l is_const; m is_const |] ==>
13.72 - (x - m * v) + l * v = x + (-m + l) * v" and
13.73 + (x - m * v) + l * v = x + (-m + l) * v" (*and*)
13.74 subtrahiere_x_minus1_plus: "[| l is_const |] ==>
13.75 - (x - v) + l * v = x + (-1 + l) * v" and
13.76 + (x - v) + l * v = x + (-1 + l) * v" (*and*)
13.77 subtrahiere_x_minus_plus1: "[| m is_const |] ==>
13.78 - (x - m * v) + v = x + (-m + 1) * v" and
13.79 + (x - m * v) + v = x + (-m + 1) * v" (*and*)
13.80
13.81 subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>
13.82 - (x - m * v) - l * v = x + (-m - l) * v" and
13.83 + (x - m * v) - l * v = x + (-m - l) * v" (*and*)
13.84 subtrahiere_x_minus1_minus:"[| l is_const |] ==>
13.85 - (x - v) - l * v = x + (-1 - l) * v" and
13.86 + (x - v) - l * v = x + (-1 - l) * v" (*and*)
13.87 subtrahiere_x_minus_minus1:"[| m is_const |] ==>
13.88 - (x - m * v) - v = x + (-m - 1) * v" and
13.89 + (x - m * v) - v = x + (-m - 1) * v" (*and*)
13.90
13.91
13.92 addiere_vor_minus: "[| l is_const; m is_const |] ==>
13.93 - - (l * v) + m * v = (-l + m) * v" and
13.94 + - (l * v) + m * v = (-l + m) * v" (*and*)
13.95 addiere_eins_vor_minus: "[| m is_const |] ==>
13.96 - - v + m * v = (-1 + m) * v" and
13.97 + - v + m * v = (-1 + m) * v" (*and*)
13.98 subtrahiere_vor_minus: "[| l is_const; m is_const |] ==>
13.99 - - (l * v) - m * v = (-l - m) * v" and
13.100 + - (l * v) - m * v = (-l - m) * v" (*and*)
13.101 subtrahiere_eins_vor_minus:"[| m is_const |] ==>
13.102 - - v - m * v = (-1 - m) * v" and
13.103 + - v - m * v = (-1 - m) * v" (*and*)
13.104
13.105 - vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" and
13.106 - vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" and
13.107 - vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
13.108 - vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
13.109 + vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" (*and*)
13.110 + vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" (*and*)
13.111 + vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" (*and*)
13.112 + vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" (*and*)
13.113
13.114 (*klammer_plus_plus = (add_assoc RS sym)*)
13.115 - klammer_plus_minus: "a + (b - c) = (a + b) - c" and
13.116 - klammer_minus_plus: "a - (b + c) = (a - b) - c" and
13.117 - klammer_minus_minus: "a - (b - c) = (a - b) + c" and
13.118 + klammer_plus_minus: "a + (b - c) = (a + b) - c" (*and*)
13.119 + klammer_minus_plus: "a - (b + c) = (a - b) - c" (*and*)
13.120 + klammer_minus_minus: "a - (b - c) = (a - b) + c" (*and*)
13.121
13.122 - klammer_mult_minus: "a * (b - c) = a * b - a * c" and
13.123 + klammer_mult_minus: "a * (b - c) = a * b - a * c" (*and*)
13.124 klammer_minus_mult: "(b - c) * a = b * a - c * a"
13.125
13.126 ML {*
14.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Tue Jul 26 16:50:27 2011 +0200
14.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Jul 27 09:30:15 2011 +0200
14.3 @@ -20,25 +20,25 @@
14.4 ("((Script Solve'_rat'_equation (_ _ =))//
14.5 (_))" 9)
14.6
14.7 -axiomatization where
14.8 +axioms(*axiomatization where*)
14.9 (* FIXME also in Poly.thy def. --> FIXED*)
14.10 (*real_diff_minus
14.11 "a - b = a + (-1) * b"*)
14.12 - real_rat_mult_1: "a*(b/c) = (a*b)/c" and
14.13 - real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)" and
14.14 - real_rat_mult_3: "(a/b)*c = (a*c)/b" and
14.15 - real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2" and
14.16 + real_rat_mult_1: "a*(b/c) = (a*b)/c" (*and*)
14.17 + real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)" (*and*)
14.18 + real_rat_mult_3: "(a/b)*c = (a*c)/b" (*and*)
14.19 + real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2" (*and*)
14.20
14.21 - rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" and
14.22 + rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" (*and*)
14.23 rat_double_rat_2: "[|Not(b=0);Not(c=0); Not(d=0)|] ==>
14.24 - ((a/b) / (c/d) = (a*d) / (b*c))" and
14.25 - rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" and
14.26 + ((a/b) / (c/d) = (a*d) / (b*c))" (*and*)
14.27 + rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" (*and*)
14.28
14.29 (* equation to same denominator *)
14.30 rat_mult_denominator_both:
14.31 - "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" and
14.32 + "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" (*and*)
14.33 rat_mult_denominator_left:
14.34 - "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" and
14.35 + "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" (*and*)
14.36 rat_mult_denominator_right:
14.37 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
14.38
15.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Jul 26 16:50:27 2011 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Jul 27 09:30:15 2011 +0200
15.3 @@ -16,51 +16,51 @@
15.4 is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
15.5 is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
15.6
15.7 -axiomatization where (*.not contained in Isabelle2002,
15.8 +axioms(*axiomatization where*) (*.not contained in Isabelle2002,
15.9 stated as axioms, TODO?: prove as theorems*)
15.10
15.11 - mult_cross: "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)" and
15.12 - mult_cross1: " b ~= 0 ==> (a / b = c ) = (a = b * c)" and
15.13 - mult_cross2: " d ~= 0 ==> (a = c / d) = (a * d = c)" and
15.14 + mult_cross: "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)" (*and*)
15.15 + mult_cross1: " b ~= 0 ==> (a / b = c ) = (a = b * c)" (*and*)
15.16 + mult_cross2: " d ~= 0 ==> (a = c / d) = (a * d = c)" (*and*)
15.17
15.18 - add_minus: "a + b - b = a"(*RL->Poly.thy*) and
15.19 - add_minus1: "a - b + b = a"(*RL->Poly.thy*) and
15.20 + add_minus: "a + b - b = a"(*RL->Poly.thy*) (*and*)
15.21 + add_minus1: "a - b + b = a"(*RL->Poly.thy*) (*and*)
15.22
15.23 - rat_mult: "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) and
15.24 - rat_mult2: "a / b * c = a * c / b "(*?Isa02*) and
15.25 -
15.26 - rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a / b" and
15.27 - rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c / b" and
15.28 + rat_mult: "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) (*and*)
15.29 + rat_mult2: "a / b * c = a * c / b "(*?Isa02*) (*and*)
15.30 +
15.31 + rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a / b" (*and*)
15.32 + rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c / b" (*and*)
15.33
15.34 (*real_times_divide1_eq .. Isa02*)
15.35 - real_times_divide_1_eq: "-1 * (c / d) =-1 * c / d " and
15.36 + real_times_divide_1_eq: "-1 * (c / d) =-1 * c / d " (*and*)
15.37 real_times_divide_num: "a is_const ==>
15.38 - a * (c / d) = a * c / d " and
15.39 -
15.40 - real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n" and
15.41 + a * (c / d) = a * c / d " (*and*)
15.42 +
15.43 + real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n" (*and*)
15.44 (*real_mult_div_cancel1: "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
15.45
15.46 - real_divide_divide1: "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" and
15.47 - real_divide_divide1_mg: "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and
15.48 + real_divide_divide1: "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" (*and*)
15.49 + real_divide_divide1_mg: "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" (*and*)
15.50 (*real_divide_divide2_eq: "x / y / z = x / (y * z)"..Isa02*)
15.51
15.52 - rat_power: "(a / b)^^^n = (a^^^n) / (b^^^n)" and
15.53 + rat_power: "(a / b)^^^n = (a^^^n) / (b^^^n)" (*and*)
15.54
15.55
15.56 rat_add: "[| a is_const; b is_const; c is_const; d is_const |] ==>
15.57 - a / c + b / d = (a * d + b * c) / (c * d)" and
15.58 + a / c + b / d = (a * d + b * c) / (c * d)" (*and*)
15.59 rat_add_assoc: "[| a is_const; b is_const; c is_const; d is_const |] ==>
15.60 - a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
15.61 + a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" (*and*)
15.62 rat_add1: "[| a is_const; b is_const; c is_const |] ==>
15.63 - a / c + b / c = (a + b) / c" and
15.64 + a / c + b / c = (a + b) / c" (*and*)
15.65 rat_add1_assoc: "[| a is_const; b is_const; c is_const |] ==>
15.66 - a / c + (b / c + e) = (a + b) / c + e" and
15.67 + a / c + (b / c + e) = (a + b) / c + e" (*and*)
15.68 rat_add2: "[| a is_const; b is_const; c is_const |] ==>
15.69 - a / c + b = (a + b * c) / c" and
15.70 + a / c + b = (a + b * c) / c" (*and*)
15.71 rat_add2_assoc: "[| a is_const; b is_const; c is_const |] ==>
15.72 - a / c + (b + e) = (a + b * c) / c + e" and
15.73 + a / c + (b + e) = (a + b * c) / c + e" (*and*)
15.74 rat_add3: "[| a is_const; b is_const; c is_const |] ==>
15.75 - a + b / c = (a * c + b) / c" and
15.76 + a + b / c = (a * c + b) / c" (*and*)
15.77 rat_add3_assoc: "[| a is_const; b is_const; c is_const |] ==>
15.78 a + (b / c + e) = (a * c + b) / c + e"
15.79
16.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Jul 26 16:50:27 2011 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Jul 27 09:30:15 2011 +0200
16.3 @@ -13,32 +13,32 @@
16.4 (*sqrt :: "real => real" Isabelle "NthRoot.sqrt"*)
16.5 nroot :: "[real, real] => real"
16.6
16.7 -axiomatization where (*.not contained in Isabelle2002,
16.8 +axioms(*axiomatization where*) (*.not contained in Isabelle2002,
16.9 stated as axioms, TODO: prove as theorems;
16.10 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
16.11
16.12 root_plus_minus: "0 <= b ==>
16.13 - (a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" and
16.14 - root_false: "b < 0 ==> (a^^^2 = b) = False" and
16.15 + (a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" (*and*)
16.16 + root_false: "b < 0 ==> (a^^^2 = b) = False" (*and*)
16.17
16.18 (* for expand_rootbinom *)
16.19 - real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
16.20 - real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
16.21 - real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
16.22 - real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
16.23 - real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
16.24 - real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
16.25 - realpow_mul: "(a*b)^^^n = a^^^n * b^^^n" and
16.26 + real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" (*and*)
16.27 + real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" (*and*)
16.28 + real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" (*and*)
16.29 + real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" (*and*)
16.30 + real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" (*and*)
16.31 + real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" (*and*)
16.32 + realpow_mul: "(a*b)^^^n = a^^^n * b^^^n" (*and*)
16.33
16.34 - real_diff_minus: "a - b = a + (-1) * b" and
16.35 - real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
16.36 - real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
16.37 - real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
16.38 - real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
16.39 - real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
16.40 - real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
16.41 + real_diff_minus: "a - b = a + (-1) * b" (*and*)
16.42 + real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" (*and*)
16.43 + real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" (*and*)
16.44 + real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" (*and*)
16.45 + real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" (*and*)
16.46 + real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" (*and*)
16.47 + real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" (*and*)
16.48
16.49 - real_root_positive: "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)" and
16.50 + real_root_positive: "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)" (*and*)
16.51 real_root_negative: "a < 0 ==> (x ^^^ 2 = a) = False"
16.52
16.53 ML {*
17.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Jul 26 16:50:27 2011 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Jul 27 09:30:15 2011 +0200
17.3 @@ -37,83 +37,83 @@
17.4 ("((Script Solve'_right'_sq'_root'_equation (_ _ =))//
17.5 (_))" 9)
17.6
17.7 -axiomatization where
17.8 +axioms(*axiomatization where*)
17.9
17.10 (* normalize *)
17.11 - makex1_x: "a^^^1 = a" and
17.12 - real_assoc_1: "a+(b+c) = a+b+c" and
17.13 - real_assoc_2: "a*(b*c) = a*b*c" and
17.14 + makex1_x: "a^^^1 = a" (*and*)
17.15 + real_assoc_1: "a+(b+c) = a+b+c" (*and*)
17.16 + real_assoc_2: "a*(b*c) = a*b*c" (*and*)
17.17
17.18 (* simplification of root*)
17.19 - sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a" and
17.20 - sqrt_square_2: "sqrt (a ^^^ 2) = a" and
17.21 - sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)" and
17.22 - sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)" and
17.23 + sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a" (*and*)
17.24 + sqrt_square_2: "sqrt (a ^^^ 2) = a" (*and*)
17.25 + sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)" (*and*)
17.26 + sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)" (*and*)
17.27
17.28 (* isolate one root on the LEFT or RIGHT hand side of the equation *)
17.29 sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==>
17.30 - (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" and
17.31 + (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" (*and*)
17.32 sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==>
17.33 - (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" and
17.34 + (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" (*and*)
17.35 sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==>
17.36 - (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" and
17.37 + (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" (*and*)
17.38 sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==>
17.39 - (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" and
17.40 + (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" (*and*)
17.41 sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==>
17.42 - (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" and
17.43 + (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" (*and*)
17.44 sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==>
17.45 - (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" and
17.46 + (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" (*and*)
17.47 sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==>
17.48 - (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" and
17.49 + (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" (*and*)
17.50 sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>
17.51 - (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" and
17.52 + (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" (*and*)
17.53 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
17.54 sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>
17.55 - (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" and
17.56 + (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" (*and*)
17.57 sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>
17.58 - (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" and
17.59 + (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" (*and*)
17.60 sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==>
17.61 - (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" and
17.62 + (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" (*and*)
17.63 sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==>
17.64 - (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" and
17.65 + (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" (*and*)
17.66
17.67 (* eliminate isolates sqrt *)
17.68 sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==>
17.69 ( (sqrt a + sqrt b = sqrt c + sqrt d) =
17.70 - (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" and
17.71 + (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" (*and*)
17.72 sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==>
17.73 ( (sqrt a - sqrt b = sqrt c + sqrt d) =
17.74 - (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" and
17.75 + (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" (*and*)
17.76 sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==>
17.77 ( (sqrt a + sqrt b = sqrt c - sqrt d) =
17.78 - (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" and
17.79 + (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" (*and*)
17.80 sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==>
17.81 ( (sqrt a - sqrt b = sqrt c - sqrt d) =
17.82 - (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" and
17.83 + (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" (*and*)
17.84 sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
17.85 - ( (sqrt (a) = b) = (a = (b^^^2)))" and
17.86 + ( (sqrt (a) = b) = (a = (b^^^2)))" (*and*)
17.87 sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
17.88 - ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" and
17.89 + ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" (*and*)
17.90 sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
17.91 - ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" and
17.92 + ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" (*and*)
17.93 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
17.94 sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
17.95 - ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" and
17.96 + ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" (*and*)
17.97 sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
17.98 - ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" and
17.99 + ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" (*and*)
17.100 sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
17.101 - ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" and
17.102 + ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" (*and*)
17.103 sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
17.104 - ( (a = sqrt (b)) = (a^^^2 = b))" and
17.105 + ( (a = sqrt (b)) = (a^^^2 = b))" (*and*)
17.106 sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
17.107 - ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" and
17.108 + ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" (*and*)
17.109 sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
17.110 - ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" and
17.111 + ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" (*and*)
17.112 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
17.113 sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
17.114 - ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" and
17.115 + ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" (*and*)
17.116 sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
17.117 - ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" and
17.118 + ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" (*and*)
17.119 sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
17.120 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
17.121
18.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jul 26 16:50:27 2011 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Jul 27 09:30:15 2011 +0200
18.3 @@ -22,14 +22,14 @@
18.4 (_))" 9)
18.5 (*-------------------- rules------------------------------------------------*)
18.6
18.7 -axiomatization where
18.8 +axioms(*axiomatization where*)
18.9 (* eliminate ratRootTerm *)
18.10 rootrat_equation_left_1:
18.11 - "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" and
18.12 + "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" (*and*)
18.13 rootrat_equation_left_2:
18.14 - "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" and
18.15 + "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" (*and*)
18.16 rootrat_equation_right_2:
18.17 - "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" and
18.18 + "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" (*and*)
18.19 rootrat_equation_right_1:
18.20 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
18.21
19.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Jul 26 16:50:27 2011 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Jul 27 09:30:15 2011 +0200
19.3 @@ -63,109 +63,109 @@
19.4
19.5 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
19.6
19.7 -axiomatization where (*TODO: prove as theorems*)
19.8 +axioms(*axiomatization where*) (*TODO: prove as theorems*)
19.9
19.10 - radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" and
19.11 - rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" and
19.12 - rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" and
19.13 - rdistr_div_right: "((k::real) + l) / n = k / n + l / n" and
19.14 + radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" (*and*)
19.15 + rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" (*and*)
19.16 + rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" (*and*)
19.17 + rdistr_div_right: "((k::real) + l) / n = k / n + l / n" (*and*)
19.18 rcollect_right:
19.19 - "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
19.20 + "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" (*and*)
19.21 rcollect_one_left:
19.22 - "m is_const ==> (n::real) + m * n = (1 + m) * n" and
19.23 + "m is_const ==> (n::real) + m * n = (1 + m) * n" (*and*)
19.24 rcollect_one_left_assoc:
19.25 - "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
19.26 + "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" (*and*)
19.27 rcollect_one_left_assoc_p:
19.28 - "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
19.29 + "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" (*and*)
19.30
19.31 - rtwo_of_the_same: "a + a = 2 * a" and
19.32 - rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" and
19.33 - rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
19.34 + rtwo_of_the_same: "a + a = 2 * a" (*and*)
19.35 + rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" (*and*)
19.36 + rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" (*and*)
19.37
19.38 - rcancel_den: "not(a=0) ==> a * (b / a) = b" and
19.39 - rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
19.40 - rshift_nominator: "(a::real) * b / c = a / c * b" and
19.41 + rcancel_den: "not(a=0) ==> a * (b / a) = b" (*and*)
19.42 + rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" (*and*)
19.43 + rshift_nominator: "(a::real) * b / c = a / c * b" (*and*)
19.44
19.45 - exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
19.46 - rsqare: "(a::real) * a = a ^^^ 2" and
19.47 - power_1: "(a::real) ^^^ 1 = a" and
19.48 - rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" and
19.49 + exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" (*and*)
19.50 + rsqare: "(a::real) * a = a ^^^ 2" (*and*)
19.51 + power_1: "(a::real) ^^^ 1 = a" (*and*)
19.52 + rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" (*and*)
19.53
19.54 - rmult_1: "1 * k = (k::real)" and
19.55 - rmult_1_right: "k * 1 = (k::real)" and
19.56 - rmult_0: "0 * k = (0::real)" and
19.57 - rmult_0_right: "k * 0 = (0::real)" and
19.58 - radd_0: "0 + k = (k::real)" and
19.59 - radd_0_right: "k + 0 = (k::real)" and
19.60 + rmult_1: "1 * k = (k::real)" (*and*)
19.61 + rmult_1_right: "k * 1 = (k::real)" (*and*)
19.62 + rmult_0: "0 * k = (0::real)" (*and*)
19.63 + rmult_0_right: "k * 0 = (0::real)" (*and*)
19.64 + radd_0: "0 + k = (k::real)" (*and*)
19.65 + radd_0_right: "k + 0 = (k::real)" (*and*)
19.66
19.67 radd_real_const_eq:
19.68 - "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
19.69 + "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" (*and*)
19.70 radd_real_const:
19.71 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
19.72 - and
19.73 + (*and*)
19.74 (*for AC-operators*)
19.75 - radd_commute: "(m::real) + (n::real) = n + m" and
19.76 - radd_left_commute: "(x::real) + (y + z) = y + (x + z)" and
19.77 - radd_assoc: "(m::real) + n + k = m + (n + k)" and
19.78 - rmult_commute: "(m::real) * n = n * m" and
19.79 - rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" and
19.80 - rmult_assoc: "(m::real) * n * k = m * (n * k)" and
19.81 + radd_commute: "(m::real) + (n::real) = n + m" (*and*)
19.82 + radd_left_commute: "(x::real) + (y + z) = y + (x + z)" (*and*)
19.83 + radd_assoc: "(m::real) + n + k = m + (n + k)" (*and*)
19.84 + rmult_commute: "(m::real) * n = n * m" (*and*)
19.85 + rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" (*and*)
19.86 + rmult_assoc: "(m::real) * n * k = m * (n * k)" (*and*)
19.87
19.88 (*for equations: 'bdv' is a meta-constant*)
19.89 - risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and
19.90 - risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and
19.91 - risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" and
19.92 + risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" (*and*)
19.93 + risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" (*and*)
19.94 + risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" (*and*)
19.95
19.96 rnorm_equation_add:
19.97 - "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and
19.98 + "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" (*and*)
19.99
19.100 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
19.101 - root_ge0: "0 <= a ==> 0 <= sqrt a" and
19.102 + root_ge0: "0 <= a ==> 0 <= sqrt a" (*and*)
19.103 (*should be dropped with better simplification in eval_rls ...*)
19.104 root_add_ge0:
19.105 - "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and
19.106 + "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" (*and*)
19.107 root_ge0_1:
19.108 - "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and
19.109 + "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" (*and*)
19.110 root_ge0_2:
19.111 - "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and
19.112 + "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" (*and*)
19.113
19.114
19.115 - rroot_square_inv: "(sqrt a)^^^ 2 = a" and
19.116 - rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" and
19.117 - rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and
19.118 - rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and
19.119 + rroot_square_inv: "(sqrt a)^^^ 2 = a" (*and*)
19.120 + rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" (*and*)
19.121 + rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" (*and*)
19.122 + rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" (*and*)
19.123
19.124
19.125 (*for root-equations*)
19.126 square_equation_left:
19.127 - "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" and
19.128 + "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" (*and*)
19.129 square_equation_right:
19.130 - "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" and
19.131 + "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" (*and*)
19.132 (*causes frequently non-termination:*)
19.133 square_equation:
19.134 - "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" and
19.135 + "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" (*and*)
19.136
19.137 - risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" and
19.138 - risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and
19.139 - risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" and
19.140 + risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" (*and*)
19.141 + risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" (*and*)
19.142 + risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" (*and*)
19.143
19.144 (*for polynomial equations of degree 2; linear case in RatArith*)
19.145 - mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" and
19.146 - constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" and
19.147 - constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" and
19.148 + mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" (*and*)
19.149 + constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" (*and*)
19.150 + constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" (*and*)
19.151
19.152 square_equality:
19.153 - "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
19.154 + "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" (*and*)
19.155 square_equality_0:
19.156 - "(x^^^2 = 0) = (x = 0)" and
19.157 + "(x^^^2 = 0) = (x = 0)" (*and*)
19.158
19.159 (*isolate root on the LEFT hand side of the equation
19.160 otherwise shuffling from left to right would not terminate*)
19.161
19.162 rroot_to_lhs:
19.163 - "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
19.164 + "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" (*and*)
19.165 rroot_to_lhs_mult:
19.166 - "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
19.167 + "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" (*and*)
19.168 rroot_to_lhs_add_mult:
19.169 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
19.170 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
20.1 --- a/src/Tools/isac/ProgLang/ListC.thy Tue Jul 26 16:50:27 2011 +0200
20.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Wed Jul 27 09:30:15 2011 +0200
20.3 @@ -34,35 +34,35 @@
20.4
20.5 consts NTH :: "[real, 'a list] => 'a"
20.6
20.7 -axiomatization where
20.8 +axioms(*axiomatization where*)
20.9 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
20.10 - NTH_NIL: "NTH 1 (x#xs) = x" and
20.11 + NTH_NIL: "NTH 1 (x#xs) = x" (*and*)
20.12 (* NTH_CONS: "NTH n (x#xs) = NTH (n+ -1) xs" *)
20.13
20.14 (*rewriter does not reach base case ...... ;
20.15 the condition involves another rule set (erls, eval_binop in Atools):*)
20.16 - NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" and
20.17 + NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" (*and*)
20.18
20.19 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
20.20 (*primrec*)
20.21 - hd_thm: "hd(x#xs) = x" and
20.22 + hd_thm: "hd(x#xs) = x" (*and*)
20.23 (*primrec*)
20.24 - tl_Nil: "tl([]) = []" and
20.25 - tl_Cons: "tl(x#xs) = xs" and
20.26 + tl_Nil: "tl([]) = []" (*and*)
20.27 + tl_Cons: "tl(x#xs) = xs" (*and*)
20.28 (*primrec*)
20.29 - null_Nil: "null([]) = True" and
20.30 - null_Cons: "null(x#xs) = False" and
20.31 + null_Nil: "null([]) = True" (*and*)
20.32 + null_Cons: "null(x#xs) = False" (*and*)
20.33 (*primrec*)
20.34 - LAST: "last(x#xs) = (if xs=[] then x else last xs)" and
20.35 + LAST: "last(x#xs) = (if xs=[] then x else last xs)" (*and*)
20.36 (*primrec*)
20.37 - butlast_Nil: "butlast [] = []" and
20.38 - butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" and
20.39 + butlast_Nil: "butlast [] = []" (*and*)
20.40 + butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" (*and*)
20.41 (*primrec
20.42 mem_Nil: "x mem [] = False"
20.43 mem_Cons: "x mem (y#ys) = (if y=x then True else x mem ys)"
20.44 *)
20.45 - mem_Nil: "x : set [] = False" and
20.46 - mem_Cons: "x : set (y#ys) = (if y=x then True else x : set ys)" and
20.47 + mem_Nil: "x : set [] = False" (*and*)
20.48 + mem_Cons: "x : set (y#ys) = (if y=x then True else x : set ys)" (*and*)
20.49 (*primrec-------already named---
20.50 "set [] = {}"
20.51 "set (x#xs) = insert x (set xs)"
20.52 @@ -71,27 +71,27 @@
20.53 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
20.54 ----------------*)
20.55 (*primrec*)
20.56 - map_Nil: "map f [] = []" and
20.57 - map_Cons: "map f (x#xs) = f(x)#map f xs" and
20.58 + map_Nil: "map f [] = []" (*and*)
20.59 + map_Cons: "map f (x#xs) = f(x)#map f xs" (*and*)
20.60 (*primrec*)
20.61 - append_Nil: "[] @ys = ys" and
20.62 - append_Cons: "(x#xs)@ys = x#(xs@ys)" and
20.63 + append_Nil: "[] @ys = ys" (*and*)
20.64 + append_Cons: "(x#xs)@ys = x#(xs@ys)" (*and*)
20.65 (*primrec*)
20.66 - rev_Nil: "rev([]) = []" and
20.67 - rev_Cons: "rev(x#xs) = rev(xs) @ [x]" and
20.68 + rev_Nil: "rev([]) = []" (*and*)
20.69 + rev_Cons: "rev(x#xs) = rev(xs) @ [x]" (*and*)
20.70 (*primrec*)
20.71 - filter_Nil: "filter P [] = []" and
20.72 - filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" and
20.73 + filter_Nil: "filter P [] = []" (*and*)
20.74 + filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" (*and*)
20.75 (*primrec-------already named---
20.76 foldl_Nil "foldl f a [] = a"
20.77 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
20.78 ----------------*)
20.79 (*primrec*)
20.80 - foldr_Nil: "foldr f [] a = a" and
20.81 - foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)" and
20.82 + foldr_Nil: "foldr f [] a = a" (*and*)
20.83 + foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)" (*and*)
20.84 (*primrec*)
20.85 - concat_Nil: "concat([]) = []" and
20.86 - concat_Cons: "concat(x#xs) = x @ concat(xs)" and
20.87 + concat_Nil: "concat([]) = []" (*and*)
20.88 + concat_Cons: "concat(x#xs) = x @ concat(xs)" (*and*)
20.89 (*primrec-------already named---
20.90 drop_Nil "drop n [] = []"
20.91 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
20.92 @@ -112,16 +112,16 @@
20.93 | Suc j => x # xs[j:=v])"
20.94 ----------------*)
20.95 (*primrec*)
20.96 - takeWhile_Nil: "takeWhile P [] = []" and
20.97 + takeWhile_Nil: "takeWhile P [] = []" (*and*)
20.98 takeWhile_Cons:
20.99 - "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" and
20.100 + "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" (*and*)
20.101 (*primrec*)
20.102 - dropWhile_Nil: "dropWhile P [] = []" and
20.103 + dropWhile_Nil: "dropWhile P [] = []" (*and*)
20.104 dropWhile_Cons:
20.105 - "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" and
20.106 + "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" (*and*)
20.107 (*primrec*)
20.108 - zip_Nil: "zip xs [] = []" and
20.109 - zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" and
20.110 + zip_Nil: "zip xs [] = []" (*and*)
20.111 + zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" (*and*)
20.112 (* Warning: simpset does not contain this definition but separate theorems
20.113 for xs=[] / xs=z#zs *)
20.114 (*primrec
20.115 @@ -129,10 +129,10 @@
20.116 upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
20.117 *)
20.118 (*primrec*)
20.119 - distinct_Nil: "distinct [] = True" and
20.120 - distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)" and
20.121 + distinct_Nil: "distinct [] = True" (*and*)
20.122 + distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)" (*and*)
20.123 (*primrec*)
20.124 - remdups_Nil: "remdups [] = []" and
20.125 + remdups_Nil: "remdups [] = []" (*and*)
20.126 remdups_Cons: "remdups (x#xs) =
20.127 (if x : set xs then remdups xs else x # remdups xs)"
20.128 (*primrec-------already named---