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