1.1 --- a/src/sml/IsacKnowledge/Atools.ML Fri Dec 28 14:57:38 2007 +0100
1.2 +++ b/src/sml/IsacKnowledge/Atools.ML Mon Dec 31 09:55:43 2007 +0100
1.3 @@ -187,7 +187,8 @@
1.4 case (numeral t1, numeral t2) of
1.5 (Some n1, Some n2) =>
1.6 let val (T1,T2,Trange) = dest_binop_typ t0
1.7 - val res = calc op0 n1 n2
1.8 + val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
1.9 + (*WN071229 "HOL.divide" never tried*)
1.10 val rhs = var_op_float v op_ t0 T1 res
1.11 val prop = Trueprop $ (mk_equality (t, rhs))
1.12 in Some (mk_thmid_f thmid n1 n2, prop) end
1.13 @@ -201,6 +202,7 @@
1.14 if op0 = op0' then
1.15 case (numeral t1, numeral t2) of
1.16 (Some n1, Some n2) =>
1.17 + if op0 = "op -" then None else
1.18 let val (T1,T2,Trange) = dest_binop_typ t0
1.19 val res = calc op0 n1 n2
1.20 val rhs = float_op_var v op_ t0 T1 res
1.21 @@ -507,11 +509,17 @@
1.22 append_rls "Atools_erls" e_rls
1.23 [Calc ("op =",eval_equal "#equal_"),
1.24 Thm ("not_true",num_str not_true),
1.25 + (*"(~ True) = False"*)
1.26 Thm ("not_false",num_str not_false),
1.27 + (*"(~ False) = True"*)
1.28 Thm ("and_true",and_true),
1.29 + (*"(?a & True) = ?a"*)
1.30 Thm ("and_false",and_false),
1.31 + (*"(?a & False) = False"*)
1.32 Thm ("or_true",or_true),
1.33 + (*"(?a | True) = True"*)
1.34 Thm ("or_false",or_false),
1.35 + (*"(?a | False) = ?a"*)
1.36
1.37 Thm ("rat_leq1",rat_leq1),
1.38 Thm ("rat_leq2",rat_leq2),
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/IsacKnowledge/Float.ML Mon Dec 31 09:55:43 2007 +0100
2.3 @@ -0,0 +1,95 @@
2.4 +(* use"Float.ML";
2.5 + *)
2.6 +
2.7 +theory' := overwritel (!theory', [("Float.thy",Float.thy)]);
2.8 +
2.9 +(*.used for calculating built in binary operations in Isabelle2002.
2.10 + integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)
2.11 +fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int) =
2.12 + if b < d
2.13 + then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
2.14 + else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
2.15 + | calc "op -" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
2.16 + ((a - c,0),(0,0))
2.17 + | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
2.18 + ((a * c, b + d), (0, 0))
2.19 + | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
2.20 + ((a div c, 0), (0, 0))
2.21 + | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
2.22 + ((power a c, 0), (0, 0))
2.23 + | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
2.24 + raise error ("calc: not impl. for Float (("^
2.25 + (string_of_int a )^","^(string_of_int b )^"), ("^
2.26 + (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
2.27 + (string_of_int c )^","^(string_of_int d )^"), ("^
2.28 + (string_of_int p21)^","^(string_of_int p22)^"))");
2.29 +(*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
2.30 +val it = ((1,0),(0,0))*)
2.31 +
2.32 +(*.toggle the sign of an integer numeral.*)
2.33 +fun minus ((a, b:int), _:int * int) = ((~1 * a, b), (0, 0));
2.34 +
2.35 +(*.convert internal floatingpoint prepresentation to int and float.*)
2.36 +fun term_of_float T ((val1, 0), ( 0, 0)) =
2.37 + term_of_num T val1
2.38 + | term_of_float T ((val1, val2), (precision1, precision2)) =
2.39 + let val pT = pairT T T
2.40 + in Const ("Float.Float", (pairT pT pT) --> T)
2.41 + $ (pairt (pairt (Free (str_of_int val1, T))
2.42 + (Free (str_of_int val2, T)))
2.43 + (pairt (Free (str_of_int precision1, T))
2.44 + (Free (str_of_int precision2, T))))
2.45 + end;
2.46 +(*> val t = str2term "Float ((1,2),(0,0))";
2.47 +> val Const ("Float.Float", fT) $ _ = t;
2.48 +> atomtyp fT;
2.49 +> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
2.50 +> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
2.51 +> atomtyp ffT;
2.52 +> fT = ffT;
2.53 +val it = true : bool
2.54 +
2.55 +t = float_term_of_num HOLogic.realT ((1,2),(0,0));
2.56 +val it = true : bool*)
2.57 +
2.58 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
2.59 +fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
2.60 + var_op_num v op_ optype ntyp v1
2.61 + | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
2.62 + let val pT = pairT T T
2.63 + in Const (op_, optype) $ v $
2.64 + (Const ("Float.Float", (pairT pT pT) --> T)
2.65 + $ (pairt (pairt (Free (str_of_int v1, T))
2.66 + (Free (str_of_int v2, T)))
2.67 + (pairt (Free (str_of_int p1, T))
2.68 + (Free (str_of_int p2, T)))))
2.69 + end;
2.70 +(*> val t = str2term "a + b";
2.71 +> val Const ("op +", optype) $ _ $ _ = t;
2.72 +> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
2.73 +> t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0));
2.74 +val it = true : bool*)
2.75 +
2.76 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
2.77 +fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
2.78 + num_op_var v op_ optype ntyp v1
2.79 + | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
2.80 + let val pT = pairT T T
2.81 + in Const (op_,optype) $
2.82 + (Const ("Float.Float", (pairT pT pT) --> T)
2.83 + $ (pairt (pairt (Free (str_of_int v1, T))
2.84 + (Free (str_of_int v2, T)))
2.85 + (pairt (Free (str_of_int p1, T))
2.86 + (Free (str_of_int p2, T))))) $ v
2.87 + end;
2.88 +(*> val t = str2term "a + b";
2.89 +> val Const ("op +", optype) $ _ $ _ = t;
2.90 +> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
2.91 +> t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0));
2.92 +val it = true : bool*)
2.93 +
2.94 +
2.95 +
2.96 +
2.97 +
2.98 +
3.1 --- a/src/sml/IsacKnowledge/Poly.ML Fri Dec 28 14:57:38 2007 +0100
3.2 +++ b/src/sml/IsacKnowledge/Poly.ML Mon Dec 31 09:55:43 2007 +0100
3.3 @@ -404,14 +404,21 @@
3.4 (*"(a + b)^^^4 = ... "*)
3.5 Thm ("real_plus_binom_pow5",num_str real_plus_binom_pow5),
3.6 (*"(a + b)^^^5 = ... "*)
3.7 - Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
3.8 - (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
3.9 Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
3.10 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
3.11 - Thm ("real_plus_minus_binom1_p_p",num_str real_plus_minus_binom1_p_p),
3.12 +
3.13 + (*WN071229 changed/removed for Schaerding -----vvv*)
3.14 + (*Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),*)
3.15 + (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
3.16 + Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
3.17 + (*"(a + b)^^^2 = (a + b) * (a + b)"*)
3.18 + (*Thm ("real_plus_minus_binom1_p_p",
3.19 + num_str real_plus_minus_binom1_p_p),*)
3.20 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
3.21 - Thm ("real_plus_minus_binom2_p_p",num_str real_plus_minus_binom2_p_p),
3.22 + (*Thm ("real_plus_minus_binom2_p_p",
3.23 + num_str real_plus_minus_binom2_p_p),*)
3.24 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
3.25 + (*WN071229 changed/removed for Schaerding -----^^^*)
3.26
3.27 Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
3.28 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
3.29 @@ -589,6 +596,8 @@
3.30 (*"1 * z = z"*)
3.31 Thm ("real_mult_0",num_str real_mult_0),
3.32 (*"0 * z = 0"*)
3.33 + Thm ("real_mult_0_right",num_str real_mult_0_right),
3.34 + (*"z * 0 = 0"*)
3.35 Thm ("real_add_zero_left",num_str real_add_zero_left),
3.36 (*"0 + z = z"*)
3.37 Thm ("real_add_zero_right",num_str real_add_zero_right),
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/sml/IsacKnowledge/Poly.thy Mon Dec 31 09:55:43 2007 +0100
4.3 @@ -0,0 +1,147 @@
4.4 +(* WN.020812: theorems in the Reals,
4.5 + necessary for special rule sets, in addition to Isabelle2002.
4.6 + !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
4.7 + !!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!
4.8 + !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
4.9 + xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002
4.10 + changed by: Richard Lang 020912
4.11 +*)
4.12 +
4.13 +(*
4.14 + use_thy"IsacKnowledge/Poly";
4.15 + use_thy"Poly";
4.16 + use_thy_only"IsacKnowledge/Poly";
4.17 +
4.18 + remove_thy"Poly";
4.19 + use_thy"IsacKnowledge/Isac";
4.20 +
4.21 +
4.22 + use"ROOT.ML";
4.23 + cd"IsacKnowledge";
4.24 + *)
4.25 +
4.26 +Poly = Simplify +
4.27 +
4.28 +(*-------------------- consts-----------------------------------------------*)
4.29 +consts
4.30 +
4.31 + is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
4.32 + is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *)
4.33 + has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
4.34 + is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
4.35 +
4.36 + is'_multUnordered :: "real => bool" ("_ is'_multUnordered")
4.37 + is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
4.38 + is'_polyexp :: "real => bool" ("_ is'_polyexp")
4.39 +
4.40 + Expand'_binoms
4.41 + :: "['y, \
4.42 + \ 'y] => 'y"
4.43 + ("((Script Expand'_binoms (_ =))// \
4.44 + \ (_))" 9)
4.45 +
4.46 +(*-------------------- rules------------------------------------------------*)
4.47 +rules (*.not contained in Isabelle2002,
4.48 + stated as axioms, TODO: prove as theorems;
4.49 + theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
4.50 +
4.51 + realpow_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
4.52 + realpow_addI "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
4.53 + realpow_addI_assoc_l "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"
4.54 + realpow_addI_assoc_r "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"
4.55 +
4.56 + realpow_oneI "r ^^^ 1 = r"
4.57 + realpow_zeroI "r ^^^ 0 = 1"
4.58 + realpow_eq_oneI "1 ^^^ n = 1"
4.59 + realpow_multI "(r * s) ^^^ n = r ^^^ n * s ^^^ n"
4.60 + realpow_multI_poly "[| r is_polyexp; s is_polyexp |] ==> \
4.61 + \(r * s) ^^^ n = r ^^^ n * s ^^^ n"
4.62 + realpow_minus_oneI "-1 ^^^ (2 * n) = 1"
4.63 +
4.64 + realpow_twoI "r ^^^ 2 = r * r"
4.65 + realpow_twoI_assoc_l "r * (r * s) = r ^^^ 2 * s"
4.66 + realpow_twoI_assoc_r "s * r * r = s * r ^^^ 2"
4.67 + realpow_two_atom "r is_atom ==> r * r = r ^^^ 2"
4.68 + realpow_plus_1 "r * r ^^^ n = r ^^^ (n + 1)"
4.69 + realpow_plus_1_assoc_l "r * (r ^^^ m * s) = r ^^^ (1 + m) * s"
4.70 + realpow_plus_1_assoc_l2 "r ^^^ m * (r * s) = r ^^^ (1 + m) * s"
4.71 + realpow_plus_1_assoc_r "s * r * r ^^^ m = s * r ^^^ (1 + m)"
4.72 + realpow_plus_1_atom "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
4.73 + realpow_def_atom "[| Not (r is_atom); 1 < n |] \
4.74 + \ ==> r ^^^ n = r * r ^^^ (n + -1)"
4.75 + realpow_addI_atom "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
4.76 +
4.77 +
4.78 + realpow_minus_even "n is_even ==> (- r) ^^^ n = r ^^^ n"
4.79 + realpow_minus_odd "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
4.80 +
4.81 +
4.82 +(* RL 020914 *)
4.83 + real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
4.84 + real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
4.85 + real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
4.86 + real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
4.87 + real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
4.88 + real_plus_binom_pow3_poly "[| a is_polyexp; b is_polyexp |] ==> \
4.89 + \(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
4.90 + real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
4.91 + real_minus_binom_pow3_p "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 + -1*b^^^3"
4.92 +(* real_plus_binom_pow "[| n is_const; 3 < n |] ==> \
4.93 + \(a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
4.94 + real_plus_binom_pow4 "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a + b)"
4.95 + real_plus_binom_pow4_poly "[| a is_polyexp; b is_polyexp |] ==> \
4.96 + \(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a + b)"
4.97 + real_plus_binom_pow5 "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
4.98 +
4.99 + real_plus_binom_pow5_poly "[| a is_polyexp; b is_polyexp |] ==> \
4.100 + \(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
4.101 +
4.102 + real_diff_plus "a - b = a + -b" (*17.3.03: do_NOT_use*)
4.103 + real_diff_minus "a - b = a + -1 * b"
4.104 + real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
4.105 + real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
4.106 + (*WN071229 changed for Schaerding -----vvv*)
4.107 + (*real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
4.108 + real_plus_binom_pow2 "(a + b)^^^2 = (a + b) * (a + b)"
4.109 + (*WN071229 changed for Schaerding -----^^^*)
4.110 + real_plus_binom_pow2_poly "[| a is_polyexp; b is_polyexp |] ==> \
4.111 + \(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
4.112 + real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
4.113 + real_minus_binom_pow2_p "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
4.114 + real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2"
4.115 + real_plus_minus_binom1_p "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
4.116 + real_plus_minus_binom1_p_p "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"
4.117 + real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2"
4.118 + real_plus_minus_binom2_p "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
4.119 + real_plus_minus_binom2_p_p "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
4.120 + real_plus_binom_times1 "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
4.121 + real_plus_binom_times2 "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"
4.122 +
4.123 + real_num_collect "[| l is_const; m is_const |] ==> \
4.124 + \l * n + m * n = (l + m) * n"
4.125 +(* FIXME.MG.0401: replace 'real_num_collect_assoc'
4.126 + by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
4.127 + real_num_collect_assoc "[| l is_const; m is_const |] ==> \
4.128 + \l * n + (m * n + k) = (l + m) * n + k"
4.129 + real_num_collect_assoc_l "[| l is_const; m is_const |] ==> \
4.130 + \l * n + (m * n + k) = (l + m)
4.131 + * n + k"
4.132 + real_num_collect_assoc_r "[| l is_const; m is_const |] ==> \
4.133 + \(k + m * n) + l * n = k + (l + m) * n"
4.134 + real_one_collect "m is_const ==> n + m * n = (1 + m) * n"
4.135 +(* FIXME.MG.0401: replace 'real_one_collect_assoc'
4.136 + by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
4.137 + real_one_collect_assoc "m is_const ==> n + (m * n + k) = (1 + m)* n + k"
4.138 +
4.139 + real_one_collect_assoc_l "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
4.140 + real_one_collect_assoc_r "m is_const ==>(k + n) + m * n = k + (1 + m) * n"
4.141 +
4.142 +(* FIXME.MG.0401: replace 'real_mult_2_assoc'
4.143 + by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
4.144 + real_mult_2_assoc "z1 + (z1 + k) = 2 * z1 + k"
4.145 + real_mult_2_assoc_l "z1 + (z1 + k) = 2 * z1 + k"
4.146 + real_mult_2_assoc_r "(k + z1) + z1 = k + 2 * z1"
4.147 +
4.148 + real_add_mult_distrib_poly "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w"
4.149 + real_add_mult_distrib2_poly "w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
4.150 +end
5.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Fri Dec 28 14:57:38 2007 +0100
5.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Mon Dec 31 09:55:43 2007 +0100
5.3 @@ -151,6 +151,19 @@
5.4 Calc ("op *", eval_binop "#mult_")
5.5 ], scr = EmptyScr}:rls;
5.6
5.7 +val klammern_ausmultiplizieren =
5.8 + Rls{id = "klammern_ausmultiplizieren", preconds = [],
5.9 + rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
5.10 + rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)),
5.11 + (*"a + (b + c) = (a + b) + c"*)
5.12 + Thm ("klammer_plus_minus",num_str klammer_plus_minus),
5.13 + (*"a + (b - c) = (a + b) - c"*)
5.14 + Thm ("klammer_minus_plus",num_str klammer_minus_plus),
5.15 + (*"a - (b + c) = (a - b) - c"*)
5.16 + Thm ("klammer_minus_minus",num_str klammer_minus_minus)
5.17 + (*"a - (b - c) = (a - b) + c"*)
5.18 + ], scr = EmptyScr}:rls;
5.19 +
5.20 val multipliziere_aus =
5.21 Rls{id = "multipliziere_aus", preconds = [],
5.22 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
5.23 @@ -164,6 +177,8 @@
5.24 [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
5.25 ("fasse_zusammen", prep_rls fasse_zusammen),
5.26 ("verschoenere", prep_rls verschoenere),
5.27 + ("klammern_ausmultiplizieren",
5.28 + prep_rls klammern_ausmultiplizieren),
5.29 ("multipliziere_aus", prep_rls multipliziere_aus)
5.30 ]);
5.31
5.32 @@ -173,13 +188,38 @@
5.33 (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
5.34 (["polynom","vereinfachen"],
5.35 [("#Given" ,["term t_"]),
5.36 + ("#Where" ,["t_ is_polyexp",
5.37 + "Not (matchsub (?a + (?b + ?c)) t_ & \
5.38 + \ matchsub (?a + (?b - ?c)) t_ & \
5.39 + \ matchsub (?a - (?b + ?c)) t_ & \
5.40 + \ matchsub (?a + (?b - ?c)) t_ )"]),
5.41 + ("#Find" ,["normalform n_"])
5.42 + ],
5.43 + append_rls "prls_pbl_vereinf_poly" e_rls
5.44 + [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
5.45 + Calc ("Tools.matchsub", eval_matchsub ""),
5.46 + Thm ("and_true",and_true),
5.47 + (*"(?a & True) = ?a"*)
5.48 + Thm ("and_false",and_false),
5.49 + (*"(?a & False) = False"*)
5.50 + Thm ("not_true",num_str not_true),
5.51 + (*"(~ True) = False"*)
5.52 + Thm ("not_false",num_str not_false)
5.53 + (*"(~ False) = True"*)],
5.54 + Some "Vereinfache t_",
5.55 + [["simplification","for_polynomials","with_minus"]]));
5.56 +
5.57 +store_pbt
5.58 + (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID
5.59 + (["klammer","polynom","vereinfachen"],
5.60 + [("#Given" ,["term t_"]),
5.61 ("#Where" ,["t_ is_polyexp"]),
5.62 ("#Find" ,["normalform n_"])
5.63 ],
5.64 append_rls "e_rls" e_rls [(*for preds in where_*)
5.65 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
5.66 Some "Vereinfache t_",
5.67 - [["simplification","for_polynomials","with_minus"]]));
5.68 + [["simplification","for_polynomials","with_parentheses"]]));
5.69
5.70 store_pbt
5.71 (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
5.72 @@ -219,6 +259,36 @@
5.73 (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID
5.74 (["simplification","for_polynomials","with_minus"],
5.75 [("#Given" ,["term t_"]),
5.76 + ("#Where" ,["t_ is_polyexp",
5.77 + "Not (matchsub (?a + (?b + ?c)) t_ & \
5.78 + \ matchsub (?a + (?b - ?c)) t_ & \
5.79 + \ matchsub (?a - (?b + ?c)) t_ & \
5.80 + \ matchsub (?a + (?b - ?c)) t_ )"]),
5.81 + ("#Find" ,["normalform n_"])
5.82 + ],
5.83 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
5.84 + prls = append_rls "prls_met_simp_poly_minus" e_rls
5.85 + [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
5.86 + Calc ("Tools.matchsub", eval_matchsub ""),
5.87 + Thm ("and_true",and_true),
5.88 + (*"(?a & True) = ?a"*)
5.89 + Thm ("and_false",and_false),
5.90 + (*"(?a & False) = False"*)
5.91 + Thm ("not_true",num_str not_true),
5.92 + (*"(~ True) = False"*)
5.93 + Thm ("not_false",num_str not_false)
5.94 + (*"(~ False) = True"*)],
5.95 + crls = e_rls, nrls = multipliziere_aus},
5.96 +"Script SimplifyScript (t_::real) = \
5.97 +\ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
5.98 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
5.99 +\ (Try (Rewrite_Set verschoenere False))) t_)"
5.100 + ));
5.101 +
5.102 +store_met
5.103 + (prep_met PolyMinus.thy "met_simp_poly_parenth" [] e_metID
5.104 + (["simplification","for_polynomials","with_parentheses"],
5.105 + [("#Given" ,["term t_"]),
5.106 ("#Where" ,["t_ is_polyexp"]),
5.107 ("#Find" ,["normalform n_"])
5.108 ],
5.109 @@ -227,10 +297,11 @@
5.110 [(*for preds in where_*)
5.111 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
5.112 crls = e_rls, nrls = multipliziere_aus},
5.113 -"Script SimplifyScript (t_::real) = \
5.114 -\ (((Try (Rewrite_Set ordne_alphabetisch False)) @@\
5.115 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
5.116 -\ (Try (Rewrite_Set verschoenere False))) t_)"
5.117 +"Script SimplifyScript (t_::real) = \
5.118 +\ (((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ \
5.119 +\ (Try (Rewrite_Set ordne_alphabetisch False)) @@ \
5.120 +\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
5.121 +\ (Try (Rewrite_Set verschoenere False))) t_)"
5.122 ));
5.123
5.124 store_met
6.1 --- a/src/sml/IsacKnowledge/PolyMinus.thy Fri Dec 28 14:57:38 2007 +0100
6.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy Mon Dec 31 09:55:43 2007 +0100
6.3 @@ -49,5 +49,10 @@
6.4 vorzeichen_minus_weg3 "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
6.5 vorzeichen_minus_weg4 "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
6.6
6.7 + (*klammer_plus_plus = (real_add_assoc RS sym)*)
6.8 + klammer_plus_minus "a + (b - c) = (a + b) - c"
6.9 + klammer_minus_plus "a - (b + c) = (a - b) - c"
6.10 + klammer_minus_minus "a - (b - c) = (a - b) + c"
6.11 +
6.12 end
6.13
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/sml/ME/rewtools.sml Mon Dec 31 09:55:43 2007 +0100
7.3 @@ -0,0 +1,755 @@
7.4 +(* tools for rewriting, reverse rewriting, context to thy concerning rewriting
7.5 + authors: Walther Neuper 2002, 2006
7.6 + (c) due to copyright terms
7.7 +
7.8 +use"ME/rewtools.sml";
7.9 +use"rewtools.sml";
7.10 +*)
7.11 +
7.12 +
7.13 +
7.14 +(***.reverse rewriting.***)
7.15 +
7.16 +(*.derivation for insertin one level of nodes into the calctree.*)
7.17 +type deriv = (term * rule * (term *term list)) list;
7.18 +
7.19 +fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str' r)^", ("^
7.20 + (term2str t')^", "^(terms2str a)^"))";
7.21 +fun trtas2str trtas = (strs2str o (map trta2str)) trtas;
7.22 +val deriv2str = trtas2str;
7.23 +fun rta2str (r,(t,a)) = "\n("^(rule2str' r)^", ("^
7.24 + (term2str t)^", "^(terms2str a)^"))";
7.25 +fun rtas2str rtas = (strs2str o (map rta2str)) rtas;
7.26 +val deri2str = rtas2str;
7.27 +
7.28 +
7.29 +(*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*)
7.30 +fun sym_thm thm =
7.31 + let
7.32 + val {sign_ref = sign_ref, der = der, maxidx = maxidx,
7.33 + shyps = shyps, hyps = hyps, (*tpairs = tpairs,*) prop = prop} =
7.34 + rep_thm_G thm;
7.35 + val (lhs,rhs) = (dest_equals' o strip_trueprop
7.36 + o Logic.strip_imp_concl) prop;
7.37 + val prop' = case strip_imp_prems' prop of
7.38 + None => Trueprop $ (mk_equality (rhs, lhs))
7.39 + | Some cs =>
7.40 + ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
7.41 + in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;
7.42 +(*
7.43 + (sym RS real_mult_div_cancel1) handle e => print_exn e;
7.44 +Exception THM 1 raised:
7.45 +RSN: no unifiers
7.46 +"?s = ?t ==> ?t = ?s"
7.47 +"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"
7.48 +
7.49 + val thm = real_mult_div_cancel1;
7.50 + val prop = (#prop o rep_thm) thm;
7.51 + atomt prop;
7.52 + val ppp = Logic.strip_imp_concl prop;
7.53 + atomt ppp;
7.54 + ((#prop o rep_thm o sym_thm o sym_thm) thm) = (#prop o rep_thm) thm;
7.55 +val it = true : bool
7.56 + ((sym_thm o sym_thm) thm) = thm;
7.57 +val it = true : bool
7.58 +
7.59 + val thm = real_le_anti_sym;
7.60 + ((sym_thm o sym_thm) thm) = thm;
7.61 +val it = true : bool
7.62 +
7.63 + val thm = real_minus_zero;
7.64 + ((sym_thm o sym_thm) thm) = thm;
7.65 +val it = true : bool
7.66 +*)
7.67 +
7.68 +
7.69 +
7.70 +(*.derive normalform of a rls, or derive until Some goal,
7.71 + and record rules applied and rewrites.
7.72 +val it = fn
7.73 + : theory
7.74 + -> rls
7.75 + -> rule list
7.76 + -> rew_ord : the order of this rls, which 1 theorem of is used
7.77 + for rewriting 1 single step (?14.4.03)
7.78 + -> term option : 040214 ??? nonsense ???
7.79 + -> term
7.80 + -> (term * : to this term ...
7.81 + rule * : ... this rule is applied yielding ...
7.82 + (term * : ... this term ...
7.83 + term list)) : ... under these assumptions.
7.84 + list :
7.85 +returns empty list for a normal form
7.86 +FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
7.87 +
7.88 +WN060825 too complicated for the intended use by cancel_, common_nominator_
7.89 +and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
7.90 + -- replaced below*)
7.91 +(* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);
7.92 + val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, None, tt);
7.93 + *)
7.94 +fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
7.95 + let datatype switch = Appl | Noap
7.96 + fun rew_once lim rts t Noap [] =
7.97 + (case goal of
7.98 + None => rts
7.99 + | Some g =>
7.100 + raise error ("make_deriv: no derivation for "^(term2str t)))
7.101 + | rew_once lim rts t Appl [] =
7.102 + (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
7.103 + (*| Seq _ => rts) FIXXXXXME 14.3.03*)
7.104 + | rew_once lim rts t apno rs' =
7.105 + (case goal of
7.106 + None => rew_or_calc lim rts t apno rs'
7.107 + | Some g =>
7.108 + if g = t then rts
7.109 + else rew_or_calc lim rts t apno rs')
7.110 + and rew_or_calc lim rts t apno (rrs' as (r::rs')) =
7.111 + if lim < 0
7.112 + then (writeln ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
7.113 + "with deriv =\n"); writeln (deriv2str rts); rts)
7.114 + else
7.115 + case r of
7.116 + Thm (thmid, tm) =>
7.117 + (if not (!trace_rewrite) then () else
7.118 + writeln ("### trying thm '" ^ thmid ^ "'");
7.119 + case rewrite_ thy ro erls true tm t of
7.120 + None => rew_once lim rts t apno rs'
7.121 + | Some (t',a') =>
7.122 + (if ! trace_rewrite
7.123 + then writeln ("### rewrites to: "^(term2str t')) else();
7.124 + rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))
7.125 + | Calc (c as (op_,_)) =>
7.126 + let val _ = if not (!trace_rewrite) then () else
7.127 + writeln ("### trying calc. '" ^ op_ ^ "'")
7.128 + val t = app_num_tr'2 t
7.129 + in case get_calculation_ thy c t of
7.130 + None => rew_once lim rts t apno rs'
7.131 + | Some (thmid, tm) =>
7.132 + (let val Some (t',a') = rewrite_ thy ro erls true tm t
7.133 + val _ = if not (!trace_rewrite) then () else
7.134 + writeln("### calc. to: " ^ (term2str t'))
7.135 + val r' = Thm (thmid, tm)
7.136 + in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
7.137 + end)
7.138 + handle _ => raise error "derive_norm, Calc: no rewrite"
7.139 + end
7.140 + | Rls_ rls =>
7.141 + (case rewrite_set_ thy true rls t of
7.142 + None => rew_once lim rts t apno rs'
7.143 + | Some (t',a') =>
7.144 + rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');
7.145 +(*WN060829 | Rls_ rls =>
7.146 + (case rewrite_set_ thy true rls t of
7.147 + None => rew_once lim rts t apno rs'
7.148 + | Some (t',a') =>
7.149 + if ro [] (t, t') then rew_once lim rts t apno rs'
7.150 + else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs');
7.151 +...lead to deriv = [] with make_polynomial.
7.152 +THERE IS SOMETHING DIFFERENT beetween rewriting with the code above
7.153 +and between rewriting with rewrite_set: with rules from make_polynomial and
7.154 +t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code
7.155 +leads to cycling Rls_ order_mult_rls_..Rls_ discard_parentheses_..Rls_ order..
7.156 +*)
7.157 + in rew_once (!lim_deriv) [] tt Noap rs end;
7.158 +
7.159 +
7.160 +(*.toggles the marker for 'fun sym_thm'.*)
7.161 +fun sym_thmID (thmID : thmID) =
7.162 + case explode thmID of
7.163 + "s"::"y"::"m"::"_"::id => implode id : thmID
7.164 + | id => "sym_"^thmID;
7.165 +(*
7.166 +> val thmID = "sym_real_mult_2";
7.167 +> sym_thmID thmID;
7.168 +val it = "real_mult_2" : string
7.169 +> val thmID = "real_num_collect";
7.170 +> sym_thmID thmID;
7.171 +val it = "sym_real_num_collect" : string*)
7.172 +fun sym_drop (thmID : thmID) =
7.173 + case explode thmID of
7.174 + "s"::"y"::"m"::"_"::id => implode id : thmID
7.175 + | id => thmID;
7.176 +fun is_sym (thmID : thmID) =
7.177 + case explode thmID of
7.178 + "s"::"y"::"m"::"_"::id => true
7.179 + | id => false;
7.180 +
7.181 +
7.182 +(*FIXXXXME.040219: detail has to handle Rls id="sym_..."
7.183 + by applying make_deriv, rev_deriv'; see concat_deriv*)
7.184 +fun sym_rls Erls = Erls
7.185 + | sym_rls (Rls {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =
7.186 + Rls {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls,
7.187 + rules=rules, rew_ord=rew_ord, preconds=preconds}
7.188 + | sym_rls (Seq {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =
7.189 + Seq {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls,
7.190 + rules=rules, rew_ord=rew_ord, preconds=preconds}
7.191 + | sym_rls (Rrls {id, scr, calc, erls, prepat, rew_ord}) =
7.192 + Rrls {id="sym_"^id, scr=scr, calc=calc, erls=erls, prepat=prepat,
7.193 + rew_ord=rew_ord};
7.194 +
7.195 +fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
7.196 + | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
7.197 + | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
7.198 +(*
7.199 + val th = Thm ("real_one_collect",num_str real_one_collect);
7.200 + sym_Thm th;
7.201 +val th =
7.202 + Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")
7.203 + : rule
7.204 +ML> val it =
7.205 + Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)
7.206 +
7.207 +
7.208 +(*version for reverse rewrite used before 040214*)
7.209 +fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
7.210 +(* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, None, t');
7.211 + *)
7.212 +fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
7.213 + (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);
7.214 +(*
7.215 + val rev_rew = reverse_deriv thy e_rls ;
7.216 + writeln(rtas2str rev_rew);
7.217 +*)
7.218 +
7.219 +fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2
7.220 + | eq_Thm (Thm (id1,_), _) = false
7.221 + | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2
7.222 + | eq_Thm (Rls_ r1, _) = false
7.223 + | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^
7.224 + (rule2str r1)^"' '"^(rule2str r2)^"'");
7.225 +fun distinct_Thm r = gen_distinct eq_Thm r;
7.226 +
7.227 +fun eq_Thms thmIDs thm = ((id_of_thm thm) mem thmIDs)
7.228 + handle _ => false;
7.229 +
7.230 +
7.231 +
7.232 +
7.233 +(***. context to thy concerning rewriting .***)
7.234 +
7.235 +(*.create the unique handles and filenames for the theory-data.*)
7.236 +fun part2guh ([str]:theID) =
7.237 + (case str of
7.238 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
7.239 + | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
7.240 + | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
7.241 + | str => raise error ("thy2guh: called with '"^str^"'"))
7.242 + | part2guh theID = raise error ("part2guh called with theID = "
7.243 + ^ theID2str theID);
7.244 +fun part2filename str = part2guh str ^ ".xml" : filename;
7.245 +
7.246 +
7.247 +fun thy2guh ([part, thyID]:theID) =
7.248 + (case part of
7.249 + "Isabelle" => "thy_isab_" ^ thyID : guh
7.250 + | "IsacScripts" => "thy_scri_" ^ thyID
7.251 + | "IsacKnowledge" => "thy_isac_" ^ thyID
7.252 + | str => raise error ("thy2guh: called with '"^str^"'"))
7.253 + | thy2guh theID = raise error ("thy2guh called with '"^strs2str' theID^"'");
7.254 +fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;
7.255 +fun thypart2guh ([part, thyID, thypart]:theID) =
7.256 + case part of
7.257 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
7.258 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
7.259 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
7.260 + | str => raise error ("thypart2guh: called with '"^str^"'");
7.261 +fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;
7.262 +
7.263 +(*.convert the data got via contextToThy to a globally unique handle
7.264 + there is another way to get the guh out of the 'theID' in the hierarchy.*)
7.265 +fun thm2guh (isa, thyID:thyID) (thmID:thmID) =
7.266 + case isa of
7.267 + "Isabelle" =>
7.268 + "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
7.269 + | "IsacKnowledge" =>
7.270 + "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
7.271 + | "IsacScripts" =>
7.272 + "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
7.273 + | str => raise error ("thm2guh called with isa = '"^isa^
7.274 + "' for thm = "^thmID^"'");
7.275 +fun thm2filename (isa_thyID: string * thyID) thmID =
7.276 + (thm2guh isa_thyID thmID) ^ ".xml" : filename;
7.277 +
7.278 +fun rls2guh (isa, thyID:thyID) (rls':rls') =
7.279 + case isa of
7.280 + "Isabelle" =>
7.281 + "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
7.282 + | "IsacKnowledge" =>
7.283 + "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
7.284 + | "IsacScripts" =>
7.285 + "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
7.286 + | str => raise error ("rls2guh called with isa = '"^isa^
7.287 + "' for rls = '"^rls'^"'");
7.288 + fun rls2filename (isa, thyID) rls' =
7.289 + rls2guh (isa, thyID) rls' ^ ".xml" : filename;
7.290 +
7.291 +fun cal2guh (isa, thyID:thyID) calID =
7.292 + case isa of
7.293 + "Isabelle" =>
7.294 + "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
7.295 + | "IsacKnowledge" =>
7.296 + "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
7.297 + | "IsacScripts" =>
7.298 + "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
7.299 + | str => raise error ("cal2guh called with isa = '"^isa^
7.300 + "' for cal = '"^calID^"'");
7.301 +fun cal2filename (isa, thyID:thyID) calID =
7.302 + cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;
7.303 +
7.304 +fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') =
7.305 + case isa of
7.306 + "Isabelle" =>
7.307 + "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
7.308 + | "IsacKnowledge" =>
7.309 + "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
7.310 + | "IsacScripts" =>
7.311 + "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
7.312 + | str => raise error ("ord2guh called with isa = '"^isa^
7.313 + "' for ord = '"^rew_ord'^"'");
7.314 +fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =
7.315 + ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;
7.316 +
7.317 +
7.318 +(**.set up isab_thm_thy in Isac.ML.**)
7.319 +
7.320 +fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm));
7.321 +fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm));
7.322 +
7.323 +(*.lookup the missing theorems in some thy (of Isabelle).*)
7.324 +fun make_isa missthms thy =
7.325 + map (pair (theory2thyID thy))
7.326 + (curry (gen_inter eq_thmI) missthms (thms_of thy))
7.327 + : (thyID * (thmID * Thm.thm)) list;
7.328 +
7.329 +(*.separate handling of sym_thms.*)
7.330 +fun make_isab rlsthmsNOTisac isab_thys =
7.331 + let fun les ((s1,_), (s2,_)) = (s1 : string) < s2
7.332 + val notsym = filter_out (is_sym o #1) rlsthmsNOTisac
7.333 + val notsym_isab = (flat o (map (make_isa notsym))) isab_thys
7.334 +
7.335 + val sym = filter (is_sym o #1) rlsthmsNOTisac
7.336 +
7.337 + val symsym = map ((apfst sym_drop) o (apsnd sym_thm)) sym
7.338 + val symsym_isab = (flat o (map (make_isa symsym))) isab_thys
7.339 +
7.340 + val sym_isab = map (((apsnd o apfst) sym_drop) o
7.341 + ((apsnd o apsnd) sym_thm)) symsym_isab
7.342 +
7.343 + val isab = notsym_isab @ symsym_isab @ sym_isab
7.344 + in ((map rearrange) o (gen_sort les)) isab
7.345 + : (thmID * (thyID * Thm.thm)) list
7.346 + end;
7.347 +
7.348 +(*.which theory below thy' contains a theorem; this can be in isabelle !
7.349 +get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
7.350 +(* val (str, (_, thy)) = ("real_diff_minus", ("Root.thy", Root.thy));
7.351 + val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));
7.352 + *)
7.353 +fun thy_contains_thm (str:xstring) (_, thy) =
7.354 + str mem (map (strip_thy o fst) (thms_of thy));
7.355 +(* val (thy', str) = ("Isac.thy", "real_mult_minus1");
7.356 + val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
7.357 + *)
7.358 +fun thy_containing_thm (thy':theory') (str:xstring) =
7.359 + let val thy' = thyID2theory' thy'
7.360 + val str = sym_drop str
7.361 + val startsearch = dropuntil ((curry op= thy') o
7.362 + (#1:theory' * theory -> theory'))
7.363 + (rev (!theory'))
7.364 + in case find_first (thy_contains_thm str) startsearch of
7.365 + Some (thy',_) => ("IsacKnowledge", thy')
7.366 + | None => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of
7.367 + Some (thyID,_) => ("Isabelle", thyID)
7.368 + | None =>
7.369 + raise error ("thy_containing_thm: theorem '"^str^
7.370 + "' not in !theory' above thy '"^thy'^"'"))
7.371 + end;
7.372 +
7.373 +
7.374 +(*.which theory below thy' contains a ruleset;
7.375 +get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
7.376 +(* val (thy', rls') = ("PolyEq.thy", "separate_bdv");
7.377 + *)
7.378 +fun thy_containing_rls (thy':theory') (rls':rls') =
7.379 + let val rls' = strip_thy rls'
7.380 + val thy' = thyID2theory' thy'
7.381 + (*take thys between "Isac" and thy' not to search #1#*)
7.382 + val dropthys = takewhile [] (not o (curry op= thy') o
7.383 + (#1:theory' * theory -> theory'))
7.384 + (rev (!theory'))
7.385 + val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
7.386 + dropthys
7.387 + (*drop those rulesets which are generated in a theory found in #1#*)
7.388 + val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
7.389 + ((#1 o #2) : rls' * (theory' * rls)
7.390 + -> theory'))
7.391 + (rev (!ruleset'))
7.392 + in case assoc (startsearch, rls') of
7.393 + Some (thy', _) => ("IsacKnowledge", thyID2theory' thy')
7.394 + | _ => raise error ("thy_containing_rls : rls '"^rls'^
7.395 + "' not in !rulset' above thy '"^thy'^"'")
7.396 + end;
7.397 +(* val (thy', termop) = (thyID, termop);
7.398 + *)
7.399 +fun thy_containing_cal (thy':theory') termop =
7.400 + let val thy' = thyID2theory' thy'
7.401 + val dropthys = takewhile [] (not o (curry op= thy') o
7.402 + (#1:theory' * theory -> theory'))
7.403 + (rev (!theory'))
7.404 + val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
7.405 + dropthys
7.406 + val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
7.407 + (#1 : calc -> string)) (rev (!calclist'))
7.408 + in case assoc (startsearch, strip_thy termop) of
7.409 + Some (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
7.410 + | _ => raise error ("thy_containing_rls : rls '"^termop^
7.411 + "' not in !calclist' above thy '"^thy'^"'")
7.412 + end;
7.413 +
7.414 +(* print_depth 99; map #1 startsearch; print_depth 3;
7.415 + *)
7.416 +
7.417 +(*.packing return-values to matchTheory, contextToThy for xml-generation.*)
7.418 +datatype contthy = (*also an item from KEStore on Browser ......#*)
7.419 + EContThy (*not from KEStore ...........................*)
7.420 + | ContThm of (*a theorem in contex =============*)
7.421 + {thyID : thyID, (*for *2guh in sub-elems here .*)
7.422 + thm : guh, (*theorem in the context .*)
7.423 + applto : term, (*applied to formula ... .*)
7.424 + applat : term, (*... with lhs inserted .*)
7.425 + reword : rew_ord', (*order used for rewrite .*)
7.426 + asms : (term (*asumption instantiated .*)
7.427 + * term) list, (*asumption evaluated .*)
7.428 + lhs : term (*lhs of the theorem ... #*)
7.429 + * term, (*... instantiated .*)
7.430 + rhs : term (*rhs of the theorem ... #*)
7.431 + * term, (*... instantiated .*)
7.432 + result : term, (*resulting from the rewrite .*)
7.433 + resasms : term list, (*... with asms stored .*)
7.434 + asmrls : rls' (*ruleset for evaluating asms .*)
7.435 + }
7.436 + | ContThmInst of (*a theorem with bdvs in contex ======== *)
7.437 + {thyID : thyID, (*for *2guh in sub-elems here .*)
7.438 + thm : guh, (*theorem in the context .*)
7.439 + bdvs : subst, (*bound variables to modify....*)
7.440 + thminst : term, (*... theorem instantiated .*)
7.441 + applto : term, (*applied to formula ... .*)
7.442 + applat : term, (*... with lhs inserted .*)
7.443 + reword : rew_ord', (*order used for rewrite .*)
7.444 + asms : (term (*asumption instantiated .*)
7.445 + * term) list, (*asumption evaluated .*)
7.446 + lhs : term (*lhs of the theorem ... #*)
7.447 + * term, (*... instantiated .*)
7.448 + rhs : term (*rhs of the theorem ... #*)
7.449 + * term, (*... instantiated .*)
7.450 + result : term, (*resulting from the rewrite .*)
7.451 + resasms : term list, (*... with asms stored .*)
7.452 + asmrls : rls' (*ruleset for evaluating asms .*)
7.453 + }
7.454 + | ContRls of (*a rule set in contex ===================== *)
7.455 + {thyID : thyID, (*for *2guh in sub-elems here .*)
7.456 + rls : guh, (*rule set in the context .*)
7.457 + applto : term, (*rewrite this formula .*)
7.458 + result : term, (*resulting from the rewrite .*)
7.459 + asms : term list (*... with asms stored .*)
7.460 + }
7.461 + | ContRlsInst of (*a rule set with bdvs in contex ======= *)
7.462 + {thyID : thyID, (*for *2guh in sub-elems here .*)
7.463 + rls : guh, (*rule set in the context .*)
7.464 + bdvs : subst, (*for bound variables in thms .*)
7.465 + applto : term, (*rewrite this formula .*)
7.466 + result : term, (*resulting from the rewrite .*)
7.467 + asms : term list (*... with asms stored .*)
7.468 + }
7.469 + | ContNOrew of (*no rewrite for thm or rls ============== *)
7.470 + {thyID : thyID, (*for *2guh in sub-elems here .*)
7.471 + thm_rls : guh, (*thm or rls in the context .*)
7.472 + applto : term (*rewrite this formula .*)
7.473 + }
7.474 + | ContNOrewInst of (*no rewrite for some instantiation == *)
7.475 + {thyID : thyID, (*for *2guh in sub-elems here .*)
7.476 + thm_rls : guh, (*thm or rls in the context .*)
7.477 + bdvs : subst, (*for bound variables in thms .*)
7.478 + thminst : term, (*... theorem instantiated .*)
7.479 + applto : term (*rewrite this formula .*)
7.480 + };
7.481 +
7.482 +(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
7.483 + pass other tacs unchanged.*)
7.484 +fun get_tac_checked pt ((p,p_) : pos') = get_obj g_tac pt p;
7.485 +
7.486 +(*..*)
7.487 +
7.488 +
7.489 +
7.490 +(*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*)
7.491 +(* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac';
7.492 + *)
7.493 +fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) =
7.494 + (case applicable_in pos pt tac of
7.495 + Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>
7.496 + let val thy = assoc_thy thy'
7.497 + val thm = (norm o #prop o rep_thm o (get_thm thy)) thmID
7.498 + (*WN060616 the following must be done on subterm found _IN_ rew_sub
7.499 + val (lhs,rhs) = (dest_equals' o strip_trueprop
7.500 + o Logic.strip_imp_concl) thm
7.501 + val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)
7.502 + val thm' = ren_inst (insts, thm, lhs, f)
7.503 + val (lhs',rhs') = (dest_equals' o strip_trueprop
7.504 + o Logic.strip_imp_concl) thm'
7.505 + val asms = map strip_trueprop (Logic.strip_imp_prems thm)
7.506 + val asms' = map strip_trueprop (Logic.strip_imp_prems thm')
7.507 + *)
7.508 + in ContThm {thyID = theory'2thyID thy',
7.509 + thm = thm2guh (thy_containing_thm thy' thmID) thmID,
7.510 + applto = f,
7.511 + applat = e_term,
7.512 + reword = ord',
7.513 + asms = [](*asms ~~ asms'*),
7.514 + lhs = (e_term, e_term)(*(lhs, lhs')*),
7.515 + rhs = (e_term, e_term)(*(rhs, rhs')*),
7.516 + result = res,
7.517 + resasms = asm,
7.518 + asmrls = id_rls erls}
7.519 + end
7.520 + | Notappl _ =>
7.521 + let val pp = par_pblobj pt p
7.522 + val thy' = get_obj g_domID pt pp
7.523 + val f = case p_ of
7.524 + Frm => get_obj g_form pt p
7.525 + | Res => (fst o (get_obj g_result pt)) p
7.526 + in ContNOrew {thyID = theory'2thyID thy',
7.527 + thm_rls = thm2guh (thy_containing_thm thy' thmID) thmID,
7.528 + applto = f}
7.529 + end)
7.530 +
7.531 +(* val ((pt,p), tac as Rewrite_Inst (subs, (thmID,_))) = ((pt,pos), tac);
7.532 + *)
7.533 + | context_thy (pt, pos as (p,p_))
7.534 + (tac as Rewrite_Inst (subs, (thmID,_))) =
7.535 + (case applicable_in pos pt tac of
7.536 +(* val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_),
7.537 + f, (res,asm))) = applicable_in p pt tac;
7.538 + *)
7.539 + Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_),
7.540 + f, (res,(*path to subterm,*)asm))) =>
7.541 + let val thm = (norm o #prop o rep_thm o
7.542 + (get_thm (assoc_thy thy'))) thmID
7.543 + val thminst = inst_bdv subst thm
7.544 + (*WN060616 the following must be done on subterm found _IN_ rew_sub
7.545 + val (lhs,rhs) = (dest_equals' o strip_trueprop
7.546 + o Logic.strip_imp_concl) thminst
7.547 + val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)
7.548 + val thm' = ren_inst (insts, thminst, lhs, f)
7.549 + val (lhs',rhs') = (dest_equals' o strip_trueprop
7.550 + o Logic.strip_imp_concl) thm'
7.551 + val asms = map strip_trueprop (Logic.strip_imp_prems thminst)
7.552 + val asms' = map strip_trueprop (Logic.strip_imp_prems thm')
7.553 + *)
7.554 + in ContThmInst {thyID = theory'2thyID thy',
7.555 + thm = thm2guh (thy_containing_thm
7.556 + thy' thmID) thmID,
7.557 + bdvs = subst,
7.558 + thminst = thminst,
7.559 + applto = f,
7.560 + applat = e_term,
7.561 + reword = ord',
7.562 + asms = [](*asms ~~ asms'*),
7.563 + lhs = (e_term, e_term)(*(lhs, lhs')*),
7.564 + rhs = (e_term, e_term)(*(rhs, rhs')*),
7.565 + result = res,
7.566 + resasms = asm,
7.567 + asmrls = id_rls erls}
7.568 + end
7.569 + | Notappl _ =>
7.570 + let val pp = par_pblobj pt p
7.571 + val thy' = get_obj g_domID pt pp
7.572 + val subst = subs2subst (assoc_thy thy') subs
7.573 + val thm = (norm o #prop o rep_thm o
7.574 + (get_thm (assoc_thy thy'))) thmID
7.575 + val thminst = inst_bdv subst thm
7.576 + val f = case p_ of
7.577 + Frm => get_obj g_form pt p
7.578 + | Res => (fst o (get_obj g_result pt)) p
7.579 + in ContNOrewInst {thyID = theory'2thyID thy',
7.580 + thm_rls = thm2guh (thy_containing_thm
7.581 + thy' thmID) thmID,
7.582 + bdvs = subst,
7.583 + thminst = thminst,
7.584 + applto = f}
7.585 + end)
7.586 + | context_thy (pt,p) (tac as Rewrite_Set rls') =
7.587 + (case applicable_in p pt tac of
7.588 + Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) =>
7.589 + ContRls {thyID = theory'2thyID thy',
7.590 + rls = rls2guh (thy_containing_rls thy' rls') rls',
7.591 + applto = f,
7.592 + result = res,
7.593 + asms = asm})
7.594 + | context_thy (pt,p) (tac as Rewrite_Set_Inst (subs, rls')) =
7.595 + (case applicable_in p pt tac of
7.596 + Appl (Rewrite_Set_Inst' (thy', _, subst, rls, f, (res,asm))) =>
7.597 + ContRlsInst {thyID = theory'2thyID thy',
7.598 + rls = rls2guh (thy_containing_rls thy' rls') rls',
7.599 + bdvs = subst,
7.600 + applto = f,
7.601 + result = res,
7.602 + asms = asm});
7.603 +
7.604 +(*.get all theorems in a rule set (recursivley containing rule sets).*)
7.605 +fun thm_of_rule Erule = []
7.606 + | thm_of_rule (thm as Thm _) = [thm]
7.607 + | thm_of_rule (Calc _) = []
7.608 + | thm_of_rule (Rls_ rls) = thms_of_rls rls
7.609 +and thms_of_rls Erls = []
7.610 + | thms_of_rls (Rls {rules,...}) = (flat o (map thm_of_rule)) rules
7.611 + | thms_of_rls (Seq {rules,...}) = (flat o (map thm_of_rule)) rules
7.612 + | thms_of_rls (Rrls _) = [];
7.613 +(* val Hrls {thy_rls = (_, rls),...} =
7.614 + get_the ["IsacKnowledge", "Test", "Rulesets", "expand_binomtest"];
7.615 +> thms_of_rls rls;
7.616 + *)
7.617 +
7.618 +(*.not only for thydata, but also for thy's etc.*)
7.619 +fun theID2guh (theID:theID) =
7.620 + case length theID of
7.621 + 0 => raise error ("theID2guh: called with theID = "^strs2str' theID)
7.622 + | 1 => part2guh theID
7.623 + | 2 => thy2guh theID
7.624 + | 3 => thypart2guh theID
7.625 + | 4 => let val [isa, thyID, typ, elemID] = theID
7.626 + in case typ of
7.627 + "Theorems" => thm2guh (isa, thyID) elemID
7.628 + | "Rulesets" => rls2guh (isa, thyID) elemID
7.629 + | "Calculations" => cal2guh (isa, thyID) elemID
7.630 + | "Orders" => ord2guh (isa, thyID) elemID
7.631 + | "Theorems" => thy2guh [isa, thyID]
7.632 + | str => raise error ("theID2guh: called with theID = "^
7.633 + strs2str' theID)
7.634 + end
7.635 + | n => raise error ("theID2guh called with theID = "^strs2str' theID);
7.636 +(*.filenames not only for thydata, but also for thy's etc.*)
7.637 +fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
7.638 +
7.639 +fun guh2theID (guh:guh) =
7.640 + let val guh' = explode guh
7.641 + val part = implode (take_fromto 1 4 guh')
7.642 + val isa = implode (take_fromto 5 9 guh')
7.643 + in if not (part mem ["exp_", "thy_", "pbl_", "met_"])
7.644 + then raise error ("guh '"^guh^"' does not begin with \
7.645 + \exp_ | thy_ | pbl_ | met_")
7.646 + else let val chap = case isa of
7.647 + "isab_" => "Isabelle"
7.648 + | "scri_" => "IsacScripts"
7.649 + | "isac_" => "IsacKnowledge"
7.650 + | _ =>
7.651 + raise error ("guh2theID: '"^guh^
7.652 + "' does not have isab_ | scri_ | \
7.653 + \isac_ at position 5..9")
7.654 + val rest = takerest (9, guh')
7.655 + val thyID = takewhile [] (not o (curry op= "-")) rest
7.656 + val rest' = dropuntil (curry op= "-") rest
7.657 + in case implode rest' of
7.658 + "-part" => [chap] : theID
7.659 + | "" => [chap, implode thyID]
7.660 + | "-Theorems" => [chap, implode thyID, "Theorems"]
7.661 + | "-Rulesets" => [chap, implode thyID, "Rulesets"]
7.662 + | "-Operations" => [chap, implode thyID, "Operations"]
7.663 + | "-Orders" => [chap, implode thyID, "Orders"]
7.664 + | _ =>
7.665 + let val sect = implode (take_fromto 1 5 rest')
7.666 + val sect' =
7.667 + case sect of
7.668 + "-thm-" => "Theorems"
7.669 + | "-rls-" => "Rulesets"
7.670 + | "-cal-" => "Operations"
7.671 + | "-ord-" => "Orders"
7.672 + | str =>
7.673 + raise error ("guh2theID: '"^guh^"' has '"^sect^
7.674 + "' instead -thm- | -rls- | \
7.675 + \-cal- | -ord-")
7.676 + in [chap, implode thyID, sect', implode
7.677 + (takerest (5, rest'))]
7.678 + end
7.679 + end
7.680 + end;
7.681 +(*> guh2theID "thy_isac_Biegelinie-Theorems";
7.682 +val it = ["IsacKnowledge", "Biegelinie", "Theorems"] : theID
7.683 +> guh2theID "thy_scri_ListG-thm-zip_Nil";
7.684 +val it = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] : theID*)
7.685 +
7.686 +fun guh2filename (guh : guh) = guh ^ ".xml" : filename;
7.687 +
7.688 +
7.689 +(*..*)
7.690 +fun guh2rewtac (guh:guh) ([] : subs) =
7.691 + let val [isa, thy, sect, xstr] = guh2theID guh
7.692 + in case sect of
7.693 + "Theorems" => Rewrite (xstr, "")
7.694 + | "Rulesets" => Rewrite_Set xstr
7.695 + | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'")
7.696 + end
7.697 + | guh2rewtac (guh:guh) subs =
7.698 + let val [isa, thy, sect, xstr] = guh2theID guh
7.699 + in case sect of
7.700 + "Theorems" => Rewrite_Inst (subs, (xstr, ""))
7.701 + | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
7.702 + | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'")
7.703 + end;
7.704 +(*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];
7.705 +val it = Rewrite ("constant_mult_square", "") : tac
7.706 +> guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"];
7.707 +val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac
7.708 +> guh2rewtac "thy_isac_Test-rls-Test_simplify" [];
7.709 +val it = Rewrite_Set "Test_simplify" : tac
7.710 +> guh2rewtac "thy_isac_Test-rls-isolate_bdv" ["(bdv, x)"];
7.711 +val it = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") : tac*)
7.712 +
7.713 +
7.714 +(*.the front-end may request a context for any element of the hierarchy.*)
7.715 +(* val guh = "thy_isac_Test-rls-Test_simplify";
7.716 + *)
7.717 +fun no_thycontext (guh : guh) = (guh2theID guh; false)
7.718 + handle _ => true;
7.719 +
7.720 +(*> has_thycontext "thy_isac_Test";
7.721 +if has_thycontext "thy_isac_Test" then "OK" else "NOTOK";
7.722 + *)
7.723 +
7.724 +
7.725 +
7.726 +(*.get the substitution of bound variables for matchTheory:
7.727 + # lookup the thm|rls' in the script
7.728 + # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
7.729 + # instantiate this subs with the istates env to [(bdv, x),..]
7.730 + # otherwise [].*)
7.731 +(*WN060617 hack assuming that all scripts use only one bound variable
7.732 +and use 'v_' as the formal argument for this bound variable*)
7.733 +(* val (ScrState (env,_,_,_,_,_), _, guh) = (is, "dummy", guh);
7.734 + *)
7.735 +fun subs_from (ScrState (env,_,_,_,_,_)) _(*:Script sc*) (guh:guh) =
7.736 + let val theID as [isa, thyID, sect, xstr] = guh2theID guh
7.737 + in case sect of
7.738 + "Theorems" =>
7.739 + let val thm = get_thm (assoc_thy (thyID2theory' thyID)) xstr
7.740 + in if contains_bdv thm
7.741 + then let val formal_arg = str2term "v_"
7.742 + val value = subst_atomic env formal_arg
7.743 + in ["(bdv," ^ term2str value ^ ")"]:subs end
7.744 + else []
7.745 + end
7.746 + | "Rulesets" =>
7.747 + let val rules = (get_rules o assoc_rls) xstr
7.748 + in if contain_bdv rules
7.749 + then let val formal_arg = str2term"v_"
7.750 + val value = subst_atomic env formal_arg
7.751 + in ["(bdv,"^term2str value^")"]:subs end
7.752 + else []
7.753 + end
7.754 + end;
7.755 +
7.756 +(* use"ME/rewtools.sml";
7.757 + *)
7.758 +
8.1 --- a/src/sml/ROOT.ML Fri Dec 28 14:57:38 2007 +0100
8.2 +++ b/src/sml/ROOT.ML Mon Dec 31 09:55:43 2007 +0100
8.3 @@ -122,6 +122,7 @@
8.4 use"rewrite.sml";
8.5 use"scrtools.sml";
8.6 use"term_G.sml";
8.7 + use"tools.sml";
8.8 cd "../..";
8.9 cd"smltest/ME";
8.10 use"ctree.sml";
9.1 --- a/src/sml/RTEST-root.sml Fri Dec 28 14:57:38 2007 +0100
9.2 +++ b/src/sml/RTEST-root.sml Mon Dec 31 09:55:43 2007 +0100
9.3 @@ -32,6 +32,7 @@
9.4 use"rewrite.sml";
9.5 use"scrtools.sml";
9.6 use"term_G.sml";
9.7 + use"tools.sml";
9.8 cd "../..";
9.9 cd"smltest/ME";
9.10 use"ctree.sml";
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/sml/Scripts/Tools.ML Mon Dec 31 09:55:43 2007 +0100
10.3 @@ -0,0 +1,199 @@
10.4 +(* auxiliary functions for scripts
10.5 + WN.9.00
10.6 +*)
10.7 +(* use"~/proto2/isac/src/sml/Scripts/Tools.ML";
10.8 + *)
10.9 +
10.10 +
10.11 +(*11.02: for equation solving only*)
10.12 +val UniversalList = (term_of o the o (parse Tools.thy)) "UniversalList";
10.13 +val EmptyList = (term_of o the o (parse Tools.thy)) "[]::bool list";
10.14 +
10.15 +
10.16 +
10.17 +(*+ for Or_to_List +*)
10.18 +fun or2list (Const ("True",_)) = (writeln"### or2list True";UniversalList)
10.19 + | or2list (Const ("False",_)) = (writeln"### or2list False";EmptyList)
10.20 + | or2list (t as Const ("op =",_) $ _ $ _) =
10.21 + (writeln"### or2list _ = _";list2isalist bool [t])
10.22 + | or2list ors =
10.23 + (writeln"### or2list _ | _";
10.24 + let fun get ls (Const ("op |",_) $ o1 $ o2) =
10.25 + case o2 of
10.26 + Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2
10.27 + | _ => ls @ [o1, o2]
10.28 + in (((list2isalist bool) o (get [])) ors)
10.29 + handle _ => raise error ("or2list: no ORs= "^(term2str ors)) end
10.30 + );
10.31 +(*>val t = HOLogic.true_const;
10.32 +> val t' = or2list t;
10.33 +> term2str t';
10.34 +"Atools.UniversalList"
10.35 +> val t = HOLogic.false_const;
10.36 +> val t' = or2list t;
10.37 +> term2str t';
10.38 +"[]"
10.39 +> val t=(term_of o the o (parse thy)) "x=3";
10.40 +> val t' = or2list t;
10.41 +> term2str t';
10.42 +"[x = 3]"
10.43 +> val t=(term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
10.44 +> val t' = or2list t;
10.45 +> term2str t';
10.46 +"[x = #3, x = #-3, x = #0]" : string *)
10.47 +
10.48 +
10.49 +
10.50 +
10.51 +(** evaluation on the meta-level **)
10.52 +
10.53 +(*. evaluate the predicate matches (match on whole term only) .*)
10.54 +(*("matches",("Tools.matches",eval_matches "#matches_")):calc*)
10.55 +fun eval_matches (thmid:string) "Tools.matches"
10.56 + (t as Const ("Tools.matches",_) $ pat $ tst) thy =
10.57 + if matches thy tst pat
10.58 + then let val prop = Trueprop $ (mk_equality (t, true_as_term))
10.59 + in Some ((string_of_cterm o cterm_of (sign_of thy)) prop,
10.60 + prop) end
10.61 + else let val prop = Trueprop $ (mk_equality (t, false_as_term))
10.62 + in Some ((string_of_cterm o cterm_of (sign_of thy)) prop,
10.63 + prop) end
10.64 + | eval_matches _ _ _ _ = None;
10.65 +(*
10.66 +> val t = (term_of o the o (parse thy))
10.67 + "matches (?x = 0) (1 * x ^^^ 2 = 0)";
10.68 +> eval_matches "/thmid/" "/op_/" t thy;
10.69 +val it =
10.70 + Some
10.71 + ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
10.72 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
10.73 +
10.74 +> val t = (term_of o the o (parse thy))
10.75 + "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
10.76 +> eval_matches "/thmid/" "/op_/" t thy;
10.77 +val it =
10.78 + Some
10.79 + ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
10.80 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
10.81 +
10.82 +> val t = (term_of o the o (parse thy))
10.83 + "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
10.84 +> eval_matches "/thmid/" "/op_/" t thy;
10.85 +val it =
10.86 + Some
10.87 + ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
10.88 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
10.89 +
10.90 +> val t = (term_of o the o (parse thy))
10.91 + "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
10.92 +> eval_matches "/thmid/" "/op_/" t thy;
10.93 +val it =
10.94 + Some
10.95 + ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
10.96 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
10.97 +----- before ?patterns ---:
10.98 +> val t = (term_of o the o (parse thy))
10.99 + "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
10.100 +> eval_matches "/thmid/" "/op_/" t thy;
10.101 +Some
10.102 + ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
10.103 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
10.104 + : (string * term) option
10.105 +
10.106 +> val t = (term_of o the o (parse thy))
10.107 + "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
10.108 +> eval_matches "/thmid/" "/op_/" t thy;
10.109 +Some ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
10.110 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
10.111 +
10.112 +> val t = (term_of o the o (parse thy))
10.113 + "matches (a = b) (x + #1 + #-1 * #2 = #0)";
10.114 +> eval_matches "/thmid/" "/op_/" t thy;
10.115 +Some ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
10.116 +*)
10.117 +
10.118 +(*.does a pattern match some subterm ?.*)
10.119 +fun matchsub thy t pat =
10.120 + let fun matchs (t as Const _) = matches thy t pat
10.121 + | matchs (t as Free _) = matches thy t pat
10.122 + | matchs (t as Var _) = matches thy t pat
10.123 + | matchs (Bound _) = false
10.124 + | matchs (t as Abs (_, _, body)) =
10.125 + if matches thy t pat then true else matches thy body pat
10.126 + | matchs (t as f1 $ f2) =
10.127 + if matches thy t pat then true
10.128 + else if matchs f1 then true else matchs f2
10.129 + in matchs t end;
10.130 +
10.131 +(*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*)
10.132 +fun eval_matchsub (thmid:string) "Tools.matchsub"
10.133 + (t as Const ("Tools.matchsub",_) $ pat $ tst) thy =
10.134 + if matchsub thy tst pat
10.135 + then let val prop = Trueprop $ (mk_equality (t, true_as_term))
10.136 + in Some ((string_of_cterm o cterm_of (sign_of thy)) prop,
10.137 + prop) end
10.138 + else let val prop = Trueprop $ (mk_equality (t, false_as_term))
10.139 + in Some ((string_of_cterm o cterm_of (sign_of thy)) prop,
10.140 + prop) end
10.141 + | eval_matchsub _ _ _ _ = None;
10.142 +
10.143 +
10.144 +
10.145 +(*get the variables in an isabelle-term*)
10.146 +(*("Vars" ,("Tools.Vars" ,eval_var "#Vars_")):calc*)
10.147 +fun eval_var (thmid:string) "Tools.Vars"
10.148 + (t as (Const(op0,t0) $ arg)) thy =
10.149 + let
10.150 + val t' = ((list2isalist HOLogic.realT) o vars) t;
10.151 + val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
10.152 + in Some (thmId, Trueprop $ (mk_equality (t,t'))) end
10.153 + | eval_var _ _ _ _ = None;
10.154 +
10.155 +fun lhs (Const ("op =",_) $ l $ _) = l
10.156 + | lhs t = error("lhs called with (" ^ term2str t ^ ")");
10.157 +(*("lhs" ,("Tools.lhs" ,eval_lhs "")):calc*)
10.158 +fun eval_lhs _ "Tools.lhs"
10.159 + (t as (Const ("Tools.lhs",_) $ (Const ("op =",_) $ l $ _))) _ =
10.160 + Some ((term2str t) ^ " = " ^ (term2str l),
10.161 + Trueprop $ (mk_equality (t, l)))
10.162 + | eval_lhs _ _ _ _ = None;
10.163 +(*
10.164 +> val t = (term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
10.165 +> val Some (id,t') = eval_lhs 0 0 t 0;
10.166 +val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
10.167 +> term2str t';
10.168 +val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
10.169 +*)
10.170 +
10.171 +fun rhs (Const ("op =",_) $ _ $ r) = r
10.172 + | rhs t = error("rhs called with (" ^ term2str t ^ ")");
10.173 +(*("rhs" ,("Tools.rhs" ,eval_rhs "")):calc*)
10.174 +fun eval_rhs _ "Tools.rhs"
10.175 + (t as (Const ("Tools.rhs",_) $ (Const ("op =",_) $ _ $ r))) _ =
10.176 + Some ((term2str t) ^ " = " ^ (term2str r),
10.177 + Trueprop $ (mk_equality (t, r)))
10.178 + | eval_rhs _ _ _ _ = None;
10.179 +
10.180 +
10.181 +
10.182 +
10.183 +
10.184 +
10.185 +
10.186 +
10.187 +
10.188 +
10.189 +
10.190 +
10.191 +val list_rls = append_rls "list_rls" list_rls
10.192 + [Calc ("Tools.rhs",eval_rhs "")];
10.193 +ruleset' := overwritelthy thy (!ruleset',
10.194 + [("list_rls",list_rls)
10.195 + ]);
10.196 +calclist':= overwritel (!calclist',
10.197 + [("matches",("Tools.matches",eval_matches "#matches_")),
10.198 + ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")),
10.199 + ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
10.200 + ("lhs" ,("Tools.lhs" ,eval_lhs "")),
10.201 + ("rhs" ,("Tools.rhs" ,eval_rhs ""))
10.202 + ]);
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/sml/Scripts/Tools.thy Mon Dec 31 09:55:43 2007 +0100
11.3 @@ -0,0 +1,51 @@
11.4 +(* auxiliary functions used in scripts
11.5 + author: Walther Neuper 000301
11.6 + WN0509 shift into Atools ?!? (because used also in where of models !)
11.7 +
11.8 + (c) copyright due to lincense terms.
11.9 +
11.10 +remove_thy"Tools";
11.11 +use_thy"Scripts/Tools";
11.12 +*)
11.13 +
11.14 +
11.15 +Tools = ListG +
11.16 +
11.17 +types (*for Descript.thy*)
11.18 +
11.19 + (***********************************************************************)
11.20 + (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*)
11.21 + (***********************************************************************)
11.22 + nam (* named variables *)
11.23 + una (* unnamed variables *)
11.24 + unl (* unnamed variables of type list, elementwise input prohibited*)
11.25 + str (* structured variables *)
11.26 + toreal (* var with undef real value: forces typing *)
11.27 + toreall (* var with undef real list value: forces typing *)
11.28 + tobooll (* var with undef bool list value: forces typing *)
11.29 + unknow (* input without dsc in fmz=[] *)
11.30 + cpy (* UNUSED: copy-named variables
11.31 + identified by .._0, .._i .._' in pbt *)
11.32 + (***********************************************************************)
11.33 + (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*)
11.34 + (***********************************************************************)
11.35 +
11.36 +arities
11.37 +
11.38 + nam, una, unl, str, toreal, toreall, tobooll, unknow, cpy :: type
11.39 +
11.40 +consts
11.41 +
11.42 + UniversalList :: bool list
11.43 +
11.44 + lhs, rhs :: bool => real (*of an equality*)
11.45 + Vars :: 'a => real list (*get the variables of a term *)
11.46 + matches :: ['a, 'a] => bool
11.47 + matchsub :: ['a, 'a] => bool
11.48 +
11.49 +constdefs
11.50 +
11.51 + Testvar :: "[real, 'a] => bool" (*is a variable in a term: unused 6.5.03*)
11.52 + "Testvar v t == v mem (Vars t)" (*by rewriting only,no Calcunused 6.5.03*)
11.53 +
11.54 +end
12.1 --- a/src/sml/Scripts/term_G.sml Fri Dec 28 14:57:38 2007 +0100
12.2 +++ b/src/sml/Scripts/term_G.sml Mon Dec 31 09:55:43 2007 +0100
12.3 @@ -576,8 +576,8 @@
12.4 val it = false : bool
12.5 *)
12.6
12.7 -(*used for calculating built in binary operations in Isabelle2002->Float.ML
12.8 -fun calc "op +" (n1, n2) = n1+n2
12.9 +(*used for calculating built in binary operations in Isabelle2002->Float.ML*)
12.10 +(*fun calc "op +" (n1, n2) = n1+n2
12.11 | calc "op -" (n1, n2) = n1-n2
12.12 | calc "op *" (n1, n2) = n1*n2
12.13 | calc "HOL.divide"(n1, n2) = n1 div n2
13.1 --- a/src/smltest/IsacKnowledge/poly.sml Fri Dec 28 14:57:38 2007 +0100
13.2 +++ b/src/smltest/IsacKnowledge/poly.sml Mon Dec 31 09:55:43 2007 +0100
13.3 @@ -67,14 +67,13 @@
13.4 "-------- Bsple aus Schalk I -------------------------------------";
13.5 "-------- Bsple aus Schalk I -------------------------------------";
13.6 (*SPB Schalk I p.63 No.267b*)
13.7 - val t = str2term
13.8 - "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
13.9 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.10 - term2str t;
13.11 +val t = str2term
13.12 + "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
13.13 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.14 if (term2str t) =
13.15 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
13.16 then ()
13.17 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.18 +else raise error "poly.sml: diff.behav. in make_polynomial 1";
13.19
13.20 (*SPB Schalk I p.63 No.275b*)
13.21 val t = str2term
13.22 @@ -85,7 +84,7 @@
13.23 "3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \
13.24 \4 * x * y ^^^ 3 +\n-2 * y ^^^ 4"
13.25 then ()
13.26 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.27 +else raise error "poly.sml: diff.behav. in make_polynomial 2";
13.28
13.29 (*SPB Schalk I p.63 No.279b*)
13.30 val t = str2term
13.31 @@ -96,7 +95,7 @@
13.32 if (term2str t) =
13.33 "a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\nc * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4"
13.34 then ()
13.35 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.36 +else raise error "poly.sml: diff.behav. in make_polynomial 3";
13.37
13.38 (*SPB Schalk I p.63 No.291*)
13.39 val t = str2term
13.40 @@ -106,7 +105,7 @@
13.41 if (term2str t) =
13.42 "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
13.43 then ()
13.44 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.45 +else raise error "poly.sml: diff.behav. in make_polynomial 4";
13.46
13.47 (*SPB Schalk I p.64 No.295c*)
13.48 val t = str2term
13.49 @@ -117,7 +116,7 @@
13.50 "169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\
13.51 \ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18"
13.52 then ()
13.53 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.54 +else raise error "poly.sml: diff.behav. in make_polynomial 5";
13.55
13.56 (*SPB Schalk I p.64 No.299a*)
13.57 val t = str2term
13.58 @@ -127,7 +126,7 @@
13.59 if (term2str t) =
13.60 "x ^^^ 2 + -1 * y ^^^ 2"
13.61 then ()
13.62 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.63 +else raise error "poly.sml: diff.behav. in make_polynomial 6";
13.64
13.65 (*SPB Schalk I p.64 No.300c*)
13.66 val t = str2term
13.67 @@ -137,79 +136,62 @@
13.68 if (term2str t) =
13.69 "-1 + 9 * x ^^^ 4 * y ^^^ 2"
13.70 then ()
13.71 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.72 +else raise error "poly.sml: diff.behav. in make_polynomial 7";
13.73
13.74 (*SPB Schalk I p.64 No.302*)
13.75 - val t = str2term
13.76 +val t = str2term
13.77 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
13.78 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.79 - term2str t;
13.80 -if (term2str t) =
13.81 -"0"
13.82 -then ()
13.83 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.84 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.85 +if term2str t = "0" then ()
13.86 +else raise error "poly.sml: diff.behav. in make_polynomial 8";
13.87 (* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
13.88
13.89
13.90 (*SPB Schalk I p.64 No.306a*)
13.91 - val t = str2term
13.92 - "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
13.93 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.94 - term2str t;
13.95 -if (term2str t) =
13.96 -"1 + -2 * x ^^^ 4 + x ^^^ 8"
13.97 -then ()
13.98 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.99 +val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
13.100 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.101 +if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
13.102 +else raise error "poly.sml: diff.behav. in make_polynomial: not confluent \
13.103 + \2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again";
13.104 +
13.105 +
13.106 +(*WN071729 when reducing "rls reduce_012_" for Schaerding,
13.107 +the above resulted in the term below ... but reduces from then correctly*)
13.108 +val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";
13.109 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.110 +if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()
13.111 +else raise error "poly.sml: diff.behav. in make_polynomial 9b";
13.112
13.113 (*SPB Schalk I p.64 No.296a*)
13.114 - val t = str2term
13.115 - "(x - a)^^^3";
13.116 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.117 - term2str t;
13.118 -if (term2str t) =
13.119 -"-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
13.120 -then ()
13.121 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.122 +val t = str2term "(x - a)^^^3";
13.123 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.124 +if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
13.125 +then () else raise error "poly.sml: diff.behav. in make_polynomial 10";
13.126
13.127 (*SPB Schalk I p.64 No.296c*)
13.128 - val t = str2term
13.129 - "(-3*x - 4*y)^^^3";
13.130 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.131 - term2str t;
13.132 +val t = str2term "(-3*x - 4*y)^^^3";
13.133 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.134 if (term2str t) =
13.135 "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
13.136 -then ()
13.137 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.138 +then () else raise error "poly.sml: diff.behav. in make_polynomial 11";
13.139
13.140 (*SPB Schalk I p.62 No.242c*)
13.141 - val t = str2term
13.142 - "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
13.143 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.144 - term2str t;
13.145 -if (term2str t) =
13.146 -"1"
13.147 -then ()
13.148 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.149 +val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
13.150 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.151 +if (term2str t) = "1" then ()
13.152 +else raise error "poly.sml: diff.behav. in make_polynomial 12";
13.153
13.154 (*SPB Schalk I p.60 No.209a*)
13.155 - val t = str2term
13.156 - "a^^^(7-x) * a^^^x";
13.157 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.158 - term2str t;
13.159 -if (term2str t) =
13.160 -"a ^^^ 7"
13.161 -then ()
13.162 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.163 +val t = str2term "a^^^(7-x) * a^^^x";
13.164 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.165 +if term2str t = "a ^^^ 7" then ()
13.166 +else raise error "poly.sml: diff.behav. in make_polynomial 13";
13.167
13.168 (*SPB Schalk I p.60 No.209d*)
13.169 - val t = str2term
13.170 - "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
13.171 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.172 - term2str t;
13.173 -if (term2str t) =
13.174 -"d ^^^ 3"
13.175 -then ()
13.176 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.177 +val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
13.178 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.179 +if term2str t = "d ^^^ 3" then ()
13.180 +else raise error "poly.sml: diff.behav. in make_polynomial 14";
13.181
13.182
13.183 (*---------------------------------------------------------------------*)
13.184 @@ -217,11 +199,10 @@
13.185 (*---------------------------------------------------------------------*)
13.186
13.187 (*Schalk I p.64 No.303*)
13.188 - val t = str2term
13.189 - "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";
13.190 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.191 - term2str t;
13.192 -"1280 * b ^^^ 4";
13.193 +val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";
13.194 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.195 +if term2str t = "1280 * b ^^^ 4" then ()
13.196 +else raise error "poly.sml: diff.behav. in make_polynomial 14b";
13.197 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
13.198
13.199
13.200 @@ -230,100 +211,64 @@
13.201 (*--------------------------------------------------------------------*)
13.202 (*SPO*)
13.203 val t = str2term "a^^^2*a^^^(-2)";
13.204 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.205 - term2str t;
13.206 -if (term2str t) =
13.207 -"1"
13.208 -then ()
13.209 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.210 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.211 +if term2str t = "1" then ()
13.212 +else raise error "poly.sml: diff.behav. in make_polynomial 15";
13.213 (*SPO*)
13.214 val t = str2term "a + a + a";
13.215 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.216 - term2str t;
13.217 -if (term2str t) =
13.218 -"3 * a"
13.219 -then ()
13.220 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.221 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.222 +if term2str t = "3 * a" then ()
13.223 +else raise error "poly.sml: diff.behav. in make_polynomial 16";
13.224 (*SPO*)
13.225 val t = str2term "a + b + b + b";
13.226 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.227 - term2str t;
13.228 -if (term2str t) =
13.229 -"a + 3 * b"
13.230 -then ()
13.231 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.232 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.233 +if term2str t = "a + 3 * b" then ()
13.234 +else raise error "poly.sml: diff.behav. in make_polynomial 17";
13.235 (*SPO*)
13.236 val t = str2term "a^^^2*b*b^^^(-1)";
13.237 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.238 - term2str t;
13.239 -if (term2str t) =
13.240 -"a ^^^ 2"
13.241 -then ()
13.242 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.243 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.244 +if term2str t = "a ^^^ 2" then ()
13.245 +else raise error "poly.sml: diff.behav. in make_polynomial 18";
13.246 (*SPO*)
13.247 val t = str2term "a^^^2*a^^^(-2)";
13.248 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.249 - term2str t;
13.250 -if (term2str t) =
13.251 -"1"
13.252 -then ()
13.253 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.254 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.255 +if (term2str t) = "1" then ()
13.256 +else raise error "poly.sml: diff.behav. in make_polynomial 19";
13.257 (*SPO*)
13.258 val t = str2term "b + a - b";
13.259 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.260 - term2str t;
13.261 -if (term2str t) =
13.262 -"a"
13.263 -then ()
13.264 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.265 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.266 +if (term2str t) = "a" then ()
13.267 +else raise error "poly.sml: diff.behav. in make_polynomial 20";
13.268 (*SPO*)
13.269 -val t = (term_of o the o (parse thy)) "b * a * a";
13.270 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.271 -term2str t;
13.272 -if (term2str t) =
13.273 -"a ^^^ 2 * b"
13.274 -then ()
13.275 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.276 +val t = str2term "b * a * a";
13.277 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.278 +if term2str t = "a ^^^ 2 * b" then ()
13.279 +else raise error "poly.sml: diff.behav. in make_polynomial 21";
13.280 (*SPO*)
13.281 val t = str2term "(a^^^2)^^^3";
13.282 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.283 -term2str t;
13.284 -if (term2str t) =
13.285 -"a ^^^ 6"
13.286 -then ()
13.287 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.288 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.289 +if term2str t = "a ^^^ 6" then ()
13.290 +else raise error "poly.sml: diff.behav. in make_polynomial 22";
13.291 (*SPO*)
13.292 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
13.293 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.294 -term2str t;
13.295 -if (term2str t) =
13.296 -"x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2"
13.297 -then ()
13.298 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.299 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.300 +if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
13.301 +else raise error "poly.sml: diff.behav. in make_polynomial 23";
13.302 (*SPO*)
13.303 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
13.304 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.305 -term2str t;
13.306 -if (term2str t) =
13.307 -"a ^^^ 4"
13.308 -then ()
13.309 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.310 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.311 +if (term2str t) = "a ^^^ 4" then ()
13.312 +else raise error "poly.sml: diff.behav. in make_polynomial 24";
13.313 (*SPO*)
13.314 val t = str2term "a * b * b^^^(-1) + a";
13.315 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.316 -term2str t;
13.317 -if (term2str t) =
13.318 -"2 * a"
13.319 -then ()
13.320 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.321 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.322 +if (term2str t) = "2 * a" then ()
13.323 +else raise error "poly.sml: diff.behav. in make_polynomial 25";
13.324 (*SPO*)
13.325 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
13.326 - val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.327 - term2str t;
13.328 -if (term2str t) =
13.329 -"3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
13.330 -then ()
13.331 -else raise error "poly.sml: diff.behav. in make_polynomial";
13.332 +val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
13.333 +if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
13.334 +then () else raise error "poly.sml: diff.behav. in make_polynomial 26";
13.335
13.336
13.337 (*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
13.338 @@ -332,12 +277,12 @@
13.339 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.340 term2str t;
13.341 if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"
13.342 - then () else raise error "poly.sml: diff.behav. in make_polynomial";(*SPO*)
13.343 + then () else raise error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
13.344 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";
13.345 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
13.346 term2str t;
13.347 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
13.348 - then () else raise error "poly.sml: diff.behav. in make_polynomial";
13.349 + then () else raise error "poly.sml: diff.behav. in make_polynomial 28";
13.350
13.351 "-------- Script 'simplification for_polynomials' ----------------";
13.352 "-------- Script 'simplification for_polynomials' ----------------";
14.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Fri Dec 28 14:57:38 2007 +0100
14.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Mon Dec 31 09:55:43 2007 +0100
14.3 @@ -19,6 +19,7 @@
14.4 "----------- pbl polynom vereinfachen ----------------------------";
14.5 "----------- met probe fuer_polynom ------------------------------";
14.6 "----------- pbl polynom probe -----------------------------------";
14.7 +"----------- pbl klammer polynom vereinfachen p.34 ---------------";
14.8 "-----------------------------------------------------------------";
14.9 "-----------------------------------------------------------------";
14.10 "-----------------------------------------------------------------";
14.11 @@ -200,7 +201,6 @@
14.12 then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
14.13 show_pt pt;
14.14
14.15 -
14.16 "----------- met probe fuer_polynom ------------------------------";
14.17 "----------- met probe fuer_polynom ------------------------------";
14.18 "----------- met probe fuer_polynom ------------------------------";
14.19 @@ -228,19 +228,40 @@
14.20 moveActiveRoot 1;
14.21 autoCalculate 1 CompleteCalc;
14.22 val ((pt,p),_) = get_calc 1;
14.23 -(*if p = ([], Res) andalso
14.24 - term2str (get_obj g_res pt (fst p)) = "11 = 11"
14.25 -then () else raise error "polyminus.sml: Probe 11 = 11";*)
14.26 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11"
14.27 +then () else raise error "polyminus.sml: Probe 11 = 11";
14.28 show_pt pt;
14.29
14.30
14.31 +"----------- pbl klammer polynom vereinfachen p.34 ---------------";
14.32 +"----------- pbl klammer polynom vereinfachen p.34 ---------------";
14.33 +"----------- pbl klammer polynom vereinfachen p.34 ---------------";
14.34 +states:=[];
14.35 +CalcTree [(["term (2*u - 5 - (3 - 4*u) + (8*u + 9))",
14.36 + "normalform N"],
14.37 + ("PolyMinus.thy",["klammer","polynom","vereinfachen"],
14.38 + ["simplification","for_polynomials","with_parentheses"]))];
14.39 +moveActiveRoot 1;
14.40 +autoCalculate 1 CompleteCalc;
14.41 +val ((pt,p),_) = get_calc 1;
14.42 +if p = ([], Res) andalso
14.43 + term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
14.44 +then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
14.45 +show_pt pt;
14.46
14.47 -
14.48 -
14.49 -
14.50 -
14.51 -
14.52 -
14.53 +"----- probe p.34 -----";
14.54 +states:=[];
14.55 +CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)",
14.56 + "mitWert [u = 2]",
14.57 + "Geprueft b"],
14.58 + ("PolyMinus.thy",["polynom","probe"],
14.59 + ["probe","fuer_polynom"]))];
14.60 +moveActiveRoot 1;
14.61 +autoCalculate 1 CompleteCalc;
14.62 +val ((pt,p),_) = get_calc 1;
14.63 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29"
14.64 +then () else raise error "polyminus.sml: Probe 29 = 29";
14.65 +show_pt pt;
14.66
14.67
14.68 (*
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/smltest/Scripts/tools.sml Mon Dec 31 09:55:43 2007 +0100
15.3 @@ -0,0 +1,27 @@
15.4 +(* tests on Tools
15.5 + author: Walther Neuper
15.6 + WN071229,
15.7 + (c) due to copyright terms
15.8 +
15.9 +use"../smltest/Scripts/tools.sml";
15.10 +use"tools.sml";
15.11 +*)
15.12 +val thy = Real.thy;
15.13 +
15.14 +"-----------------------------------------------------------------";
15.15 +"table of contents -----------------------------------------------";
15.16 +"-----------------------------------------------------------------";
15.17 +"----------- fun matchsub ----------------------------------------";
15.18 +"-----------------------------------------------------------------";
15.19 +"-----------------------------------------------------------------";
15.20 +"-----------------------------------------------------------------";
15.21 +
15.22 +
15.23 +"----------- fun matchsub ----------------------------------------";
15.24 +"----------- fun matchsub ----------------------------------------";
15.25 +"----------- fun matchsub ----------------------------------------";
15.26 +if matchsub thy (str2term "(a + (b + c))") (str2term "?x + (?y + ?z)")
15.27 +then () else raise error "tools.sml matchsub a + (b + c)";
15.28 +
15.29 +if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)")
15.30 +then () else raise error "tools.sml matchsub (a + (b + c)) + d";