1.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Thu Jan 17 12:31:17 2008 +0100
1.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Thu Jan 17 15:34:56 2008 +0100
1.3 @@ -13,33 +13,34 @@
1.4
1.5 (** eval functions **)
1.6
1.7 -(* get the identifier from a monomial of the form num | var | num*var;
1.8 - attention: num is Free("123",_) *)
1.9 -fun identifier (Free (id,_)) = id
1.10 +(*. get the identifier from specific monomials; see fun ist_monom .*)
1.11 +(*HACK.WN080107*)
1.12 +fun increase str =
1.13 + let val s::ss = explode str
1.14 + in implode ((chr (ord s + 1))::ss) end;
1.15 +fun identifier (Free (id,_)) = id (* 2, a *)
1.16 | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
1.17 + id (* 2*a, a*b *)
1.18 + | identifier (Const ("op *", _) $ (* 3*a*b *)
1.19 + (Const ("op *", _) $
1.20 + Free (num, _) $ Free _) $ Free (id, _)) =
1.21 if is_numeral num then id
1.22 else "|||||||||||||"
1.23 + | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
1.24 + if is_numeral base then "|||||||||||||" (* a^2 *)
1.25 + else (*increase*) base
1.26 + | identifier (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
1.27 + (Const ("Atools.pow", _) $
1.28 + Free (base, _) $ Free (exp, _))) =
1.29 + if is_numeral num andalso not (is_numeral base) then (*increase*) base
1.30 + else "|||||||||||||"
1.31 | identifier _ = "|||||||||||||"(*the "largest" string*);
1.32
1.33 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
1.34 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
1.35 fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
1.36 - if is_num a andalso is_num b then
1.37 - if int_of_Free a < int_of_Free b then
1.38 - Some ((term2str p) ^ " = True",
1.39 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.40 - else Some ((term2str p) ^ " = False",
1.41 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.42 - else
1.43 - if identifier a < identifier b then
1.44 - Some ((term2str p) ^ " = True",
1.45 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.46 - else Some ((term2str p) ^ " = False",
1.47 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.48 - | eval_kleiner _ _ _ _ = None;
1.49 -fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
1.50 if is_num b then
1.51 - if is_num a then
1.52 + if is_num a then (*123 kleiner 32 = True !!!*)
1.53 if int_of_Free a < int_of_Free b then
1.54 Some ((term2str p) ^ " = True",
1.55 Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.56 @@ -60,6 +61,21 @@
1.57 | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) =
1.58 if is_numeral num then true else false
1.59 | ist_monom _ = false;
1.60 +(*. this function only accepts the most simple monoms vvvvvvvvvv .*)
1.61 +fun ist_monom (Free (id,_)) = true (* 2, a *)
1.62 + | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
1.63 + if is_numeral id then false else true
1.64 + | ist_monom (Const ("op *", _) $ (* 3*a*b *)
1.65 + (Const ("op *", _) $
1.66 + Free (num, _) $ Free _) $ Free (id, _)) =
1.67 + if is_numeral num andalso not (is_numeral id) then true else false
1.68 + | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
1.69 + true (* a^2 *)
1.70 + | ist_monom (Const ("op *", _) $ Free (num, _) $ (* 3*a^2 *)
1.71 + (Const ("Atools.pow", _) $
1.72 + Free (base, _) $ Free (exp, _))) =
1.73 + if is_numeral num then true else false
1.74 + | ist_monom _ = false;
1.75
1.76 (* is this a univariate monomial ? *)
1.77 (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
1.78 @@ -298,16 +314,20 @@
1.79 "Not (matchsub (?a + (?b + ?c)) t_ | \
1.80 \ matchsub (?a + (?b - ?c)) t_ | \
1.81 \ matchsub (?a - (?b + ?c)) t_ | \
1.82 - \ matchsub (?a + (?b - ?c)) t_ )"]),
1.83 + \ matchsub (?a + (?b - ?c)) t_ )",
1.84 + "Not (matchsub (?a * (?b + ?c)) t_ | \
1.85 + \ matchsub (?a * (?b - ?c)) t_ | \
1.86 + \ matchsub ((?b + ?c) * ?a) t_ | \
1.87 + \ matchsub ((?b - ?c) * ?a) t_ )"]),
1.88 ("#Find" ,["normalform n_"])
1.89 ],
1.90 append_rls "prls_pbl_vereinf_poly" e_rls
1.91 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
1.92 Calc ("Tools.matchsub", eval_matchsub ""),
1.93 - Thm ("and_true",and_true),
1.94 - (*"(?a & True) = ?a"*)
1.95 - Thm ("and_false",and_false),
1.96 - (*"(?a & False) = False"*)
1.97 + Thm ("or_true",or_true),
1.98 + (*"(?a | True) = True"*)
1.99 + Thm ("or_false",or_false),
1.100 + (*"(?a | False) = ?a"*)
1.101 Thm ("not_true",num_str not_true),
1.102 (*"(~ True) = False"*)
1.103 Thm ("not_false",num_str not_false)
1.104 @@ -319,11 +339,23 @@
1.105 (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID
1.106 (["klammer","polynom","vereinfachen"],
1.107 [("#Given" ,["term t_"]),
1.108 - ("#Where" ,["t_ is_polyexp"]),
1.109 + ("#Where" ,["t_ is_polyexp",
1.110 + "Not (matchsub (?a * (?b + ?c)) t_ | \
1.111 + \ matchsub (?a * (?b - ?c)) t_ | \
1.112 + \ matchsub ((?b + ?c) * ?a) t_ | \
1.113 + \ matchsub ((?b - ?c) * ?a) t_ )"]),
1.114 ("#Find" ,["normalform n_"])
1.115 ],
1.116 - append_rls "e_rls" e_rls [(*for preds in where_*)
1.117 - Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.118 + append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
1.119 + Calc ("Tools.matchsub", eval_matchsub ""),
1.120 + Thm ("or_true",or_true),
1.121 + (*"(?a | True) = True"*)
1.122 + Thm ("or_false",or_false),
1.123 + (*"(?a | False) = ?a"*)
1.124 + Thm ("not_true",num_str not_true),
1.125 + (*"(~ True) = False"*)
1.126 + Thm ("not_false",num_str not_false)
1.127 + (*"(~ False) = True"*)],
1.128 Some "Vereinfache t_",
1.129 [["simplification","for_polynomials","with_parentheses"]]));
1.130
2.1 --- a/src/sml/RCODE-root.sml Thu Jan 17 12:31:17 2008 +0100
2.2 +++ b/src/sml/RCODE-root.sml Thu Jan 17 15:34:56 2008 +0100
2.3 @@ -22,6 +22,7 @@
2.4 | find_first pred (x :: xs) =
2.5 if pred x then Some x else find_first pred xs;
2.6 fun swap (x, y) = (y, x);
2.7 +(*HACK.WN080107*) val sstr = str;
2.8
2.9 "**** build the isac kernel = math-engine + IsacKnowledge ";
2.10 "**** build the math-engine ******************************";
3.1 --- a/src/sml/ROOT.ML Thu Jan 17 12:31:17 2008 +0100
3.2 +++ b/src/sml/ROOT.ML Thu Jan 17 15:34:56 2008 +0100
3.3 @@ -22,6 +22,7 @@
3.4 | find_first pred (x :: xs) =
3.5 if pred x then Some x else find_first pred xs;
3.6 fun swap (x, y) = (y, x);
3.7 +(*HACK.WN080107*) val sstr = str;
3.8
3.9 "**** build the isac kernel = math-engine + IsacKnowledge ";
3.10 "**** build the math-engine ******************************";
4.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Thu Jan 17 12:31:17 2008 +0100
4.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Thu Jan 17 15:34:56 2008 +0100
4.3 @@ -11,6 +11,7 @@
4.4 "-----------------------------------------------------------------";
4.5 "table of contents -----------------------------------------------";
4.6 "-----------------------------------------------------------------";
4.7 +"----------- fun eval_ist_monom ----------------------------------";
4.8 "----------- watch order_add_mult -------------------------------";
4.9 "----------- build predicate for +- ordering ---------------------";
4.10 "----------- build fasse_zusammen --------------------------------";
4.11 @@ -22,11 +23,46 @@
4.12 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
4.13 "----------- try fun applyTactics --------------------------------";
4.14 "----------- pbl binom polynom vereinfachen p.39 -----------------";
4.15 +"----------- pbl binom polynom vereinfachen: cube ----------------";
4.16 +"----------- refine Vereinfache ----------------------------------";
4.17 "-----------------------------------------------------------------";
4.18 "-----------------------------------------------------------------";
4.19 "-----------------------------------------------------------------";
4.20
4.21
4.22 +"----------- fun eval_ist_monom ----------------------------------";
4.23 +"----------- fun eval_ist_monom ----------------------------------";
4.24 +"----------- fun eval_ist_monom ----------------------------------";
4.25 +ist_monom (str2term "12");
4.26 +case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of
4.27 + Some ("12 ist_monom = True", _) => ()
4.28 + | _ => raise error "polyminus.sml: 12 ist_monom = True";
4.29 +
4.30 +case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of
4.31 + Some ("a ist_monom = True", _) => ()
4.32 + | _ => raise error "polyminus.sml: a ist_monom = True";
4.33 +
4.34 +case eval_ist_monom 0 0 (str2term "(3*a) ist_monom") 0 of
4.35 + Some ("3 * a ist_monom = True", _) => ()
4.36 + | _ => raise error "polyminus.sml: 3 * a ist_monom = True";
4.37 +
4.38 +case eval_ist_monom 0 0 (str2term "(a^^^2) ist_monom") 0 of
4.39 + Some ("a ^^^ 2 ist_monom = True", _) => ()
4.40 + | _ => raise error "polyminus.sml: a^^^2 ist_monom = True";
4.41 +
4.42 +case eval_ist_monom 0 0 (str2term "(3*a^^^2) ist_monom") 0 of
4.43 + Some ("3 * a ^^^ 2 ist_monom = True", _) => ()
4.44 + | _ => raise error "polyminus.sml: 3*a^^^2 ist_monom = True";
4.45 +
4.46 +case eval_ist_monom 0 0 (str2term "(a*b) ist_monom") 0 of
4.47 + Some ("a * b ist_monom = True", _) => ()
4.48 + | _ => raise error "polyminus.sml: a*b ist_monom = True";
4.49 +
4.50 +case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of
4.51 + Some ("3 * a * b ist_monom = True", _) => ()
4.52 + | _ => raise error "polyminus.sml: 3*a*b ist_monom = True";
4.53 +
4.54 +
4.55 "----------- watch order_add_mult -------------------------------";
4.56 "----------- watch order_add_mult -------------------------------";
4.57 "----------- watch order_add_mult -------------------------------";
4.58 @@ -91,11 +127,11 @@
4.59 " a kleiner b ==> (b + a) = (a + b)";
4.60 str2term "aaa";
4.61 str2term "222 * aaa";
4.62 -
4.63 -case eval_kleiner 0 0 (str2term "12 kleiner 9") 0 of
4.64 +(*
4.65 +case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of
4.66 Some ("12 kleiner 9 = False", _) => ()
4.67 | _ => raise error "polyminus.sml: 12 kleiner 9 = False";
4.68 -
4.69 +*)
4.70 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of
4.71 Some ("a kleiner b = True", _) => ()
4.72 | _ => raise error "polyminus.sml: a kleiner b = True";
4.73 @@ -104,6 +140,24 @@
4.74 Some ("10 * g kleiner f = False", _) => ()
4.75 | _ => raise error "polyminus.sml: 10 * g kleiner f = False";
4.76
4.77 +case eval_kleiner 0 0 (str2term "(a^^^2) kleiner b") 0 of
4.78 + Some ("a ^^^ 2 kleiner b = True", _) => ()
4.79 + | _ => raise error "polyminus.sml: a ^^^ 2 kleiner b = True";
4.80 +
4.81 +case eval_kleiner 0 0 (str2term "(3*a^^^2) kleiner b") 0 of
4.82 + Some ("3 * a ^^^ 2 kleiner b = True", _) => ()
4.83 + | _ => raise error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True";
4.84 +
4.85 +case eval_kleiner 0 0 (str2term "(a*b) kleiner c") 0 of
4.86 + Some ("a * b kleiner c = True", _) => ()
4.87 + | _ => raise error "polyminus.sml: a * b kleiner b = True";
4.88 +
4.89 +case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of
4.90 + Some ("3 * a * b kleiner c = True", _) => ()
4.91 + | _ => raise error "polyminus.sml: 3 * a * b kleiner b = True";
4.92 +
4.93 +
4.94 +
4.95 "----- compare tausche_plus with real_num_collect";
4.96 val od = dummy_ord;
4.97
4.98 @@ -447,7 +501,7 @@
4.99 trace_rewrite := true;
4.100 trace_rewrite := false;
4.101
4.102 -
4.103 +(*@@@@@@@*)
4.104 states:=[];
4.105 CalcTree [(["term ((3*a + 2) * (4*a - 1))",
4.106 "normalform N"],
4.107 @@ -464,15 +518,66 @@
4.108 *)
4.109
4.110
4.111 +"----------- pbl binom polynom vereinfachen: cube ----------------";
4.112 +"----------- pbl binom polynom vereinfachen: cube ----------------";
4.113 +"----------- pbl binom polynom vereinfachen: cube ----------------";
4.114 +states:=[];
4.115 +CalcTree [(["term (8*(a - q) + a - 2*q + 3*(a - 2*q))",
4.116 + "normalform N"],
4.117 + ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"],
4.118 + ["simplification","for_polynomials","with_parentheses_mult"]))];
4.119 +moveActiveRoot 1;
4.120 +autoCalculate 1 CompleteCalc;
4.121 +val ((pt,p),_) = get_calc 1; show_pt pt;
4.122
4.123
4.124 +"----------- refine Vereinfache ----------------------------------";
4.125 +"----------- refine Vereinfache ----------------------------------";
4.126 +"----------- refine Vereinfache ----------------------------------";
4.127 +val fmz = ["term (8*(a - q) + a - 2*q + 3*(a - 2*q))",
4.128 + "normalform N"];
4.129 +print_depth 11;
4.130 +val matches = refine fmz ["vereinfachen"];
4.131 +print_depth 3;
4.132
4.133 +"----- go into details, if it seems not to work -----";
4.134 +"--- does the predicate evaluate correctly ?";
4.135 +val t = str2term
4.136 + "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + \
4.137 + \3 * (a - 2 * q))";
4.138 +val ma = eval_matchsub "" "Tools.matchsub" t thy;
4.139 +case ma of
4.140 + Some ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
4.141 + \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()
4.142 + | _ => raise error "polyminus.sml matchsub (?a * (?b - ?c)...A";
4.143
4.144 +"--- does the respective prls rewrite ?";
4.145 +val prls = append_rls "prls_pbl_vereinf_poly" e_rls
4.146 + [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
4.147 + Calc ("Tools.matchsub", eval_matchsub ""),
4.148 + Thm ("or_true",or_true),
4.149 + (*"(?a | True) = True"*)
4.150 + Thm ("or_false",or_false),
4.151 + (*"(?a | False) = ?a"*)
4.152 + Thm ("not_true",num_str not_true),
4.153 + (*"(~ True) = False"*)
4.154 + Thm ("not_false",num_str not_false)
4.155 + (*"(~ False) = True"*)];
4.156 +trace_rewrite := true;
4.157 +val Some (t', _) = rewrite_set_ thy false prls t;
4.158 +trace_rewrite := false;
4.159
4.160 -
4.161 -
4.162 -
4.163 -
4.164 +"--- does the respective prls rewrite the whole predicate ?";
4.165 +val t = str2term
4.166 + "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \
4.167 + \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
4.168 + \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
4.169 + \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
4.170 +trace_rewrite := true;
4.171 +val Some (t', _) = rewrite_set_ thy false prls t;
4.172 +trace_rewrite := false;
4.173 +if term2str t' = "False" then ()
4.174 +else raise error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
4.175
4.176
4.177