1.1 --- a/src/sml/IsacKnowledge/Poly.ML Tue Aug 29 11:43:53 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Poly.ML Tue Aug 29 13:30:35 2006 +0200
1.3 @@ -1337,6 +1337,70 @@
1.4 scr = EmptyScr
1.5 }:rls;
1.6
1.7 +(*.a minimal ruleset for reverse rewriting of factions [2];
1.8 + compare expand_binoms.*)
1.9 +val rev_rew_p =
1.10 +Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
1.11 + erls = Atools_erls, srls = Erls,
1.12 + calc = [(*("plus" , ("op +", eval_binop "#add_")),
1.13 + ("times" , ("op *", eval_binop "#mult_")),
1.14 + ("power_", ("Atools.pow", eval_binop "#power_"))*)
1.15 + ],
1.16 + rules = [Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.17 + (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1.18 + Thm ("real_plus_binom_times1" ,num_str real_plus_binom_times1),
1.19 + (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1.20 + Thm ("real_plus_binom_times2" ,num_str real_plus_binom_times2),
1.21 + (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1.22 +
1.23 + Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
1.24 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.25 + Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
1.26 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.27 +
1.28 + Thm ("real_mult_assoc", num_str real_mult_assoc),
1.29 + (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1.30 + Rls_ order_mult_rls_,
1.31 + (*Rls_ order_add_rls_,*)
1.32 +
1.33 + Calc ("op +", eval_binop "#add_"),
1.34 + Calc ("op *", eval_binop "#mult_"),
1.35 + Calc ("Atools.pow", eval_binop "#power_"),
1.36 +
1.37 + Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.38 + (*"r1 * r1 = r1 ^^^ 2"*)
1.39 + Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.40 + (*"z1 + z1 = 2 * z1"*)
1.41 + Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.42 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.43 +
1.44 + Thm ("real_num_collect",num_str real_num_collect),
1.45 + (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.46 + Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.47 + (*"[| l is_const; m is_const |] ==>
1.48 + l * n + (m * n + k) = (l + m) * n + k"*)
1.49 + Thm ("real_one_collect",num_str real_one_collect),
1.50 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.51 + Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.52 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.53 +
1.54 + Thm ("realpow_multI", num_str realpow_multI),
1.55 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.56 +
1.57 + Calc ("op +", eval_binop "#add_"),
1.58 + Calc ("op *", eval_binop "#mult_"),
1.59 + Calc ("Atools.pow", eval_binop "#power_"),
1.60 +
1.61 + Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
1.62 + Thm ("real_mult_0",num_str real_mult_0),(*"0 * z = 0"*)
1.63 + Thm ("real_add_zero_left",num_str real_add_zero_left)
1.64 + (*"0 + z = z"*)
1.65 +
1.66 + (*Rls_ order_add_rls_*)
1.67 + ],
1.68 +
1.69 + scr = EmptyScr}:rls;
1.70 +
1.71 ruleset' :=
1.72 overwritelthy thy (!ruleset',
1.73 [("norm_Poly", prep_rls norm_Poly),
1.74 @@ -1350,6 +1414,7 @@
1.75 ("discard_parentheses", prep_rls discard_parentheses),
1.76 ("make_polynomial", prep_rls make_polynomial),
1.77 ("expand_binoms", prep_rls expand_binoms),
1.78 + ("rev_rew_p", prep_rls rev_rew_p),
1.79 ("discard_minus_", prep_rls discard_minus_),
1.80 ("expand_poly_", prep_rls expand_poly_),
1.81 ("expand_poly_rat_", prep_rls expand_poly_rat_),
2.1 --- a/src/sml/IsacKnowledge/Poly.thy Tue Aug 29 11:43:53 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Poly.thy Tue Aug 29 13:30:35 2006 +0200
2.3 @@ -13,7 +13,7 @@
2.4 use_thy_only"IsacKnowledge/Poly";
2.5
2.6 remove_thy"Poly";
2.7 - use_thy"Isac";
2.8 + use_thy"IsacKnowledge/Isac";
2.9
2.10
2.11 use"ROOT.ML";
2.12 @@ -111,6 +111,8 @@
2.13 real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2"
2.14 real_plus_minus_binom2_p "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
2.15 real_plus_minus_binom2_p_p "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
2.16 + real_plus_binom_times1 "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
2.17 + real_plus_binom_times2 "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"
2.18
2.19 real_num_collect "[| l is_const; m is_const |] ==> \
2.20 \l * n + m * n = (l + m) * n"
3.1 --- a/src/sml/IsacKnowledge/Rational.ML Tue Aug 29 11:43:53 2006 +0200
3.2 +++ b/src/sml/IsacKnowledge/Rational.ML Tue Aug 29 13:30:35 2006 +0200
3.3 @@ -2785,6 +2785,11 @@
3.4
3.5 val {rules, rew_ord=(_,ro),...} =
3.6 rep_rls (assoc_rls "make_polynomial");
3.7 +(*WN060829 ... make_deriv does not terminate with 1st expl above,
3.8 + see rational.sml --- investigate rulesets for cancel_p ---*)
3.9 +val {rules, rew_ord=(_,ro),...} =
3.10 + rep_rls (assoc_rls "rev_rew_p");
3.11 +
3.12 val thy = Rational.thy;
3.13
3.14 (*.init_state = fn : term -> istate
3.15 @@ -3006,6 +3011,10 @@
3.16
3.17 val {rules=rules,rew_ord=(_,ro),...} =
3.18 rep_rls (assoc_rls "make_polynomial");
3.19 +(*WN060829 ... make_deriv does not terminate with 1st expl above,
3.20 + see rational.sml --- investigate rulesets for cancel_p ---*)
3.21 +val {rules, rew_ord=(_,ro),...} =
3.22 + rep_rls (assoc_rls "rev_rew_p");
3.23 val thy = Rational.thy;
3.24
3.25
4.1 --- a/src/sml/ME/rewtools.sml Tue Aug 29 11:43:53 2006 +0200
4.2 +++ b/src/sml/ME/rewtools.sml Tue Aug 29 13:30:35 2006 +0200
4.3 @@ -13,7 +13,7 @@
4.4 (*.derivation for insertin one level of nodes into the calctree.*)
4.5 type deriv = (term * rule * (term *term list)) list;
4.6
4.7 -fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str r)^", ("^
4.8 +fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str' r)^", ("^
4.9 (term2str t')^", "^(terms2str a)^"))";
4.10 fun trtas2str trtas = (strs2str o (map trta2str)) trtas;
4.11 val deriv2str = trtas2str;
5.1 --- a/src/sml/calcelems.sml Tue Aug 29 11:43:53 2006 +0200
5.2 +++ b/src/sml/calcelems.sml Tue Aug 29 13:30:35 2006 +0200
5.3 @@ -149,6 +149,11 @@
5.4 | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thm thm)^")"
5.5 | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
5.6 | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
5.7 +fun rule2str' Erule = "Erule"
5.8 + | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
5.9 + | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
5.10 + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
5.11 +
5.12 fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
5.13 | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
5.14 | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
6.1 --- a/src/smltest/IsacKnowledge/rational.sml Tue Aug 29 11:43:53 2006 +0200
6.2 +++ b/src/smltest/IsacKnowledge/rational.sml Tue Aug 29 13:30:35 2006 +0200
6.3 @@ -2058,45 +2058,38 @@
6.4 val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
6.5 val Some (tt',asm) = rewrite_set_ thy false make_polynomial tt;
6.6 term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
6.7 -"----- with make_deriv under rls before 060829";
6.8 +"----- with make_deriv";
6.9 +val Some (tt, _) = factout_p_ Isac.thy t; term2str tt =
6.10 +"(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
6.11 (*
6.12 +"--- with ruleset as before 060829";
6.13 val {rules, rew_ord=(_,ro),...} =
6.14 rep_rls (assoc_rls "make_polynomial");
6.15 -val der = make_deriv thy Atools_erls rules ro None t;
6.16 +val der = make_deriv thy Atools_erls rules ro None tt;
6.17 print_depth 99; map (term2str o #1) der; print_depth 3;
6.18 print_depth 99; map (rule2str o #2) der; print_depth 3;
6.19 ... did not terminate"*)
6.20 +"--- with simpler ruleset";
6.21 +val {rules, rew_ord=(_,ro),...} =
6.22 + rep_rls (assoc_rls "rev_rew_p");
6.23 +val der = make_deriv thy Atools_erls rules ro None tt;
6.24 +print_depth 99; writeln (deriv2str der); print_depth 3;
6.25
6.26 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
6.27 +print_depth 99; map (term2str o #1) der; print_depth 3;
6.28 +"...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
6.29 +print_depth 99; map (rule2str o #2) der; print_depth 3;
6.30
6.31 -(*-----
6.32 -(term2str o #1 o the o (cancel_p_ Isac.thy)) t =
6.33 -"(1 * a + 1 * b) / (1 * a + -1 * b)";
6.34 -val Some (tt, _) = factout_p_ Isac.thy t; term2str tt;
6.35 -"(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
6.36 +val der = make_deriv thy Atools_erls rules ro None
6.37 + (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
6.38 +print_depth 99; writeln (deriv2str der); print_depth 3;
6.39
6.40 -val deriv = make_deriv reverse_rewriting tt;
6.41 -writeln (deriv2str deriv);
6.42 -(*
6.43 -if (term2str o #1 o #3 o last_elem) deriv = (*TODO!!!!!!........*)
6.44 - "(a ^^^ 2 + a * (-1 * b) + b * a + b * (-1 * b)) /\n\
6.45 - \(a ^^^ 2 + 2 * a * (-1 * b) + b ^^^ 2)" then ()
6.46 -else raise error "rewtools.sml: make_deriv, expand_binoms changed";
6.47 -*)
6.48 -
6.49 -"---------------- (1 * a + 1 * b) * (1 * a + -1 * b)";
6.50 -val t = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)";
6.51 -
6.52 -val deriv = make_deriv reverse_rewriting t;
6.53 -writeln (deriv2str deriv);
6.54 -(term2str o #1 o #3 o last_elem) deriv;
6.55 -
6.56 -print_depth 99; map (term2str o #1) deriv; print_depth 3;
6.57 -print_depth 9; map #2 deriv; print_depth 3;
6.58 ------*)
6.59 -
6.60 -
6.61 -
6.62 +val {rules, rew_ord=(_,ro),...} =
6.63 + rep_rls (assoc_rls "rev_rew_p");
6.64 +val der = make_deriv thy Atools_erls rules ro None
6.65 + (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
6.66 +print_depth 99; writeln (deriv2str der); print_depth 3;
6.67 +print_depth 99; map (term2str o #1) der; print_depth 3;
6.68 +(*WN060829 ...postponed*)
6.69
6.70
6.71 "-------- investigate format of factout_ and factout_p_ ----------";