Isar command 'method' as combination of KEStore_Elems.add_mets + MethodC.prep_import, without change of semantics;
1 (* collecting all knowledge for Root and Rational Equations
7 (c) by Richard Lang, 2003
10 theory RootRatEq imports LinEq RootEq RatEq RootRat begin
12 text \<open>univariate equations over rational terms containing real square roots:
13 In 2003 this type has been developed as part of ISAC's equation solver
14 by Richard Lang in 2003.
15 The migration Isabelle2002 --> 2011 dropped this type of equation, see RootEq.thy.
18 subsection \<open>consts definition for predicates\<close>
20 is_rootRatAddTerm_in :: "[real, real] => bool" ("_ is'_rootRatAddTerm'_in _") (*RL*)
22 subsection \<open>theorems not yet adopted from Isabelle\<close>
24 (* eliminate ratRootTerm *)
25 rootrat_equation_left_1:
26 "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" and
27 rootrat_equation_left_2:
28 "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" and
29 rootrat_equation_right_2:
30 "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" and
31 rootrat_equation_right_1:
32 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
34 subsection \<open>predicates\<close>
36 (* true if denominator contains (sq)root in + or - term
37 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
38 if false then (term)^2 contains no (sq)root *)
39 fun is_rootRatAddTerm_in t v =
41 fun rootadd (Const ("Groups.plus_class.plus", _) $ t2 $ t3) v =
42 is_rootTerm_in t2 v orelse is_rootTerm_in t3 v
43 | rootadd (Const ("Groups.minus_class.minus",_) $ t2 $ t3) v =
44 is_rootTerm_in t2 v orelse is_rootTerm_in t3 v
45 | rootadd _ _ = false;
46 fun findrootrat (t as (_ $ _ $ _ $ _)) _ = raise TERM ("is_rootRatAddTerm_in", [t])
47 (* at the moment there is no term like this, but ....*)
48 | findrootrat (Const ("Rings.divide_class.divide",_) $ _ $ t3) v =
49 if (is_rootTerm_in t3 v) then rootadd t3 v else false
50 | findrootrat (_ $ t1 $ t2) v =
51 findrootrat t1 v orelse findrootrat t2 v
52 | findrootrat (_ $ t1) v = findrootrat t1 v
53 | findrootrat _ _ = false;
58 fun eval_is_rootRatAddTerm_in _ _ (p as (Const ("RootRatEq.is_rootRatAddTerm_in",_) $ t $ v)) _ =
59 if is_rootRatAddTerm_in t v
60 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
61 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
62 | eval_is_rootRatAddTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
64 setup \<open>KEStore_Elems.add_calcs
65 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))]\<close>
67 subsection \<open>rule-sets\<close>
70 Rule_Set.append_rules "RootRatEq_prls" Rule_Set.empty
71 [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
72 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
73 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
74 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
75 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
76 \<^rule_eval>\<open>is_rootRatAddTerm_in\<close> (eval_is_rootRatAddTerm_in ""),
77 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
78 \<^rule_thm>\<open>not_true\<close>,
79 \<^rule_thm>\<open>not_false\<close>,
80 \<^rule_thm>\<open>and_true\<close>,
81 \<^rule_thm>\<open>and_false\<close>,
82 \<^rule_thm>\<open>or_true\<close>,
83 \<^rule_thm>\<open>or_false\<close>];
86 Rule_Set.merge "RooRatEq_erls" rootrat_erls
87 (Rule_Set.merge "" RootEq_erls
88 (Rule_Set.merge "" rateq_erls
89 (Rule_Set.append_rules "" Rule_Set.empty
93 Rule_Set.merge "RootRatEq_crls" rootrat_erls
94 (Rule_Set.merge "" RootEq_erls
95 (Rule_Set.merge "" rateq_erls
96 (Rule_Set.append_rules "" Rule_Set.empty
99 (* Solves a rootrat Equation *)
100 val rootrat_solve = prep_rls'(
101 Rule_Def.Repeat {id = "rootrat_solve", preconds = [],
102 rew_ord = ("termlessI",termlessI),
103 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
105 [\<^rule_thm>\<open>rootrat_equation_left_1\<close>,
106 (* [|c is_rootTerm_in bdv|] ==>
107 ( (a + b/c = d) = ( b = (d - a) * c )) *)
108 \<^rule_thm>\<open>rootrat_equation_left_2\<close>,
109 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
110 \<^rule_thm>\<open>rootrat_equation_right_1\<close>,
111 (* [|f is_rootTerm_in bdv|] ==>
112 ( (a = d + e/f) = ( (a - d) * f = e )) *)
113 \<^rule_thm>\<open>rootrat_equation_right_2\<close>
114 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
115 ], scr = Rule.Empty_Prog});
118 RooRatEq_erls = RooRatEq_erls and
119 rootrat_solve = rootrat_solve
121 subsection \<open>problems\<close>
123 setup \<open>KEStore_Elems.add_pbts
124 [(Problem.prep_input @{theory} "pbl_equ_univ_root_sq_rat" [] Problem.id_empty
125 (["rat", "sq", "rootX", "univariate", "equation"],
126 [("#Given" ,["equality e_e", "solveFor v_v"]),
127 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
128 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
129 ("#Find" ,["solutions v_v'i'"])],
130 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq", "elim_rootrat_equation"]]))]\<close>
132 subsection \<open>methods\<close>
134 setup \<open>KEStore_Elems.add_mets
135 [MethodC.prep_input @{theory LinEq} "met_rootrateq" [] MethodC.id_empty
137 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
138 crls=Atools_erls, errpats = [], nrls = norm_Rational}, @{thm refl})]
140 (*-- left 20.10.02 --*)
141 partial_function (tailrec) solve_rootrat_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
143 "solve_rootrat_equ e_e v_v =
146 (Try (Rewrite_Set ''expand_rootbinoms'')) #>
147 (Try (Rewrite_Set ''rooteq_simplify'')) #>
148 (Try (Rewrite_Set ''make_rooteq'')) #>
149 (Try (Rewrite_Set ''rooteq_simplify'')) #>
150 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e
151 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
153 method met_rootrateq_elim : "RootRatEq/elim_rootrat_equation" =
154 \<open>{rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule_Set.empty, prls=RootRatEq_prls, calc=[],
155 crls=RootRatEq_crls, errpats = [], nrls = norm_Rational}\<close>
156 Program: solve_rootrat_equ.simps
157 Given: "equality e_e" "solveFor v_v"
158 Where: "( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) |
159 ( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"
160 Find: "solutions v_v'i'"