1.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Mar 15 10:17:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Thu Mar 15 12:42:04 2018 +0100
1.3 @@ -75,103 +75,103 @@
1.4 fun eval_is_ratequation_in _ _
1.5 (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _ =
1.6 if is_rateqation_in t v then
1.7 - SOME ((term2str p) ^ " = True",
1.8 + SOME ((Celem.term2str p) ^ " = True",
1.9 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.10 - else SOME ((term2str p) ^ " = True",
1.11 + else SOME ((Celem.term2str p) ^ " = True",
1.12 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.13 | eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
1.14
1.15 (*-------------------------rulse-----------------------*)
1.16 val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
1.17 - append_rls "RatEq_prls" e_rls
1.18 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.19 - Calc ("Tools.matches",eval_matches ""),
1.20 - Calc ("Tools.lhs" ,eval_lhs ""),
1.21 - Calc ("Tools.rhs" ,eval_rhs ""),
1.22 - Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
1.23 - Calc ("HOL.eq",eval_equal "#equal_"),
1.24 - Thm ("not_true",TermC.num_str @{thm not_true}),
1.25 - Thm ("not_false",TermC.num_str @{thm not_false}),
1.26 - Thm ("and_true",TermC.num_str @{thm and_true}),
1.27 - Thm ("and_false",TermC.num_str @{thm and_false}),
1.28 - Thm ("or_true",TermC.num_str @{thm or_true}),
1.29 - Thm ("or_false",TermC.num_str @{thm or_false})
1.30 + Celem.append_rls "RatEq_prls" Celem.e_rls
1.31 + [Celem.Calc ("Atools.ident",eval_ident "#ident_"),
1.32 + Celem.Calc ("Tools.matches",eval_matches ""),
1.33 + Celem.Calc ("Tools.lhs" ,eval_lhs ""),
1.34 + Celem.Calc ("Tools.rhs" ,eval_rhs ""),
1.35 + Celem.Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
1.36 + Celem.Calc ("HOL.eq",eval_equal "#equal_"),
1.37 + Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.38 + Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
1.39 + Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
1.40 + Celem.Thm ("and_false",TermC.num_str @{thm and_false}),
1.41 + Celem.Thm ("or_true",TermC.num_str @{thm or_true}),
1.42 + Celem.Thm ("or_false",TermC.num_str @{thm or_false})
1.43 ];
1.44
1.45
1.46 -(*rls = merge_rls erls Poly_erls *)
1.47 +(*rls = Celem.merge_rls erls Poly_erls *)
1.48 val rateq_erls =
1.49 - remove_rls "rateq_erls" (*WN: ein Hack*)
1.50 - (merge_rls "is_ratequation_in" calculate_Rational
1.51 - (append_rls "is_ratequation_in"
1.52 + Celem.remove_rls "rateq_erls" (*WN: ein Hack*)
1.53 + (Celem.merge_rls "is_ratequation_in" calculate_Rational
1.54 + (Celem.append_rls "is_ratequation_in"
1.55 Poly_erls
1.56 - [(*Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),*)
1.57 - Calc ("RatEq.is'_ratequation'_in",
1.58 + [(*Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),*)
1.59 + Celem.Calc ("RatEq.is'_ratequation'_in",
1.60 eval_is_ratequation_in "")
1.61
1.62 ]))
1.63 - [Thm ("and_commute",TermC.num_str @{thm and_commute}), (*WN: ein Hack*)
1.64 - Thm ("or_commute",TermC.num_str @{thm or_commute}) (*WN: ein Hack*)
1.65 + [Celem.Thm ("and_commute",TermC.num_str @{thm and_commute}), (*WN: ein Hack*)
1.66 + Celem.Thm ("or_commute",TermC.num_str @{thm or_commute}) (*WN: ein Hack*)
1.67 ];
1.68 *}
1.69 setup {* KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))] *}
1.70 ML {*
1.71
1.72 val RatEq_crls =
1.73 - remove_rls "RatEq_crls" (*WN: ein Hack*)
1.74 - (merge_rls "is_ratequation_in" calculate_Rational
1.75 - (append_rls "is_ratequation_in"
1.76 + Celem.remove_rls "RatEq_crls" (*WN: ein Hack*)
1.77 + (Celem.merge_rls "is_ratequation_in" calculate_Rational
1.78 + (Celem.append_rls "is_ratequation_in"
1.79 Poly_erls
1.80 - [(*Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),*)
1.81 - Calc ("RatEq.is'_ratequation'_in",
1.82 + [(*Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),*)
1.83 + Celem.Calc ("RatEq.is'_ratequation'_in",
1.84 eval_is_ratequation_in "")
1.85 ]))
1.86 - [Thm ("and_commute",TermC.num_str @{thm and_commute}), (*WN: ein Hack*)
1.87 - Thm ("or_commute",TermC.num_str @{thm or_commute}) (*WN: ein Hack*)
1.88 + [Celem.Thm ("and_commute",TermC.num_str @{thm and_commute}), (*WN: ein Hack*)
1.89 + Celem.Thm ("or_commute",TermC.num_str @{thm or_commute}) (*WN: ein Hack*)
1.90 ];
1.91
1.92 val RatEq_eliminate = prep_rls'(
1.93 - Rls {id = "RatEq_eliminate", preconds = [],
1.94 - rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls,
1.95 + Celem.Rls {id = "RatEq_eliminate", preconds = [],
1.96 + rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Celem.Erls,
1.97 calc = [], errpatts = [],
1.98 rules = [
1.99 - Thm("rat_mult_denominator_both",TermC.num_str @{thm rat_mult_denominator_both}),
1.100 + Celem.Thm("rat_mult_denominator_both",TermC.num_str @{thm rat_mult_denominator_both}),
1.101 (* a/b=c/d -> ad=cb *)
1.102 - Thm("rat_mult_denominator_left",TermC.num_str @{thm rat_mult_denominator_left}),
1.103 + Celem.Thm("rat_mult_denominator_left",TermC.num_str @{thm rat_mult_denominator_left}),
1.104 (* a =c/d -> ad=c *)
1.105 - Thm("rat_mult_denominator_right",TermC.num_str @{thm rat_mult_denominator_right})
1.106 + Celem.Thm("rat_mult_denominator_right",TermC.num_str @{thm rat_mult_denominator_right})
1.107 (* a/b=c -> a=cb *)
1.108 ],
1.109 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.110 - }:rls);
1.111 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.112 + });
1.113 *}
1.114 setup {* KEStore_Elems.add_rlss [("RatEq_eliminate",
1.115 (Context.theory_name @{theory}, RatEq_eliminate))] *}
1.116 ML {*
1.117
1.118 val RatEq_simplify = prep_rls'(
1.119 - Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
1.120 - erls = rateq_erls, srls = Erls, calc = [], errpatts = [],
1.121 + Celem.Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
1.122 + erls = rateq_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.123 rules = [
1.124 - Thm("real_rat_mult_1",TermC.num_str @{thm real_rat_mult_1}),
1.125 + Celem.Thm("real_rat_mult_1",TermC.num_str @{thm real_rat_mult_1}),
1.126 (*a*(b/c) = (a*b)/c*)
1.127 - Thm("real_rat_mult_2",TermC.num_str @{thm real_rat_mult_2}),
1.128 + Celem.Thm("real_rat_mult_2",TermC.num_str @{thm real_rat_mult_2}),
1.129 (*(a/b)*(c/d) = (a*c)/(b*d)*)
1.130 - Thm("real_rat_mult_3",TermC.num_str @{thm real_rat_mult_3}),
1.131 + Celem.Thm("real_rat_mult_3",TermC.num_str @{thm real_rat_mult_3}),
1.132 (* (a/b)*c = (a*c)/b*)
1.133 - Thm("real_rat_pow",TermC.num_str @{thm real_rat_pow}),
1.134 + Celem.Thm("real_rat_pow",TermC.num_str @{thm real_rat_pow}),
1.135 (*(a/b)^^^2 = a^^^2/b^^^2*)
1.136 - Thm("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.137 + Celem.Thm("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.138 (* a - b = a + (-1) * b *)
1.139 - Thm("rat_double_rat_1",TermC.num_str @{thm rat_double_rat_1}),
1.140 + Celem.Thm("rat_double_rat_1",TermC.num_str @{thm rat_double_rat_1}),
1.141 (* (a / (c/d) = (a*d) / c) *)
1.142 - Thm("rat_double_rat_2",TermC.num_str @{thm rat_double_rat_2}),
1.143 + Celem.Thm("rat_double_rat_2",TermC.num_str @{thm rat_double_rat_2}),
1.144 (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
1.145 - Thm("rat_double_rat_3",TermC.num_str @{thm rat_double_rat_3})
1.146 + Celem.Thm("rat_double_rat_3",TermC.num_str @{thm rat_double_rat_3})
1.147 (* ((a/b) / c = a / (b*c) ) *)
1.148 ],
1.149 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.150 - }:rls);
1.151 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.152 + });
1.153 *}
1.154 setup {* KEStore_Elems.add_rlss [("RatEq_simplify",
1.155 (Context.theory_name @{theory}, RatEq_simplify))] *}
1.156 @@ -183,7 +183,7 @@
1.157 *)
1.158 *}
1.159 setup {* KEStore_Elems.add_pbts
1.160 - [(Specify.prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
1.161 + [(Specify.prep_pbt thy "pbl_equ_univ_rat" [] Celem.e_pblID
1.162 (["rational","univariate","equation"],
1.163 [("#Given", ["equality e_e","solveFor v_v"]),
1.164 ("#Where", ["(e_e::bool) is_ratequation_in (v_v::real)"]),
1.165 @@ -192,16 +192,16 @@
1.166
1.167 (*-------------------------methods-----------------------*)
1.168 setup {* KEStore_Elems.add_mets
1.169 - [Specify.prep_met thy "met_rateq" [] e_metID
1.170 + [Specify.prep_met thy "met_rateq" [] Celem.e_metID
1.171 (["RatEq"], [],
1.172 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.173 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.174 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"),
1.175 - Specify.prep_met thy "met_rat_eq" [] e_metID
1.176 + Specify.prep_met thy "met_rat_eq" [] Celem.e_metID
1.177 (["RatEq", "solve_rat_equation"],
1.178 [("#Given" ,["equality e_e","solveFor v_v"]),
1.179 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
1.180 ("#Find" ,["solutions v_v'i'"])],
1.181 - {rew_ord'="termlessI", rls'=rateq_erls, srls=e_rls, prls=RatEq_prls, calc=[],
1.182 + {rew_ord'="termlessI", rls'=rateq_erls, srls=Celem.e_rls, prls=RatEq_prls, calc=[],
1.183 crls=RatEq_crls, errpats = [], nrls = norm_Rational},
1.184 "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
1.185 "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^