1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed May 16 15:01:47 2012 +0200
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Wed May 16 15:47:22 2012 +0200
1.3 @@ -315,7 +315,7 @@
1.4 prls : rls, (*for evaluating predicates in modelpattern *)
1.5 crls : rls, (*for check_elementwise, ie. formulae in calc.*)
1.6 nrls : rls, (*canonical simplifier specific for this met *)
1.7 -(* errpats : errpat list,(*error patterns expected in this method *)*)
1.8 + errpats : errpat list,(*error patterns expected in this method *)
1.9 calc : calc list, (*040207: <--- calclist' in fun prep_met *)
1.10 (*branch : TransitiveB set in append_problem at generation ob pblobj
1.11 FIXXXME.0308: set branch from met in Apply_Method ? *)
1.12 @@ -330,7 +330,7 @@
1.13 val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
1.14 rew_ord' = "e_rew_ord'": rew_ord',
1.15 erls = e_rls, srls = e_rls, prls = e_rls,
1.16 - calc = [], crls = e_rls, (*errpats = [],*) nrls= e_rls,
1.17 + calc = [], crls = e_rls, errpats = [], nrls= e_rls,
1.18 ppc = []: (string * (term * term)) list,
1.19 pre = []: term list,
1.20 scr = EmptyScr: scr}:met;
1.21 @@ -634,7 +634,7 @@
1.22 (metID, ppc: (string * string list) list (*'#Where' -> #pre*),
1.23 {rew_ord'=ro, rls'=rls, srls=srls, prls=prls,
1.24 calc = scr_isa_fns(*FIXME.040207: del - auto-done*),
1.25 - crls=cr, (*errpats = ep,*) nrls= nr}, scr) =
1.26 + crls=cr, errpats = ep, nrls= nr}, scr) =
1.27 let fun eq f (f', _) = f = f';
1.28 (*val thy = (assoc_thy o fst) metID*)
1.29 val gi = filter (eq "#Given") ppc;
1.30 @@ -693,7 +693,7 @@
1.31 calc = if scr = "empty_script" then []
1.32 else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
1.33 (filter is_calc) o stacpbls) sc,
1.34 - crls=cr, (*errpats = ep,*) nrls= nr, scr=Script sc}:met,
1.35 + crls=cr, errpats = ep, nrls= nr, scr=Script sc}:met,
1.36 metID:metID)
1.37 end;
1.38
2.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Wed May 16 15:01:47 2012 +0200
2.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Wed May 16 15:47:22 2012 +0200
2.3 @@ -64,7 +64,7 @@
2.4 [],
2.5 {rew_ord'="tless_true", rls'= Erls, calc = [],
2.6 srls = Erls, prls = Erls,
2.7 - crls =Erls , nrls = Erls},
2.8 + crls =Erls , errpats = [], nrls = Erls},
2.9 "empty_script"
2.10 ));
2.11
2.12 @@ -74,7 +74,7 @@
2.13 [],
2.14 {rew_ord'="tless_true", rls'= Erls, calc = [],
2.15 srls = Erls, prls = Erls,
2.16 - crls =Erls , nrls = Erls},
2.17 + crls =Erls , errpats = [], nrls = Erls},
2.18 "empty_script"
2.19 ));
2.20
2.21 @@ -92,7 +92,7 @@
2.22 srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
2.23 [Calc ("Atools.boollist2sum",
2.24 eval_boollist2sum "")],
2.25 - prls = e_rls, crls =e_rls , nrls = norm_Rational},
2.26 + prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational},
2.27 "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
2.28 "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
2.29 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
2.30 @@ -129,7 +129,7 @@
2.31 [Calc ("Atools.boollist2sum",
2.32 eval_boollist2sum "")],
2.33 prls = e_rls,
2.34 - crls =e_rls , nrls = norm_Rational},
2.35 + crls =e_rls , errpats = [], nrls = norm_Rational},
2.36 "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
2.37 "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
2.38 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed May 16 15:01:47 2012 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed May 16 15:47:22 2012 +0200
3.3 @@ -239,7 +239,7 @@
3.4 [Calc ("Atools.ident",eval_ident "#ident_"),
3.5 Thm ("not_true",num_str @{thm not_true}),
3.6 Thm ("not_false",num_str @{thm not_false})],
3.7 - calc = [], srls = srls, prls = Erls, crls = Atools_erls, nrls = Erls},
3.8 + calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
3.9 "Script BiegelinieScript " ^
3.10 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
3.11 "(r_b::bool list) (r_m::bool list) = " ^
3.12 @@ -327,7 +327,7 @@
3.13 Thm ("last_thmI",num_str @{thm last_thmI}),
3.14 Thm ("if_True",num_str @{thm if_True}),
3.15 Thm ("if_False",num_str @{thm if_False})],
3.16 - prls = Erls, crls = Atools_erls, nrls = Erls},
3.17 + prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
3.18 "Script Biegelinie2Script " ^
3.19 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
3.20 " (let " ^
3.21 @@ -357,7 +357,7 @@
3.22 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.23 srls = e_rls,
3.24 prls=e_rls,
3.25 - crls = Atools_erls, nrls = e_rls},
3.26 + crls = Atools_erls, errpats = [], nrls = e_rls},
3.27 "empty_script"
3.28 ));
3.29
3.30 @@ -368,7 +368,7 @@
3.31 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.32 srls = e_rls,
3.33 prls=e_rls,
3.34 - crls = Atools_erls, nrls = e_rls},
3.35 + crls = Atools_erls, errpats = [], nrls = e_rls},
3.36 "empty_script"
3.37 ));
3.38
3.39 @@ -379,7 +379,7 @@
3.40 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.41 srls = e_rls,
3.42 prls=e_rls,
3.43 - crls = Atools_erls, nrls = e_rls},
3.44 + crls = Atools_erls, errpats = [], nrls = e_rls},
3.45 "empty_script"
3.46 ));
3.47
3.48 @@ -390,7 +390,7 @@
3.49 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.50 srls = e_rls,
3.51 prls=e_rls,
3.52 - crls = Atools_erls, nrls = e_rls},
3.53 + crls = Atools_erls, errpats = [], nrls = e_rls},
3.54 "empty_script"
3.55 ));
3.56
3.57 @@ -409,7 +409,7 @@
3.58 calc = [],
3.59 srls = append_rls "srls_ausBelastung" e_rls
3.60 [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
3.61 - prls = e_rls, crls = Atools_erls, nrls = e_rls},
3.62 + prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
3.63 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
3.64 " (let q___q = Take (qq v_v = q__q); " ^
3.65 " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
3.66 @@ -446,7 +446,7 @@
3.67 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.68 srls = srls2,
3.69 prls=e_rls,
3.70 - crls = Atools_erls, nrls = e_rls},
3.71 + crls = Atools_erls, errpats = [], nrls = e_rls},
3.72 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
3.73 " (let b_1 = NTH 1 r_b; " ^
3.74 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
3.75 @@ -513,7 +513,7 @@
3.76 srls = append_rls "srls_in_EquationfromFunc" e_rls
3.77 [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
3.78 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
3.79 - prls=e_rls, crls = Atools_erls, nrls = e_rls},
3.80 + prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
3.81 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
3.82 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.83 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed May 16 15:01:47 2012 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed May 16 15:47:22 2012 +0200
4.3 @@ -278,7 +278,7 @@
4.4 (prep_met thy "met_diff" [] e_metID
4.5 (["diff"], [],
4.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
4.7 - crls = Atools_erls, nrls = norm_diff}, "empty_script"));
4.8 + crls = Atools_erls, errpats = [], nrls = norm_diff}, "empty_script"));
4.9
4.10 store_met
4.11 (prep_met thy "met_diff_onR" [] e_metID
4.12 @@ -287,7 +287,7 @@
4.13 ("#Find" ,["derivative f_f'"])
4.14 ],
4.15 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
4.16 - prls=e_rls, crls = Atools_erls, nrls = norm_diff},
4.17 + prls=e_rls, crls = Atools_erls, errpats = [], nrls = norm_diff},
4.18 "Script DiffScr (f_f::real) (v_v::real) = " ^
4.19 " (let f_f' = Take (d_d v_v f_f) " ^
4.20 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
4.21 @@ -320,7 +320,7 @@
4.22 ("#Find" ,["derivative f_f'"])
4.23 ],
4.24 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
4.25 - prls=e_rls, crls = Atools_erls, nrls = norm_diff},
4.26 + prls=e_rls, crls = Atools_erls, errpats = [], nrls = norm_diff},
4.27 "Script DiffScr (f_f::real) (v_v::real) = " ^
4.28 " (let f_f' = Take (d_d v_v f_f) " ^
4.29 " in (( " ^
4.30 @@ -352,7 +352,7 @@
4.31 ("#Find" ,["derivativeEq f_f'"])
4.32 ],
4.33 {rew_ord'="tless_true", rls' = erls_diff, calc = [],
4.34 - srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
4.35 + srls = srls_diff, prls=e_rls, crls=Atools_erls, errpats = [], nrls = norm_diff},
4.36 "Script DiffEqScr (f_f::bool) (v_v::real) = " ^
4.37 " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
4.38 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
4.39 @@ -385,7 +385,7 @@
4.40 ("#Find" ,["derivative f_f'"])
4.41 ],
4.42 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
4.43 - crls=Atools_erls, nrls = norm_Rational},
4.44 + crls=Atools_erls, errpats = [], nrls = norm_Rational},
4.45 "Script DiffScr (f_f::real) (v_v::real) = " ^
4.46 " (let f_f' = Take (d_d v_v f_f) " ^
4.47 " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed May 16 15:01:47 2012 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed May 16 15:47:22 2012 +0200
5.3 @@ -150,7 +150,7 @@
5.4 (["DiffApp"],
5.5 [],
5.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
5.7 - crls = Atools_erls, nrls = norm_Rational
5.8 + crls = Atools_erls, errpats = [], nrls = norm_Rational
5.9 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
5.10 *}
5.11 ML{*
5.12 @@ -163,7 +163,7 @@
5.13 ("#Relate",[])
5.14 ],
5.15 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
5.16 - crls = eval_rls, nrls = norm_Rational
5.17 + crls = eval_rls, errpats = [], nrls = norm_Rational
5.18 (*, asm_rls=[],asm_thm=[]*)},
5.19 "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
5.20 " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
5.21 @@ -189,7 +189,7 @@
5.22 ("#Find" ,["functionEq f_1"])
5.23 ],
5.24 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
5.25 - calc=[], crls = eval_rls, nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
5.26 + calc=[], crls = eval_rls, errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
5.27 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
5.28 " (eqs::bool list) = " ^
5.29 "(let h_h = (hd o (filterVar f_f)) eqs; " ^
5.30 @@ -216,7 +216,7 @@
5.31 ("#Find" ,["functionEq f_1"])
5.32 ],
5.33 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
5.34 - crls = eval_rls, nrls = norm_Rational
5.35 + crls = eval_rls, errpats = [], nrls = norm_Rational
5.36 (*, asm_rls=[],asm_thm=[]*)},
5.37 "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
5.38 " (eqs::bool list) = " ^
5.39 @@ -239,7 +239,7 @@
5.40 ("#Find" ,["maxArgument v_0"])
5.41 ],
5.42 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
5.43 - crls = eval_rls, nrls = norm_Rational
5.44 + crls = eval_rls, errpats = [], nrls = norm_Rational
5.45 (*, asm_rls=[],asm_thm=[]*)},
5.46 "empty_script"
5.47 ));
5.48 @@ -250,7 +250,7 @@
5.49 (["DiffApp","find_values"]:metID,
5.50 [],
5.51 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
5.52 - crls = eval_rls, nrls = norm_Rational(*,
5.53 + crls = eval_rls, errpats = [], nrls = norm_Rational(*,
5.54 asm_rls=[],asm_thm=[]*)},
5.55 "empty_script"));
5.56
6.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Wed May 16 15:01:47 2012 +0200
6.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed May 16 15:47:22 2012 +0200
6.3 @@ -45,7 +45,7 @@
6.4 ("#Find" ,["boolTestFind s_s"])
6.5 ],
6.6 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
6.7 - prls = e_rls, calc = [], crls = tval_rls, nrls = Test_simplify},
6.8 + prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
6.9 "Script Diophant_equation (e_e::bool) (v_v::int)= " ^
6.10 "(Repeat " ^
6.11 " ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed May 16 15:01:47 2012 +0200
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed May 16 15:47:22 2012 +0200
7.3 @@ -561,7 +561,7 @@
7.4 (["EqSystem"],
7.5 [],
7.6 {rew_ord'="tless_true", rls' = Erls, calc = [],
7.7 - srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
7.8 + srls = Erls, prls = Erls, crls = Erls, errpats = [], nrls = Erls},
7.9 "empty_script"
7.10 ));
7.11 store_met
7.12 @@ -569,7 +569,7 @@
7.13 (["EqSystem","top_down_substitution"],
7.14 [],
7.15 {rew_ord'="tless_true", rls' = Erls, calc = [],
7.16 - srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
7.17 + srls = Erls, prls = Erls, crls = Erls, errpats = [], nrls = Erls},
7.18 "empty_script"
7.19 ));
7.20 *}
7.21 @@ -589,7 +589,7 @@
7.22 Thm ("tl_Cons",num_str @{thm tl_Cons}),
7.23 Thm ("tl_Nil",num_str @{thm tl_Nil})
7.24 ],
7.25 - prls = prls_triangular, crls = Erls, nrls = Erls},
7.26 + prls = prls_triangular, crls = Erls, errpats = [], nrls = Erls},
7.27 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.28 " (let e_1 = Take (hd e_s); " ^
7.29 " e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
7.30 @@ -631,7 +631,7 @@
7.31 (["EqSystem","normalize"],
7.32 [],
7.33 {rew_ord'="tless_true", rls' = Erls, calc = [],
7.34 - srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
7.35 + srls = Erls, prls = Erls, crls = Erls, errpats = [], nrls = Erls},
7.36 "empty_script"
7.37 ));
7.38 *}
7.39 @@ -647,7 +647,7 @@
7.40 Thm ("tl_Cons",num_str @{thm tl_Cons}),
7.41 Thm ("tl_Nil",num_str @{thm tl_Nil})
7.42 ],
7.43 - prls = Erls, crls = Erls, nrls = Erls},
7.44 + prls = Erls, crls = Erls, errpats = [], nrls = Erls},
7.45 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.46 " (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
7.47 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
7.48 @@ -690,7 +690,7 @@
7.49 Thm ("tl_Cons",num_str @{thm tl_Cons}),
7.50 Thm ("tl_Nil",num_str @{thm tl_Nil})
7.51 ],
7.52 - prls = Erls, crls = Erls, nrls = Erls},
7.53 + prls = Erls, crls = Erls, errpats = [], nrls = Erls},
7.54 (*STOPPED.WN06? met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
7.55 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.56 " (let e__s = " ^
7.57 @@ -726,7 +726,7 @@
7.58 srls = append_rls "srls_top_down_4x4" srls [],
7.59 prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular
7.60 [Calc ("Atools.occurs'_in",eval_occurs_in "")],
7.61 - crls = Erls, nrls = Erls},
7.62 + crls = Erls, errpats = [], nrls = Erls},
7.63 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
7.64 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.65 " (let e_1 = NTH 1 e_s; " ^
8.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed May 16 15:01:47 2012 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed May 16 15:47:22 2012 +0200
8.3 @@ -105,7 +105,7 @@
8.4 {rew_ord'="tless_true", rls'=Erls, calc = [],
8.5 srls = e_rls,
8.6 prls=e_rls,
8.7 - crls = Atools_erls, nrls = e_rls},
8.8 + crls = Atools_erls, errpats = [], nrls = e_rls},
8.9 "empty_script"
8.10 ));
8.11 *}
9.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Wed May 16 15:01:47 2012 +0200
9.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Wed May 16 15:47:22 2012 +0200
9.3 @@ -85,7 +85,7 @@
9.4 (["InsSort"],
9.5 [],
9.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
9.7 - crls = Atools_rls, nrls = norm_Rational
9.8 + crls = Atools_rls, errpats = [], nrls = norm_Rational
9.9 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
9.10 store_met
9.11 (prep_met (Thy_Info.get_theory "InsSort") (*test-version for [#1,#3,#2] only: see *.sml*)
9.12 @@ -94,7 +94,7 @@
9.13 ("#Find" ,["sorted s_"])
9.14 ],
9.15 {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls,
9.16 - crls = eval_rls, nrls = norm_Rational},
9.17 + crls = eval_rls, errpats = [], nrls = norm_Rational},
9.18 "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
9.19 ));
9.20
10.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed May 16 15:01:47 2012 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed May 16 15:47:22 2012 +0200
10.3 @@ -374,7 +374,7 @@
10.4 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
10.5 srls = e_rls,
10.6 prls=e_rls,
10.7 - crls = Atools_erls, nrls = e_rls},
10.8 + crls = Atools_erls, errpats = [], nrls = e_rls},
10.9 "Script IntegrationScript (f_f::real) (v_v::real) = " ^
10.10 " (let t_t = Take (Integral f_f D v_v) " ^
10.11 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"
10.12 @@ -391,7 +391,7 @@
10.13 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
10.14 srls = e_rls,
10.15 prls=e_rls,
10.16 - crls = Atools_erls, nrls = e_rls},
10.17 + crls = Atools_erls, errpats = [], nrls = e_rls},
10.18 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
10.19 " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
10.20 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^
11.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed May 16 15:01:47 2012 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed May 16 15:47:22 2012 +0200
11.3 @@ -89,12 +89,12 @@
11.4 (prep_met thy "met_SP" [] e_metID
11.5 (["SignalProcessing"], [],
11.6 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
11.7 - crls = e_rls, nrls = e_rls}, "empty_script"));
11.8 + crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
11.9 store_met
11.10 (prep_met thy "met_SP_Ztrans" [] e_metID
11.11 (["SignalProcessing", "Z_Transform"], [],
11.12 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
11.13 - crls = e_rls, nrls = e_rls}, "empty_script"));
11.14 + crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
11.15 val thy = @{theory}; (*latest version of thy required*)
11.16 store_met
11.17 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
11.18 @@ -103,7 +103,7 @@
11.19 ("#Find" ,["stepResponse (n_eq::bool)"])
11.20 ],
11.21 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
11.22 - crls = e_rls, nrls = e_rls},
11.23 + crls = e_rls, errpats = [], nrls = e_rls},
11.24 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
11.25 " (let X = Take X_eq;" ^
11.26 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
11.27 @@ -136,7 +136,7 @@
11.28 rls'= e_rls, calc = [],
11.29 srls = srls_partial_fraction,
11.30 prls = e_rls,
11.31 - crls = e_rls, nrls = e_rls
11.32 + crls = e_rls, errpats = [], nrls = e_rls
11.33 },
11.34 "Script InverseZTransform (X_eq::bool) = "^
11.35 (*(1/z) instead of z ^^^ -1*)
11.36 @@ -236,7 +236,7 @@
11.37 eval_factors_from_solution "#factors_from_solution"),
11.38 Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
11.39 scr = EmptyScr},
11.40 - prls = e_rls, crls = e_rls, nrls = norm_Rational},
11.41 + prls = e_rls, crls = e_rls, errpats = [], nrls = norm_Rational},
11.42 "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
11.43 "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
11.44 " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
12.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed May 16 15:01:47 2012 +0200
12.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed May 16 15:47:22 2012 +0200
12.3 @@ -145,7 +145,7 @@
12.4 (["LinEq"],
12.5 [],
12.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
12.7 - crls=LinEq_crls, nrls = norm_Poly}, "empty_script"));
12.8 + crls=LinEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"));
12.9
12.10 (* ansprechen mit ["LinEq","solve_univar_equation"] *)
12.11 store_met
12.12 @@ -157,7 +157,7 @@
12.13 ("#Find", ["solutions v_v'i'"])
12.14 ],
12.15 {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
12.16 - calc=[], crls=LinEq_crls, nrls = norm_Poly},
12.17 + calc=[], crls=LinEq_crls, errpats = [], nrls = norm_Poly},
12.18 "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
12.19 "(let e_e =((Try (Rewrite all_left False)) @@ " ^
12.20 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
13.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Wed May 16 15:01:47 2012 +0200
13.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed May 16 15:47:22 2012 +0200
13.3 @@ -50,7 +50,7 @@
13.4 ("#Find" ,["solutions v_v'i'"])
13.5 ],
13.6 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
13.7 - calc=[],crls=PolyEq_crls, nrls = norm_Rational},
13.8 + calc=[],crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
13.9 "Script Solve_log (e_e::bool) (v_v::real) = " ^
13.10 "(let e_e = ((Rewrite equality_power False) @@ " ^
13.11 " (Rewrite exp_invers_log False) @@ " ^
14.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed May 16 15:01:47 2012 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed May 16 15:47:22 2012 +0200
14.3 @@ -243,7 +243,7 @@
14.4 ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
14.5 ("#Find" ,["decomposedFunction p_p'''"])],
14.6 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls,
14.7 - crls = e_rls, nrls = e_rls}, (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
14.8 + crls = e_rls, errpats = [], nrls = e_rls}, (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
14.9 "Script PartFracScript (f_f::real) (zzz::real) = " ^(*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
14.10 "(let f_f = Take f_f; " ^(*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
14.11 " (num_orig::real) = get_numerator f_f; " ^(* num_orig = 3*)
15.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed May 16 15:01:47 2012 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed May 16 15:47:22 2012 +0200
15.3 @@ -1645,7 +1645,7 @@
15.4 prls = append_rls "simplification_for_polynomials_prls" e_rls
15.5 [(*for preds in where_*)
15.6 Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
15.7 - crls = e_rls, nrls = norm_Poly},
15.8 + crls = e_rls, errpats = [], nrls = norm_Poly},
15.9 "Script SimplifyScript (t_t::real) = " ^
15.10 " ((Rewrite_Set norm_Poly False) t_t)"
15.11 ));
16.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed May 16 15:01:47 2012 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed May 16 15:47:22 2012 +0200
16.3 @@ -1041,7 +1041,7 @@
16.4 (["PolyEq"],
16.5 [],
16.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
16.7 - crls=PolyEq_crls, nrls = norm_Rational}, "empty_script"));
16.8 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"));
16.9
16.10 store_met
16.11 (prep_met thy "met_polyeq_norm" [] e_metID
16.12 @@ -1056,7 +1056,7 @@
16.13 srls=e_rls,
16.14 prls=PolyEq_prls,
16.15 calc=[],
16.16 - crls=PolyEq_crls, nrls = norm_Rational},
16.17 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.18 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
16.19 "(let e_e =((Try (Rewrite all_left False)) @@ " ^
16.20 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
16.21 @@ -1083,7 +1083,7 @@
16.22 srls=e_rls,
16.23 prls=PolyEq_prls,
16.24 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.25 - crls=PolyEq_crls, nrls = norm_Rational},
16.26 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.27 "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
16.28 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
16.29 " d0_polyeq_simplify False))) e_e " ^
16.30 @@ -1101,7 +1101,7 @@
16.31 ],
16.32 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
16.33 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.34 - crls=PolyEq_crls, nrls = norm_Rational},
16.35 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.36 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
16.37 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
16.38 " d1_polyeq_simplify True)) @@ " ^
16.39 @@ -1125,7 +1125,7 @@
16.40 srls=e_rls,
16.41 prls=PolyEq_prls,
16.42 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.43 - crls=PolyEq_crls, nrls = norm_Rational},
16.44 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.45 "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
16.46 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
16.47 " d2_polyeq_simplify True)) @@ " ^
16.48 @@ -1152,7 +1152,7 @@
16.49 srls=e_rls,
16.50 prls=PolyEq_prls,
16.51 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.52 - crls=PolyEq_crls, nrls = norm_Rational},
16.53 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.54 "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
16.55 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
16.56 " d2_polyeq_bdv_only_simplify True)) @@ " ^
16.57 @@ -1179,7 +1179,7 @@
16.58 srls=e_rls,
16.59 prls=PolyEq_prls,
16.60 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.61 - crls=PolyEq_crls, nrls = norm_Rational},
16.62 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.63 "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
16.64 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
16.65 " d2_polyeq_sq_only_simplify True)) @@ " ^
16.66 @@ -1203,7 +1203,7 @@
16.67 srls=e_rls,
16.68 prls=PolyEq_prls,
16.69 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.70 - crls=PolyEq_crls, nrls = norm_Rational},
16.71 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.72 "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
16.73 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
16.74 " d2_polyeq_pqFormula_simplify True)) @@ " ^
16.75 @@ -1227,7 +1227,7 @@
16.76 srls=e_rls,
16.77 prls=PolyEq_prls,
16.78 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.79 - crls=PolyEq_crls, nrls = norm_Rational},
16.80 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.81 "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
16.82 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
16.83 " d2_polyeq_abcFormula_simplify True)) @@ " ^
16.84 @@ -1251,7 +1251,7 @@
16.85 srls=e_rls,
16.86 prls=PolyEq_prls,
16.87 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.88 - crls=PolyEq_crls, nrls = norm_Rational},
16.89 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.90 "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
16.91 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
16.92 " d3_polyeq_simplify True)) @@ " ^
16.93 @@ -1281,7 +1281,7 @@
16.94 ],
16.95 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
16.96 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
16.97 - crls=PolyEq_crls, nrls = norm_Rational},
16.98 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.99 "Script Complete_square (e_e::bool) (v_v::real) = " ^
16.100 "(let e_e = " ^
16.101 " ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^
17.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed May 16 15:01:47 2012 +0200
17.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed May 16 15:47:22 2012 +0200
17.3 @@ -526,7 +526,7 @@
17.4 (*"(~ True) = False"*)
17.5 Thm ("not_false",num_str @{thm not_false})
17.6 (*"(~ False) = True"*)],
17.7 - crls = e_rls, nrls = rls_p_33},
17.8 + crls = e_rls, errpats = [], nrls = rls_p_33},
17.9 "Script SimplifyScript (t_t::real) = " ^
17.10 " ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
17.11 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
17.12 @@ -544,7 +544,7 @@
17.13 prls = append_rls "simplification_for_polynomials_prls" e_rls
17.14 [(*for preds in where_*)
17.15 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
17.16 - crls = e_rls, nrls = rls_p_34},
17.17 + crls = e_rls, errpats = [], nrls = rls_p_34},
17.18 "Script SimplifyScript (t_t::real) = " ^
17.19 " ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
17.20 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
17.21 @@ -563,7 +563,7 @@
17.22 prls = append_rls "simplification_for_polynomials_prls" e_rls
17.23 [(*for preds in where_*)
17.24 Calc("Poly.is'_polyexp",eval_is_polyexp"")],
17.25 - crls = e_rls, nrls = rls_p_34},
17.26 + crls = e_rls, errpats = [], nrls = rls_p_34},
17.27 "Script SimplifyScript (t_t::real) = " ^
17.28 " ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ " ^
17.29 " (Try (Rewrite_Set discard_parentheses False)) @@ " ^
17.30 @@ -579,7 +579,7 @@
17.31 (["probe"],
17.32 [],
17.33 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
17.34 - prls = Erls, crls = e_rls, nrls = Erls},
17.35 + prls = Erls, crls = e_rls, errpats = [], nrls = Erls},
17.36 "empty_script"));
17.37
17.38 store_met
17.39 @@ -594,7 +594,7 @@
17.40 e_rls [(*for preds in where_*)
17.41 Calc ("Rational.is'_ratpolyexp",
17.42 eval_is_ratpolyexp "")],
17.43 - crls = e_rls, nrls = rechnen},
17.44 + crls = e_rls, errpats = [], nrls = rechnen},
17.45 "Script ProbeScript (e_e::bool) (w_w::bool list) = " ^
17.46 " (let e_e = Take e_e; " ^
17.47 " e_e = Substitute w_w e_e " ^
17.48 @@ -615,7 +615,7 @@
17.49 e_rls [(*for preds in where_*)
17.50 Calc ("Rational.is'_ratpolyexp",
17.51 eval_is_ratpolyexp "")],
17.52 - crls = e_rls, nrls = Erls},
17.53 + crls = e_rls, errpats = [], nrls = Erls},
17.54 "empty_script"));
17.55 *}
17.56
18.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed May 16 15:01:47 2012 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed May 16 15:47:22 2012 +0200
18.3 @@ -201,7 +201,7 @@
18.4 (["RatEq"],
18.5 [],
18.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
18.7 - crls=RatEq_crls, nrls = norm_Rational}, "empty_script"));
18.8 + crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"));
18.9 *}
18.10
18.11 ML {*
18.12 @@ -217,7 +217,7 @@
18.13 srls=e_rls,
18.14 prls=RatEq_prls,
18.15 calc=[],
18.16 - crls=RatEq_crls, nrls = norm_Rational},
18.17 + crls=RatEq_crls, errpats = [], nrls = norm_Rational},
18.18 "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
18.19 "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^
18.20 " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^
19.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed May 16 15:01:47 2012 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed May 16 15:47:22 2012 +0200
19.3 @@ -3838,7 +3838,7 @@
19.4 [(*for preds in where_*)
19.5 Calc ("Rational.is'_ratpolyexp",
19.6 eval_is_ratpolyexp "")],
19.7 - crls = e_rls, nrls = norm_Rational_rls},
19.8 + crls = e_rls, errpats = [], nrls = norm_Rational_rls},
19.9 "Script SimplifyScript (t_t::real) = " ^
19.10 " ((Try (Rewrite_Set discard_minus False) @@ " ^
19.11 " Try (Rewrite_Set rat_mult_poly False) @@ " ^
20.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed May 16 15:01:47 2012 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed May 16 15:47:22 2012 +0200
20.3 @@ -530,7 +530,7 @@
20.4 (["RootEq"],
20.5 [],
20.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
20.7 - crls=RootEq_crls, nrls = norm_Poly}, "empty_script"));
20.8 + crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"));
20.9
20.10 (*-- normalize 20.10.02 --*)
20.11 store_met
20.12 @@ -544,7 +544,7 @@
20.13 ("#Find" ,["solutions v_v'i'"])
20.14 ],
20.15 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
20.16 - calc=[], crls=RootEq_crls, nrls = norm_Poly},
20.17 + calc=[], crls=RootEq_crls, errpats = [], nrls = norm_Poly},
20.18 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
20.19 "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
20.20 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
20.21 @@ -570,7 +570,7 @@
20.22 ("#Find" ,["solutions v_v'i'"])
20.23 ],
20.24 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
20.25 - prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls = norm_Poly},
20.26 + prls = RootEq_prls, calc = [], crls=RootEq_crls, errpats = [], nrls = norm_Poly},
20.27 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
20.28 "(let e_e = " ^
20.29 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
20.30 @@ -598,7 +598,7 @@
20.31 ("#Find" ,["solutions v_v'i'"])
20.32 ],
20.33 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls,
20.34 - prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
20.35 + prls = RootEq_prls, calc = [], crls = RootEq_crls, errpats = [], nrls = norm_Poly},
20.36 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
20.37 "(let e_e = " ^
20.38 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^
20.39 @@ -627,7 +627,7 @@
20.40 srls=e_rls,
20.41 prls=RootEq_prls,
20.42 calc=[],
20.43 - crls=RootEq_crls, nrls = norm_Poly},
20.44 + crls=RootEq_crls, errpats = [], nrls = norm_Poly},
20.45 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
20.46 "(let e_e = " ^
20.47 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^
21.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed May 16 15:01:47 2012 +0200
21.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed May 16 15:47:22 2012 +0200
21.3 @@ -162,7 +162,7 @@
21.4 (["RootRatEq"],
21.5 [],
21.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
21.7 - crls=Atools_erls, nrls = norm_Rational}, "empty_script"));
21.8 + crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script"));
21.9 (*-- left 20.10.02 --*)
21.10 store_met
21.11 (prep_met thy "met_rootrateq_elim" [] e_metID
21.12 @@ -177,7 +177,7 @@
21.13 srls=e_rls,
21.14 prls=RootRatEq_prls,
21.15 calc=[],
21.16 - crls=RootRatEq_crls, nrls = norm_Rational},
21.17 + crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
21.18 "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
21.19 "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^
21.20 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
22.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Wed May 16 15:01:47 2012 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed May 16 15:47:22 2012 +0200
22.3 @@ -47,23 +47,21 @@
22.4 append_rls "e_rls" e_rls [(*for preds in where_*)],
22.5 SOME "Vereinfache t_t",
22.6 []));
22.7 +*}
22.8 +ML {*
22.9
22.10 (** methods **)
22.11
22.12 store_met
22.13 - (prep_met thy "met_tsimp" [] e_metID
22.14 - (["simplification"],
22.15 - [("#Given" ,["Term t_t"]),
22.16 - ("#Find" ,["normalform n_n"])
22.17 - ],
22.18 - {rew_ord'="tless_true",
22.19 - rls'= e_rls,
22.20 - calc = [],
22.21 - srls = e_rls,
22.22 - prls=e_rls,
22.23 - crls = e_rls, nrls = e_rls},
22.24 - "empty_script"
22.25 - ));
22.26 + (prep_met thy "met_tsimp" [] e_metID
22.27 + (["simplification"],
22.28 + [("#Given" ,["Term t_t"]),
22.29 + ("#Find" ,["normalform n_n"])],
22.30 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls=e_rls,
22.31 + crls = e_rls, errpats = [], nrls = e_rls},
22.32 + "empty_script"));
22.33 +*}
22.34 +ML {*
22.35
22.36 (** CAS-command **)
22.37
23.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed May 16 15:01:47 2012 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed May 16 15:47:22 2012 +0200
23.3 @@ -596,7 +596,7 @@
23.4 (["Test"],
23.5 [],
23.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
23.7 - crls=Atools_erls, nrls = e_rls}, "empty_script"));
23.8 + crls=Atools_erls, errpats = [], nrls = e_rls}, "empty_script"));
23.9 *}
23.10 ML {*
23.11 store_met
23.12 @@ -608,7 +608,7 @@
23.13 ],
23.14 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
23.15 prls = assoc_rls "matches", calc = [], crls = tval_rls,
23.16 - nrls = Test_simplify},
23.17 + errpats = [], nrls = Test_simplify},
23.18 "Script Solve_linear (e_e::bool) (v_v::real)= " ^
23.19 "(let e_e = " ^
23.20 " Repeat " ^
23.21 @@ -915,7 +915,7 @@
23.22 prls =append_rls "prls_contains_root" e_rls
23.23 [Calc ("Test.contains'_root",eval_contains_root "")],
23.24 calc=[],
23.25 - crls=tval_rls, nrls = e_rls(*,asm_rls=[],
23.26 + crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
23.27 asm_thm=[("square_equation_left",""),
23.28 ("square_equation_right","")]*)},
23.29 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.30 @@ -947,7 +947,7 @@
23.31 srls = append_rls "srls_contains_root" e_rls
23.32 [Calc ("Test.contains'_root",eval_contains_root"")],
23.33 prls=e_rls,calc=[],
23.34 - crls=tval_rls, nrls = e_rls(*,asm_rls=[],
23.35 + crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
23.36 asm_thm=[("square_equation_left",""),
23.37 ("square_equation_right","")]*)},
23.38 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.39 @@ -981,7 +981,7 @@
23.40 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
23.41 prls = append_rls "prls_met_test_squ_sub" e_rls
23.42 [Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
23.43 - calc=[], crls=tval_rls, nrls = Test_simplify},
23.44 + calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
23.45 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.46 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
23.47 " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
23.48 @@ -1003,7 +1003,7 @@
23.49 ("#Find" ,["solutions v_v'i'"])
23.50 ],
23.51 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
23.52 - crls=tval_rls, nrls = e_rls(*,
23.53 + crls=tval_rls, errpats = [], nrls = e_rls(*,
23.54 asm_rls=[],asm_thm=[("square_equation_left",""),
23.55 ("square_equation_right","")]*)},
23.56 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.57 @@ -1026,7 +1026,7 @@
23.58 srls = append_rls "srls_contains_root" e_rls
23.59 [Calc ("Test.contains'_root",eval_contains_root"")],
23.60 prls=e_rls,calc=[],
23.61 - crls=tval_rls, nrls = e_rls(*,asm_rls=[],
23.62 + crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
23.63 asm_thm=[("square_equation_left",""),
23.64 ("square_equation_right","")]*)},
23.65 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.66 @@ -1059,7 +1059,7 @@
23.67 srls = append_rls "srls_contains_root" e_rls
23.68 [Calc ("Test.contains'_root",eval_contains_root"")],
23.69 prls=e_rls,calc=[],
23.70 - crls=tval_rls, nrls = e_rls(*,asm_rls=[],
23.71 + crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
23.72 asm_thm=[("square_equation_left",""),
23.73 ("square_equation_right","")]*)},
23.74 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.75 @@ -1091,7 +1091,7 @@
23.76 srls = append_rls "srls_contains_root" e_rls
23.77 [Calc ("Test.contains'_root",eval_contains_root"")],
23.78 prls=e_rls,calc=[],
23.79 - crls=tval_rls, nrls = e_rls(*,asm_rls=[],
23.80 + crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
23.81 asm_thm=[("square_equation_left",""),
23.82 ("square_equation_right","")]*)},
23.83 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.84 @@ -1124,7 +1124,7 @@
23.85 srls = append_rls "srls_contains_root" e_rls
23.86 [Calc ("Test.contains'_root",eval_contains_root"")],
23.87 prls=e_rls,calc=[],
23.88 - crls=tval_rls, nrls = e_rls(*,asm_rls=[],
23.89 + crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
23.90 asm_thm=[("square_equation_left",""),
23.91 ("square_equation_right","")]*)},
23.92 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.93 @@ -1159,7 +1159,7 @@
23.94 ],
23.95 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
23.96 prls = assoc_rls "matches",
23.97 - crls=tval_rls, nrls = e_rls(*,
23.98 + crls=tval_rls, errpats = [], nrls = e_rls(*,
23.99 asm_rls=[],asm_thm=[]*)},
23.100 "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
23.101 " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
23.102 @@ -1182,7 +1182,7 @@
23.103 ],
23.104 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
23.105 calc=[],
23.106 - crls=tval_rls, nrls = e_rls},
23.107 + crls=tval_rls, errpats = [], nrls = e_rls},
23.108 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
23.109 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
23.110 " (Try (Rewrite_Set Test_simplify False))) e_e " ^
23.111 @@ -1200,7 +1200,7 @@
23.112 ("#Find" ,["intTestFind s_s"])
23.113 ],
23.114 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
23.115 - prls = e_rls, calc = [], crls = tval_rls, nrls = Test_simplify},
23.116 + prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
23.117 "Script STest_simplify (t_t::int) = " ^
23.118 "(Repeat " ^
23.119 " ((Try (Calculate PLUS)) @@ " ^
24.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Wed May 16 15:01:47 2012 +0200
24.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Wed May 16 15:47:22 2012 +0200
24.3 @@ -204,7 +204,7 @@
24.4 requires elements (rls, calc, ...) to be reorganized.*)
24.5 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
24.6 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
24.7 - crls,erls,(*errpats,*)nrls,prls,srls,rew_ord'}:met) =
24.8 + crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
24.9 let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
24.10 val crls' = (#id o rep_rls) crls
24.11 val erls' = (#id o rep_rls) erls
24.12 @@ -242,7 +242,7 @@
24.13 (*.format a method in xml for presentation on the method browser;
24.14 old version with 'dead' strings for rls, calc, ....*)
24.15 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
24.16 - crls,erls,(*errpats,*)nrls,prls,srls,rew_ord'}:met) =
24.17 + crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
24.18 "<NODECONTENT>\n" ^
24.19 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
24.20 id2xml i id ^
25.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed May 16 15:01:47 2012 +0200
25.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed May 16 15:47:22 2012 +0200
25.3 @@ -938,13 +938,13 @@
25.4 (["SignalProcessing"], [],
25.5 {rew_ord'="tless_true", rls'= e_rls, calc = [],
25.6 srls = e_rls, prls = e_rls,
25.7 - crls = e_rls, nrls = e_rls}, "empty_script"));
25.8 + crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
25.9 store_met
25.10 (prep_met thy "met_SP_Ztrans" [] e_metID
25.11 (["SignalProcessing", "Z_Transform"], [],
25.12 {rew_ord'="tless_true", rls'= e_rls, calc = [],
25.13 srls = e_rls, prls = e_rls,
25.14 - crls = e_rls, nrls = e_rls}, "empty_script"));
25.15 + crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
25.16 *}
25.17
25.18 text{*\noindent After we generated both nodes, we can fill the containing
25.19 @@ -960,7 +960,7 @@
25.20 ],
25.21 {rew_ord'="tless_true", rls'= e_rls, calc = [],
25.22 srls = e_rls, prls = e_rls,
25.23 - crls = e_rls, nrls = e_rls}, "empty_script"));
25.24 + crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
25.25 *}
25.26
25.27 text{*\noindent After we stored the definition we can start implementing the
25.28 @@ -976,7 +976,7 @@
25.29 ],
25.30 {rew_ord'="tless_true", rls'= e_rls, calc = [],
25.31 srls = e_rls, prls = e_rls,
25.32 - crls = e_rls, nrls = e_rls},
25.33 + crls = e_rls, errpats = [], nrls = e_rls},
25.34 "Script InverseZTransform (Xeq::bool) =" ^
25.35 " (let X = Take Xeq;" ^
25.36 " X = Rewrite ruleZY False X" ^
25.37 @@ -1160,7 +1160,7 @@
25.38 rls'= e_rls, calc = [],
25.39 srls = srls,
25.40 prls = e_rls,
25.41 - crls = e_rls, nrls = e_rls
25.42 + crls = e_rls, errpats = [], nrls = e_rls
25.43 },
25.44 "Script InverseZTransform (X_eq::bool) = "^
25.45 (*(1/z) instead of z ^^^ -1*)
26.1 --- a/test/Tools/isac/Interpret/solve.sml Wed May 16 15:01:47 2012 +0200
26.2 +++ b/test/Tools/isac/Interpret/solve.sml Wed May 16 15:47:22 2012 +0200
26.3 @@ -114,7 +114,7 @@
26.4 ("#Find" ,["realTestFind s_s"])
26.5 ],
26.6 {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
26.7 - crls = tval_rls, nrls = e_rls(*,
26.8 + crls = tval_rls, errpats = [], nrls = e_rls(*,
26.9 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
26.10 "Script Testterm (g_g::real) = \
26.11 \(((Rewrite_Set expand_binoms False) @@\
26.12 @@ -127,7 +127,7 @@
26.13 ("#Find" ,["realTestFind s_s"])
26.14 ],
26.15 {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
26.16 - crls = tval_rls, nrls = e_rls(*,
26.17 + crls = tval_rls, errpats = [], nrls = e_rls(*,
26.18 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
26.19 "Script Testterm (g_g::real) = \
26.20 \(((Rewrite_Set make_polynomial False) @@\
27.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed May 16 15:01:47 2012 +0200
27.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed May 16 15:47:22 2012 +0200
27.3 @@ -513,7 +513,7 @@
27.4 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
27.5 srls = e_rls,
27.6 prls=e_rls,
27.7 - crls = Atools_erls, nrls = e_rls},
27.8 + crls = Atools_erls, errpats = [], nrls = e_rls},
27.9 "Script IntegrationScript (f_f::real) (v_v::real) = \
27.10 \ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
27.11 \ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \
28.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Wed May 16 15:01:47 2012 +0200
28.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Wed May 16 15:47:22 2012 +0200
28.3 @@ -39,7 +39,7 @@
28.4 ("#Find" ,["realTestFind f_"])
28.5 ],
28.6 {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
28.7 - crls=tval_rls, nrls=e_rls(*,
28.8 + crls=tval_rls, errpats = [], nrls=e_rls(*,
28.9 asm_rls=[],asm_thm=[]*)},
28.10 "Script Testterm (g_::real) = \
28.11 \Repeat\
28.12 @@ -109,7 +109,7 @@
28.13 {rew_ord'="tless_true",rls'=tval_rls,
28.14 srls=append_rls "testeq1_srls" e_rls
28.15 [Calc ("Test.contains'_root", eval_contains_root"")],
28.16 - prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls
28.17 + prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls=e_rls
28.18 (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
28.19 "Script Testeq (e_e::bool) = \
28.20 \(While (contains_root e_e) Do \
28.21 @@ -167,7 +167,7 @@
28.22 {rew_ord'="tless_true",rls'=tval_rls,
28.23 srls=append_rls "testlet_srls" e_rls
28.24 [Calc ("Test.contains'_root",eval_contains_root"")],
28.25 - prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls
28.26 + prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls=e_rls
28.27 (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
28.28 "Script Testeq2 (e_e::bool) = \
28.29 \(let e_e =\
29.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed May 16 15:01:47 2012 +0200
29.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed May 16 15:47:22 2012 +0200
29.3 @@ -97,7 +97,7 @@
29.4 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
29.5 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
29.6 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
29.7 - crls=tval_rls, nrls=e_rls(*,
29.8 + crls=tval_rls, errpats = [], nrls=e_rls(*,
29.9 asm_rls=[],asm_thm=[]*)},
29.10 "Script STest_simplify (t_t::real) = \
29.11 \(Repeat \
30.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Wed May 16 15:01:47 2012 +0200
30.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Wed May 16 15:47:22 2012 +0200
30.3 @@ -28,7 +28,7 @@
30.4 ("#Find" ,["normalform n_n"])
30.5 ],
30.6 {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
30.7 - crls=tval_rls, nrls=e_rls},
30.8 + crls=tval_rls, errpats = [], nrls=e_rls},
30.9 "Script Stepwise t_t = \
30.10 \(Try (Rewrite_Set discard_minus False) @@ \
30.11 \ Try (Rewrite_Set expand_poly False) @@ \
31.1 --- a/test/Tools/isac/Test_Isac.thy Wed May 16 15:01:47 2012 +0200
31.2 +++ b/test/Tools/isac/Test_Isac.thy Wed May 16 15:47:22 2012 +0200
31.3 @@ -8,7 +8,7 @@
31.4 10 20 30 40 50 60 70 80 90 100
31.5 *)
31.6
31.7 -theory Test_Isac imports
31.8 +theory Test_Isac imports
31.9 Isac
31.10 "Knowledge/Rational_Test"
31.11 "ADDTESTS/Ctxt"
31.12 @@ -100,7 +100,7 @@
31.13
31.14 begin
31.15
31.16 - ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
31.17 + ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
31.18 use "library.sml"
31.19 use "calcelems.sml"
31.20 use "ProgLang/termC.sml"