neuper@37906
|
1 |
(*.(c) by Richard Lang, 2003 .*)
|
neuper@37906
|
2 |
(* defines equation and univariate-equation
|
neuper@37906
|
3 |
created by: rlang
|
neuper@37906
|
4 |
date: 02.09
|
neuper@37906
|
5 |
changed by: rlang
|
neuper@37906
|
6 |
last change by: rlang
|
neuper@37906
|
7 |
date: 02.11.29
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37947
|
10 |
(* use_thy_only"Knowledge/Equation";
|
neuper@37947
|
11 |
use_thy"Knowledge/Equation";
|
neuper@37947
|
12 |
use"Knowledge/Equation.ML";
|
neuper@37906
|
13 |
use"Equation.ML";
|
neuper@37906
|
14 |
*)
|
neuper@37906
|
15 |
|
neuper@37906
|
16 |
theory' := overwritel (!theory', [("Equation.thy",Equation.thy)]);
|
neuper@37906
|
17 |
|
neuper@37906
|
18 |
val univariate_equation_prls =
|
neuper@37906
|
19 |
append_rls "univariate_equation_prls" e_rls
|
neuper@37906
|
20 |
[Calc ("Tools.matches",eval_matches "")];
|
neuper@37906
|
21 |
ruleset' :=
|
neuper@37906
|
22 |
overwritelthy thy (!ruleset',
|
neuper@37906
|
23 |
[("univariate_equation_prls",
|
neuper@37906
|
24 |
prep_rls univariate_equation_prls)]);
|
neuper@37906
|
25 |
|
neuper@37906
|
26 |
|
neuper@37906
|
27 |
store_pbt
|
neuper@37906
|
28 |
(prep_pbt Equation.thy "pbl_equ" [] e_pblID
|
neuper@37906
|
29 |
(["equation"],
|
neuper@37906
|
30 |
[("#Given" ,["equality e_","solveFor v_"]),
|
neuper@37906
|
31 |
("#Where" ,["matches (?a = ?b) e_"]),
|
neuper@37906
|
32 |
("#Find" ,["solutions v_i_"])
|
neuper@37906
|
33 |
],
|
neuper@37906
|
34 |
append_rls "equation_prls" e_rls
|
neuper@37906
|
35 |
[Calc ("Tools.matches",eval_matches "")],
|
neuper@37926
|
36 |
SOME "solve (e_::bool, v_)",
|
neuper@37906
|
37 |
[]));
|
neuper@37906
|
38 |
|
neuper@37906
|
39 |
store_pbt
|
neuper@37906
|
40 |
(prep_pbt Equation.thy "pbl_equ_univ" [] e_pblID
|
neuper@37906
|
41 |
(["univariate","equation"],
|
neuper@37906
|
42 |
[("#Given" ,["equality e_","solveFor v_"]),
|
neuper@37906
|
43 |
("#Where" ,["matches (?a = ?b) e_"]),
|
neuper@37906
|
44 |
("#Find" ,["solutions v_i_"])
|
neuper@37906
|
45 |
],
|
neuper@37926
|
46 |
univariate_equation_prls,SOME "solve (e_::bool, v_)",[]));
|
neuper@37906
|
47 |
|
neuper@37906
|
48 |
|
neuper@37906
|
49 |
(*.function for handling the cas-input "solve (x+1=2, x)":
|
neuper@37906
|
50 |
make a model which is already in ptree-internal format.*)
|
neuper@37906
|
51 |
(* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
|
neuper@37906
|
52 |
val (h,argl) = strip_comb ((term_of o the o (parse thy))
|
neuper@37906
|
53 |
"solveTest (x+1=2, x)");
|
neuper@37906
|
54 |
*)
|
neuper@37906
|
55 |
fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
|
neuper@37906
|
56 |
[((term_of o the o (parse thy)) "equality", [eq]),
|
neuper@37906
|
57 |
((term_of o the o (parse thy)) "solveFor", [bdv]),
|
neuper@37906
|
58 |
((term_of o the o (parse thy)) "solutions",
|
neuper@37906
|
59 |
[(term_of o the o (parse thy)) "L"])
|
neuper@37906
|
60 |
]
|
neuper@37906
|
61 |
| argl2dtss _ = raise error "Equation.ML: wrong argument for argl2dtss";
|
neuper@37906
|
62 |
|
neuper@37906
|
63 |
castab :=
|
neuper@37906
|
64 |
overwritel (!castab,
|
neuper@37906
|
65 |
[((term_of o the o (parse thy)) "solveTest",
|
neuper@37906
|
66 |
(("Test.thy", ["univariate","equation","test"], ["no_met"]),
|
neuper@37906
|
67 |
argl2dtss)),
|
neuper@37906
|
68 |
((term_of o the o (parse thy)) "solve",
|
neuper@37906
|
69 |
(("Isac.thy", ["univariate","equation"], ["no_met"]),
|
neuper@37906
|
70 |
argl2dtss))
|
neuper@37906
|
71 |
]);
|
neuper@37906
|
72 |
|
neuper@37906
|
73 |
|
neuper@37906
|
74 |
|
neuper@37906
|
75 |
store_met
|
neuper@37906
|
76 |
(prep_met Equation.thy "met_equ" [] e_metID
|
neuper@37906
|
77 |
(["Equation"],
|
neuper@37906
|
78 |
[],
|
neuper@37906
|
79 |
{rew_ord'="tless_true", rls'=Erls, calc = [],
|
neuper@37906
|
80 |
srls = e_rls,
|
neuper@37906
|
81 |
prls=e_rls,
|
neuper@37906
|
82 |
crls = Atools_erls, nrls = e_rls},
|
neuper@37906
|
83 |
"empty_script"
|
neuper@37906
|
84 |
));
|
neuper@37906
|
85 |
|