1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 22 13:15:52 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 22 14:34:06 2019 +0200
1.3 @@ -12,59 +12,6 @@
1.4
1.5 theory PolyEq imports LinEq RootRatEq begin
1.6
1.7 -consts
1.8 -
1.9 -(*---------scripts--------------------------*)
1.10 - Complete'_square
1.11 - :: "[bool,real,
1.12 - bool list] => bool list"
1.13 - ("((Script Complete'_square (_ _ =))// (_))" 9)
1.14 - (*----- poly ----- *)
1.15 - Normalize'_poly
1.16 - :: "[bool,real,
1.17 - bool list] => bool list"
1.18 - ("((Script Normalize'_poly (_ _=))// (_))" 9)
1.19 - Solve'_d0'_polyeq'_equation
1.20 - :: "[bool,real,
1.21 - bool list] => bool list"
1.22 - ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// (_))" 9)
1.23 - Solve'_d1'_polyeq'_equation
1.24 - :: "[bool,real,
1.25 - bool list] => bool list"
1.26 - ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// (_))" 9)
1.27 - Solve'_d2'_polyeq'_equation
1.28 - :: "[bool,real,
1.29 - bool list] => bool list"
1.30 - ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// (_))" 9)
1.31 - Solve'_d2'_polyeq'_sqonly'_equation
1.32 - :: "[bool,real,
1.33 - bool list] => bool list"
1.34 - ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// (_))" 9)
1.35 - Solve'_d2'_polyeq'_bdvonly'_equation
1.36 - :: "[bool,real,
1.37 - bool list] => bool list"
1.38 - ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// (_))" 9)
1.39 - Solve'_d2'_polyeq'_pq'_equation
1.40 - :: "[bool,real,
1.41 - bool list] => bool list"
1.42 - ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// (_))" 9)
1.43 - Solve'_d2'_polyeq'_abc'_equation
1.44 - :: "[bool,real,
1.45 - bool list] => bool list"
1.46 - ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// (_))" 9)
1.47 - Solve'_d3'_polyeq'_equation
1.48 - :: "[bool,real,
1.49 - bool list] => bool list"
1.50 - ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// (_))" 9)
1.51 - Solve'_d4'_polyeq'_equation
1.52 - :: "[bool,real,
1.53 - bool list] => bool list"
1.54 - ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// (_))" 9)
1.55 - Biquadrat'_poly
1.56 - :: "[bool,real,
1.57 - bool list] => bool list"
1.58 - ("((Script Biquadrat'_poly (_ _=))// (_))" 9)
1.59 -
1.60 (*-------------------- rules -------------------------------------------------*)
1.61 (* type real enforced by op "^^^" *)
1.62 axiomatization where
1.63 @@ -952,20 +899,6 @@
1.64 ("#Find", ["solutions v_v'i'"])],
1.65 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","complete_square"]]))]\<close>
1.66
1.67 -ML\<open>
1.68 -val scr =
1.69 - "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
1.70 - "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
1.71 - " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
1.72 - " (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@ " ^
1.73 - " (Try (Repeat (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.74 - " ''make_ratpoly_in'' False))) @@ " ^
1.75 - " (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e " ^
1.76 - " in (SubProblem (''PolyEq'',[''polynomial'',''univariate'',''equation''], [''no_met'']) " ^
1.77 - " [BOOL e_e, REAL v_v]))";
1.78 -TermC.parse thy scr;
1.79 -\<close>
1.80 -
1.81 text \<open>"-------------------------methods-----------------------"\<close>
1.82 setup \<open>KEStore_Elems.add_mets
1.83 [Specify.prep_met thy "met_polyeq" [] Celem.e_metID
1.84 @@ -993,16 +926,7 @@
1.85 ("#Find" ,["solutions v_v'i'"])],
1.86 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls, calc=[],
1.87 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
1.88 - @{thm normalize_poly_eq.simps}
1.89 - (*"Script Normalize_poly (e_e::bool) (v_v::real) = " ^
1.90 - "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
1.91 - " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
1.92 - " (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@ " ^
1.93 - " (Try (Repeat (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.94 - " ''make_ratpoly_in'' False))) @@ " ^
1.95 - " (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e " ^
1.96 - " in (SubProblem (''PolyEq'',[''polynomial'',''univariate'',''equation''], [''no_met'']) " ^
1.97 - " [BOOL e_e, REAL v_v]))"*))]
1.98 + @{thm normalize_poly_eq.simps})]
1.99 \<close>
1.100
1.101 partial_function (tailrec) solve_poly_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.102 @@ -1019,11 +943,7 @@
1.103 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
1.104 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.105 nrls = norm_Rational},
1.106 - @{thm solve_poly_equ.simps}
1.107 - (*"Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.108 - "(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.109 - " ''d0_polyeq_simplify'' False))) e_e " ^
1.110 - " in ((Or_to_List e_e)::bool list))"*))]
1.111 + @{thm solve_poly_equ.simps})]
1.112 \<close>
1.113
1.114 partial_function (tailrec) solve_poly_eq1 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.115 @@ -1042,14 +962,7 @@
1.116 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
1.117 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.118 nrls = norm_Rational},
1.119 - @{thm solve_poly_eq1.simps}
1.120 - (*"Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.121 - "(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.122 - " ''d1_polyeq_simplify'' True)) @@ " ^
1.123 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.124 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
1.125 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.126 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
1.127 + @{thm solve_poly_eq1.simps})]
1.128 \<close>
1.129
1.130 partial_function (tailrec) solve_poly_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.131 @@ -1071,17 +984,7 @@
1.132 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
1.133 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.134 nrls = norm_Rational},
1.135 - @{thm solve_poly_equ2.simps}
1.136 - (*"Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.137 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.138 - " ''d2_polyeq_simplify'' True)) @@ " ^
1.139 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.140 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.141 - " ''d1_polyeq_simplify'' True)) @@ " ^
1.142 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.143 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
1.144 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.145 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
1.146 + @{thm solve_poly_equ2.simps})]
1.147 \<close>
1.148
1.149 partial_function (tailrec) solve_poly_equ0 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.150 @@ -1103,17 +1006,7 @@
1.151 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
1.152 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.153 nrls = norm_Rational},
1.154 - @{thm solve_poly_equ0.simps}
1.155 - (*"Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
1.156 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.157 - " ''d2_polyeq_bdv_only_simplify'' True)) @@ " ^
1.158 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.159 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.160 - " ''d1_polyeq_simplify'' True)) @@ " ^
1.161 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.162 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
1.163 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.164 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
1.165 + @{thm solve_poly_equ0.simps})]
1.166 \<close>
1.167
1.168 partial_function (tailrec) solve_poly_equ_sqrt :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.169 @@ -1134,14 +1027,7 @@
1.170 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
1.171 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.172 nrls = norm_Rational},
1.173 - @{thm solve_poly_equ_sqrt.simps}
1.174 - (*"Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
1.175 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.176 - " ''d2_polyeq_sq_only_simplify'' True)) @@ " ^
1.177 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.178 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e; " ^
1.179 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.180 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
1.181 + @{thm solve_poly_equ_sqrt.simps})]
1.182 \<close>
1.183
1.184 partial_function (tailrec) solve_poly_equ_pq :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.185 @@ -1160,14 +1046,7 @@
1.186 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
1.187 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.188 nrls = norm_Rational},
1.189 - @{thm solve_poly_equ_pq.simps}
1.190 - (*"Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
1.191 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.192 - " ''d2_polyeq_pqFormula_simplify'' True)) @@ " ^
1.193 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.194 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
1.195 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.196 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
1.197 + @{thm solve_poly_equ_pq.simps})]
1.198 \<close>
1.199
1.200 partial_function (tailrec) solve_poly_equ_abc :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.201 @@ -1187,14 +1066,7 @@
1.202 {rew_ord'="termlessI", rls'=PolyEq_erls,srls=Rule.e_rls, prls=PolyEq_prls,
1.203 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.204 nrls = norm_Rational},
1.205 - @{thm solve_poly_equ_abc.simps}
1.206 - (*"Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
1.207 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.208 - " ''d2_polyeq_abcFormula_simplify'' True)) @@ " ^
1.209 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.210 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
1.211 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.212 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
1.213 + @{thm solve_poly_equ_abc.simps})]
1.214 \<close>
1.215
1.216 partial_function (tailrec) solve_poly_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.217 @@ -1217,20 +1089,7 @@
1.218 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
1.219 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.220 nrls = norm_Rational},
1.221 - @{thm solve_poly_equ3.simps}
1.222 - (*"Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.223 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.224 - " ''d3_polyeq_simplify'' True)) @@ " ^
1.225 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.226 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.227 - " ''d2_polyeq_simplify'' True)) @@ " ^
1.228 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.229 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
1.230 - " ''d1_polyeq_simplify'' True)) @@ " ^
1.231 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
1.232 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
1.233 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.234 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
1.235 + @{thm solve_poly_equ3.simps})]
1.236 \<close>
1.237 (*.solves all expanded (ie. normalised) terms of degree 2.*)
1.238 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
1.239 @@ -1259,21 +1118,7 @@
1.240 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=Rule.e_rls,prls=PolyEq_prls,
1.241 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.242 nrls = norm_Rational},
1.243 - @{thm solve_by_completing_square.simps}
1.244 - (*"Script Complete_square (e_e::bool) (v_v::real) = " ^
1.245 - "(let e_e = " ^
1.246 - " ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''cancel_leading_coeff'' True)) " ^
1.247 - " @@ (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''complete_square'' True)) " ^
1.248 - " @@ (Try (Rewrite ''square_explicit1'' False)) " ^
1.249 - " @@ (Try (Rewrite ''square_explicit2'' False)) " ^
1.250 - " @@ (Rewrite ''root_plus_minus'' True) " ^
1.251 - " @@ (Try (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''bdv_explicit1'' False))) " ^
1.252 - " @@ (Try (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''bdv_explicit2'' False))) " ^
1.253 - " @@ (Try (Repeat " ^
1.254 - " (Rewrite_Inst [(''bdv'',v_v)] ''bdv_explicit3'' False))) " ^
1.255 - " @@ (Try (Rewrite_Set ''calculate_RootRat'' False)) " ^
1.256 - " @@ (Try (Repeat (Calculate ''SQRT'')))) e_e " ^
1.257 - " in ((Or_to_List e_e)::bool list))"*))]
1.258 + @{thm solve_by_completing_square.simps})]
1.259 \<close>
1.260
1.261 ML\<open>