1 (* equations and functions; functions NOT as lambda-terms
2 author: Walther Neuper 2005, 2006
3 (c) due to copyright terms
6 theory Equation imports Base_Tools begin
8 text \<open>univariate equations over terms :
9 In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing
10 the Lucas-Interpreter's Subproblem mechanism.
11 This prototype suffers from the drop-out of Matthias Goldgruber for a year,
12 who had started to work on simplification in parallel. So this implementation
13 replaced simplifiers by many specific theorems for specific terms in specific
14 phases of equation solving; these specific solutions wait for generalisation
15 in future improvements of ISAC's equation solver.
20 (*descriptions in the related problems TODOshift here from Descriptions.thy*)
21 substitution :: "bool => una"
24 solve :: "[bool * real] => bool list"(*solveFor ::"real => una"; eg.solve (x+1=2, x)*)
25 solveTest :: "[bool * 'a] => bool list" (* for test collection *)
27 text \<open>defines equation and univariate-equation
33 (c) by Richard Lang, 2003\<close>
36 val univariate_equation_prls =
37 Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty
38 [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
40 rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>
42 problem pbl_equ : "equation" =
43 \<open>Rule_Set.append_rules "equation_prls" Rule_Set.empty
44 [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")]\<close>
45 CAS: "solve (e_e::bool, v_v)"
46 Given: "equality e_e" "solveFor v_v"
47 Where: "matches (?a = ?b) e_e"
48 Find: "solutions v_v'i'"
50 problem pbl_equ_univ : "univariate/equation" =
51 \<open>univariate_equation_prls\<close>
52 CAS: "solve (e_e::bool, v_v)"
53 Given: "equality e_e" "solveFor v_v"
54 Where: "matches (?a = ?b) e_e"
55 Find: "solutions v_v'i'"
58 (* function for handling the cas-input "solve (x+1=2, x)":
59 make a model which is already in ctree-internal format *)
60 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ eq $ bdv] =
61 [(ParseC.term_opt \<^context> "equality" |> the, [eq]),
62 (ParseC.term_opt \<^context> "solveFor" |> the, [bdv]),
63 (ParseC.term_opt \<^context> "solutions" |> the,
64 [ParseC.term_opt\<^context> "L" |> the])
66 | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss";
68 cas solveTest = \<open>argl2dtss\<close>
70 Problem_Ref: "univariate/equation/test"
71 cas solve = \<open>argl2dtss\<close>
72 Problem_Ref: "univariate/equation"
74 method met_equ : "Equation" =
75 \<open>{rew_ord = "tless_true", rls' = Rule_Set.Empty, calc = [], prog_rls = Rule_Set.empty,
76 where_rls=Rule_Set.empty, errpats = [], rew_rls = Rule_Set.empty}\<close>