1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Mon Sep 06 14:48:38 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Mon Sep 06 15:09:37 2010 +0200
1.3 @@ -55,7 +55,7 @@
1.4 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
1.5 (*
1.6 Don't use
1.7 - Calc ("HOL.divide", eval_cancel "#divide_"),
1.8 + Calc ("HOL.divide", eval_cancel "#divide_e"),
1.9 Calc ("Atools.pow" ,eval_binop "#power_"),
1.10 *)
1.11 ];
1.12 @@ -66,7 +66,7 @@
1.13 [Thm ("real_assoc_1",num_str @{thm real_assoc_1})
1.14 (*
1.15 Don't use
1.16 - Calc ("HOL.divide", eval_cancel "#divide_"),
1.17 + Calc ("HOL.divide", eval_cancel "#divide_e"),
1.18 Calc ("Atools.pow" ,eval_binop "#power_"),
1.19 *)
1.20 ];
1.21 @@ -88,7 +88,7 @@
1.22 Calc ("op -",eval_binop "#sub_"),
1.23 Calc ("op *",eval_binop "#mult_"),
1.24 (* Dont use
1.25 - Calc ("HOL.divide", eval_cancel "#divide_"),
1.26 + Calc ("HOL.divide", eval_cancel "#divide_e"),
1.27 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.28 *)
1.29 Calc ("Atools.pow" ,eval_binop "#power_")
1.30 @@ -128,15 +128,15 @@
1.31 store_pbt
1.32 (prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
1.33 (["linear","univariate","equation"],
1.34 - [("#Given" ,["equality e_","solveFor v_"]),
1.35 + [("#Given" ,["equality e_e","solveFor v_v"]),
1.36 ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*)
1.37 - "Not( (lhs e_) is_polyrat_in v_)",
1.38 - "Not( (rhs e_) is_polyrat_in v_)",
1.39 - "((lhs e_) has_degree_in v_)=1",
1.40 - "((rhs e_) has_degree_in v_)=1"]),
1.41 - ("#Find" ,["solutions v_i_"])
1.42 + "Not( (lhs e_e) is_polyrat_in v_v)",
1.43 + "Not( (rhs e_e) is_polyrat_in v_v)",
1.44 + "((lhs e_e) has_degree_in v_v)=1",
1.45 + "((rhs e_e) has_degree_in v_v)=1"]),
1.46 + ("#Find" ,["solutions v_i"])
1.47 ],
1.48 - LinEq_prls, SOME "solve (e_::bool, v_)",
1.49 + LinEq_prls, SOME "solve (e_e::bool, v_v)",
1.50 [["LinEq","solve_lineq_equation"]]));
1.51
1.52 (*-------------- methods------------------------------------------------------*)
1.53 @@ -152,10 +152,10 @@
1.54 store_met
1.55 (prep_met thy "met_eq_lin" [] e_metID
1.56 (["LinEq","solve_lineq_equation"],
1.57 - [("#Given" ,["equality e_","solveFor v_"]),
1.58 - ("#Where" ,["Not( (lhs e_) is_polyrat_in v_)",
1.59 - "( (lhs e_) has_degree_in v_)=1"]),
1.60 - ("#Find" ,["solutions v_i_"])
1.61 + [("#Given" ,["equality e_e","solveFor v_v"]),
1.62 + ("#Where" ,["Not( (lhs e_e) is_polyrat_in v_v)",
1.63 + "( (lhs e_e) has_degree_in v_v)=1"]),
1.64 + ("#Find" ,["solutions v_i"])
1.65 ],
1.66 {rew_ord'="termlessI",
1.67 rls'=LinEq_erls,
1.68 @@ -165,17 +165,17 @@
1.69 crls=LinEq_crls, nrls=norm_Poly(*,
1.70 asm_rls=[],
1.71 asm_thm=[("lin_isolate_div","")]*)},
1.72 - "Script Solve_lineq_equation (e_::bool) (v_::real) = " ^
1.73 - "(let e_ =((Try (Rewrite all_left False)) @@ " ^
1.74 + "Script Solve_lineq_equation (e_e::bool) (v_::real) = " ^
1.75 + "(let e_e =((Try (Rewrite all_left False)) @@ " ^
1.76 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
1.77 " (Try (Rewrite_Set expand_binoms False)) @@ " ^
1.78 " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.79 " make_ratpoly_in False))) @@ " ^
1.80 " (Try (Repeat (Rewrite_Set LinPoly_simplify False)))) e_;" ^
1.81 - " e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.82 + " e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.83 " LinEq_simplify True)) @@ " ^
1.84 - " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_ " ^
1.85 - " in ((Or_to_List e_)::bool list))"
1.86 + " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_e " ^
1.87 + " in ((Or_to_List e_e)::bool list))"
1.88 ));
1.89 "******* LinEq.ML end *******";
1.90 get_met ["LinEq","solve_lineq_equation"];