76 Calc ("Tools.rhs" ,eval_rhs ""), |
76 Calc ("Tools.rhs" ,eval_rhs ""), |
77 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""), |
77 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""), |
78 Calc ("RootRatEq.is'_rootRatAddTerm'_in", |
78 Calc ("RootRatEq.is'_rootRatAddTerm'_in", |
79 eval_is_rootRatAddTerm_in ""), |
79 eval_is_rootRatAddTerm_in ""), |
80 Calc ("op =",eval_equal "#equal_"), |
80 Calc ("op =",eval_equal "#equal_"), |
81 Thm ("not_true",num_str @{not_true), |
81 Thm ("not_true",num_str @{thm not_true}), |
82 Thm ("not_false",num_str @{not_false), |
82 Thm ("not_false",num_str @{thm not_false}), |
83 Thm ("and_true",num_str @{and_true), |
83 Thm ("and_true",num_str @{thm and_true}), |
84 Thm ("and_false",num_str @{and_false), |
84 Thm ("and_false",num_str @{thm and_false}), |
85 Thm ("or_true",num_str @{or_true), |
85 Thm ("or_true",num_str @{thm or_true}), |
86 Thm ("or_false",num_str @{or_false) |
86 Thm ("or_false",num_str @{thm or_false}) |
87 ]; |
87 ]; |
88 |
88 |
89 val RooRatEq_erls = |
89 val RooRatEq_erls = |
90 merge_rls "RooRatEq_erls" rootrat_erls |
90 merge_rls "RooRatEq_erls" rootrat_erls |
91 (merge_rls "" RootEq_erls |
91 (merge_rls "" RootEq_erls |
106 (* Solves a rootrat Equation *) |
106 (* Solves a rootrat Equation *) |
107 val rootrat_solve = prep_rls( |
107 val rootrat_solve = prep_rls( |
108 Rls {id = "rootrat_solve", preconds = [], |
108 Rls {id = "rootrat_solve", preconds = [], |
109 rew_ord = ("termlessI",termlessI), |
109 rew_ord = ("termlessI",termlessI), |
110 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
110 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
111 rules = [Thm("rootrat_equation_left_1", num_str @{rootrat_equation_left_1), |
111 rules = [Thm("rootrat_equation_left_1", num_str @{thm }rootrat_equation_left_1), |
112 (* [|c is_rootTerm_in bdv|] ==> |
112 (* [|c is_rootTerm_in bdv|] ==> |
113 ( (a + b/c = d) = ( b = (d - a) * c )) *) |
113 ( (a + b/c = d) = ( b = (d - a) * c )) *) |
114 Thm("rootrat_equation_left_2",num_str @{rootrat_equation_left_2), |
114 Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}), |
115 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *) |
115 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *) |
116 Thm("rootrat_equation_right_1",num_str @{rootrat_equation_right_1), |
116 Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}), |
117 (* [|f is_rootTerm_in bdv|] ==> |
117 (* [|f is_rootTerm_in bdv|] ==> |
118 ( (a = d + e/f) = ( (a - d) * f = e )) *) |
118 ( (a = d + e/f) = ( (a - d) * f = e )) *) |
119 Thm("rootrat_equation_right_2",num_str @{rootrat_equation_right_2) |
119 Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2}) |
120 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*) |
120 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*) |
121 ], |
121 ], |
122 scr = Script ((term_of o the o (parse thy)) "empty_script") |
122 scr = Script ((term_of o the o (parse thy)) "empty_script") |
123 }:rls); |
123 }:rls); |
124 ruleset' := overwritelthy @{theory} (!ruleset', |
124 ruleset' := overwritelthy @{theory} (!ruleset', |