1.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue Jul 26 11:36:43 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Jul 26 13:28:39 2011 +0200
1.3 @@ -43,28 +43,30 @@
1.4 ("filter'_sameFunId _ _" 10)
1.5 boollist2sum :: "bool list => real"
1.6
1.7 -axioms (*for evaluating the assumptions of conditional rules*)
1.8 +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)"
1.11 - real_unari_minus: "- a = (-1) * a"
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"
1.16 - radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)"
1.17 - not_true: "(~ True) = False"
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 - and_true: "(a & True) = a"
1.23 - and_false: "(a & False) = False"
1.24 - or_true: "(a | True) = True"
1.25 - or_false: "(a | False) = a"
1.26 - and_commute: "(a & b) = (b & a)"
1.27 +axiomatization where
1.28 + and_true: "(a & True) = a" and
1.29 + and_false: "(a & False) = False" and
1.30 + or_true: "(a | True) = True" and
1.31 + or_false: "(a | False) = a" and
1.32 + and_commute: "(a & b) = (b & a)" and
1.33 or_commute: "(a | b) = (b | a)"
1.34
1.35 (*.should be in Rational.thy, but:
1.36 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
1.37 +axiomatization where
1.38 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
1.39 - ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
1.40 + ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
1.41 rat_leq2: "d ~= 0 ==>
1.42 - ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*)
1.43 + ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
1.44 rat_leq3: "b ~= 0 ==>
1.45 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
1.46
2.1 --- a/src/Tools/isac/Knowledge/Delete.thy Tue Jul 26 11:36:43 2011 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Tue Jul 26 13:28:39 2011 +0200
2.3 @@ -5,13 +5,13 @@
2.4
2.5 theory Delete imports "../ProgLang/ProgLang" begin
2.6
2.7 -axioms (* theorems which are available only with long names,
2.8 +axiomatization where (* theorems which are available only with long names,
2.9 which can not yet be handled in isac's scripts *)
2.10
2.11 - real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)"
2.12 + real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" and
2.13 (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)
2.14 - real_mult_minus1: "-1 * z = - (z::real)"
2.15 - real_mult_2: "2 * z = z + (z::real)"
2.16 + real_mult_minus1: "-1 * z = - (z::real)" and
2.17 + real_mult_2: "2 * z = z + (z::real)" and
2.18 real_diff_0: "0 - x = - (x::real)"
2.19
2.20
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Jul 26 11:36:43 2011 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Jul 26 13:28:39 2011 +0200
3.3 @@ -50,29 +50,29 @@
3.4 disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
3.5 *}
3.6
3.7 -axioms (*stated as axioms, todo: prove as theorems
3.8 +axiomatization where (*stated as axioms, todo: prove as theorems
3.9 'bdv' is a constant on the meta-level *)
3.10 - diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
3.11 - diff_var: "d_d bdv bdv = 1"
3.12 + diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" and
3.13 + diff_var: "d_d bdv bdv = 1" and
3.14 diff_prod_const:"[| Not (bdv occurs_in u) |] ==>
3.15 - d_d bdv (u * v) = u * d_d bdv v"
3.16 + d_d bdv (u * v) = u * d_d bdv v" and
3.17
3.18 - diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
3.19 - diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v"
3.20 - diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
3.21 + diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v" and
3.22 + diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v" and
3.23 + diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" and
3.24 diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) =
3.25 - (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
3.26 + (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" and
3.27
3.28 - diff_sin: "d_d bdv (sin bdv) = cos bdv"
3.29 - diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u"
3.30 - diff_cos: "d_d bdv (cos bdv) = - sin bdv"
3.31 - diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u"
3.32 - diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
3.33 - diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u"
3.34 - diff_ln: "d_d bdv (ln bdv) = 1 / bdv"
3.35 - diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u"
3.36 - diff_exp: "d_d bdv (exp bdv) = exp bdv"
3.37 - diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u"
3.38 + diff_sin: "d_d bdv (sin bdv) = cos bdv" and
3.39 + diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u" and
3.40 + diff_cos: "d_d bdv (cos bdv) = - sin bdv" and
3.41 + diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u" and
3.42 + diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" and
3.43 + diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" and
3.44 + diff_ln: "d_d bdv (ln bdv) = 1 / bdv" and
3.45 + diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u" and
3.46 + diff_exp: "d_d bdv (exp bdv) = exp bdv" and
3.47 + diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u" and
3.48 (*
3.49 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
3.50 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
3.51 @@ -80,16 +80,16 @@
3.52 (*...*)
3.53
3.54 frac_conv: "[| bdv occurs_in b; 0 < n |] ==>
3.55 - a / (b ^^^ n) = a * b ^^^ (-n)"
3.56 - frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
3.57 + a / (b ^^^ n) = a * b ^^^ (-n)" and
3.58 + frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" and
3.59
3.60 - sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)"
3.61 - sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
3.62 - sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
3.63 - sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)"
3.64 + sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)" and
3.65 + sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" and
3.66 + sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" and
3.67 + sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)" and
3.68
3.69 - root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
3.70 - root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)"
3.71 + root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" and
3.72 + root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)" and
3.73
3.74 realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
3.75
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Tue Jul 26 11:36:43 2011 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Jul 26 13:28:39 2011 +0200
4.3 @@ -28,8 +28,8 @@
4.4 (*for script Maximum_value*)
4.5 filterVar :: "[real, 'a list] => 'a list"
4.6
4.7 -(*primrec*)axioms
4.8 - filterVar_Nil: "filterVar v [] = []"
4.9 +(*primrec*)axiomatization where
4.10 + filterVar_Nil: "filterVar v [] = []" and
4.11 filterVar_Const: "filterVar v (x#xs) =
4.12 (if (v : set (Vars x)) then x#(filterVar v xs)
4.13 else filterVar v xs) "
5.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Tue Jul 26 11:36:43 2011 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Tue Jul 26 13:28:39 2011 +0200
5.3 @@ -12,7 +12,7 @@
5.4 Diophant'_equation :: "[bool, int, bool ]
5.5 => bool "
5.6 ("((Script Diophant'_equation (_ _ =))//(_))" 9)
5.7 -axioms
5.8 +axiomatization where
5.9
5.10 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
5.11
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Jul 26 11:36:43 2011 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Jul 26 13:28:39 2011 +0200
6.3 @@ -23,37 +23,35 @@
6.4 => bool list"
6.5 ("((Script SolveSystemScript (_ _ =))// (_))" 9)
6.6
6.7 -axioms
6.8 +axiomatization where
6.9 (*stated as axioms, todo: prove as theorems
6.10 'bdv' is a constant handled on the meta-level
6.11 specifically as a 'bound variable' *)
6.12
6.13 - commute_0_equality: "(0 = a) = (a = 0)"
6.14 + commute_0_equality: "(0 = a) = (a = 0)" and
6.15
6.16 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
6.17 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
6.18 separate_bdvs_add:
6.19 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]
6.20 - ==> (a + b = c) = (b = c + -1*a)"
6.21 + ==> (a + b = c) = (b = c + -1*a)" and
6.22 separate_bdvs0:
6.23 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |]
6.24 - ==> (a = b) = (a + -1*b = 0)"
6.25 + ==> (a = b) = (a + -1*b = 0)" and
6.26 separate_bdvs_add1:
6.27 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]
6.28 - ==> (a = b + c) = (a + -1*c = b)"
6.29 + ==> (a = b + c) = (a + -1*c = b)" and
6.30 separate_bdvs_add2:
6.31 "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |]
6.32 - ==> (a + b = c) = (b = -1*a + c)"
6.33 -
6.34 -
6.35 -
6.36 + ==> (a + b = c) = (b = -1*a + c)" and
6.37 separate_bdvs_mult:
6.38 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]
6.39 - ==>(a * b = c) = (b = c / a)"
6.40 -
6.41 + ==>(a * b = c) = (b = c / a)"
6.42 +axiomatization where (*..if replaced by "and" we get an error in
6.43 + --- rewrite in [EqSystem,normalize,2x2] --- step "--- 3---";*)
6.44 + order_system_NxN: "[a,b] = [b,a]"
6.45 (*requires rew_ord for termination, eg. ord_simplify_Integral;
6.46 works for lists of any length, interestingly !?!*)
6.47 - order_system_NxN: "[a,b] = [b,a]"
6.48
6.49 ML {*
6.50 val thy = @{theory};
6.51 @@ -412,8 +410,8 @@
6.52 ],
6.53 scr = EmptyScr};
6.54 *}
6.55 +
6.56 ML {*
6.57 -
6.58 ruleset' :=
6.59 overwritelthy @{theory}
6.60 (!ruleset',
6.61 @@ -427,9 +425,8 @@
6.62 ("norm_System", prep_rls norm_System)
6.63 ]);
6.64 *}
6.65 +
6.66 ML {*
6.67 -
6.68 -
6.69 (** problems **)
6.70
6.71 store_pbt
7.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Tue Jul 26 11:36:43 2011 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Jul 26 13:28:39 2011 +0200
7.3 @@ -26,18 +26,18 @@
7.4 NamedIntegrationScript :: "[real,real, real=>real, bool] => bool"
7.5 ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
7.6
7.7 -axioms
7.8 +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 - integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
7.14 - integral_var: "Integral bdv D bdv = bdv ^^^ 2 / 2"
7.15 + integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
7.16 + integral_var: "Integral bdv D bdv = bdv ^^^ 2 / 2" and
7.17
7.18 integral_add: "Integral (u + v) D bdv =
7.19 - (Integral u D bdv) + (Integral v D bdv)"
7.20 + (Integral u D bdv) + (Integral v D bdv)" and
7.21 integral_mult: "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>
7.22 - Integral (u * v) D bdv = u * (Integral v D bdv)"
7.23 + Integral (u * v) D bdv = u * (Integral v D bdv)" and
7.24 (*WN080222: this goes into sub-terms, too ...
7.25 call_for_new_c: "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>
7.26 a = a + new_c a"
8.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Jul 26 11:36:43 2011 +0200
8.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Jul 26 13:28:39 2011 +0200
8.3 @@ -16,17 +16,17 @@
8.4 ("((Script Solve'_lineq'_equation (_ _ =))//
8.5 (_))" 9)
8.6
8.7 -axioms
8.8 +axiomatization where
8.9 (*-- normalize --*)
8.10 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
8.11 - all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
8.12 - makex1_x: "a^^^1 = a"
8.13 - real_assoc_1: "a+(b+c) = a+b+c"
8.14 - real_assoc_2: "a*(b*c) = a*b*c"
8.15 + all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
8.16 + makex1_x: "a^^^1 = a" and
8.17 + real_assoc_1: "a+(b+c) = a+b+c" and
8.18 + real_assoc_2: "a*(b*c) = a*b*c" and
8.19
8.20 (*-- solve --*)
8.21 - lin_isolate_add1: "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
8.22 - lin_isolate_add2: "(a + bdv = 0) = ( bdv = (-1)*a)"
8.23 + lin_isolate_add1: "(a + b*bdv = 0) = (b*bdv = (-1)*a)" and
8.24 + lin_isolate_add2: "(a + bdv = 0) = ( bdv = (-1)*a)" and
8.25 lin_isolate_div: "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
8.26
8.27 ML {*
9.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Tue Jul 26 11:36:43 2011 +0200
9.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Tue Jul 26 13:28:39 2011 +0200
9.3 @@ -17,11 +17,11 @@
9.4 => bool list"
9.5 ("((Script Solve'_log (_ _=))//(_))" 9)
9.6
9.7 -axioms
9.8 +axiomatization where
9.9
9.10 - equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)"
9.11 + equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)" and
9.12 (* this is what students ^^^^^^^... are told to do *)
9.13 - equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)"
9.14 + equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)" and
9.15 exp_invers_log: "a^^^(a log b) = b"
9.16
9.17 ML {*
10.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Jul 26 11:36:43 2011 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Jul 26 13:28:39 2011 +0200
10.3 @@ -27,111 +27,111 @@
10.4 (_))" 9)
10.5
10.6 (*-------------------- rules------------------------------------------------*)
10.7 -axioms (*.not contained in Isabelle2002,
10.8 +axiomatization where (*.not contained in Isabelle2002,
10.9 stated as axioms, TODO: prove as theorems;
10.10 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
10.11
10.12 - realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
10.13 - realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
10.14 - realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"
10.15 - realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"
10.16 + realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
10.17 + realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
10.18 + realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
10.19 + realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
10.20
10.21 - realpow_oneI: "r ^^^ 1 = r"
10.22 - realpow_zeroI: "r ^^^ 0 = 1"
10.23 - realpow_eq_oneI: "1 ^^^ n = 1"
10.24 - realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n"
10.25 + realpow_oneI: "r ^^^ 1 = r" and
10.26 + realpow_zeroI: "r ^^^ 0 = 1" and
10.27 + realpow_eq_oneI: "1 ^^^ n = 1" and
10.28 + realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
10.29 realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
10.30 - (r * s) ^^^ n = r ^^^ n * s ^^^ n"
10.31 - realpow_minus_oneI: "-1 ^^^ (2 * n) = 1"
10.32 + (r * s) ^^^ n = r ^^^ n * s ^^^ n" and
10.33 + realpow_minus_oneI: "-1 ^^^ (2 * n) = 1" and
10.34
10.35 - realpow_twoI: "r ^^^ 2 = r * r"
10.36 - realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s"
10.37 - realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2"
10.38 - realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2"
10.39 - realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)"
10.40 - realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s"
10.41 - realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s"
10.42 - realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)"
10.43 - realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
10.44 + realpow_twoI: "r ^^^ 2 = r * r" and
10.45 + realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" and
10.46 + realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" and
10.47 + realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" and
10.48 + realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" and
10.49 + realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" and
10.50 + realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" and
10.51 + realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
10.52 + realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
10.53 realpow_def_atom: "[| Not (r is_atom); 1 < n |]
10.54 - ==> r ^^^ n = r * r ^^^ (n + -1)"
10.55 - realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
10.56 + ==> r ^^^ n = r * r ^^^ (n + -1)" and
10.57 + realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
10.58
10.59
10.60 - realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n"
10.61 - realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
10.62 + realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" and
10.63 + realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
10.64
10.65
10.66 (* RL 020914 *)
10.67 - real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
10.68 - real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
10.69 - real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
10.70 - real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
10.71 - real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
10.72 + real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
10.73 + real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
10.74 + real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
10.75 + real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
10.76 + real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
10.77 real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
10.78 - (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
10.79 - real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
10.80 + (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
10.81 + real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
10.82 real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
10.83 - -1*b^^^3"
10.84 + -1*b^^^3" and
10.85 (* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
10.86 (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
10.87 real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
10.88 - *(a + b)"
10.89 + *(a + b)" and
10.90 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
10.91 (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
10.92 - *(a + b)"
10.93 + *(a + b)" and
10.94 real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
10.95 - *(a^^^2 + 2*a*b + b^^^2)"
10.96 + *(a^^^2 + 2*a*b + b^^^2)" and
10.97 real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
10.98 (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
10.99 - + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
10.100 - real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*)
10.101 - real_diff_minus: "a - b = a + -1 * b"
10.102 - real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
10.103 - real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
10.104 + + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" and
10.105 + real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) and
10.106 + real_diff_minus: "a - b = a + -1 * b" and
10.107 + real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
10.108 + real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
10.109 (*WN071229 changed for Schaerding -----vvv*)
10.110 (*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
10.111 - real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)"
10.112 + real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" and
10.113 (*WN071229 changed for Schaerding -----^^^*)
10.114 real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
10.115 - (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
10.116 - real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
10.117 - real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
10.118 - real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2"
10.119 - real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
10.120 - real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"
10.121 - real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2"
10.122 - real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
10.123 - real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
10.124 - real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
10.125 - real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"
10.126 + (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
10.127 + real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
10.128 + real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
10.129 + real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
10.130 + real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
10.131 + real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
10.132 + real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
10.133 + real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
10.134 + real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
10.135 + real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
10.136 + real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" and
10.137
10.138 real_num_collect: "[| l is_const; m is_const |] ==>
10.139 - l * n + m * n = (l + m) * n"
10.140 + l * n + m * n = (l + m) * n" and
10.141 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
10.142 by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
10.143 real_num_collect_assoc: "[| l is_const; m is_const |] ==>
10.144 - l * n + (m * n + k) = (l + m) * n + k"
10.145 + l * n + (m * n + k) = (l + m) * n + k" and
10.146 real_num_collect_assoc_l: "[| l is_const; m is_const |] ==>
10.147 l * n + (m * n + k) = (l + m)
10.148 - * n + k"
10.149 + * n + k" and
10.150 real_num_collect_assoc_r: "[| l is_const; m is_const |] ==>
10.151 - (k + m * n) + l * n = k + (l + m) * n"
10.152 - real_one_collect: "m is_const ==> n + m * n = (1 + m) * n"
10.153 + (k + m * n) + l * n = k + (l + m) * n" and
10.154 + real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" and
10.155 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
10.156 by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
10.157 - real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k"
10.158 + real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
10.159
10.160 - real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
10.161 - real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n"
10.162 + real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
10.163 + real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" and
10.164
10.165 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
10.166 by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
10.167 - real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k"
10.168 - real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k"
10.169 - real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1"
10.170 + real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" and
10.171 + real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" and
10.172 + real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" and
10.173
10.174 - real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w"
10.175 + real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
10.176 real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
10.177
10.178 text {* remark on 'polynomials'
11.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Jul 26 11:36:43 2011 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Jul 26 13:28:39 2011 +0200
11.3 @@ -78,112 +78,114 @@
11.4 (_))" 9)
11.5
11.6 (*-------------------- rules -------------------------------------------------*)
11.7 -axioms
11.8 -
11.9 +axiomatization where
11.10 cancel_leading_coeff1: "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) =
11.11 - (a/c + b/c*bdv + bdv^^^2 = 0)"
11.12 + (a/c + b/c*bdv + bdv^^^2 = 0)" and
11.13 cancel_leading_coeff2: "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) =
11.14 - (a/c - b/c*bdv + bdv^^^2 = 0)"
11.15 + (a/c - b/c*bdv + bdv^^^2 = 0)" and
11.16 cancel_leading_coeff3: "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) =
11.17 - (a/c + b/c*bdv - bdv^^^2 = 0)"
11.18 + (a/c + b/c*bdv - bdv^^^2 = 0)" and
11.19
11.20 cancel_leading_coeff4: "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) =
11.21 - (a/c + 1/c*bdv + bdv^^^2 = 0)"
11.22 + (a/c + 1/c*bdv + bdv^^^2 = 0)" and
11.23 cancel_leading_coeff5: "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) =
11.24 - (a/c - 1/c*bdv + bdv^^^2 = 0)"
11.25 + (a/c - 1/c*bdv + bdv^^^2 = 0)" and
11.26 cancel_leading_coeff6: "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) =
11.27 - (a/c + 1/c*bdv - bdv^^^2 = 0)"
11.28 + (a/c + 1/c*bdv - bdv^^^2 = 0)" and
11.29
11.30 cancel_leading_coeff7: "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) =
11.31 - ( b/c*bdv + bdv^^^2 = 0)"
11.32 + ( b/c*bdv + bdv^^^2 = 0)" and
11.33 cancel_leading_coeff8: "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) =
11.34 - ( b/c*bdv - bdv^^^2 = 0)"
11.35 + ( b/c*bdv - bdv^^^2 = 0)" and
11.36
11.37 cancel_leading_coeff9: "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) =
11.38 - ( 1/c*bdv + bdv^^^2 = 0)"
11.39 + ( 1/c*bdv + bdv^^^2 = 0)" and
11.40 cancel_leading_coeff10:"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) =
11.41 - ( 1/c*bdv - bdv^^^2 = 0)"
11.42 + ( 1/c*bdv - bdv^^^2 = 0)" and
11.43
11.44 cancel_leading_coeff11:"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) =
11.45 - (a/b + bdv^^^2 = 0)"
11.46 + (a/b + bdv^^^2 = 0)" and
11.47 cancel_leading_coeff12:"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) =
11.48 - (a/b - bdv^^^2 = 0)"
11.49 + (a/b - bdv^^^2 = 0)" and
11.50 cancel_leading_coeff13:"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) =
11.51 - ( bdv^^^2 = 0/b)"
11.52 + ( bdv^^^2 = 0/b)" and
11.53
11.54 complete_square1: "(q + p*bdv + bdv^^^2 = 0) =
11.55 - (q + (p/2 + bdv)^^^2 = (p/2)^^^2)"
11.56 + (q + (p/2 + bdv)^^^2 = (p/2)^^^2)" and
11.57 complete_square2: "( p*bdv + bdv^^^2 = 0) =
11.58 - ( (p/2 + bdv)^^^2 = (p/2)^^^2)"
11.59 + ( (p/2 + bdv)^^^2 = (p/2)^^^2)" and
11.60 complete_square3: "( bdv + bdv^^^2 = 0) =
11.61 - ( (1/2 + bdv)^^^2 = (1/2)^^^2)"
11.62 + ( (1/2 + bdv)^^^2 = (1/2)^^^2)" and
11.63
11.64 complete_square4: "(q - p*bdv + bdv^^^2 = 0) =
11.65 - (q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
11.66 + (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" and
11.67 complete_square5: "(q + p*bdv - bdv^^^2 = 0) =
11.68 - (q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
11.69 + (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" and
11.70
11.71 - square_explicit1: "(a + b^^^2 = c) = ( b^^^2 = c - a)"
11.72 - square_explicit2: "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
11.73 + square_explicit1: "(a + b^^^2 = c) = ( b^^^2 = c - a)" and
11.74 + square_explicit2: "(a - b^^^2 = c) = (-(b^^^2) = c - a)" and
11.75
11.76 - bdv_explicit1: "(a + bdv = b) = (bdv = - a + b)"
11.77 - bdv_explicit2: "(a - bdv = b) = ((-1)*bdv = - a + b)"
11.78 - bdv_explicit3: "((-1)*bdv = b) = (bdv = (-1)*b)"
11.79 + bdv_explicit1: "(a + bdv = b) = (bdv = - a + b)" and
11.80 + bdv_explicit2: "(a - bdv = b) = ((-1)*bdv = - a + b)" and
11.81 + bdv_explicit3: "((-1)*bdv = b) = (bdv = (-1)*b)" and
11.82
11.83 - plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)
11.84 - minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*)
11.85 + plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) and
11.86 + minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*) and
11.87
11.88 (*-- normalize --*)
11.89 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
11.90 - all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"
11.91 - makex1_x: "a^^^1 = a"
11.92 - real_assoc_1: "a+(b+c) = a+b+c"
11.93 - real_assoc_2: "a*(b*c) = a*b*c"
11.94 + all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
11.95 + makex1_x: "a^^^1 = a" and
11.96 + real_assoc_1: "a+(b+c) = a+b+c" and
11.97 + real_assoc_2: "a*(b*c) = a*b*c" and
11.98
11.99 (* ---- degree 0 ----*)
11.100 - d0_true: "(0=0) = True"
11.101 - d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False"
11.102 + d0_true: "(0=0) = True" and
11.103 + d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" and
11.104 (* ---- degree 1 ----*)
11.105 d1_isolate_add1:
11.106 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)"
11.107 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" and
11.108 d1_isolate_add2:
11.109 - "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)"
11.110 + "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" and
11.111 d1_isolate_div:
11.112 - "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)"
11.113 + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" and
11.114 (* ---- degree 2 ----*)
11.115 d2_isolate_add1:
11.116 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)"
11.117 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" and
11.118 d2_isolate_add2:
11.119 - "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)"
11.120 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" and
11.121 d2_isolate_div:
11.122 - "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)"
11.123 + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)" and
11.124
11.125 - d2_prescind1: "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"
11.126 - d2_prescind2: "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)"
11.127 - d2_prescind3: "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"
11.128 - d2_prescind4: "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)"
11.129 + d2_prescind1: "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" and
11.130 + d2_prescind2: "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)" and
11.131 + d2_prescind3: "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" and
11.132 + d2_prescind4: "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)" and
11.133 (* eliminate degree 2 *)
11.134 (* thm for neg arguments in sqroot have postfix _neg *)
11.135 d2_sqrt_equation1: "[|(0<=c);Not(bdv occurs_in c)|] ==>
11.136 - (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))"
11.137 - d2_sqrt_equation1_neg:
11.138 - "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False"
11.139 - d2_sqrt_equation2: "(bdv^^^2=0) = (bdv=0)"
11.140 + (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" and
11.141 + d2_sqrt_equation1_neg:
11.142 + "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" and
11.143 + d2_sqrt_equation2: "(bdv^^^2=0) = (bdv=0)" and
11.144 d2_sqrt_equation3: "(b*bdv^^^2=0) = (bdv=0)"
11.145 - d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
11.146 + axiomatization where
11.147 + d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" and
11.148 d2_reduce_equation2: "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
11.149 - d2_pqformula1: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
11.150 + axiomatization where
11.151 +d2_pqformula1: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
11.152 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
11.153 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
11.154 - d2_pqformula1_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False"
11.155 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" and
11.156 + d2_pqformula1_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False" and
11.157 d2_pqformula2: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
11.158 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
11.159 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
11.160 - d2_pqformula2_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False"
11.161 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" and
11.162 + d2_pqformula2_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False" and
11.163 d2_pqformula3: "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
11.164 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
11.165 - | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
11.166 + | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" and
11.167 d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False"
11.168 + axioms
11.169 d2_pqformula4: "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
11.170 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
11.171 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
12.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jul 26 11:36:43 2011 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jul 26 13:28:39 2011 +0200
12.3 @@ -25,84 +25,84 @@
12.4 => bool"
12.5 ("((Script ProbeScript (_ _ =))// (_))" 9)
12.6
12.7 -axioms
12.8 +axiomatization where
12.9
12.10 - null_minus: "0 - a = -a"
12.11 - vor_minus_mal: "- a * b = (-a) * b"
12.12 + null_minus: "0 - a = -a" and
12.13 + vor_minus_mal: "- a * b = (-a) * b" and
12.14
12.15 (*commute with invariant (a.b).c -association*)
12.16 tausche_plus: "[| b ist_monom; a kleiner b |] ==>
12.17 - (b + a) = (a + b)"
12.18 + (b + a) = (a + b)" and
12.19 tausche_minus: "[| b ist_monom; a kleiner b |] ==>
12.20 - (b - a) = (-a + b)"
12.21 + (b - a) = (-a + b)" and
12.22 tausche_vor_plus: "[| b ist_monom; a kleiner b |] ==>
12.23 - (- b + a) = (a - b)"
12.24 + (- b + a) = (a - b)" and
12.25 tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==>
12.26 - (- b - a) = (-a - b)"
12.27 - tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)"
12.28 - tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)"
12.29 - tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)"
12.30 - tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)"
12.31 + (- b - a) = (-a - b)" and
12.32 + tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" and
12.33 + tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" and
12.34 + tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" and
12.35 + tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" and
12.36
12.37 (*commute with invariant (a.b).c -association*)
12.38 tausche_mal: "[| b is_atom; a kleiner b |] ==>
12.39 - (b * a) = (a * b)"
12.40 + (b * a) = (a * b)" and
12.41 tausche_vor_mal: "[| b is_atom; a kleiner b |] ==>
12.42 - (-b * a) = (-a * b)"
12.43 + (-b * a) = (-a * b)" and
12.44 tausche_mal_mal: "[| c is_atom; b kleiner c |] ==>
12.45 - (x * c * b) = (x * b * c)"
12.46 - x_quadrat: "(x * a) * a = x * a ^^^ 2"
12.47 + (x * c * b) = (x * b * c)" and
12.48 + x_quadrat: "(x * a) * a = x * a ^^^ 2" and
12.49
12.50
12.51 subtrahiere: "[| l is_const; m is_const |] ==>
12.52 - m * v - l * v = (m - l) * v"
12.53 + m * v - l * v = (m - l) * v" and
12.54 subtrahiere_von_1: "[| l is_const |] ==>
12.55 - v - l * v = (1 - l) * v"
12.56 + v - l * v = (1 - l) * v" and
12.57 subtrahiere_1: "[| l is_const; m is_const |] ==>
12.58 - m * v - v = (m - 1) * v"
12.59 + m * v - v = (m - 1) * v" and
12.60
12.61 subtrahiere_x_plus_minus: "[| l is_const; m is_const |] ==>
12.62 - (x + m * v) - l * v = x + (m - l) * v"
12.63 + (x + m * v) - l * v = x + (m - l) * v" and
12.64 subtrahiere_x_plus1_minus: "[| l is_const |] ==>
12.65 - (x + v) - l * v = x + (1 - l) * v"
12.66 + (x + v) - l * v = x + (1 - l) * v" and
12.67 subtrahiere_x_plus_minus1: "[| m is_const |] ==>
12.68 - (x + m * v) - v = x + (m - 1) * v"
12.69 + (x + m * v) - v = x + (m - 1) * v" and
12.70
12.71 subtrahiere_x_minus_plus: "[| l is_const; m is_const |] ==>
12.72 - (x - m * v) + l * v = x + (-m + l) * v"
12.73 + (x - m * v) + l * v = x + (-m + l) * v" and
12.74 subtrahiere_x_minus1_plus: "[| l is_const |] ==>
12.75 - (x - v) + l * v = x + (-1 + l) * v"
12.76 + (x - v) + l * v = x + (-1 + l) * v" and
12.77 subtrahiere_x_minus_plus1: "[| m is_const |] ==>
12.78 - (x - m * v) + v = x + (-m + 1) * v"
12.79 + (x - m * v) + v = x + (-m + 1) * v" and
12.80
12.81 subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>
12.82 - (x - m * v) - l * v = x + (-m - l) * v"
12.83 + (x - m * v) - l * v = x + (-m - l) * v" and
12.84 subtrahiere_x_minus1_minus:"[| l is_const |] ==>
12.85 - (x - v) - l * v = x + (-1 - l) * v"
12.86 + (x - v) - l * v = x + (-1 - l) * v" and
12.87 subtrahiere_x_minus_minus1:"[| m is_const |] ==>
12.88 - (x - m * v) - v = x + (-m - 1) * v"
12.89 + (x - m * v) - v = x + (-m - 1) * v" and
12.90
12.91
12.92 addiere_vor_minus: "[| l is_const; m is_const |] ==>
12.93 - - (l * v) + m * v = (-l + m) * v"
12.94 + - (l * v) + m * v = (-l + m) * v" and
12.95 addiere_eins_vor_minus: "[| m is_const |] ==>
12.96 - - v + m * v = (-1 + m) * v"
12.97 + - v + m * v = (-1 + m) * v" and
12.98 subtrahiere_vor_minus: "[| l is_const; m is_const |] ==>
12.99 - - (l * v) - m * v = (-l - m) * v"
12.100 + - (l * v) - m * v = (-l - m) * v" and
12.101 subtrahiere_eins_vor_minus:"[| m is_const |] ==>
12.102 - - v - m * v = (-1 - m) * v"
12.103 + - v - m * v = (-1 - m) * v" and
12.104
12.105 - vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b"
12.106 - vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b"
12.107 - vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
12.108 - vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
12.109 + vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" and
12.110 + vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" and
12.111 + vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
12.112 + vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
12.113
12.114 (*klammer_plus_plus = (add_assoc RS sym)*)
12.115 - klammer_plus_minus: "a + (b - c) = (a + b) - c"
12.116 - klammer_minus_plus: "a - (b + c) = (a - b) - c"
12.117 - klammer_minus_minus: "a - (b - c) = (a - b) + c"
12.118 + klammer_plus_minus: "a + (b - c) = (a + b) - c" and
12.119 + klammer_minus_plus: "a - (b + c) = (a - b) - c" and
12.120 + klammer_minus_minus: "a - (b - c) = (a - b) + c" and
12.121
12.122 - klammer_mult_minus: "a * (b - c) = a * b - a * c"
12.123 + klammer_mult_minus: "a * (b - c) = a * b - a * c" and
12.124 klammer_minus_mult: "(b - c) * a = b * a - c * a"
12.125
12.126 ML {*
13.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Tue Jul 26 11:36:43 2011 +0200
13.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Jul 26 13:28:39 2011 +0200
13.3 @@ -20,25 +20,25 @@
13.4 ("((Script Solve'_rat'_equation (_ _ =))//
13.5 (_))" 9)
13.6
13.7 -axioms
13.8 +axiomatization where
13.9 (* FIXME also in Poly.thy def. --> FIXED*)
13.10 (*real_diff_minus
13.11 "a - b = a + (-1) * b"*)
13.12 - real_rat_mult_1: "a*(b/c) = (a*b)/c"
13.13 - real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)"
13.14 - real_rat_mult_3: "(a/b)*c = (a*c)/b"
13.15 - real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2"
13.16 + real_rat_mult_1: "a*(b/c) = (a*b)/c" and
13.17 + real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)" and
13.18 + real_rat_mult_3: "(a/b)*c = (a*c)/b" and
13.19 + real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2" and
13.20
13.21 - rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
13.22 + rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" and
13.23 rat_double_rat_2: "[|Not(b=0);Not(c=0); Not(d=0)|] ==>
13.24 - ((a/b) / (c/d) = (a*d) / (b*c))"
13.25 - rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
13.26 + ((a/b) / (c/d) = (a*d) / (b*c))" and
13.27 + rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" and
13.28
13.29 (* equation to same denominator *)
13.30 rat_mult_denominator_both:
13.31 - "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"
13.32 + "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" and
13.33 rat_mult_denominator_left:
13.34 - "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
13.35 + "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" and
13.36 rat_mult_denominator_right:
13.37 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
13.38
14.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Jul 26 11:36:43 2011 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Jul 26 13:28:39 2011 +0200
14.3 @@ -16,51 +16,51 @@
14.4 is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
14.5 is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
14.6
14.7 -axioms (*.not contained in Isabelle2002,
14.8 +axiomatization where (*.not contained in Isabelle2002,
14.9 stated as axioms, TODO?: prove as theorems*)
14.10
14.11 - mult_cross: "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)"
14.12 - mult_cross1: " b ~= 0 ==> (a / b = c ) = (a = b * c)"
14.13 - mult_cross2: " d ~= 0 ==> (a = c / d) = (a * d = c)"
14.14 + mult_cross: "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)" and
14.15 + mult_cross1: " b ~= 0 ==> (a / b = c ) = (a = b * c)" and
14.16 + mult_cross2: " d ~= 0 ==> (a = c / d) = (a * d = c)" and
14.17
14.18 - add_minus: "a + b - b = a"(*RL->Poly.thy*)
14.19 - add_minus1: "a - b + b = a"(*RL->Poly.thy*)
14.20 + add_minus: "a + b - b = a"(*RL->Poly.thy*) and
14.21 + add_minus1: "a - b + b = a"(*RL->Poly.thy*) and
14.22
14.23 - rat_mult: "a / b * (c / d) = a * c / (b * d)"(*?Isa02*)
14.24 - rat_mult2: "a / b * c = a * c / b "(*?Isa02*)
14.25 -
14.26 - rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a / b"
14.27 - rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c / b"
14.28 + rat_mult: "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) and
14.29 + rat_mult2: "a / b * c = a * c / b "(*?Isa02*) and
14.30 +
14.31 + rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a / b" and
14.32 + rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c / b" and
14.33
14.34 (*real_times_divide1_eq .. Isa02*)
14.35 - real_times_divide_1_eq: "-1 * (c / d) =-1 * c / d "
14.36 + real_times_divide_1_eq: "-1 * (c / d) =-1 * c / d " and
14.37 real_times_divide_num: "a is_const ==>
14.38 - a * (c / d) = a * c / d "
14.39 -
14.40 - real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n"
14.41 + a * (c / d) = a * c / d " and
14.42 +
14.43 + real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n" and
14.44 (*real_mult_div_cancel1: "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
14.45
14.46 - real_divide_divide1: "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)"
14.47 - real_divide_divide1_mg: "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"
14.48 + real_divide_divide1: "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" and
14.49 + real_divide_divide1_mg: "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and
14.50 (*real_divide_divide2_eq: "x / y / z = x / (y * z)"..Isa02*)
14.51
14.52 - rat_power: "(a / b)^^^n = (a^^^n) / (b^^^n)"
14.53 + rat_power: "(a / b)^^^n = (a^^^n) / (b^^^n)" and
14.54
14.55
14.56 rat_add: "[| a is_const; b is_const; c is_const; d is_const |] ==>
14.57 - a / c + b / d = (a * d + b * c) / (c * d)"
14.58 + a / c + b / d = (a * d + b * c) / (c * d)" and
14.59 rat_add_assoc: "[| a is_const; b is_const; c is_const; d is_const |] ==>
14.60 - a / c +(b / d + e) = (a * d + b * c)/(d * c) + e"
14.61 + a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
14.62 rat_add1: "[| a is_const; b is_const; c is_const |] ==>
14.63 - a / c + b / c = (a + b) / c"
14.64 + a / c + b / c = (a + b) / c" and
14.65 rat_add1_assoc: "[| a is_const; b is_const; c is_const |] ==>
14.66 - a / c + (b / c + e) = (a + b) / c + e"
14.67 + a / c + (b / c + e) = (a + b) / c + e" and
14.68 rat_add2: "[| a is_const; b is_const; c is_const |] ==>
14.69 - a / c + b = (a + b * c) / c"
14.70 + a / c + b = (a + b * c) / c" and
14.71 rat_add2_assoc: "[| a is_const; b is_const; c is_const |] ==>
14.72 - a / c + (b + e) = (a + b * c) / c + e"
14.73 + a / c + (b + e) = (a + b * c) / c + e" and
14.74 rat_add3: "[| a is_const; b is_const; c is_const |] ==>
14.75 - a + b / c = (a * c + b) / c"
14.76 + a + b / c = (a * c + b) / c" and
14.77 rat_add3_assoc: "[| a is_const; b is_const; c is_const |] ==>
14.78 a + (b / c + e) = (a * c + b) / c + e"
14.79
15.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Jul 26 11:36:43 2011 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Jul 26 13:28:39 2011 +0200
15.3 @@ -13,32 +13,32 @@
15.4 (*sqrt :: "real => real" Isabelle "NthRoot.sqrt"*)
15.5 nroot :: "[real, real] => real"
15.6
15.7 -axioms (*.not contained in Isabelle2002,
15.8 +axiomatization where (*.not contained in Isabelle2002,
15.9 stated as axioms, TODO: prove as theorems;
15.10 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
15.11
15.12 root_plus_minus: "0 <= b ==>
15.13 - (a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))"
15.14 - root_false: "b < 0 ==> (a^^^2 = b) = False"
15.15 + (a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" and
15.16 + root_false: "b < 0 ==> (a^^^2 = b) = False" and
15.17
15.18 (* for expand_rootbinom *)
15.19 - real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
15.20 - real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
15.21 - real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
15.22 - real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
15.23 - real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
15.24 - real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
15.25 - realpow_mul: "(a*b)^^^n = a^^^n * b^^^n"
15.26 + real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
15.27 + real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
15.28 + real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
15.29 + real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
15.30 + real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
15.31 + real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
15.32 + realpow_mul: "(a*b)^^^n = a^^^n * b^^^n" and
15.33
15.34 - real_diff_minus: "a - b = a + (-1) * b"
15.35 - real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
15.36 - real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
15.37 - real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
15.38 - real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
15.39 - real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2"
15.40 - real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2"
15.41 + real_diff_minus: "a - b = a + (-1) * b" and
15.42 + real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
15.43 + real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
15.44 + real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
15.45 + real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
15.46 + real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
15.47 + real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
15.48
15.49 - real_root_positive: "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)"
15.50 + real_root_positive: "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)" and
15.51 real_root_negative: "a < 0 ==> (x ^^^ 2 = a) = False"
15.52
15.53 ML {*
16.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Jul 26 11:36:43 2011 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Jul 26 13:28:39 2011 +0200
16.3 @@ -37,83 +37,83 @@
16.4 ("((Script Solve'_right'_sq'_root'_equation (_ _ =))//
16.5 (_))" 9)
16.6
16.7 -axioms
16.8 +axiomatization where
16.9
16.10 (* normalize *)
16.11 - makex1_x: "a^^^1 = a"
16.12 - real_assoc_1: "a+(b+c) = a+b+c"
16.13 - real_assoc_2: "a*(b*c) = a*b*c"
16.14 + makex1_x: "a^^^1 = a" and
16.15 + real_assoc_1: "a+(b+c) = a+b+c" and
16.16 + real_assoc_2: "a*(b*c) = a*b*c" and
16.17
16.18 (* simplification of root*)
16.19 - sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a"
16.20 - sqrt_square_2: "sqrt (a ^^^ 2) = a"
16.21 - sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)"
16.22 - sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)"
16.23 + sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a" and
16.24 + sqrt_square_2: "sqrt (a ^^^ 2) = a" and
16.25 + sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)" and
16.26 + sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)" and
16.27
16.28 (* isolate one root on the LEFT or RIGHT hand side of the equation *)
16.29 sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==>
16.30 - (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
16.31 + (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" and
16.32 sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==>
16.33 - (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
16.34 + (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" and
16.35 sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==>
16.36 - (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)"
16.37 + (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" and
16.38 sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==>
16.39 - (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)"
16.40 + (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" and
16.41 sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==>
16.42 - (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
16.43 + (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" and
16.44 sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==>
16.45 - (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
16.46 + (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" and
16.47 sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==>
16.48 - (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
16.49 + (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" and
16.50 sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>
16.51 - (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
16.52 + (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" and
16.53 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
16.54 sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>
16.55 - (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
16.56 + (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" and
16.57 sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>
16.58 - (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
16.59 + (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" and
16.60 sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==>
16.61 - (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
16.62 + (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" and
16.63 sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==>
16.64 - (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
16.65 + (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" and
16.66
16.67 (* eliminate isolates sqrt *)
16.68 sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==>
16.69 ( (sqrt a + sqrt b = sqrt c + sqrt d) =
16.70 - (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
16.71 + (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" and
16.72 sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==>
16.73 ( (sqrt a - sqrt b = sqrt c + sqrt d) =
16.74 - (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
16.75 + (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" and
16.76 sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==>
16.77 ( (sqrt a + sqrt b = sqrt c - sqrt d) =
16.78 - (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
16.79 + (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" and
16.80 sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==>
16.81 ( (sqrt a - sqrt b = sqrt c - sqrt d) =
16.82 - (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
16.83 + (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" and
16.84 sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
16.85 - ( (sqrt (a) = b) = (a = (b^^^2)))"
16.86 + ( (sqrt (a) = b) = (a = (b^^^2)))" and
16.87 sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
16.88 - ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
16.89 + ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" and
16.90 sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
16.91 - ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
16.92 + ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" and
16.93 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
16.94 sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
16.95 - ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
16.96 + ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" and
16.97 sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
16.98 - ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
16.99 + ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" and
16.100 sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
16.101 - ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"
16.102 + ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" and
16.103 sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
16.104 - ( (a = sqrt (b)) = (a^^^2 = b))"
16.105 + ( (a = sqrt (b)) = (a^^^2 = b))" and
16.106 sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
16.107 - ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
16.108 + ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" and
16.109 sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
16.110 - ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
16.111 + ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" and
16.112 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
16.113 sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
16.114 - ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
16.115 + ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" and
16.116 sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
16.117 - ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
16.118 + ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" and
16.119 sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
16.120 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
16.121
17.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jul 26 11:36:43 2011 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jul 26 13:28:39 2011 +0200
17.3 @@ -22,14 +22,14 @@
17.4 (_))" 9)
17.5 (*-------------------- rules------------------------------------------------*)
17.6
17.7 -axioms
17.8 +axiomatization where
17.9 (* eliminate ratRootTerm *)
17.10 rootrat_equation_left_1:
17.11 - "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
17.12 + "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" and
17.13 rootrat_equation_left_2:
17.14 - "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
17.15 + "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" and
17.16 rootrat_equation_right_2:
17.17 - "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
17.18 + "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" and
17.19 rootrat_equation_right_1:
17.20 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
17.21
18.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Jul 26 11:36:43 2011 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Jul 26 13:28:39 2011 +0200
18.3 @@ -63,109 +63,109 @@
18.4
18.5 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
18.6
18.7 -axioms (*TODO: prove as theorems*)
18.8 +axiomatization where (*TODO: prove as theorems*)
18.9
18.10 - radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n"
18.11 - rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n"
18.12 - rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k"
18.13 - rdistr_div_right: "((k::real) + l) / n = k / n + l / n"
18.14 + radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" and
18.15 + rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" and
18.16 + rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" and
18.17 + rdistr_div_right: "((k::real) + l) / n = k / n + l / n" and
18.18 rcollect_right:
18.19 - "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"
18.20 + "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
18.21 rcollect_one_left:
18.22 - "m is_const ==> (n::real) + m * n = (1 + m) * n"
18.23 + "m is_const ==> (n::real) + m * n = (1 + m) * n" and
18.24 rcollect_one_left_assoc:
18.25 - "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"
18.26 + "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
18.27 rcollect_one_left_assoc_p:
18.28 - "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"
18.29 + "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
18.30
18.31 - rtwo_of_the_same: "a + a = 2 * a"
18.32 - rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a"
18.33 - rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x"
18.34 + rtwo_of_the_same: "a + a = 2 * a" and
18.35 + rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" and
18.36 + rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
18.37
18.38 - rcancel_den: "not(a=0) ==> a * (b / a) = b"
18.39 - rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
18.40 - rshift_nominator: "(a::real) * b / c = a / c * b"
18.41 + rcancel_den: "not(a=0) ==> a * (b / a) = b" and
18.42 + rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
18.43 + rshift_nominator: "(a::real) * b / c = a / c * b" and
18.44
18.45 - exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
18.46 - rsqare: "(a::real) * a = a ^^^ 2"
18.47 - power_1: "(a::real) ^^^ 1 = a"
18.48 - rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
18.49 + exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
18.50 + rsqare: "(a::real) * a = a ^^^ 2" and
18.51 + power_1: "(a::real) ^^^ 1 = a" and
18.52 + rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" and
18.53
18.54 - rmult_1: "1 * k = (k::real)"
18.55 - rmult_1_right: "k * 1 = (k::real)"
18.56 - rmult_0: "0 * k = (0::real)"
18.57 - rmult_0_right: "k * 0 = (0::real)"
18.58 - radd_0: "0 + k = (k::real)"
18.59 - radd_0_right: "k + 0 = (k::real)"
18.60 + rmult_1: "1 * k = (k::real)" and
18.61 + rmult_1_right: "k * 1 = (k::real)" and
18.62 + rmult_0: "0 * k = (0::real)" and
18.63 + rmult_0_right: "k * 0 = (0::real)" and
18.64 + radd_0: "0 + k = (k::real)" and
18.65 + radd_0_right: "k + 0 = (k::real)" and
18.66
18.67 radd_real_const_eq:
18.68 - "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"
18.69 + "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
18.70 radd_real_const:
18.71 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
18.72 -
18.73 + and
18.74 (*for AC-operators*)
18.75 - radd_commute: "(m::real) + (n::real) = n + m"
18.76 - radd_left_commute: "(x::real) + (y + z) = y + (x + z)"
18.77 - radd_assoc: "(m::real) + n + k = m + (n + k)"
18.78 - rmult_commute: "(m::real) * n = n * m"
18.79 - rmult_left_commute: "(x::real) * (y * z) = y * (x * z)"
18.80 - rmult_assoc: "(m::real) * n * k = m * (n * k)"
18.81 + radd_commute: "(m::real) + (n::real) = n + m" and
18.82 + radd_left_commute: "(x::real) + (y + z) = y + (x + z)" and
18.83 + radd_assoc: "(m::real) + n + k = m + (n + k)" and
18.84 + rmult_commute: "(m::real) * n = n * m" and
18.85 + rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" and
18.86 + rmult_assoc: "(m::real) * n * k = m * (n * k)" and
18.87
18.88 (*for equations: 'bdv' is a meta-constant*)
18.89 - risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
18.90 - risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
18.91 - risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)"
18.92 + risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and
18.93 + risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and
18.94 + risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" and
18.95
18.96 rnorm_equation_add:
18.97 - "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"
18.98 + "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and
18.99
18.100 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
18.101 - root_ge0: "0 <= a ==> 0 <= sqrt a"
18.102 + root_ge0: "0 <= a ==> 0 <= sqrt a" and
18.103 (*should be dropped with better simplification in eval_rls ...*)
18.104 root_add_ge0:
18.105 - "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"
18.106 + "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and
18.107 root_ge0_1:
18.108 - "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"
18.109 + "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and
18.110 root_ge0_2:
18.111 - "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"
18.112 + "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and
18.113
18.114
18.115 - rroot_square_inv: "(sqrt a)^^^ 2 = a"
18.116 - rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)"
18.117 - rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
18.118 - rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
18.119 + rroot_square_inv: "(sqrt a)^^^ 2 = a" and
18.120 + rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" and
18.121 + rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and
18.122 + rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and
18.123
18.124
18.125 (*for root-equations*)
18.126 square_equation_left:
18.127 - "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"
18.128 + "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" and
18.129 square_equation_right:
18.130 - "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"
18.131 + "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" and
18.132 (*causes frequently non-termination:*)
18.133 square_equation:
18.134 - "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"
18.135 + "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" and
18.136
18.137 - risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"
18.138 - risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
18.139 - risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)"
18.140 + risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" and
18.141 + risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and
18.142 + risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" and
18.143
18.144 (*for polynomial equations of degree 2; linear case in RatArith*)
18.145 - mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
18.146 - constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
18.147 - constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
18.148 + mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" and
18.149 + constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" and
18.150 + constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" and
18.151
18.152 square_equality:
18.153 - "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"
18.154 + "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
18.155 square_equality_0:
18.156 - "(x^^^2 = 0) = (x = 0)"
18.157 + "(x^^^2 = 0) = (x = 0)" and
18.158
18.159 (*isolate root on the LEFT hand side of the equation
18.160 otherwise shuffling from left to right would not terminate*)
18.161
18.162 rroot_to_lhs:
18.163 - "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"
18.164 + "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
18.165 rroot_to_lhs_mult:
18.166 - "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"
18.167 + "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
18.168 rroot_to_lhs_add_mult:
18.169 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
18.170 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
19.1 --- a/src/Tools/isac/ProgLang/ListC.thy Tue Jul 26 11:36:43 2011 +0200
19.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Jul 26 13:28:39 2011 +0200
19.3 @@ -33,35 +33,36 @@
19.4 where "a -- b == foldl del a b"
19.5
19.6 consts NTH :: "[real, 'a list] => 'a"
19.7 -axioms
19.8 +
19.9 +axiomatization where
19.10 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
19.11 - NTH_NIL: "NTH 1 (x#xs) = x"
19.12 + NTH_NIL: "NTH 1 (x#xs) = x" and
19.13 (* NTH_CONS: "NTH n (x#xs) = NTH (n+ -1) xs" *)
19.14
19.15 (*rewriter does not reach base case ...... ;
19.16 the condition involves another rule set (erls, eval_binop in Atools):*)
19.17 - NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs"
19.18 + NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" and
19.19
19.20 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
19.21 (*primrec*)
19.22 - hd_thm: "hd(x#xs) = x"
19.23 + hd_thm: "hd(x#xs) = x" and
19.24 (*primrec*)
19.25 - tl_Nil: "tl([]) = []"
19.26 - tl_Cons: "tl(x#xs) = xs"
19.27 + tl_Nil: "tl([]) = []" and
19.28 + tl_Cons: "tl(x#xs) = xs" and
19.29 (*primrec*)
19.30 - null_Nil: "null([]) = True"
19.31 - null_Cons: "null(x#xs) = False"
19.32 + null_Nil: "null([]) = True" and
19.33 + null_Cons: "null(x#xs) = False" and
19.34 (*primrec*)
19.35 - LAST: "last(x#xs) = (if xs=[] then x else last xs)"
19.36 + LAST: "last(x#xs) = (if xs=[] then x else last xs)" and
19.37 (*primrec*)
19.38 - butlast_Nil: "butlast [] = []"
19.39 - butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
19.40 + butlast_Nil: "butlast [] = []" and
19.41 + butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" and
19.42 (*primrec
19.43 mem_Nil: "x mem [] = False"
19.44 mem_Cons: "x mem (y#ys) = (if y=x then True else x mem ys)"
19.45 *)
19.46 - mem_Nil: "x : set [] = False"
19.47 - mem_Cons: "x : set (y#ys) = (if y=x then True else x : set ys)"
19.48 + mem_Nil: "x : set [] = False" and
19.49 + mem_Cons: "x : set (y#ys) = (if y=x then True else x : set ys)" and
19.50 (*primrec-------already named---
19.51 "set [] = {}"
19.52 "set (x#xs) = insert x (set xs)"
19.53 @@ -70,27 +71,27 @@
19.54 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
19.55 ----------------*)
19.56 (*primrec*)
19.57 - map_Nil: "map f [] = []"
19.58 - map_Cons: "map f (x#xs) = f(x)#map f xs"
19.59 + map_Nil: "map f [] = []" and
19.60 + map_Cons: "map f (x#xs) = f(x)#map f xs" and
19.61 (*primrec*)
19.62 - append_Nil: "[] @ys = ys"
19.63 - append_Cons: "(x#xs)@ys = x#(xs@ys)"
19.64 + append_Nil: "[] @ys = ys" and
19.65 + append_Cons: "(x#xs)@ys = x#(xs@ys)" and
19.66 (*primrec*)
19.67 - rev_Nil: "rev([]) = []"
19.68 - rev_Cons: "rev(x#xs) = rev(xs) @ [x]"
19.69 + rev_Nil: "rev([]) = []" and
19.70 + rev_Cons: "rev(x#xs) = rev(xs) @ [x]" and
19.71 (*primrec*)
19.72 - filter_Nil: "filter P [] = []"
19.73 - filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)"
19.74 + filter_Nil: "filter P [] = []" and
19.75 + filter_Cons: "filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" and
19.76 (*primrec-------already named---
19.77 foldl_Nil "foldl f a [] = a"
19.78 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
19.79 ----------------*)
19.80 (*primrec*)
19.81 - foldr_Nil: "foldr f [] a = a"
19.82 - foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)"
19.83 + foldr_Nil: "foldr f [] a = a" and
19.84 + foldr_Cons: "foldr f (x#xs) a = f x (foldr f xs a)" and
19.85 (*primrec*)
19.86 - concat_Nil: "concat([]) = []"
19.87 - concat_Cons: "concat(x#xs) = x @ concat(xs)"
19.88 + concat_Nil: "concat([]) = []" and
19.89 + concat_Cons: "concat(x#xs) = x @ concat(xs)" and
19.90 (*primrec-------already named---
19.91 drop_Nil "drop n [] = []"
19.92 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
19.93 @@ -111,16 +112,16 @@
19.94 | Suc j => x # xs[j:=v])"
19.95 ----------------*)
19.96 (*primrec*)
19.97 - takeWhile_Nil: "takeWhile P [] = []"
19.98 + takeWhile_Nil: "takeWhile P [] = []" and
19.99 takeWhile_Cons:
19.100 - "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
19.101 + "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" and
19.102 (*primrec*)
19.103 - dropWhile_Nil: "dropWhile P [] = []"
19.104 + dropWhile_Nil: "dropWhile P [] = []" and
19.105 dropWhile_Cons:
19.106 - "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
19.107 + "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" and
19.108 (*primrec*)
19.109 - zip_Nil: "zip xs [] = []"
19.110 - zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)"
19.111 + zip_Nil: "zip xs [] = []" and
19.112 + zip_Cons: "zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" and
19.113 (* Warning: simpset does not contain this definition but separate theorems
19.114 for xs=[] / xs=z#zs *)
19.115 (*primrec
19.116 @@ -128,12 +129,12 @@
19.117 upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
19.118 *)
19.119 (*primrec*)
19.120 - distinct_Nil: "distinct [] = True"
19.121 - distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)"
19.122 + distinct_Nil: "distinct [] = True" and
19.123 + distinct_Cons: "distinct (x#xs) = (x ~: set xs & distinct xs)" and
19.124 (*primrec*)
19.125 - remdups_Nil: "remdups [] = []"
19.126 - remdups_Cons: "remdups (x#xs) =
19.127 - (if x : set xs then remdups xs else x # remdups xs)"
19.128 + remdups_Nil: "remdups [] = []" and
19.129 + remdups_Cons: "remdups (x#xs) =
19.130 + (if x : set xs then remdups xs else x # remdups xs)"
19.131 (*primrec-------already named---
19.132 replicate_0 "replicate 0 x = []"
19.133 replicate_Suc "replicate (Suc n) x = x # replicate n x"
20.1 --- a/test/Tools/isac/Knowledge/algein.sml Tue Jul 26 11:36:43 2011 +0200
20.2 +++ b/test/Tools/isac/Knowledge/algein.sml Tue Jul 26 13:28:39 2011 +0200
20.3 @@ -36,17 +36,7 @@
20.4 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.5 === inhibit exn 110722=============================================================*)
20.6
20.7 -val str =
20.8 -"Script RechnenSymbolScript (k_::bool) (q__::bool) \
20.9 -\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
20.10 -\ (let t_ = Take (l_ = Oben + Senkrecht + Unten); \
20.11 -\ sum_ = boollist2sum o_;\
20.12 -\ t_ = Substitute [Oben = sum_] t_;\
20.13 -\ t_ = Substitute o_ t_;\
20.14 -\ t_ = Substitute [k_, q__] t_;\
20.15 -\ t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
20.16 -\ in t_)"
20.17 -;
20.18 +
20.19 (*=== inhibit exn 110722=============================================================
20.20 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.21
21.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Tue Jul 26 11:36:43 2011 +0200
21.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Tue Jul 26 13:28:39 2011 +0200
21.3 @@ -10,7 +10,6 @@
21.4 "table of contents -----------------------------------------------";
21.5 "-----------------------------------------------------------------";
21.6 "----------- the rules -------------------------------------------";
21.7 -"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
21.8 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
21.9 "----------- simplify_leaf for this script -----------------------";
21.10 "----------- Bsp 7.27 me -----------------------------------------";
21.11 @@ -50,70 +49,7 @@
21.12 else error "biegelinie.sml: Moment_Neigung";
21.13 === inhibit exn 110722=============================================================*)
21.14
21.15 -"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
21.16 -"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
21.17 -"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
21.18 -val str =
21.19 -"Script BiegelinieScript \
21.20 -\(l_::real) (q__::real) (v_v::real) (b_::real=>real) \
21.21 -\(rb_::bool list) (rm_::bool list) = \
21.22 -\ (let q___ = Take (q_ v_v = q__); \
21.23 -\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
21.24 -\ (Rewrite Belastung_Querkraft True)) q___; \
21.25 -\ (Q__:: bool) = \
21.26 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
21.27 -\ [diff,integration,named]) \
21.28 -\ [REAL (rhs q___), REAL v_v, real_REAL Q]); \
21.29 -\ Q__ = Rewrite Querkraft_Moment True Q__; \
21.30 -\ (M__::bool) = \
21.31 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
21.32 -\ [diff,integration,named]) \
21.33 -\ [REAL (rhs Q__), REAL v_v, real_REAL M_b]); \
21.34 -\ e1__ = nth_ 1 rm_; \
21.35 -\ (x1__::real) = argument_in (lhs e1__); \
21.36 -\ (M1__::bool) = (Substitute [v_ = x1__]) M__; \
21.37 -\ M1__ = (Substitute [e1__]) M1__ ; \
21.38 -\ M2__ = Take M__; "^
21.39 -(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
21.40 -" e2__ = nth_ 2 rm_; \
21.41 -\ (x2__::real) = argument_in (lhs e2__); \
21.42 -\ (M2__::bool) = ((Substitute [v_ = x2__]) @@ \
21.43 -\ (Substitute [e2__])) M2__; \
21.44 -\ (c_1_2__::bool list) = \
21.45 -\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
21.46 -\ [booll_ [M1__, M2__], reall [c,c_2]]); \
21.47 -\ M__ = Take M__; \
21.48 -\ M__ = ((Substitute c_1_2__) @@ \
21.49 -\ (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]\
21.50 -\ simplify_System False)) @@ \
21.51 -\ (Rewrite Moment_Neigung False) @@ \
21.52 -\ (Rewrite make_fun_explicit False)) M__; "^
21.53 -(*----------------------- and the same once more ------------------------*)
21.54 -" (N__:: bool) = \
21.55 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
21.56 -\ [diff,integration,named]) \
21.57 -\ [REAL (rhs M__), REAL v_v, real_REAL y']); \
21.58 -\ (B__:: bool) = \
21.59 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
21.60 -\ [diff,integration,named]) \
21.61 -\ [REAL (rhs N__), REAL v_v, real_REAL y]); \
21.62 -\ e1__ = nth_ 1 rb_; \
21.63 -\ (x1__::real) = argument_in (lhs e1__); \
21.64 -\ (B1__::bool) = (Substitute [v_ = x1__]) B__; \
21.65 -\ B1__ = (Substitute [e1__]) B1__ ; \
21.66 -\ B2__ = Take B__; \
21.67 -\ e2__ = nth_ 2 rb_; \
21.68 -\ (x2__::real) = argument_in (lhs e2__); \
21.69 -\ (B2__::bool) = ((Substitute [v_ = x2__]) @@ \
21.70 -\ (Substitute [e2__])) B2__; \
21.71 -\ (c_1_2__::bool list) = \
21.72 -\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
21.73 -\ [booll_ [B1__, B2__], reall [c,c_2]]); \
21.74 -\ B__ = Take B__; \
21.75 -\ B__ = ((Substitute c_1_2__) @@ \
21.76 -\ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \
21.77 -\ in B__)"
21.78 -;
21.79 +
21.80 (*=== inhibit exn 110722=============================================================
21.81 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.82
21.83 @@ -666,63 +602,7 @@
21.84 \ in (equs_::bool list))"
21.85 ;
21.86 (*=== inhibit exn 110722=============================================================
21.87 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.88 -val str =
21.89 -"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
21.90 -\ (let b1_ = Take (nth_ 1 beds_); \
21.91 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
21.92 -\ f1_ = hd fs_ \
21.93 -\ in (equs_::bool list))"
21.94 -;
21.95 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.96
21.97 -val ttt = str2term "sameFunId (lhs b1_) fun___"; atomty ttt;
21.98 -val ttt = str2term "filter"; atomty ttt;
21.99 -val ttt = str2term "filter::[real => bool, real list] => real list";atomty ttt;
21.100 -val ttt = str2term "filter::[bool => bool, bool list] => bool list";
21.101 -val ttt = str2term "filter (sameFunId (lhs b1_)) funs_"; atomty ttt;
21.102 -
21.103 -val str =
21.104 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
21.105 -\ (let beds_ = rev beds_; \
21.106 -\ b1_ = Take (nth_ 1 beds_); \
21.107 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
21.108 -\ f1_ = hd fs_ \
21.109 -\ in (equs_::bool list))"
21.110 -;
21.111 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.112 -val str =
21.113 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
21.114 -\ (let b1_ = Take (nth_ 1 rb_); \
21.115 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
21.116 -\ (equ_::bool) = \
21.117 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
21.118 -\ [Equation,fromFunction]) \
21.119 -\ [BOOL (hd fs_), BOOL b1_]) \
21.120 -\ in [equ_])"
21.121 -;
21.122 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.123 -val str =
21.124 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
21.125 -\ (let b1_ = Take (nth_ 1 rb_); \
21.126 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
21.127 -\ (e1_::bool) = \
21.128 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
21.129 -\ [Equation,fromFunction]) \
21.130 -\ [BOOL (hd fs_), BOOL b1_]); \
21.131 -\ b2_ = Take (nth_ 2 rb_); \
21.132 -\ fs_ = filter (sameFunId (lhs b2_)) funs_; \
21.133 -\ (e2_::bool) = \
21.134 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
21.135 -\ [Equation,fromFunction]) \
21.136 -\ [BOOL (hd fs_), BOOL b2_]) \
21.137 -\ in [e1_,e1_])"
21.138 -;
21.139 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.140 -
21.141 -atomty sc;
21.142 -
21.143 -"----- execute script by manual rewriting";
21.144 (*show_types := true;*)
21.145 val funs_ = str2term "funs_::bool list";
21.146 val funs = str2term
21.147 @@ -896,38 +776,6 @@
21.148 \ [BOOL (hd fs_), BOOL b1_]) \
21.149 \ in [e1_,e2_,e3_,e4_])"
21.150 ;
21.151 -(*=== inhibit exn 110722=============================================================
21.152 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.153 -val str =
21.154 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
21.155 -\ (let b1_ = nth_ 1 rb_; \
21.156 -\ fs_ = filter_sameFunId (lhs b1_) funs_; \
21.157 -\ (e1_::bool) = \
21.158 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
21.159 -\ [Equation,fromFunction]) \
21.160 -\ [BOOL (hd fs_), BOOL b1_]); \
21.161 -\ b2_ = nth_ 2 rb_; \
21.162 -\ fs_ = filter_sameFunId (lhs b2_) funs_; \
21.163 -\ (e2_::bool) = \
21.164 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
21.165 -\ [Equation,fromFunction]) \
21.166 -\ [BOOL (hd fs_), BOOL b2_]); \
21.167 -\ b3_ = nth_ 3 rb_; \
21.168 -\ fs_ = filter_sameFunId (lhs b3_) funs_; \
21.169 -\ (e3_::bool) = \
21.170 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
21.171 -\ [Equation,fromFunction]) \
21.172 -\ [BOOL (hd fs_), BOOL b3_]); \
21.173 -\ b4_ = nth_ 4 rb_; \
21.174 -\ fs_ = filter_sameFunId (lhs b4_) funs_; \
21.175 -\ (e4_::bool) = \
21.176 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
21.177 -\ [Equation,fromFunction]) \
21.178 -\ [BOOL (hd fs_), BOOL b4_]) \
21.179 -\ in [e1_,e2_,e3_,e4_])"
21.180 -;
21.181 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.182 -=== inhibit exn 110722=============================================================*)
21.183
21.184
21.185
22.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue Jul 26 11:36:43 2011 +0200
22.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Tue Jul 26 13:28:39 2011 +0200
22.3 @@ -1,3 +1,4 @@
22.4 +
22.5 (* tests for IsacKnowledge/DiffApp
22.6 author Walther Neuper 000301
22.7 (c) due to copyright terms
22.8 @@ -20,7 +21,6 @@
22.9 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
22.10
22.11
22.12 -(*=== inhibit exn 110722=============================================================
22.13
22.14
22.15
22.16 @@ -29,8 +29,10 @@
22.17 " #################################################### ";
22.18 " -------------- [maximum_of,function] --------------- ";
22.19 val pbt =
22.20 - ["fixedValues f_ix","maximum m_","valuesFor v_s","relations r_s"];
22.21 + ["fixedValues f_ix","maximum m_m","valuesFor v_s","relations r_s"];
22.22 +(*=== inhibit exn 110722=============================================================
22.23 map (the o (parseold thy)) pbt;
22.24 +=== inhibit exn 110722=============================================================*)
22.25 val fmz =
22.26 ["fixedValues [r=Arbfix]","maximum A",
22.27 "valuesFor [a,b]",
22.28 @@ -43,11 +45,14 @@
22.29 "interval {x::real. 0 <= x & x <= 2*r}",
22.30 "interval {x::real. 0 <= x & x <= pi}",
22.31 "errorBound (eps=(0::real))"];
22.32 +(*=== inhibit exn 110722=============================================================
22.33 map (the o (parseold thy)) fmz;
22.34 " -------------- [make,function] -------------- ";
22.35 +=== inhibit exn 110722=============================================================*)
22.36 val pbt =
22.37 ["functionOf f_f","boundVariable v_v","equalities eqs",
22.38 - "functionTerm f_0_"];
22.39 + "functionTerm f_0_0"];
22.40 +(*=== inhibit exn 110722=============================================================
22.41 map (the o (parseold thy)) pbt;
22.42 val fmz12 =
22.43 ["functionOf A","boundVariable a","boundVariable b",
22.44 @@ -61,7 +66,7 @@
22.45 map (the o (parseold thy)) fmz3;
22.46 " --------- [univar,equation] --------- ";
22.47 val pbt =
22.48 - ["equality e_e","solveFor v_v","solutions v_i_"];
22.49 + ["equality e_e","solveFor v_v","solutions v_i_i"];
22.50 map (the o (parseold thy)) pbt;
22.51 val fmz =
22.52 ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
22.53 @@ -69,8 +74,8 @@
22.54 map (the o (parseold thy)) fmz;
22.55 " ---- [on_interval,maximum_of,function] ---- ";
22.56 val pbt =
22.57 - ["functionTerm t_","boundVariable v_v","interval itv_",
22.58 - "errorBound err_","maxArgument v_0"];
22.59 + ["functionTerm t_t","boundVariable v_v","interval itv_v",
22.60 + "errorBound err_r","maxArgument v_0"];
22.61 map (the o (parseold thy)) pbt;
22.62 val fmz12 =
22.63 [(*28.11.00: "functionTerm (A_0 = a*sqrt(#4*r^^^#2 - a^^^#2))",*)
22.64 @@ -100,8 +105,8 @@
22.65 map (the o (parseold thy)) fmz;
22.66 " --------- [find_values,tool] --------- ";
22.67 val pbt =
22.68 - ["maxArgument ma_","functionTerm f_f","boundVariable v_v",
22.69 - "valuesFor vls_","additionalRels r_s"];
22.70 + ["maxArgument ma_a","functionTerm f_f","boundVariable v_v",
22.71 + "valuesFor vls_s","additionalRels r_s"];
22.72 map (the o (parseold thy)) pbt;
22.73 val fmz1 =
22.74 ["maxArgument (a_0=(srqt 2)*r)",
22.75 @@ -762,3 +767,4 @@
22.76
22.77
22.78 ===== inhibit exn 110722===========================================================*)
22.79 +
23.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue Jul 26 11:36:43 2011 +0200
23.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue Jul 26 13:28:39 2011 +0200
23.3 @@ -166,17 +166,17 @@
23.4 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
23.5
23.6 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
23.7 -if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"
23.8 -then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
23.9 +if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
23.10
23.11 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
23.12 if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"
23.13 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
23.14
23.15 +"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...";
23.16 val SOME (t,_) = rewrite_set_ thy true order_system t;
23.17 if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"
23.18 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
23.19 -
23.20 +"--- 4---";
23.21
23.22 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
23.23 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
23.24 @@ -547,103 +547,6 @@
23.25 \ e1__1 = hd es__e\
23.26 \ in ([]))"
23.27 ;
23.28 -(*=== inhibit exn 110722=============================================================
23.29 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.30 -val str =
23.31 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.32 -\ (let es__ = Take es_; \
23.33 -\ e1__ = hd es__; \
23.34 -\ e2__ = hd (tl es__)\
23.35 -\ in ([]))"
23.36 -;
23.37 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.38 -val str =
23.39 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.40 -\ (let es__ = Take es_; \
23.41 -\ e1__ = hd es__; \
23.42 -\ e2__ = hd (tl es__);\
23.43 -\ es__ = [1=2,3=4]\
23.44 -\ in ([]))"
23.45 -;
23.46 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.47 -val str =
23.48 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.49 -\ (let es__ = Take es_; \
23.50 -\ e1__ = hd es__; \
23.51 -\ e2__ = hd (tl es__);\
23.52 -\ es__ = [e1__,e2__]\
23.53 -\ in ([]))"
23.54 -;
23.55 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.56 -val str =
23.57 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.58 -\ (let es__ = Take es_; \
23.59 -\ e1__ = hd es__; \
23.60 -\ e2__ = hd (tl es__);\
23.61 -\ es__ = [e1__, Substitute [e1__] e2__];\
23.62 -\ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.63 -\ simplify_System False)) es__ \
23.64 -\ in ([]))"
23.65 -;
23.66 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.67 -val str =
23.68 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.69 -\ (let es__ = Take es_; \
23.70 -\ e1__ = hd es__; \
23.71 -\ e2__ = hd (tl es__);\
23.72 -\ es__ = [e1__, Substitute [e1__] e2__];\
23.73 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.74 -\ isolate_bdvs False)) @@ \
23.75 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.76 -\ simplify_System False))) es__ \
23.77 -\ in ([]))"
23.78 -;
23.79 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.80 -val str =
23.81 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.82 -\ (let es__ = Take es_; \
23.83 -\ e1__ = hd es__; \
23.84 -\ e2__ = hd (tl es__);\
23.85 -\ es__ = [e1__, Substitute [e1__] e2__];\
23.86 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.87 -\ simplify_System_parenthesized False)) @@ \
23.88 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.89 -\ isolate_bdvs False)) @@ \
23.90 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.91 -\ simplify_System False))) es__ \
23.92 -\ in ([]))"
23.93 -;
23.94 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.95 -val str =
23.96 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.97 -\ (let es__ = Take es_; \
23.98 -\ e1__ = hd es__; \
23.99 -\ e2__ = hd (tl es__); \
23.100 -\ es__ = [e1__, Substitute [e1__] e2__]; \
23.101 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.102 -\ simplify_System_parenthesized False)) @@ \
23.103 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.104 -\ isolate_bdvs False)) @@ \
23.105 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.106 -\ simplify_System False))) es__ \
23.107 -\ in es__)"
23.108 -;
23.109 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.110 -val str =
23.111 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.112 -\ (let es__ = Take es_; \
23.113 -\ e1__ = hd es__; \
23.114 -\ e2__ = hd (tl es__); \
23.115 -\ es__ = [e1__, Substitute [e1__] e2__] \
23.116 -\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.117 -\ simplify_System_parenthesized False)) @@ \
23.118 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
23.119 -\ isolate_bdvs False)) @@ \
23.120 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.121 -\ simplify_System False))) es__)"
23.122 -;
23.123 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.124 -=== inhibit exn 110722=============================================================*)
23.125
23.126 val str =
23.127 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.128 @@ -1189,107 +1092,8 @@
23.129 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.130 (*---^^^-OK-----------------------------------------------------------------*)
23.131 (*---vvv-NOT ok-------------------------------------------------------------*)
23.132 -val str =
23.133 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.134 -\ (let e1_ = hd es_; \
23.135 -\ v1_ = hd v_s; \
23.136 -\ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
23.137 -\ e2_ = Take (hd (tl es_)); \
23.138 -\ e2_ = (Substitute [e1__]) e2_ \
23.139 -\ in [e1_, e2_])";
23.140 -(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
23.141 -val str = "if lhs e1_ =!= v1_ then 1 else 2";
23.142 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.143
23.144 -val str = "let xxx = (if lhs e1_ =!= v1_ then 1 else 2) in xxx";
23.145 -(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
23.146 -atomty sc; term2str sc;
23.147
23.148 -"--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
23.149 -val str =
23.150 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.151 -\ (let e2__ = Take (hd (tl es_)); \
23.152 -\ e2__ = ((Substitute [e1__]) @@ \
23.153 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.154 -\ simplify_System_parenthesized False)) @@ \
23.155 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.156 -\ isolate_bdvs False)) @@ \
23.157 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.158 -\ simplify_System False))) e2__;\
23.159 -\ es__ = Take [e1__, e2__] \
23.160 -\ in (Try (Rewrite_Set order_system False)) es__)"
23.161 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.162 -val str =
23.163 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.164 -\ (let e2__ = Take (nth_ 2 es_); \
23.165 -\ e2__ = ((Substitute [e1__]) @@ \
23.166 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.167 -\ simplify_System_parenthesized False)) @@ \
23.168 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.169 -\ isolate_bdvs False)) @@ \
23.170 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
23.171 -\ simplify_System False))) e2__;\
23.172 -\ es__ = Take [e1__, e2__] \
23.173 -\ in (Try (Rewrite_Set order_system False)) es__)"
23.174 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.175 -val str =
23.176 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.177 -\ (let e2__ = Take (nth_ 2 es_); \
23.178 -\ e2__ = ((Substitute [e1__]) @@ \
23.179 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
23.180 -\ simplify_System_parenthesized False)) @@ \
23.181 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
23.182 -\ isolate_bdvs False)) @@ \
23.183 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
23.184 -\ simplify_System False))) e2__;\
23.185 -\ es__ = Take [e1__, e2__] \
23.186 -\ in (Try (Rewrite_Set order_system False)) es__)"
23.187 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.188 -val str =
23.189 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.190 -\ (let e2__ = Take (nth_ 2 es_); \
23.191 -\ e2__ = ((Substitute [e1__]) @@ \
23.192 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
23.193 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
23.194 -\ simplify_System_parenthesized False)) @@ \
23.195 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
23.196 -\ isolate_bdvs False)) @@ \
23.197 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
23.198 -\ norm_Rational False))) e2__; \
23.199 -\ es__ = Take [e1__, e2__] \
23.200 -\ in [])"
23.201 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.202 -val str =
23.203 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.204 -\ (let e2_ = Take (nth_ 2 es_); \
23.205 -\ e2_ = ((Substitute [e1_]) @@ \
23.206 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
23.207 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
23.208 -\ simplify_System_parenthesized False)) @@ \
23.209 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
23.210 -\ isolate_bdvs False)) @@ \
23.211 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
23.212 -\ norm_Rational False))) e2_; \
23.213 -\ es_ = Take [e1_, e2_] \
23.214 -\ in [e1_, e2_,e3_, e4_])"
23.215 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.216 -val str =
23.217 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.218 -\ (let e2_ = Take (nth_ 2 es_); \
23.219 -\ e2_ = ((Substitute [e1_]) @@ \
23.220 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
23.221 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
23.222 -\ simplify_System_parenthesized False)) @@ \
23.223 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
23.224 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
23.225 -\ isolate_bdvs False)) @@ \
23.226 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
23.227 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
23.228 -\ norm_Rational False))) e2_; \
23.229 -\ es_ = Take [e1_, e2_] \
23.230 -\ in [e1_, e2_,e3_, e4_])"
23.231 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
23.232 -(*---^^^-OK-----------------------------------------------------------------*)
23.233 val str =
23.234 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
23.235 \ (let e2_ = Take (nth_ 2 es_); \
23.236 @@ -1455,3 +1259,4 @@
23.237 use"eqsystem.sml";
23.238 *)
23.239 ===== inhibit exn 110722===========================================================*)
23.240 +