1.1 --- a/src/Tools/isac/Knowledge/Atools.thy Wed Dec 05 10:21:35 2012 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Wed Dec 05 15:29:36 2012 +0100
1.3 @@ -252,7 +252,7 @@
1.4 (SOME n1, SOME n2) =>
1.5 let val (T1,T2,Trange) = dest_binop_typ t0
1.6 val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2
1.7 - (*WN071229 "Rings.inverse_class.divide" never tried*)
1.8 + (*WN071229 "Fields.inverse_class.divide" never tried*)
1.9 val rhs = var_op_float v op_ t0 T1 res
1.10 val prop = Trueprop $ (mk_equality (t, rhs))
1.11 in SOME (mk_thmid_f thmid n1 n2, prop) end
1.12 @@ -432,8 +432,8 @@
1.13 (** evaluation on the metalevel **)
1.14
1.15 (*. evaluate HOL.divide .*)
1.16 -(*("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e"))*)
1.17 -fun eval_cancel (thmid:string) "Rings.inverse_class.divide" (t as
1.18 +(*("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e"))*)
1.19 +fun eval_cancel (thmid:string) "Fields.inverse_class.divide" (t as
1.20 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
1.21 (case (int_of_str n1, int_of_str n2) of
1.22 (SOME n1', SOME n2') =>
1.23 @@ -701,7 +701,7 @@
1.24 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
1.25 ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")),
1.26 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
1.27 - ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
1.28 + ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
1.29 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
1.30 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
1.31 ]);
2.1 --- a/src/Tools/isac/Knowledge/Delete.thy Wed Dec 05 10:21:35 2012 +0100
2.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Wed Dec 05 15:29:36 2012 +0100
2.3 @@ -29,7 +29,7 @@
2.4 ((a - c,0),(0,0))
2.5 | calc "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
2.6 ((a * c, b + d), (0, 0))
2.7 - | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
2.8 + | calc "Fields.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
2.9 ((a div c, 0), (0, 0))
2.10 | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
2.11 ((power a c, 0), (0, 0))
3.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Dec 05 10:21:35 2012 +0100
3.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Dec 05 15:29:36 2012 +0100
3.3 @@ -274,7 +274,7 @@
3.4 (*Rls_ discard_parentheses *3**),
3.5 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
3.6 Rls_ separate_bdv2,
3.7 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
3.8 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
3.9 ],
3.10 scr = EmptyScr}:rls;
3.11 *}
3.12 @@ -292,7 +292,7 @@
3.13 Rls_ discard_parentheses,
3.14 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
3.15 Rls_ separate_bdv2,
3.16 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
3.17 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
3.18 ],
3.19 scr = EmptyScr}:rls;
3.20 (*
4.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Dec 05 10:21:35 2012 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Dec 05 15:29:36 2012 +0100
4.3 @@ -200,7 +200,7 @@
4.4 Thm ("divide_divide_eq_left",
4.5 num_str @{thm divide_divide_eq_left}),
4.6 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
4.7 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
4.8 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e"),
4.9
4.10 Thm ("rat_power", num_str @{thm rat_power})
4.11 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
4.12 @@ -264,7 +264,7 @@
4.13 Rls_ discard_parentheses,
4.14 (*Rls_ collect_bdv, from make_polynomial_in*)
4.15 Rls_ separate_bdv2,
4.16 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
4.17 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
4.18 ],
4.19 scr = EmptyScr}:rls;
4.20
4.21 @@ -302,7 +302,7 @@
4.22 * num_str @{thm add_divide_distrib})
4.23 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
4.24 * ]),
4.25 -* Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
4.26 +* Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
4.27 * ],
4.28 * scr = EmptyScr
4.29 * }:rls);
5.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Dec 05 10:21:35 2012 +0100
5.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Dec 05 15:29:36 2012 +0100
5.3 @@ -55,7 +55,7 @@
5.4 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
5.5 (*
5.6 Don't use
5.7 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
5.8 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
5.9 Calc ("Atools.pow" ,eval_binop "#power_"),
5.10 *)
5.11 ];
5.12 @@ -66,7 +66,7 @@
5.13 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
5.14 (*
5.15 Don't use
5.16 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
5.17 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
5.18 Calc ("Atools.pow" ,eval_binop "#power_"),
5.19 *)
5.20 ];
5.21 @@ -87,7 +87,7 @@
5.22 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
5.23 Calc ("Groups.times_class.times",eval_binop "#mult_"),
5.24 (* Dont use
5.25 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
5.26 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
5.27 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
5.28 *)
5.29 Calc ("Atools.pow" ,eval_binop "#power_")
6.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Dec 05 10:21:35 2012 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Dec 05 15:29:36 2012 +0100
6.3 @@ -177,7 +177,7 @@
6.4 let fun coeff_in c v = member op = (vars c) v;
6.5 fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
6.6 (* at the moment there is no term like this, but ....*)
6.7 - | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v =
6.8 + | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v =
6.9 not(coeff_in b v)
6.10 | finddivide (_ $ t1 $ t2) v =
6.11 (finddivide t1 v) orelse (finddivide t2 v)
6.12 @@ -1359,7 +1359,7 @@
6.13 eval_is_multUnordered "")],
6.14 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
6.15 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
6.16 - ("DIVIDE", ("Rings.inverse_class.divide",
6.17 + ("DIVIDE", ("Fields.inverse_class.divide",
6.18 eval_cancel "#divide_e")),
6.19 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
6.20 errpatts = [],
6.21 @@ -1417,7 +1417,7 @@
6.22 eval_is_addUnordered "")],
6.23 calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
6.24 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
6.25 - ("DIVIDE",("Rings.inverse_class.divide",
6.26 + ("DIVIDE",("Fields.inverse_class.divide",
6.27 eval_cancel "#divide_e")),
6.28 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
6.29 errpatts = [],
7.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Dec 05 10:21:35 2012 +0100
7.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Dec 05 15:29:36 2012 +0100
7.3 @@ -479,7 +479,7 @@
7.4 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
7.5 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
7.6 Calc ("Groups.times_class.times",eval_binop "#mult_"),
7.7 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
7.8 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
7.9 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
7.10 Calc ("Atools.pow" ,eval_binop "#power_"),
7.11 Rls_ reduce_012
7.12 @@ -1487,7 +1487,7 @@
7.13 Rls_ separate_bdvs,
7.14 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
7.15 Rls_ cancel_p
7.16 - (*Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e") too weak!*)
7.17 + (*Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e") too weak!*)
7.18 ],
7.19 scr = EmptyScr}:rls);
7.20
8.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed Dec 05 10:21:35 2012 +0100
8.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Dec 05 15:29:36 2012 +0100
8.3 @@ -64,7 +64,7 @@
8.4 fun coeff_in c v = member op = (vars c) v;
8.5 fun finddivide (_ $ _ $ _ $ _) v = error("is_rateqation_in:")
8.6 (* at the moment there is no term like this, but ....*)
8.7 - | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v
8.8 + | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v
8.9 | finddivide (_ $ t1 $ t2) v = (finddivide t1 v)
8.10 orelse (finddivide t2 v)
8.11 | finddivide (_ $ t1) v = (finddivide t1 v)
8.12 @@ -106,7 +106,7 @@
8.13 (merge_rls "is_ratequation_in" calculate_Rational
8.14 (append_rls "is_ratequation_in"
8.15 Poly_erls
8.16 - [(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*)
8.17 + [(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)
8.18 Calc ("RatEq.is'_ratequation'_in",
8.19 eval_is_ratequation_in "")
8.20
8.21 @@ -124,7 +124,7 @@
8.22 (merge_rls "is_ratequation_in" calculate_Rational
8.23 (append_rls "is_ratequation_in"
8.24 Poly_erls
8.25 - [(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*)
8.26 + [(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)
8.27 Calc ("RatEq.is'_ratequation'_in",
8.28 eval_is_ratequation_in "")
8.29 ]))
9.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Dec 05 10:21:35 2012 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Dec 05 15:29:36 2012 +0100
9.3 @@ -1753,7 +1753,7 @@
9.4
9.5
9.6 (*. calculates the greatest common divisor of numerator and denominator and seperates it from each .*)
9.7 -fun step_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
9.8 +fun step_cancel (t as Const ("Fields.inverse_class.divide",_) $ p1 $ p2) =
9.9 let
9.10 val p1' = Unsynchronized.ref [];
9.11 val p2' = Unsynchronized.ref [];
9.12 @@ -1766,7 +1766,7 @@
9.13 p3:= sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));
9.14 if (!p3)=[(1,mv_null2(vars))] then
9.15 (
9.16 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
9.17 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
9.18 )
9.19 else
9.20 (
9.21 @@ -1776,7 +1776,7 @@
9.22
9.23 if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then
9.24 (
9.25 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.26 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.27 $
9.28 (
9.29 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.30 @@ -1796,7 +1796,7 @@
9.31 p2':=mv_skalar_mul(!p2',~1);
9.32 p3:=mv_skalar_mul(!p3,~1);
9.33 (
9.34 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.35 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.36 $
9.37 (
9.38 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.39 @@ -1818,7 +1818,7 @@
9.40
9.41
9.42 (*. same as step_cancel, this time for expanded forms (input+output) .*)
9.43 -fun step_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
9.44 +fun step_cancel_expanded (t as Const ("Fields.inverse_class.divide",_) $ p1 $ p2) =
9.45 let
9.46 val p1' = Unsynchronized.ref [];
9.47 val p2' = Unsynchronized.ref [];
9.48 @@ -1831,7 +1831,7 @@
9.49 p3:= sort (mv_geq LEX_) (mv_gcd (!p1') (!p2'));
9.50 if (!p3)=[(1,mv_null2(vars))] then
9.51 (
9.52 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
9.53 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2
9.54 )
9.55 else
9.56 (
9.57 @@ -1841,7 +1841,7 @@
9.58
9.59 if #1(hd(sort (mv_geq LEX_) (!p2')))(* mv_lc2(!p2',LEX_)*)>0 then
9.60 (
9.61 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.62 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.63 $
9.64 (
9.65 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.66 @@ -1861,7 +1861,7 @@
9.67 p2':=mv_skalar_mul(!p2',~1);
9.68 p3:=mv_skalar_mul(!p3,~1);
9.69 (
9.70 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.71 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.72 $
9.73 (
9.74 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.75 @@ -1882,7 +1882,7 @@
9.76 | step_cancel_expanded _ = error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
9.77
9.78 (*. calculates the greatest common divisor of numerator and denominator and divides each through it .*)
9.79 -fun direct_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
9.80 +fun direct_cancel (t as Const ("Fields.inverse_class.divide",_) $ p1 $ p2) =
9.81 let
9.82 val p1' = Unsynchronized.ref [];
9.83 val p2' = Unsynchronized.ref [];
9.84 @@ -1896,7 +1896,7 @@
9.85
9.86 if (!p3)=[(1,mv_null2(vars))] then
9.87 (
9.88 - (Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
9.89 + (Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
9.90 )
9.91 else
9.92 (
9.93 @@ -1905,7 +1905,7 @@
9.94 if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then
9.95 (
9.96 (
9.97 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.98 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.99 $
9.100 (
9.101 poly2term((!p1'),vars)
9.102 @@ -1936,7 +1936,7 @@
9.103 p2':=mv_skalar_mul(!p2',~1);
9.104 if length(!p3)> 2*(count_neg(!p3)) then () else p3 :=mv_skalar_mul(!p3,~1);
9.105 (
9.106 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.107 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.108 $
9.109 (
9.110 poly2term((!p1'),vars)
9.111 @@ -1967,7 +1967,7 @@
9.112 | direct_cancel _ = error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
9.113
9.114 (*. same es direct_cancel, this time for expanded forms (input+output).*)
9.115 -fun direct_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
9.116 +fun direct_cancel_expanded (t as Const ("Fields.inverse_class.divide",_) $ p1 $ p2) =
9.117 let
9.118 val p1' = Unsynchronized.ref [];
9.119 val p2' = Unsynchronized.ref [];
9.120 @@ -1981,7 +1981,7 @@
9.121
9.122 if (!p3)=[(1,mv_null2(vars))] then
9.123 (
9.124 - (Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
9.125 + (Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $ p1 $ p2,[])
9.126 )
9.127 else
9.128 (
9.129 @@ -1990,7 +1990,7 @@
9.130 if #1(hd(sort (mv_geq LEX_) (!p2'))) (*mv_lc2(!p2',LEX_)*)>0 then
9.131 (
9.132 (
9.133 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.134 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.135 $
9.136 (
9.137 poly2expanded((!p1'),vars)
9.138 @@ -2021,7 +2021,7 @@
9.139 p2':=mv_skalar_mul(!p2',~1);
9.140 if length(!p3)> 2*(count_neg(!p3)) then () else p3 :=mv_skalar_mul(!p3,~1);
9.141 (
9.142 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.143 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.144 $
9.145 (
9.146 poly2expanded((!p1'),vars)
9.147 @@ -2053,7 +2053,7 @@
9.148
9.149
9.150 (*. adds two fractions .*)
9.151 -fun add_fract ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
9.152 +fun add_fract ((Const("Fields.inverse_class.divide",_) $ t11 $ t12),(Const("Fields.inverse_class.divide",_) $ t21 $ t22)) =
9.153 let
9.154 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
9.155 val t11'= Unsynchronized.ref (the(term2poly t11 vars));
9.156 @@ -2084,7 +2084,7 @@
9.157 LEX_));
9.158 tracing"### add_fract: done sort mv_add";
9.159 (
9.160 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.161 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.162 $
9.163 (
9.164 poly2term((!nom),vars)
9.165 @@ -2099,7 +2099,7 @@
9.166 | add_fract (_,_) = error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");
9.167
9.168 (*. adds two expanded fractions .*)
9.169 -fun add_fract_exp ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
9.170 +fun add_fract_exp ((Const("Fields.inverse_class.divide",_) $ t11 $ t12),(Const("Fields.inverse_class.divide",_) $ t21 $ t22)) =
9.171 let
9.172 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
9.173 val t11'= Unsynchronized.ref (the(expanded2poly t11 vars));
9.174 @@ -2118,7 +2118,7 @@
9.175 m2 :=sort (mv_geq LEX_) (#1(mv_division(!den,!t22',LEX_)));
9.176 nom :=sort (mv_geq LEX_) (mv_shorten(mv_add(mv_mul(!t11',!m1,LEX_),mv_mul(!t21',!m2,LEX_),LEX_),LEX_));
9.177 (
9.178 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.179 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.180 $
9.181 (
9.182 poly2expanded((!nom),vars)
9.183 @@ -2176,11 +2176,11 @@
9.184
9.185 (*. converts a list of terms to a list of mv_poly .*)
9.186 fun t2d([],_)=[]
9.187 - | t2d((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);
9.188 + | t2d((t as (Const("Fields.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);
9.189
9.190 (*. same as t2d, this time for expanded forms .*)
9.191 fun t2d_exp([],_)=[]
9.192 - | t2d_exp((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
9.193 + | t2d_exp((t as (Const("Fields.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
9.194
9.195 (*. converts a list of fract terms to a list of their denominators .*)
9.196 fun termlist2denominators [] = ([],[])
9.197 @@ -2193,7 +2193,7 @@
9.198 while length(!xxs)>0 do
9.199 (
9.200 let
9.201 - val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
9.202 + val (t as Const ("Fields.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
9.203 in
9.204 (
9.205 xxs:=tl(!xxs);
9.206 @@ -2210,11 +2210,11 @@
9.207
9.208 (*. converts a list of terms to a list of mv_poly .*)
9.209 fun t2d([],_)=[]
9.210 - | t2d((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);
9.211 + | t2d((t as (Const("Fields.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(term2poly p2 vars)) :: t2d(xs,vars);
9.212
9.213 (*. same as t2d, this time for expanded forms .*)
9.214 fun t2d_exp([],_)=[]
9.215 - | t2d_exp((t as (Const("Rings.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
9.216 + | t2d_exp((t as (Const("Fields.inverse_class.divide",_) $ p1 $ p2))::xs,vars)= (the(expanded2poly p2 vars)) :: t2d_exp(xs,vars);
9.217
9.218 (*. converts a list of fract terms to a list of their denominators .*)
9.219 fun termlist2denominators [] = ([],[])
9.220 @@ -2227,7 +2227,7 @@
9.221 while length(!xxs)>0 do
9.222 (
9.223 let
9.224 - val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
9.225 + val (t as Const ("Fields.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
9.226 in
9.227 (
9.228 xxs:=tl(!xxs);
9.229 @@ -2249,7 +2249,7 @@
9.230 while length(!xxs)>0 do
9.231 (
9.232 let
9.233 - val (t as Const ("Rings.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
9.234 + val (t as Const ("Fields.inverse_class.divide",_) $ p1x $ p2x)=hd(!xxs);
9.235 in
9.236 (
9.237 xxs:=tl(!xxs);
9.238 @@ -2263,7 +2263,7 @@
9.239 (*. reduces all fractions to the least common denominator .*)
9.240 fun com_den(x::xs,denom,den,var)=
9.241 let
9.242 - val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
9.243 + val (t as Const ("Fields.inverse_class.divide",_) $ p1' $ p2')=x;
9.244 val p2= sort (mv_geq LEX_) (the(term2poly p2' var));
9.245 val p3= #1(mv_division(denom,p2,LEX_));
9.246 val p1var=get_vars(p1');
9.247 @@ -2274,7 +2274,7 @@
9.248 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.249 $
9.250 (
9.251 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.252 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.253 $
9.254 poly2term(the (term2poly p1' p1var),p1var)
9.255 $
9.256 @@ -2290,7 +2290,7 @@
9.257 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.258 $
9.259 (
9.260 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.261 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.262 $
9.263 (
9.264 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.265 @@ -2311,7 +2311,7 @@
9.266 if p3=[(1,mv_null2(var))] then
9.267 (
9.268 (
9.269 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.270 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.271 $
9.272 poly2term(the (term2poly p1' p1var),p1var)
9.273 $
9.274 @@ -2322,7 +2322,7 @@
9.275 )
9.276 else
9.277 (
9.278 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.279 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.280 $
9.281 (
9.282 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.283 @@ -2339,7 +2339,7 @@
9.284 (*. same as com_den, this time for expanded forms .*)
9.285 fun com_den_exp(x::xs,denom,den,var)=
9.286 let
9.287 - val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
9.288 + val (t as Const ("Fields.inverse_class.divide",_) $ p1' $ p2')=x;
9.289 val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));
9.290 val p3= #1(mv_division(denom,p2,LEX_));
9.291 val p1var=get_vars(p1');
9.292 @@ -2350,7 +2350,7 @@
9.293 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.294 $
9.295 (
9.296 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.297 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.298 $
9.299 poly2expanded(the(expanded2poly p1' p1var),p1var)
9.300 $
9.301 @@ -2366,7 +2366,7 @@
9.302 Const ("Groups.plus_class.plus",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.303 $
9.304 (
9.305 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.306 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.307 $
9.308 (
9.309 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.310 @@ -2387,7 +2387,7 @@
9.311 if p3=[(1,mv_null2(var))] then
9.312 (
9.313 (
9.314 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.315 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.316 $
9.317 poly2expanded(the(expanded2poly p1' p1var),p1var)
9.318 $
9.319 @@ -2398,7 +2398,7 @@
9.320 )
9.321 else
9.322 (
9.323 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.324 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
9.325 $
9.326 (
9.327 Const ("Groups.times_class.times",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.328 @@ -2417,7 +2417,7 @@
9.329 (* WN0210???SK brauch ma des überhaupt *)
9.330 fun com_den2(x::xs,denom,den,var)=
9.331 let
9.332 - val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
9.333 + val (t as Const ("Fields.inverse_class.divide",_) $ p1' $ p2')=x;
9.334 val p2= sort (mv_geq LEX_) (the(term2poly p2' var));
9.335 val p3= #1(mv_division(denom,p2,LEX_));
9.336 val p1var=get_vars(p1');
9.337 @@ -2461,7 +2461,7 @@
9.338 (* WN0210???SK brauch ma des überhaupt *)
9.339 fun com_den_exp2(x::xs,denom,den,var)=
9.340 let
9.341 - val (t as Const ("Rings.inverse_class.divide",_) $ p1' $ p2')=x;
9.342 + val (t as Const ("Fields.inverse_class.divide",_) $ p1' $ p2')=x;
9.343 val p2= sort (mv_geq LEX_) (the(expanded2poly p2' var));
9.344 val p3= #1(mv_division(denom,p2,LEX_));
9.345 val p1var=get_vars p1';
9.346 @@ -2654,7 +2654,7 @@
9.347 val den=factorize_den(#1(den_list),denom,var); (* faktorisierter Nenner !!! *)
9.348 in
9.349 (
9.350 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.351 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.352 com_den2(xs,denom, poly2term(denom,var)(*den*),var) $
9.353 poly2term(denom,var)
9.354 ,
9.355 @@ -2672,7 +2672,7 @@
9.356 val den=factorize_den_exp(#1(den_list),denom,var); (* faktorisierter Nenner !!! *)
9.357 in
9.358 (
9.359 - Const ("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.360 + Const ("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.361 com_den_exp2(xs,denom, poly2term(denom,var)(*den*),var) $
9.362 poly2expanded(denom,var)
9.363 ,
9.364 @@ -2683,18 +2683,18 @@
9.365
9.366
9.367 (* converts a term, which contains several terms seperated by +, into a list of these terms .*)
9.368 -fun term2list (t as (Const("Rings.inverse_class.divide",_) $ _ $ _)) = [t]
9.369 +fun term2list (t as (Const("Fields.inverse_class.divide",_) $ _ $ _)) = [t]
9.370 | term2list (t as (Const("Atools.pow",_) $ _ $ _)) =
9.371 - [Const ("Rings.inverse_class.divide",
9.372 + [Const ("Fields.inverse_class.divide",
9.373 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $
9.374 t $ Free("1",HOLogic.realT)
9.375 ]
9.376 | term2list (t as (Free(_,_))) =
9.377 - [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.378 + [Const("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.379 t $ Free("1",HOLogic.realT)
9.380 ]
9.381 | term2list (t as (Const("Groups.times_class.times",_) $ _ $ _)) =
9.382 - [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.383 + [Const("Fields.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
9.384 t $ Free("1",HOLogic.realT)
9.385 ]
9.386 | term2list (Const("Groups.plus_class.plus",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)
9.387 @@ -2790,7 +2790,7 @@
9.388 erls = calc_rat_erls, srls = Erls,
9.389 calc = [], errpatts = [],
9.390 rules =
9.391 - [Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
9.392 + [Calc ("Fields.inverse_class.divide",eval_cancel "#divide_e"),
9.393
9.394 Thm ("minus_divide_left",num_str (@{thm minus_divide_left} RS @{thm sym})),
9.395 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
9.396 @@ -3011,7 +3011,7 @@
9.397 erls = rational_erls,
9.398 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
9.399 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
9.400 - ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
9.401 + ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
9.402 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
9.403 errpatts = [],
9.404 scr=Rfuns {init_state = init_state thy Atools_erls ro,
9.405 @@ -3097,7 +3097,7 @@
9.406 erls = rational_erls,
9.407 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
9.408 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
9.409 - ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
9.410 + ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
9.411 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
9.412 errpatts = [],
9.413 scr=Rfuns {init_state = init_state thy Atools_erls ro,
9.414 @@ -3251,7 +3251,7 @@
9.415 erls = rational_erls,
9.416 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
9.417 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
9.418 - ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
9.419 + ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
9.420 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
9.421 errpatts = [],
9.422 scr=Rfuns {init_state = init_state thy Atools_erls ro,
9.423 @@ -3402,7 +3402,7 @@
9.424 erls = rational_erls,
9.425 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
9.426 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
9.427 - ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
9.428 + ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
9.429 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
9.430 errpatts = [],
9.431 scr=Rfuns {init_state = init_state thy Atools_erls ro,
9.432 @@ -3425,7 +3425,7 @@
9.433 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
9.434 | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
9.435 | is_ratpolyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
9.436 - | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ Free _ $ Free _) = true
9.437 + | is_ratpolyexp (Const ("Fields.inverse_class.divide",_) $ Free _ $ Free _) = true
9.438 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
9.439 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
9.440 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
9.441 @@ -3434,7 +3434,7 @@
9.442 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
9.443 | is_ratpolyexp (Const ("Atools.pow",_) $ t1 $ t2) =
9.444 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
9.445 - | is_ratpolyexp (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) =
9.446 + | is_ratpolyexp (Const ("Fields.inverse_class.divide",_) $ t1 $ t2) =
9.447 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
9.448 | is_ratpolyexp _ = false;
9.449
9.450 @@ -3455,7 +3455,7 @@
9.451 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
9.452 fun eval_get_denominator (thmid:string) _
9.453 (t as Const ("Rational.get_denominator", _) $
9.454 - (Const ("Rings.inverse_class.divide", _) $ num $
9.455 + (Const ("Fields.inverse_class.divide", _) $ num $
9.456 denom)) thy =
9.457 SOME (mk_thmid thmid ""
9.458 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",
9.459 @@ -3466,7 +3466,7 @@
9.460 (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
9.461 fun eval_get_numerator (thmid:string) _
9.462 (t as Const ("Rational.get_numerator", _) $
9.463 - (Const ("Rings.inverse_class.divide", _) $num
9.464 + (Const ("Fields.inverse_class.divide", _) $num
9.465 $denom )) thy =
9.466 SOME (mk_thmid thmid ""
9.467 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) num) "",
9.468 @@ -3559,7 +3559,7 @@
9.469 Thm ("divide_divide_eq_left",
9.470 num_str @{thm divide_divide_eq_left}),
9.471 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
9.472 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e")
9.473 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e")
9.474 ],
9.475 scr = EmptyScr
9.476 }:rls);
9.477 @@ -3737,7 +3737,7 @@
9.478 Thm ("divide_divide_eq_left",
9.479 num_str @{thm divide_divide_eq_left}),
9.480 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
9.481 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
9.482 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e"),
9.483
9.484 Thm ("rat_power", num_str @{thm rat_power})
9.485 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
10.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Dec 05 10:21:35 2012 +0100
10.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Dec 05 15:29:36 2012 +0100
10.3 @@ -167,7 +167,7 @@
10.4 append_rls "Root_crls" Atools_erls
10.5 [Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
10.6 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
10.7 - Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
10.8 + Calc ("Fields.inverse_class.divide",eval_cancel "#divide_e"),
10.9 Calc ("Atools.pow" ,eval_binop "#power_"),
10.10 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.11 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
10.12 @@ -179,7 +179,7 @@
10.13 append_rls "Root_erls" Atools_erls
10.14 [Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
10.15 Calc ("NthRoot.sqrt" ,eval_sqrt "#sqrt_"),
10.16 - Calc ("Rings.inverse_class.divide",eval_cancel "#divide_e"),
10.17 + Calc ("Fields.inverse_class.divide",eval_cancel "#divide_e"),
10.18 Calc ("Atools.pow" ,eval_binop "#power_"),
10.19 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.20 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
10.21 @@ -296,7 +296,7 @@
10.22 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.23 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
10.24 Calc ("Groups.times_class.times", eval_binop "#mult_"),
10.25 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
10.26 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e"),
10.27 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
10.28 Calc ("Atools.pow", eval_binop "#power_"),
10.29
10.30 @@ -321,7 +321,7 @@
10.31 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
10.32 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
10.33 Calc ("Groups.times_class.times", eval_binop "#mult_"),
10.34 - Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e"),
10.35 + Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e"),
10.36 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
10.37 Calc ("Atools.pow", eval_binop "#power_")
10.38 ],
11.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed Dec 05 10:21:35 2012 +0100
11.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Dec 05 15:29:36 2012 +0100
11.3 @@ -169,7 +169,7 @@
11.4 | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
11.5 | isnorm (Const ("Groups.times_class.times",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
11.6 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false
11.7 - | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
11.8 + | isnorm (Const ("Fields.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
11.9 (is_sqrtTerm_in t2 v)
11.10 | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v
11.11 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
11.12 @@ -458,7 +458,7 @@
11.13 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
11.14 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
11.15 Calc ("Groups.times_class.times",eval_binop "#mult_"),
11.16 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
11.17 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
11.18 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
11.19 Calc ("Atools.pow" ,eval_binop "#power_"),
11.20 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
12.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed Dec 05 10:21:35 2012 +0100
12.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Dec 05 15:29:36 2012 +0100
12.3 @@ -56,7 +56,7 @@
12.4 | rootadd _ _ = false;
12.5 fun findrootrat (_ $ _ $ _ $ _) v = error("is_rootRatAddTerm_in:")
12.6 (* at the moment there is no term like this, but ....*)
12.7 - | findrootrat (t as (Const ("Rings.inverse_class.divide",_) $ _ $ t3)) v =
12.8 + | findrootrat (t as (Const ("Fields.inverse_class.divide",_) $ _ $ t3)) v =
12.9 if (is_rootTerm_in t3 v) then rootadd t3 v else false
12.10 | findrootrat (_ $ t1 $ t2) v =
12.11 (findrootrat t1 v) orelse (findrootrat t2 v)
13.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Dec 05 10:21:35 2012 +0100
13.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Dec 05 15:29:36 2012 +0100
13.3 @@ -425,7 +425,7 @@
13.4 thus they MUST be done IMMEDIATELY before calc *)
13.5 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
13.6 Calc ("Groups.times_class.times", eval_binop "#mult_"),
13.7 - Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),
13.8 + Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
13.9 Calc ("Atools.pow", eval_binop "#power_"),
13.10
13.11 Thm ("rcollect_right",num_str @{thm rcollect_right}),
13.12 @@ -503,7 +503,7 @@
13.13 (*aus Atools.ML*)
13.14 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
13.15 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
13.16 - ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
13.17 + ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
13.18 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
13.19 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
13.20 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
14.1 --- a/src/Tools/isac/ProgLang/termC.sml Wed Dec 05 10:21:35 2012 +0100
14.2 +++ b/src/Tools/isac/ProgLang/termC.sml Wed Dec 05 15:29:36 2012 +0100
14.3 @@ -632,7 +632,7 @@
14.4 (*fun calc "Groups.plus_class.plus" (n1, n2) = n1+n2
14.5 | calc "Groups.minus_class.minus" (n1, n2) = n1-n2
14.6 | calc "Groups.times_class.times" (n1, n2) = n1*n2
14.7 - | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
14.8 + | calc "Fields.inverse_class.divide"(n1, n2) = n1 div n2
14.9 | calc "Atools.pow"(n1, n2) = power n1 n2
14.10 | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*)
14.11 fun calc_equ "less" (n1, n2) = n1 < n2
15.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Wed Dec 05 10:21:35 2012 +0100
15.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Wed Dec 05 15:29:36 2012 +0100
15.3 @@ -24,7 +24,7 @@
15.4 *)
15.5 fun eval_get_denominator (thmid:string) _
15.6 (t as Const ("Rational.get_denominator", _) $
15.7 - (Const ("Rings.inverse_class.divide", _) $num
15.8 + (Const ("Fields.inverse_class.divide", _) $num
15.9 $denom)) thy =
15.10 SOME (mk_thmid thmid ""
15.11 (Print_Mode.setmp []
16.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Dec 05 10:21:35 2012 +0100
16.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Dec 05 15:29:36 2012 +0100
16.3 @@ -182,7 +182,7 @@
16.4 ML {*
16.5 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
16.6 val (_, denom) =
16.7 - HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr;
16.8 + HOLogic.dest_bin "Fields.inverse_class.divide" (type_of expr) expr;
16.9 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
16.10 *}
16.11
16.12 @@ -216,7 +216,7 @@
16.13 *)
16.14 fun eval_get_denominator (thmid:string) _
16.15 (t as Const ("Rational.get_denominator", _) $
16.16 - (Const ("Rings.inverse_class.divide", _) $num
16.17 + (Const ("Fields.inverse_class.divide", _) $num
16.18 $denom)) thy =
16.19 SOME (mk_thmid thmid ""
16.20 (Print_Mode.setmp []
16.21 @@ -238,7 +238,7 @@
16.22 *)
16.23 fun eval_get_numerator (thmid:string) _
16.24 (t as Const ("Rational.get_numerator", _) $
16.25 - (Const ("Rings.inverse_class.divide", _) $num
16.26 + (Const ("Fields.inverse_class.divide", _) $num
16.27 $denom )) thy =
16.28 SOME (mk_thmid thmid ""
16.29 (Print_Mode.setmp []
16.30 @@ -595,7 +595,7 @@
16.31 val SOME numerator = parseNEW ctxt "3::real";
16.32
16.33 val expr' = HOLogic.mk_binop
16.34 - "Rings.inverse_class.divide" (numerator, denominator');
16.35 + "Fields.inverse_class.divide" (numerator, denominator');
16.36 term2str expr';
16.37 *}
16.38
17.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Wed Dec 05 10:21:35 2012 +0100
17.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Wed Dec 05 15:29:36 2012 +0100
17.3 @@ -91,8 +91,8 @@
17.4 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
17.5
17.6 val test = HOLogic.mk_binop "Groups.plus_class.plus"
17.7 - (HOLogic.mk_binop "Rings.inverse_class.divide" (A_var, denom1),
17.8 - HOLogic.mk_binop "Rings.inverse_class.divide" (B_var, denom2));
17.9 + (HOLogic.mk_binop "Fields.inverse_class.divide" (A_var, denom1),
17.10 + HOLogic.mk_binop "Fields.inverse_class.divide" (B_var, denom2));
17.11
17.12 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
17.13 else error "HOLogic.mk_binop broken ?";
18.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed Dec 05 10:21:35 2012 +0100
18.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Dec 05 15:29:36 2012 +0100
18.3 @@ -198,7 +198,7 @@
18.4 val thy = @{theory Test};
18.5 val t = (term_of o the o (parse thy)) "(-4) / 2";
18.6
18.7 -val SOME (_, t) = eval_cancel "xxx" "Rings.inverse_class.divide" t thy;
18.8 +val SOME (_, t) = eval_cancel "xxx" "Fields.inverse_class.divide" t thy;
18.9
18.10 term2str t;
18.11 "-4 / 2 = (-2)";
19.1 --- a/test/Tools/isac/Test_Some.thy Wed Dec 05 10:21:35 2012 +0100
19.2 +++ b/test/Tools/isac/Test_Some.thy Wed Dec 05 15:29:36 2012 +0100
19.3 @@ -1,8 +1,8 @@
19.4
19.5 theory Test_Some imports Isac
19.6 -uses ("ProgLang/calculate.sml")
19.7 +uses ("ProgLang/scrtools.sml")
19.8 begin
19.9 -use "ProgLang/calculate.sml"
19.10 +use "ProgLang/scrtools.sml"
19.11
19.12 declare [[show_types]]
19.13 declare [[show_sorts]]
19.14 @@ -19,57 +19,7 @@
19.15 find_consts "Arbfix"
19.16 *}
19.17 ML {* (*==================*)
19.18 -"----------- fun calculate_ -----------------------------";
19.19 -val thy = @{theory "Test"};
19.20 -"===== test 1";
19.21 -val t = (term_of o the o (parse thy)) "1+2";
19.22 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
19.23 -if term2str (prop_of thm) = "1 + 2 = 3" then ()
19.24 -else error "get_calculation_: 1 + 2 = 3";
19.25 -
19.26 -"===== test 2";
19.27 -val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
19.28 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
19.29 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
19.30 -if term2str t = "(3 * 4 / 3) ^^^ 2" then ()
19.31 -else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2";
19.32 -
19.33 -"===== test 3b -- 2 contiued";
19.34 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
19.35 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
19.36 -if term2str t = "(12 / 3) ^^^ 2" then ()
19.37 -else error "calculate TIMES: (3 * 4 / 3) ^^^ 2 --> (12 / 3) ^^^ 2";
19.38 -
19.39 -"===== test 4";
19.40 -*}
19.41 -ML {*
19.42 -assoc(calclist,"DIVIDE");
19.43 -the(assoc(calclist,"DIVIDE"));
19.44 -get_calculation_ thy;
19.45 -get_calculation_ thy(the(assoc(calclist,"DIVIDE")))
19.46 -*}
19.47 -ML {*
19.48 -term2str t
19.49 -*}
19.50 -ML {*
19.51 -get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
19.52 -*}
19.53 -ML {*
19.54 -*}
19.55 -ML {*
19.56 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
19.57 -*}
19.58 -ML {*
19.59 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
19.60 -term2str t;
19.61 -(*it = "#4 ^^^ #2" : string*)
19.62 -
19.63 -"===== test 5";
19.64 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
19.65 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
19.66 -(*show_types := false;*)
19.67 -if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"
19.68 -else ();
19.69 +@{term "a/b"}
19.70 *}
19.71 ML {*
19.72 *}