154 fun is_normSqrtTerm_in t v = |
154 fun is_normSqrtTerm_in t v = |
155 let |
155 let |
156 fun coeff_in c v = member op = (vars c) v; |
156 fun coeff_in c v = member op = (vars c) v; |
157 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:") |
157 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:") |
158 (* at the moment there is no term like this, but ....*) |
158 (* at the moment there is no term like this, but ....*) |
159 | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
159 | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
160 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
160 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
161 | isnorm (Const ("op -",_) $ _ $ _) v = false |
161 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false |
162 | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse |
162 | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse |
163 (is_sqrtTerm_in t2 v) |
163 (is_sqrtTerm_in t2 v) |
164 | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v |
164 | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v |
165 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v |
165 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v |
166 | isnorm _ _ = false; |
166 | isnorm _ _ = false; |
167 in |
167 in |
443 (*asm_thm = [("sqrt_square_1","")],*) |
443 (*asm_thm = [("sqrt_square_1","")],*) |
444 rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}), |
444 rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}), |
445 (* a+(b+c) = a+b+c *) |
445 (* a+(b+c) = a+b+c *) |
446 Thm ("real_assoc_2",num_str @{thm real_assoc_2}), |
446 Thm ("real_assoc_2",num_str @{thm real_assoc_2}), |
447 (* a*(b*c) = a*b*c *) |
447 (* a*(b*c) = a*b*c *) |
448 Calc ("op +",eval_binop "#add_"), |
448 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
449 Calc ("op -",eval_binop "#sub_"), |
449 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
450 Calc ("op *",eval_binop "#mult_"), |
450 Calc ("op *",eval_binop "#mult_"), |
451 Calc ("HOL.divide", eval_cancel "#divide_e"), |
451 Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), |
452 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
452 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
453 Calc ("Atools.pow" ,eval_binop "#power_"), |
453 Calc ("Atools.pow" ,eval_binop "#power_"), |
454 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}), |
454 Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}), |
455 Thm("real_minus_binom_pow2",num_str @{thm real_minus_binom_pow2}), |
455 Thm("real_minus_binom_pow2",num_str @{thm real_minus_binom_pow2}), |
456 Thm("realpow_mul",num_str @{thm realpow_mul}), |
456 Thm("realpow_mul",num_str @{thm realpow_mul}), |