1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Aug 09 14:20:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Aug 10 09:43:07 2021 +0200
1.3 @@ -176,22 +176,21 @@
1.4 subsection \<open>rule-sets\<close>
1.5 ML \<open>
1.6 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
1.7 - Rule_Set.append_rules "RootEq_prls" Rule_Set.empty
1.8 - [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.9 - \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
1.10 - \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
1.11 - \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
1.12 - \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
1.13 - \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
1.14 - \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in ""),
1.15 - \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.16 - \<^rule_thm>\<open>not_true\<close>,
1.17 - \<^rule_thm>\<open>not_false\<close>,
1.18 - \<^rule_thm>\<open>and_true\<close>,
1.19 - \<^rule_thm>\<open>and_false\<close>,
1.20 - \<^rule_thm>\<open>or_true\<close>,
1.21 - \<^rule_thm>\<open>or_false\<close>
1.22 - ];
1.23 + Rule_Set.append_rules "RootEq_prls" Rule_Set.empty [
1.24 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.25 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
1.26 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
1.27 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
1.28 + \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
1.29 + \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
1.30 + \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in ""),
1.31 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.32 + \<^rule_thm>\<open>not_true\<close>,
1.33 + \<^rule_thm>\<open>not_false\<close>,
1.34 + \<^rule_thm>\<open>and_true\<close>,
1.35 + \<^rule_thm>\<open>and_false\<close>,
1.36 + \<^rule_thm>\<open>or_true\<close>,
1.37 + \<^rule_thm>\<open>or_false\<close>];
1.38
1.39 val RootEq_erls =
1.40 Rule_Set.append_rules "RootEq_erls" Root_erls
1.41 @@ -202,8 +201,8 @@
1.42 [\<^rule_thm>\<open>divide_divide_eq_left\<close>];
1.43
1.44 val rooteq_srls =
1.45 - Rule_Set.append_rules "rooteq_srls" Rule_Set.empty
1.46 - [\<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
1.47 + Rule_Set.append_rules "rooteq_srls" Rule_Set.empty [
1.48 + \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
1.49 \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in""),
1.50 \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in "")];
1.51 \<close>
1.52 @@ -211,206 +210,128 @@
1.53
1.54 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
1.55 val sqrt_isolate = prep_rls'(
1.56 - Rule_Def.Repeat {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
1.57 - erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.58 - rules = [
1.59 - \<^rule_thm>\<open>sqrt_square_1\<close>,
1.60 - (* (sqrt a) \<up> 2 -> a *)
1.61 - \<^rule_thm>\<open>sqrt_square_2\<close>,
1.62 - (* sqrt (a \<up> 2) -> a *)
1.63 - \<^rule_thm>\<open>sqrt_times_root_1\<close>,
1.64 - (* sqrt a sqrt b -> sqrt(ab) *)
1.65 - \<^rule_thm>\<open>sqrt_times_root_2\<close>,
1.66 - (* a sqrt b sqrt c -> a sqrt(bc) *)
1.67 - \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>,
1.68 - (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
1.69 - (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
1.70 - \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>,
1.71 - (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
1.72 - (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
1.73 - \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>,
1.74 - (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
1.75 - (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
1.76 - \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>,
1.77 - (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
1.78 - (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
1.79 - \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
1.80 - (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
1.81 - \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
1.82 - (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
1.83 - \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
1.84 - (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
1.85 - \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
1.86 - (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
1.87 - \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
1.88 - (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
1.89 - \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
1.90 - (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
1.91 - (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
1.92 - (* b*sqrt(x) = d sqrt(x) d/b *)
1.93 - \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
1.94 - (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
1.95 - \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
1.96 - (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
1.97 - \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
1.98 - (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
1.99 - \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
1.100 - (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
1.101 - \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
1.102 - (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
1.103 - \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
1.104 - (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
1.105 - (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
1.106 - (* a=e*sqrt(x) -> a/e = sqrt(x) *)
1.107 - \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
1.108 - (* sqrt(x)=b -> x=b^2 *)
1.109 - \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
1.110 - (* c*sqrt(x)=b -> c^2*x=b^2 *)
1.111 - \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
1.112 - (* c/sqrt(x)=b -> c^2/x=b^2 *)
1.113 - \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
1.114 - (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
1.115 - \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
1.116 - (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
1.117 - \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>,
1.118 - (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
1.119 - \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
1.120 - (* a=sqrt(x) ->a^2=x *)
1.121 - \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
1.122 - (* a=c*sqrt(x) ->a^2=c^2*x *)
1.123 - \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
1.124 - (* a=c/sqrt(x) ->a^2=c^2/x *)
1.125 - \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
1.126 - (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
1.127 - \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
1.128 - (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
1.129 - \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
1.130 - (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
1.131 - ],scr = Rule.Empty_Prog
1.132 - });
1.133 + Rule_Def.Repeat {
1.134 + id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
1.135 + erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.136 + rules = [
1.137 + \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)
1.138 + \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)
1.139 + \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)
1.140 + \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)
1.141 + \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>, (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
1.142 + (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
1.143 + \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>, (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
1.144 + (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
1.145 + \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>, (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
1.146 + (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
1.147 + \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>, (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
1.148 + (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
1.149 + \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>, (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
1.150 + \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
1.151 + \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
1.152 + \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
1.153 + \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
1.154 + \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
1.155 + (*
1.156 + \<^rule_thm>\<open>sqrt_isolate_l_div\<close>, (* b*sqrt(x) = d sqrt(x) d/b *)*)
1.157 + \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>, (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
1.158 + \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>, (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
1.159 + \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>, (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
1.160 + \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>, (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
1.161 + \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>, (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
1.162 + \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>, (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
1.163 + (*
1.164 + \<^rule_thm>\<open>sqrt_isolate_r_div\<close>, (* a=e*sqrt(x) -> a/e = sqrt(x) *)*)
1.165 + \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>, (* sqrt(x)=b -> x=b^2 *)
1.166 + \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>, (* c*sqrt(x)=b -> c^2*x=b^2 *)
1.167 + \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>, (* c/sqrt(x)=b -> c^2/x=b^2 *)
1.168 + \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>, (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
1.169 + \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>, (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
1.170 + \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>, (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
1.171 + \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>, (* a=sqrt(x) ->a^2=x *)
1.172 + \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>, (* a=c*sqrt(x) ->a^2=c^2*x *)
1.173 + \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>, (* a=c/sqrt(x) ->a^2=c^2/x *)
1.174 + \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>, (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
1.175 + \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>, (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
1.176 + \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>], (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
1.177 + scr = Rule.Empty_Prog});
1.178
1.179 \<close> ML \<open>
1.180 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
1.181 - val l_sqrt_isolate = prep_rls'(
1.182 - Rule_Def.Repeat {id = "l_sqrt_isolate", preconds = [],
1.183 - rew_ord = ("termlessI",termlessI),
1.184 - erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.185 - rules = [
1.186 - \<^rule_thm>\<open>sqrt_square_1\<close>,
1.187 - (* (sqrt a) \<up> 2 -> a *)
1.188 - \<^rule_thm>\<open>sqrt_square_2\<close>,
1.189 - (* sqrt (a \<up> 2) -> a *)
1.190 - \<^rule_thm>\<open>sqrt_times_root_1\<close>,
1.191 - (* sqrt a sqrt b -> sqrt(ab) *)
1.192 - \<^rule_thm>\<open>sqrt_times_root_2\<close>,
1.193 - (* a sqrt b sqrt c -> a sqrt(bc) *)
1.194 - \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
1.195 - (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
1.196 - \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
1.197 - (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
1.198 - \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
1.199 - (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
1.200 - \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
1.201 - (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
1.202 - \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
1.203 - (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
1.204 - \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
1.205 - (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
1.206 - (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
1.207 - (* b*sqrt(x) = d sqrt(x) d/b *)
1.208 - \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
1.209 - (* sqrt(x)=b -> x=b^2 *)
1.210 - \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
1.211 - (* a*sqrt(x)=b -> a^2*x=b^2*)
1.212 - \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
1.213 - (* c/sqrt(x)=b -> c^2/x=b^2 *)
1.214 - \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>,
1.215 - (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
1.216 - \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>,
1.217 - (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
1.218 - \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>
1.219 - (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
1.220 - ],
1.221 - scr = Rule.Empty_Prog
1.222 - });
1.223 +val l_sqrt_isolate = prep_rls'(
1.224 + Rule_Def.Repeat {
1.225 + id = "l_sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
1.226 + erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.227 + rules = [
1.228 + \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)
1.229 + \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)
1.230 + \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)
1.231 + \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)
1.232 + \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>, (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
1.233 + \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
1.234 + \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
1.235 + \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
1.236 + \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
1.237 + \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
1.238 + (*
1.239 + \<^rule_thm>\<open>sqrt_isolate_l_div\<close>, (* b*sqrt(x) = d sqrt(x) d/b *)*)
1.240 + \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>, (* sqrt(x)=b -> x=b^2 *)
1.241 + \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>, (* a*sqrt(x)=b -> a^2*x=b^2*)
1.242 + \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>, (* c/sqrt(x)=b -> c^2/x=b^2 *)
1.243 + \<^rule_thm>\<open>sqrt_square_equation_left_4\<close>, (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
1.244 + \<^rule_thm>\<open>sqrt_square_equation_left_5\<close>, (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
1.245 + \<^rule_thm>\<open>sqrt_square_equation_left_6\<close>], (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
1.246 + scr = Rule.Empty_Prog});
1.247
1.248 \<close> ML \<open>
1.249 (* -- right 28.8.02--*)
1.250 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
1.251 - val r_sqrt_isolate = prep_rls'(
1.252 - Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [],
1.253 - rew_ord = ("termlessI",termlessI),
1.254 - erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.255 - rules = [
1.256 - \<^rule_thm>\<open>sqrt_square_1\<close>,
1.257 - (* (sqrt a) \<up> 2 -> a *)
1.258 - \<^rule_thm>\<open>sqrt_square_2\<close>,
1.259 - (* sqrt (a \<up> 2) -> a *)
1.260 - \<^rule_thm>\<open>sqrt_times_root_1\<close>,
1.261 - (* sqrt a sqrt b -> sqrt(ab) *)
1.262 - \<^rule_thm>\<open>sqrt_times_root_2\<close>,
1.263 - (* a sqrt b sqrt c -> a sqrt(bc) *)
1.264 - \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
1.265 - (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
1.266 - \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
1.267 - (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
1.268 - \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
1.269 - (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
1.270 - \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
1.271 - (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
1.272 - \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
1.273 - (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
1.274 - \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
1.275 - (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
1.276 - (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
1.277 - (* a=e*sqrt(x) -> a/e = sqrt(x) *)
1.278 - \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>,
1.279 - (* a=sqrt(x) ->a^2=x *)
1.280 - \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>,
1.281 - (* a=c*sqrt(x) ->a^2=c^2*x *)
1.282 - \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>,
1.283 - (* a=c/sqrt(x) ->a^2=c^2/x *)
1.284 - \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>,
1.285 - (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
1.286 - \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>,
1.287 - (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
1.288 - \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>
1.289 - (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
1.290 - ],
1.291 - scr = Rule.Empty_Prog
1.292 - });
1.293 +val r_sqrt_isolate = prep_rls'(
1.294 + Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
1.295 + erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.296 + rules = [
1.297 + \<^rule_thm>\<open>sqrt_square_1\<close>, (* (sqrt a) \<up> 2 -> a *)
1.298 + \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) -> a *)
1.299 + \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt a sqrt b -> sqrt(ab) *)
1.300 + \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a sqrt b sqrt c -> a sqrt(bc) *)
1.301 + \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>, (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
1.302 + \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>, (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
1.303 + \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>, (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
1.304 + \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>, (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
1.305 + \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>, (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
1.306 + \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>, (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
1.307 + (*
1.308 + \<^rule_thm>\<open>sqrt_isolate_r_div\<close>, (* a=e*sqrt(x) -> a/e = sqrt(x) *)*)
1.309 + \<^rule_thm>\<open>sqrt_square_equation_right_1\<close>, (* a=sqrt(x) ->a^2=x *)
1.310 + \<^rule_thm>\<open>sqrt_square_equation_right_2\<close>, (* a=c*sqrt(x) ->a^2=c^2*x *)
1.311 + \<^rule_thm>\<open>sqrt_square_equation_right_3\<close>, (* a=c/sqrt(x) ->a^2=c^2/x *)
1.312 + \<^rule_thm>\<open>sqrt_square_equation_right_4\<close>, (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
1.313 + \<^rule_thm>\<open>sqrt_square_equation_right_5\<close>, (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
1.314 + \<^rule_thm>\<open>sqrt_square_equation_right_6\<close>], (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
1.315 + scr = Rule.Empty_Prog});
1.316
1.317 \<close> ML \<open>
1.318 val rooteq_simplify = prep_rls'(
1.319 - Rule_Def.Repeat {id = "rooteq_simplify",
1.320 - preconds = [], rew_ord = ("termlessI",termlessI),
1.321 - erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.322 - (*asm_thm = [("sqrt_square_1", "")],*)
1.323 - rules = [\<^rule_thm>\<open>real_assoc_1\<close>,
1.324 - (* a+(b+c) = a+b+c *)
1.325 - \<^rule_thm>\<open>real_assoc_2\<close>,
1.326 - (* a*(b*c) = a*b*c *)
1.327 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.328 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
1.329 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.330 - \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.331 - \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
1.332 - \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
1.333 - \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
1.334 - \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
1.335 - \<^rule_thm>\<open>realpow_mul\<close>,
1.336 - (* (a * b)^n = a^n * b^n*)
1.337 - \<^rule_thm>\<open>sqrt_times_root_1\<close>,
1.338 - (* sqrt b * sqrt c = sqrt(b*c) *)
1.339 - \<^rule_thm>\<open>sqrt_times_root_2\<close>,
1.340 - (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
1.341 - \<^rule_thm>\<open>sqrt_square_2\<close>,
1.342 - (* sqrt (a \<up> 2) = a *)
1.343 - \<^rule_thm>\<open>sqrt_square_1\<close>
1.344 - (* sqrt a \<up> 2 = a *)
1.345 - ],
1.346 - scr = Rule.Empty_Prog
1.347 - });
1.348 + Rule_Def.Repeat {
1.349 + id = "rooteq_simplify", preconds = [], rew_ord = ("termlessI",termlessI),
1.350 + erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.351 + rules = [
1.352 + \<^rule_thm>\<open>real_assoc_1\<close>, (* a+(b+c) = a+b+c *)
1.353 + \<^rule_thm>\<open>real_assoc_2\<close>, (* a*(b*c) = a*b*c *)
1.354 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.355 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
1.356 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.357 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.358 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
1.359 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
1.360 + \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
1.361 + \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
1.362 + \<^rule_thm>\<open>realpow_mul\<close>, (* (a * b)^n = a^n * b^n*)
1.363 + \<^rule_thm>\<open>sqrt_times_root_1\<close>, (* sqrt b * sqrt c = sqrt(b*c) *)
1.364 + \<^rule_thm>\<open>sqrt_times_root_2\<close>, (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
1.365 + \<^rule_thm>\<open>sqrt_square_2\<close>, (* sqrt (a \<up> 2) = a *)
1.366 + \<^rule_thm>\<open>sqrt_square_1\<close>], (* sqrt a \<up> 2 = a *)
1.367 + scr = Rule.Empty_Prog});
1.368 \<close>
1.369 rule_set_knowledge
1.370 RootEq_erls = RootEq_erls and