1.1 --- a/src/Tools/isac/Knowledge/Atools.thy Mon Jul 25 08:32:32 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
8.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
9.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
13.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Jul 26 13:27:59 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 Mon Jul 25 08:32:32 2011 +0200
19.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Jul 26 13:27:59 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/biegelinie.sml Mon Jul 25 08:32:32 2011 +0200
20.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Tue Jul 26 13:27:59 2011 +0200
20.3 @@ -602,63 +602,7 @@
20.4 \ in (equs_::bool list))"
20.5 ;
20.6 (*=== inhibit exn 110722=============================================================
20.7 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.8 -val str =
20.9 -"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
20.10 -\ (let b1_ = Take (nth_ 1 beds_); \
20.11 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
20.12 -\ f1_ = hd fs_ \
20.13 -\ in (equs_::bool list))"
20.14 -;
20.15 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.16
20.17 -val ttt = str2term "sameFunId (lhs b1_) fun___"; atomty ttt;
20.18 -val ttt = str2term "filter"; atomty ttt;
20.19 -val ttt = str2term "filter::[real => bool, real list] => real list";atomty ttt;
20.20 -val ttt = str2term "filter::[bool => bool, bool list] => bool list";
20.21 -val ttt = str2term "filter (sameFunId (lhs b1_)) funs_"; atomty ttt;
20.22 -
20.23 -val str =
20.24 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
20.25 -\ (let beds_ = rev beds_; \
20.26 -\ b1_ = Take (nth_ 1 beds_); \
20.27 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
20.28 -\ f1_ = hd fs_ \
20.29 -\ in (equs_::bool list))"
20.30 -;
20.31 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.32 -val str =
20.33 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
20.34 -\ (let b1_ = Take (nth_ 1 rb_); \
20.35 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
20.36 -\ (equ_::bool) = \
20.37 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
20.38 -\ [Equation,fromFunction]) \
20.39 -\ [BOOL (hd fs_), BOOL b1_]) \
20.40 -\ in [equ_])"
20.41 -;
20.42 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.43 -val str =
20.44 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
20.45 -\ (let b1_ = Take (nth_ 1 rb_); \
20.46 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
20.47 -\ (e1_::bool) = \
20.48 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
20.49 -\ [Equation,fromFunction]) \
20.50 -\ [BOOL (hd fs_), BOOL b1_]); \
20.51 -\ b2_ = Take (nth_ 2 rb_); \
20.52 -\ fs_ = filter (sameFunId (lhs b2_)) funs_; \
20.53 -\ (e2_::bool) = \
20.54 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
20.55 -\ [Equation,fromFunction]) \
20.56 -\ [BOOL (hd fs_), BOOL b2_]) \
20.57 -\ in [e1_,e1_])"
20.58 -;
20.59 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.60 -
20.61 -atomty sc;
20.62 -
20.63 -"----- execute script by manual rewriting";
20.64 (*show_types := true;*)
20.65 val funs_ = str2term "funs_::bool list";
20.66 val funs = str2term
21.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Jul 25 08:32:32 2011 +0200
21.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue Jul 26 13:27:59 2011 +0200
21.3 @@ -166,17 +166,17 @@
21.4 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
21.5
21.6 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
21.7 -if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"
21.8 -then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
21.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";
21.10
21.11 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
21.12 if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"
21.13 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
21.14
21.15 +"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...";
21.16 val SOME (t,_) = rewrite_set_ thy true order_system t;
21.17 if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"
21.18 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
21.19 -
21.20 +"--- 4---";
21.21
21.22 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
21.23 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
21.24 @@ -547,103 +547,6 @@
21.25 \ e1__1 = hd es__e\
21.26 \ in ([]))"
21.27 ;
21.28 -(*=== inhibit exn 110722=============================================================
21.29 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.30 -val str =
21.31 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.32 -\ (let es__ = Take es_; \
21.33 -\ e1__ = hd es__; \
21.34 -\ e2__ = hd (tl es__)\
21.35 -\ in ([]))"
21.36 -;
21.37 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.38 -val str =
21.39 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.40 -\ (let es__ = Take es_; \
21.41 -\ e1__ = hd es__; \
21.42 -\ e2__ = hd (tl es__);\
21.43 -\ es__ = [1=2,3=4]\
21.44 -\ in ([]))"
21.45 -;
21.46 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.47 -val str =
21.48 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.49 -\ (let es__ = Take es_; \
21.50 -\ e1__ = hd es__; \
21.51 -\ e2__ = hd (tl es__);\
21.52 -\ es__ = [e1__,e2__]\
21.53 -\ in ([]))"
21.54 -;
21.55 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.56 -val str =
21.57 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.58 -\ (let es__ = Take es_; \
21.59 -\ e1__ = hd es__; \
21.60 -\ e2__ = hd (tl es__);\
21.61 -\ es__ = [e1__, Substitute [e1__] e2__];\
21.62 -\ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.63 -\ simplify_System False)) es__ \
21.64 -\ in ([]))"
21.65 -;
21.66 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.67 -val str =
21.68 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.69 -\ (let es__ = Take es_; \
21.70 -\ e1__ = hd es__; \
21.71 -\ e2__ = hd (tl es__);\
21.72 -\ es__ = [e1__, Substitute [e1__] e2__];\
21.73 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.74 -\ isolate_bdvs False)) @@ \
21.75 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.76 -\ simplify_System False))) es__ \
21.77 -\ in ([]))"
21.78 -;
21.79 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.80 -val str =
21.81 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.82 -\ (let es__ = Take es_; \
21.83 -\ e1__ = hd es__; \
21.84 -\ e2__ = hd (tl es__);\
21.85 -\ es__ = [e1__, Substitute [e1__] e2__];\
21.86 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.87 -\ simplify_System_parenthesized False)) @@ \
21.88 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.89 -\ isolate_bdvs False)) @@ \
21.90 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.91 -\ simplify_System False))) es__ \
21.92 -\ in ([]))"
21.93 -;
21.94 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.95 -val str =
21.96 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.97 -\ (let es__ = Take es_; \
21.98 -\ e1__ = hd es__; \
21.99 -\ e2__ = hd (tl es__); \
21.100 -\ es__ = [e1__, Substitute [e1__] e2__]; \
21.101 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.102 -\ simplify_System_parenthesized False)) @@ \
21.103 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.104 -\ isolate_bdvs False)) @@ \
21.105 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.106 -\ simplify_System False))) es__ \
21.107 -\ in es__)"
21.108 -;
21.109 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.110 -val str =
21.111 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.112 -\ (let es__ = Take es_; \
21.113 -\ e1__ = hd es__; \
21.114 -\ e2__ = hd (tl es__); \
21.115 -\ es__ = [e1__, Substitute [e1__] e2__] \
21.116 -\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.117 -\ simplify_System_parenthesized False)) @@ \
21.118 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
21.119 -\ isolate_bdvs False)) @@ \
21.120 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.121 -\ simplify_System False))) es__)"
21.122 -;
21.123 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.124 -=== inhibit exn 110722=============================================================*)
21.125
21.126 val str =
21.127 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.128 @@ -1189,107 +1092,8 @@
21.129 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.130 (*---^^^-OK-----------------------------------------------------------------*)
21.131 (*---vvv-NOT ok-------------------------------------------------------------*)
21.132 -val str =
21.133 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.134 -\ (let e1_ = hd es_; \
21.135 -\ v1_ = hd v_s; \
21.136 -\ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
21.137 -\ e2_ = Take (hd (tl es_)); \
21.138 -\ e2_ = (Substitute [e1__]) e2_ \
21.139 -\ in [e1_, e2_])";
21.140 -(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
21.141 -val str = "if lhs e1_ =!= v1_ then 1 else 2";
21.142 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.143
21.144 -val str = "let xxx = (if lhs e1_ =!= v1_ then 1 else 2) in xxx";
21.145 -(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
21.146 -atomty sc; term2str sc;
21.147
21.148 -"--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
21.149 -val str =
21.150 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.151 -\ (let e2__ = Take (hd (tl es_)); \
21.152 -\ e2__ = ((Substitute [e1__]) @@ \
21.153 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.154 -\ simplify_System_parenthesized False)) @@ \
21.155 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.156 -\ isolate_bdvs False)) @@ \
21.157 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.158 -\ simplify_System False))) e2__;\
21.159 -\ es__ = Take [e1__, e2__] \
21.160 -\ in (Try (Rewrite_Set order_system False)) es__)"
21.161 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.162 -val str =
21.163 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.164 -\ (let e2__ = Take (nth_ 2 es_); \
21.165 -\ e2__ = ((Substitute [e1__]) @@ \
21.166 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.167 -\ simplify_System_parenthesized False)) @@ \
21.168 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.169 -\ isolate_bdvs False)) @@ \
21.170 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
21.171 -\ simplify_System False))) e2__;\
21.172 -\ es__ = Take [e1__, e2__] \
21.173 -\ in (Try (Rewrite_Set order_system False)) es__)"
21.174 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.175 -val str =
21.176 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.177 -\ (let e2__ = Take (nth_ 2 es_); \
21.178 -\ e2__ = ((Substitute [e1__]) @@ \
21.179 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
21.180 -\ simplify_System_parenthesized False)) @@ \
21.181 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
21.182 -\ isolate_bdvs False)) @@ \
21.183 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
21.184 -\ simplify_System False))) e2__;\
21.185 -\ es__ = Take [e1__, e2__] \
21.186 -\ in (Try (Rewrite_Set order_system False)) es__)"
21.187 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.188 -val str =
21.189 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.190 -\ (let e2__ = Take (nth_ 2 es_); \
21.191 -\ e2__ = ((Substitute [e1__]) @@ \
21.192 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
21.193 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
21.194 -\ simplify_System_parenthesized False)) @@ \
21.195 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
21.196 -\ isolate_bdvs False)) @@ \
21.197 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
21.198 -\ norm_Rational False))) e2__; \
21.199 -\ es__ = Take [e1__, e2__] \
21.200 -\ in [])"
21.201 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.202 -val str =
21.203 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.204 -\ (let e2_ = Take (nth_ 2 es_); \
21.205 -\ e2_ = ((Substitute [e1_]) @@ \
21.206 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
21.207 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
21.208 -\ simplify_System_parenthesized False)) @@ \
21.209 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
21.210 -\ isolate_bdvs False)) @@ \
21.211 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
21.212 -\ norm_Rational False))) e2_; \
21.213 -\ es_ = Take [e1_, e2_] \
21.214 -\ in [e1_, e2_,e3_, e4_])"
21.215 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.216 -val str =
21.217 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.218 -\ (let e2_ = Take (nth_ 2 es_); \
21.219 -\ e2_ = ((Substitute [e1_]) @@ \
21.220 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
21.221 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
21.222 -\ simplify_System_parenthesized False)) @@ \
21.223 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
21.224 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
21.225 -\ isolate_bdvs False)) @@ \
21.226 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
21.227 -\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
21.228 -\ norm_Rational False))) e2_; \
21.229 -\ es_ = Take [e1_, e2_] \
21.230 -\ in [e1_, e2_,e3_, e4_])"
21.231 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
21.232 -(*---^^^-OK-----------------------------------------------------------------*)
21.233 val str =
21.234 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
21.235 \ (let e2_ = Take (nth_ 2 es_); \
21.236 @@ -1455,3 +1259,4 @@
21.237 use"eqsystem.sml";
21.238 *)
21.239 ===== inhibit exn 110722===========================================================*)
21.240 +
22.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 25 08:32:32 2011 +0200
22.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 26 13:27:59 2011 +0200
22.3 @@ -7,545 +7,10 @@
22.4
22.5 ML{* writeln "**** run the test ***************************************" *}
22.6
22.7 -use"../../../test/Tools/isac/Interpret/script.sml"
22.8 +use"../../../test/Tools/isac/Knowledge/eqsystem.sml"
22.9
22.10 ML{*
22.11 -
22.12 -
22.13 -
22.14 -(* Title: tests on solve.sml
22.15 - Author: Walther Neuper 060508,
22.16 - (c) due to copyright terms
22.17 -
22.18 -is NOT ONLY dependent on Test, but on other thys:
22.19 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
22.20 -uses from Rational.ML: Rrls cancel_p, Rrls cancel
22.21 -which in turn
22.22 -uses from Poly.ML: Rls make_polynomial, Rls expand_binom
22.23 -
22.24 -use"../smltest/ME/solve.sml";
22.25 -use"solve.sml";
22.26 -*)
22.27 -
22.28 -"-----------------------------------------------------------------";
22.29 -"table of contents -----------------------------------------------";
22.30 -"-----------------------------------------------------------------";
22.31 -"--------- interSteps on norm_Rational ---------------------------";
22.32 -(*---vvv NOT working after meNEW.04mmdd*)
22.33 -"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
22.34 -"--------- prepare pbl, met --------------------------------------";
22.35 -"-------- cancel, without detail ------------------------------";
22.36 -"-------- cancel, detail rev-rew (cancel) afterwards ----------";
22.37 -"-------------- cancel_p, without detail ------------------------------";
22.38 -"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
22.39 -(*---^^^ NOT working*)
22.40 -"on 'miniscript with mini-subpbl':";
22.41 -"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
22.42 -"------ interSteps'detailrls' after CompleteCalc -----------------";
22.43 -"------ interSteps after appendFormula ---------------------------";
22.44 -(*---vvv not brought to work 0403*)
22.45 -"------ Detail_Set -----------------------------------------------";
22.46 -"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
22.47 -"-----------------------------------------------------------------";
22.48 -"-----------------------------------------------------------------";
22.49 -"-----------------------------------------------------------------";
22.50 -
22.51 -
22.52 -"--------- interSteps on norm_Rational ---------------------------";
22.53 -"--------- interSteps on norm_Rational ---------------------------";
22.54 -"--------- interSteps on norm_Rational ---------------------------";
22.55 - states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
22.56 - CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
22.57 - ("Rational",
22.58 - ["rational","simplification"],
22.59 - ["simplification","of_rationals"]))];
22.60 - moveActiveRoot 1;
22.61 - autoCalculate 1 CompleteCalc;
22.62 - val ((pt,_),_) = get_calc 1; show_pt pt;
22.63 -
22.64 -(*with "Script SimplifyScript (t_::real) = -----------------
22.65 - \ ((Rewrite_Set norm_Rational False) t_)"
22.66 -case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
22.67 - | _ => error "solve.sml: interSteps on norm_Rational 1";
22.68 -interSteps 1 ([1], Res);
22.69 -getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
22.70 -interSteps 1 ([1,3], Res);
22.71 -
22.72 -getTactic 1 ([1,4], Res) (*here get the tactic, and ...*);
22.73 -interSteps 1 ([1,5], Res) (*... here get the intermediate steps above*);
22.74 -
22.75 -getTactic 1 ([1,5,1], Frm);
22.76 -val ((pt,_),_) = get_calc 1; show_pt pt;
22.77 -
22.78 -getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);
22.79 -interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);
22.80 ---------------------------------------------------------------------*)
22.81 -
22.82 -case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
22.83 - | _ => error "solve.sml: interSteps on norm_Rational 1";
22.84 -(*these have been done now by the script ^^^ immediately...
22.85 -interSteps 1 ([1], Res);
22.86 -getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
22.87 -*)
22.88 -interSteps 1 ([6], Res);
22.89 -
22.90 -getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*);
22.91 -interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
22.92 -(*========== inhibit exn AK110721 ================================================
22.93 -
22.94 -getTactic 1 ([3,4,1], Frm);
22.95 -val ((pt,_),_) = get_calc 1; show_pt pt;
22.96 -val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));
22.97 -case (term2str form, tac, terms2strs asm) of
22.98 - ("1 / 2", Check_Postcond ["rational", "simplification"],
22.99 - ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()
22.100 - | _ => error "solve.sml: interSteps on norm_Rational 2";
22.101 -
22.102 -
22.103 -
22.104 -"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
22.105 -"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
22.106 -"###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
22.107 -val intermediate_ptyps = !ptyps;
22.108 -val intermediate_mets = !mets;
22.109 -
22.110 -"--------- prepare pbl, met --------------------------------------";
22.111 -"--------- prepare pbl, met --------------------------------------";
22.112 -"--------- prepare pbl, met --------------------------------------";
22.113 -store_pbt
22.114 - (prep_pbt Test.thy "pbl_ttestt" [] e_pblID
22.115 - (["test"],
22.116 - [],
22.117 - e_rls, NONE, []));
22.118 -store_pbt
22.119 - (prep_pbt Test.thy "pbl_ttestt_detail" [] e_pblID
22.120 - (["detail","test"],
22.121 - [("#Given" ,["realTestGiven t_"]),
22.122 - ("#Find" ,["realTestFind s_"])
22.123 - ],
22.124 - e_rls, NONE, [["Test","test_detail"]]));
22.125 -
22.126 -store_met
22.127 - (prep_met Test.thy "met_detbin" [] e_metID
22.128 - (["Test","test_detail_binom"]:metID,
22.129 - [("#Given" ,["realTestGiven t_"]),
22.130 - ("#Find" ,["realTestFind s_"])
22.131 - ],
22.132 - {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls,
22.133 - crls=tval_rls, nrls=e_rls(*,
22.134 - asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
22.135 - "Script Testterm (g_::real) = \
22.136 - \(((Rewrite_Set expand_binoms False) @@\
22.137 - \ (Rewrite_Set cancel False)) g_)"
22.138 - ));
22.139 -store_met
22.140 - (prep_met Test.thy "met_detpoly" [] e_metID
22.141 - (["Test","test_detail_poly"]:metID,
22.142 - [("#Given" ,["realTestGiven t_"]),
22.143 - ("#Find" ,["realTestFind s_"])
22.144 - ],
22.145 - {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
22.146 - crls=tval_rls, nrls=e_rls(*,
22.147 - asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
22.148 - "Script Testterm (g_::real) = \
22.149 - \(((Rewrite_Set make_polynomial False) @@\
22.150 - \ (Rewrite_Set cancel_p False)) g_)"
22.151 - ));
22.152 -
22.153 -(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
22.154 -
22.155 -"-------- cancel, without detail ------------------------------";
22.156 -"-------- cancel, without detail ------------------------------";
22.157 -"-------- cancel, without detail ------------------------------";
22.158 -val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",
22.159 - "realTestFind s"];
22.160 -val (dI',pI',mI') =
22.161 - ("Test",["detail","test"],["Test","test_detail_binom"]);
22.162 -
22.163 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.164 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.165 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.166 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.167 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.168 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.169 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.170 -(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
22.171 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.172 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.173 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.174 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.175 -(*"(3 + -1 * x) / (3 + x)"*)
22.176 -if nxt = ("End_Proof'",End_Proof') then ()
22.177 -else error "details.sml, changed behaviour in: without detail";
22.178 -
22.179 - val str = pr_ptree pr_short pt;
22.180 - writeln str;
22.181 -
22.182 -
22.183 -"-------- cancel, detail rev-rew (cancel) afterwards ----------";
22.184 -"-------- cancel, detail rev-rew (cancel) afterwards ----------";
22.185 -"-------- cancel, detail rev-rew (cancel) afterwards ----------";
22.186 - val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.187 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.188 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.189 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.190 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.191 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.192 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.193 - (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
22.194 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.195 - (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)
22.196 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
22.197 -(* val nxt = ("Detail",Detail);"----------------------";*)
22.198 -
22.199 -
22.200 -(*WN.11.9.03: after meNEW not yet implemented -------------------------*)
22.201 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.202 -(*FIXXXXXME.040216 #####################################################
22.203 -# val nxt = ("Detail", Detail) : string * tac
22.204 -val it = "----------------------" : string
22.205 -> val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.206 -val f = Form' (FormKF (~1, EdUndef, ...)) : mout
22.207 -val nxt = ("Empty_Tac", Empty_Tac) : string * tac
22.208 -val p = ([2, 1], Res) : pos'
22.209 -#########################################################################
22.210 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.211 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.212 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.213 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.214 - (*val nxt = ("End_Detail",End_Detail)*)
22.215 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.216 - (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)
22.217 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
22.218 - val nxt = ("Detail",Detail);"----------------------";
22.219 - val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
22.220 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.221 -(*15.10.02*)
22.222 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.223 -(*
22.224 -rewrite "Rationals" "tless_true""e_rls"true("sym_real_plus_minus_binom","")
22.225 - "3 ^^^ 2 - x ^^^ 2";
22.226 -*)
22.227 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.228 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.229 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.230 - val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
22.231 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.232 -if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))
22.233 - andalso nxt = ("End_Proof'",End_Proof') then ()
22.234 -else error "new behaviour in details.sml, \
22.235 - \cancel, rev-rew (cancel) afterwards";
22.236 -FIXXXXXME.040216 #####################################################*)
22.237 -
22.238 -(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
22.239 -
22.240 -"-------------- cancel_p, without detail ------------------------------";
22.241 -"-------------- cancel_p, without detail ------------------------------";
22.242 -"-------------- cancel_p, without detail ------------------------------";
22.243 -val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",
22.244 - "realTestFind s"];
22.245 -val (dI',pI',mI') =
22.246 - ("Test",["detail","test"],["Test","test_detail_poly"]);
22.247 -
22.248 -(*val p = e_pos'; val c = [];
22.249 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
22.250 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
22.251 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.252 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.253 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.254 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.255 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.256 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.257 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.258 -(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
22.259 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.260 -"(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
22.261 -
22.262 - (*14.3.03*)
22.263 -(*---------------WN060614?!?---
22.264 - val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
22.265 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
22.266 - "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)";
22.267 - val SOME (t,_) = rewrite_set_ thy false cancel_p t; term2str t;
22.268 - cancel_p_ thy t;
22.269 -(---------------WN060614?!?---*)
22.270 -
22.271 - val t = str2term "(3 + x) * (3 + -1 * x)";
22.272 - val SOME (t,_) = rewrite_set_ thy false expand_poly t; term2str t;
22.273 - "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";
22.274 - val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
22.275 - "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";
22.276 - val SOME (t,_) = rewrite_set_ thy false simplify_power t; term2str t;
22.277 - "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";
22.278 - val SOME (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;
22.279 - "9 + (0 * x + -1 * x ^^^ 2)";
22.280 - val SOME (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;
22.281 - "9 + - (x ^^^ 2)";
22.282 - (*14.3.03*)
22.283 -
22.284 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.285 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.286 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.287 -(*"(3 + -1 * x) / (3 + x)"*)
22.288 -if nxt = ("End_Proof'",End_Proof') then ()
22.289 -else error "details.sml, changed behaviour in: cancel_p, without detail";
22.290 -
22.291 -"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
22.292 -"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
22.293 -"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
22.294 -(* val p = e_pos'; val c = [];
22.295 - val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
22.296 - val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
22.297 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.298 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.299 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.300 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.301 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.302 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.303 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.304 - (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
22.305 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.306 - (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
22.307 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
22.308 -
22.309 -(*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:
22.310 - fun make_deriv ... Rls_ not yet impl. (| Thm | Calc)
22.311 - Rls_ needed for make_polynomial ----------------------
22.312 - val nxt = ("Detail",Detail);"----------------------";
22.313 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.314 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.315 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.316 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.317 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.318 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.319 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.320 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.321 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.322 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.323 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.324 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.325 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.326 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.327 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.328 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.329 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.330 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.331 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.332 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.333 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.334 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.335 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.336 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.337 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.338 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.339 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.340 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.341 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.342 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.343 - if nxt = ("End_Detail",End_Detail) then ()
22.344 - else error "details.sml: new behav. in Detail make_polynomial";
22.345 -----------------------------------------------------------------------*)
22.346 -
22.347 -(*---------------
22.348 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.349 - (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)
22.350 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
22.351 - val nxt = ("Detail",Detail);"----------------------";
22.352 - val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
22.353 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.354 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.355 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.356 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.357 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.358 - val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
22.359 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.360 -if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))
22.361 - andalso nxt = ("End_Proof'",End_Proof') then ()
22.362 -else error "new behaviour in details.sml, cancel_p afterwards";
22.363 -
22.364 -----------------*)
22.365 -
22.366 -
22.367 -
22.368 -
22.369 -
22.370 -val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",
22.371 - "realTestFind s"];
22.372 -val (dI',pI',mI') =
22.373 - ("Test",["detail","test"],["Test","test_detail_poly"]);
22.374 -
22.375 -(* val p = e_pos'; val c = [];
22.376 - val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
22.377 - val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
22.378 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.379 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.380 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.381 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.382 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.383 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.384 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.385 - (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
22.386 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.387 -(*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------
22.388 - (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
22.389 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
22.390 - val nxt = ("Detail",Detail);"----------------------";
22.391 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.392 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.393 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.394 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.395 --------------------------------------------------------------------------*)
22.396 -
22.397 -
22.398 -"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
22.399 -"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
22.400 -"------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
22.401 - states:=[];
22.402 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
22.403 - ("Test", ["sqroot-test","univariate","equation","test"],
22.404 - ["Test","squ-equ-test-subpbl1"]))];
22.405 - Iterator 1;
22.406 - moveActiveRoot 1;
22.407 - autoCalculate 1 CompleteCalc;
22.408 - moveActiveRoot 1;
22.409 -
22.410 - interSteps 1 ([],Res);
22.411 - val [(_,(((pt,_),_),[(_,ip)]))] = !states;
22.412 - val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
22.413 - (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3),(_,_,t4),(_,_,t5),(_,_,t6)] =>
22.414 - (writeln o terms2str) [t1,t2,t3,t4,t5,t6]
22.415 - | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([4], Res) then ()
22.416 - else error "details.sml: diff.behav. in interSteps'donesteps' 1";
22.417 -
22.418 - moveActiveDown 1;
22.419 - moveActiveDown 1;
22.420 - moveActiveDown 1;
22.421 - moveActiveDown 1;
22.422 -
22.423 - interSteps 1 ([3],Pbl) (*subproblem*);
22.424 - val [(_,(((pt,_),_),[(_,ip)]))] = !states;
22.425 - val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
22.426 - (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3)] =>
22.427 - (writeln o terms2str) [t1,t2,t3]
22.428 - | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([3, 2], Res) then ()
22.429 - else error "details.sml: diff.behav. in interSteps'donesteps' 1";
22.430 -
22.431 -
22.432 -(* val [(_,(((pt,_),_),[(_,ip)]))] = !states;
22.433 - writeln (pr_ptree pr_short pt);
22.434 - get_obj g_tac pt [4];
22.435 - *)
22.436 -
22.437 -
22.438 -"------ interSteps'detailrls' after CompleteCalc -----------------";
22.439 -"------ interSteps'detailrls' after CompleteCalc -----------------";
22.440 -"------ interSteps'detailrls' after CompleteCalc -----------------";
22.441 - states:=[];
22.442 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
22.443 - ("Test", ["sqroot-test","univariate","equation","test"],
22.444 - ["Test","squ-equ-test-subpbl1"]))];
22.445 - Iterator 1;
22.446 - moveActiveRoot 1;
22.447 - autoCalculate 1 CompleteCalc;
22.448 - interSteps 1 ([],Res);
22.449 - moveActiveRoot 1;
22.450 - moveActiveDown 1;
22.451 - moveActiveDown 1;
22.452 - moveActiveDown 1;
22.453 - refFormula 1 (get_pos 1 1); (* 2 Res, <ISA> -1 + x = 0 </ISA> *)
22.454 -
22.455 - interSteps 1 ([2],Res);
22.456 - val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
22.457 - if length (children (get_nd pt p)) = 6 then ()
22.458 - else error "details.sml: diff.behav. in interSteps'detailrls' 1";
22.459 -
22.460 - moveActiveDown 1;
22.461 - moveActiveDown 1; refFormula 1 (get_pos 1 1); (* 3,1 Frm, <ISA> -1 + x = 0 </ISA> *);
22.462 -
22.463 - interSteps 1 ([3,1],Frm) (*<ERROR> first formula on level has NO detail </E*);
22.464 - val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
22.465 - if length (children (get_nd pt p)) = 0 then () (*NO detail at ([xxx,1],Frm)*)
22.466 - else error "details.sml: diff.behav. in interSteps'detailrls' 2";
22.467 -
22.468 - moveActiveDown 1;
22.469 - refFormula 1 (get_pos 1 1); (* 3,1 Res, <ISA> x = 0 + -1 * -1 </ISA> *)
22.470 -
22.471 - interSteps 1 ([3,1],Res);
22.472 - val ((pt,p),_) = get_calc 1; show_pt pt;
22.473 - term2str (get_obj g_res pt [3,1,1]);(*"x = 0 + -1 * -1" ok*)
22.474 - term2str (get_obj g_form pt [3,2]); (*"x = 0 + -1 * -1" ok*)
22.475 - get_obj g_tac pt [3,1,1]; (*Rewrite_Inst.."risolate_bdv_add ok*)
22.476 -
22.477 - moveActiveDown 1;
22.478 - refFormula 1 (get_pos 1 1); (* 3,2 Res, <ISA> x = 1 </ISA> *)
22.479 -
22.480 - interSteps 1 ([3,2],Res);
22.481 - val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
22.482 - if length (children (get_nd pt p)) = 2 then ()
22.483 - else error "details.sml: diff.behav. in interSteps'detailrls' 3";
22.484 -
22.485 - val ((pt,p),_) = get_calc 1; show_pt pt;
22.486 -
22.487 -
22.488 -"------ interSteps after appendFormula ---------------------------";
22.489 -"------ interSteps after appendFormula ---------------------------";
22.490 -"------ interSteps after appendFormula ---------------------------";
22.491 -states:=[];
22.492 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
22.493 - ("Test", ["sqroot-test","univariate","equation","test"],
22.494 - ["Test","squ-equ-test-subpbl1"]))];
22.495 -Iterator 1;
22.496 -moveActiveRoot 1;
22.497 -autoCalculate 1 CompleteCalcHead;
22.498 -autoCalculate 1 (Step 1);
22.499 -autoCalculate 1 (Step 1);
22.500 -appendFormula 1 "x - 1 = 0"(*generates intermediate steps*);
22.501 -(*these are not shown, because the resulting formula is on the same
22.502 - level as the previous formula*)
22.503 -interSteps 1 ([2],Res) (*error: last unchanged was ([2, 9], Res)*);
22.504 -(*...and these are the internals*)
22.505 -val ((pt,p),_) = get_calc 1; show_pt pt;
22.506 -val (_,_,lastpos) =detailstep pt p;
22.507 -if p = ([2], Res) andalso lastpos = ([2, 9], Res) then ()
22.508 -else error "solve.sml: diff.beh. after appendFormula x - 1 = 0";
22.509 -
22.510 -
22.511 -"------ Detail_Set -----------------------------------------------";
22.512 -"------ Detail_Set -----------------------------------------------";
22.513 -"------ Detail_Set -----------------------------------------------";
22.514 - states:=[]; (*start of calculation, return No.1*)
22.515 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
22.516 - ("Test", ["sqroot-test","univariate","equation","test"],
22.517 - ["Test","squ-equ-test-subpbl1"]))];
22.518 - Iterator 1; moveActiveRoot 1;
22.519 - autoCalculate 1 CompleteCalcHead;
22.520 - autoCalculate 1 (Step 1);
22.521 - autoCalculate 1 (Step 1);
22.522 -
22.523 - fetchProposedTactic 1 (*DG decides to do this tactic in detail*);
22.524 - (*TODO ...*)
22.525 - setNextTactic 1 (Detail_Set "Test_simplify");
22.526 -
22.527 -
22.528 - val ((pt,p),tacis) = get_calc 1;
22.529 - val str = pr_ptree pr_short pt;
22.530 - writeln str;
22.531 -
22.532 - print_depth 3;
22.533 - term2str (fst (get_obj g_result pt [1]));
22.534 -
22.535 -
22.536 -
22.537 -
22.538 -"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
22.539 -"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
22.540 -"###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
22.541 -ptyps:= intermediate_ptyps;
22.542 -mets:= intermediate_mets;
22.543 -========== inhibit exn AK110721 ================================================*)
22.544 -
22.545 -
22.546 -
22.547 +order_system
22.548
22.549 *}
22.550 ML{*