1.1 --- a/src/Tools/isac/Knowledge/Test.thy Sat Jun 22 13:15:52 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sat Jun 22 14:34:06 2019 +0200
1.3 @@ -14,36 +14,7 @@
1.4
1.5 theory Test imports Base_Tools Poly Rational Root Diff begin
1.6
1.7 -section \<open>consts\<close>
1.8 -subsection \<open>for scripts\<close>
1.9 -consts
1.10 - Solve'_univar'_err
1.11 - :: "[bool,real,bool,
1.12 - bool list] => bool list"
1.13 - ("((Script Solve'_univar'_err (_ _ _ =))// (_))" 9)
1.14 - Solve'_linear
1.15 - :: "[bool,real,
1.16 - bool list] => bool list"
1.17 - ("((Script Solve'_linear (_ _ =))// (_))" 9)
1.18 - Solve'_root'_equation
1.19 - :: "[bool,real,
1.20 - bool list] => bool list"
1.21 - ("((Script Solve'_root'_equation (_ _ =))// (_))" 9)
1.22 - Solve'_plain'_square
1.23 - :: "[bool,real,
1.24 - bool list] => bool list"
1.25 - ("((Script Solve'_plain'_square (_ _ =))// (_))" 9)
1.26 - Norm'_univar'_equation
1.27 - :: "[bool,real,
1.28 - bool] => bool"
1.29 - ("((Script Norm'_univar'_equation (_ _ =))// (_))" 9)
1.30 - STest'_simplify
1.31 - :: "['z,
1.32 - 'z] => 'z"
1.33 - ("((Script STest'_simplify (_ =))// (_))" 9)
1.34 -
1.35 -
1.36 -subsection \<open>for problems\<close>
1.37 +section \<open>consts for problems\<close>
1.38 consts
1.39 "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
1.40 "contains'_root" :: "'a => bool" ("contains'_root _" 10)
1.41 @@ -885,13 +856,7 @@
1.42 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,
1.43 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
1.44 nrls = Test_simplify},
1.45 - @{thm solve_linear.simps}
1.46 - (*"Script Solve_linear (e_e::bool) (v_v::real)= " ^
1.47 - "(let e_e = " ^
1.48 - " Repeat " ^
1.49 - " (((Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@ " ^
1.50 - " (Rewrite_Set ''Test_simplify'' False))) e_e" ^
1.51 - " in [e_e::bool])"*))]
1.52 + @{thm solve_linear.simps})]
1.53 \<close>
1.54 subsection \<open>root equation\<close>
1.55
1.56 @@ -924,69 +889,8 @@
1.57 [Rule.Calc ("Test.contains'_root",eval_contains_root "")],
1.58 calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
1.59 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.60 - @{thm solve_root_equ.simps}
1.61 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.62 - "(let e_e = " ^
1.63 - " ((While (contains_root e_e) Do" ^
1.64 - " ((Rewrite ''square_equation_left'' True) @@" ^
1.65 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
1.66 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
1.67 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
1.68 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
1.69 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
1.70 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
1.71 - " (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^
1.72 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
1.73 - " e_e" ^
1.74 - " in [e_e::bool])"*))]
1.75 + @{thm solve_root_equ.simps})]
1.76 \<close>
1.77 -(* UNUSED?
1.78 -partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.79 - where "solve_root_equ e_e v_v =
1.80 -(let e_e =
1.81 - ((While (contains_root e_e) Do
1.82 - ((Rewrite ''square_equation_left'' True) @@
1.83 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
1.84 - (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
1.85 - (Try (Rewrite_Set ''isolate_root'' False)) @@
1.86 - (Try (Rewrite_Set ''Test_simplify'' False)))) @@
1.87 - (Try (Rewrite_Set ''norm_equation'' False)) @@
1.88 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
1.89 - (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@
1.90 - (Try (Rewrite_Set ''Test_simplify'' False)))
1.91 - e_e;
1.92 - (L_L::bool list) = Tac ''subproblem_equation_dummy'';
1.93 - L_L = Tac ''solve_equation_dummy''
1.94 - in Check_elementwise L_L {(v_v::real). Assumptions}) "
1.95 -setup \<open>KEStore_Elems.add_mets
1.96 - [Specify.prep_met thy "met_test_sqrt2" [] Celem.e_metID
1.97 - (*root-equation ... for test-*.sml until 8.01*)
1.98 - (["Test","squ-equ-test2"],
1.99 - [("#Given" ,["equality e_e","solveFor v_v"]),
1.100 - ("#Find" ,["solutions v_v'i'"])],
1.101 - {rew_ord'="e_rew_ord",rls'=tval_rls,
1.102 - srls = Rule.append_rls "srls_contains_root" Rule.e_rls
1.103 - [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
1.104 - prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],
1.105 - asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.106 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.107 - "(let e_e = " ^
1.108 - " ((While (contains_root e_e) Do" ^
1.109 - " ((Rewrite ''square_equation_left'' True) @@" ^
1.110 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
1.111 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
1.112 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
1.113 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
1.114 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
1.115 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
1.116 - " (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^
1.117 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
1.118 - " e_e;" ^
1.119 - " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
1.120 - " L_L = Tac solve_equation_dummy " ^
1.121 - " in Check_elementwise L_L {(v_v::real). Assumptions})")]
1.122 -\<close>
1.123 -*)
1.124
1.125 partial_function (tailrec) minisubpbl ::
1.126 "bool \<Rightarrow> real \<Rightarrow> bool list"
1.127 @@ -1008,16 +912,7 @@
1.128 prls = Rule.append_rls "prls_met_test_squ_sub" Rule.e_rls
1.129 [Rule.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
1.130 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
1.131 - @{thm minisubpbl.simps}
1.132 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.133 - " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@ " ^
1.134 - " (Try (Rewrite_Set ''Test_simplify'' False))) e_e; " ^
1.135 - " (L_L::bool list) = " ^
1.136 - " (SubProblem (''Test'', " ^
1.137 - " [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
1.138 - " [''Test'', ''solve_linear'']) " ^
1.139 - " [BOOL e_e, REAL v_v]) " ^
1.140 - " in Check_elementwise L_L {(v_v::real). Assumptions}) "*))]
1.141 + @{thm minisubpbl.simps})]
1.142 \<close>
1.143
1.144 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.145 @@ -1045,21 +940,7 @@
1.146 [Rule.Calc ("Test.contains'_root",eval_contains_root"")], prls=Rule.e_rls, calc=[], crls=tval_rls,
1.147 errpats = [], nrls = Rule.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
1.148 ("square_equation_right","")]*)},
1.149 - @{thm solve_root_equ2.simps}
1.150 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.151 - "(let e_e = " ^
1.152 - " ((While (contains_root e_e) Do" ^
1.153 - " ((Rewrite ''square_equation_left'' True) @@" ^
1.154 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
1.155 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
1.156 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
1.157 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
1.158 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
1.159 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
1.160 - " e_e;" ^
1.161 - " (L_L::bool list) = (SubProblem (''Test'',[''LINEAR'',''univariate'',''equation'',''test'']," ^
1.162 - " [''Test'',''solve_linear'']) [BOOL e_e, REAL v_v])" ^
1.163 - " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
1.164 + @{thm solve_root_equ2.simps})]
1.165 \<close>
1.166
1.167 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.168 @@ -1089,22 +970,7 @@
1.169 [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
1.170 prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],
1.171 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.172 - @{thm solve_root_equ3.simps}
1.173 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.174 - "(let e_e = " ^
1.175 - " ((While (contains_root e_e) Do" ^
1.176 - " (((Rewrite ''square_equation_left'' True) Or " ^
1.177 - " (Rewrite ''square_equation_right'' True)) @@" ^
1.178 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
1.179 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
1.180 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
1.181 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
1.182 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
1.183 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
1.184 - " e_e;" ^
1.185 - " (L_L::bool list) = (SubProblem (''Test'',[''plain_square'',''univariate'',''equation'',''test'']," ^
1.186 - " [''Test'',''solve_plain_square'']) [BOOL e_e, REAL v_v])" ^
1.187 - " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
1.188 + @{thm solve_root_equ3.simps})]
1.189 \<close>
1.190
1.191 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.192 @@ -1134,22 +1000,7 @@
1.193 [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
1.194 prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
1.195 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
1.196 - @{thm solve_root_equ4.simps}
1.197 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.198 - "(let e_e = " ^
1.199 - " ((While (contains_root e_e) Do" ^
1.200 - " (((Rewrite ''square_equation_left'' True) Or" ^
1.201 - " (Rewrite ''square_equation_right'' True)) @@" ^
1.202 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
1.203 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
1.204 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
1.205 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
1.206 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
1.207 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
1.208 - " e_e;" ^
1.209 - " (L_L::bool list) = (SubProblem (''Test'',[''univariate'',''equation'',''test'']," ^
1.210 - " [''no_met'']) [BOOL e_e, REAL v_v])" ^
1.211 - " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
1.212 + @{thm solve_root_equ4.simps})]
1.213 \<close>
1.214
1.215 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
1.216 @@ -1174,14 +1025,7 @@
1.217 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule.e_rls,
1.218 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,
1.219 asm_rls=[],asm_thm=[]*)},
1.220 - @{thm solve_plain_square.simps}
1.221 - (*"Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
1.222 - " (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@ " ^
1.223 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@ " ^
1.224 - " ((Rewrite ''square_equality_0'' False) Or " ^
1.225 - " (Rewrite ''square_equality'' True)) @@ " ^
1.226 - " (Try (Rewrite_Set ''tval_rls'' False))) e_e " ^
1.227 - " in ((Or_to_List e_e)::bool list))"*))]
1.228 + @{thm solve_plain_square.simps})]
1.229 \<close>
1.230 subsection \<open>polynomial equation\<close>
1.231
1.232 @@ -1200,12 +1044,7 @@
1.233 ("#Find" ,["solutions v_v'i'"])],
1.234 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule.e_rls,prls=Rule.e_rls, calc=[], crls=tval_rls,
1.235 errpats = [], nrls = Rule.e_rls},
1.236 - @{thm norm_univariate_equ.simps}
1.237 - (*"Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
1.238 - " (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@ " ^
1.239 - " (Try (Rewrite_Set ''Test_simplify'' False))) e_e " ^
1.240 - " in (SubProblem (''Test'',[''univariate'',''equation'',''test''], " ^
1.241 - " [''no_met'']) [BOOL e_e, REAL v_v]))"*))]
1.242 + @{thm norm_univariate_equ.simps})]
1.243 \<close>
1.244 subsection \<open>diophantine equation\<close>
1.245
1.246 @@ -1223,11 +1062,7 @@
1.247 ("#Find" ,["intTestFind s_s"])],
1.248 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
1.249 crls = tval_rls, errpats = [], nrls = Test_simplify},
1.250 - @{thm test_simplify.simps}
1.251 - (*"Script STest_simplify (t_t::int) = " ^
1.252 - "(Repeat " ^
1.253 - " ((Try (Calculate ''PLUS'')) @@ " ^
1.254 - " (Try (Calculate ''TIMES''))) t_t::int)"*))]
1.255 + @{thm test_simplify.simps})]
1.256 \<close>
1.257
1.258 end