1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Mon Sep 06 15:53:18 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Mon Sep 06 16:56:22 2010 +0200
1.3 @@ -57,19 +57,19 @@
1.4 bool list] => bool list"
1.5 ("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
1.6
1.7 -rules
1.8 +axioms
1.9
1.10 - Querkraft_Belastung "Q' x = -q_ x"
1.11 - Belastung_Querkraft "-q_ x = Q' x"
1.12 + Querkraft_Belastung: "Q' x = -q_ x"
1.13 + Belastung_Querkraft: "-q_ x = Q' x"
1.14
1.15 - Moment_Querkraft "M_b' x = Q x"
1.16 - Querkraft_Moment "Q x = M_b' x"
1.17 + Moment_Querkraft: "M_b' x = Q x"
1.18 + Querkraft_Moment: "Q x = M_b' x"
1.19
1.20 - Neigung_Moment "y'' x = -M_b x/ EI"
1.21 - Moment_Neigung "M_b x = -EI * y'' x"
1.22 + Neigung_Moment: "y'' x = -M_b x/ EI"
1.23 + Moment_Neigung: "M_b x = -EI * y'' x"
1.24
1.25 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
1.26 - make_fun_explicit "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
1.27 + make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
1.28
1.29 ML {*
1.30 val thy = @{theory};
2.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Sep 06 15:53:18 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Sep 06 16:56:22 2010 +0200
2.3 @@ -48,46 +48,46 @@
2.4
2.5 axioms (*stated as axioms, todo: prove as theorems
2.6 'bdv' is a constant on the meta-level *)
2.7 - diff_const "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
2.8 - diff_var "d_d bdv bdv = 1"
2.9 - diff_prod_const"[| Not (bdv occurs_in u) |] ==>
2.10 + diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
2.11 + diff_var: "d_d bdv bdv = 1"
2.12 + diff_prod_const:"[| Not (bdv occurs_in u) |] ==>
2.13 d_d bdv (u * v) = u * d_d bdv v"
2.14
2.15 - diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
2.16 - diff_dif "d_d bdv (u - v) = d_d bdv u - d_d bdv v"
2.17 - diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
2.18 - diff_quot "Not (v = 0) ==> (d_d bdv (u / v) =
2.19 + diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
2.20 + diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v"
2.21 + diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
2.22 + diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) =
2.23 (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
2.24
2.25 - diff_sin "d_d bdv (sin bdv) = cos bdv"
2.26 - diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
2.27 - diff_cos "d_d bdv (cos bdv) = - sin bdv"
2.28 - diff_cos_chain "d_d bdv (cos u) = - sin u * d_d bdv u"
2.29 - diff_pow "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
2.30 - diff_pow_chain "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u"
2.31 - diff_ln "d_d bdv (ln bdv) = 1 / bdv"
2.32 - diff_ln_chain "d_d bdv (ln u) = d_d bdv u / u"
2.33 - diff_exp "d_d bdv (exp bdv) = exp bdv"
2.34 - diff_exp_chain "d_d bdv (exp u) = exp u * d_d x u"
2.35 + diff_sin: "d_d bdv (sin bdv) = cos bdv"
2.36 + diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u"
2.37 + diff_cos: "d_d bdv (cos bdv) = - sin bdv"
2.38 + diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u"
2.39 + diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
2.40 + diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u"
2.41 + diff_ln: "d_d bdv (ln bdv) = 1 / bdv"
2.42 + diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u"
2.43 + diff_exp: "d_d bdv (exp bdv) = exp bdv"
2.44 + diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u"
2.45 (*
2.46 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
2.47 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
2.48 *)
2.49 (*...*)
2.50
2.51 - frac_conv "[| bdv occurs_in b; 0 < n |] ==>
2.52 + frac_conv: "[| bdv occurs_in b; 0 < n |] ==>
2.53 a / (b ^^^ n) = a * b ^^^ (-n)"
2.54 - frac_sym_conv "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
2.55 + frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
2.56
2.57 - sqrt_conv_bdv "sqrt bdv = bdv ^^^ (1 / 2)"
2.58 - sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
2.59 - sqrt_conv "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
2.60 - sqrt_sym_conv "u ^^^ (a / 2) = sqrt (u ^^^ a)"
2.61 + sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)"
2.62 + sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
2.63 + sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
2.64 + sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)"
2.65
2.66 - root_conv "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
2.67 - root_sym_conv "u ^^^ (a / b) = nroot b (u ^^^ a)"
2.68 + root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
2.69 + root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)"
2.70
2.71 - realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
2.72 + realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
2.73
2.74 ML {*
2.75 val thy = @{theory};
3.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Mon Sep 06 15:53:18 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Mon Sep 06 16:56:22 2010 +0200
3.3 @@ -28,7 +28,7 @@
3.4 (*for script Maximum_value*)
3.5 filterVar :: "[real, 'a list] => 'a list"
3.6
3.7 -(*primrec*)rules
3.8 +(*primrec*)axioms
3.9 filterVar_Nil "filterVar v [] = []"
3.10 filterVar_Const "filterVar v (x#xs) =
3.11 (if (v mem (Vars x)) then x#(filterVar v xs)
4.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Sep 06 15:53:18 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Sep 06 16:56:22 2010 +0200
4.3 @@ -28,32 +28,32 @@
4.4 'bdv' is a constant handled on the meta-level
4.5 specifically as a 'bound variable' *)
4.6
4.7 - commute_0_equality "(0 = a) = (a = 0)"
4.8 + commute_0_equality: "(0 = a) = (a = 0)"
4.9
4.10 (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL)
4.11 [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*)
4.12 - separate_bdvs_add
4.13 + separate_bdvs_add:
4.14 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]
4.15 ==> (a + b = c) = (b = c + -1*a)"
4.16 - separate_bdvs0
4.17 + separate_bdvs0:
4.18 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |]
4.19 ==> (a = b) = (a + -1*b = 0)"
4.20 - separate_bdvs_add1
4.21 + separate_bdvs_add1:
4.22 "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]
4.23 ==> (a = b + c) = (a + -1*c = b)"
4.24 - separate_bdvs_add2
4.25 + separate_bdvs_add2:
4.26 "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |]
4.27 ==> (a + b = c) = (b = -1*a + c)"
4.28
4.29
4.30
4.31 - separate_bdvs_mult
4.32 + separate_bdvs_mult:
4.33 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]
4.34 ==>(a * b = c) = (b = c / a)"
4.35
4.36 (*requires rew_ord for termination, eg. ord_simplify_Integral;
4.37 works for lists of any length, interestingly !?!*)
4.38 - order_system_NxN "[a,b] = [b,a]"
4.39 + order_system_NxN: "[a,b] = [b,a]"
4.40
4.41 ML {*
4.42 val thy = @{theory};
5.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Sep 06 15:53:18 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Sep 06 16:56:22 2010 +0200
5.3 @@ -31,18 +31,18 @@
5.4 'bdv' is a constant handled on the meta-level
5.5 specifically as a 'bound variable' *)
5.6
5.7 - integral_const "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
5.8 - integral_var "Integral bdv D bdv = bdv ^^^ 2 / 2"
5.9 + integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
5.10 + integral_var: "Integral bdv D bdv = bdv ^^^ 2 / 2"
5.11
5.12 - integral_add "Integral (u + v) D bdv =
5.13 + integral_add: "Integral (u + v) D bdv =
5.14 (Integral u D bdv) + (Integral v D bdv)"
5.15 - integral_mult "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>
5.16 + integral_mult: "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>
5.17 Integral (u * v) D bdv = u * (Integral v D bdv)"
5.18 (*WN080222: this goes into sub-terms, too ...
5.19 - call_for_new_c "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>
5.20 + call_for_new_c: "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>
5.21 a = a + new_c a"
5.22 *)
5.23 - integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
5.24 + integral_pow: "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
5.25
5.26 ML {*
5.27 val thy = @{theory};
6.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Mon Sep 06 15:53:18 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Mon Sep 06 16:56:22 2010 +0200
6.3 @@ -17,12 +17,12 @@
6.4 => bool list"
6.5 ("((Script Solve'_log (_ _=))//(_))" 9)
6.6
6.7 -rules
6.8 +axioms
6.9
6.10 - equality_pow "0 < a ==> (l = r) = (a^^^l = a^^^r)"
6.11 + equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)"
6.12 (* this is what students ^^^^^^^... are told to do *)
6.13 - equality_power "((a log b) = c) = (a^^^(a log b) = a^^^c)"
6.14 - exp_invers_log "a^^^(a log b) = b"
6.15 + equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)"
6.16 + exp_invers_log: "a^^^(a log b) = b"
6.17
6.18 ML {*
6.19 val thy = @{theory};
7.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 06 15:53:18 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 06 16:56:22 2010 +0200
7.3 @@ -80,240 +80,240 @@
7.4 (*-------------------- rules -------------------------------------------------*)
7.5 axioms
7.6
7.7 - cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) =
7.8 + cancel_leading_coeff1: "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) =
7.9 (a/c + b/c*bdv + bdv^^^2 = 0)"
7.10 - cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) =
7.11 + cancel_leading_coeff2: "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) =
7.12 (a/c - b/c*bdv + bdv^^^2 = 0)"
7.13 - cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) =
7.14 + cancel_leading_coeff3: "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) =
7.15 (a/c + b/c*bdv - bdv^^^2 = 0)"
7.16
7.17 - cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) =
7.18 + cancel_leading_coeff4: "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) =
7.19 (a/c + 1/c*bdv + bdv^^^2 = 0)"
7.20 - cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) =
7.21 + cancel_leading_coeff5: "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) =
7.22 (a/c - 1/c*bdv + bdv^^^2 = 0)"
7.23 - cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) =
7.24 + cancel_leading_coeff6: "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) =
7.25 (a/c + 1/c*bdv - bdv^^^2 = 0)"
7.26
7.27 - cancel_leading_coeff7 "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) =
7.28 + cancel_leading_coeff7: "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) =
7.29 ( b/c*bdv + bdv^^^2 = 0)"
7.30 - cancel_leading_coeff8 "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) =
7.31 + cancel_leading_coeff8: "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) =
7.32 ( b/c*bdv - bdv^^^2 = 0)"
7.33
7.34 - cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) =
7.35 + cancel_leading_coeff9: "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) =
7.36 ( 1/c*bdv + bdv^^^2 = 0)"
7.37 - cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) =
7.38 + cancel_leading_coeff10:"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) =
7.39 ( 1/c*bdv - bdv^^^2 = 0)"
7.40
7.41 - cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) =
7.42 + cancel_leading_coeff11:"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) =
7.43 (a/b + bdv^^^2 = 0)"
7.44 - cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) =
7.45 + cancel_leading_coeff12:"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) =
7.46 (a/b - bdv^^^2 = 0)"
7.47 - cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) =
7.48 + cancel_leading_coeff13:"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) =
7.49 ( bdv^^^2 = 0/b)"
7.50
7.51 - complete_square1 "(q + p*bdv + bdv^^^2 = 0) =
7.52 + complete_square1: "(q + p*bdv + bdv^^^2 = 0) =
7.53 (q + (p/2 + bdv)^^^2 = (p/2)^^^2)"
7.54 - complete_square2 "( p*bdv + bdv^^^2 = 0) =
7.55 + complete_square2: "( p*bdv + bdv^^^2 = 0) =
7.56 ( (p/2 + bdv)^^^2 = (p/2)^^^2)"
7.57 - complete_square3 "( bdv + bdv^^^2 = 0) =
7.58 + complete_square3: "( bdv + bdv^^^2 = 0) =
7.59 ( (1/2 + bdv)^^^2 = (1/2)^^^2)"
7.60
7.61 - complete_square4 "(q - p*bdv + bdv^^^2 = 0) =
7.62 + complete_square4: "(q - p*bdv + bdv^^^2 = 0) =
7.63 (q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
7.64 - complete_square5 "(q + p*bdv - bdv^^^2 = 0) =
7.65 + complete_square5: "(q + p*bdv - bdv^^^2 = 0) =
7.66 (q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
7.67
7.68 - square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)"
7.69 - square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
7.70 + square_explicit1: "(a + b^^^2 = c) = ( b^^^2 = c - a)"
7.71 + square_explicit2: "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
7.72
7.73 - bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)"
7.74 - bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)"
7.75 - bdv_explicit3 "((-1)*bdv = b) = (bdv = (-1)*b)"
7.76 + bdv_explicit1: "(a + bdv = b) = (bdv = - a + b)"
7.77 + bdv_explicit2: "(a - bdv = b) = ((-1)*bdv = - a + b)"
7.78 + bdv_explicit3: "((-1)*bdv = b) = (bdv = (-1)*b)"
7.79
7.80 - plus_leq "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)
7.81 - minus_leq "(0 <= a - b) = ( b <= a)"(*Isa?*)
7.82 + plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)
7.83 + minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*)
7.84
7.85 (*-- normalize --*)
7.86 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
7.87 - all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"
7.88 - makex1_x "a^^^1 = a"
7.89 - real_assoc_1 "a+(b+c) = a+b+c"
7.90 - real_assoc_2 "a*(b*c) = a*b*c"
7.91 + all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"
7.92 + makex1_x: "a^^^1 = a"
7.93 + real_assoc_1: "a+(b+c) = a+b+c"
7.94 + real_assoc_2: "a*(b*c) = a*b*c"
7.95
7.96 (* ---- degree 0 ----*)
7.97 - d0_true "(0=0) = True"
7.98 - d0_false "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False"
7.99 + d0_true: "(0=0) = True"
7.100 + d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False"
7.101 (* ---- degree 1 ----*)
7.102 - d1_isolate_add1
7.103 + d1_isolate_add1:
7.104 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)"
7.105 - d1_isolate_add2
7.106 + d1_isolate_add2:
7.107 "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)"
7.108 - d1_isolate_div
7.109 + d1_isolate_div:
7.110 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)"
7.111 (* ---- degree 2 ----*)
7.112 - d2_isolate_add1
7.113 + d2_isolate_add1:
7.114 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)"
7.115 - d2_isolate_add2
7.116 + d2_isolate_add2:
7.117 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)"
7.118 - d2_isolate_div
7.119 + d2_isolate_div:
7.120 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)"
7.121
7.122 - d2_prescind1 "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"
7.123 - d2_prescind2 "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)"
7.124 - d2_prescind3 "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"
7.125 - d2_prescind4 "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)"
7.126 + d2_prescind1: "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"
7.127 + d2_prescind2: "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)"
7.128 + d2_prescind3: "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"
7.129 + d2_prescind4: "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)"
7.130 (* eliminate degree 2 *)
7.131 (* thm for neg arguments in sqroot have postfix _neg *)
7.132 - d2_sqrt_equation1 "[|(0<=c);Not(bdv occurs_in c)|] ==>
7.133 + d2_sqrt_equation1: "[|(0<=c);Not(bdv occurs_in c)|] ==>
7.134 (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))"
7.135 - d2_sqrt_equation1_neg
7.136 + d2_sqrt_equation1_neg:
7.137 "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False"
7.138 - d2_sqrt_equation2 "(bdv^^^2=0) = (bdv=0)"
7.139 - d2_sqrt_equation3 "(b*bdv^^^2=0) = (bdv=0)"
7.140 - d2_reduce_equation1 "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
7.141 - d2_reduce_equation2 "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
7.142 - d2_pqformula1 "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
7.143 + d2_sqrt_equation2: "(bdv^^^2=0) = (bdv=0)"
7.144 + d2_sqrt_equation3: "(b*bdv^^^2=0) = (bdv=0)"
7.145 + d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
7.146 + d2_reduce_equation2: "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
7.147 + d2_pqformula1: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
7.148 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
7.149 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
7.150 - d2_pqformula1_neg "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False"
7.151 - d2_pqformula2 "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
7.152 + d2_pqformula1_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False"
7.153 + d2_pqformula2: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
7.154 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
7.155 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
7.156 - d2_pqformula2_neg "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False"
7.157 - d2_pqformula3 "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
7.158 + d2_pqformula2_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False"
7.159 + d2_pqformula3: "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
7.160 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
7.161 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
7.162 - d2_pqformula3_neg "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False"
7.163 - d2_pqformula4 "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
7.164 + d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False"
7.165 + d2_pqformula4: "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
7.166 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
7.167 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
7.168 - d2_pqformula4_neg "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False"
7.169 - d2_pqformula5 "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
7.170 + d2_pqformula4_neg: "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False"
7.171 + d2_pqformula5: "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
7.172 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
7.173 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
7.174 (* d2_pqformula5_neg not need p^2 never less zero in R *)
7.175 - d2_pqformula6 "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
7.176 + d2_pqformula6: "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
7.177 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
7.178 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
7.179 (* d2_pqformula6_neg not need p^2 never less zero in R *)
7.180 - d2_pqformula7 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
7.181 + d2_pqformula7: "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
7.182 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
7.183 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
7.184 (* d2_pqformula7_neg not need, because 1<0 ==> False*)
7.185 - d2_pqformula8 "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) =
7.186 + d2_pqformula8: "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) =
7.187 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
7.188 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
7.189 (* d2_pqformula8_neg not need, because 1<0 ==> False*)
7.190 - d2_pqformula9 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==>
7.191 + d2_pqformula9: "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==>
7.192 (q+ 1*bdv^^^2=0) = ((bdv= 0 + sqrt(0 - 4*q)/2)
7.193 | (bdv= 0 - sqrt(0 - 4*q)/2))"
7.194 - d2_pqformula9_neg
7.195 + d2_pqformula9_neg:
7.196 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False"
7.197 - d2_pqformula10
7.198 + d2_pqformula10:
7.199 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) =
7.200 ((bdv= 0 + sqrt(0 - 4*q)/2)
7.201 | (bdv= 0 - sqrt(0 - 4*q)/2))"
7.202 - d2_pqformula10_neg
7.203 + d2_pqformula10_neg:
7.204 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False"
7.205 - d2_abcformula1
7.206 + d2_abcformula1:
7.207 "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
7.208 ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a))
7.209 | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))"
7.210 - d2_abcformula1_neg
7.211 + d2_abcformula1_neg:
7.212 "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False"
7.213 - d2_abcformula2
7.214 + d2_abcformula2:
7.215 "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) =
7.216 ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
7.217 | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))"
7.218 - d2_abcformula2_neg
7.219 + d2_abcformula2_neg:
7.220 "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False"
7.221 - d2_abcformula3
7.222 + d2_abcformula3:
7.223 "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) =
7.224 ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1))
7.225 | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))"
7.226 - d2_abcformula3_neg
7.227 + d2_abcformula3_neg:
7.228 "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False"
7.229 - d2_abcformula4
7.230 + d2_abcformula4:
7.231 "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) =
7.232 ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1))
7.233 | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))"
7.234 - d2_abcformula4_neg
7.235 + d2_abcformula4_neg:
7.236 "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False"
7.237 - d2_abcformula5
7.238 + d2_abcformula5:
7.239 "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) =
7.240 ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
7.241 | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))"
7.242 - d2_abcformula5_neg
7.243 + d2_abcformula5_neg:
7.244 "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False"
7.245 - d2_abcformula6
7.246 + d2_abcformula6:
7.247 "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) =
7.248 ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
7.249 | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))"
7.250 - d2_abcformula6_neg
7.251 + d2_abcformula6_neg:
7.252 "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False"
7.253 - d2_abcformula7
7.254 + d2_abcformula7:
7.255 "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) =
7.256 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
7.257 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"
7.258 (* d2_abcformula7_neg not need b^2 never less zero in R *)
7.259 - d2_abcformula8
7.260 + d2_abcformula8:
7.261 "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) =
7.262 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
7.263 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"
7.264 (* d2_abcformula8_neg not need b^2 never less zero in R *)
7.265 - d2_abcformula9
7.266 + d2_abcformula9:
7.267 "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) =
7.268 ((bdv=( -1 + sqrt(1 - 0))/(2*a))
7.269 | (bdv=( -1 - sqrt(1 - 0))/(2*a)))"
7.270 (* d2_abcformula9_neg not need, because 1<0 ==> False*)
7.271 - d2_abcformula10
7.272 + d2_abcformula10:
7.273 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
7.274 ((bdv=( -1 + sqrt(1 - 0))/(2*1))
7.275 | (bdv=( -1 - sqrt(1 - 0))/(2*1)))"
7.276 (* d2_abcformula10_neg not need, because 1<0 ==> False*)
7.277
7.278 (* ---- degree 3 ----*)
7.279 - d3_reduce_equation1
7.280 + d3_reduce_equation1:
7.281 "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))"
7.282 - d3_reduce_equation2
7.283 + d3_reduce_equation2:
7.284 "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))"
7.285 - d3_reduce_equation3
7.286 + d3_reduce_equation3:
7.287 "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))"
7.288 - d3_reduce_equation4
7.289 + d3_reduce_equation4:
7.290 "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))"
7.291 - d3_reduce_equation5
7.292 + d3_reduce_equation5:
7.293 "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))"
7.294 - d3_reduce_equation6
7.295 + d3_reduce_equation6:
7.296 "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))"
7.297 - d3_reduce_equation7
7.298 + d3_reduce_equation7:
7.299 "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
7.300 - d3_reduce_equation8
7.301 + d3_reduce_equation8:
7.302 "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
7.303 - d3_reduce_equation9
7.304 + d3_reduce_equation9:
7.305 "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))"
7.306 - d3_reduce_equation10
7.307 + d3_reduce_equation10:
7.308 "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))"
7.309 - d3_reduce_equation11
7.310 + d3_reduce_equation11:
7.311 "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))"
7.312 - d3_reduce_equation12
7.313 + d3_reduce_equation12:
7.314 "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))"
7.315 - d3_reduce_equation13
7.316 + d3_reduce_equation13:
7.317 "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))"
7.318 - d3_reduce_equation14
7.319 + d3_reduce_equation14:
7.320 "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))"
7.321 - d3_reduce_equation15
7.322 + d3_reduce_equation15:
7.323 "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))"
7.324 - d3_reduce_equation16
7.325 + d3_reduce_equation16:
7.326 "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))"
7.327 - d3_isolate_add1
7.328 + d3_isolate_add1:
7.329 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)"
7.330 - d3_isolate_add2
7.331 + d3_isolate_add2:
7.332 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)"
7.333 - d3_isolate_div
7.334 + d3_isolate_div:
7.335 "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"
7.336 - d3_root_equation2
7.337 + d3_root_equation2:
7.338 "(bdv^^^3=0) = (bdv=0)"
7.339 - d3_root_equation1
7.340 + d3_root_equation1:
7.341 "(bdv^^^3=c) = (bdv = nroot 3 c)"
7.342
7.343 (* ---- degree 4 ----*)
7.344 @@ -324,42 +324,42 @@
7.345
7.346 (* ---- 7.3.02 von Termorder ---- *)
7.347
7.348 - bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv"
7.349 - bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv"
7.350 - bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv"
7.351 + bdv_collect_1: "l * bdv + m * bdv = (l + m) * bdv"
7.352 + bdv_collect_2: "bdv + m * bdv = (1 + m) * bdv"
7.353 + bdv_collect_3: "l * bdv + bdv = (l + 1) * bdv"
7.354
7.355 (* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
7.356 bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
7.357 bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
7.358 *)
7.359 - bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k"
7.360 - bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k"
7.361 - bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k"
7.362 + bdv_collect_assoc1_1:"l * bdv + (m * bdv + k) = (l + m) * bdv + k"
7.363 + bdv_collect_assoc1_2:"bdv + (m * bdv + k) = (1 + m) * bdv + k"
7.364 + bdv_collect_assoc1_3:"l * bdv + (bdv + k) = (l + 1) * bdv + k"
7.365
7.366 - bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv"
7.367 - bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv"
7.368 - bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv"
7.369 + bdv_collect_assoc2_1:"k + l * bdv + m * bdv = k + (l + m) * bdv"
7.370 + bdv_collect_assoc2_2:"k + bdv + m * bdv = k + (1 + m) * bdv"
7.371 + bdv_collect_assoc2_3:"k + l * bdv + bdv = k + (l + 1) * bdv"
7.372
7.373
7.374 - bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
7.375 - bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
7.376 - bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*)
7.377 + bdv_n_collect_1: "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
7.378 + bdv_n_collect_2: " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
7.379 + bdv_n_collect_3: "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*)
7.380
7.381 - bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
7.382 - bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
7.383 - bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
7.384 + bdv_n_collect_assoc1_1:"l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
7.385 + bdv_n_collect_assoc1_2:"bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
7.386 + bdv_n_collect_assoc1_3:"l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
7.387
7.388 - bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"
7.389 - bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
7.390 - bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
7.391 + bdv_n_collect_assoc2_1:"k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"
7.392 + bdv_n_collect_assoc2_2:"k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
7.393 + bdv_n_collect_assoc2_3:"k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
7.394
7.395 (*WN.14.3.03*)
7.396 - real_minus_div "- (a / b) = (-1 * a) / b"
7.397 + real_minus_div: "- (a / b) = (-1 * a) / b"
7.398
7.399 - separate_bdv "(a * bdv) / b = (a / b) * bdv"
7.400 - separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
7.401 - separate_1_bdv "bdv / b = (1 / b) * bdv"
7.402 - separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
7.403 + separate_bdv: "(a * bdv) / b = (a / b) * bdv"
7.404 + separate_bdv_n: "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
7.405 + separate_1_bdv: "bdv / b = (1 / b) * bdv"
7.406 + separate_1_bdv_n: "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
7.407
7.408 ML {*
7.409 val thy = @{theory};
8.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Mon Sep 06 15:53:18 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Mon Sep 06 16:56:22 2010 +0200
8.3 @@ -24,28 +24,22 @@
8.4 (* FIXME also in Poly.thy def. --> FIXED*)
8.5 (*real_diff_minus
8.6 "a - b = a + (-1) * b"*)
8.7 - real_rat_mult_1
8.8 - "a*(b/c) = (a*b)/c"
8.9 - real_rat_mult_2
8.10 - "(a/b)*(c/d) = (a*c)/(b*d)"
8.11 - real_rat_mult_3
8.12 - "(a/b)*c = (a*c)/b"
8.13 - real_rat_pow
8.14 - "(a/b)^^^2 = a^^^2/b^^^2"
8.15 + real_rat_mult_1: "a*(b/c) = (a*b)/c"
8.16 + real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)"
8.17 + real_rat_mult_3: "(a/b)*c = (a*c)/b"
8.18 + real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2"
8.19
8.20 - rat_double_rat_1
8.21 - "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
8.22 - rat_double_rat_2
8.23 - "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))"
8.24 - rat_double_rat_3
8.25 - "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
8.26 + rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
8.27 + rat_double_rat_2: "[|Not(b=0);Not(c=0); Not(d=0)|] ==>
8.28 + ((a/b) / (c/d) = (a*d) / (b*c))"
8.29 + rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
8.30
8.31 (* equation to same denominator *)
8.32 - rat_mult_denominator_both
8.33 + rat_mult_denominator_both:
8.34 "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"
8.35 - rat_mult_denominator_left
8.36 + rat_mult_denominator_left:
8.37 "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
8.38 - rat_mult_denominator_right
8.39 + rat_mult_denominator_right:
8.40 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
8.41
8.42 ML {*
9.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 06 15:53:18 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 06 16:56:22 2010 +0200
9.3 @@ -40,81 +40,81 @@
9.4 axioms
9.5
9.6 (* normalize *)
9.7 - makex1_x "a^^^1 = a"
9.8 - real_assoc_1 "a+(b+c) = a+b+c"
9.9 - real_assoc_2 "a*(b*c) = a*b*c"
9.10 + makex1_x: "a^^^1 = a"
9.11 + real_assoc_1: "a+(b+c) = a+b+c"
9.12 + real_assoc_2: "a*(b*c) = a*b*c"
9.13
9.14 (* simplification of root*)
9.15 - sqrt_square_1 "[|0 <= a|] ==> (sqrt a)^^^2 = a"
9.16 - sqrt_square_2 "sqrt (a ^^^ 2) = a"
9.17 - sqrt_times_root_1 "sqrt a * sqrt b = sqrt(a*b)"
9.18 - sqrt_times_root_2 "a * sqrt b * sqrt c = a * sqrt(b*c)"
9.19 + sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a"
9.20 + sqrt_square_2: "sqrt (a ^^^ 2) = a"
9.21 + sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)"
9.22 + sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)"
9.23
9.24 (* isolate one root on the LEFT or RIGHT hand side of the equation *)
9.25 - sqrt_isolate_l_add1 "[|bdv occurs_in c|] ==>
9.26 + sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==>
9.27 (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
9.28 - sqrt_isolate_l_add2 "[|bdv occurs_in c|] ==>
9.29 + sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==>
9.30 (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
9.31 - sqrt_isolate_l_add3 "[|bdv occurs_in c|] ==>
9.32 + sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==>
9.33 (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)"
9.34 - sqrt_isolate_l_add4 "[|bdv occurs_in c|] ==>
9.35 + sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==>
9.36 (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)"
9.37 - sqrt_isolate_l_add5 "[|bdv occurs_in c|] ==>
9.38 + sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==>
9.39 (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
9.40 - sqrt_isolate_l_add6 "[|bdv occurs_in c|] ==>
9.41 + sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==>
9.42 (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
9.43 - sqrt_isolate_r_add1 "[|bdv occurs_in f|] ==>
9.44 + sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==>
9.45 (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
9.46 - sqrt_isolate_r_add2 "[|bdv occurs_in f|] ==>
9.47 + sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>
9.48 (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
9.49 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
9.50 - sqrt_isolate_r_add3 "[|bdv occurs_in f|] ==>
9.51 + sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>
9.52 (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
9.53 - sqrt_isolate_r_add4 "[|bdv occurs_in f|] ==>
9.54 + sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>
9.55 (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
9.56 - sqrt_isolate_r_add5 "[|bdv occurs_in f|] ==>
9.57 + sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==>
9.58 (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
9.59 - sqrt_isolate_r_add6 "[|bdv occurs_in f|] ==>
9.60 + sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==>
9.61 (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
9.62
9.63 (* eliminate isolates sqrt *)
9.64 - sqrt_square_equation_both_1 "[|bdv occurs_in b; bdv occurs_in d|] ==>
9.65 + sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==>
9.66 ( (sqrt a + sqrt b = sqrt c + sqrt d) =
9.67 (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
9.68 - sqrt_square_equation_both_2 "[|bdv occurs_in b; bdv occurs_in d|] ==>
9.69 + sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==>
9.70 ( (sqrt a - sqrt b = sqrt c + sqrt d) =
9.71 (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
9.72 - sqrt_square_equation_both_3 "[|bdv occurs_in b; bdv occurs_in d|] ==>
9.73 + sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==>
9.74 ( (sqrt a + sqrt b = sqrt c - sqrt d) =
9.75 (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
9.76 - sqrt_square_equation_both_4 "[|bdv occurs_in b; bdv occurs_in d|] ==>
9.77 + sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==>
9.78 ( (sqrt a - sqrt b = sqrt c - sqrt d) =
9.79 (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
9.80 - sqrt_square_equation_left_1 "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
9.81 + sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
9.82 ( (sqrt (a) = b) = (a = (b^^^2)))"
9.83 - sqrt_square_equation_left_2 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
9.84 + sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
9.85 ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
9.86 - sqrt_square_equation_left_3 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
9.87 + sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
9.88 ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
9.89 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
9.90 - sqrt_square_equation_left_4 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
9.91 + sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
9.92 ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
9.93 - sqrt_square_equation_left_5 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
9.94 + sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
9.95 ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
9.96 - sqrt_square_equation_left_6 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
9.97 + sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
9.98 ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"
9.99 - sqrt_square_equation_right_1 "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
9.100 + sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
9.101 ( (a = sqrt (b)) = (a^^^2 = b))"
9.102 - sqrt_square_equation_right_2 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
9.103 + sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
9.104 ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
9.105 - sqrt_square_equation_right_3 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
9.106 + sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
9.107 ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
9.108 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
9.109 - sqrt_square_equation_right_4 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
9.110 + sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
9.111 ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
9.112 - sqrt_square_equation_right_5 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
9.113 + sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
9.114 ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
9.115 - sqrt_square_equation_right_6 "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
9.116 + sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
9.117 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
9.118
9.119 ML {*
10.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Mon Sep 06 15:53:18 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Sep 06 16:56:22 2010 +0200
10.3 @@ -24,13 +24,13 @@
10.4
10.5 axioms
10.6 (* eliminate ratRootTerm *)
10.7 - rootrat_equation_left_1
10.8 + rootrat_equation_left_1:
10.9 "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
10.10 - rootrat_equation_left_2
10.11 + rootrat_equation_left_2:
10.12 "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
10.13 - rootrat_equation_right_2
10.14 + rootrat_equation_right_2:
10.15 "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
10.16 - rootrat_equation_right_1
10.17 + rootrat_equation_right_1:
10.18 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
10.19
10.20 ML {*
11.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Sep 06 15:53:18 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Sep 06 16:56:22 2010 +0200
11.3 @@ -60,108 +60,108 @@
11.4
11.5 axioms (*TODO: prove as theorems*)
11.6
11.7 - radd_mult_distrib2 "(k::real) * (m + n) = k * m + k * n"
11.8 - rdistr_right_assoc "(k::real) + l * n + m * n = k + (l + m) * n"
11.9 - rdistr_right_assoc_p "l * n + (m * n + (k::real)) = (l + m) * n + k"
11.10 - rdistr_div_right "((k::real) + l) / n = k / n + l / n"
11.11 - rcollect_right
11.12 + radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n"
11.13 + rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n"
11.14 + rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k"
11.15 + rdistr_div_right: "((k::real) + l) / n = k / n + l / n"
11.16 + rcollect_right:
11.17 "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"
11.18 - rcollect_one_left
11.19 + rcollect_one_left:
11.20 "m is_const ==> (n::real) + m * n = (1 + m) * n"
11.21 - rcollect_one_left_assoc
11.22 + rcollect_one_left_assoc:
11.23 "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"
11.24 - rcollect_one_left_assoc_p
11.25 + rcollect_one_left_assoc_p:
11.26 "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"
11.27
11.28 - rtwo_of_the_same "a + a = 2 * a"
11.29 - rtwo_of_the_same_assoc "(x + a) + a = x + 2 * a"
11.30 - rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x"
11.31 + rtwo_of_the_same: "a + a = 2 * a"
11.32 + rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a"
11.33 + rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x"
11.34
11.35 - rcancel_den "not(a=0) ==> a * (b / a) = b"
11.36 - rcancel_const "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
11.37 - rshift_nominator "(a::real) * b / c = a / c * b"
11.38 + rcancel_den: "not(a=0) ==> a * (b / a) = b"
11.39 + rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"
11.40 + rshift_nominator: "(a::real) * b / c = a / c * b"
11.41
11.42 - exp_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
11.43 - rsqare "(a::real) * a = a ^^^ 2"
11.44 - power_1 "(a::real) ^^^ 1 = a"
11.45 - rbinom_power_2 "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
11.46 + exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
11.47 + rsqare: "(a::real) * a = a ^^^ 2"
11.48 + power_1: "(a::real) ^^^ 1 = a"
11.49 + rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"
11.50
11.51 - rmult_1 "1 * k = (k::real)"
11.52 - rmult_1_right "k * 1 = (k::real)"
11.53 - rmult_0 "0 * k = (0::real)"
11.54 - rmult_0_right "k * 0 = (0::real)"
11.55 - radd_0 "0 + k = (k::real)"
11.56 - radd_0_right "k + 0 = (k::real)"
11.57 + rmult_1: "1 * k = (k::real)"
11.58 + rmult_1_right: "k * 1 = (k::real)"
11.59 + rmult_0: "0 * k = (0::real)"
11.60 + rmult_0_right: "k * 0 = (0::real)"
11.61 + radd_0: "0 + k = (k::real)"
11.62 + radd_0_right: "k + 0 = (k::real)"
11.63
11.64 - radd_real_const_eq
11.65 + radd_real_const_eq:
11.66 "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"
11.67 - radd_real_const
11.68 + radd_real_const:
11.69 "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
11.70
11.71 (*for AC-operators*)
11.72 - radd_commute "(m::real) + (n::real) = n + m"
11.73 - radd_left_commute "(x::real) + (y + z) = y + (x + z)"
11.74 - radd_assoc "(m::real) + n + k = m + (n + k)"
11.75 - rmult_commute "(m::real) * n = n * m"
11.76 - rmult_left_commute "(x::real) * (y * z) = y * (x * z)"
11.77 - rmult_assoc "(m::real) * n * k = m * (n * k)"
11.78 + radd_commute: "(m::real) + (n::real) = n + m"
11.79 + radd_left_commute: "(x::real) + (y + z) = y + (x + z)"
11.80 + radd_assoc: "(m::real) + n + k = m + (n + k)"
11.81 + rmult_commute: "(m::real) * n = n * m"
11.82 + rmult_left_commute: "(x::real) * (y * z) = y * (x * z)"
11.83 + rmult_assoc: "(m::real) * n * k = m * (n * k)"
11.84
11.85 (*for equations: 'bdv' is a meta-constant*)
11.86 - risolate_bdv_add "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
11.87 - risolate_bdv_mult_add "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
11.88 - risolate_bdv_mult "((n::real) * bdv = m) = (bdv = m / n)"
11.89 + risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)"
11.90 + risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"
11.91 + risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)"
11.92
11.93 - rnorm_equation_add
11.94 + rnorm_equation_add:
11.95 "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"
11.96
11.97 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
11.98 - root_ge0 "0 <= a ==> 0 <= sqrt a"
11.99 + root_ge0: "0 <= a ==> 0 <= sqrt a"
11.100 (*should be dropped with better simplification in eval_rls ...*)
11.101 - root_add_ge0
11.102 + root_add_ge0:
11.103 "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"
11.104 - root_ge0_1
11.105 + root_ge0_1:
11.106 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"
11.107 - root_ge0_2
11.108 + root_ge0_2:
11.109 "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"
11.110
11.111
11.112 - rroot_square_inv "(sqrt a)^^^ 2 = a"
11.113 - rroot_times_root "sqrt a * sqrt b = sqrt(a*b)"
11.114 - rroot_times_root_assoc "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
11.115 - rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
11.116 + rroot_square_inv: "(sqrt a)^^^ 2 = a"
11.117 + rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)"
11.118 + rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)"
11.119 + rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a"
11.120
11.121
11.122 (*for root-equations*)
11.123 - square_equation_left
11.124 + square_equation_left:
11.125 "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"
11.126 - square_equation_right
11.127 + square_equation_right:
11.128 "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"
11.129 (*causes frequently non-termination:*)
11.130 - square_equation
11.131 + square_equation:
11.132 "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"
11.133
11.134 - risolate_root_add "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"
11.135 - risolate_root_mult "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
11.136 - risolate_root_div "(a * sqrt c = d) = ( sqrt c = d / a)"
11.137 + risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)"
11.138 + risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"
11.139 + risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)"
11.140
11.141 (*for polynomial equations of degree 2; linear case in RatArith*)
11.142 - mult_square "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
11.143 - constant_square "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
11.144 - constant_mult_square "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
11.145 + mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"
11.146 + constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"
11.147 + constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"
11.148
11.149 - square_equality
11.150 + square_equality:
11.151 "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"
11.152 - square_equality_0
11.153 + square_equality_0:
11.154 "(x^^^2 = 0) = (x = 0)"
11.155
11.156 (*isolate root on the LEFT hand side of the equation
11.157 otherwise shuffling from left to right would not terminate*)
11.158
11.159 - rroot_to_lhs
11.160 + rroot_to_lhs:
11.161 "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"
11.162 - rroot_to_lhs_mult
11.163 + rroot_to_lhs_mult:
11.164 "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"
11.165 - rroot_to_lhs_add_mult
11.166 + rroot_to_lhs_add_mult:
11.167 "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
11.168 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
11.169