diff -r 067d4e3ac358 -r 15775bd26979 src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 09 13:39:30 2010 +0200 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Sep 10 10:36:41 2010 +0200 @@ -3,7 +3,7 @@ (c) due to copyright terms *) -theory Test imports Atools + Rational + Root + Poly + +theory Test imports Atools Rational Root Poly begin consts @@ -29,8 +29,8 @@ (*17.9.02 aus SqRoot.thy------------------------------vvv---*) - "is'_root'_free" :: 'a => bool ("is'_root'_free _" 10) - "contains'_root" :: 'a => bool ("contains'_root _" 10) + "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10) + "contains'_root" :: "'a => bool" ("contains'_root _" 10) Solve'_root'_equation :: "[bool,real, @@ -203,9 +203,10 @@ ]); (** term order **) -fun Term_Ord.term_order (_:subst) tu = (term_ordI [] tu = LESS); - -(** rule sets GOON **) +fun term_order (_:subst) tu = (term_ordI [] tu = LESS); +*} +ML {* +(** rule sets **) val testerls = Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), @@ -237,7 +238,8 @@ scr = Script ((term_of o the o (parse thy)) "empty_script") }:rls; - +*} +ML {* (*.for evaluation of conditions in rewrite rules.*) (*FIXXXXXXME 10.8.02: handle like _simplify*) val tval_rls = @@ -255,7 +257,7 @@ Thm ("or_true",num_str @{thm or_true}), Thm ("or_false",num_str @{thm or_false}), Thm ("and_commute",num_str @{thm and_commute}), - Thm ("or_commute",num_str @{or_commute}), + Thm ("or_commute",num_str @{thm or_commute}), Thm ("real_diff_minus",num_str @{thm real_diff_minus}), @@ -282,7 +284,8 @@ scr = Script ((term_of o the o (parse thy)) "empty_script") }:rls; - +*} +ML {* ruleset' := overwritelthy @{theory} (!ruleset', [("testerls", prep_rls testerls) @@ -319,16 +322,17 @@ val norm_equation = Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord), erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*) - rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add) + rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add}) ], scr = Script ((term_of o the o (parse thy)) "empty_script") }:rls; - +*} +ML {* (** rule sets **) val STest_simplify = (* vv--- not changed to real by parse*) - "Script STest_simplify (t_::'z) = " ^ + "Script STest_simplify (t_t::'z) = " ^ "(Repeat" ^ " ((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^ " (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ " ^ @@ -372,9 +376,10 @@ " (Try (Repeat (Rewrite rmult_0_right False))) @@ " ^ " (Try (Repeat (Rewrite radd_0 False))) @@ " ^ " (Try (Repeat (Rewrite radd_0_right False)))) " ^ - " t_)"; + " t_t)"; - +*} +ML {* (* expects * distributed over + *) val Test_simplify = Rls{id = "Test_simplify", preconds = [], @@ -417,7 +422,7 @@ Thm ("rroot_times_root",num_str @{thm rroot_times_root}), Thm ("rroot_times_root_assoc_p",num_str @{thm rroot_times_root_assoc_p}), Thm ("rsqare",num_str @{thm rsqare}), - Thm ("power_1",num_str @{power_1}), + Thm ("power_1",num_str @{thm power_1}), Thm ("rtwo_of_the_same",num_str @{thm rtwo_of_the_same}), Thm ("rtwo_of_the_same_assoc_p",num_str @{thm rtwo_of_the_same_assoc_p}), @@ -431,10 +436,8 @@ scr = Script ((term_of o the o (parse thy)) "empty_script") (*since 040209 filled by prep_rls: STest_simplify*) }:rls; - - - - +*} +ML {* (** rule sets **) @@ -462,16 +465,15 @@ [Thm ("risolate_bdv_add",num_str @{thm risolate_bdv_add}), Thm ("risolate_bdv_mult_add",num_str @{thm risolate_bdv_mult_add}), Thm ("risolate_bdv_mult",num_str @{thm risolate_bdv_mult}), - Thm ("mult_square",num_str @{mult_square}), - Thm ("constant_square",num_str @{constant_square}), - Thm ("constant_mult_square",num_str @{constant_mult_square}) + Thm ("mult_square",num_str @{thm mult_square}), + Thm ("constant_square",num_str @{thm constant_square}), + Thm ("constant_mult_square",num_str @{thm constant_mult_square}) ], scr = Script ((term_of o the o (parse thy)) "empty_script") }:rls; - - - +*} +ML {* (* association list for calculate_, calculate "op +" etc. not usable in scripts *) @@ -507,6 +509,8 @@ [Calc ("Tools.matches",eval_matches "#matches_")])) ]); +*} +ML {* (** problem types **) store_pbt (prep_pbt thy "pbl_test" [] e_pblID @@ -537,8 +541,8 @@ (prep_pbt thy "pbl_test_uni_lin" [] e_pblID (["linear","univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_ = 0) e_e) |" ^ - "(matches (?a+v_ = 0) e_e) | (matches (?a+?b*v_ = 0) e_e) "]), + ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^ + "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]), ("#Find" ,["solutions v_i"]) ], assoc_rls "matches", @@ -548,7 +552,7 @@ store_pbt (prep_pbt thy (["thy"], - [("#Given" ,"boolTestGiven g_"), + [("#Given" ,"boolTestGiven g_g"), ("#Find" ,"boolTestFind f_f") ], [])); @@ -556,7 +560,7 @@ store_pbt (prep_pbt thy (["testeq","thy"], - [("#Given" ,"boolTestGiven g_"), + [("#Given" ,"boolTestGiven g_g"), ("#Find" ,"boolTestFind f_f") ], [])); @@ -566,7 +570,8 @@ ------ 25.8.01*) - +*} +ML {* (** methods **) store_met (prep_met (theory "Diff") "met_test" [] e_metID @@ -583,6 +588,8 @@ {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], asm_rls=[],asm_thm=[]}, "Undef"));*) +*} +ML {* store_met (prep_met thy "met_test_solvelin" [] e_metID (["Test","solve_linear"]:metID, @@ -590,27 +597,26 @@ ("#Where" ,["matches (?a = ?b) e_e"]), ("#Find" ,["solutions v_i"]) ], - {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls, - prls=assoc_rls "matches", - calc=[], - crls=tval_rls, nrls=Test_simplify}, - "Script Solve_linear (e_e::bool) (v_v::real)= " ^ - "(let e_e =" ^ - " Repeat" ^ - " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^ + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, + prls = assoc_rls "matches", calc = [], crls = tval_rls, + nrls = Test_simplify}, + "Script Solve_linear (e_e::bool) (v_v::real)= " ^ + "(let e_e = " ^ + " Repeat " ^ + " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^ " (Rewrite_Set Test_simplify False))) e_e" ^ - " in [e_::bool])" + " in [e_e::bool])" ) (*, prep_met thy (*test for equations*) (["Test","testeq"]:metID, - [("#Given" ,["boolTestGiven g_"]), + [("#Given" ,["boolTestGiven g_g"]), ("#Find" ,["boolTestFind f_f"]) ], {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]}, - "Script Testeq (eq_::bool) = " ^ + "Script Testeq (e_q::bool) = " ^ "Repeat " ^ - " (let e_e = Try (Repeat (Rewrite rroot_square_inv False eq_)); " ^ + " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^ " e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^ " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^ " in e_e) Until (is_root_free e_e)" (*deleted*) @@ -618,8 +624,8 @@ , ---------27.4.02*) ); - - +*} +ML {* ruleset' := overwritelthy @{theory} (!ruleset', [("norm_equation", prep_rls norm_equation), @@ -764,7 +770,8 @@ fun rational t div_op bdVar = is_denom bdVar div_op t andalso bin_ops_only t; - +*} +ML {* (** problem types **) @@ -772,8 +779,8 @@ (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID (["plain_square","univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_e) |" ^ - "(matches ( ?b*v_ ^^^2 = 0) e_e) |" ^ + ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^ + "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ "(matches (?a + v_v ^^^2 = 0) e_e) |" ^ "(matches ( v_v ^^^2 = 0) e_e)"]), ("#Find" ,["solutions v_i"]) @@ -781,13 +788,13 @@ assoc_rls "matches", SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]])); (* - val e_e = (term_of o the o (parse thy)) "e_::bool"; + val e_e = (term_of o the o (parse thy)) "e_e::bool"; val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0"; val env = [(e_,ve)]; val pre = (term_of o the o (parse thy)) - "(matches (a + b*v_ ^^^2 = 0, e_e::bool)) |" ^ - "(matches ( b*v_ ^^^2 = 0, e_e::bool)) |" ^ + "(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^ + "(matches ( b*v_v ^^^2 = 0, e_e::bool)) |" ^ "(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^ "(matches ( v_v ^^^2 = 0, e_e::bool))"; val prei = subst_atomic env pre; @@ -803,10 +810,12 @@ *) +*} +ML {* store_pbt (prep_pbt thy "pbl_test_uni_poly" [] e_pblID (["polynomial","univariate","equation","test"], - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]), + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), ("#Where" ,["False"]), ("#Find" ,["solutions v_i"]) ], @@ -815,27 +824,29 @@ store_pbt (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID (["degree_two","polynomial","univariate","equation","test"], - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]), + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), ("#Find" ,["solutions v_i"]) ], - e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", [])); + e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])); store_pbt (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID (["pq_formula","degree_two","polynomial","univariate","equation","test"], - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]), + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), ("#Find" ,["solutions v_i"]) ], - e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", [])); + e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])); store_pbt (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID (["abc_formula","degree_two","polynomial","univariate","equation","test"], - [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_v"]), + [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]), ("#Find" ,["solutions v_i"]) ], - e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_v)", [])); + e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])); +*} +ML {* store_pbt (prep_pbt thy "pbl_test_uni_root" [] e_pblID (["squareroot","univariate","equation","test"], @@ -868,6 +879,8 @@ (* (#ppc o get_pbt) ["sqroot-test","univariate","equation"]; *) +*} +ML {* store_met @@ -900,9 +913,11 @@ " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ " e_e" ^ - " in [e_::bool])" + " in [e_e::bool])" )); +*} +ML {* store_met (prep_met thy "met_test_sqrt2" [] e_metID (*root-equation ... for test-*.sml until 8.01*) @@ -930,11 +945,13 @@ " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ " e_e;" ^ - " (L_::bool list) = Tac subproblem_equation_dummy; " ^ + " (L_L::bool list) = Tac subproblem_equation_dummy; " ^ " L_L = Tac solve_equation_dummy " ^ " in Check_elementwise L_L {(v_v::real). Assumptions})" )); +*} +ML {* store_met (prep_met thy "met_test_squ_sub" [] e_metID (*tests subproblem fixed linear*) @@ -944,14 +961,18 @@ ], {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], crls=tval_rls, nrls=Test_simplify}, - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ - " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^ - " (Try (Rewrite_Set Test_simplify False))) e_e; " ^ - "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^ - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^ + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ + " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^ + " (Try (Rewrite_Set Test_simplify False))) e_e; " ^ + "(L_L::bool list) = (SubProblem (Test', " ^ + " [linear,univariate,equation,test], " ^ + " [Test,solve_linear])" ^ + " [BOOL e_e, REAL v_v])" ^ "in Check_elementwise L_L {(v_v::real). Assumptions})" )); +*} +ML {* store_met (prep_met thy "met_test_squ_sub2" [] e_metID (*tests subproblem fixed degree 2*) @@ -965,11 +986,13 @@ ("square_equation_right","")]*)}, "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^ - "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^ - " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_])" ^ + "(L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^ + " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^ "in Check_elementwise L_L {(v_v::real). Assumptions})" )); +*} +ML {* store_met (prep_met thy "met_test_squ_nonterm" [] e_metID (*root-equation: see foils..., but notTerminating*) @@ -995,12 +1018,14 @@ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ " e_e;" ^ - " (L_::bool list) = " ^ - " (SubProblem (Test_,[linear,univariate,equation,test]," ^ - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^ + " (L_L::bool list) = " ^ + " (SubProblem (Test',[linear,univariate,equation,test]," ^ + " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^ "in Check_elementwise L_L {(v_v::real). Assumptions})" )); +*} +ML {* store_met (prep_met thy "met_test_eq1" [] e_metID (*root-equation1:*) @@ -1026,11 +1051,13 @@ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ " e_e;" ^ - " (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^ - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^ + " (L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^ + " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^ " in Check_elementwise L_L {(v_v::real). Assumptions})" )); +*} +ML {* store_met (prep_met thy "met_test_squ2" [] e_metID (*root-equation2*) @@ -1057,11 +1084,13 @@ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ " e_e;" ^ - " (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^ - " [Test,solve_plain_square]) [BOOL e_e, REAL v_])" ^ + " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^ + " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^ " in Check_elementwise L_L {(v_v::real). Assumptions})" )); +*} +ML {* store_met (prep_met thy "met_test_squeq" [] e_metID (*root-equation*) @@ -1088,18 +1117,20 @@ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ " e_e;" ^ - " (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^ - " [no_met]) [BOOL e_e, REAL v_])" ^ + " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^ + " [no_met]) [BOOL e_e, REAL v_v])" ^ " in Check_elementwise L_L {(v_v::real). Assumptions})" ) ); (*#######*) +*} +ML {* store_met (prep_met thy "met_test_eq_plain" [] e_metID (*solve_plain_square*) (["Test","solve_plain_square"]:metID, [("#Given",["equality e_e","solveFor v_v"]), - ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_e) |" ^ - "(matches ( ?b*v_ ^^^2 = 0) e_e) |" ^ + ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^ + "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ "(matches (?a + v_v ^^^2 = 0) e_e) |" ^ "(matches ( v_v ^^^2 = 0) e_e)"]), ("#Find" ,["solutions v_i"]) @@ -1117,6 +1148,8 @@ " in ((Or_to_List e_e)::bool list))" )); +*} +ML {* store_met (prep_met thy "met_test_norm_univ" [] e_metID (["Test","norm_univar_equation"]:metID, @@ -1130,13 +1163,15 @@ "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^ " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^ " (Try (Rewrite_Set Test_simplify False))) e_e " ^ - " in (SubProblem (Test_,[univariate,equation,test], " ^ - " [no_met]) [BOOL e_e, REAL v_]))" + " in (SubProblem (Test',[univariate,equation,test], " ^ + " [no_met]) [BOOL e_e, REAL v_v]))" )); (*17.9.02 aus SqRoot.ML------------------------------^^^---*) +*} +ML {* (*8.4.03 aus Poly.ML--------------------------------vvv--- make_polynomial ---> make_poly @@ -1171,18 +1206,18 @@ | size_of_term' (f$t) = size_of_term' f + size_of_term' t | size_of_term' _ = 1; -fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) - (case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) - | Term_Ord.term_ord' pr thy (t, u) = +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) + (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) + | term_ord' pr thy (t, u) = (if pr then let val (f, ts) = strip_comb t and (g, us) = strip_comb u; val _=writeln("t= f@ts= " ^ "" ^ ((Syntax.string_of_term (thy2ctxt thy)) f)^ "\" @ " ^ "[" ^ - (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]"""); + (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]\""); val _=writeln("u= g@us= " ^ "" ^ ((Syntax.string_of_term (thy2ctxt thy)) g) ^ "\" @ " ^ "[" ^ - (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]"""); + (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\""); val _=writeln("size_of_term(t,u)= ("^ (string_of_int(size_of_term' t)) ^ ", " ^ (string_of_int(size_of_term' u)) ^ ")"); @@ -1209,6 +1244,8 @@ (term_ord' pr thy(***) tu = LESS ); end;(*local*) +*} +ML {* rew_ord' := overwritel (!rew_ord', [("termlessI", termlessI), @@ -1217,7 +1254,7 @@ (*WN060510 this was a preparation for prep_rls ... val scr_make_polytest = -"Script Expand_binomtest t_ =" ^ +"Script Expand_binomtest t_t =" ^ "(Repeat " ^ "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^ @@ -1251,7 +1288,7 @@ " (Try (Repeat (Calculate PLUS ))) @@ " ^ " (Try (Repeat (Calculate TIMES ))) @@ " ^ " (Try (Repeat (Calculate POWER)))) " ^ -" t_)"; +" t_t)"; -----------------------------------------------------*) val make_polytest = @@ -1321,10 +1358,12 @@ ], scr = EmptyScr(*Script ((term_of o the o (parse thy)) scr_make_polytest)*) - }:rls; -(*WN060510 this was done before 'fun prep_rls' ... + }:rls; +*} +ML {* +(*WN060510 this was done before 'fun prep_rls' ...------------------------ val scr_expand_binomtest = -"Script Expand_binomtest t_ =" ^ +"Script Expand_binomtest t_t =" ^ "(Repeat " ^ "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^ " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^ @@ -1355,8 +1394,8 @@ " (Try (Repeat (Calculate PLUS ))) @@ " ^ " (Try (Repeat (Calculate TIMES ))) @@ " ^ " (Try (Repeat (Calculate POWER)))) " ^ -" t_)"; -------------------------------------------------------*) +" t_t)"; +--------------------------------------------------------------------------*) val expand_binomtest = Rls{id = "expand_binomtest", preconds = [], @@ -1366,85 +1405,90 @@ ("TIMES" , ("op *", eval_binop "#mult_")), ("POWER", ("Atools.pow", eval_binop "#power_")) ], - rules = [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}), + rules = + [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}), (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*) - Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}), + Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}), (*"(a + b)*(a + b) = ...*) - Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}), - (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*) - Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}), - (*"(a - b)*(a - b) = ...*) - Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}), - (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*) - Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}), - (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*) - (*RL 020915*) - Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}), - (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) - Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}), - (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*) - Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}), - (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*) - Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}), - (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*) - Thm ("realpow_multI",num_str @{thm realpow_multI}), - (*(a*b)^^^n = a^^^n * b^^^n*) - Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}), - (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *) - Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}), - (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *) + Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}), + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*) + Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}), + (*"(a - b)*(a - b) = ...*) + Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}), + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*) + Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}), + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*) + (*RL 020915*) + Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}), + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) + Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}), + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*) + Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}), + (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*) + Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}), + (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*) + Thm ("realpow_multI",num_str @{thm realpow_multI}), + (*(a*b)^^^n = a^^^n * b^^^n*) + Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}), + (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *) + Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}), + (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *) - (* Thm ("left_distrib" ,num_str @{thm left_distrib}}), - (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) - Thm ("right_distrib",num_str @{thm right_distrib}), - (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) - Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}}), - (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) - Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}), - (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) - *) - - Thm ("mult_1_left",num_str @{thm mult_1_left}}), (*"1 * z = z"*) - Thm ("mult_zero_left",num_str @{thm mult_zero_left}}), (*"0 * z = 0"*) - Thm ("add_0_left",num_str @{thm add_0_left}}),(*"0 + z = z"*) + (* Thm ("left_distrib" ,num_str @{thm left_distrib}), + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) + Thm ("right_distrib",num_str @{thm right_distrib}), + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) + Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}), + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) + Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}), + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) + *) + + Thm ("mult_1_left",num_str @{thm mult_1_left}), + (*"1 * z = z"*) + Thm ("mult_zero_left",num_str @{thm mult_zero_left}), + (*"0 * z = 0"*) + Thm ("add_0_left",num_str @{thm add_0_left}), + (*"0 + z = z"*) - Calc ("op +", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), - Calc ("Atools.pow", eval_binop "#power_"), - (* - Thm ("real_mult_commute",num_str @{thm real_mult_commute}), (*AC-rewriting*) - Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}), (**) - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}), (**) - Thm ("add_commute",num_str @{thm add_commute}), (**) - Thm ("add_left_commute",num_str @{thm add_left_commute}), (**) - Thm ("add_assoc",num_str @{thm add_assoc}), (**) - *) - - Thm ("sym_realpow_twoI", - num_str (@{thm realpow_twoI} RS @{thm sym})), - (*"r1 * r1 = r1 ^^^ 2"*) - Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}), - (*"r * r ^^^ n = r ^^^ (n + 1)"*) - (*Thm ("sym_real_mult_2", - num_str (@{thm real_mult_2} RS @{thm sym})), - (*"z1 + z1 = 2 * z1"*)*) - Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}), - (*"z1 + (z1 + k) = 2 * z1 + k"*) + Calc ("op +", eval_binop "#add_"), + Calc ("op *", eval_binop "#mult_"), + Calc ("Atools.pow", eval_binop "#power_"), + (* + Thm ("real_mult_commute",num_str @{thm real_mult_commute}), + (*AC-rewriting*) + Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}), + Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}), + Thm ("add_commute",num_str @{thm add_commute}), + Thm ("add_left_commute",num_str @{thm add_left_commute}), + Thm ("add_assoc",num_str @{thm add_assoc}), + *) + + Thm ("sym_realpow_twoI", + num_str (@{thm realpow_twoI} RS @{thm sym})), + (*"r1 * r1 = r1 ^^^ 2"*) + Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}), + (*"r * r ^^^ n = r ^^^ (n + 1)"*) + (*Thm ("sym_real_mult_2", + num_str (@{thm real_mult_2} RS @{thm sym})), + (*"z1 + z1 = 2 * z1"*)*) + Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}), + (*"z1 + (z1 + k) = 2 * z1 + k"*) - Thm ("real_num_collect",num_str @{thm real_num_collect}), - (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*) - Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}), - (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*) - Thm ("real_one_collect",num_str @{thm real_one_collect}), - (*"m is_const ==> n + m * n = (1 + m) * n"*) - Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), - (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) + Thm ("real_num_collect",num_str @{thm real_num_collect}), + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*) + Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}), + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*) + Thm ("real_one_collect",num_str @{thm real_one_collect}), + (*"m is_const ==> n + m * n = (1 + m) * n"*) + Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) - Calc ("op +", eval_binop "#add_"), - Calc ("op *", eval_binop "#mult_"), - Calc ("Atools.pow", eval_binop "#power_") - ], + Calc ("op +", eval_binop "#add_"), + Calc ("op *", eval_binop "#mult_"), + Calc ("Atools.pow", eval_binop "#power_") + ], scr = EmptyScr (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*) }:rls;